Theory AOT_syntax
1
2theory AOT_syntax
3 imports AOT_commands
4 keywords "AOT_register_variable_names" :: thy_decl
5 and "AOT_register_metavariable_names" :: thy_decl
6 and "AOT_register_premise_set_names" :: thy_decl
7 and "AOT_register_type_constraints" :: thy_decl
8 abbrevs "actually" = "❙𝒜"
9 and "neccessarily" = "□"
10 and "possibly" = "◇"
11 and "the" = "❙ι"
12 and "lambda" = "[λ]"
13 and "being such that" = "[λ ]"
14 and "forall" = "∀"
15 and "exists" = "∃"
16 and "equivalent" = "≡"
17 and "not" = "¬"
18 and "implies" = "→"
19 and "equal" = "="
20 and "by definition" = "⇩d⇩f"
21 and "df" = "⇩d⇩f"
22 and "denotes" = "↓"
23begin
24
25
26section‹Approximation of the Syntax of PLM›
27
28locale AOT_meta_syntax
29begin
30notation AOT_model_valid_in ("❙[_ ❙⊨ _❙]")
31notation AOT_model_axiom ("❙□❙[_❙]")
32notation AOT_model_act_axiom ("❙𝒜❙[_❙]")
33end
34locale AOT_no_meta_syntax
35begin
36no_notation AOT_model_valid_in ("❙[_ ❙⊨ _❙]")
37no_notation AOT_model_axiom ("❙□❙[_❙]")
38no_notation AOT_model_act_axiom ("❙𝒜❙[_❙]")
39end
40
41consts AOT_denotes :: ‹'a::AOT_Term ⇒ 𝗈›
42 AOT_imp :: ‹[𝗈, 𝗈] ⇒ 𝗈›
43 AOT_not :: ‹𝗈 ⇒ 𝗈›
44 AOT_box :: ‹𝗈 ⇒ 𝗈›
45 AOT_act :: ‹𝗈 ⇒ 𝗈›
46 AOT_forall :: ‹('a::AOT_Term ⇒ 𝗈) ⇒ 𝗈›
47 AOT_eq :: ‹'a::AOT_Term ⇒ 'a::AOT_Term ⇒ 𝗈›
48 AOT_desc :: ‹('a::AOT_UnaryIndividualTerm ⇒ 𝗈) ⇒ 'a›
49 AOT_exe :: ‹<'a::AOT_IndividualTerm> ⇒ 'a ⇒ 𝗈›
50 AOT_lambda :: ‹('a::AOT_IndividualTerm ⇒ 𝗈) ⇒ <'a>›
51 AOT_lambda0 :: ‹𝗈 ⇒ 𝗈›
52 AOT_concrete :: ‹<'a::AOT_UnaryIndividualTerm> AOT_var›
53
54nonterminal κ⇩s and Π and Π0 and α and exe_arg and exe_args
55 and lambda_args and desc and free_var and free_vars
56 and AOT_props and AOT_premises and AOT_world_relative_prop
57
58syntax "_AOT_process_frees" :: ‹φ ⇒ φ'› ("_")
59 "_AOT_verbatim" :: ‹any ⇒ φ› (‹«_»›)
60 "_AOT_verbatim" :: ‹any ⇒ τ› (‹«_»›)
61 "_AOT_quoted" :: ‹φ' ⇒ any› (‹«_»›)
62 "_AOT_quoted" :: ‹τ' ⇒ any› (‹«_»›)
63 "" :: ‹φ ⇒ φ› (‹'(_')›)
64 "_AOT_process_frees" :: ‹τ ⇒ τ'› ("_")
65 "" :: ‹κ⇩s ⇒ τ› ("_")
66 "" :: ‹Π ⇒ τ› ("_")
67 "" :: ‹φ ⇒ τ› ("'(_')")
68 "_AOT_term_var" :: ‹id_position ⇒ τ› ("_")
69 "_AOT_term_var" :: ‹id_position ⇒ φ› ("_")
70 "_AOT_exe_vars" :: ‹id_position ⇒ exe_arg› ("_")
71 "_AOT_lambda_vars" :: ‹id_position ⇒ lambda_args› ("_")
72 "_AOT_var" :: ‹id_position ⇒ α› ("_")
73 "_AOT_vars" :: ‹id_position ⇒ any›
74 "_AOT_verbatim" :: ‹any ⇒ α› (‹«_»›)
75 "_AOT_valid" :: ‹w ⇒ φ' ⇒ bool› (‹[_ ⊨ _]›)
76 "_AOT_denotes" :: ‹τ ⇒ φ› (‹_↓›)
77 "_AOT_imp" :: ‹[φ, φ] ⇒ φ› (infixl ‹→› 25)
78 "_AOT_not" :: ‹φ ⇒ φ› (‹~_› [50] 50)
79 "_AOT_not" :: ‹φ ⇒ φ› (‹¬_› [50] 50)
80 "_AOT_box" :: ‹φ ⇒ φ› (‹□_› [49] 54)
81 "_AOT_act" :: ‹φ ⇒ φ› (‹❙𝒜_› [49] 54)
82 "_AOT_all" :: ‹α ⇒ φ ⇒ φ› (‹∀_ _› [1,40])
83syntax (input)
84 "_AOT_all_ellipse"
85 :: ‹id_position ⇒ id_position ⇒ φ ⇒ φ› (‹∀_...∀_ _› [1,40])
86syntax (output)
87 "_AOT_all_ellipse"
88 :: ‹id_position ⇒ id_position ⇒ φ ⇒ φ› (‹∀_...∀_'(_')› [1,40])
89syntax
90 "_AOT_eq" :: ‹[τ, τ] ⇒ φ› (infixl ‹=› 50)
91 "_AOT_desc" :: ‹α ⇒ φ ⇒ desc› ("❙ι__" [1,1000])
92 "" :: ‹desc ⇒ κ⇩s› ("_")
93 "_AOT_lambda" :: ‹lambda_args ⇒ φ ⇒ Π› (‹[λ_ _]›)
94 "_explicitRelation" :: ‹τ ⇒ Π› ("[_]")
95 "" :: ‹κ⇩s ⇒ exe_arg› ("_")
96 "" :: ‹exe_arg ⇒ exe_args› ("_")
97 "_AOT_exe_args" :: ‹exe_arg ⇒ exe_args ⇒ exe_args› ("__")
98 "_AOT_exe_arg_ellipse" :: ‹id_position ⇒ id_position ⇒ exe_arg› ("_..._")
99 "_AOT_lambda_arg_ellipse"
100 :: ‹id_position ⇒ id_position ⇒ lambda_args› ("_..._")
101 "_AOT_term_ellipse" :: ‹id_position ⇒ id_position ⇒ τ› ("_..._")
102 "_AOT_exe" :: ‹Π ⇒ exe_args ⇒ φ› (‹__›)
103 "_AOT_enc" :: ‹exe_args ⇒ Π ⇒ φ› (‹__›)
104 "_AOT_lambda0" :: ‹φ ⇒ Π0› (‹[λ _]›)
105 "" :: ‹Π0 ⇒ φ› ("_")
106 "" :: ‹Π0 ⇒ τ› ("_")
107 "_AOT_concrete" :: ‹Π› (‹E!›)
108 "" :: ‹any ⇒ exe_arg› ("«_»")
109 "" :: ‹desc ⇒ free_var› ("_")
110 "" :: ‹Π ⇒ free_var› ("_")
111 "_AOT_appl" :: ‹id_position ⇒ free_vars ⇒ φ› ("_'{_'}")
112 "_AOT_appl" :: ‹id_position ⇒ free_vars ⇒ τ› ("_'{_'}")
113 "_AOT_appl" :: ‹id_position ⇒ free_vars ⇒ free_vars› ("_'{_'}")
114 "_AOT_appl" :: ‹id_position ⇒ free_vars ⇒ free_vars› ("_'{_'}")
115 "_AOT_term_var" :: ‹id_position ⇒ free_var› ("_")
116 "" :: ‹any ⇒ free_var› ("«_»")
117 "" :: ‹free_var ⇒ free_vars› ("_")
118 "_AOT_args" :: ‹free_var ⇒ free_vars ⇒ free_vars› ("_,_")
119 "_AOT_free_var_ellipse" :: ‹id_position ⇒ id_position ⇒ free_var› ("_..._")
120syntax "_AOT_premises"
121 :: ‹AOT_world_relative_prop ⇒ AOT_premises ⇒ AOT_premises› (infixr ‹,› 3)
122 "_AOT_world_relative_prop" :: "φ ⇒ AOT_world_relative_prop" ("_")
123 "" :: "AOT_world_relative_prop ⇒ AOT_premises" ("_")
124 "_AOT_prop" :: ‹AOT_world_relative_prop ⇒ AOT_prop› (‹_›)
125 "" :: ‹AOT_prop ⇒ AOT_props› (‹_›)
126 "_AOT_derivable" :: "AOT_premises ⇒ φ' ⇒ AOT_prop" (infixl ‹❙⊢› 2)
127 "_AOT_nec_derivable" :: "AOT_premises ⇒ φ' ⇒ AOT_prop" (infixl ‹❙⊢⇩□› 2)
128 "_AOT_theorem" :: "φ' ⇒ AOT_prop" (‹❙⊢ _›)
129 "_AOT_nec_theorem" :: "φ' ⇒ AOT_prop" (‹❙⊢⇩□ _›)
130 "_AOT_equiv_def" :: ‹φ ⇒ φ ⇒ AOT_prop› (infixl ‹≡⇩d⇩f› 3)
131 "_AOT_axiom" :: "φ' ⇒ AOT_axiom" (‹_›)
132 "_AOT_act_axiom" :: "φ' ⇒ AOT_act_axiom" (‹_›)
133 "_AOT_axiom" :: "φ' ⇒ AOT_prop" (‹_ ∈ Λ⇩□›)
134 "_AOT_act_axiom" :: "φ' ⇒ AOT_prop" (‹_ ∈ Λ›)
135 "_AOT_id_def" :: ‹τ ⇒ τ ⇒ AOT_prop› (infixl ‹=⇩d⇩f› 3)
136 "_AOT_for_arbitrary"
137 :: ‹id_position ⇒ AOT_prop ⇒ AOT_prop› (‹for arbitrary _: _› [1000,1] 1)
138syntax (output) "_lambda_args" :: ‹any ⇒ patterns ⇒ patterns› ("__")
139
140translations
141 "[w ⊨ φ]" => "CONST AOT_model_valid_in w φ"
142
143AOT_syntax_print_translations
144 "[w ⊨ φ]" <= "CONST AOT_model_valid_in w φ"
145
146ML_file AOT_syntax.ML
147
148AOT_register_type_constraints
149 Individual: ‹_::AOT_UnaryIndividualTerm› ‹_::AOT_IndividualTerm› and
150 Proposition: 𝗈 and
151 Relation: ‹<_::AOT_IndividualTerm>› and
152 Term: ‹_::AOT_Term›
153
154AOT_register_variable_names
155 Individual: x y z ν μ a b c d and
156 Proposition: p q r s and
157 Relation: F G H P Q R S and
158 Term: α β γ δ
159
160AOT_register_metavariable_names
161 Individual: κ and
162 Proposition: φ ψ χ θ ζ ξ Θ and
163 Relation: Π and
164 Term: τ σ
165
166AOT_register_premise_set_names Γ Δ Λ
167
168parse_ast_translation‹[
169 (\<^syntax_const>‹_AOT_var›, K AOT_check_var),
170 (\<^syntax_const>‹_AOT_exe_vars›, K AOT_split_exe_vars),
171 (\<^syntax_const>‹_AOT_lambda_vars›, K AOT_split_lambda_args)
172]›
173
174translations
175 "_AOT_denotes τ" => "CONST AOT_denotes τ"
176 "_AOT_imp φ ψ" => "CONST AOT_imp φ ψ"
177 "_AOT_not φ" => "CONST AOT_not φ"
178 "_AOT_box φ" => "CONST AOT_box φ"
179 "_AOT_act φ" => "CONST AOT_act φ"
180 "_AOT_eq τ τ'" => "CONST AOT_eq τ τ'"
181 "_AOT_lambda0 φ" => "CONST AOT_lambda0 φ"
182 "_AOT_concrete" => "CONST AOT_term_of_var (CONST AOT_concrete)"
183 "_AOT_lambda α φ" => "CONST AOT_lambda (_abs α φ)"
184 "_explicitRelation Π" => "Π"
185
186AOT_syntax_print_translations
187 "_AOT_lambda (_lambda_args x y) φ" <= "CONST AOT_lambda (_abs (_pattern x y) φ)"
188 "_AOT_lambda (_lambda_args x y) φ" <= "CONST AOT_lambda (_abs (_patterns x y) φ)"
189 "_AOT_lambda x φ" <= "CONST AOT_lambda (_abs x φ)"
190 "_lambda_args x (_lambda_args y z)" <= "_lambda_args x (_patterns y z)"
191 "_lambda_args (x y z)" <= "_lambda_args (_tuple x (_tuple_arg (_tuple y z)))"
192
193
194AOT_syntax_print_translations
195 "_AOT_imp φ ψ" <= "CONST AOT_imp φ ψ"
196 "_AOT_not φ" <= "CONST AOT_not φ"
197 "_AOT_box φ" <= "CONST AOT_box φ"
198 "_AOT_act φ" <= "CONST AOT_act φ"
199 "_AOT_all α φ" <= "CONST AOT_forall (_abs α φ)"
200 "_AOT_all α φ" <= "CONST AOT_forall (λα. φ)"
201 "_AOT_eq τ τ'" <= "CONST AOT_eq τ τ'"
202 "_AOT_desc x φ" <= "CONST AOT_desc (_abs x φ)"
203 "_AOT_desc x φ" <= "CONST AOT_desc (λx. φ)"
204 "_AOT_lambda0 φ" <= "CONST AOT_lambda0 φ"
205 "_AOT_concrete" <= "CONST AOT_term_of_var (CONST AOT_concrete)"
206
207translations
208 "_AOT_appl φ (_AOT_args a b)" => "_AOT_appl (φ a) b"
209 "_AOT_appl φ a" => "φ a"
210
211
212parse_translation‹
213[
214 (\<^syntax_const>‹_AOT_var›, parseVar true),
215 (\<^syntax_const>‹_AOT_vars›, parseVar false),
216 (\<^syntax_const>‹_AOT_valid›, fn ctxt => fn [w,x] =>
217 \<^const>‹AOT_model_valid_in› $ w $ x),
218 (\<^syntax_const>‹_AOT_quoted›, fn ctxt => fn [x] => x),
219 (\<^syntax_const>‹_AOT_process_frees›, fn ctxt => fn [x] => processFrees ctxt x),
220 (\<^syntax_const>‹_AOT_world_relative_prop›, fn ctxt => fn [x] => let
221 val (x, premises) = processFreesAndPremises ctxt x
222 val (world::formulas) = Variable.variant_frees ctxt [x]
223 (("v", dummyT)::(map (fn _ => ("φ", dummyT)) premises))
224 val term = HOLogic.mk_Trueprop
225 (@{const AOT_model_valid_in} $ Free world $ processFrees ctxt x)
226 val term = fold (fn (premise,form) => fn trm =>
227 @{const "Pure.imp"} $
228 HOLogic.mk_Trueprop
229 (Const (\<^const_name>‹Set.member›, dummyT) $ Free form $ premise) $
230 (Term.absfree (Term.dest_Free (dropConstraints premise)) trm $ Free form)
231 ) (ListPair.zipEq (premises,formulas)) term
232 val term = fold (fn (form) => fn trm =>
233 Const (\<^const_name>‹Pure.all›, dummyT) $
234 (Term.absfree form trm)
235 ) formulas term
236 val term = Term.absfree world term
237 in term end),
238 (\<^syntax_const>‹_AOT_prop›, fn ctxt => fn [x] => let
239 val world = case (AOT_ProofData.get ctxt) of SOME w => w
240 | _ => raise Fail "Expected world to be stored in the proof state."
241 in x $ world end),
242 (\<^syntax_const>‹_AOT_theorem›, fn ctxt => fn [x] =>
243 HOLogic.mk_Trueprop (@{const AOT_model_valid_in} $ @{const w⇩0} $ x)),
244 (\<^syntax_const>‹_AOT_axiom›, fn ctxt => fn [x] =>
245 HOLogic.mk_Trueprop (@{const AOT_model_axiom} $ x)),
246 (\<^syntax_const>‹_AOT_act_axiom›, fn ctxt => fn [x] =>
247 HOLogic.mk_Trueprop (@{const AOT_model_act_axiom} $ x)),
248 (\<^syntax_const>‹_AOT_nec_theorem›, fn ctxt => fn [trm] => let
249 val world = singleton (Variable.variant_frees ctxt [trm]) ("v", @{typ w})
250 val trm = HOLogic.mk_Trueprop (@{const AOT_model_valid_in} $ Free world $ trm)
251 val trm = Term.absfree world trm
252 val trm = Const (\<^const_name>‹Pure.all›, dummyT) $ trm
253 in trm end),
254 (\<^syntax_const>‹_AOT_derivable›, fn ctxt => fn [x,y] => let
255 val world = case (AOT_ProofData.get ctxt) of SOME w => w
256 | _ => raise Fail "Expected world to be stored in the proof state."
257 in foldPremises world x y end),
258 (\<^syntax_const>‹_AOT_nec_derivable›, fn ctxt => fn [x,y] => let
259 in Const (\<^const_name>‹Pure.all›, dummyT) $
260 Abs ("v", dummyT, foldPremises (Bound 0) x y) end),
261 (\<^syntax_const>‹_AOT_for_arbitrary›, fn ctxt => fn [_ $ var $ pos,trm] => let
262 val trm = Const (\<^const_name>‹Pure.all›, dummyT) $
263 (Const ("_constrainAbs", dummyT) $ Term.absfree (Term.dest_Free var) trm $ pos)
264 in trm end),
265 (\<^syntax_const>‹_AOT_equiv_def›, parseEquivDef),
266 (\<^syntax_const>‹_AOT_exe›, parseExe),
267 (\<^syntax_const>‹_AOT_enc›, parseEnc)
268]
269›
270
271parse_ast_translation‹
272[
273 (\<^syntax_const>‹_AOT_exe_arg_ellipse›, parseEllipseList "_AOT_term_vars"),
274 (\<^syntax_const>‹_AOT_lambda_arg_ellipse›, parseEllipseList "_AOT_vars"),
275 (\<^syntax_const>‹_AOT_free_var_ellipse›, parseEllipseList "_AOT_term_vars"),
276 (\<^syntax_const>‹_AOT_term_ellipse›, parseEllipseList "_AOT_term_vars"),
277 (\<^syntax_const>‹_AOT_all_ellipse›, fn ctx => fn [a,b,c] =>
278 Ast.mk_appl (Ast.Constant \<^const_name>‹AOT_forall›) [
279 Ast.mk_appl (Ast.Constant "_abs") [parseEllipseList "_AOT_vars" ctx [a,b],c]
280 ])
281]
282›
283
284syntax (output)
285 "_AOT_individual_term" :: ‹'a ⇒ tuple_args› ("_")
286 "_AOT_individual_terms" :: ‹tuple_args ⇒ tuple_args ⇒ tuple_args› ("__")
287 "_AOT_relation_term" :: ‹'a ⇒ Π›
288 "_AOT_any_term" :: ‹'a ⇒ τ›
289
290
291print_ast_translation‹AOT_syntax_print_ast_translations[
292 (\<^syntax_const>‹_AOT_individual_term›, AOT_print_individual_term),
293 (\<^syntax_const>‹_AOT_relation_term›, AOT_print_relation_term),
294 (\<^syntax_const>‹_AOT_any_term›, AOT_print_generic_term)
295]›
296
297AOT_syntax_print_translations
298 "_AOT_individual_terms (_AOT_individual_term x) (_AOT_individual_terms (_tuple y z))"
299 <= "_AOT_individual_terms (_tuple x (_tuple_args y z))"
300 "_AOT_individual_terms (_AOT_individual_term x) (_AOT_individual_term y)"
301 <= "_AOT_individual_terms (_tuple x (_tuple_arg y))"
302 "_AOT_individual_terms (_tuple x y)" <= "_AOT_individual_term (_tuple x y)"
303 "_AOT_exe (_AOT_relation_term Π) (_AOT_individual_term κ)" <= "CONST AOT_exe Π κ"
304 "_AOT_denotes (_AOT_any_term κ)" <= "CONST AOT_denotes κ"
305
306AOT_define AOT_conj :: ‹[φ, φ] ⇒ φ› (infixl ‹&› 35) ‹φ & ψ ≡⇩d⇩f ¬(φ → ¬ψ)›
307declare "AOT_conj"[AOT del, AOT_defs del]
308AOT_define AOT_disj :: ‹[φ, φ] ⇒ φ› (infixl ‹∨› 35) ‹φ ∨ ψ ≡⇩d⇩f ¬φ → ψ›
309declare "AOT_disj"[AOT del, AOT_defs del]
310AOT_define AOT_equiv :: ‹[φ, φ] ⇒ φ› (infix ‹≡› 20) ‹φ ≡ ψ ≡⇩d⇩f (φ → ψ) & (ψ → φ)›
311declare "AOT_equiv"[AOT del, AOT_defs del]
312AOT_define AOT_dia :: ‹φ ⇒ φ› (‹◇_› [49] 54) ‹◇φ ≡⇩d⇩f ¬□¬φ›
313declare "AOT_dia"[AOT del, AOT_defs del]
314
315context AOT_meta_syntax
316begin
317notation AOT_dia ("❙◇_" [49] 54)
318notation AOT_conj (infixl ‹❙&› 35)
319notation AOT_disj (infixl ‹❙∨› 35)
320notation AOT_equiv (infixl ‹❙≡› 20)
321end
322context AOT_no_meta_syntax
323begin
324no_notation AOT_dia ("❙◇_" [49] 54)
325no_notation AOT_conj (infixl ‹❙&› 35)
326no_notation AOT_disj (infixl ‹❙∨› 35)
327no_notation AOT_equiv (infixl ‹❙≡› 20)
328end
329
330
331print_translation ‹
332AOT_syntax_print_translations
333 [
334 AOT_preserve_binder_abs_tr'
335 \<^const_syntax>‹AOT_forall›
336 \<^syntax_const>‹_AOT_all›
337 (\<^syntax_const>‹_AOT_all_ellipse›, true)
338 \<^const_name>‹AOT_imp›,
339 AOT_binder_trans @{theory} @{binding "AOT_forall_binder"} \<^syntax_const>‹_AOT_all›,
340 Syntax_Trans.preserve_binder_abs_tr'
341 \<^const_syntax>‹AOT_desc›
342 \<^syntax_const>‹_AOT_desc›,
343 AOT_binder_trans @{theory} @{binding "AOT_desc_binder"} \<^syntax_const>‹_AOT_desc›,
344 AOT_preserve_binder_abs_tr'
345 \<^const_syntax>‹AOT_lambda›
346 \<^syntax_const>‹_AOT_lambda›
347 (\<^syntax_const>‹_AOT_lambda_arg_ellipse›, false)
348 \<^const_name>‹undefined›,
349 AOT_binder_trans
350 @{theory}
351 @{binding "AOT_lambda_binder"}
352 \<^syntax_const>‹_AOT_lambda›
353 ]
354›
355
356parse_translation‹
357[(\<^syntax_const>‹_AOT_id_def›, parseIdDef)]
358›
359
360parse_ast_translation‹[
361 (\<^syntax_const>‹_AOT_all›,
362 AOT_restricted_binder \<^const_name>‹AOT_forall› \<^const_name>‹AOT_imp›),
363 (\<^syntax_const>‹_AOT_desc›,
364 AOT_restricted_binder \<^const_name>‹AOT_desc› \<^const_name>‹AOT_conj›)
365]›
366
367AOT_define AOT_exists :: ‹α ⇒ φ ⇒ φ› ‹«AOT_exists φ» ≡⇩d⇩f ¬∀α ¬φ{α}›
368declare AOT_exists[AOT del, AOT_defs del]
369syntax "_AOT_exists" :: ‹α ⇒ φ ⇒ φ› ("∃_ _" [1,40])
370
371AOT_syntax_print_translations
372 "_AOT_exists α φ" <= "CONST AOT_exists (_abs α φ)"
373 "_AOT_exists α φ" <= "CONST AOT_exists (λα. φ)"
374
375parse_ast_translation‹
376[(\<^syntax_const>‹_AOT_exists›,
377 AOT_restricted_binder \<^const_name>‹AOT_exists› \<^const_name>‹AOT_conj›)]
378›
379
380context AOT_meta_syntax
381begin
382notation AOT_exists (binder "❙∃" 8)
383end
384context AOT_no_meta_syntax
385begin
386no_notation AOT_exists (binder "❙∃" 8)
387end
388
389
390syntax (input)
391 "_AOT_exists_ellipse" :: ‹id_position ⇒ id_position ⇒ φ ⇒ φ› (‹∃_...∃_ _› [1,40])
392syntax (output)
393 "_AOT_exists_ellipse" :: ‹id_position ⇒ id_position ⇒ φ ⇒ φ› (‹∃_...∃_ '(_')› [1,40])
394parse_ast_translation‹[(\<^syntax_const>‹_AOT_exists_ellipse›, fn ctx => fn [a,b,c] =>
395 Ast.mk_appl (Ast.Constant "AOT_exists")
396 [Ast.mk_appl (Ast.Constant "_abs") [parseEllipseList "_AOT_vars" ctx [a,b],c]])]›
397print_translation‹AOT_syntax_print_translations [
398 AOT_preserve_binder_abs_tr'
399 \<^const_syntax>‹AOT_exists›
400 \<^syntax_const>‹_AOT_exists›
401 (\<^syntax_const>‹_AOT_exists_ellipse›,true) \<^const_name>‹AOT_conj›,
402 AOT_binder_trans
403 @{theory}
404 @{binding "AOT_exists_binder"}
405 \<^syntax_const>‹_AOT_exists›
406]›
407
408
409
410syntax "_AOT_DDDOT" :: "φ" ("...")
411syntax "_AOT_DDDOT" :: "φ" ("…")
412parse_translation‹[(\<^syntax_const>‹_AOT_DDDOT›, parseDDOT)]›
413
414print_translation‹AOT_syntax_print_translations
415[(\<^const_syntax>‹Pure.all›, fn ctxt => fn [Abs (_, _,
416 Const (\<^const_syntax>‹HOL.Trueprop›, _) $
417 (Const (\<^const_syntax>‹AOT_model_valid_in›, _) $ Bound 0 $ y))] => let
418 val y = (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ y)
419 in (Const (\<^syntax_const>‹_AOT_nec_theorem›, dummyT) $ y) end
420| [p as Abs (name, _,
421 Const (\<^const_syntax>‹HOL.Trueprop›, _) $
422 (Const (\<^const_syntax>‹AOT_model_valid_in›, _) $ w $ y))]
423=> (Const (\<^syntax_const>‹_AOT_for_arbitrary›, dummyT) $
424 (Const ("_bound", dummyT) $ Free (name, dummyT)) $
425 (Term.betapply (p, (Const ("_bound", dummyT) $ Free (name, dummyT)))))
426),
427
428 (\<^const_syntax>‹AOT_model_valid_in›, fn ctxt =>
429 fn [w as (Const ("_free", _) $ Free (v, _)), y] => let
430 val is_world = (case (AOT_ProofData.get ctxt)
431 of SOME (Free (w, _)) => Name.clean w = Name.clean v | _ => false)
432 val y = (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ y)
433 in if is_world then y else Const (\<^syntax_const>‹_AOT_valid›, dummyT) $ w $ y end
434 | [Const (\<^const_syntax>‹w⇩0›, _), y] => let
435 val y = (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ y)
436 in case (AOT_ProofData.get ctxt) of SOME (Const (\<^const_name>‹w⇩0›, _)) => y |
437 _ => Const (\<^syntax_const>‹_AOT_theorem›, dummyT) $ y end
438 | [Const ("_var", _) $ _, y] => let
439 val y = (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ y)
440 in Const (\<^syntax_const>‹_AOT_nec_theorem›, dummyT) $ y end
441 ),
442 (\<^const_syntax>‹AOT_model_axiom›, fn ctxt => fn [trm] =>
443 Const (\<^syntax_const>‹_AOT_axiom›, dummyT) $
444 (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ trm)),
445 (\<^const_syntax>‹AOT_model_act_axiom›, fn ctxt => fn [trm] =>
446 Const (\<^syntax_const>‹_AOT_axiom›, dummyT) $
447 (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ trm)),
448(\<^syntax_const>‹_AOT_process_frees›, fn _ => fn [t] => let
449 fun mapAppls (x as Const ("_free", _) $
450 Free (_, Type ("_ignore_type", [Type ("fun", _)])))
451 = (Const ("_AOT_raw_appl", dummyT) $ x)
452 | mapAppls (x as Const ("_free", _) $ Free (_, Type ("fun", _)))
453 = (Const ("_AOT_raw_appl", dummyT) $ x)
454 | mapAppls (x as Const ("_var", _) $
455 Var (_, Type ("_ignore_type", [Type ("fun", _)])))
456 = (Const ("_AOT_raw_appl", dummyT) $ x)
457 | mapAppls (x as Const ("_var", _) $ Var (_, Type ("fun", _)))
458 = (Const ("_AOT_raw_appl", dummyT) $ x)
459 | mapAppls (x $ y) = mapAppls x $ mapAppls y
460 | mapAppls (Abs (x,y,z)) = Abs (x,y, mapAppls z)
461 | mapAppls x = x
462 in mapAppls t end
463)
464]
465›
466
467print_ast_translation‹AOT_syntax_print_ast_translations
468let
469fun handleTermOfVar x kind name = (
470let
471val _ = case kind of "_free" => () | "_var" => () | "_bound" => () | _ => raise Match
472in
473 case printVarKind name
474 of (SingleVariable name) => Ast.Appl [Ast.Constant kind, Ast.Variable name]
475 | (Ellipses (s, e)) => Ast.Appl [Ast.Constant "_AOT_free_var_ellipse",
476 Ast.Appl [Ast.Constant kind, Ast.Variable s],
477 Ast.Appl [Ast.Constant kind, Ast.Variable e]
478 ]
479 | Verbatim name => Ast.mk_appl (Ast.Constant "_AOT_quoted")
480 [Ast.mk_appl (Ast.Constant "_AOT_term_of_var") [x]]
481end
482)
483fun termOfVar ctxt (Ast.Appl [Ast.Constant "_constrain",
484 x as Ast.Appl [Ast.Constant kind, Ast.Variable name], _]) = termOfVar ctxt x
485 | termOfVar ctxt (x as Ast.Appl [Ast.Constant kind, Ast.Variable name])
486 = handleTermOfVar x kind name
487 | termOfVar ctxt (x as Ast.Appl [Ast.Constant rep, y]) = (
488let
489val (restr,_) = Local_Theory.raw_theory_result (fn thy => (
490let
491val restrs = Symtab.dest (AOT_Restriction.get thy)
492val restr = List.find (fn (n,(_,Const (c,t))) => (
493 c = rep orelse c = Lexicon.unmark_const rep) | _ => false) restrs
494in
495(restr,thy)
496end
497)) ctxt
498in
499 case restr of SOME r => Ast.Appl [Ast.Constant (\<^const_syntax>‹AOT_term_of_var›), y]
500 | _ => raise Match
501end)
502
503in
504[(\<^const_syntax>‹AOT_term_of_var›, fn ctxt => fn [x] => termOfVar ctxt x),
505("_AOT_raw_appl", fn ctxt => fn t::a::args => let
506fun applyTermOfVar (t as Ast.Appl (Ast.Constant \<^const_syntax>‹AOT_term_of_var›::[x]))
507 = (case try (termOfVar ctxt) x of SOME y => y | _ => t)
508 | applyTermOfVar y = (case try (termOfVar ctxt) y of SOME x => x | _ => y)
509val ts = fold (fn a => fn b => Ast.mk_appl (Ast.Constant \<^syntax_const>‹_AOT_args›)
510 [b,applyTermOfVar a]) args (applyTermOfVar a)
511in Ast.mk_appl (Ast.Constant \<^syntax_const>‹_AOT_appl›) [t,ts] end)]
512end
513›
514
515context AOT_meta_syntax
516begin
517notation AOT_denotes ("_❙↓")
518notation AOT_imp (infixl "❙→" 25)
519notation AOT_not ("❙¬_" [50] 50)
520notation AOT_box ("❙□_" [49] 54)
521notation AOT_act ("❙𝒜_" [49] 54)
522notation AOT_forall (binder "❙∀" 8)
523notation AOT_eq (infixl "❙=" 50)
524notation AOT_desc (binder "❙ι" 100)
525notation AOT_lambda (binder "❙λ" 100)
526notation AOT_lambda0 ("❙[❙λ _❙]")
527notation AOT_exe ("❙⦇_,_❙⦈")
528notation AOT_model_equiv_def (infixl "❙≡⇩d⇩f" 10)
529notation AOT_model_id_def (infixl "❙=⇩d⇩f" 10)
530notation AOT_term_of_var ("❙⟨_❙⟩")
531notation AOT_concrete ("❙E❙!")
532end
533context AOT_no_meta_syntax
534begin
535no_notation AOT_denotes ("_❙↓")
536no_notation AOT_imp (infixl "❙→" 25)
537no_notation AOT_not ("❙¬_" [50] 50)
538no_notation AOT_box ("❙□_" [49] 54)
539no_notation AOT_act ("❙𝒜_" [49] 54)
540no_notation AOT_forall (binder "❙∀" 8)
541no_notation AOT_eq (infixl "❙=" 50)
542no_notation AOT_desc (binder "❙ι" 100)
543no_notation AOT_lambda (binder "❙λ" 100)
544no_notation AOT_lambda0 ("❙[❙λ _❙]")
545no_notation AOT_exe ("❙⦇_,_❙⦈")
546no_notation AOT_model_equiv_def (infixl "❙≡⇩d⇩f" 10)
547no_notation AOT_model_id_def (infixl "❙=⇩d⇩f" 10)
548no_notation AOT_term_of_var ("❙⟨_❙⟩")
549no_notation AOT_concrete ("❙E❙!")
550end
551
552bundle AOT_syntax
553begin
554declare[[show_AOT_syntax=true, show_question_marks=false, eta_contract=false]]
555end
556
557bundle AOT_no_syntax
558begin
559declare[[show_AOT_syntax=false, show_question_marks=true]]
560end
561
562parse_translation‹
563[("_AOT_restriction", fn ctxt => fn [Const (name,_)] =>
564let
565val (restr, ctxt) = ctxt |> Local_Theory.raw_theory_result
566 (fn thy => (Option.map fst (Symtab.lookup (AOT_Restriction.get thy) name), thy))
567val restr = case restr of SOME x => x
568 | _ => raise Fail ("Unknown restricted type: " ^ name)
569in restr end
570)]
571›
572
573print_translation‹
574AOT_syntax_print_translations
575[
576 (\<^const_syntax>‹AOT_model_equiv_def›, fn ctxt => fn [x,y] =>
577 Const (\<^syntax_const>‹_AOT_equiv_def›, dummyT) $
578 (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ x) $
579 (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ y))
580]
581›
582
583print_translation‹
584AOT_syntax_print_translations [
585(\<^const_syntax>‹AOT_model_id_def›, fn ctxt =>
586 fn [lhs as Abs (lhsName, lhsTy, lhsTrm), rhs as Abs (rhsName, rhsTy, rhsTrm)] =>
587 let
588 val (name,_) = Name.variant lhsName
589 (Term.declare_term_names rhsTrm (Term.declare_term_names lhsTrm Name.context));
590 val lhs = Term.betapply (lhs, Const ("_bound", dummyT) $ Free (name, lhsTy))
591 val rhs = Term.betapply (rhs, Const ("_bound", dummyT) $ Free (name, rhsTy))
592 in
593 Const (\<^const_syntax>‹AOT_model_id_def›, dummyT) $ lhs $ rhs
594 end
595 | [Const (\<^const_syntax>‹case_prod›, _) $ lhs,
596 Const (\<^const_syntax>‹case_prod›, _) $ rhs] =>
597 Const (\<^const_syntax>‹AOT_model_id_def›, dummyT) $ lhs $ rhs
598 | [Const (\<^const_syntax>‹case_unit›, _) $ lhs,
599 Const (\<^const_syntax>‹case_unit›, _) $ rhs] =>
600 Const (\<^const_syntax>‹AOT_model_id_def›, dummyT) $ lhs $ rhs
601 | [x, y] =>
602 Const (\<^syntax_const>‹_AOT_id_def›, dummyT) $
603 (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ x) $
604 (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ y)
605)]›
606
607text‹Special marker for printing propositions as theorems
608 and for pretty-printing AOT terms.›
609definition print_as_theorem :: ‹𝗈 ⇒ bool› where
610 ‹print_as_theorem ≡ λ φ . ∀v . [v ⊨ φ]›
611lemma print_as_theoremI:
612 assumes ‹⋀ v . [v ⊨ φ]›
613 shows ‹print_as_theorem φ›
614 using assms by (simp add: print_as_theorem_def)
615attribute_setup print_as_theorem =
616 ‹Scan.succeed (Thm.rule_attribute []
617 (K (fn thm => thm RS @{thm print_as_theoremI})))›
618 "Print as theorem."
619print_translation‹AOT_syntax_print_translations [
620 (\<^const_syntax>‹print_as_theorem›, fn ctxt => fn [x] =>
621 (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ x))
622]›
623
624definition print_term :: ‹'a ⇒ 'a› where ‹print_term ≡ λ x . x›
625syntax "_AOT_print_term" :: ‹τ ⇒ 'a› (‹AOT'_TERM[_]›)
626translations
627 "_AOT_print_term φ" => "CONST print_term (_AOT_process_frees φ)"
628print_translation‹AOT_syntax_print_translations [
629 (\<^const_syntax>‹print_term›, fn ctxt => fn [x] =>
630 (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ x))
631]›
632
633
634
635
636
637interpretation AOT_no_meta_syntax.
638
639
641unbundle AOT_syntax
642
644
645
646
647end
648
649