Quelle  AOT_semantics.thy

(*<*)
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=‹λ τ . ε_\o 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=‹λ φ ψ . ε_\o w . ([w ⊨ φ] ⟶ [w ⊨ ψ])›])
    (simp add: AOT_model_proposition_choice_simp)

specification(AOT_not)
  AOT_sem_not: ‹[w ⊨ ¬φ] = (¬[w ⊨ φ])›
  by (rule exI[where x=‹λ φ . ε_\o 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=‹λ φ . ε_\o w . ∀ w . [w ⊨ φ]›])
     (simp add: AOT_model_proposition_choice_simp)

text‹\linelabel{AOT_act_spec}›
specification(AOT_act)
  AOT_sem_act: ‹[w ⊨ \Aφ] = [w₀ ⊨ φ]›
  by (rule exI[where x=‹λ φ . ε_\o w . [w₀ ⊨ φ]›])
     (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 . ε_\o 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=‹λ τ τ' . ε_\o 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})↓] = (∃! κ . [w₀ ⊨ κ↓] ∧ [w₀ ⊨ φ{κ}])›
  ― ‹Denoting descriptions satisfy their matrix in the actual world.›
  AOT_sem_desc_prop: ‹[w ⊨ \ιx(φ{x})↓] ==> [w₀ ⊨ φ{\ιx(φ{x})}]›
  ― ‹Uniqueness of denoting descriptions.›
  AOT_sem_desc_unique: ‹[w ⊨ \ιx(φ{x})↓] ==> [w ⊨ κ↓] ==> [w₀ ⊨ φ{κ}] ==>
 [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 → o) → 'a› where
    nondenoting: ‹∀ φ . ¬AOT_model_denotes (nondenoting φ)›
    by fast
  define desc where
    ‹desc = (λ φ . if (∃! κ . [w₀ ⊨ κ↓] ∧ [w₀ ⊨ φ{κ}])
 then (THE κ . [w₀ ⊨ κ↓] ∧ [w₀ ⊨ φ{κ}])
 else nondenoting φ)›
  {
    fix φ :: ‹'a → o›
    assume ex1: ‹∃! κ . [w₀ ⊨ κ↓] ∧ [w₀ ⊨ φ{κ}]›
    then obtain κ where x_prop: "[w₀ ⊨ κ↓] ∧ [w₀ ⊨ φ{κ}]"
      unfolding AOT_sem_denotes by blast
    moreover have "(desc φ) = κ"
      unfolding desc_def using x_prop ex1 by fastforce
    ultimately have "[w₀ ⊨ «desc φ¬↓] ∧ [w₀ ⊨ «φ (desc φ)¬]"
      by blast
  } note 1 = this
  moreover {
    fix φ :: ‹'a → o›
    assume nex1: ‹∄! κ . [w₀ ⊨ κ↓] ∧ [w₀ ⊨ φ{κ}]›
    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 φ¬↓] = (∃! κ . [w₀ ⊨ κ↓] ∧ [w₀ ⊨ φ{κ}])› for φ w
    by (simp add: AOT_sem_denotes desc_def nondenoting)
  have ‹(∀φ w. [w ⊨ «desc φ¬↓] = (∃!κ. [w₀ ⊨ κ↓] ∧ [w₀ ⊨ φ{κ}])) ∧
 (∀φ w. [w ⊨ «desc φ¬↓] ⟶ [w₀ ⊨ «φ (desc φ)¬]) ∧
 (∀φ w κ. [w ⊨ «desc φ¬↓] ⟶ [w ⊨ κ↓] ⟶ [w₀ ⊨ φ{κ}] ⟶
 [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 ⊨ [Π]κ₁...κ_n] = ([w ⊨ Π↓] ∧ [w ⊨ κ₁...κ_n↓] ∧
 [w ⊨ «Rep_rel Π κ₁κ_n¬])›
  ― ‹\eta-conversion for denoting terms; equivalent to AOT's axiom›
  AOT_sem_lambda_eta: ‹[w ⊨ Π↓] ==> [w ⊨ [λν₁...ν_n [Π]ν₁...ν_n] = Π]›
  ― ‹\beta-conversion; equivalent to AOT's axiom›
  AOT_sem_lambda_beta: ‹[w ⊨ [λν₁...ν_n φ{ν₁...ν_n}]↓] ==> [w ⊨ κ₁...κ_n↓] ==>
 [w ⊨ [λν₁...ν_n φ{ν₁...ν_n}]κ₁...κ_n] = [w ⊨ φ{κ₁...κ_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 ⊨ [λν₁...ν_n φ{ν₁...ν_n}]↓] =
 (∀ v κ₁κ_n κ₁'κ_n' . [v ⊨ κ₁...κ_n↓] ∧ [v ⊨ κ₁'...κ_n'↓] ∧
 (∀ Π v . [v ⊨ Π↓] ⟶ [v ⊨ [Π]κ₁...κ_n] = [v ⊨ [Π]κ₁'...κ_n']) ⟶
 [v ⊨ φ{κ₁...κ_n}] = [v ⊨ φ{κ₁'...κ_n'}])›
  ― ‹Equivalent to AOT's coexistence axiom.›
  AOT_sem_lambda_coex: ‹[w ⊨ [λν₁...ν_n φ{ν₁...ν_n}]↓] ==>
 (∀ w κ₁κ_n . [w ⊨ κ₁...κ_n↓] ⟶ [w ⊨ φ{κ₁...κ_n}] = [w ⊨ ψ{κ₁...κ_n}]) ==>
 [w ⊨ [λν₁...ν_n ψ{ν₁...ν_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: ‹«[λν₁...ν_n φ]¬ = «[λν₁...ν_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 . ε_\o w. True)›])
       (meson AOT_model_denotes_rel.abs_eq AOT_model_nondenoting_ex
              AOT_model_proposition_choice_simp)
  define exe :: ‹<'a> → 'a → o› where
    ‹exe ≡ λ Π κs . if AOT_model_denotes Π
 then Rep_rel Π κs
 else (ε_\o w . False)›
  define lambda :: ‹('a→o) → <'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 (ε_\o 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→o›
    using that AOT_model_term_equiv_eps(2) by blast
  have exe_rep_rel: ‹[w ⊨ «exe Π κ₁κ_n¬] = ([w ⊨ Π↓] ∧ [w ⊨ κ₁...κ_n↓] ∧
 [w ⊨ «Rep_rel Π κ₁κ_n¬])› for w Π κ₁κ_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 κ₁κ_n κ₁'κ_n' . [v ⊨ κ₁...κ_n↓] ∧ [v ⊨ κ₁'...κ_n'↓] ∧
 (∀ Π v . [v ⊨ Π↓] ⟶ [v ⊨ «exe Π κ₁κ_n¬] = [v ⊨ «exe Π κ₁'κ_n'¬]) ⟶
 [v ⊨ φ{κ₁...κ_n}] = [v ⊨ φ{κ₁'...κ_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 κ₁κ_n κ₁'κ_n' . [v ⊨ κ₁...κ_n↓] ∧ [v ⊨ κ₁'...κ_n'↓] ∧
 (∀ Π v . [v ⊨ Π↓] ⟶ [v ⊨ «exe Π κ₁κ_n¬] = [v ⊨ «exe Π κ₁'κ_n'¬]) ⟶
 [v ⊨ φ{κ₁...κ_n}] = [v ⊨ φ{κ₁'...κ_n'}]›
      unfolding AOT_sem_denotes
      by (metis (no_types) AOT_sem_denotes lambda_denotes_beta)
  next
    assume ‹∀ v κ₁κ_n κ₁'κ_n' . [v ⊨ κ₁...κ_n↓] ∧ [v ⊨ κ₁'...κ_n'↓] ∧
 (∀ Π v . [v ⊨ Π↓] ⟶ [v ⊨ «exe Π κ₁κ_n¬] = [v ⊨ «exe Π κ₁'κ_n'¬]) ⟶
 [v ⊨ φ{κ₁...κ_n}] = [v ⊨ φ{κ₁'...κ_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 κ₁κ_n . [w ⊨ κ₁...κ_n↓] ⟶ [w ⊨ φ{κ₁...κ_n}] = [w ⊨ ψ{κ₁...κ_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 κ₁κ_n ∧
 AOT_model_denotes κ₁'κ_n' ∧
 (∀Π v. AOT_model_denotes Π ⟶ [v ⊨ [Π]κ₁...κ_n] = [v ⊨ [Π]κ₁'...κ_n']) ⟶
 [v ⊨ φ{κ₁...κ_n}] = [v ⊨ φ{κ₁'...κ_n'}]› for κ₁κ_n κ₁'κ_n' v
    using AOT_sem_lambda_denotes[simplified AOT_sem_denotes] by blast
  {
    fix v and κ₁κ_n κ₁'κ_n' :: 'a
    assume d: ‹AOT_model_denotes κ₁κ_n ∧ AOT_model_denotes κ₁'κ_n' ∧
 AOT_model_term_equiv κ₁κ_n κ₁'κ_n'›
    hence ‹∀Π w. AOT_model_denotes Π ⟶ [w ⊨ [Π]κ₁...κ_n] = [w ⊨ [Π]κ₁'...κ_n']›
      by (metis AOT_sem_exe_equiv)
    hence ‹[v ⊨ φ{κ₁...κ_n}] = [v ⊨ φ{κ₁'...κ_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 κ₁κ_n κ₁'κ_n' :: 'a
    assume den: ‹AOT_model_denotes κ₁κ_n›
    moreover assume den': ‹AOT_model_denotes κ₁'κ_n'›
    assume ‹∀Π v . AOT_model_denotes Π ⟶
 [v ⊨ [Π]κ₁...κ_n] = [v ⊨ [Π]κ₁'...κ_n']›
    hence ‹∀Π v . AOT_model_denotes Π ⟶
 [v ⊨ «Rep_rel Π κ₁κ_n¬] = [v ⊨ «Rep_rel Π κ₁'κ_n'¬]›
      by (simp add: AOT_sem_denotes AOT_sem_exe den den')
    hence "AOT_model_term_equiv κ₁κ_n κ₁'κ_n'"
      unfolding AOT_model_term_equiv_rel_equiv[OF den, OF den']
      by argo
    hence ‹[v ⊨ φ{κ₁...κ_n}] = [v ⊨ φ{κ₁'...κ_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 . ε_\o 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 → o) → ('a → o) → o›
  assumes AOT_sem_proj_id_prop:
    ‹[v ⊨ Π = Π'] =
 [v ⊨ Π↓ & Π'↓ & ∀α («AOT_sem_proj_id α (λ τ . «[Π]τ¬) (λ τ . «[Π']τ¬)¬)]›
      and AOT_sem_proj_id_refl:
    ‹[v ⊨ τ↓] ==> [v ⊨ [λν₁...ν_n φ{ν₁...ν_n}] = [λν₁...ν_n φ{ν₁...ν_n}]] ==>
 [v ⊨ «AOT_sem_proj_id τ φ φ¬]›

class AOT_UnaryRelationProjection = AOT_RelationProjection +
  assumes AOT_sem_unary_proj_id:
    ‹AOT_sem_proj_id κ φ ψ = «[λν₁...ν_n φ{ν₁...ν_n}] = [λν₁...ν_n ψ{ν₁...ν_n}]¬›

instantiation κ :: AOT_UnaryRelationProjection
begin
definition AOT_sem_proj_id_κ :: ‹κ → (κ → o) → (κ → o) → o› where
  ‹AOT_sem_proj_id_κ κ φ ψ = «[λz φ{z}] = [λz ψ{z}]¬›
instance proof
  show ‹[v ⊨ Π = Π'] =
 [v ⊨ Π↓ & Π'↓ & ∀α («AOT_sem_proj_id α (λ τ . «[Π]τ¬) (λ τ . «[Π']τ¬)¬)]›
    for v and Π Π' :: ‹<\<kappa>>›
    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 κ φ ψ = «[λν₁...ν_n φ{ν₁...ν_n}] = [λν₁...ν_n ψ{ν₁...ν_n}]¬›
    for κ :: κ and φ ψ
    unfolding AOT_sem_proj_id_κ_def ..
next
  show ‹[v ⊨ «AOT_sem_proj_id τ φ φ¬]›
    if ‹[v ⊨ τ↓]› and ‹[v ⊨ [λν₁...ν_n φ{ν₁...ν_n}] = [λν₁...ν_n φ{ν₁...ν_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 → o) → ('a×'b → o) → o› 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 κ₁'κ_n'›
               if ‹[w ⊨ [Π]κ κ₁'...κ_n']› for w κ₁'κ_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 κ₁'κ_n' :: 'b and Π :: ‹<'a×'b>›
    assume Π_denotes: ‹AOT_model_denotes Π›
    assume β_denotes: ‹AOT_model_denotes κ₁'κ_n'›
    hence ‹AOT_exe Π (x, κ₁'κ_n') = AOT_exe Π (y, κ₁'κ_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 ⊨ [Π]κ κ₁'...κ_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,κ₁'κ_n') = AOT_model_irregular (λz. AOT_exe Π (z,κ₁'κ_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,κ₁'κ_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 κ₁'κ_n' :: 'b
      assume ‹Π = Π'›
      assume ‹AOT_model_denotes (κ,κ₁'κ_n')›
      hence ‹AOT_model_denotes κ› and beta_denotes: ‹AOT_model_denotes κ₁'κ_n'›
        by (auto simp: AOT_model_denotes_prod_def)
      have ‹AOT_model_denotes «[λz [Π]z κ₁'...κ_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 κ₁'...κ_n']¬ = «[λz [Π']z κ₁'...κ_n']¬›
        by (simp add: ‹Π = Π'›)
      moreover have ‹[v ⊨ «AOT_sem_proj_id κ₁'κ_n' (λκ₁'κ_n'. «[Π]κ κ₁'...κ_n'¬)
 (λκ₁'κ_n'. «[Π']κ κ₁'...κ_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 (κ,κ₁'κ_n') (λ κ₁κ_n . «[Π]κ₁...κ_n¬)
 (λ κ₁κ_n . «[Π']κ₁...κ_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 α (λ κ₁κ_n . «[Π]κ₁...κ_n¬) (λ κ₁κ_n . «[Π']κ₁...κ_n¬)¬]›
      hence 0: ‹AOT_model_denotes κ ==> AOT_model_denotes κ₁'κ_n' ==>
 AOT_model_denotes «[λz [Π]z κ₁'...κ_n']¬ ∧
 AOT_model_denotes «[λz [Π']z κ₁'...κ_n']¬ ∧
 «[λz [Π]z κ₁'...κ_n']¬ = «[λz [Π']z κ₁'...κ_n']¬ ∧
 [v ⊨ «AOT_sem_proj_id κ₁'κ_n' (λκ₁κ_n. «[Π]κ κ₁...κ_n¬)
 (λκ₁κ_n. «[Π']κ κ₁...κ_n¬)¬]› for κ κ₁'κ_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 κ₁'κ_n' (λκ₁'κ_n'. «[Π]κ κ₁'...κ_n'¬)
 (λκ₁'κ_n'. «[Π']κ κ₁'...κ_n'¬)¬]›
          if ‹AOT_model_denotes κ₁'κ_n'› for κ₁'κ_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 κ₁'κ_n' :: 'b
        assume βden: ‹AOT_model_denotes κ₁'κ_n'›
        have 1: ‹«[λz [Π]z κ₁'...κ_n']¬ = «[λz [Π']z κ₁'...κ_n']¬›
          using 0 βden AOT_model_denoting_ex by blast
        hence ‹Abs_rel (λz. Rep_rel Π (z, κ₁'κ_n')) =
 Abs_rel (λz. Rep_rel Π' (z, κ₁'κ_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,κ₁'κ_n') = Rep_rel Π' (x,κ₁'κ_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 κ (λ κ₁κ_n . «[Π]κ₁...κ_n¬)
 (λ κ₁κ_n . «[Π']κ₁...κ_n¬)¬])›
      by auto
  }
  thus ‹[v ⊨ Π = Π'] = [v ⊨ Π↓ & Π'↓ &
 ∀α («AOT_sem_proj_id α (λ κ₁κ_n . «[Π]κ₁...κ_n¬) (λ κ₁κ_n . «[Π']κ₁...κ_n¬)¬)]›
    by (auto simp: AOT_sem_eq AOT_sem_denotes AOT_sem_forall AOT_sem_conj)
next
  fix v and φ :: ‹'a×'b→o› and τ :: ‹'a×'b›
  assume ‹[v ⊨ τ↓]›
  moreover assume ‹[v ⊨ [λz₁...z_n «φ z₁z_n¬] = [λz₁...z_n «φ z₁z_n¬]]›
  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 Π :: ‹<\<kappa>×κ>›
  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 ⊨ Π↓ & Π'↓ & ∀x₁∀x₂∀x₃ (
 [λz [Π]z x₂ x₃] = [λz [Π']z x₂ x₃] &
 [λz [Π]x₁ z x₃] = [λz [Π']x₁ z x₃] &
 [λz [Π]x₁ x₂ z] = [λz [Π']x₁ x₂ z])]›
  for Π :: ‹<\<kappa>×κ×κ>›
  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 ⊨ Π↓ & Π'↓ & ∀x₁∀x₂∀x₃∀x₄ (
 [λz [Π]z x₂ x₃ x₄] = [λz [Π']z x₂ x₃ x₄] &
 [λz [Π]x₁ z x₃ x₄] = [λz [Π']x₁ z x₃ x₄] &
 [λz [Π]x₁ x₂ z x₄] = [λz [Π']x₁ x₂ z x₄] &
 [λz [Π]x₁ x₂ x₃ z] = [λz [Π']x₁ x₂ x₃ z])]›
  for Π :: ‹<\<kappa>×κ×κ×κ>›
  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> → o›
    and AOT_proj_enc :: ‹'a → ('a → o) → o›
  assumes AOT_sem_enc_denotes:
    ‹[v ⊨ «AOT_enc κ₁κ_n Π¬] ==> [v ⊨ κ₁...κ_n↓] ∧ [v ⊨ Π↓]›
  assumes AOT_sem_enc_proj_enc:
    ‹[v ⊨ «AOT_enc κ₁κ_n Π¬] =
 [v ⊨ Π↓ & «AOT_proj_enc κ₁κ_n (λ κ₁κ_n. «[Π]κ₁...κ_n¬)¬]›
  assumes AOT_sem_proj_enc_denotes:
    ‹[v ⊨ «AOT_proj_enc κ₁κ_n φ¬] ==> [v ⊨ κ₁...κ_n↓]›
  assumes AOT_sem_enc_nec:
    ‹[v ⊨ «AOT_enc κ₁κ_n Π¬] ==> [w ⊨ «AOT_enc κ₁κ_n Π¬]›
  assumes AOT_sem_proj_enc_nec:
    ‹[v ⊨ «AOT_proj_enc κ₁κ_n φ¬] ==> [w ⊨ «AOT_proj_enc κ₁κ_n φ¬]›
  assumes AOT_sem_universal_encoder:
    ‹∃ κ₁κ_n. [v ⊨ κ₁...κ_n↓] ∧ (∀ Π . [v ⊨ Π↓] ⟶ [v ⊨ «AOT_enc κ₁κ_n Π¬]) ∧
 (∀ φ . [v ⊨ [λz₁...z_n φ{z₁...z_n}]↓] ⟶ [v ⊨ «AOT_proj_enc κ₁κ_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 ⊨ Π'↓] ==> (∧ κ₀ . [v ⊨ [λx ♢[E!]x]κ₀] ==>
 (∧ w . [w ⊨ [Π']κ₀] = [w ⊨ [Π]κ₀])) ==> [v ⊨ κ[Π']]) ==>
 (∧ Π' . [v ⊨ Π'↓] ==> (∧ κ₀ . [v ⊨ [λx ♢[E!]x]κ₀] ==>
 (∧ w . [w ⊨ [Π']κ₀] = [w ⊨ [Π]κ₀])) ==> [v ⊨ κ'[Π']])›
      and AOT_sem_enc_indistinguishable_ex:
          ‹AOT_ExtendedModel ==>
 [v ⊨ [λx ¬♢[E!]x]κ] ==>
 [v ⊨ [λx ¬♢[E!]x]κ'] ==>
 (∧ Π' . [v ⊨ Π'↓] ==> (∧ w . [w ⊨ [Π']κ] = [w ⊨ [Π']κ'])) ==>
 [v ⊨ Π↓] ==>
 ∃ Π' . [v ⊨ Π'↓] ∧ [v ⊨ κ[Π']] ∧
 (∀ κ₀ . [v ⊨ [λx ♢[E!]x]κ₀] ⟶
 (∀ w . [w ⊨ [Π']κ₀] = [w ⊨ [Π]κ₀])) ==>
 ∃ Π' . [v ⊨ Π'↓] ∧ [v ⊨ κ'[Π']] ∧
 (∀ κ₀ . [v ⊨ [λx ♢[E!]x]κ₀] ⟶
 (∀ w . [w ⊨ [Π']κ₀] = [w ⊨ [Π]κ₀]))›

text‹We specify encoding to align with the model-construction of encoding.›
consts AOT_sem_enc_κ :: ‹κ → <\<kappa>> → o›
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=‹λ κ Π . ε_\o 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_κ :: ‹κ → <\<kappa>> → o› where
  ‹AOT_enc_κ ≡ AOT_sem_enc_κ›
definition AOT_proj_enc_κ :: ‹κ → (κ → o) → o› 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 Π Π' :: ‹<\<kappa>>›
  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 φ:: ‹<\<kappa>> → o›
  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 «ε_\o w . κυ z = κυ κ¬]↓]›
      unfolding AOT_sem_denotes AOT_model_lambda_denotes
      by (simp add: AOT_model_term_equiv_κ_def)
    hence "[v ⊨ [λz «ε_\<o> w . κυ z = κυ κ¬]κ] = [v ⊨ [λz «ε_\<o> 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 Π Π' :: ‹<\<kappa>>›
  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 ⊨ Π'↓] ==>
 (∧ κ₀ w. [v ⊨ [λx ♢[E!]x]κ₀] ==>
 [w ⊨ [Π']κ₀] = [w ⊨ [Π]κ₀]) ==>
 [v ⊨ κ[Π']]› for Π'
  assume Π_den': ‹[v ⊨ Π↓]›
  hence Π_den: ‹AOT_model_denotes Π›
    using AOT_sem_denotes by blast
  {
    fix Π' :: ‹<\<kappa>>›
    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 κ₀ :: κ and w
      assume ‹[v ⊨ [λx ♢[E!]x]κ₀]›
      hence ‹is_ψκ κ₀›
        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: ‹κ₀ = ψκ 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 ⊨ [Π']κ₀] = [w ⊨ [Π]κ₀]› 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]κ₀] ==>
 [w ⊨ [Π']κ₀] = [w ⊨ [Π]κ₀]› for κ₀ w
  {
    fix w and κ₀ :: κ
    assume 0: ‹∃w. AOT_model_concrete w κ₀›
    hence ‹[v ⊨ [λx ♢[E!]x]κ₀]›
      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 ⊨ [Π]κ₀]›
      using ord_indist by metis 
    hence ‹[w ⊨ «Rep_rel Π' κ₀¬] = [w ⊨ «Rep_rel Π κ₀¬]›
      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 Π Π' :: ‹<\<kappa>>›
  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 ⊨ κ[Π']] ∧
 (∀κ₀. [v ⊨ [λx ♢[E!]x]κ₀] ⟶
 (∀w. [w ⊨ [Π']κ₀] = [w ⊨ [Π]κ₀]))›
  then obtain Π' where
      Π'_den: ‹[v ⊨ Π'↓]› and
      Π'_enc: ‹[v ⊨ κ[Π']]› and
      Π'_prop: ‹∀κ₀. [v ⊨ [λx ♢[E!]x]κ₀] ⟶
 (∀w. [w ⊨ [Π']κ₀] = [w ⊨ [Π]κ₀])›
    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 κ₀) ==>
 [v ⊨ «Rep_rel Π' κ₀¬] = [v ⊨ «Rep_rel Π κ₀¬]› for κ₀ v
  proof -
    assume 0: ‹∃w. AOT_model_concrete w κ₀›
    hence ‹[v ⊨ [λx ♢[E!]x]κ₀]› 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 ⊨ [Π']κ₀] = [w ⊨ [Π]κ₀]› using Π'_prop by blast
    thus ‹[v ⊨ «Rep_rel Π' κ₀¬] = [v ⊨ «Rep_rel Π κ₀¬]›
      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]κ₀] ==>
 (∀w. [w ⊨ [Π'']κ₀] = [w ⊨ [Π]κ₀])› for κ₀
  proof -
    assume ‹[v ⊨ [λx ♢[E!]x]κ₀]›
    hence ‹∃w. AOT_model_concrete w κ₀›
      by (metis AOT_sem_concrete AOT_sem_dia AOT_sem_exe AOT_sem_lambda_beta)
    thus ‹∀w. [w ⊨ [Π'']κ₀] = [w ⊨ [Π]κ₀]›
      using Π''_prop
      by (metis AOT_sem_denotes AOT_sem_exe Π''_den Π_den)
  qed
  ultimately show ‹∃Π'. [v ⊨ Π'↓] ∧ [v ⊨ κ'[Π']] ∧
 (∀κ₀. [v ⊨ [λx ♢[E!]x]κ₀] ⟶
 (∀w. [w ⊨ [Π']κ₀] = [w ⊨ [Π]κ₀]))›
    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 → o) → o› where
  ‹AOT_proj_enc_prod ≡ λ (κ,κ') φ . «κ[λν «φ (ν,κ')¬] &
 «AOT_proj_enc κ' (λν. φ (κ,ν))¬¬›
definition AOT_enc_prod :: ‹'a×'b → <'a×'b> → o› where
  ‹AOT_enc_prod ≡ λ κ Π . «Π↓ & «AOT_proj_enc κ (λ κ₁'κ_n'. «[Π]κ₁'...κ_n'¬)¬¬›
instance proof
  show ‹[v ⊨ κ₁...κ_n[Π]] ==> [v ⊨ κ₁...κ_n↓] ∧ [v ⊨ Π↓]›
    for v and κ₁κ_n :: ‹'a×'b› and Π
    unfolding AOT_enc_prod_def
    apply (induct κ₁κ_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 ⊨ κ₁...κ_n[Π]] =
 [v ⊨ «Π¬↓ & «AOT_proj_enc κ₁κ_n (λ κ₁κ_n. «[Π]κ₁...κ_n¬)¬]›
    for v and κ₁κ_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 κ₁κ_n :: ‹'a×'b›
  show ‹[w ⊨ κ₁...κ_n[Π]]› if ‹[v ⊨ κ₁...κ_n[Π]]› for v w Π and κ₁κ_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 κ₁κ_n φ¬]› if ‹[v ⊨ «AOT_proj_enc κ₁κ_n φ¬]›
    for v w φ and κ₁κ_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 κ₁'κ_n' :: 'b where b_prop:
    ‹[v ⊨ κ₁'...κ_n'↓] ∧ (∀ φ . [v ⊨ [λν₁...ν_n «φ ν₁ν_n¬]↓] ⟶
 [v ⊨ «AOT_proj_enc κ₁'κ_n' φ¬])›
    using AOT_sem_universal_encoder by blast
  have ‹AOT_model_denotes «[λν₁...ν_n [«Π¬]ν₁...ν_n κ₁'...κ_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 «[λν₁...ν_n [«Π¬]κ ν₁...ν_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 ⊨ «(κ,κ₁'κ_n')¬↓]›
              and 2: ‹(∀ Π . [v ⊨ Π↓] ⟶ [v ⊨ κ κ₁'...κ_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 «[λz₁...z_n «φ (z₁z_n, κ₁'κ_n')¬]¬›
    if ‹AOT_model_denotes «[λz₁...z_m φ{z₁...z_m}]¬› for φ :: ‹'a×'b → o›
    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 «[λz₁...z_n «φ (κ, z₁z_n)¬]¬›
    if ‹AOT_model_denotes «[λz₁...z_m φ{z₁...z_m}]¬› for φ :: ‹'a×'b → o›
    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 ⊨ «(κ,κ₁'κ_n')¬↓] ∧ (∀ φ . [v ⊨ [λz₁...z_n φ{z₁...z_n}]↓] ⟶
 [v ⊨ «AOT_proj_enc (κ,κ₁'κ_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 ‹∃κ₁κ_n::'a×'b. [v ⊨ κ₁...κ_n↓] ∧ (∀ Π . [v ⊨ Π↓] ⟶ [v ⊨ κ₁...κ_n[Π]]) ∧
 (∀ φ . [v ⊨ [λz₁...z_n «φ z₁z_n¬]↓] ⟶
 [v ⊨ «AOT_proj_enc κ₁κ_n φ¬])›
    apply (rule exI[where x=‹(κ,κ₁'κ_n')›]) using 1 2 3 by blast
qed
end

text‹Sanity-check to verify that n-ary encoding follows.›
lemma ‹[v ⊨ κ₁κ₂[Π]] = [v ⊨ Π↓ & κ₁[λν [Π]νκ₂] & κ₂[λν [Π]κ₁ν]]›
  for κ₁ :: "'a::AOT_UnaryEnc" and κ₂ :: "'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 ⊨ κ₁κ₂κ₃[Π]] =
 [v ⊨ Π↓ & κ₁[λν [Π]νκ₂κ₃] & κ₂[λν [Π]κ₁νκ₃] & κ₃[λν [Π]κ₁κ₂ν]]›
  for κ₁ κ₂ κ₃ :: "'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 ⊨ α₁...α_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 → o) → 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 ⊨ [λν₁...ν_n φ{ν₁...ν_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 (λτ. «\Aφ{τ}¬)›
  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 (λκ₁κ_n :: 'b::AOT_κs.
 «[λν₁...ν_n φ{κ₁...κ_n,ν₁...ν_n}]«κs κ₁κ_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‹<\<kappa>> 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 ‹«(κ₁,κ₂)¬↓› shows ‹κ₁↓ & κ₂↓›
  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 ‹κ₁↓ & κ₂↓› shows ‹«(κ₁,κ₂)¬↓›
  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 Π' :: ‹<\<kappa>>›
        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 Π' :: ‹<\<kappa>>›
      assume Π_den: ‹[v ⊨ Π'↓]›
      assume 4: ‹[v ⊨ ∀z (O!z → ◻([Π']z ≡ [Π]z))]›
      {
        fix κ₀
        assume ‹[v ⊨ [λx ♢[E!]x]κ₀]›
        hence ‹[v ⊨ O!κ₀]›
          using AOT_sem_ordinary by metis
        moreover have ‹[v ⊨ κ₀↓]›
          using calculation by (simp add: AOT_sem_exe)
        ultimately have ‹[v ⊨ ◻([Π']κ₀ ≡ [Π]κ₀)]›
          using 4 by (auto simp: AOT_sem_forall AOT_sem_imp)
      } note 4 = this
      {
        fix Π'' :: ‹<\<kappa>>›
        assume ‹[v ⊨ Π''↓]›
        moreover assume ‹[w ⊨ [Π'']κ₀] = [w ⊨ [Π']κ₀]› if ‹[v ⊨ [λx ♢E!x]κ₀]› for κ₀ 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 Π' :: ‹<\<kappa>>›
        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 Π' :: ‹<\<kappa>>›
      assume Π_den: ‹[v ⊨ Π'↓]›
      assume 4: ‹[v ⊨ ∀z (O!z → ◻([Π']z ≡ [Π]z))]›
      {
        fix κ₀
        assume ‹[v ⊨ [λx ♢[E!]x]κ₀]›
        hence ‹[v ⊨ O!κ₀]›
          using AOT_sem_ordinary by metis
        moreover have ‹[v ⊨ κ₀↓]›
          using calculation by (simp add: AOT_sem_exe)
        ultimately have ‹[v ⊨ ◻([Π']κ₀ ≡ [Π]κ₀)]›
          using 4 by (auto simp: AOT_sem_forall AOT_sem_imp)
      } note 4 = this
      {
        fix Π'' :: ‹<\<kappa>>›
        assume ‹[v ⊨ Π''↓]›
        moreover assume ‹[w ⊨ [Π'']κ₀] = [w ⊨ [Π']κ₀]› if ‹[v ⊨ [λx ♢E!x]κ₀]› for w κ₀
        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 κ₀
        AOT_assume ‹[λx ♢[E!]x]κ₀›
        AOT_hence ‹◻([Π']κ₀ ≡ [Π]κ₀)›
          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]κ₀ → ◻([Π'']κ₀ ≡ [Π]κ₀)› and
          y_enc_Π'': ‹y[Π'']› for κ₀
        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
(*>*)