Theory AOT_semantics

(*<*)
theory AOT_semantics
  imports AOT_syntax
begin
(*>*)

section‹Abstract Semantics for AOT›

specification(AOT_denotes)
  ― ‹Relate object level denoting to meta-denoting. AOT's definitions of
      denoting will become derivable at each type.›
  AOT_sem_denotes: ‹[w ⊨ τ↓] = AOT_model_denotes τ›
  by (rule exI[where x=‹λ τ . ε𝗈 w . AOT_model_denotes τ›])
     (simp add: AOT_model_proposition_choice_simp)

lemma AOT_sem_var_induct[induct type: AOT_var]:
  assumes AOT_denoting_term_case: ‹⋀ τ . [v ⊨ τ↓] ⟹ [v ⊨ φ{τ}]›
  shows ‹[v ⊨ φ{α}]›
  by (simp add: AOT_denoting_term_case AOT_sem_denotes AOT_term_of_var)

text‹\linelabel{AOT_imp_spec}›
specification(AOT_imp)
  AOT_sem_imp: ‹[w ⊨ φ → ψ] = ([w ⊨ φ] ⟶ [w ⊨ ψ])›
  by (rule exI[where x=‹λ φ ψ . ε𝗈 w . ([w ⊨ φ] ⟶ [w ⊨ ψ])›])
    (simp add: AOT_model_proposition_choice_simp)

specification(AOT_not)
  AOT_sem_not: ‹[w ⊨ ¬φ] = (¬[w ⊨ φ])›
  by (rule exI[where x=‹λ φ . ε𝗈 w . ¬[w ⊨ φ]›])
     (simp add: AOT_model_proposition_choice_simp)

text‹\linelabel{AOT_box_spec}›
specification(AOT_box)
  AOT_sem_box: ‹[w ⊨ □φ] = (∀ w . [w ⊨ φ])›
  by (rule exI[where x=‹λ φ . ε𝗈 w . ∀ w . [w ⊨ φ]›])
     (simp add: AOT_model_proposition_choice_simp)

text‹\linelabel{AOT_act_spec}›
specification(AOT_act)
  AOT_sem_act: ‹[w ⊨ 𝒜φ] = [w0 ⊨ φ]›
  by (rule exI[where x=‹λ φ . ε𝗈 w . [w0 ⊨ φ]›])
     (simp add: AOT_model_proposition_choice_simp)

text‹Derived semantics for basic defined connectives.›
lemma AOT_sem_conj: ‹[w ⊨ φ & ψ] = ([w ⊨ φ] ∧ [w ⊨ ψ])›
  using AOT_conj AOT_model_equiv_def AOT_sem_imp AOT_sem_not by auto
lemma AOT_sem_equiv: ‹[w ⊨ φ ≡ ψ] = ([w ⊨ φ] = [w ⊨ ψ])›
  using AOT_equiv AOT_sem_conj AOT_model_equiv_def AOT_sem_imp by auto
lemma AOT_sem_disj: ‹[w ⊨ φ ∨ ψ] = ([w ⊨ φ] ∨ [w ⊨ ψ])›
  using AOT_disj AOT_model_equiv_def AOT_sem_imp AOT_sem_not by auto
lemma AOT_sem_dia: ‹[w ⊨ ◇φ] = (∃ w . [w ⊨ φ])›
  using AOT_dia AOT_sem_box AOT_model_equiv_def AOT_sem_not by auto

specification(AOT_forall)
  AOT_sem_forall: ‹[w ⊨ ∀α φ{α}] = (∀ τ . [w ⊨ τ↓] ⟶ [w ⊨ φ{τ}])›
  by (rule exI[where x=‹λ op . ε𝗈 w . ∀ τ . [w ⊨ τ↓] ⟶ [w ⊨ «op τ»]›])
     (simp add: AOT_model_proposition_choice_simp)

lemma AOT_sem_exists: ‹[w ⊨ ∃α φ{α}] = (∃ τ . [w ⊨ τ↓] ∧ [w ⊨ φ{τ}])›
  unfolding AOT_exists[unfolded AOT_model_equiv_def, THEN spec]
  by (simp add: AOT_sem_forall AOT_sem_not)

text‹\linelabel{AOT_eq_spec}›
specification(AOT_eq)
  ― ‹Relate identity to denoting identity in the meta-logic. AOT's definitions
      of identity will become derivable at each type.›
  AOT_sem_eq: ‹[w ⊨ τ = τ'] = ([w ⊨ τ↓] ∧ [w ⊨ τ'↓] ∧ τ = τ')›
  by (rule exI[where x=‹λ τ τ' . ε𝗈 w . [w ⊨ τ↓] ∧ [w ⊨ τ'↓] ∧ τ = τ'›])
     (simp add: AOT_model_proposition_choice_simp)

text‹\linelabel{AOT_desc_spec}›
specification(AOT_desc)
  ― ‹Descriptions denote, if there is a unique denoting object satisfying the
      matrix in the actual world.›
  AOT_sem_desc_denotes: ‹[w ⊨ ιx(φ{x})↓] = (∃! κ . [w0 ⊨ κ↓] ∧ [w0 ⊨ φ{κ}])›
  ― ‹Denoting descriptions satisfy their matrix in the actual world.›
  AOT_sem_desc_prop: ‹[w ⊨ ιx(φ{x})↓] ⟹ [w0 ⊨ φ{ιx(φ{x})}]›
  ― ‹Uniqueness of denoting descriptions.›
  AOT_sem_desc_unique: ‹[w ⊨ ιx(φ{x})↓] ⟹ [w ⊨ κ↓] ⟹ [w0 ⊨ φ{κ}] ⟹
                        [w ⊨ ιx(φ{x}) = κ]›
proof -
  have ‹∃x::'a . ¬AOT_model_denotes x›
    using AOT_model_nondenoting_ex
    by blast
  text‹Note that we may choose a distinct non-denoting object for each matrix.
       We do this explicitly merely to convince ourselves that our specification
       can still be satisfied.›
  then obtain nondenoting :: ‹('a ⇒ 𝗈) ⇒ 'a› where
    nondenoting: ‹∀ φ . ¬AOT_model_denotes (nondenoting φ)›
    by fast
  define desc where
    ‹desc = (λ φ . if (∃! κ . [w0 ⊨ κ↓] ∧ [w0 ⊨ φ{κ}])
                   then (THE κ . [w0 ⊨ κ↓] ∧ [w0 ⊨ φ{κ}])
                   else nondenoting φ)›
  {
    fix φ :: ‹'a ⇒ 𝗈›
    assume ex1: ‹∃! κ . [w0 ⊨ κ↓] ∧ [w0 ⊨ φ{κ}]›
    then obtain κ where x_prop: "[w0 ⊨ κ↓] ∧ [w0 ⊨ φ{κ}]"
      unfolding AOT_sem_denotes by blast
    moreover have "(desc φ) = κ"
      unfolding desc_def using x_prop ex1 by fastforce
    ultimately have "[w0 ⊨ «desc φ»↓] ∧ [w0 ⊨ «φ (desc φ)»]"
      by blast
  } note 1 = this
  moreover {
    fix φ :: ‹'a ⇒ 𝗈›
    assume nex1: ‹∄! κ . [w0 ⊨ κ↓] ∧ [w0 ⊨ φ{κ}]›
    hence "(desc φ) = nondenoting φ" by (simp add: desc_def AOT_sem_denotes)
    hence "[w ⊨ ¬«desc φ»↓]" for w
      by (simp add: AOT_sem_denotes nondenoting AOT_sem_not)
  }
  ultimately have desc_denotes_simp:
    ‹[w ⊨ «desc φ»↓] = (∃! κ . [w0 ⊨ κ↓] ∧ [w0 ⊨ φ{κ}])› for φ w
    by (simp add: AOT_sem_denotes desc_def nondenoting)
  have ‹(∀φ w. [w ⊨ «desc φ»↓] = (∃!κ. [w0 ⊨ κ↓] ∧ [w0 ⊨ φ{κ}])) ∧
    (∀φ w. [w ⊨ «desc φ»↓] ⟶ [w0 ⊨ «φ (desc φ)»]) ∧
    (∀φ w κ. [w ⊨ «desc φ»↓] ⟶ [w ⊨ κ↓] ⟶ [w0 ⊨ φ{κ}] ⟶
             [w ⊨ «desc φ» = κ])›
    by (insert 1; auto simp: desc_denotes_simp AOT_sem_eq AOT_sem_denotes
                             desc_def nondenoting)
  thus ?thesis
    by (safe intro!: exI[where x=desc]; presburger)
qed

text‹\linelabel{AOT_exe_lambda_spec}›
specification(AOT_exe AOT_lambda)
  ― ‹Truth conditions of exemplification formulas.›
  AOT_sem_exe: ‹[w ⊨ [Π]κ1...κn] = ([w ⊨ Π↓] ∧ [w ⊨ κ1...κn↓] ∧
                                     [w ⊨ «Rep_rel Π κ1κn»])›
  ― ‹\eta-conversion for denoting terms; equivalent to AOT's axiom›
  AOT_sem_lambda_eta: ‹[w ⊨ Π↓] ⟹ [w ⊨ [λν1...νn [Π]ν1...νn] = Π]›
  ― ‹\beta-conversion; equivalent to AOT's axiom›
  AOT_sem_lambda_beta: ‹[w ⊨ [λν1...νn φ{ν1...νn}]↓] ⟹ [w ⊨ κ1...κn↓] ⟹
                        [w ⊨ [λν1...νn φ{ν1...νn}]κ1...κn] = [w ⊨ φ{κ1...κn}]›
  ― ‹Necessary and sufficient conditions for relations to denote. Equivalent
      to a theorem of AOT and used to derive the base cases of denoting relations
      (cqt.2).›
  AOT_sem_lambda_denotes: ‹[w ⊨ [λν1...νn φ{ν1...νn}]↓] =
    (∀ v κ1κn κ1'κn' . [v ⊨ κ1...κn↓] ∧ [v ⊨ κ1'...κn'↓] ∧
        (∀ Π v . [v ⊨ Π↓] ⟶ [v ⊨ [Π]κ1...κn] = [v ⊨ [Π]κ1'...κn']) ⟶
                 [v ⊨ φ{κ1...κn}] = [v ⊨ φ{κ1'...κn'}])›
  ― ‹Equivalent to AOT's coexistence axiom.›
  AOT_sem_lambda_coex: ‹[w ⊨ [λν1...νn φ{ν1...νn}]↓] ⟹
    (∀ w κ1κn . [w ⊨ κ1...κn↓] ⟶ [w ⊨ φ{κ1...κn}] = [w ⊨ ψ{κ1...κn}]) ⟹
    [w ⊨ [λν1...νn ψ{ν1...νn}]↓]›
  ― ‹Only the unary case of the following should hold, but our specification
      has to range over all types. We might move @{const AOT_exe} and
      @{const AOT_lambda} to type classes in the future to solve this.›
  AOT_sem_lambda_eq_prop_eq: ‹«[λν1...νn φ]» = «[λν1...νn ψ]» ⟹ φ = ψ›
  ― ‹The following is solely required for validating n-ary relation identity
      and has the danger of implying artifactual theorems. Possibly avoidable
      by moving @{const AOT_exe} and @{const AOT_lambda} to type classes.›
  AOT_sem_exe_denoting: ‹[w ⊨ Π↓] ⟹ AOT_exe Π κs = Rep_rel Π κs›
  ― ‹The following is required for validating the base cases of denoting
      relations (cqt.2). A version of this meta-logical identity will
      become derivable in future versions of AOT, so this will ultimately not
      result in artifactual theorems.›
  AOT_sem_exe_equiv: ‹AOT_model_term_equiv x y ⟹ AOT_exe Π x = AOT_exe Π y›
proof -
  have ‹∃ x :: <'a> . ¬AOT_model_denotes x›
    by (rule exI[where x=‹Abs_rel (λ x . ε𝗈 w. True)›])
       (meson AOT_model_denotes_rel.abs_eq AOT_model_nondenoting_ex
              AOT_model_proposition_choice_simp)
  define exe :: ‹<'a> ⇒ 'a ⇒ 𝗈› where
    ‹exe ≡ λ Π κs . if AOT_model_denotes Π
                     then Rep_rel Π κs
                     else (ε𝗈 w . False)›
  define lambda :: ‹('a⇒𝗈) ⇒ <'a>› where
    ‹lambda ≡ λ φ . if AOT_model_denotes (Abs_rel φ)
      then (Abs_rel φ)
      else
        if (∀ κ κ' w . (AOT_model_denotes κ ∧ AOT_model_term_equiv κ κ') ⟶
                       [w ⊨ «φ κ»] = [w ⊨ «φ κ'»])
        then
          Abs_rel (fix_irregular (λ x . if AOT_model_denotes x
                                        then φ (SOME y . AOT_model_term_equiv x y)
                                        else  (ε𝗈 w . False)))
        else 
          Abs_rel φ›
  have fix_irregular_denoting_simp[simp]:
    ‹fix_irregular (λx. if AOT_model_denotes x then φ x else ψ x) κ = φ κ›
    if ‹AOT_model_denotes κ›
    for κ :: 'a and φ ψ
    by (simp add: that fix_irregular_denoting)
  have denoting_eps_cong[cong]:
    ‹[w ⊨ «φ (Eps (AOT_model_term_equiv κ))»] = [w ⊨ «φ κ»]›
    if ‹AOT_model_denotes κ›
    and ‹∀ κ κ'. AOT_model_denotes κ ∧ AOT_model_term_equiv κ κ' ⟶
                 (∀w. [w ⊨ «φ κ»] = [w ⊨ «φ κ'»])›
    for w :: w and κ :: 'a and φ :: ‹'a⇒𝗈›
    using that AOT_model_term_equiv_eps(2) by blast
  have exe_rep_rel: ‹[w ⊨ «exe Π κ1κn»] = ([w ⊨ Π↓] ∧ [w ⊨ κ1...κn↓] ∧
                                            [w ⊨ «Rep_rel Π κ1κn»])› for w Π κ1κn
    by (metis AOT_model_denotes_rel.rep_eq exe_def AOT_sem_denotes
              AOT_model_proposition_choice_simp)
  moreover have ‹[w ⊨ «Π»↓] ⟹ [w ⊨ «lambda (exe Π)» = «Π»]› for Π w
    by (auto simp: Rep_rel_inverse lambda_def AOT_sem_denotes AOT_sem_eq
                   AOT_model_denotes_rel_def Abs_rel_inverse exe_def)
  moreover have lambda_denotes_beta:
    ‹[w ⊨ «exe (lambda φ) κ »] = [w ⊨ «φ κ»]›
    if ‹[w ⊨ «lambda φ»↓]› and ‹[w ⊨ «κ»↓]›
    for φ κ w
    using that unfolding exe_def AOT_sem_denotes
    by (auto simp: lambda_def Abs_rel_inverse split: if_split_asm)
  moreover have lambda_denotes_simp:
    ‹[w ⊨ «lambda φ»↓] = (∀ v κ1κn κ1'κn' . [v ⊨ κ1...κn↓] ∧ [v ⊨ κ1'...κn'↓] ∧
        (∀ Π v . [v ⊨ Π↓] ⟶ [v ⊨ «exe Π κ1κn»] = [v ⊨ «exe Π κ1'κn'»]) ⟶
        [v ⊨ φ{κ1...κn}] = [v ⊨ φ{κ1'...κn'}])› for φ w
  proof
    assume ‹[w ⊨ «lambda φ»↓]›
    hence ‹AOT_model_denotes (lambda φ)›
      unfolding AOT_sem_denotes by simp
    moreover have ‹[w ⊨ «φ κ»] ⟹ [w ⊨ «φ κ'»]›
      and ‹[w ⊨ «φ κ'»] ⟹ [w ⊨ «φ κ»]›
      if ‹AOT_model_denotes κ› and ‹AOT_model_term_equiv κ κ'›
      for w κ κ'
      by (metis (no_types, lifting) AOT_model_denotes_rel.abs_eq lambda_def
                                    that calculation)+
    ultimately show ‹∀ v κ1κn κ1'κn' . [v ⊨ κ1...κn↓] ∧ [v ⊨ κ1'...κn'↓] ∧
        (∀ Π v . [v ⊨ Π↓] ⟶ [v ⊨ «exe Π κ1κn»] = [v ⊨ «exe Π κ1'κn'»]) ⟶
        [v ⊨ φ{κ1...κn}] = [v ⊨ φ{κ1'...κn'}]›
      unfolding AOT_sem_denotes
      by (metis (no_types) AOT_sem_denotes lambda_denotes_beta)
  next
    assume ‹∀ v κ1κn κ1'κn' . [v ⊨ κ1...κn↓] ∧ [v ⊨ κ1'...κn'↓] ∧
      (∀ Π v . [v ⊨ Π↓] ⟶ [v ⊨ «exe Π κ1κn»] = [v ⊨ «exe Π κ1'κn'»]) ⟶
      [v ⊨ φ{κ1...κn}] = [v ⊨ φ{κ1'...κn'}]›
    hence ‹[w ⊨ «φ κ»] = [w ⊨ «φ κ'»]›
      if ‹AOT_model_denotes κ ∧ AOT_model_denotes κ' ∧ AOT_model_term_equiv κ κ'›
      for w κ κ'
      using that
      by (auto simp: AOT_sem_denotes)
         (meson AOT_model_term_equiv_rel_equiv AOT_sem_denotes exe_rep_rel)+
    hence ‹[w ⊨ «φ κ»] = [w ⊨ «φ κ'»]›
      if ‹AOT_model_denotes κ ∧ AOT_model_term_equiv κ κ'›
      for w κ κ'
      using that AOT_model_term_equiv_denotes by blast
    hence ‹AOT_model_denotes (lambda φ)›
      by (auto simp: lambda_def Abs_rel_inverse AOT_model_denotes_rel.abs_eq
                     AOT_model_irregular_equiv AOT_model_term_equiv_eps(3)
                     AOT_model_term_equiv_regular fix_irregular_def AOT_sem_denotes
                     AOT_model_term_equiv_denotes AOT_model_proposition_choice_simp
                     AOT_model_irregular_false
               split: if_split_asm
               intro: AOT_model_irregular_eqI)
    thus ‹[w ⊨ «lambda φ»↓]›
      by (simp add: AOT_sem_denotes)
  qed
  moreover have ‹[w ⊨ «lambda ψ»↓]›
    if ‹[w ⊨ «lambda φ»↓]›
    and ‹∀ w κ1κn . [w ⊨ κ1...κn↓] ⟶ [w ⊨ φ{κ1...κn}] = [w ⊨ ψ{κ1...κn}]›
    for φ ψ w using that unfolding lambda_denotes_simp by auto
  moreover have ‹[w ⊨ Π↓] ⟹ exe Π κs = Rep_rel Π κs› for Π κs w
    by (simp add: exe_def AOT_sem_denotes)
  moreover have ‹lambda (λx. p) = lambda (λx. q) ⟹ p = q› for p q
    unfolding lambda_def
    by (auto split: if_split_asm simp: Abs_rel_inject fix_irregular_def)
       (meson AOT_model_irregular_nondenoting AOT_model_denoting_ex)+
  moreover have ‹AOT_model_term_equiv x y ⟹ exe Π x = exe Π y› for x y Π
    unfolding exe_def
    by (meson AOT_model_denotes_rel.rep_eq)
  note calculation = calculation this
  show ?thesis
    apply (safe intro!: exI[where x=exe] exI[where x=lambda])
    using calculation apply simp_all
    using lambda_denotes_simp by blast+
qed

lemma AOT_model_lambda_denotes:
  ‹AOT_model_denotes (AOT_lambda φ) = (∀ v κ κ' .
    AOT_model_denotes κ ∧ AOT_model_denotes κ' ∧ AOT_model_term_equiv κ κ' ⟶
    [v ⊨ «φ κ»] = [v ⊨ «φ κ'»])›
proof(safe)
  fix v and κ κ' :: 'a
  assume ‹AOT_model_denotes (AOT_lambda φ)›
  hence 1: ‹AOT_model_denotes κ1κn ∧
        AOT_model_denotes κ1'κn' ∧
        (∀Π v. AOT_model_denotes Π ⟶ [v ⊨ [Π]κ1...κn] = [v ⊨ [Π]κ1'...κn']) ⟶
        [v ⊨ φ{κ1...κn}] = [v ⊨ φ{κ1'...κn'}]› for κ1κn κ1'κn' v
    using AOT_sem_lambda_denotes[simplified AOT_sem_denotes] by blast
  {
    fix v and κ1κn κ1'κn' :: 'a
    assume d: ‹AOT_model_denotes κ1κn ∧ AOT_model_denotes κ1'κn' ∧
               AOT_model_term_equiv κ1κn κ1'κn'›
    hence ‹∀Π w. AOT_model_denotes Π ⟶ [w ⊨ [Π]κ1...κn] = [w ⊨ [Π]κ1'...κn']›
      by (metis AOT_sem_exe_equiv)
    hence ‹[v ⊨ φ{κ1...κn}] = [v ⊨ φ{κ1'...κn'}]› using d 1 by auto
  }
  moreover assume ‹AOT_model_denotes κ›
  moreover assume ‹AOT_model_denotes κ'›
  moreover assume ‹AOT_model_term_equiv κ κ'›
  ultimately show ‹[v ⊨ «φ κ»] ⟹ [v ⊨ «φ κ'»]›
              and ‹[v ⊨ «φ κ'»] ⟹ [v ⊨ «φ κ»]›
    by auto
next
  assume 0: ‹∀ v κ κ' . AOT_model_denotes κ ∧ AOT_model_denotes κ' ∧
                        AOT_model_term_equiv κ κ' ⟶ [v ⊨ «φ κ»] = [v ⊨ «φ κ'»]›
  {
    fix κ1κn κ1'κn' :: 'a
    assume den: ‹AOT_model_denotes κ1κn›
    moreover assume den': ‹AOT_model_denotes κ1'κn'›
    assume ‹∀Π v . AOT_model_denotes Π ⟶
                   [v ⊨ [Π]κ1...κn] = [v ⊨ [Π]κ1'...κn']›
    hence ‹∀Π v . AOT_model_denotes Π ⟶
                   [v ⊨ «Rep_rel Π κ1κn»] = [v ⊨ «Rep_rel Π κ1'κn'»]›
      by (simp add: AOT_sem_denotes AOT_sem_exe den den')
    hence "AOT_model_term_equiv κ1κn κ1'κn'"
      unfolding AOT_model_term_equiv_rel_equiv[OF den, OF den']
      by argo
    hence ‹[v ⊨ φ{κ1...κn}] = [v ⊨ φ{κ1'...κn'}]› for v
      using den den' 0 by blast
  }
  thus ‹AOT_model_denotes (AOT_lambda φ)›
    unfolding AOT_sem_lambda_denotes[simplified AOT_sem_denotes]
    by blast
qed

specification (AOT_lambda0)
  AOT_sem_lambda0: "AOT_lambda0 φ = φ"
  by (rule exI[where x=‹λx. x›]) simp

specification(AOT_concrete)
  AOT_sem_concrete: ‹[w ⊨ [E!]κ] =
                     AOT_model_concrete w κ›
  by (rule exI[where x=‹AOT_var_of_term (Abs_rel
                          (λ x . ε𝗈 w . AOT_model_concrete w x))›];
      subst AOT_var_of_term_inverse)
     (auto simp: AOT_model_unary_regular AOT_model_concrete_denotes
                 AOT_model_concrete_equiv AOT_model_regular_κ_def
                 AOT_model_proposition_choice_simp AOT_sem_exe Abs_rel_inverse
                 AOT_model_denotes_rel_def AOT_sem_denotes)

lemma AOT_sem_equiv_defI:
  assumes ‹⋀ v . [v ⊨ φ] ⟹ [v ⊨ ψ]›
      and ‹⋀ v . [v ⊨ ψ] ⟹ [v ⊨ φ]›
    shows ‹AOT_model_equiv_def φ ψ›
  using AOT_model_equiv_def assms by blast

lemma AOT_sem_id_defI:
  assumes ‹⋀ α v . [v ⊨ «σ α»↓] ⟹ [v ⊨ «τ α» = «σ α»]›
  assumes ‹⋀ α v . ¬[v ⊨ «σ α»↓] ⟹ [v ⊨ ¬«τ α»↓]›
  shows ‹AOT_model_id_def τ σ›
  using assms
  unfolding AOT_sem_denotes AOT_sem_eq AOT_sem_not
  using AOT_model_id_def[THEN iffD2]
  by metis

lemma AOT_sem_id_def2I:
  assumes ‹⋀ α β v . [v ⊨ «σ α β»↓] ⟹ [v ⊨ «τ α β» = «σ α β»]›
  assumes ‹⋀ α β v . ¬[v ⊨ «σ α β»↓] ⟹ [v ⊨ ¬«τ α β»↓]›
  shows ‹AOT_model_id_def (case_prod τ) (case_prod σ)›
  apply (rule AOT_sem_id_defI)
  using assms by (auto simp: AOT_sem_conj AOT_sem_not AOT_sem_eq AOT_sem_denotes
      AOT_model_denotes_prod_def)

lemma AOT_sem_id_defE1:
  assumes ‹AOT_model_id_def τ σ›
      and ‹[v ⊨ «σ α»↓]›
    shows ‹[v ⊨ «τ α» = «σ α»]›
  using assms by (simp add: AOT_model_id_def AOT_sem_denotes AOT_sem_eq)

lemma AOT_sem_id_defE2:
  assumes ‹AOT_model_id_def τ σ›
      and ‹¬[v ⊨ «σ α»↓]›
    shows ‹¬[v ⊨ «τ α»↓]›
  using assms by (simp add: AOT_model_id_def AOT_sem_denotes AOT_sem_eq)

lemma AOT_sem_id_def0I:
  assumes ‹⋀ v . [v ⊨ σ↓] ⟹ [v ⊨ τ = σ]›
      and ‹⋀ v . ¬[v ⊨ σ↓] ⟹ [v ⊨ ¬τ↓]›
  shows ‹AOT_model_id_def (case_unit τ) (case_unit σ)›
  apply (rule AOT_sem_id_defI)
  using assms
  by (simp_all add: AOT_sem_conj AOT_sem_eq AOT_sem_not AOT_sem_denotes
                    AOT_model_denotes_unit_def case_unit_Unity)

lemma AOT_sem_id_def0E1:
  assumes ‹AOT_model_id_def (case_unit τ) (case_unit σ)›
      and ‹[v ⊨ σ↓]›
    shows ‹[v ⊨ τ = σ]›
  by (metis (full_types) AOT_sem_id_defE1 assms(1) assms(2) case_unit_Unity)

lemma AOT_sem_id_def0E2:
  assumes ‹AOT_model_id_def (case_unit τ) (case_unit σ)›
      and ‹¬[v ⊨ σ↓]›
    shows ‹¬[v ⊨ τ↓]›
  by (metis AOT_sem_id_defE2 assms(1) assms(2) case_unit_Unity)

lemma AOT_sem_id_def0E3:
  assumes ‹AOT_model_id_def (case_unit τ) (case_unit σ)›
      and ‹[v ⊨ σ↓]›
    shows ‹[v ⊨ τ↓]›
  using AOT_sem_id_def0E1[OF assms]
  by (simp add: AOT_sem_eq AOT_sem_denotes)

lemma AOT_sem_ordinary_def_denotes: ‹[w ⊨ [λx ◇[E!]x]↓]›
  unfolding AOT_sem_denotes AOT_model_lambda_denotes
  by (auto simp: AOT_sem_dia AOT_model_concrete_equiv
                 AOT_sem_concrete AOT_sem_denotes)
lemma AOT_sem_abstract_def_denotes: ‹[w ⊨ [λx ¬◇[E!]x]↓]›
  unfolding AOT_sem_denotes AOT_model_lambda_denotes
  by (auto simp: AOT_sem_dia AOT_model_concrete_equiv
                 AOT_sem_concrete AOT_sem_denotes AOT_sem_not)

text‹Relation identity is constructed using an auxiliary abstract projection
     mechanism with suitable instantiations for @{typ κ} and products.›
class AOT_RelationProjection = 
  fixes AOT_sem_proj_id :: ‹'a::AOT_IndividualTerm ⇒ ('a ⇒ 𝗈) ⇒ ('a ⇒ 𝗈) ⇒ 𝗈›
  assumes AOT_sem_proj_id_prop:
    ‹[v ⊨ Π = Π'] =
     [v ⊨ Π↓ & Π'↓ & ∀α («AOT_sem_proj_id α (λ τ . «[Π]τ») (λ τ . «[Π']τ»)»)]›
      and AOT_sem_proj_id_refl:
    ‹[v ⊨ τ↓] ⟹ [v ⊨ [λν1...νn φ{ν1...νn}] = [λν1...νn φ{ν1...νn}]] ⟹
     [v ⊨ «AOT_sem_proj_id τ φ φ»]›

class AOT_UnaryRelationProjection = AOT_RelationProjection +
  assumes AOT_sem_unary_proj_id:
    ‹AOT_sem_proj_id κ φ ψ = «[λν1...νn φ{ν1...νn}] = [λν1...νn ψ{ν1...νn}]»›

instantiation κ :: AOT_UnaryRelationProjection
begin
definition AOT_sem_proj_id_κ :: ‹κ ⇒ (κ ⇒ 𝗈) ⇒ (κ ⇒ 𝗈) ⇒ 𝗈› where
  ‹AOT_sem_proj_id_κ κ φ ψ = «[λz φ{z}] = [λz ψ{z}]»›
instance proof
  show ‹[v ⊨ Π = Π'] =
        [v ⊨ Π↓ & Π'↓ & ∀α («AOT_sem_proj_id α (λ τ . «[Π]τ») (λ τ . «[Π']τ»)»)]›
    for v and Π Π' :: ‹<κ>›
    unfolding AOT_sem_proj_id_κ_def
    by (simp add: AOT_sem_eq AOT_sem_conj AOT_sem_denotes AOT_sem_forall)
       (metis AOT_sem_denotes AOT_model_denoting_ex AOT_sem_eq AOT_sem_lambda_eta)
next
  show ‹AOT_sem_proj_id κ φ ψ = «[λν1...νn φ{ν1...νn}] = [λν1...νn ψ{ν1...νn}]»›
    for κ :: κ and φ ψ
    unfolding AOT_sem_proj_id_κ_def ..
next
  show ‹[v ⊨ «AOT_sem_proj_id τ φ φ»]›
    if ‹[v ⊨ τ↓]› and ‹[v ⊨ [λν1...νn φ{ν1...νn}] = [λν1...νn φ{ν1...νn}]]›
    for τ :: κ and v φ
    using that by (simp add: AOT_sem_proj_id_κ_def AOT_sem_eq)
qed
end

instantiation prod ::
  ("{AOT_UnaryRelationProjection, AOT_UnaryIndividualTerm}", AOT_RelationProjection)
  AOT_RelationProjection
begin
definition AOT_sem_proj_id_prod :: ‹'a×'b ⇒ ('a×'b ⇒ 𝗈) ⇒ ('a×'b ⇒ 𝗈) ⇒ 𝗈› where
  ‹AOT_sem_proj_id_prod ≡ λ (x,y) φ ψ . «[λz «φ (z,y)»] = [λz «ψ (z,y)»] &
    «AOT_sem_proj_id y (λ a . φ (x,a)) (λ a . ψ (x,a))»»›
instance proof
  text‹This is the main proof that allows to derive the definition of n-ary
       relation identity. We need to show that our defined projection identity
       implies relation identity for relations on pairs of individual terms.›
  fix v and Π Π' :: ‹<'a×'b>›
  have AOT_meta_proj_denotes1: ‹AOT_model_denotes (Abs_rel (λz. AOT_exe Π (z, β)))›
    if ‹AOT_model_denotes Π› for Π :: ‹<'a×'b>› and β
    using that unfolding AOT_model_denotes_rel.rep_eq
    apply (simp add: Abs_rel_inverse AOT_meta_prod_equivI(2) AOT_sem_denotes
                      that)
    by (metis (no_types, lifting) AOT_meta_prod_equivI(2) AOT_model_denotes_prod_def
              AOT_model_unary_regular AOT_sem_exe AOT_sem_exe_equiv case_prodD)
  {
    fix κ :: 'a and Π :: ‹<'a×'b>›
    assume Π_denotes: ‹AOT_model_denotes Π›
    assume α_denotes: ‹AOT_model_denotes κ›
    hence ‹AOT_exe Π (κ, x) = AOT_exe Π (κ, y)›
      if ‹AOT_model_term_equiv x y› for x y :: 'b
      by (simp add: AOT_meta_prod_equivI(1) AOT_sem_exe_equiv that)
    moreover have ‹AOT_model_denotes κ1'κn'›
               if ‹[w ⊨ [Π]κ κ1'...κn']› for w κ1'κn'
      by (metis that AOT_model_denotes_prod_def AOT_sem_exe
                AOT_sem_denotes case_prodD)
    moreover {
      fix x :: 'b
      assume x_irregular: ‹¬AOT_model_regular x›
      hence prod_irregular: ‹¬AOT_model_regular (κ, x)›
        by (metis (no_types, lifting) AOT_model_irregular_nondenoting
                                      AOT_model_regular_prod_def case_prodD)
      hence ‹(¬AOT_model_denotes κ ∨ ¬AOT_model_regular x) ∧
             (AOT_model_denotes κ ∨ ¬AOT_model_denotes x)›
        unfolding AOT_model_regular_prod_def by blast
      hence x_nonden: ‹¬AOT_model_regular x›
        by (simp add: α_denotes)
      have ‹Rep_rel Π (κ, x) = AOT_model_irregular (Rep_rel Π) (κ, x)›
        using AOT_model_denotes_rel.rep_eq Π_denotes prod_irregular by blast
      moreover have ‹AOT_model_irregular (Rep_rel Π) (κ, x) =
                     AOT_model_irregular (λz. Rep_rel Π (κ, z)) x›
        using Π_denotes x_irregular prod_irregular x_nonden
        using AOT_model_irregular_prod_generic
        apply (induct arbitrary: Π x rule: AOT_model_irregular_prod.induct)
        by (auto simp: α_denotes AOT_model_irregular_nondenoting
                       AOT_model_regular_prod_def AOT_meta_prod_equivI(2)
                       AOT_model_denotes_rel.rep_eq AOT_model_term_equiv_eps(1)
                 intro!: AOT_model_irregular_eqI)
      ultimately have
        ‹AOT_exe Π (κ, x) = AOT_model_irregular (λz. AOT_exe Π (κ, z)) x›
        unfolding AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π_denotes]
        by auto
    }
    ultimately have ‹AOT_model_denotes (Abs_rel (λz. AOT_exe Π (κ, z)))›
      by (simp add: Abs_rel_inverse AOT_model_denotes_rel.rep_eq)
  } note AOT_meta_proj_denotes2 = this
  {
    fix κ1'κn' :: 'b and Π :: ‹<'a×'b>›
    assume Π_denotes: ‹AOT_model_denotes Π›
    assume β_denotes: ‹AOT_model_denotes κ1'κn'›
    hence ‹AOT_exe Π (x, κ1'κn') = AOT_exe Π (y, κ1'κn')›
      if ‹AOT_model_term_equiv x y› for x y :: 'a
      by (simp add: AOT_meta_prod_equivI(2) AOT_sem_exe_equiv that)
    moreover have ‹AOT_model_denotes κ›
               if ‹[w ⊨ [Π]κ κ1'...κn']› for w κ
      by (metis that AOT_model_denotes_prod_def AOT_sem_exe
                AOT_sem_denotes case_prodD)
    moreover {
      fix x :: 'a
      assume ‹¬AOT_model_regular x›
      hence ‹False›
        using AOT_model_unary_regular by blast
      hence
        ‹AOT_exe Π (x,κ1'κn') = AOT_model_irregular (λz. AOT_exe Π (z,κ1'κn')) x›
        unfolding AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π_denotes]
        by auto
    }
    ultimately have ‹AOT_model_denotes (Abs_rel (λz. AOT_exe Π (z,κ1'κn')))›
      by (simp add: Abs_rel_inverse AOT_model_denotes_rel.rep_eq)
  } note AOT_meta_proj_denotes1 = this
  {
    assume Π_denotes: ‹AOT_model_denotes Π›
    assume Π'_denotes: ‹AOT_model_denotes Π'›
    have Π_proj2_den: ‹AOT_model_denotes (Abs_rel (λz. Rep_rel Π (α, z)))›
      if ‹AOT_model_denotes α› for α
      using that AOT_meta_proj_denotes2[OF Π_denotes]
            AOT_sem_exe_denoting[simplified AOT_sem_denotes,OF Π_denotes] by simp
    have Π'_proj2_den: ‹AOT_model_denotes (Abs_rel (λz. Rep_rel Π' (α, z)))›
      if ‹AOT_model_denotes α› for α
      using that AOT_meta_proj_denotes2[OF Π'_denotes]
            AOT_sem_exe_denoting[simplified AOT_sem_denotes,OF Π'_denotes] by simp
    have Π_proj1_den: ‹AOT_model_denotes (Abs_rel (λz. Rep_rel Π (z, α)))›
      if ‹AOT_model_denotes α› for α
      using that AOT_meta_proj_denotes1[OF Π_denotes]
            AOT_sem_exe_denoting[simplified AOT_sem_denotes,OF Π_denotes] by simp
    have Π'_proj1_den: ‹AOT_model_denotes (Abs_rel (λz. Rep_rel Π' (z, α)))›
      if ‹AOT_model_denotes α› for α
      using that AOT_meta_proj_denotes1[OF Π'_denotes]
            AOT_sem_exe_denoting[simplified AOT_sem_denotes,OF Π'_denotes] by simp
    {
      fix κ :: 'a and κ1'κn' :: 'b
      assume ‹Π = Π'›
      assume ‹AOT_model_denotes (κ,κ1'κn')›
      hence ‹AOT_model_denotes κ› and beta_denotes: ‹AOT_model_denotes κ1'κn'›
        by (auto simp: AOT_model_denotes_prod_def)
      have ‹AOT_model_denotes «[λz [Π]z κ1'...κn']»›
        by (rule AOT_model_lambda_denotes[THEN iffD2])
           (metis AOT_sem_exe_denoting AOT_meta_prod_equivI(2)
                  AOT_model_denotes_rel.rep_eq AOT_sem_denotes
                  AOT_sem_exe_denoting Π_denotes)
      moreover have ‹«[λz [Π]z κ1'...κn']» = «[λz [Π']z κ1'...κn']»›
        by (simp add: ‹Π = Π'›)
      moreover have ‹[v ⊨ «AOT_sem_proj_id κ1'κn' (λκ1'κn'. «[Π]κ κ1'...κn'»)
                                                  (λκ1'κn'. «[Π']κ κ1'...κn'»)»]›
        unfolding ‹Π = Π'› using beta_denotes
        by (rule AOT_sem_proj_id_refl[unfolded AOT_sem_denotes];
            simp add: AOT_sem_denotes AOT_sem_eq AOT_model_lambda_denotes)
           (metis AOT_meta_prod_equivI(1) AOT_model_denotes_rel.rep_eq
                  AOT_sem_exe AOT_sem_exe_denoting Π'_denotes)
      ultimately have ‹[v ⊨ «AOT_sem_proj_id (κ,κ1'κn') (λ κ1κn . «[Π]κ1...κn»)
                                                         (λ κ1κn . «[Π']κ1...κn»)»]›
        unfolding AOT_sem_proj_id_prod_def
        by (simp add: AOT_sem_denotes AOT_sem_conj AOT_sem_eq)
    }
    moreover {
      assume ‹⋀ α . AOT_model_denotes α ⟹
        [v ⊨ «AOT_sem_proj_id α (λ κ1κn . «[Π]κ1...κn») (λ κ1κn . «[Π']κ1...κn»)»]›
      hence 0: ‹AOT_model_denotes κ ⟹ AOT_model_denotes κ1'κn' ⟹
             AOT_model_denotes «[λz [Π]z κ1'...κn']» ∧
             AOT_model_denotes «[λz [Π']z κ1'...κn']» ∧
             «[λz [Π]z κ1'...κn']» = «[λz [Π']z κ1'...κn']» ∧
             [v ⊨ «AOT_sem_proj_id κ1'κn' (λκ1κn. «[Π]κ κ1...κn»)
                                          (λκ1κn. «[Π']κ κ1...κn»)»]› for κ κ1'κn'
        unfolding AOT_sem_proj_id_prod_def
        by (auto simp: AOT_sem_denotes AOT_sem_conj AOT_sem_eq
                       AOT_model_denotes_prod_def)
      obtain αden :: 'a and βden :: 'b where
        αden: ‹AOT_model_denotes αden› and βden: ‹AOT_model_denotes βden›
        using AOT_model_denoting_ex by metis
      {
        fix κ :: 'a
        assume αdenotes: ‹AOT_model_denotes κ›
        have 1: ‹[v ⊨ «AOT_sem_proj_id κ1'κn' (λκ1'κn'. «[Π]κ κ1'...κn'»)
                                              (λκ1'κn'. «[Π']κ κ1'...κn'»)»]›
          if ‹AOT_model_denotes κ1'κn'› for κ1'κn'
          using that 0 using αdenotes by blast
        hence ‹[v ⊨ «AOT_sem_proj_id β (λz. Rep_rel Π (κ, z))
                                        (λz. Rep_rel Π' (κ, z))»]›
          if ‹AOT_model_denotes β› for β
          using that
          unfolding AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π_denotes]
                    AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π'_denotes]
          by blast
        hence ‹Abs_rel (λz. Rep_rel Π (κ, z)) = Abs_rel (λz. Rep_rel Π' (κ, z))›
          using AOT_sem_proj_id_prop[of v ‹Abs_rel (λz. Rep_rel Π (κ, z))›
                                          ‹Abs_rel (λz. Rep_rel Π' (κ, z))›,
                  simplified AOT_sem_eq AOT_sem_conj AOT_sem_forall
                             AOT_sem_denotes, THEN iffD2]
                Π_proj2_den[OF αdenotes] Π'_proj2_den[OF αdenotes]
          unfolding AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π_denotes]
                    AOT_sem_exe_denoting[simplified AOT_sem_denotes,
                                         OF Π_proj2_den[OF αdenotes]]
                    AOT_sem_exe_denoting[simplified AOT_sem_denotes,
                                         OF Π'_proj2_den[OF αdenotes]]
          by (metis Abs_rel_inverse UNIV_I)
        hence "Rep_rel Π (κ,β) = Rep_rel Π' (κ,β)" for β
          by (simp add: Abs_rel_inject[simplified]) meson
      } note αdenotes = this
      {
        fix κ1'κn' :: 'b
        assume βden: ‹AOT_model_denotes κ1'κn'›
        have 1: ‹«[λz [Π]z κ1'...κn']» = «[λz [Π']z κ1'...κn']»›
          using 0 βden AOT_model_denoting_ex by blast
        hence ‹Abs_rel (λz. Rep_rel Π (z, κ1'κn')) =
               Abs_rel (λz. Rep_rel Π' (z, κ1'κn'))› (is ‹?a = ?b›)
          apply (safe intro!: AOT_sem_proj_id_prop[of v ‹?a› ‹?b›,
                  simplified AOT_sem_eq AOT_sem_conj AOT_sem_forall
                  AOT_sem_denotes, THEN iffD2, THEN conjunct2, THEN conjunct2]
                  Π_proj1_den[OF βden] Π'_proj1_den[OF βden])
          unfolding AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π_denotes]
                    AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π'_denotes]
                    AOT_sem_exe_denoting[simplified AOT_sem_denotes,
                                         OF Π_proj1_den[OF βden]]
                    AOT_sem_exe_denoting[simplified AOT_sem_denotes,
                                         OF Π'_proj1_den[OF βden]]
          by (subst (0 1) Abs_rel_inverse; simp?)
             (metis (no_types, lifting) AOT_model_denotes_rel.abs_eq
                            AOT_model_lambda_denotes AOT_sem_denotes AOT_sem_eq
                            AOT_sem_unary_proj_id Π_proj1_den[OF βden])
        hence ‹Rep_rel Π (x,κ1'κn') = Rep_rel Π' (x,κ1'κn')› for x
          by (simp add: Abs_rel_inject)
             metis
      } note βdenotes = this
      {
        fix α :: 'a and β :: 'b
        assume ‹AOT_model_regular (α, β)›
        moreover {
          assume ‹AOT_model_denotes α ∧ AOT_model_regular β›
          hence ‹Rep_rel Π (α,β) = Rep_rel Π' (α,β)›
            using αdenotes by presburger
        }
        moreover {
          assume ‹¬AOT_model_denotes α ∧ AOT_model_denotes β›
          hence ‹Rep_rel Π (α,β) = Rep_rel Π' (α,β)›
            by (simp add: βdenotes)
        }
        ultimately have ‹Rep_rel Π (α,β) = Rep_rel Π' (α,β)›
          by (metis (no_types, lifting) AOT_model_regular_prod_def case_prodD)
      }
      hence ‹Rep_rel Π = Rep_rel Π'›
        using Π_denotes[unfolded AOT_model_denotes_rel.rep_eq,
                        THEN conjunct2, THEN conjunct2, THEN spec, THEN mp]
        using Π'_denotes[unfolded AOT_model_denotes_rel.rep_eq,
                         THEN conjunct2, THEN conjunct2, THEN spec, THEN mp]
        using AOT_model_irregular_eqI[of ‹Rep_rel Π› ‹Rep_rel Π'› ‹(_,_)›]
        using AOT_model_irregular_nondenoting by fastforce
      hence ‹Π = Π'›
        by (rule Rep_rel_inject[THEN iffD1])
    }
    ultimately have ‹Π = Π' = (∀ κ . AOT_model_denotes κ ⟶
        [v ⊨ «AOT_sem_proj_id κ (λ κ1κn . «[Π]κ1...κn»)
                                (λ κ1κn . «[Π']κ1...κn»)»])›
      by auto
  }
  thus ‹[v ⊨ Π = Π'] = [v ⊨ Π↓ & Π'↓ &
      ∀α («AOT_sem_proj_id α (λ κ1κn . «[Π]κ1...κn») (λ κ1κn . «[Π']κ1...κn»)»)]›
    by (auto simp: AOT_sem_eq AOT_sem_denotes AOT_sem_forall AOT_sem_conj)
next
  fix v and φ :: ‹'a×'b⇒𝗈› and τ :: ‹'a×'b›
  assume ‹[v ⊨ τ↓]›
  moreover assume ‹[v ⊨ [λz1...zn «φ z1zn»] = [λz1...zn «φ z1zn»]]›
  ultimately show ‹[v ⊨ «AOT_sem_proj_id τ φ φ»]›
    unfolding AOT_sem_proj_id_prod_def
    using AOT_sem_proj_id_refl[of v "snd τ" "λb. φ (fst τ, b)"]
    by (auto simp: AOT_sem_eq AOT_sem_conj AOT_sem_denotes
                   AOT_model_denotes_prod_def AOT_model_lambda_denotes
                   AOT_meta_prod_equivI)
qed
end

text‹Sanity-check to verify that n-ary relation identity follows.›
lemma ‹[v ⊨ Π = Π'] = [v ⊨ Π↓ & Π'↓ & ∀x∀y([λz [Π]z y] = [λz [Π']z y] &
                                              [λz [Π]x z] = [λz [Π']x z])]›
  for Π :: ‹<κ×κ>›
  by (auto simp: AOT_sem_proj_id_prop[of v Π Π'] AOT_sem_proj_id_prod_def
                 AOT_sem_conj AOT_sem_denotes AOT_sem_forall AOT_sem_unary_proj_id
                 AOT_model_denotes_prod_def)
lemma ‹[v ⊨ Π = Π'] = [v ⊨ Π↓ & Π'↓ & ∀x1∀x2∀x3 (
  [λz [Π]z x2 x3] = [λz [Π']z x2 x3] &
  [λz [Π]x1 z x3] = [λz [Π']x1 z x3] &
  [λz [Π]x1 x2 z] = [λz [Π']x1 x2 z])]›
  for Π :: ‹<κ×κ×κ>›
  by (auto simp: AOT_sem_proj_id_prop[of v Π Π'] AOT_sem_proj_id_prod_def
                 AOT_sem_conj AOT_sem_denotes AOT_sem_forall AOT_sem_unary_proj_id
                 AOT_model_denotes_prod_def)
lemma ‹[v ⊨ Π = Π'] = [v ⊨ Π↓ & Π'↓ & ∀x1∀x2∀x3∀x4 (
    [λz [Π]z x2 x3 x4] = [λz [Π']z x2 x3 x4] &
    [λz [Π]x1 z x3 x4] = [λz [Π']x1 z x3 x4] &
    [λz [Π]x1 x2 z x4] = [λz [Π']x1 x2 z x4] &
    [λz [Π]x1 x2 x3 z] = [λz [Π']x1 x2 x3 z])]›
  for Π :: ‹<κ×κ×κ×κ>›
  by (auto simp: AOT_sem_proj_id_prop[of v Π Π'] AOT_sem_proj_id_prod_def
                 AOT_sem_conj AOT_sem_denotes AOT_sem_forall AOT_sem_unary_proj_id
                 AOT_model_denotes_prod_def)

text‹n-ary Encoding is constructed using a similar mechanism as n-ary relation
     identity using an auxiliary notion of projection-encoding.›
class AOT_Enc =
  fixes AOT_enc :: ‹'a ⇒ <'a::AOT_IndividualTerm> ⇒ 𝗈›
    and AOT_proj_enc :: ‹'a ⇒ ('a ⇒ 𝗈) ⇒ 𝗈›
  assumes AOT_sem_enc_denotes:
    ‹[v ⊨ «AOT_enc κ1κn Π»] ⟹ [v ⊨ κ1...κn↓] ∧ [v ⊨ Π↓]›
  assumes AOT_sem_enc_proj_enc:
    ‹[v ⊨ «AOT_enc κ1κn Π»] =
     [v ⊨ Π↓ & «AOT_proj_enc κ1κn (λ κ1κn.  «[Π]κ1...κn»)»]›
  assumes AOT_sem_proj_enc_denotes:
    ‹[v ⊨ «AOT_proj_enc κ1κn φ»] ⟹ [v ⊨ κ1...κn↓]›
  assumes AOT_sem_enc_nec:
    ‹[v ⊨ «AOT_enc κ1κn Π»] ⟹ [w ⊨ «AOT_enc κ1κn Π»]›
  assumes AOT_sem_proj_enc_nec:
    ‹[v ⊨ «AOT_proj_enc κ1κn φ»] ⟹ [w ⊨ «AOT_proj_enc κ1κn φ»]›
  assumes AOT_sem_universal_encoder:
    ‹∃ κ1κn. [v ⊨ κ1...κn↓] ∧ (∀ Π . [v ⊨ Π↓] ⟶ [v ⊨ «AOT_enc κ1κn Π»]) ∧
             (∀ φ . [v ⊨ [λz1...zn φ{z1...zn}]↓] ⟶ [v ⊨ «AOT_proj_enc κ1κn φ»])›

AOT_syntax_print_translations
  "_AOT_enc (_AOT_individual_term κ) (_AOT_relation_term Π)" <= "CONST AOT_enc κ Π"

context AOT_meta_syntax
begin
notation AOT_enc ("⦃_,_⦄")
end
context AOT_no_meta_syntax
begin
no_notation AOT_enc ("⦃_,_⦄")
end

text‹Unary encoding additionally has to satisfy the axioms of unary encoding and
     the definition of property identity.›
class AOT_UnaryEnc = AOT_UnaryIndividualTerm +
  assumes AOT_sem_enc_eq: ‹[v ⊨ Π↓ & Π'↓ & □∀ν (ν[Π] ≡ ν[Π']) → Π = Π']›
      and AOT_sem_A_objects: ‹[v ⊨ ∃x (¬◇[E!]x & ∀F (x[F] ≡ φ{F}))]›
      and AOT_sem_unary_proj_enc: ‹AOT_proj_enc x ψ = AOT_enc x «[λz ψ{z}]»›
      and AOT_sem_nocoder: ‹[v ⊨ [E!]κ] ⟹ ¬[w ⊨ «AOT_enc κ Π»]›
      and AOT_sem_ind_eq: ‹([v ⊨ κ↓] ∧ [v ⊨ κ'↓] ∧ κ = (κ')) =
       (([v ⊨ [λx ◇[E!]x]κ] ∧
         [v ⊨ [λx ◇[E!]x]κ'] ∧
         (∀ v Π . [v ⊨ Π↓] ⟶ [v ⊨ [Π]κ] = [v ⊨ [Π]κ']))
        ∨ ([v ⊨ [λx ¬◇[E!]x]κ] ∧
           [v ⊨ [λx ¬◇[E!]x]κ'] ∧
           (∀ v Π . [v ⊨ Π↓] ⟶ [v ⊨ κ[Π]] = [v ⊨ κ'[Π]])))›

      (* only extended models *)
      and AOT_sem_enc_indistinguishable_all:
          ‹AOT_ExtendedModel ⟹
           [v ⊨ [λx ¬◇[E!]x]κ] ⟹
           [v ⊨ [λx ¬◇[E!]x]κ'] ⟹
           (⋀ Π' . [v ⊨ Π'↓] ⟹ (⋀ w . [w ⊨ [Π']κ] = [w ⊨ [Π']κ'])) ⟹
           [v ⊨ Π↓] ⟹
           (⋀ Π' . [v ⊨ Π'↓] ⟹ (⋀ κ0 . [v ⊨ [λx ◇[E!]x]κ0] ⟹
              (⋀ w . [w ⊨ [Π']κ0] = [w ⊨ [Π]κ0])) ⟹ [v ⊨ κ[Π']]) ⟹
           (⋀ Π' . [v ⊨ Π'↓] ⟹ (⋀ κ0 . [v ⊨ [λx ◇[E!]x]κ0] ⟹
              (⋀ w . [w ⊨ [Π']κ0] = [w ⊨ [Π]κ0])) ⟹ [v ⊨ κ'[Π']])›
      and AOT_sem_enc_indistinguishable_ex:
          ‹AOT_ExtendedModel ⟹
           [v ⊨ [λx ¬◇[E!]x]κ] ⟹
           [v ⊨ [λx ¬◇[E!]x]κ'] ⟹
           (⋀ Π' . [v ⊨ Π'↓] ⟹ (⋀ w . [w ⊨ [Π']κ] = [w ⊨ [Π']κ'])) ⟹
           [v ⊨ Π↓] ⟹
           ∃ Π' . [v ⊨ Π'↓] ∧ [v ⊨ κ[Π']] ∧
                  (∀ κ0 . [v ⊨ [λx ◇[E!]x]κ0] ⟶
                          (∀ w . [w ⊨ [Π']κ0] = [w ⊨ [Π]κ0])) ⟹
           ∃ Π' . [v ⊨ Π'↓] ∧ [v ⊨ κ'[Π']] ∧
                  (∀ κ0 . [v ⊨ [λx ◇[E!]x]κ0] ⟶
                          (∀ w . [w ⊨ [Π']κ0] = [w ⊨ [Π]κ0]))›

text‹We specify encoding to align with the model-construction of encoding.›
consts AOT_sem_enc_κ :: ‹κ ⇒ <κ> ⇒ 𝗈›
specification(AOT_sem_enc_κ)
  AOT_sem_enc_κ:
  ‹[v ⊨ «AOT_sem_enc_κ κ Π»] =
   (AOT_model_denotes κ ∧ AOT_model_denotes Π ∧ AOT_model_enc κ Π)›
  by (rule exI[where x=‹λ κ Π . ε𝗈 w . AOT_model_denotes κ ∧ AOT_model_denotes Π ∧
                                       AOT_model_enc κ Π›])
     (simp add: AOT_model_proposition_choice_simp AOT_model_enc_κ_def κ.case_eq_if)

text‹We show that @{typ κ} satisfies the generic properties of n-ary encoding.›
instantiation κ :: AOT_Enc
begin
definition AOT_enc_κ :: ‹κ ⇒ <κ> ⇒ 𝗈› where
  ‹AOT_enc_κ ≡ AOT_sem_enc_κ›
definition AOT_proj_enc_κ :: ‹κ ⇒ (κ ⇒ 𝗈) ⇒ 𝗈› where
  ‹AOT_proj_enc_κ ≡ λ κ φ . AOT_enc κ «[λz «φ z»]»›
lemma AOT_enc_κ_meta:
  ‹[v ⊨ κ[Π]] = (AOT_model_denotes κ ∧ AOT_model_denotes Π ∧ AOT_model_enc κ Π)›
  for κ::κ
  using AOT_sem_enc_κ unfolding AOT_enc_κ_def by auto
instance proof
  fix v and κ :: κ and Π
  show ‹[v ⊨ «AOT_enc κ Π»] ⟹ [v ⊨ κ↓] ∧ [v ⊨ Π↓]›
    unfolding AOT_sem_denotes
    using AOT_enc_κ_meta by blast
next
  fix v and κ :: κ and Π
  show ‹[v ⊨ κ[Π]] = [v ⊨ Π↓ & «AOT_proj_enc κ (λ κ'.  «[Π]κ'»)»]›
  proof
    assume enc: ‹[v ⊨ κ[Π]]›
    hence Π_denotes: ‹AOT_model_denotes Π›
      by (simp add: AOT_enc_κ_meta)
    hence Π_eta_denotes: ‹AOT_model_denotes «[λz [Π]z]»›
      using AOT_sem_denotes AOT_sem_eq AOT_sem_lambda_eta by metis
    show ‹[v ⊨ Π↓ & «AOT_proj_enc κ (λ κ.  «[Π]κ»)»]›
      using AOT_sem_lambda_eta[simplified AOT_sem_denotes AOT_sem_eq, OF Π_denotes]
      using Π_eta_denotes Π_denotes
      by (simp add: AOT_sem_conj AOT_sem_denotes AOT_proj_enc_κ_def enc)
  next
    assume ‹[v ⊨ Π↓ & «AOT_proj_enc κ (λ κ.  «[Π]κ»)»]›
    hence Π_denotes: "AOT_model_denotes Π" and eta_enc: "[v ⊨ κ[λz [Π]z]]" 
      by (auto simp: AOT_sem_conj AOT_sem_denotes AOT_proj_enc_κ_def)
    thus ‹[v ⊨ κ[Π]]›
      using AOT_sem_lambda_eta[simplified AOT_sem_denotes AOT_sem_eq, OF Π_denotes]
      by auto
  qed
next
  show ‹[v ⊨ «AOT_proj_enc κ φ»] ⟹ [v ⊨ κ↓]› for v and κ :: κ and φ
    by (simp add: AOT_enc_κ_meta AOT_sem_denotes AOT_proj_enc_κ_def)
next
  fix v w and κ :: κ and Π
  assume ‹[v ⊨ κ[Π]]›
  thus ‹[w ⊨ κ[Π]]›
    by (simp add: AOT_enc_κ_meta)
next
  fix v w and κ :: κ and φ
  assume ‹[v ⊨ «AOT_proj_enc κ φ»]›
  thus ‹[w ⊨ «AOT_proj_enc κ φ»]›
    by (simp add: AOT_enc_κ_meta AOT_proj_enc_κ_def)
next
  show ‹∃κ::κ. [v ⊨ κ↓] ∧ (∀ Π . [v ⊨ Π↓] ⟶  [v ⊨ κ[Π]]) ∧
               (∀ φ . [v ⊨ [λz φ{z}]↓] ⟶  [v ⊨ «AOT_proj_enc κ φ»])› for v
    by (rule exI[where x=‹ακ UNIV›])
       (simp add: AOT_sem_denotes AOT_enc_κ_meta AOT_model_enc_κ_def
                  AOT_model_denotes_κ_def  AOT_proj_enc_κ_def)
qed
end

text‹We show that @{typ κ} satisfies the properties of unary encoding.›
instantiation κ :: AOT_UnaryEnc
begin
instance proof
  fix v and Π Π' :: ‹<κ>›
  show ‹[v ⊨ Π↓ & Π'↓ & □∀ν (ν[Π] ≡ ν[Π']) → Π = Π']›
    apply (simp add: AOT_sem_forall AOT_sem_eq AOT_sem_imp AOT_sem_equiv
                     AOT_enc_κ_meta AOT_sem_conj AOT_sem_denotes AOT_sem_box)
    using AOT_meta_A_objects_κ by fastforce
next
  fix v and φ:: ‹<κ> ⇒ 𝗈›
  show ‹[v ⊨ ∃x (¬◇[E!]x & ∀F (x[F] ≡ φ{F}))]›
    using AOT_model_A_objects[of "λ Π . [v ⊨ φ{Π}]"]
    by (auto simp: AOT_sem_denotes AOT_sem_exists AOT_sem_conj AOT_sem_not
                   AOT_sem_dia AOT_sem_concrete AOT_enc_κ_meta AOT_sem_equiv
                   AOT_sem_forall)
next
  show ‹AOT_proj_enc x ψ = AOT_enc x (AOT_lambda ψ)› for x :: κ and ψ
    by (simp add: AOT_proj_enc_κ_def)
next
  show ‹[v ⊨ [E!]κ] ⟹ ¬ [w ⊨ κ[Π]]› for v w and κ :: κ and Π
    by (simp add: AOT_enc_κ_meta AOT_sem_concrete AOT_model_nocoder)
next
  fix v and κ κ' :: κ
  show ‹([v ⊨ κ↓] ∧ [v ⊨ κ'↓] ∧ κ = κ') =
         (([v ⊨ [λx ◇[E!]x]κ] ∧
           [v ⊨ [λx ◇[E!]x]κ'] ∧
           (∀ v Π . [v ⊨ Π↓] ⟶ [v ⊨ [Π]κ] = [v ⊨ [Π]κ']))
          ∨ ([v ⊨ [λx ¬◇[E!]x]κ] ∧
             [v ⊨ [λx ¬◇[E!]x]κ'] ∧
             (∀ v Π . [v ⊨ Π↓] ⟶ [v ⊨ κ[Π]] = [v ⊨ κ'[Π]])))›
    (is ‹?lhs = (?ordeq ∨ ?abseq)›)
  proof -
  {
    assume 0: ‹[v ⊨ κ↓] ∧ [v ⊨ κ'↓] ∧ κ = κ'›
    {
      assume ‹is_ωκ κ'›
      hence ‹[v ⊨ [λx ◇[E!]x]κ']›
        apply (subst AOT_sem_lambda_beta[OF AOT_sem_ordinary_def_denotes, of v κ'])
         apply (simp add: "0")
        apply (simp add: AOT_sem_dia)
        using AOT_sem_concrete AOT_model_ω_concrete_in_some_world is_ωκ_def by force
      hence ‹?ordeq› unfolding 0[THEN conjunct2, THEN conjunct2] by auto
    }
    moreover {
      assume ‹is_ακ κ'›
      hence ‹[v ⊨ [λx ¬◇[E!]x]κ']›
        apply (subst AOT_sem_lambda_beta[OF AOT_sem_abstract_def_denotes, of v κ'])
         apply (simp add: "0")
        apply (simp add: AOT_sem_not AOT_sem_dia)
        using AOT_sem_concrete is_ακ_def by force
      hence ‹?abseq› unfolding 0[THEN conjunct2, THEN conjunct2] by auto
    }
    ultimately have ‹?ordeq ∨ ?abseq›
      by (meson "0" AOT_sem_denotes AOT_model_denotes_κ_def κ.exhaust_disc)
  }
  moreover {
    assume ordeq: ‹?ordeq›
    hence κ_denotes: ‹[v ⊨ κ↓]› and κ'_denotes: ‹[v ⊨ κ'↓]› 
      by (simp add: AOT_sem_denotes AOT_sem_exe)+
    hence ‹is_ωκ κ› and ‹is_ωκ κ'›
      by (metis AOT_model_concrete_κ.simps(2) AOT_model_denotes_κ_def
                AOT_sem_concrete AOT_sem_denotes AOT_sem_dia AOT_sem_lambda_beta
                AOT_sem_ordinary_def_denotes κ.collapse(2) κ.exhaust_disc ordeq)+
    have denotes: ‹[v ⊨ [λz «ε𝗈 w . κυ z = κυ κ»]↓]›
      unfolding AOT_sem_denotes AOT_model_lambda_denotes
      by (simp add: AOT_model_term_equiv_κ_def)
    hence "[v ⊨ [λz «ε𝗈 w . κυ z = κυ κ»]κ] = [v ⊨ [λz «ε𝗈 w . κυ z = κυ κ»]κ']"
      using ordeq by (simp add: AOT_sem_denotes)
    hence ‹[v ⊨ «κ»↓] ∧ [v ⊨ «κ'»↓] ∧ κ = κ'›
      unfolding AOT_sem_lambda_beta[OF denotes, OF κ_denotes]
                AOT_sem_lambda_beta[OF denotes, OF κ'_denotes]
      using κ'_denotes ‹is_ωκ κ'› ‹is_ωκ κ› is_ωκ_def
            AOT_model_proposition_choice_simp by force
  }
  moreover {
    assume 0: ‹?abseq›
    hence κ_denotes: ‹[v ⊨ κ↓]› and κ'_denotes: ‹[v ⊨ κ'↓]› 
      by (simp add: AOT_sem_denotes AOT_sem_exe)+
    hence ‹¬is_ωκ κ› and ‹¬is_ωκ κ'›
      by (metis AOT_model_ω_concrete_in_some_world AOT_model_concrete_κ.simps(1)
                AOT_sem_concrete AOT_sem_dia AOT_sem_exe AOT_sem_lambda_beta
                AOT_sem_not κ.collapse(1) 0)+
    hence ‹is_ακ κ› and ‹is_ακ κ'›
      by (meson AOT_sem_denotes AOT_model_denotes_κ_def κ.exhaust_disc
                κ_denotes κ'_denotes)+
    then obtain x y where κ_def: ‹κ = ακ x› and κ'_def: ‹κ' = ακ y›
      using is_ακ_def by auto
    {
      fix r
      assume ‹r ∈ x›
      hence ‹[v ⊨ κ[«urrel_to_rel r»]]›
        unfolding κ_def
        unfolding AOT_enc_κ_meta
        unfolding AOT_model_enc_κ_def
        apply (simp add: AOT_model_denotes_κ_def)
        by (metis (mono_tags) AOT_rel_equiv_def Quotient_def urrel_quotient)
      hence ‹[v ⊨ κ'[«urrel_to_rel r»]]›
        using AOT_enc_κ_meta 0 by (metis AOT_sem_enc_denotes)
      hence ‹r ∈ y›
        unfolding κ'_def
        unfolding AOT_enc_κ_meta
        unfolding AOT_model_enc_κ_def
        apply (simp add: AOT_model_denotes_κ_def)
        using Quotient_abs_rep urrel_quotient by fastforce
    }
    moreover {
      fix r
      assume ‹r ∈ y›
      hence ‹[v ⊨ κ'[«urrel_to_rel r»]]›
        unfolding κ'_def
        unfolding AOT_enc_κ_meta
        unfolding AOT_model_enc_κ_def
        apply (simp add: AOT_model_denotes_κ_def)
        by (metis (mono_tags) AOT_rel_equiv_def Quotient_def urrel_quotient)
      hence ‹[v ⊨ κ[«urrel_to_rel r»]]›
        using AOT_enc_κ_meta 0 by (metis AOT_sem_enc_denotes)
      hence ‹r ∈ x›
        unfolding κ_def
        unfolding AOT_enc_κ_meta
        unfolding AOT_model_enc_κ_def
        apply (simp add: AOT_model_denotes_κ_def)
        using Quotient_abs_rep urrel_quotient by fastforce
    }
    ultimately have "x = y" by blast
    hence ‹[v ⊨ κ↓] ∧ [v ⊨ κ'↓] ∧ κ = κ'›
      using κ'_def κ'_denotes κ_def by blast
  }
  ultimately show ?thesis
    unfolding AOT_sem_denotes
    by auto
  qed
(* Only extended model *)
next
  fix v and κ κ' :: κ and Π Π' :: ‹<κ>›
  assume ext: ‹AOT_ExtendedModel›
  assume ‹[v ⊨ [λx ¬◇[E!]x]κ]›
  hence ‹is_ακ κ›
    by (metis AOT_model_ω_concrete_in_some_world AOT_model_concrete_κ.simps(1)
              AOT_model_denotes_κ_def AOT_sem_concrete AOT_sem_denotes AOT_sem_dia
              AOT_sem_exe AOT_sem_lambda_beta AOT_sem_not κ.collapse(1) κ.exhaust_disc)
  hence κ_abs: ‹¬(∃ w . AOT_model_concrete w κ)›
    using is_ακ_def by fastforce
  have κ_den: ‹AOT_model_denotes κ›
    by (simp add: AOT_model_denotes_κ_def κ.distinct_disc(5) ‹is_ακ κ›)
  assume ‹[v ⊨ [λx ¬◇[E!]x]κ']›
  hence ‹is_ακ κ'›
    by (metis AOT_model_ω_concrete_in_some_world AOT_model_concrete_κ.simps(1)
              AOT_model_denotes_κ_def AOT_sem_concrete AOT_sem_denotes AOT_sem_dia
              AOT_sem_exe AOT_sem_lambda_beta AOT_sem_not κ.collapse(1)
              κ.exhaust_disc)
  hence κ'_abs: ‹¬(∃ w . AOT_model_concrete w κ')›
    using is_ακ_def by fastforce
  have κ'_den: ‹AOT_model_denotes κ'›
    by (meson AOT_model_denotes_κ_def κ.distinct_disc(6) ‹is_ακ κ'›)
  assume ‹[v ⊨ Π'↓] ⟹ [w ⊨ [Π']κ] = [w ⊨ [Π']κ']› for Π' w
  hence indist: ‹[v ⊨ «Rep_rel Π' κ»] = [v ⊨ «Rep_rel Π' κ'»]›
    if ‹AOT_model_denotes Π'› for Π' v
    by (metis AOT_sem_denotes AOT_sem_exe κ'_den κ_den that)
  assume κ_enc_cond: ‹[v ⊨ Π'↓] ⟹
    (⋀ κ0 w. [v ⊨ [λx ◇[E!]x]κ0] ⟹
             [w ⊨ [Π']κ0] = [w ⊨ [Π]κ0]) ⟹
    [v ⊨ κ[Π']]› for Π'
  assume Π_den': ‹[v ⊨ Π↓]›
  hence Π_den: ‹AOT_model_denotes Π›
    using AOT_sem_denotes by blast
  {
    fix Π' :: ‹<κ>›
    assume Π'_den: ‹AOT_model_denotes Π'›
    hence Π'_den': ‹[v ⊨ Π'↓]›
      by (simp add: AOT_sem_denotes)
    assume 1: ‹∃w. AOT_model_concrete w x ⟹
               [v ⊨ «Rep_rel Π' x»] = [v ⊨ «Rep_rel Π x»]› for v x
    {
      fix κ0 :: κ and w
      assume ‹[v ⊨ [λx ◇[E!]x]κ0]›
      hence ‹is_ωκ κ0›
        by (smt (z3) AOT_model_concrete_κ.simps(2) AOT_model_denotes_κ_def
                     AOT_sem_concrete AOT_sem_denotes AOT_sem_dia AOT_sem_exe
                     AOT_sem_lambda_beta κ.exhaust_disc is_ακ_def)
      then obtain x where x_prop: ‹κ0 = ωκ x›
        using is_ωκ_def by blast
      have ‹∃w . AOT_model_concrete w (ωκ x)›
        by (simp add: AOT_model_ω_concrete_in_some_world)
      hence ‹[v ⊨ «Rep_rel Π' (ωκ x)»] = [v ⊨ «Rep_rel Π (ωκ x)»]› for v
        using 1 by blast
      hence ‹[w ⊨ [Π']κ0] = [w ⊨ [Π]κ0]› unfolding x_prop
        by (simp add: AOT_sem_exe AOT_sem_denotes AOT_model_denotes_κ_def
                      Π'_den Π_den)
    } note 2 = this
    have ‹[v ⊨ κ[Π']]›
      using κ_enc_cond[OF Π'_den', OF 2]
      by metis
    hence ‹AOT_model_enc κ Π'›
      using AOT_enc_κ_meta by blast
  } note κ_enc_cond = this
  hence ‹AOT_model_denotes Π' ⟹
       (⋀v x. ∃w. AOT_model_concrete w x ⟹
              [v ⊨ «Rep_rel Π' x»] = [v ⊨ «Rep_rel Π x»]) ⟹
       AOT_model_enc κ Π'› for Π'
    by blast
  assume Π'_den': ‹[v ⊨ Π'↓]›
  hence Π'_den: ‹AOT_model_denotes Π'›
    using AOT_sem_denotes by blast
  assume ord_indist: ‹[v ⊨ [λx ◇[E!]x]κ0] ⟹
                      [w ⊨ [Π']κ0] = [w ⊨ [Π]κ0]› for κ0 w
  {
    fix w and κ0 :: κ
    assume 0: ‹∃w. AOT_model_concrete w κ0›
    hence ‹[v ⊨ [λx ◇[E!]x]κ0]›
      using AOT_model_concrete_denotes AOT_sem_concrete AOT_sem_denotes AOT_sem_dia
            AOT_sem_lambda_beta AOT_sem_ordinary_def_denotes by blast
    hence ‹[w ⊨ [Π']κ0] = [w ⊨ [Π]κ0]›
      using ord_indist by metis 
    hence ‹[w ⊨ «Rep_rel Π' κ0»] = [w ⊨ «Rep_rel Π κ0»]›
      by (metis AOT_model_concrete_denotes AOT_sem_denotes AOT_sem_exe Π'_den Π_den 0)
  } note ord_indist = this
  have ‹AOT_model_enc κ' Π'›
    using AOT_model_enc_indistinguishable_all
            [OF ext, OF κ_den, OF κ_abs, OF κ'_den, OF κ'_abs, OF Π_den]
          indist κ_enc_cond Π'_den ord_indist by blast
  thus ‹[v ⊨ κ'[Π']]›
    using AOT_enc_κ_meta Π'_den κ'_den by blast
next
  fix v and κ κ' :: κ and Π Π' :: ‹<κ>›
  assume ext: ‹AOT_ExtendedModel›
  assume ‹[v ⊨ [λx ¬◇[E!]x]κ]›
  hence ‹is_ακ κ›
    by (metis AOT_model_ω_concrete_in_some_world AOT_model_concrete_κ.simps(1)
              AOT_model_denotes_κ_def AOT_sem_concrete AOT_sem_denotes AOT_sem_dia
              AOT_sem_exe AOT_sem_lambda_beta AOT_sem_not κ.collapse(1)
              κ.exhaust_disc)
  hence κ_abs: ‹¬(∃ w . AOT_model_concrete w κ)›
    using is_ακ_def by fastforce
  have κ_den: ‹AOT_model_denotes κ›
    by (simp add: AOT_model_denotes_κ_def κ.distinct_disc(5) ‹is_ακ κ›)
  assume ‹[v ⊨ [λx ¬◇[E!]x]κ']›
  hence ‹is_ακ κ'›
    by (metis AOT_model_ω_concrete_in_some_world AOT_model_concrete_κ.simps(1)
              AOT_model_denotes_κ_def AOT_sem_concrete AOT_sem_denotes AOT_sem_dia
              AOT_sem_exe AOT_sem_lambda_beta AOT_sem_not κ.collapse(1)
              κ.exhaust_disc)
  hence κ'_abs: ‹¬(∃ w . AOT_model_concrete w κ')›
    using is_ακ_def by fastforce
  have κ'_den: ‹AOT_model_denotes κ'›
    by (meson AOT_model_denotes_κ_def κ.distinct_disc(6) ‹is_ακ κ'›)
  assume ‹[v ⊨ Π'↓] ⟹ [w ⊨ [Π']κ] = [w ⊨ [Π']κ']› for Π' w
  hence indist: ‹[v ⊨ «Rep_rel Π' κ»] = [v ⊨ «Rep_rel Π' κ'»]›
    if ‹AOT_model_denotes Π'› for Π' v
    by (metis AOT_sem_denotes AOT_sem_exe κ'_den κ_den that)
  assume Π_den': ‹[v ⊨ Π↓]›
  hence Π_den: ‹AOT_model_denotes Π›
    using AOT_sem_denotes by blast
  assume ‹∃Π'. [v ⊨ Π'↓] ∧ [v ⊨ κ[Π']] ∧
               (∀κ0. [v ⊨ [λx ◇[E!]x]κ0] ⟶
                     (∀w. [w ⊨ [Π']κ0] = [w ⊨ [Π]κ0]))›
  then obtain Π' where
      Π'_den: ‹[v ⊨ Π'↓]› and
      Π'_enc: ‹[v ⊨ κ[Π']]› and
      Π'_prop: ‹∀κ0. [v ⊨ [λx ◇[E!]x]κ0] ⟶
                     (∀w. [w ⊨ [Π']κ0] = [w ⊨ [Π]κ0])›
    by blast
  have ‹AOT_model_denotes Π'›
    using AOT_enc_κ_meta Π'_enc by force
  moreover have ‹AOT_model_enc κ Π'›
    using AOT_enc_κ_meta Π'_enc by blast
  moreover have ‹(∃w. AOT_model_concrete w κ0) ⟹
                 [v ⊨ «Rep_rel Π' κ0»] = [v ⊨ «Rep_rel Π κ0»]› for κ0 v
  proof -
    assume 0: ‹∃w. AOT_model_concrete w κ0›
    hence ‹[v ⊨ [λx ◇[E!]x]κ0]› for v
      using AOT_model_concrete_denotes AOT_sem_concrete AOT_sem_denotes AOT_sem_dia
            AOT_sem_lambda_beta AOT_sem_ordinary_def_denotes by blast
    hence ‹∀w. [w ⊨ [Π']κ0] = [w ⊨ [Π]κ0]› using Π'_prop by blast
    thus ‹[v ⊨ «Rep_rel Π' κ0»] = [v ⊨ «Rep_rel Π κ0»]›
      by (meson "0" AOT_model_concrete_denotes AOT_sem_denotes AOT_sem_exe Π_den
                calculation(1))
  qed
  ultimately have ‹∃Π'. AOT_model_denotes Π' ∧ AOT_model_enc κ Π' ∧
                        (∀v x. (∃w. AOT_model_concrete w x) ⟶
                         [v ⊨ «Rep_rel Π' x»] = [v ⊨ «Rep_rel Π x»])›
    by blast
  hence ‹∃Π'. AOT_model_denotes Π' ∧ AOT_model_enc κ' Π' ∧
              (∀v x. (∃w. AOT_model_concrete w x) ⟶
               [v ⊨ «Rep_rel Π' x»] = [v ⊨ «Rep_rel Π x»])›
    using AOT_model_enc_indistinguishable_ex
            [OF ext, OF κ_den, OF κ_abs, OF κ'_den, OF κ'_abs, OF Π_den]
          indist by blast
  then obtain Π'' where
      Π''_den: ‹AOT_model_denotes Π''›
      and Π''_enc: ‹AOT_model_enc κ' Π''›
      and Π''_prop: ‹(∃w. AOT_model_concrete w x) ⟹
                      [v ⊨ «Rep_rel Π'' x»] = [v ⊨ «Rep_rel Π x»]› for v x
    by blast
  have ‹[v ⊨ Π''↓]›
    by (simp add: AOT_sem_denotes Π''_den)
  moreover have ‹[v ⊨ κ'[Π'']]›
    by (simp add: AOT_enc_κ_meta Π''_den Π''_enc κ'_den)
  moreover have ‹[v ⊨ [λx ◇[E!]x]κ0] ⟹
                 (∀w. [w ⊨ [Π'']κ0] = [w ⊨ [Π]κ0])› for κ0
  proof -
    assume ‹[v ⊨ [λx ◇[E!]x]κ0]›
    hence ‹∃w. AOT_model_concrete w κ0›
      by (metis AOT_sem_concrete AOT_sem_dia AOT_sem_exe AOT_sem_lambda_beta)
    thus ‹∀w. [w ⊨ [Π'']κ0] = [w ⊨ [Π]κ0]›
      using Π''_prop
      by (metis AOT_sem_denotes AOT_sem_exe Π''_den Π_den)
  qed
  ultimately show ‹∃Π'. [v ⊨ Π'↓] ∧ [v ⊨ κ'[Π']] ∧
                         (∀κ0. [v ⊨ [λx ◇[E!]x]κ0] ⟶
                               (∀w. [w ⊨ [Π']κ0] = [w ⊨ [Π]κ0]))›
    by (safe intro!: exI[where x=Π'']) blast+
qed
end

text‹Define encoding for products using projection-encoding.›
instantiation prod :: (AOT_UnaryEnc, AOT_Enc) AOT_Enc
begin
definition AOT_proj_enc_prod :: ‹'a×'b ⇒ ('a×'b ⇒ 𝗈) ⇒ 𝗈› where
  ‹AOT_proj_enc_prod ≡ λ (κ,κ') φ . «κ[λν «φ (ν,κ')»] &
                                     «AOT_proj_enc κ' (λν. φ (κ,ν))»»›
definition AOT_enc_prod :: ‹'a×'b ⇒ <'a×'b> ⇒ 𝗈› where
  ‹AOT_enc_prod ≡ λ κ Π . «Π↓ & «AOT_proj_enc κ (λ κ1'κn'.  «[Π]κ1'...κn'»)»»›
instance proof
  show ‹[v ⊨ κ1...κn[Π]] ⟹ [v ⊨ κ1...κn↓] ∧ [v ⊨ Π↓]›
    for v and κ1κn :: ‹'a×'b› and Π
    unfolding AOT_enc_prod_def
    apply (induct κ1κn; simp add: AOT_sem_conj AOT_sem_denotes AOT_proj_enc_prod_def)
    by (metis AOT_sem_denotes AOT_model_denotes_prod_def AOT_sem_enc_denotes
              AOT_sem_proj_enc_denotes case_prodI)
next
  show ‹[v ⊨ κ1...κn[Π]] =
        [v ⊨ «Π»↓ & «AOT_proj_enc κ1κn (λ κ1κn.  «[Π]κ1...κn»)»]›
    for v and κ1κn :: ‹'a×'b› and Π
    unfolding AOT_enc_prod_def ..
next
  show ‹[v ⊨ «AOT_proj_enc κs φ»] ⟹ [v ⊨ «κs»↓]›
    for v and κs :: ‹'a×'b› and φ
    by (metis (mono_tags, lifting)
          AOT_sem_conj AOT_sem_denotes AOT_model_denotes_prod_def
          AOT_sem_enc_denotes AOT_sem_proj_enc_denotes
          AOT_proj_enc_prod_def case_prod_unfold)
next
  fix v w Π and κ1κn :: ‹'a×'b›
  show ‹[w ⊨ κ1...κn[Π]]› if ‹[v ⊨ κ1...κn[Π]]› for v w Π and κ1κn :: ‹'a×'b›
    by (metis (mono_tags, lifting)
          AOT_enc_prod_def AOT_sem_enc_proj_enc AOT_sem_conj AOT_sem_denotes
          AOT_sem_proj_enc_nec AOT_proj_enc_prod_def case_prod_unfold that)
next
  show ‹[w ⊨ «AOT_proj_enc κ1κn φ»]› if ‹[v ⊨ «AOT_proj_enc κ1κn φ»]›
    for v w φ and κ1κn :: ‹'a×'b›
    by (metis (mono_tags, lifting)
          that AOT_sem_enc_proj_enc AOT_sem_conj AOT_sem_denotes
          AOT_sem_proj_enc_nec AOT_proj_enc_prod_def case_prod_unfold)
next
  fix v
  obtain κ :: 'a where a_prop: ‹[v ⊨ κ↓] ∧ (∀ Π . [v ⊨ Π↓] ⟶  [v ⊨ κ[Π]])›
    using AOT_sem_universal_encoder by blast
  obtain κ1'κn' :: 'b where b_prop:
    ‹[v ⊨ κ1'...κn'↓] ∧ (∀ φ . [v ⊨ [λν1...νn «φ ν1νn»]↓] ⟶
                                [v ⊨ «AOT_proj_enc κ1'κn' φ»])›
    using AOT_sem_universal_encoder by blast
  have ‹AOT_model_denotes «[λν1...νn [«Π»]ν1...νn κ1'...κn']»›
    if ‹AOT_model_denotes Π› for Π :: ‹<'a×'b>›
    unfolding AOT_model_lambda_denotes
    by (metis AOT_meta_prod_equivI(2) AOT_sem_exe_equiv)
  moreover have ‹AOT_model_denotes  «[λν1...νn [«Π»]κ ν1...νn]»›
    if ‹AOT_model_denotes Π› for Π :: ‹<'a×'b>›
    unfolding AOT_model_lambda_denotes
    by (metis AOT_meta_prod_equivI(1) AOT_sem_exe_equiv)
  ultimately have 1: ‹[v ⊨ «(κ,κ1'κn')»↓]›
              and 2: ‹(∀ Π . [v ⊨ Π↓] ⟶  [v ⊨ κ κ1'...κn'[Π]])›
    using a_prop b_prop
    by (auto simp: AOT_sem_denotes AOT_enc_κ_meta AOT_model_enc_κ_def
                   AOT_model_denotes_κ_def AOT_model_denotes_prod_def
                   AOT_enc_prod_def AOT_proj_enc_prod_def AOT_sem_conj)
  have ‹AOT_model_denotes «[λz1...zn «φ (z1zn, κ1'κn')»]»›
    if ‹AOT_model_denotes «[λz1...zm φ{z1...zm}]»› for φ :: ‹'a×'b ⇒ 𝗈›
    using that
    unfolding AOT_model_lambda_denotes
    by (metis (no_types, lifting) AOT_sem_denotes AOT_model_denotes_prod_def
                                  AOT_meta_prod_equivI(2) b_prop case_prodI)
  moreover have ‹AOT_model_denotes «[λz1...zn «φ (κ, z1zn)»]»›
    if ‹AOT_model_denotes «[λz1...zm φ{z1...zm}]»› for φ :: ‹'a×'b ⇒ 𝗈›
    using that
    unfolding AOT_model_lambda_denotes
    by (metis (no_types, lifting) AOT_sem_denotes AOT_model_denotes_prod_def
                                  AOT_meta_prod_equivI(1) a_prop case_prodI)
  ultimately have 3:
    ‹[v ⊨ «(κ,κ1'κn')»↓] ∧ (∀ φ . [v ⊨ [λz1...zn φ{z1...zn}]↓] ⟶
                                   [v ⊨ «AOT_proj_enc (κ,κ1'κn') φ»])›
    using a_prop b_prop
    by (auto simp: AOT_sem_denotes AOT_enc_κ_meta AOT_model_enc_κ_def
                   AOT_model_denotes_κ_def AOT_enc_prod_def AOT_proj_enc_prod_def
                   AOT_sem_conj AOT_model_denotes_prod_def)
  show ‹∃κ1κn::'a×'b. [v ⊨ κ1...κn↓] ∧ (∀ Π . [v ⊨ Π↓] ⟶ [v ⊨ κ1...κn[Π]]) ∧
                      (∀ φ . [v ⊨ [λz1...zn «φ z1zn»]↓] ⟶
                             [v ⊨ «AOT_proj_enc κ1κn φ»])›
    apply (rule exI[where x=‹(κ,κ1'κn')›]) using 1 2 3 by blast
qed
end

text‹Sanity-check to verify that n-ary encoding follows.›
lemma ‹[v ⊨ κ1κ2[Π]] = [v ⊨ Π↓ & κ1[λν [Π]νκ2] & κ2[λν [Π]κ1ν]]›
  for κ1 :: "'a::AOT_UnaryEnc" and κ2 :: "'b::AOT_UnaryEnc"
  by (simp add: AOT_sem_conj AOT_enc_prod_def AOT_proj_enc_prod_def
                AOT_sem_unary_proj_enc)
lemma ‹[v ⊨ κ1κ2κ3[Π]] =
       [v ⊨ Π↓ & κ1[λν [Π]νκ2κ3] & κ2[λν [Π]κ1νκ3] & κ3[λν [Π]κ1κ2ν]]›
  for κ1 κ2 κ3 :: "'a::AOT_UnaryEnc"
  by (simp add: AOT_sem_conj AOT_enc_prod_def AOT_proj_enc_prod_def
                AOT_sem_unary_proj_enc)

lemma AOT_sem_vars_denote: ‹[v ⊨ α1...αn↓]›
  by induct simp

text‹Combine the introduced type classes and register them as
     type constraints for individual terms.›
class AOT_κs = AOT_IndividualTerm + AOT_RelationProjection + AOT_Enc
class AOT_κ = AOT_κs + AOT_UnaryIndividualTerm +
  AOT_UnaryRelationProjection + AOT_UnaryEnc

instance κ :: AOT_κ by standard
instance prod :: (AOT_κ, AOT_κs) AOT_κs by standard

AOT_register_type_constraints
  Individual: ‹_::AOT_κ› ‹_::AOT_κs› and
  Relation: ‹<_::AOT_κs>›

text‹We define semantic predicates to capture the conditions of cqt.2 (i.e.
     the base cases of denoting terms) on matrices of @{text λ}-expressions.›
definition AOT_instance_of_cqt_2 :: ‹('a::AOT_κs ⇒ 𝗈) ⇒ bool› where
  ‹AOT_instance_of_cqt_2 ≡ λ φ . ∀ x y . AOT_model_denotes x ∧ AOT_model_denotes y ∧
                                          AOT_model_term_equiv x y ⟶ φ x = φ y›
definition AOT_instance_of_cqt_2_exe_arg :: ‹('a::AOT_κs ⇒ 'b::AOT_κs) ⇒ bool› where
  ‹AOT_instance_of_cqt_2_exe_arg ≡ λ φ . ∀ x y .
      AOT_model_denotes x ∧ AOT_model_denotes y ∧ AOT_model_term_equiv x y ⟶
      AOT_model_term_equiv (φ x) (φ y)›

text‹@{text λ}-expressions with a matrix that satisfies our predicate denote.›
lemma AOT_sem_cqt_2:
  assumes ‹AOT_instance_of_cqt_2 φ›
  shows ‹[v ⊨ [λν1...νn φ{ν1...νn}]↓]›
  using assms
  by (metis AOT_instance_of_cqt_2_def AOT_model_lambda_denotes AOT_sem_denotes)

syntax AOT_instance_of_cqt_2 :: ‹id_position ⇒ AOT_prop›
  ("INSTANCE'_OF'_CQT'_2'(_')")

text‹Prove introduction rules for the predicates that match the natural language
     restrictions of the axiom.›
named_theorems AOT_instance_of_cqt_2_intro
lemma AOT_instance_of_cqt_2_intros_const[AOT_instance_of_cqt_2_intro]:
  ‹AOT_instance_of_cqt_2 (λα. φ)›
  by (simp add: AOT_instance_of_cqt_2_def AOT_sem_denotes AOT_model_lambda_denotes)
lemma AOT_instance_of_cqt_2_intros_not[AOT_instance_of_cqt_2_intro]:
  assumes ‹AOT_instance_of_cqt_2 φ›
  shows ‹AOT_instance_of_cqt_2 (λτ. «¬φ{τ}»)›
  using assms
  by (metis (no_types, lifting) AOT_instance_of_cqt_2_def)
lemma AOT_instance_of_cqt_2_intros_imp[AOT_instance_of_cqt_2_intro]:
  assumes ‹AOT_instance_of_cqt_2 φ› and ‹AOT_instance_of_cqt_2 ψ›
  shows ‹AOT_instance_of_cqt_2 (λτ. «φ{τ} → ψ{τ}»)›
  using assms
  by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes
                 AOT_model_lambda_denotes AOT_sem_imp)
lemma AOT_instance_of_cqt_2_intros_box[AOT_instance_of_cqt_2_intro]:
  assumes ‹AOT_instance_of_cqt_2 φ›
  shows ‹AOT_instance_of_cqt_2 (λτ. «□φ{τ}»)›
  using assms
  by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes
                 AOT_model_lambda_denotes AOT_sem_box)
lemma AOT_instance_of_cqt_2_intros_act[AOT_instance_of_cqt_2_intro]:
  assumes ‹AOT_instance_of_cqt_2 φ›
  shows ‹AOT_instance_of_cqt_2 (λτ. «𝒜φ{τ}»)›
  using assms
  by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes
                 AOT_model_lambda_denotes AOT_sem_act)
lemma AOT_instance_of_cqt_2_intros_diamond[AOT_instance_of_cqt_2_intro]:
  assumes ‹AOT_instance_of_cqt_2 φ›
  shows ‹AOT_instance_of_cqt_2 (λτ. «◇φ{τ}»)›
  using assms
  by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes
                 AOT_model_lambda_denotes AOT_sem_dia)
lemma AOT_instance_of_cqt_2_intros_conj[AOT_instance_of_cqt_2_intro]:
  assumes ‹AOT_instance_of_cqt_2 φ› and ‹AOT_instance_of_cqt_2 ψ›
  shows ‹AOT_instance_of_cqt_2 (λτ. «φ{τ} & ψ{τ}»)›
  using assms
  by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes
                 AOT_model_lambda_denotes AOT_sem_conj)
lemma AOT_instance_of_cqt_2_intros_disj[AOT_instance_of_cqt_2_intro]:
  assumes ‹AOT_instance_of_cqt_2 φ› and ‹AOT_instance_of_cqt_2 ψ›
  shows ‹AOT_instance_of_cqt_2 (λτ. «φ{τ} ∨ ψ{τ}»)›
  using assms
  by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes
                 AOT_model_lambda_denotes AOT_sem_disj)
lemma AOT_instance_of_cqt_2_intros_equib[AOT_instance_of_cqt_2_intro]:
  assumes ‹AOT_instance_of_cqt_2 φ› and ‹AOT_instance_of_cqt_2 ψ›
  shows ‹AOT_instance_of_cqt_2 (λτ. «φ{τ} ≡ ψ{τ}»)›
  using assms
  by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes
                 AOT_model_lambda_denotes AOT_sem_equiv)
lemma AOT_instance_of_cqt_2_intros_forall[AOT_instance_of_cqt_2_intro]:
  assumes ‹⋀ α . AOT_instance_of_cqt_2 (Φ α)›
  shows ‹AOT_instance_of_cqt_2 (λτ. «∀α Φ{α,τ}»)›
  using assms
  by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes
                 AOT_model_lambda_denotes AOT_sem_forall)
lemma AOT_instance_of_cqt_2_intros_exists[AOT_instance_of_cqt_2_intro]:
  assumes ‹⋀ α . AOT_instance_of_cqt_2 (Φ α)›
  shows ‹AOT_instance_of_cqt_2 (λτ. «∃α Φ{α,τ}»)›
  using assms
  by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes
                 AOT_model_lambda_denotes AOT_sem_exists)
lemma AOT_instance_of_cqt_2_intros_exe_arg_self[AOT_instance_of_cqt_2_intro]:
   ‹AOT_instance_of_cqt_2_exe_arg (λx. x)›
  unfolding AOT_instance_of_cqt_2_exe_arg_def AOT_instance_of_cqt_2_def
            AOT_sem_lambda_denotes
  by (auto simp: AOT_model_term_equiv_part_equivp equivp_reflp AOT_sem_denotes)
lemma AOT_instance_of_cqt_2_intros_exe_arg_const[AOT_instance_of_cqt_2_intro]:
     ‹AOT_instance_of_cqt_2_exe_arg (λx. κ)›
  unfolding AOT_instance_of_cqt_2_exe_arg_def AOT_instance_of_cqt_2_def
  by (auto simp: AOT_model_term_equiv_part_equivp equivp_reflp
                 AOT_sem_denotes AOT_sem_lambda_denotes)
lemma AOT_instance_of_cqt_2_intros_exe_arg_fst[AOT_instance_of_cqt_2_intro]:
   ‹AOT_instance_of_cqt_2_exe_arg fst›
  unfolding AOT_instance_of_cqt_2_exe_arg_def AOT_instance_of_cqt_2_def
  by (simp add: AOT_model_term_equiv_prod_def case_prod_beta)
lemma AOT_instance_of_cqt_2_intros_exe_arg_snd[AOT_instance_of_cqt_2_intro]:
   ‹AOT_instance_of_cqt_2_exe_arg snd›
  unfolding AOT_instance_of_cqt_2_exe_arg_def AOT_instance_of_cqt_2_def
  by (simp add: AOT_model_term_equiv_prod_def AOT_sem_denotes AOT_sem_lambda_denotes)
lemma AOT_instance_of_cqt_2_intros_exe_arg_Pair[AOT_instance_of_cqt_2_intro]:
  assumes ‹AOT_instance_of_cqt_2_exe_arg φ› and ‹AOT_instance_of_cqt_2_exe_arg ψ›
  shows ‹AOT_instance_of_cqt_2_exe_arg (λτ. Pair (φ τ) (ψ τ))›
  using assms
  unfolding AOT_instance_of_cqt_2_exe_arg_def AOT_instance_of_cqt_2_def
            AOT_sem_denotes AOT_sem_lambda_denotes AOT_model_term_equiv_prod_def
            AOT_model_denotes_prod_def
  by auto
lemma AOT_instance_of_cqt_2_intros_desc[AOT_instance_of_cqt_2_intro]:
  assumes ‹⋀z :: 'a::AOT_κ. AOT_instance_of_cqt_2 (Φ z)›
  shows ‹AOT_instance_of_cqt_2_exe_arg (λ κ :: 'b::AOT_κ . «ιz(Φ{z,κ})»)›
proof -
  have 0: ‹⋀ κ κ'. AOT_model_denotes κ ∧ AOT_model_denotes κ' ∧
                   AOT_model_term_equiv κ κ' ⟹
                   Φ z κ = Φ z κ'› for z
    using assms
    unfolding AOT_instance_of_cqt_2_def
              AOT_sem_denotes AOT_model_lambda_denotes by force
  {
    fix κ κ'
    have ‹«ιz(Φ{z,κ})» = «ιz(Φ{z,κ'})»›
      if ‹AOT_model_denotes κ ∧ AOT_model_denotes κ' ∧ AOT_model_term_equiv κ κ'›
      using 0[OF that]
      by auto
    moreover have ‹AOT_model_term_equiv x x› for x :: ‹'a::AOT_κ›
      by (metis AOT_instance_of_cqt_2_exe_arg_def
                AOT_instance_of_cqt_2_intros_exe_arg_const
                AOT_model_A_objects AOT_model_term_equiv_denotes
                AOT_model_term_equiv_eps(1))
    ultimately have ‹AOT_model_term_equiv «ιz(Φ{z,κ})» «ιz(Φ{z,κ'})»›
      if ‹AOT_model_denotes κ ∧ AOT_model_denotes κ' ∧ AOT_model_term_equiv κ κ'›
      using that by simp
  }
  thus ?thesis using 0
    unfolding AOT_instance_of_cqt_2_exe_arg_def
    by simp
qed

lemma AOT_instance_of_cqt_2_intros_exe_const[AOT_instance_of_cqt_2_intro]:
  assumes ‹AOT_instance_of_cqt_2_exe_arg κs›
  shows ‹AOT_instance_of_cqt_2 (λx :: 'b::AOT_κs. AOT_exe Π (κs x))›
  using assms
  unfolding AOT_instance_of_cqt_2_def AOT_sem_denotes AOT_model_lambda_denotes
            AOT_sem_disj AOT_sem_conj
            AOT_sem_not AOT_sem_box AOT_sem_act AOT_instance_of_cqt_2_exe_arg_def
            AOT_sem_equiv AOT_sem_imp AOT_sem_forall AOT_sem_exists AOT_sem_dia
  by (auto intro!: AOT_sem_exe_equiv)
lemma AOT_instance_of_cqt_2_intros_exe_lam[AOT_instance_of_cqt_2_intro]:
  assumes ‹⋀ y . AOT_instance_of_cqt_2 (λx. φ x y)›
      and ‹AOT_instance_of_cqt_2_exe_arg κs›
    shows ‹AOT_instance_of_cqt_2 (λκ1κn :: 'b::AOT_κs.
              «[λν1...νn φ{κ1...κn,ν1...νn}]«κs κ1κn»»)›
proof -
  {
    fix x y :: 'b
    assume ‹AOT_model_denotes x›
    moreover assume ‹AOT_model_denotes y›
    moreover assume ‹AOT_model_term_equiv x y›
    moreover have 1: ‹φ x = φ y›
      using assms calculation unfolding AOT_instance_of_cqt_2_def by blast
    ultimately have ‹AOT_exe (AOT_lambda (φ x)) (κs x) =
                     AOT_exe (AOT_lambda (φ y)) (κs y)›
      unfolding 1
      apply (safe intro!: AOT_sem_exe_equiv)
      by (metis AOT_instance_of_cqt_2_exe_arg_def assms(2))
  }
  thus ?thesis
  unfolding AOT_instance_of_cqt_2_def
            AOT_instance_of_cqt_2_exe_arg_def
  by blast
qed
lemma AOT_instance_of_cqt_2_intro_prod[AOT_instance_of_cqt_2_intro]:
  assumes ‹⋀ x . AOT_instance_of_cqt_2 (φ x)›
      and ‹⋀ x . AOT_instance_of_cqt_2 (λ z . φ z x)›
  shows ‹AOT_instance_of_cqt_2 (λ(x,y) . φ x y)›
  using assms unfolding AOT_instance_of_cqt_2_def
  by (auto simp add: AOT_model_lambda_denotes AOT_sem_denotes
                AOT_model_denotes_prod_def
                AOT_model_term_equiv_prod_def)

text‹The following are already derivable semantically, but not yet added
     to @{attribute AOT_instance_of_cqt_2_intro}. They will be added with the
     next planned extension of axiom cqt:2.›
named_theorems AOT_instance_of_cqt_2_intro_next
definition AOT_instance_of_cqt_2_enc_arg :: ‹('a::AOT_κs ⇒ 'b::AOT_κs) ⇒ bool› where
  ‹AOT_instance_of_cqt_2_enc_arg ≡ λ φ . ∀ x y z .
      AOT_model_denotes x ∧ AOT_model_denotes y ∧ AOT_model_term_equiv x y ⟶
      AOT_enc (φ x) z = AOT_enc (φ y) z›
definition AOT_instance_of_cqt_2_enc_rel :: ‹('a::AOT_κs ⇒ <'b::AOT_κs>) ⇒ bool› where
  ‹AOT_instance_of_cqt_2_enc_rel ≡ λ φ . ∀ x y z .
      AOT_model_denotes x ∧ AOT_model_denotes y ∧ AOT_model_term_equiv x y ⟶
      AOT_enc z (φ x) = AOT_enc z (φ y)›
lemma AOT_instance_of_cqt_2_intros_enc[AOT_instance_of_cqt_2_intro_next]:
  assumes ‹AOT_instance_of_cqt_2_enc_rel Π› and ‹AOT_instance_of_cqt_2_enc_arg κs›
  shows ‹AOT_instance_of_cqt_2 (λx . AOT_enc (κs x) «[«Π x»]»)›
  using assms
  unfolding AOT_instance_of_cqt_2_def AOT_sem_denotes AOT_model_lambda_denotes
            AOT_instance_of_cqt_2_enc_rel_def AOT_sem_not AOT_sem_box AOT_sem_act
            AOT_sem_dia AOT_sem_conj AOT_sem_disj AOT_sem_equiv AOT_sem_imp
            AOT_sem_forall AOT_sem_exists AOT_instance_of_cqt_2_enc_arg_def
  by fastforce+
lemma AOT_instance_of_cqt_2_enc_arg_intro_const[AOT_instance_of_cqt_2_intro_next]:
  ‹AOT_instance_of_cqt_2_enc_arg (λx. c)›
  unfolding AOT_instance_of_cqt_2_enc_arg_def by simp
lemma AOT_instance_of_cqt_2_enc_arg_intro_desc[AOT_instance_of_cqt_2_intro_next]:
  assumes ‹⋀z :: 'a::AOT_κ. AOT_instance_of_cqt_2 (Φ z)›
  shows ‹AOT_instance_of_cqt_2_enc_arg (λ κ :: 'b::AOT_κ . «ιz(Φ{z,κ})»)›
proof -
  have 0: ‹⋀ κ κ'. AOT_model_denotes κ ∧ AOT_model_denotes κ' ∧
                   AOT_model_term_equiv κ κ' ⟹
                   Φ z κ = Φ z κ'› for z
    using assms
    unfolding AOT_instance_of_cqt_2_def
              AOT_sem_denotes AOT_model_lambda_denotes by force
  {
    fix κ κ'
    have ‹«ιz(Φ{z,κ})» = «ιz(Φ{z,κ'})»›
      if ‹AOT_model_denotes κ ∧ AOT_model_denotes κ' ∧ AOT_model_term_equiv κ κ'›
      using 0[OF that]
      by auto
  }
  thus ?thesis using 0
    unfolding AOT_instance_of_cqt_2_enc_arg_def by meson
qed
lemma AOT_instance_of_cqt_2_enc_rel_intro[AOT_instance_of_cqt_2_intro_next]:
  assumes ‹⋀ κ . AOT_instance_of_cqt_2 (λκ' :: 'b::AOT_κs . φ κ κ')›
  assumes ‹⋀ κ' . AOT_instance_of_cqt_2 (λκ :: 'a::AOT_κs . φ κ κ')›
  shows ‹AOT_instance_of_cqt_2_enc_rel (λκ :: 'a::AOT_κs. AOT_lambda (λκ'. φ κ κ'))›
proof -
  {
    fix x y :: 'a and z ::'b
    assume ‹AOT_model_term_equiv x y›
    moreover assume ‹AOT_model_denotes x›
    moreover assume ‹AOT_model_denotes y›
    ultimately have ‹φ x = φ y›
      using assms unfolding AOT_instance_of_cqt_2_def by blast
    hence ‹AOT_enc z (AOT_lambda (φ x)) = AOT_enc z (AOT_lambda (φ y))›
      by simp
  }
  thus ?thesis
    unfolding AOT_instance_of_cqt_2_enc_rel_def by auto
qed

text‹Further restrict unary individual variables to type @{typ κ} (rather
     than class @{class AOT_κ} only) and define being ordinary and being abstract.›
AOT_register_type_constraints
  Individual: ‹κ› ‹_::AOT_κs›

AOT_define AOT_ordinary :: ‹Π› (‹O!›) ‹O! =df [λx ◇E!x]›
declare AOT_ordinary[AOT del, AOT_defs del]
AOT_define AOT_abstract :: ‹Π› (‹A!›) ‹A! =df [λx ¬◇E!x]›
declare AOT_abstract[AOT del, AOT_defs del]

context AOT_meta_syntax
begin
notation AOT_ordinary ("O!")
notation AOT_abstract ("A!")
end
context AOT_no_meta_syntax
begin
no_notation AOT_ordinary ("O!")
no_notation AOT_abstract ("A!")
end

no_translations
  "_AOT_concrete" => "CONST AOT_term_of_var (CONST AOT_concrete)"
parse_translation‹
[(syntax_const‹_AOT_concrete›, fn _ => fn [] =>
  Const (const_name‹AOT_term_of_var›, dummyT)
  $ Const (const_name‹AOT_concrete›, typ‹<κ> AOT_var›))]
›

text‹Auxiliary lemmata.›
lemma AOT_sem_ordinary: "«O!» = «[λx ◇E!x]»"
  using AOT_ordinary[THEN AOT_sem_id_def0E1] AOT_sem_ordinary_def_denotes
  by (auto simp: AOT_sem_eq)
lemma AOT_sem_abstract: "«A!» = «[λx ¬◇E!x]»"
  using AOT_abstract[THEN AOT_sem_id_def0E1]  AOT_sem_abstract_def_denotes
  by (auto simp: AOT_sem_eq)
lemma AOT_sem_ordinary_denotes: ‹[w ⊨ O!↓]›
  by (simp add: AOT_sem_ordinary AOT_sem_ordinary_def_denotes)
lemma AOT_meta_abstract_denotes: ‹[w ⊨ A!↓]›
  by (simp add: AOT_sem_abstract AOT_sem_abstract_def_denotes)
lemma AOT_model_abstract_ακ: ‹∃ a . κ = ακ a› if ‹[v ⊨ A!κ]›
  using that[unfolded AOT_sem_abstract, simplified
      AOT_meta_abstract_denotes[unfolded AOT_sem_abstract, THEN AOT_sem_lambda_beta,
          OF that[simplified AOT_sem_exe, THEN conjunct2, THEN conjunct1]]]
  apply (simp add: AOT_sem_not AOT_sem_dia AOT_sem_concrete)
  by (metis AOT_model_ω_concrete_in_some_world AOT_model_concrete_κ.simps(1)
            AOT_model_denotes_κ_def AOT_sem_denotes AOT_sem_exe κ.exhaust_disc
            is_ακ_def is_ωκ_def that)
lemma AOT_model_ordinary_ωκ: ‹∃ a . κ = ωκ a› if ‹[v ⊨ O!κ]›
  using that[unfolded AOT_sem_ordinary, simplified
      AOT_sem_ordinary_denotes[unfolded AOT_sem_ordinary, THEN AOT_sem_lambda_beta,
        OF that[simplified AOT_sem_exe, THEN conjunct2, THEN conjunct1]]]
  apply (simp add: AOT_sem_dia AOT_sem_concrete)
  by (metis AOT_model_concrete_κ.simps(2) AOT_model_concrete_κ.simps(3)
            κ.exhaust_disc is_ακ_def is_ωκ_def is_nullκ_def)
lemma AOT_model_ωκ_ordinary: ‹[v ⊨ O!«ωκ x»]›
  by (metis AOT_model_abstract_ακ AOT_model_denotes_κ_def AOT_sem_abstract
            AOT_sem_denotes AOT_sem_ind_eq AOT_sem_ordinary κ.disc(7) κ.distinct(1))
lemma AOT_model_ακ_ordinary: ‹[v ⊨ A!«ακ x»]›
  by (metis AOT_model_denotes_κ_def AOT_model_ordinary_ωκ AOT_sem_abstract
            AOT_sem_denotes AOT_sem_ind_eq AOT_sem_ordinary κ.disc(8) κ.distinct(1))
AOT_theorem prod_denotesE: assumes ‹«(κ1,κ2)»↓› shows ‹κ1↓ & κ2↓›
  using assms by (simp add: AOT_sem_denotes AOT_sem_conj AOT_model_denotes_prod_def)
declare prod_denotesE[AOT del]
AOT_theorem prod_denotesI: assumes ‹κ1↓ & κ2↓› shows ‹«(κ1,κ2)»↓›
  using assms by (simp add: AOT_sem_denotes AOT_sem_conj AOT_model_denotes_prod_def)
declare prod_denotesI[AOT del]


text‹Prepare the derivation of the additional axioms that are validated by
     our extended models.›
locale AOT_ExtendedModel =
  assumes AOT_ExtendedModel: ‹AOT_ExtendedModel›
begin
lemma AOT_sem_indistinguishable_ord_enc_all:
  assumes Π_den: ‹[v ⊨ Π↓]›
  assumes Ax: ‹[v ⊨ A!x]›
  assumes Ay: ‹[v ⊨ A!y]›
  assumes indist: ‹[v ⊨ ∀F □([F]x ≡ [F]y)]›
  shows
  ‹[v ⊨ ∀G(∀z(O!z → □([G]z ≡ [Π]z)) → x[G])] =
   [v ⊨ ∀G(∀z(O!z → □([G]z ≡ [Π]z)) → y[G])]›
proof -
    have 0: ‹[v ⊨ [λx ¬◇[E!]x]x]›
      using Ax by (simp add: AOT_sem_abstract)
    have 1: ‹[v ⊨ [λx ¬◇[E!]x]y]›
      using Ay by (simp add: AOT_sem_abstract)
    {
      assume ‹[v ⊨ ∀G(∀z (O!z → □([G]z ≡ [Π]z)) → x[G])]›
      hence 3: ‹[v ⊨ ∀G(∀z([λx ◇[E!]x]z → □([G]z ≡ [Π]z)) → x[G])]›
        by (simp add: AOT_sem_ordinary)
      {
        fix Π' :: ‹<κ>›
        assume 1: ‹[v ⊨ Π'↓]›
        assume 2: ‹[v ⊨ [λx ◇[E!]x]z → □([Π']z ≡ [Π]z)]› for z
        have ‹[v ⊨ x[Π']]›
          using 3
          by (auto simp: AOT_sem_forall AOT_sem_imp AOT_sem_box AOT_sem_denotes)
             (metis (no_types, lifting) 1 2 AOT_term_of_var_cases AOT_sem_box
                                        AOT_sem_denotes AOT_sem_imp)
      } note 3 = this
      fix Π' :: ‹<κ>›
      assume Π_den: ‹[v ⊨ Π'↓]›
      assume 4: ‹[v ⊨ ∀z (O!z → □([Π']z ≡ [Π]z))]›
      {
        fix κ0
        assume ‹[v ⊨ [λx ◇[E!]x]κ0]›
        hence ‹[v ⊨ O!κ0]›
          using AOT_sem_ordinary by metis
        moreover have ‹[v ⊨ κ0↓]›
          using calculation by (simp add: AOT_sem_exe)
        ultimately have ‹[v ⊨ □([Π']κ0 ≡ [Π]κ0)]›
          using 4 by (auto simp: AOT_sem_forall AOT_sem_imp)
      } note 4 = this
      {
        fix Π'' :: ‹<κ>›
        assume ‹[v ⊨ Π''↓]›
        moreover assume ‹[w ⊨ [Π'']κ0] = [w ⊨ [Π']κ0]› if ‹[v ⊨ [λx ◇E!x]κ0]› for κ0 w
        ultimately have 5: ‹[v ⊨ x[Π'']]›
          using 4 3
          by (auto simp: AOT_sem_imp AOT_sem_equiv AOT_sem_box)
      } note 5 = this
      have ‹[v ⊨ y[Π']]›
        apply (rule AOT_sem_enc_indistinguishable_all[OF AOT_ExtendedModel])
        apply (fact 0)
        by (auto simp: 5 0 1 Π_den indist[simplified AOT_sem_forall
                       AOT_sem_box AOT_sem_equiv])
    }
    moreover {
    {
      assume ‹[v ⊨ ∀G(∀z (O!z → □([G]z ≡ [Π]z)) → y[G])]›
      hence 3: ‹[v ⊨ ∀G(∀z ([λx ◇[E!]x]z → □([G]z ≡ [Π]z)) → y[G])]›
        by (simp add: AOT_sem_ordinary)
      {
        fix Π' :: ‹<κ>›
        assume 1: ‹[v ⊨ Π'↓]›
        assume 2: ‹[v ⊨ [λx ◇[E!]x]z → □([Π']z ≡ [Π]z)]› for z
        have ‹[v ⊨ y[Π']]›
          using 3
          apply (simp add: AOT_sem_forall AOT_sem_imp AOT_sem_box AOT_sem_denotes)
          by (metis (no_types, lifting) 1 2 AOT_model.AOT_term_of_var_cases
                                        AOT_sem_box AOT_sem_denotes AOT_sem_imp)
      } note 3 = this
      fix Π' :: ‹<κ>›
      assume Π_den: ‹[v ⊨ Π'↓]›
      assume 4: ‹[v ⊨ ∀z (O!z → □([Π']z ≡ [Π]z))]›
      {
        fix κ0
        assume ‹[v ⊨ [λx ◇[E!]x]κ0]›
        hence ‹[v ⊨ O!κ0]›
          using AOT_sem_ordinary by metis
        moreover have ‹[v ⊨ κ0↓]›
          using calculation by (simp add: AOT_sem_exe)
        ultimately have ‹[v ⊨ □([Π']κ0 ≡ [Π]κ0)]›
          using 4 by (auto simp: AOT_sem_forall AOT_sem_imp)
      } note 4 = this
      {
        fix Π'' :: ‹<κ>›
        assume ‹[v ⊨ Π''↓]›
        moreover assume ‹[w ⊨ [Π'']κ0] = [w ⊨ [Π']κ0]› if ‹[v ⊨ [λx ◇E!x]κ0]› for w κ0
        ultimately have ‹[v ⊨ y[Π'']]›
          using 3 4 by (auto simp: AOT_sem_imp AOT_sem_equiv AOT_sem_box)
      } note 5 = this
      have ‹[v ⊨ x[Π']]›
        apply (rule AOT_sem_enc_indistinguishable_all[OF AOT_ExtendedModel])
              apply (fact 1)
        by (auto simp: 5 0 1 Π_den indist[simplified AOT_sem_forall
                       AOT_sem_box AOT_sem_equiv])
    }
  }
  ultimately show ‹[v ⊨ ∀G (∀z (O!z → □([G]z ≡ [Π]z)) → x[G])] =
        [v ⊨ ∀G (∀z (O!z → □([G]z ≡ [Π]z)) → y[G])]›
    by (auto simp: AOT_sem_forall AOT_sem_imp)
qed

lemma AOT_sem_indistinguishable_ord_enc_ex:
  assumes Π_den: ‹[v ⊨ Π↓]›
  assumes Ax: ‹[v ⊨ A!x]›
  assumes Ay: ‹[v ⊨ A!y]›
  assumes indist: ‹[v ⊨ ∀F □([F]x ≡ [F]y)]›
  shows ‹[v ⊨ ∃G(∀z (O!z → □([G]z ≡ [Π]z)) & x[G])] =
         [v ⊨ ∃G(∀z(O!z → □([G]z ≡ [Π]z)) & y[G])]›
proof -
  have Aux: ‹[v ⊨ [λx ◇[E!]x]κ] = ([v ⊨ [λx ◇[E!]x]κ] ∧ [v ⊨ κ↓])› for v κ
    using AOT_sem_exe by blast
  AOT_modally_strict {
    fix x y
    AOT_assume Π_den: ‹[Π]↓›
    AOT_assume 2: ‹∀F □([F]x ≡ [F]y)›
    AOT_assume ‹A!x›
    AOT_hence 0: ‹[λx ¬◇[E!]x]x›
      by (simp add: AOT_sem_abstract)
    AOT_assume ‹A!y›
    AOT_hence 1: ‹[λx ¬◇[E!]x]y›
      by (simp add: AOT_sem_abstract)
    {
      AOT_assume ‹∃G(∀z (O!z → □([G]z ≡ [Π]z)) & x[G])›
      then AOT_obtain Π'
        where Π'_den: ‹Π'↓›
          and Π'_indist: ‹∀z (O!z → □([Π']z ≡ [Π]z))›
          and x_enc_Π': ‹x[Π']›
        by (meson AOT_sem_conj AOT_sem_exists)
      {
        fix κ0
        AOT_assume ‹[λx ◇[E!]x]κ0›
        AOT_hence ‹□([Π']κ0 ≡ [Π]κ0)›
          using Π'_indist
          by (auto simp: AOT_sem_exe AOT_sem_imp AOT_sem_exists AOT_sem_conj
                         AOT_sem_ordinary AOT_sem_forall)
      } note 3 = this
      AOT_have ‹∀z ([λx ◇[E!]x]z → □([Π']z ≡ [Π]z))›
        using Π'_indist by (simp add: AOT_sem_ordinary)
      AOT_obtain Π'' where
          Π''_den: ‹Π''↓› and
          Π''_indist: ‹[λx ◇[E!]x]κ0 → □([Π'']κ0 ≡ [Π]κ0)› and
          y_enc_Π'': ‹y[Π'']› for κ0
        using AOT_sem_enc_indistinguishable_ex[OF AOT_ExtendedModel,
                OF 0, OF 1, rotated, OF Π_den,
                OF exI[where x=Π'], OF conjI, OF Π'_den, OF conjI,
                OF x_enc_Π', OF allI, OF impI,
                OF 3[simplified AOT_sem_box AOT_sem_equiv], simplified, OF
                2[simplified AOT_sem_forall AOT_sem_equiv AOT_sem_box,
                  THEN spec, THEN mp, THEN spec], simplified]
        unfolding AOT_sem_imp AOT_sem_box AOT_sem_equiv by blast
      {
        AOT_have ‹Π''↓›
            and ‹∀x ([λx ◇[E!]x]x → □([Π'']x ≡ [Π]x))›
            and ‹y[Π'']›
          apply (simp add: Π''_den)
          apply (simp add: AOT_sem_forall Π''_indist)
          by (simp add: y_enc_Π'')
      } note 2 = this
      AOT_have ‹∃G(∀z (O!z → □([G]z ≡ [Π]z)) & y[G])›
        apply (simp add: AOT_sem_exists AOT_sem_ordinary
            AOT_sem_imp AOT_sem_box AOT_sem_forall AOT_sem_equiv AOT_sem_conj)
        using 2[simplified AOT_sem_box AOT_sem_equiv AOT_sem_imp AOT_sem_forall]
        by blast
    }
  } note 0 = this
  AOT_modally_strict {
    {
      fix x y
      AOT_assume Π_den: ‹[Π]↓›
      moreover AOT_assume ‹∀F □([F]x ≡ [F]y)›
      moreover AOT_have ‹∀F □([F]y ≡ [F]x)›
        using calculation(2)
        by (auto simp: AOT_sem_forall AOT_sem_box AOT_sem_equiv)
      moreover AOT_assume ‹A!x›
      moreover AOT_assume ‹A!y›
      ultimately AOT_have ‹∃G (∀z (O!z → □([G]z ≡ [Π]z)) & x[G]) ≡
                           ∃G (∀z (O!z → □([G]z ≡ [Π]z)) & y[G])›
        using 0 by (auto simp: AOT_sem_equiv)
    }
    have 1: ‹[v ⊨ ∀F □([F]y ≡ [F]x)]›
      using indist
      by (auto simp: AOT_sem_forall AOT_sem_box AOT_sem_equiv)
    thus ‹[v ⊨ ∃G (∀z (O!z → □([G]z ≡ [Π]z)) & x[G])] =
        [v ⊨ ∃G (∀z (O!z → □([G]z ≡ [Π]z)) & y[G])]›
      using assms
      by (auto simp: AOT_sem_imp AOT_sem_conj AOT_sem_equiv 0)
  }
qed
end


(* Collect all theorems that are not in Main and not declared [AOT]
   and store them in a blacklist. *)
setup‹setup_AOT_no_atp›
bundle AOT_no_atp begin declare AOT_no_atp[no_atp] end
(* Can be used as: "including AOT_no_atp sledgehammer" or
   "sledgehammer(del: AOT_no_atp) *)

(*<*)
end
(*>*)