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" = "df"
21         and "df" = "df"
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 df 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 =df 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_translation213[
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    constAOT_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_nameSet.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_namePure.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 w0} $ 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_namePure.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_namePure.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_namePure.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_translation272[
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_nameAOT_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_translationAOT_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) φ & ψ df ¬(φ  ¬ψ)
307declare "AOT_conj"[AOT del, AOT_defs del]
308AOT_define AOT_disj :: [φ, φ]  φ (infixl  35) φ  ψ df ¬φ  ψ
309declare "AOT_disj"[AOT del, AOT_defs del]
310AOT_define AOT_equiv :: [φ, φ]  φ (infix  20) φ  ψ df (φ  ψ) & (ψ  φ)
311declare "AOT_equiv"[AOT del, AOT_defs del]
312AOT_define AOT_dia :: φ  φ (_› [49] 54) φ df ¬¬φ
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_syntaxAOT_forall
336    syntax_const‹_AOT_all›
337    (syntax_const‹_AOT_all_ellipse›, true)
338    const_nameAOT_imp,
339  AOT_binder_trans @{theory} @{binding "AOT_forall_binder"} syntax_const‹_AOT_all›,
340  Syntax_Trans.preserve_binder_abs_tr'
341    const_syntaxAOT_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_syntaxAOT_lambda
346    syntax_const‹_AOT_lambda›
347    (syntax_const‹_AOT_lambda_arg_ellipse›, false)
348    const_nameundefined,
349  AOT_binder_trans
350    @{theory}
351    @{binding "AOT_lambda_binder"}
352    syntax_const‹_AOT_lambda›
353 ]
354
355
356parse_translation357[(syntax_const‹_AOT_id_def›, parseIdDef)]
358
359
360parse_ast_translation[
361 (syntax_const‹_AOT_all›,
362  AOT_restricted_binder const_nameAOT_forall const_nameAOT_imp),
363 (syntax_const‹_AOT_desc›,
364  AOT_restricted_binder const_nameAOT_desc const_nameAOT_conj)
365]
366
367AOT_define AOT_exists :: α  φ  φ «AOT_exists φ» df ¬α ¬φ{α}
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_translation376[(syntax_const‹_AOT_exists›,
377  AOT_restricted_binder const_nameAOT_exists const_nameAOT_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_translationAOT_syntax_print_translations [
398  AOT_preserve_binder_abs_tr'
399    const_syntaxAOT_exists
400    syntax_const‹_AOT_exists›
401    (syntax_const‹_AOT_exists_ellipse›,true) const_nameAOT_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_translationAOT_syntax_print_translations
415[(const_syntaxPure.all, fn ctxt => fn [Abs (_, _,
416  Const (const_syntaxHOL.Trueprop, _) $
417  (Const (const_syntaxAOT_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_syntaxHOL.Trueprop, _) $
422  (Const (const_syntaxAOT_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_syntaxAOT_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_syntaxw0, _), y] => let
435    val y = (Const (syntax_const‹_AOT_process_frees›, dummyT) $ y)
436    in case (AOT_ProofData.get ctxt) of SOME (Const (const_namew0, _)) => 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_syntaxAOT_model_axiom, fn ctxt => fn [trm] =>
443    Const (syntax_const‹_AOT_axiom›, dummyT) $
444    (Const (syntax_const‹_AOT_process_frees›, dummyT) $ trm)),
445 (const_syntaxAOT_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_translationAOT_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_syntaxAOT_term_of_var), y]
500  | _ => raise Match
501end)
502
503in
504[(const_syntaxAOT_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_syntaxAOT_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 "df" 10)
529notation AOT_model_id_def (infixl "=df" 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 "df" 10)
547no_notation AOT_model_id_def (infixl "=df" 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_translation563[("_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_translation574AOT_syntax_print_translations
575[
576  (const_syntaxAOT_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_translation584AOT_syntax_print_translations [
585(const_syntaxAOT_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_syntaxAOT_model_id_def, dummyT) $ lhs $ rhs
594    end
595  | [Const (const_syntaxcase_prod, _) $ lhs,
596     Const (const_syntaxcase_prod, _) $ rhs] =>
597    Const (const_syntaxAOT_model_id_def, dummyT) $ lhs $ rhs
598  | [Const (const_syntaxcase_unit, _) $ lhs,
599      Const (const_syntaxcase_unit, _) $ rhs] =>
600    Const (const_syntaxAOT_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_translationAOT_syntax_print_translations [
620  (const_syntaxprint_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_translationAOT_syntax_print_translations [
629  (const_syntaxprint_term, fn ctxt => fn [x] => 
630    (Const (syntax_const‹_AOT_process_frees›, dummyT) $ x))
631]
632
633
634(* To enable meta syntax: *)
635(* interpretation AOT_meta_syntax. *)
636(* To disable meta syntax: *)
637interpretation AOT_no_meta_syntax.
638
639(* To enable AOT syntax (takes precedence over meta syntax;
640                         can be done locally using "including" or "include"): *)
641unbundle AOT_syntax
642(* To disable AOT syntax (restoring meta syntax or no syntax;
643                          can be done locally using "including" or "include"): *)
644(* unbundle AOT_no_syntax *)
645
646(*<*)
647end
648(*>*)
649