Theory AOT_syntax

(*<*)
theory AOT_syntax
  imports AOT_commands
  keywords "AOT_register_variable_names" :: thy_decl
       and "AOT_register_metavariable_names" :: thy_decl
       and "AOT_register_premise_set_names" :: thy_decl
       and "AOT_register_type_constraints" :: thy_decl
     abbrevs "actually" = "❙𝒜"
         and "neccessarily" = "□"
         and "possibly" = "◇"
         and "the" = "❙ι"
         and "lambda" = "[λ]"
         and "being such that" = "[λ ]"
         and "forall" = "∀"
         and "exists" = "∃"
         and "equivalent" = "≡"
         and "not" = "¬"
         and "implies" = "→"
         and "equal" = "="
         and "by definition" = "⇩d⇩f"
         and "df" = "⇩d⇩f"
         and "denotes" = "↓"
begin
(*>*)

section‹Approximation of the Syntax of PLM›

locale AOT_meta_syntax
begin
notation AOT_model_valid_in (‹❙[_ ❙⊨ _❙]›)
notation AOT_model_axiom (‹❙□❙[_❙]›)
notation AOT_model_act_axiom (‹❙𝒜❙[_❙]›)
end
locale AOT_no_meta_syntax
begin
no_notation AOT_model_valid_in (‹❙[_ ❙⊨ _❙]›)
no_notation AOT_model_axiom (‹❙□❙[_❙]›)
no_notation AOT_model_act_axiom (‹❙𝒜❙[_❙]›)
end

consts AOT_denotes :: ‹'a::AOT_Term ⇒ 𝗈›
       AOT_imp :: ‹[𝗈, 𝗈] ⇒ 𝗈›
       AOT_not :: ‹𝗈 ⇒ 𝗈›
       AOT_box :: ‹𝗈 ⇒ 𝗈›
       AOT_act :: ‹𝗈 ⇒ 𝗈›
       AOT_forall :: ‹('a::AOT_Term ⇒ 𝗈) ⇒ 𝗈›
       AOT_eq :: ‹'a::AOT_Term ⇒ 'a::AOT_Term ⇒ 𝗈›
       AOT_desc :: ‹('a::AOT_UnaryIndividualTerm ⇒ 𝗈) ⇒ 'a›
       AOT_exe :: ‹<'a::AOT_IndividualTerm> ⇒ 'a ⇒ 𝗈›
       AOT_lambda :: ‹('a::AOT_IndividualTerm ⇒ 𝗈) ⇒ <'a>›
       AOT_lambda0 :: ‹𝗈 ⇒ 𝗈›
       AOT_concrete :: ‹<'a::AOT_UnaryIndividualTerm> AOT_var›

nonterminal κ⇩s and Π and Π0 and α and exe_arg and exe_args
        and lambda_args and desc and free_var and free_vars
        and AOT_props and AOT_premises and AOT_world_relative_prop

syntax "_AOT_process_frees" :: ‹φ ⇒ φ'› (‹_›)
       "_AOT_verbatim" :: ‹any ⇒ φ› (‹«_»›)
       "_AOT_verbatim" :: ‹any ⇒ τ› (‹«_»›)
       "_AOT_quoted" :: ‹φ' ⇒ any› (‹«_»›)
       "_AOT_quoted" :: ‹τ' ⇒ any› (‹«_»›)
       "" :: ‹φ ⇒ φ› (‹'(_')›)
       "_AOT_process_frees" :: ‹τ ⇒ τ'› (‹_›)
       "" :: ‹κ⇩s ⇒ τ› (‹_›)
       "" :: ‹Π ⇒ τ› (‹_›)
       "" :: ‹φ ⇒ τ› (‹'(_')›)
       "_AOT_term_var" :: ‹id_position ⇒ τ› (‹_›)
       "_AOT_term_var" :: ‹id_position ⇒ φ› (‹_›)
       "_AOT_exe_vars" :: ‹id_position ⇒ exe_arg› (‹_›)
       "_AOT_lambda_vars" :: ‹id_position ⇒ lambda_args› (‹_›)
       "_AOT_var" :: ‹id_position ⇒ α› (‹_›)
       "_AOT_vars" :: ‹id_position ⇒ any›
       "_AOT_verbatim" :: ‹any ⇒ α› (‹«_»›)
       "_AOT_valid" :: ‹w ⇒ φ' ⇒ bool› (‹[_ ⊨ _]›)
       "_AOT_denotes" :: ‹τ ⇒ φ› (‹_↓›)
       "_AOT_imp" :: ‹[φ, φ] ⇒ φ› (infixl ‹→› 25)
       "_AOT_not" :: ‹φ ⇒ φ› (‹~_› [50] 50)
       "_AOT_not" :: ‹φ ⇒ φ› (‹¬_› [50] 50)
       "_AOT_box" :: ‹φ ⇒ φ› (‹□_› [49] 54)
       "_AOT_act" :: ‹φ ⇒ φ› (‹❙𝒜_› [49] 54)
       "_AOT_all" :: ‹α ⇒ φ ⇒ φ› (‹∀_ _› [1,40])
syntax (input)
       "_AOT_all_ellipse"
            :: ‹id_position ⇒ id_position ⇒ φ ⇒ φ› (‹∀_...∀_ _› [1,40])
syntax (output)
       "_AOT_all_ellipse"
            :: ‹id_position ⇒ id_position ⇒ φ ⇒ φ› (‹∀_...∀_'(_')› [1,40])
syntax
       "_AOT_eq" :: ‹[τ, τ] ⇒ φ› (infixl ‹=› 50)
       "_AOT_desc" :: ‹α ⇒ φ ⇒ desc› (‹❙ι__› [1,1000])
       "" :: ‹desc ⇒ κ⇩s› (‹_›)
       "_AOT_lambda" :: ‹lambda_args ⇒ φ ⇒ Π› (‹[λ_ _]›)
       "_explicitRelation" :: ‹τ ⇒ Π› (‹[_]›)
       "" :: ‹κ⇩s ⇒ exe_arg› (‹_›)
       "" :: ‹exe_arg ⇒ exe_args› (‹_›)
       "_AOT_exe_args" :: ‹exe_arg ⇒ exe_args ⇒ exe_args› (‹__›)
       "_AOT_exe_arg_ellipse" :: ‹id_position ⇒ id_position ⇒ exe_arg› (‹_..._›)
       "_AOT_lambda_arg_ellipse"
            :: ‹id_position ⇒ id_position ⇒ lambda_args› (‹_..._›)
       "_AOT_term_ellipse" :: ‹id_position ⇒ id_position ⇒ τ› (‹_..._›)
       "_AOT_exe" :: ‹Π ⇒ exe_args ⇒ φ› (‹__›)
       "_AOT_enc" :: ‹exe_args ⇒ Π ⇒ φ› (‹__›)
       "_AOT_lambda0" :: ‹φ ⇒ Π0› (‹[λ _]›)
       "" :: ‹Π0 ⇒ φ› (‹_›)
       "" :: ‹Π0 ⇒ τ› (‹_›)
       "_AOT_concrete" :: ‹Π› (‹E!›)
       "" :: ‹any ⇒ exe_arg› (‹«_»›)
       "" :: ‹desc ⇒ free_var› (‹_›)
       "" :: ‹Π ⇒ free_var› (‹_›)
       "_AOT_appl" :: ‹id_position ⇒ free_vars ⇒ φ› (‹_'{_'}›)
       "_AOT_appl" :: ‹id_position ⇒ free_vars ⇒ τ› (‹_'{_'}›)
       "_AOT_appl" :: ‹id_position ⇒ free_vars ⇒ free_vars› (‹_'{_'}›)
       "_AOT_appl" :: ‹id_position ⇒ free_vars ⇒ free_vars› (‹_'{_'}›)
       "_AOT_term_var" :: ‹id_position ⇒ free_var› (‹_›)
       "" :: ‹any ⇒ free_var› (‹«_»›)
       "" :: ‹free_var ⇒ free_vars› (‹_›)
       "_AOT_args" :: ‹free_var ⇒ free_vars ⇒ free_vars› (‹_,_›)
       "_AOT_free_var_ellipse" :: ‹id_position ⇒ id_position ⇒ free_var› (‹_..._›)
syntax "_AOT_premises"
            :: ‹AOT_world_relative_prop ⇒ AOT_premises ⇒ AOT_premises› (infixr ‹,› 3)
       "_AOT_world_relative_prop" :: "φ ⇒ AOT_world_relative_prop" (‹_›)
       "" :: "AOT_world_relative_prop ⇒ AOT_premises" (‹_›)
       "_AOT_prop" :: ‹AOT_world_relative_prop ⇒ AOT_prop› (‹_›)
       "" :: ‹AOT_prop ⇒ AOT_props› (‹_›)
       "_AOT_derivable" :: "AOT_premises ⇒ φ' ⇒ AOT_prop" (infixl ‹❙⊢› 2)
       "_AOT_nec_derivable" :: "AOT_premises ⇒ φ' ⇒ AOT_prop" (infixl ‹❙⊢⇩□› 2)
       "_AOT_theorem" :: "φ' ⇒ AOT_prop" (‹❙⊢ _›)
       "_AOT_nec_theorem" :: "φ' ⇒ AOT_prop" (‹❙⊢⇩□ _›)
       "_AOT_equiv_def" :: ‹φ ⇒ φ ⇒ AOT_prop› (infixl ‹≡⇩d⇩f› 3)
       "_AOT_axiom" :: "φ' ⇒ AOT_axiom" (‹_›)
       "_AOT_act_axiom" :: "φ' ⇒ AOT_act_axiom" (‹_›)
       "_AOT_axiom" :: "φ' ⇒ AOT_prop" (‹_ ∈ Λ⇩□›)
       "_AOT_act_axiom" :: "φ' ⇒ AOT_prop" (‹_ ∈ Λ›)
       "_AOT_id_def" :: ‹τ ⇒ τ ⇒ AOT_prop› (infixl ‹=⇩d⇩f› 3)
       "_AOT_for_arbitrary"
            :: ‹id_position ⇒ AOT_prop ⇒ AOT_prop› (‹for arbitrary _: _› [1000,1] 1)
syntax (output) "_lambda_args" :: ‹any ⇒ patterns ⇒ patterns› (‹__›)

translations
  "[w ⊨ φ]" => "CONST AOT_model_valid_in w φ"

AOT_syntax_print_translations
  "[w ⊨ φ]" <= "CONST AOT_model_valid_in w φ"

ML_file AOT_syntax.ML

AOT_register_type_constraints
  Individual: ‹_::AOT_UnaryIndividualTerm› ‹_::AOT_IndividualTerm› and
  Proposition: 𝗈 and
  Relation: ‹<_::AOT_IndividualTerm>› and
  Term: ‹_::AOT_Term›

AOT_register_variable_names
  Individual: x y z ν μ a b c d and
  Proposition: p q r s and
  Relation: F G H P Q R S and
  Term: α β γ δ

AOT_register_metavariable_names
  Individual: κ and
  Proposition: φ ψ χ θ ζ ξ Θ and
  Relation: Π and
  Term: τ σ

AOT_register_premise_set_names Γ Δ Λ

parse_ast_translation‹[
  (\<^syntax_const>‹_AOT_var›, K AOT_check_var),
  (\<^syntax_const>‹_AOT_exe_vars›, K AOT_split_exe_vars),
  (\<^syntax_const>‹_AOT_lambda_vars›, K AOT_split_lambda_args)
]›

translations
  "_AOT_denotes τ" => "CONST AOT_denotes τ"
  "_AOT_imp φ ψ" => "CONST AOT_imp φ ψ"
  "_AOT_not φ" => "CONST AOT_not φ"
  "_AOT_box φ" => "CONST AOT_box φ"
  "_AOT_act φ" => "CONST AOT_act φ"
  "_AOT_eq τ τ'" => "CONST AOT_eq τ τ'"
  "_AOT_lambda0 φ" => "CONST AOT_lambda0 φ"
  "_AOT_concrete" => "CONST AOT_term_of_var (CONST AOT_concrete)"
  "_AOT_lambda α φ" => "CONST AOT_lambda (_abs α φ)"
  "_explicitRelation Π" => "Π"

AOT_syntax_print_translations
  "_AOT_lambda (_lambda_args x y) φ" <= "CONST AOT_lambda (_abs (_pattern x y) φ)"
  "_AOT_lambda (_lambda_args x y) φ" <= "CONST AOT_lambda (_abs (_patterns x y) φ)"
  "_AOT_lambda x φ" <= "CONST AOT_lambda (_abs x φ)"
  "_lambda_args x (_lambda_args y z)" <= "_lambda_args x (_patterns y z)"
  "_lambda_args (x y z)" <= "_lambda_args (_tuple x (_tuple_arg (_tuple y z)))"


AOT_syntax_print_translations
  "_AOT_imp φ ψ" <= "CONST AOT_imp φ ψ"
  "_AOT_not φ" <= "CONST AOT_not φ"
  "_AOT_box φ" <= "CONST AOT_box φ"
  "_AOT_act φ" <= "CONST AOT_act φ"
  "_AOT_all α φ" <= "CONST AOT_forall (_abs α φ)"
  "_AOT_all α φ" <= "CONST AOT_forall (λα. φ)"
  "_AOT_eq τ τ'" <= "CONST AOT_eq τ τ'"
  "_AOT_desc x φ" <= "CONST AOT_desc (_abs x φ)"
  "_AOT_desc x φ" <= "CONST AOT_desc (λx. φ)"
  "_AOT_lambda0 φ" <= "CONST AOT_lambda0 φ"
  "_AOT_concrete" <= "CONST AOT_term_of_var (CONST AOT_concrete)"

translations
  "_AOT_appl φ (_AOT_args a b)" => "_AOT_appl (φ a) b"
  "_AOT_appl φ a" => "φ a"


parse_translation‹
[
  (\<^syntax_const>‹_AOT_var›, parseVar true),
  (\<^syntax_const>‹_AOT_vars›, parseVar false),
  (\<^syntax_const>‹_AOT_valid›, fn ctxt => fn [w,x] =>
    \<^const>‹AOT_model_valid_in› $ w $ x),
  (\<^syntax_const>‹_AOT_quoted›, fn ctxt => fn [x] => x),
  (\<^syntax_const>‹_AOT_process_frees›, fn ctxt => fn [x] => processFrees ctxt x),
  (\<^syntax_const>‹_AOT_world_relative_prop›, fn ctxt => fn [x] => let
    val (x, premises) = processFreesAndPremises ctxt x
    val (world::formulas) = Variable.variant_names (Variable.declare_names x ctxt)
        (("v", dummyT)::(map (fn _ => ("φ", dummyT)) premises))
    val term = HOLogic.mk_Trueprop
        (@{const AOT_model_valid_in} $ Free world $ processFrees ctxt x)
    val term = fold (fn (premise,form) => fn trm =>
         @{const "Pure.imp"} $
        HOLogic.mk_Trueprop
          (Const (\<^const_name>‹Set.member›, dummyT) $ Free form $ premise) $
          (Term.absfree (Term.dest_Free (dropConstraints premise)) trm $ Free form)
    ) (ListPair.zipEq (premises,formulas)) term
    val term = fold (fn (form) => fn trm =>
         Const (\<^const_name>‹Pure.all›, dummyT) $
        (Term.absfree form trm)
    ) formulas term
    val term = Term.absfree world term
    in term end),
  (\<^syntax_const>‹_AOT_prop›, fn ctxt => fn [x] => let
    val world = case (AOT_ProofData.get ctxt) of SOME w => w
        | _ => raise Fail "Expected world to be stored in the proof state."
    in x $ world end),
  (\<^syntax_const>‹_AOT_theorem›, fn ctxt => fn [x] =>
      HOLogic.mk_Trueprop (@{const AOT_model_valid_in} $ @{const w⇩0} $ x)),
  (\<^syntax_const>‹_AOT_axiom›, fn ctxt => fn [x] =>
      HOLogic.mk_Trueprop (@{const AOT_model_axiom} $ x)),
  (\<^syntax_const>‹_AOT_act_axiom›, fn ctxt => fn [x] =>
      HOLogic.mk_Trueprop (@{const AOT_model_act_axiom} $ x)),
  (\<^syntax_const>‹_AOT_nec_theorem›, fn ctxt => fn [trm] => let
    val world = singleton (Variable.variant_names (Variable.declare_names trm ctxt)) ("v", @{typ w})
    val trm = HOLogic.mk_Trueprop (@{const AOT_model_valid_in} $ Free world $ trm)
    val trm = Term.absfree world trm
    val trm = Const (\<^const_name>‹Pure.all›, dummyT) $ trm
    in trm end),
  (\<^syntax_const>‹_AOT_derivable›, fn ctxt => fn [x,y] => let
    val world = case (AOT_ProofData.get ctxt) of SOME w => w
      | _ => raise Fail "Expected world to be stored in the proof state."
    in foldPremises world x y end),
  (\<^syntax_const>‹_AOT_nec_derivable›, fn ctxt => fn [x,y] => let
    in Const (\<^const_name>‹Pure.all›, dummyT) $
       Abs ("v", dummyT, foldPremises (Bound 0) x y) end),
  (\<^syntax_const>‹_AOT_for_arbitrary›, fn ctxt => fn [_ $ var $ pos,trm] => let
    val trm = Const (\<^const_name>‹Pure.all›, dummyT) $
        (Const ("_constrainAbs", dummyT) $ Term.absfree (Term.dest_Free var) trm $ pos)
    in trm end),
  (\<^syntax_const>‹_AOT_equiv_def›, parseEquivDef),
  (\<^syntax_const>‹_AOT_exe›, parseExe),
  (\<^syntax_const>‹_AOT_enc›, parseEnc)
]
›

parse_ast_translation‹
[
  (\<^syntax_const>‹_AOT_exe_arg_ellipse›, parseEllipseList "_AOT_term_vars"),
  (\<^syntax_const>‹_AOT_lambda_arg_ellipse›, parseEllipseList "_AOT_vars"),
  (\<^syntax_const>‹_AOT_free_var_ellipse›, parseEllipseList "_AOT_term_vars"),
  (\<^syntax_const>‹_AOT_term_ellipse›, parseEllipseList "_AOT_term_vars"),
  (\<^syntax_const>‹_AOT_all_ellipse›, fn ctx => fn [a,b,c] =>
      Ast.mk_appl (Ast.Constant \<^const_name>‹AOT_forall›) [
        Ast.mk_appl (Ast.Constant "_abs") [parseEllipseList "_AOT_vars" ctx [a,b],c]
      ])
]
›

syntax (output)
  "_AOT_individual_term" :: ‹'a ⇒ tuple_args› (‹_›)
  "_AOT_individual_terms" :: ‹tuple_args ⇒ tuple_args ⇒ tuple_args› (‹__›)
  "_AOT_relation_term" :: ‹'a ⇒ Π›
  "_AOT_any_term" :: ‹'a ⇒ τ›


print_ast_translation‹AOT_syntax_print_ast_translations[
 (\<^syntax_const>‹_AOT_individual_term›, AOT_print_individual_term),
 (\<^syntax_const>‹_AOT_relation_term›, AOT_print_relation_term),
 (\<^syntax_const>‹_AOT_any_term›, AOT_print_generic_term)
]›

AOT_syntax_print_translations
  "_AOT_individual_terms (_AOT_individual_term x) (_AOT_individual_terms (_tuple y z))"
  <= "_AOT_individual_terms (_tuple x (_tuple_args y z))"
  "_AOT_individual_terms (_AOT_individual_term x) (_AOT_individual_term y)"
  <= "_AOT_individual_terms (_tuple x (_tuple_arg y))"
  "_AOT_individual_terms (_tuple x y)" <= "_AOT_individual_term (_tuple x y)"
  "_AOT_exe (_AOT_relation_term Π) (_AOT_individual_term κ)" <= "CONST AOT_exe Π κ"
  "_AOT_denotes (_AOT_any_term κ)" <= "CONST AOT_denotes κ"

AOT_define AOT_conj :: ‹[φ, φ] ⇒ φ› (infixl ‹&› 35) ‹φ & ψ ≡⇩d⇩f ¬(φ → ¬ψ)›
declare "AOT_conj"[AOT del, AOT_defs del]
AOT_define AOT_disj :: ‹[φ, φ] ⇒ φ› (infixl ‹∨› 35) ‹φ ∨ ψ ≡⇩d⇩f ¬φ → ψ›
declare "AOT_disj"[AOT del, AOT_defs del]
AOT_define AOT_equiv :: ‹[φ, φ] ⇒ φ› (infix ‹≡› 20) ‹φ ≡ ψ ≡⇩d⇩f (φ → ψ) & (ψ → φ)›
declare "AOT_equiv"[AOT del, AOT_defs del]
AOT_define AOT_dia :: ‹φ ⇒ φ› (‹◇_› [49] 54) ‹◇φ ≡⇩d⇩f ¬□¬φ›
declare "AOT_dia"[AOT del, AOT_defs del]

context AOT_meta_syntax
begin
notation AOT_dia (‹❙◇_› [49] 54)
notation AOT_conj (infixl ‹❙&› 35)
notation AOT_disj (infixl ‹❙∨› 35)
notation AOT_equiv (infixl ‹❙≡› 20)
end
context AOT_no_meta_syntax
begin
no_notation AOT_dia (‹❙◇_› [49] 54)
no_notation AOT_conj (infixl ‹❙&› 35)
no_notation AOT_disj (infixl ‹❙∨› 35)
no_notation AOT_equiv (infixl ‹❙≡› 20)
end


print_translation ‹
AOT_syntax_print_translations
 [
  AOT_preserve_binder_abs_tr'
    \<^const_syntax>‹AOT_forall›
    \<^syntax_const>‹_AOT_all›
    (\<^syntax_const>‹_AOT_all_ellipse›, true)
    \<^const_name>‹AOT_imp›,
  AOT_binder_trans @{theory} @{binding "AOT_forall_binder"} \<^syntax_const>‹_AOT_all›,
  (\<^const_syntax>‹AOT_desc›, K (Syntax_Trans.preserve_binder_abs_tr' \<^syntax_const>‹_AOT_desc› dummyT)),
  AOT_binder_trans @{theory} @{binding "AOT_desc_binder"} \<^syntax_const>‹_AOT_desc›,
  AOT_preserve_binder_abs_tr'
    \<^const_syntax>‹AOT_lambda›
    \<^syntax_const>‹_AOT_lambda›
    (\<^syntax_const>‹_AOT_lambda_arg_ellipse›, false)
    \<^const_name>‹undefined›,
  AOT_binder_trans
    @{theory}
    @{binding "AOT_lambda_binder"}
    \<^syntax_const>‹_AOT_lambda›
 ]
›

parse_translation‹
[(\<^syntax_const>‹_AOT_id_def›, parseIdDef)]
›

parse_ast_translation‹[
 (\<^syntax_const>‹_AOT_all›,
  AOT_restricted_binder \<^const_name>‹AOT_forall› \<^const_name>‹AOT_imp›),
 (\<^syntax_const>‹_AOT_desc›,
  AOT_restricted_binder \<^const_name>‹AOT_desc› \<^const_name>‹AOT_conj›)
]›

AOT_define AOT_exists :: ‹α ⇒ φ ⇒ φ› ‹«AOT_exists φ» ≡⇩d⇩f ¬∀α ¬φ{α}›
declare AOT_exists[AOT del, AOT_defs del]
syntax "_AOT_exists" :: ‹α ⇒ φ ⇒ φ› (‹∃_ _› [1,40])

AOT_syntax_print_translations
  "_AOT_exists α φ" <= "CONST AOT_exists (_abs α φ)"
  "_AOT_exists α φ" <= "CONST AOT_exists (λα. φ)"

parse_ast_translation‹                              
[(\<^syntax_const>‹_AOT_exists›,
  AOT_restricted_binder \<^const_name>‹AOT_exists› \<^const_name>‹AOT_conj›)]
›

context AOT_meta_syntax
begin
notation AOT_exists (binder ‹❙∃› 8)
end
context AOT_no_meta_syntax
begin
no_notation AOT_exists (binder ‹❙∃› 8)
end


syntax (input)
   "_AOT_exists_ellipse" :: ‹id_position ⇒ id_position ⇒ φ ⇒ φ› (‹∃_...∃_ _› [1,40])
syntax (output)
   "_AOT_exists_ellipse" :: ‹id_position ⇒ id_position ⇒ φ ⇒ φ› (‹∃_...∃_ '(_')› [1,40])
parse_ast_translation‹[(\<^syntax_const>‹_AOT_exists_ellipse›, fn ctx => fn [a,b,c] =>
  Ast.mk_appl (Ast.Constant "AOT_exists")
    [Ast.mk_appl (Ast.Constant "_abs") [parseEllipseList "_AOT_vars" ctx [a,b],c]])]›
print_translation‹AOT_syntax_print_translations [
  AOT_preserve_binder_abs_tr'
    \<^const_syntax>‹AOT_exists›
    \<^syntax_const>‹_AOT_exists›
    (\<^syntax_const>‹_AOT_exists_ellipse›,true) \<^const_name>‹AOT_conj›,
  AOT_binder_trans
    @{theory}
    @{binding "AOT_exists_binder"}
    \<^syntax_const>‹_AOT_exists›
]›



syntax "_AOT_DDDOT" :: "φ" (‹...›)
syntax "_AOT_DDDOT" :: "φ" (‹…›)
parse_translation‹[(\<^syntax_const>‹_AOT_DDDOT›, parseDDOT)]›

print_translation‹AOT_syntax_print_translations
[(\<^const_syntax>‹Pure.all›, fn ctxt => fn [Abs (_, _,
  Const (\<^const_syntax>‹HOL.Trueprop›, _) $
  (Const (\<^const_syntax>‹AOT_model_valid_in›, _) $ Bound 0 $ y))] => let
    val y = (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ y)
    in (Const (\<^syntax_const>‹_AOT_nec_theorem›, dummyT) $ y) end
| [p as Abs (name, _,
  Const (\<^const_syntax>‹HOL.Trueprop›, _) $
  (Const (\<^const_syntax>‹AOT_model_valid_in›, _) $ w $ y))]
=> (Const (\<^syntax_const>‹_AOT_for_arbitrary›, dummyT) $
    (Const ("_bound", dummyT) $ Free (name, dummyT)) $
    (Term.betapply (p, (Const ("_bound", dummyT) $ Free (name, dummyT)))))
),

 (\<^const_syntax>‹AOT_model_valid_in›, fn ctxt =>
  fn [w as (Const ("_free", _) $ Free (v, _)), y] => let
    val is_world = (case (AOT_ProofData.get ctxt)
        of SOME (Free (w, _)) => Name.clean w = Name.clean v | _ => false)
    val y = (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ y)
    in if is_world then y else Const (\<^syntax_const>‹_AOT_valid›, dummyT) $ w $ y end
  | [Const (\<^const_syntax>‹w⇩0›, _), y] => let
    val y = (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ y)
    in case (AOT_ProofData.get ctxt) of SOME (Const (\<^const_name>‹w⇩0›, _)) => y |
            _ => Const (\<^syntax_const>‹_AOT_theorem›, dummyT) $ y end
  | [Const ("_var", _) $ _, y] => let
    val y = (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ y)
    in Const (\<^syntax_const>‹_AOT_nec_theorem›, dummyT) $ y end
  ),
 (\<^const_syntax>‹AOT_model_axiom›, fn ctxt => fn [trm] =>
    Const (\<^syntax_const>‹_AOT_axiom›, dummyT) $
    (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ trm)),
 (\<^const_syntax>‹AOT_model_act_axiom›, fn ctxt => fn [trm] =>
    Const (\<^syntax_const>‹_AOT_axiom›, dummyT) $
    (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ trm)),
(\<^syntax_const>‹_AOT_process_frees›, fn _ =>  fn [t] => let
  fun mapAppls (x as Const ("_free", _) $
                     Free (_, Type ("_ignore_type", [Type ("fun", _)])))
        = (Const ("_AOT_raw_appl", dummyT) $ x)
    | mapAppls (x as Const ("_free", _) $ Free (_, Type ("fun", _)))
        = (Const ("_AOT_raw_appl", dummyT) $ x)
    | mapAppls (x as Const ("_var", _) $
                     Var (_, Type ("_ignore_type", [Type ("fun", _)])))
        = (Const ("_AOT_raw_appl", dummyT) $ x)
    | mapAppls (x as Const ("_var", _) $ Var (_, Type ("fun", _)))
        = (Const ("_AOT_raw_appl", dummyT) $ x)
    | mapAppls (x $ y) = mapAppls x $ mapAppls y
    | mapAppls (Abs (x,y,z)) = Abs (x,y, mapAppls z)
    | mapAppls x = x
  in mapAppls t end
)
]
›

print_ast_translation‹AOT_syntax_print_ast_translations
let
fun handleTermOfVar x kind name = (
let
val _ = case kind of "_free" => () | "_var" => () | "_bound" => () | _ => raise Match
in
  case printVarKind name
    of (SingleVariable name) => Ast.Appl [Ast.Constant kind, Ast.Variable name]
    | (Ellipses (s, e)) =>  Ast.Appl [Ast.Constant "_AOT_free_var_ellipse",
    Ast.Appl [Ast.Constant kind, Ast.Variable s],
    Ast.Appl [Ast.Constant kind, Ast.Variable e]
      ]
  | Verbatim name => Ast.mk_appl (Ast.Constant "_AOT_quoted")
                        [Ast.mk_appl (Ast.Constant "_AOT_term_of_var") [x]]
end
)
fun termOfVar ctxt (Ast.Appl [Ast.Constant "_constrain",
      x as Ast.Appl [Ast.Constant kind, Ast.Variable name], _]) = termOfVar ctxt x
  | termOfVar ctxt (x as Ast.Appl [Ast.Constant kind, Ast.Variable name])
      = handleTermOfVar x kind name
  | termOfVar ctxt (x as Ast.Appl [Ast.Constant rep, y]) = (
let
val (restr,_) = Local_Theory.raw_theory_result (fn thy => (
let
val restrs = Symtab.dest (AOT_Restriction.get thy)
val restr = List.find (fn (n,(_,Const (c,t))) => (
  c = rep orelse c = Lexicon.unmark_const rep) | _ => false) restrs
in
(restr,thy)
end
)) ctxt
in
  case restr of SOME r => Ast.Appl [Ast.Constant (\<^const_syntax>‹AOT_term_of_var›), y]
  | _ => raise Match
end)

in
[(\<^const_syntax>‹AOT_term_of_var›, fn ctxt => fn [x] => termOfVar ctxt x),
("_AOT_raw_appl", fn ctxt => fn t::a::args => let
fun applyTermOfVar (t as Ast.Appl (Ast.Constant \<^const_syntax>‹AOT_term_of_var›::[x]))
    = (case try (termOfVar ctxt) x of SOME y => y | _ => t)
  | applyTermOfVar y = (case try (termOfVar ctxt) y of SOME x => x | _ => y)
val ts = fold (fn a => fn b => Ast.mk_appl (Ast.Constant \<^syntax_const>‹_AOT_args›)
              [b,applyTermOfVar a]) args (applyTermOfVar a)
in Ast.mk_appl (Ast.Constant \<^syntax_const>‹_AOT_appl›) [t,ts] end)]
end
›

context AOT_meta_syntax
begin
notation AOT_denotes (‹_❙↓›)
notation AOT_imp (infixl ‹❙→› 25)
notation AOT_not (‹❙¬_› [50] 50)
notation AOT_box (‹❙□_› [49] 54)
notation AOT_act (‹❙𝒜_› [49] 54)
notation AOT_forall (binder ‹❙∀› 8)
notation AOT_eq (infixl ‹❙=› 50)
notation AOT_desc (binder ‹❙ι› 100)
notation AOT_lambda (binder ‹❙λ› 100)
notation AOT_lambda0 (‹❙[❙λ _❙]›)
notation AOT_exe (‹❙⦇_,_❙⦈›)
notation AOT_model_equiv_def (infixl ‹❙≡⇩d⇩f› 10)
notation AOT_model_id_def (infixl ‹❙=⇩d⇩f› 10)
notation AOT_term_of_var (‹❙⟨_❙⟩›)
notation AOT_concrete (‹❙E❙!›)
end
context AOT_no_meta_syntax
begin
no_notation AOT_denotes (‹_❙↓›)
no_notation AOT_imp (infixl ‹❙→› 25)
no_notation AOT_not (‹❙¬_› [50] 50)
no_notation AOT_box (‹❙□_› [49] 54)
no_notation AOT_act (‹❙𝒜_› [49] 54)
no_notation AOT_forall (binder ‹❙∀› 8)
no_notation AOT_eq (infixl ‹❙=› 50)
no_notation AOT_desc (binder ‹❙ι› 100)
no_notation AOT_lambda (binder ‹❙λ› 100)
no_notation AOT_lambda0 (‹❙[❙λ _❙]›)
no_notation AOT_exe (‹❙⦇_,_❙⦈›)
no_notation AOT_model_equiv_def (infixl ‹❙≡⇩d⇩f› 10)
no_notation AOT_model_id_def (infixl ‹❙=⇩d⇩f› 10)
no_notation AOT_term_of_var (‹❙⟨_❙⟩›)
no_notation AOT_concrete (‹❙E❙!›)
end

bundle AOT_syntax
begin
declare[[show_AOT_syntax=true, show_question_marks=false, eta_contract=false]]
end

bundle AOT_no_syntax
begin
declare[[show_AOT_syntax=false, show_question_marks=true]]
end

parse_translation‹
[("_AOT_restriction", fn ctxt => fn [Const (name,_)] =>
let
val (restr, ctxt) = ctxt |> Local_Theory.raw_theory_result
  (fn thy => (Option.map fst (Symtab.lookup (AOT_Restriction.get thy) name), thy))
val restr = case restr of SOME x => x
  | _ => raise Fail ("Unknown restricted type: " ^ name)
in restr end
)]
›

print_translation‹
AOT_syntax_print_translations
[
  (\<^const_syntax>‹AOT_model_equiv_def›, fn ctxt => fn [x,y] =>
    Const (\<^syntax_const>‹_AOT_equiv_def›, dummyT) $
    (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ x) $
    (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ y))
]
›

print_translation‹
AOT_syntax_print_translations [
(\<^const_syntax>‹AOT_model_id_def›, fn ctxt =>
  fn [lhs as Abs (lhsName, lhsTy, lhsTrm), rhs as Abs (rhsName, rhsTy, rhsTrm)] =>
    let
      val (name,_) = Name.variant lhsName
        (Term.declare_term_names rhsTrm (Name.build_context (Term.declare_term_names lhsTrm)));
      val lhs = Term.betapply (lhs, Const ("_bound", dummyT) $ Free (name, lhsTy))
      val rhs = Term.betapply (rhs, Const ("_bound", dummyT) $ Free (name, rhsTy))
    in
      Const (\<^const_syntax>‹AOT_model_id_def›, dummyT) $ lhs $ rhs
    end
  | [Const (\<^const_syntax>‹case_prod›, _) $ lhs,
     Const (\<^const_syntax>‹case_prod›, _) $ rhs] =>
    Const (\<^const_syntax>‹AOT_model_id_def›, dummyT) $ lhs $ rhs
  | [Const (\<^const_syntax>‹case_unit›, _) $ lhs,
      Const (\<^const_syntax>‹case_unit›, _) $ rhs] =>
    Const (\<^const_syntax>‹AOT_model_id_def›, dummyT) $ lhs $ rhs
  | [x, y] =>
       Const (\<^syntax_const>‹_AOT_id_def›, dummyT) $
         (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ x) $
         (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ y)
)]›

text‹Special marker for printing propositions as theorems
     and for pretty-printing AOT terms.›
definition print_as_theorem :: ‹𝗈 ⇒ bool› where
  ‹print_as_theorem ≡ λ φ . ∀v . [v ⊨ φ]›
lemma print_as_theoremI:
  assumes ‹⋀ v . [v ⊨ φ]›
  shows ‹print_as_theorem φ›
  using assms by (simp add: print_as_theorem_def)
attribute_setup print_as_theorem =
  ‹Scan.succeed (Thm.rule_attribute []
      (K (fn thm => thm RS @{thm print_as_theoremI})))›
  "Print as theorem."
print_translation‹AOT_syntax_print_translations [
  (\<^const_syntax>‹print_as_theorem›, fn ctxt => fn [x] => 
   (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ x))
]›

definition print_term :: ‹'a ⇒ 'a› where ‹print_term ≡ λ x . x›
syntax "_AOT_print_term" :: ‹τ ⇒ 'a› (‹AOT'_TERM[_]›)
translations
  "_AOT_print_term φ" => "CONST print_term (_AOT_process_frees φ)"
print_translation‹AOT_syntax_print_translations [
  (\<^const_syntax>‹print_term›, fn ctxt => fn [x] => 
    (Const (\<^syntax_const>‹_AOT_process_frees›, dummyT) $ x))
]›


(* To enable meta syntax: *)
(* interpretation AOT_meta_syntax. *)
(* To disable meta syntax: *)
interpretation AOT_no_meta_syntax.

(* To enable AOT syntax (takes precedence over meta syntax;
                         can be done locally using "including" or "include"): *)
unbundle AOT_syntax
(* To disable AOT syntax (restoring meta syntax or no syntax;
                          can be done locally using "including" or "include"): *)
(* unbundle AOT_no_syntax *)

(*<*)
end
(*>*)