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[Π]]) ∧
                      (\<forall> \<phi> . [v \<Turnstile> [\<lambda>z\<^sub>1...z\<^sub>n \<guillemotleft>\<phi> z\<^sub>1z\<^sub>n\<guillemotright>]\<down>] \<longrightarrow>
                             [v \<Turnstile> \<guillemotleft>AOT_proj_enc \<kappa>\<^sub>1\<kappa>\<^sub>n \<phi>\<guillemotright>])\<close>
    apply (rule exI[where x=\<open>(\<kappa>,\<kappa>\<^sub>1'\<kappa>\<^sub>n')\<close>]) using 1 2 3 by blast
qed
end

text\<open>Sanity-check to verify that n-ary encoding follows.\<close>
lemma \<open>[v \<Turnstile> \<kappa>\<^sub>1\<kappa>\<^sub>2[\<Pi>]] = [v \<Turnstile> \<Pi>\<down> & \<kappa>\<^sub>1[\<lambda>\<nu> [\<Pi>]\<nu>\<kappa>\<^sub>2] & \<kappa>\<^sub>2[\<lambda>\<nu> [\<Pi>]\<kappa>\<^sub>1\<nu>]]\<close>
  for \<kappa>\<^sub>1 :: "'a::AOT_UnaryEnc" and \<kappa>\<^sub>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 \<open>[v \<Turnstile> \<kappa>\<^sub>1\<kappa>\<^sub>2\<kappa>\<^sub>3[\<Pi>]] =
       [v \<Turnstile> \<Pi>\<down> & \<kappa>\<^sub>1[\<lambda>\<nu> [\<Pi>]\<nu>\<kappa>\<^sub>2\<kappa>\<^sub>3] & \<kappa>\<^sub>2[\<lambda>\<nu> [\<Pi>]\<kappa>\<^sub>1\<nu>\<kappa>\<^sub>3] & \<kappa>\<^sub>3[\<lambda>\<nu> [\<Pi>]\<kappa>\<^sub>1\<kappa>\<^sub>2\<nu>]]\<close>
  for \<kappa>\<^sub>1 \<kappa>\<^sub>2 \<kappa>\<^sub>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: \<open>[v \<Turnstile> \<alpha>\<^sub>1...\<alpha>\<^sub>n\<down>]\<close>
  by induct simp

text\<open>Combine the introduced type classes and register them as
     type constraints for individual terms.\<close>
class AOT_\<kappa>s = AOT_IndividualTerm + AOT_RelationProjection + AOT_Enc
class AOT_\<kappa> = AOT_\<kappa>s + AOT_UnaryIndividualTerm +
  AOT_UnaryRelationProjection + AOT_UnaryEnc

instance \<kappa> :: AOT_\<kappa> by
 prod:(\<kappa> \kappas \<appa>s  standard

AOT_register_type_constraints
  : <open>_:AOT_\kappaclose <>_:\<>s\> and
:>:AOT_<kappa>s\close>

text\<open>We define semantic predicates to capture the conditions of cqt.2 (i.e.
     the base cases of denoting terms) on matrices of @{text \<lambda>}-expressions.\<close>
  :open(a:AOT_\kappa>s\Rightarrow><)\Rightarrow>bool\<close java.lang.StringIndexOutOfBoundsException: Index 114 out of bounds for length 114
  \<open>AOT_instance_of_cqt_2 \<equiv>
                                          AOT_model_term_equiv x y \<longrightarrow> \<phi> x = \<phi> y\<close>
definition AOT_instance_of_cqt_2_exe_arg :: \<open>('a::AOT_\<kappa>s \<Rightarrow> 'b::AOT_\<kappa>s) \<Rightarrow> subgoal
  \<open>AOT_instance_of_cqt_2_exe_arg \<equiv> \<lambda> \<phi> . \<forall> x y .
else.
      AOT_model_term_equiv (\<phi>valth =auto2_solve ' Thmcterm_of ' )

text\<open>@{text \<lambda>}-expressions with a matrix that satisfies our predicate denote.\<close>
java.lang.StringIndexOutOfBoundsException: Index 45 out of bounds for length 45
  \open>AOT_instance_of_cqt_2\<phi>\<>
  shows \<open>[v \<Turnstile> [\<lambda>\<nu>\<^
  using assms
  by is_goal_resolved prop then prop else

syntax AOT_instance_of_cqt_2 :: \<open>id_position \<Rightarrow> AOT_prop\<close>
  (\<open>INSTANCE'_OF'_CQT'_2'(_')\<close>)

\>Proveintroduction  for the  thatmatch thelanguage
     restrictions of the axiom.\<close>
named_theorems AOT_instance_of_cqt_2_intro
lemma AOT_instance_of_cqt_2_intros_const[AOT_instance_of_cqt_2_intro]:
  \<open>AOT_instance_of_cqt_2 (\<lambda>\<alpha>*java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
  new_varsf   java.lang.StringIndexOutOfBoundsException: Index 39 out of bounds for length 39
lemma AOT_instance_of_cqt_2_intros_not[AOT_instance_of_cqt_2_intro]:
  assumes \<open>AOT_instance_of_cqt_2 \<phi>\<close>
  shows \<open>AOT_instance_of_cqt_2 (\<lambda>\<tau>. \<guillemotleft>\<not>\<phi>{\<tau>}\<guillemotright>)\<close>
  using assms
 ,lifting)
lemma AOT_instance_of_cqt_2_intros_imp[AOT_instance_of_cqt_2_intro]:
  assumes \<open>AOT_instance_of_cqt_2 forall_elim
  |.implies_intr
  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 \<openjava.lang.StringIndexOutOfBoundsException: Index 45 out of bounds for length 45
  shows \<open>AOT_instance_of_cqt_2 (\   > .is_mem    elset ,
  using assms
  bylet
                 AOT_model_lambda_denotes AOT_sem_box)
lemma AOT_instance_of_cqt_2_intros_act[AOT_instance_of_cqt_2_intro]:
    java.lang.StringIndexOutOfBoundsException: Index 13 out of bounds for length 13
  shows \<open>AOT_instance_of_cqt_2 (\<lambda>\<tau>. \<guillemotleft>\<^bold>\<A>\<phi>{\<tau>}\<guillemotright>)\<close>
  using assms
  by (auto simp: AOT_instance_of_cqt_2_def. new_framejava.lang.StringIndexOutOfBoundsException: Index 71 out of bounds for length 71
                 AOT_model_lambda_denotes AOT_sem_act)
lemma AOT_instance_of_cqt_2_intros_diamond[AOT_instance_of_cqt_2_intro]:
  assumes \<open>AOT_instance_of_cqt_2    let
  shows \<open       c_vars   (.cterm_of ) java.lang.StringIndexOutOfBoundsException: Index 47 out of bounds for length 47
  using assms
  by (auto
                 AOT_model_lambda_denotes AOT_sem_dia)
lemma AOT_instance_of_cqt_2_intros_conj[AOT_instance_of_cqt_2_intro]:      val(vars, (s, C)  prop |> Thm.prems_of |> the_single
  assumes \<open>AOT_instance_of_cqt_2       context=ctxt, ..=Proof.goalstate
  shows \<open>AOT_instance_of_cqt_2 (\<lambda>\<tau>.end
  using assms
  by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes
                 AOT_model_lambda_denotes )
java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
 > <><close>and\open>AOT_instance_of_cqt_2\<psi\close
  shows \<open>AOT_instance_of_cqt_2 (\<lambda>\<tau>. \<guillemotleft>\<phi>{\<tau>} \<or> \<psi>{\tau>}<guillemotright>)\closejava.lang.StringIndexOutOfBoundsException: Index 132 out of bounds for length 132
  using assms
  by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes
                 funeq =
lemma AOT_instance_of_cqt_2_intros_equib
java.lang.StringIndexOutOfBoundsException: Index 7 out of bounds for length 7
 > \lambda><>. \guillemotleft\phi>{<tau> <equiv> <psi>{<tau>}<>)<>
  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 \<open>\<And> \<alpha> . AOT_instance_of_cqt_2 (\<Phi> \<alpha>)\<close>
  shows \<open>AOT_instance_of_cqt_2 (\<lambda>\<tau>. \<guillemotleft>\<forall>\<alpha> \<Phi>{\<alpha>,\<tau>}\<guillemotright>)\<close>
  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 \<open>\<And> \<alpha> . AOT_instance_of_cqt_2 (\<Phi> \<alpha>)\<close>
  shows \<open>AOT_instance_of_cqt_2 (\<lambda>\<tau>. \<guillemotleft>\<exists>\<alpha> \<Phi>{\<alpha>,\<tau>}\<guillemotright>)\<close>
  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]:
   \<open>AOT_instance_of_cqt_2_exe_arg (\<lambda>x. x)\<close>
  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]:
     \<open>AOT_instance_of_cqt_2_exe_arg (\<lambda>x. \<kappa>)\<close>
  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]:
   \<open>AOT_instance_of_cqt_2_exe_arg fst\<close>
  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]:
   \<open>AOT_instance_of_cqt_2_exe_arg snd\<close>
  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 \<open>AOT_instance_of_cqt_2_exe_arg \<phi>\<close> and \<open>AOT_instance_of_cqt_2_exe_arg \<psi>\<close>
  shows \<open>AOT_instance_of_cqt_2_exe_arg (\<lambda>\<tau>. Pair (\<phi> \<tau>) (\<psi> \<tau>))\<close>
  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 \<open>\<And>z :: 'a::AOT_\<kappa>. AOT_instance_of_cqt_2 (\<Phi> z)\<close>
  shows \<open>AOT_instance_of_cqt_2_exe_arg (\<lambda> \<kappa> :: 'b::AOT_\<kappa> . \<guillemotleft>\<^bold>\<iota>z(\<Phi>{z,\<kappa>})\<guillemotright>)\<close>
proof -
  have 0: \<open>\<And> \<kappa> \<kappa>'. AOT_model_denotes \<kappa> \<and> AOT_model_denotes \<kappa>' \<and>
                   AOT_model_term_equiv \<kappa> \<kappa>' \<Longrightarrow>
                   \<Phi> z \<kappa> = \<Phi> z \<kappa>'\<close> for z
    using assms
    unfolding AOT_instance_of_cqt_2_def
              AOT_sem_denotes AOT_model_lambda_denotes by force
  {
    fix \<kappa> \<kappa>'
    have \<open>\<guillemotleft>\<^bold>\<iota>z(\<Phi>{z,\<kappa>})\<guillemotright> = \<guillemotleft>\<^bold>\<iota>z(\<Phi>{z,\<kappa>'})\<guillemotright>\<close>
      if \<open>AOT_model_denotes \<kappa> \<and> AOT_model_denotes \<kappa>' \<and> AOT_model_term_equiv \<kappa> \<kappa>'\<close>
      using 0[OF that]
      by auto
    moreover have \<open>AOT_model_term_equiv x x\<close> for x :: \<open>'a::AOT_\<kappa>\<close>
      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 \<open>AOT_model_term_equiv \<guillemotleft>\<^bold>\<iota>z(\<Phi>{z,\<kappa>})\<guillemotright> \<guillemotleft>\<^bold>\<iota>z(\<Phi>{z,\<kappa>'})\<guillemotright>\<close>
      if \<open>AOT_model_denotes \<kappa> \<and> AOT_model_denotes \<kappa>' \<and> AOT_model_term_equiv \<kappa> \<kappa>'\<close>
      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 \<open>AOT_instance_of_cqt_2_exe_arg \<kappa>s\<close>
  shows \<open>AOT_instance_of_cqt_2 (\<lambda>x :: 'b::AOT_\<kappa>s. AOT_exe \<Pi> (\<kappa>s x))\<close>
  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 \<open>\<And> y . AOT_instance_of_cqt_2 (\<lambda>x. \<phi> x y)\<close>
      and \<open>AOT_instance_of_cqt_2_exe_arg \<kappa>s\<close>
    shows \<open>AOT_instance_of_cqt_2 (\<lambda>\<kappa>\<^sub>1\<kappa>\<^sub>n :: 'b::AOT_\<kappa>s.
              \<guillemotleft>[\<lambda>\<nu>\<^sub>1...\<nu>\<^sub>n \<phi>{\<kappa>\<^sub>1...\<kappa>\<^sub>n,\<nu>\<^sub>1...\<nu>\<^sub>n}]\<guillemotleft>\<kappa>s \<kappa>\<^sub>1\<kappa>\<^sub>n\<guillemotright>\<guillemotright>)\<close>
proof -
  {
    fix x y :: 'b
    assume \<open>AOT_model_denotes x\<close>
    moreover assume \<open>AOT_model_denotes y\<close>
    moreover assume \<open>AOT_model_term_equiv x y\<close>
    moreover have 1: \<open>\<phi> x = \<phi> y\<close>
      using assms calculation unfolding AOT_instance_of_cqt_2_def by blast
    ultimately have \<open>AOT_exe (AOT_lambda (\<phi> x)) (\<kappa>s x) =
                     AOT_exe (AOT_lambda (\<phi> y)) (\<kappa>s y)\<close>
      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 \<open>\<And> x . AOT_instance_of_cqt_2 (\<phi> x)\<close>
      and \<open>\<And> x . AOT_instance_of_cqt_2 (\<lambda> z . \<phi> z x)\<close>
  shows \<open>AOT_instance_of_cqt_2 (\<lambda>(x,y) . \<phi> x y)\<close>
  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\<open>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.\<close>
named_theorems AOT_instance_of_cqt_2_intro_next
definition AOT_instance_of_cqt_2_enc_arg :: \<open>('a::AOT_\<kappa>s \<Rightarrow> 'b::AOT_\<kappa>s) \<Rightarrow> bool\<close> where
  \<open>AOT_instance_of_cqt_2_enc_arg \<equiv> \<lambda> \<phi> . \<forall> x y z .
      AOT_model_denotes x \<and> AOT_model_denotes y \<and> AOT_model_term_equiv x y \<longrightarrow>
      AOT_enc (\<phi> x) z = AOT_enc (\<phi> y) z\<close>
definition AOT_instance_of_cqt_2_enc_rel :: \<open>('a::AOT_\<kappa>s \<Rightarrow> <'b::AOT_\<kappa>s>) \<Rightarrow> bool\<close> where
  \<open>AOT_instance_of_cqt_2_enc_rel \<equiv> \<lambda> \<phi> . \<forall> x y z .
      AOT_model_denotes x \<and> AOT_model_denotes y \<and> AOT_model_term_equiv x y \<longrightarrow>
      AOT_enc z (\<phi> x) = AOT_enc z (\<phi> y)\<close>
lemma AOT_instance_of_cqt_2_intros_enc[AOT_instance_of_cqt_2_intro_next]:
  assumes \<open>AOT_instance_of_cqt_2_enc_rel \<Pi>\<close> and \<open>AOT_instance_of_cqt_2_enc_arg \<kappa>s\<close>
  shows \<open>AOT_instance_of_cqt_2 (\<lambda>x . AOT_enc (\<kappa>s x) \<guillemotleft>[\<guillemotleft>\<Pi> x\<guillemotright>]\<guillemotright>)\<close>
  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]:
  \<open>AOT_instance_of_cqt_2_enc_arg (\<lambda>x. c)\<close>
  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 \<open>\<And>z :: 'a::AOT_\<kappa>. AOT_instance_of_cqt_2 (\<Phi> z)\<close>
  shows \<open>AOT_instance_of_cqt_2_enc_arg (\<lambda> \<kappa> :: 'b::AOT_\<kappa> . \<guillemotleft>\<^bold>\<iota>z(\<Phi>{z,\<kappa>})\<guillemotright>)\<close>
proof -
  have 0: \<open>\<And> \<kappa> \<kappa>'. AOT_model_denotes \<kappa> \<and> AOT_model_denotes \<kappa>' \<and>
                   AOT_model_term_equiv \<kappa> \<kappa>' \<Longrightarrow>
                   \<Phi> z \<kappa> = \<Phi> z \<kappa>'\<close> for z
    using assms
    unfolding AOT_instance_of_cqt_2_def
              AOT_sem_denotes AOT_model_lambda_denotes by force
  {
    fix \<kappa> \<kappa>'
    have \<open>\<guillemotleft>\<^bold>\<iota>z(\<Phi>{z,\<kappa>})\<guillemotright> = \<guillemotleft>\<^bold>\<iota>z(\<Phi>{z,\<kappa>'})\<guillemotright>\<close>
      if \<open>AOT_model_denotes \<kappa> \<and> AOT_model_denotes \<kappa>' \<and> AOT_model_term_equiv \<kappa> \<kappa>'\<close>
      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 \<open>\<And> \<kappa> . AOT_instance_of_cqt_2 (\<lambda>\<kappa>' :: 'b::AOT_\<kappa>s . \<phi> \<kappa> \<kappa>')\<close>
  assumes \<open>\<And> \<kappa>' . AOT_instance_of_cqt_2 (\<lambda>\<kappa> :: 'a::AOT_\<kappa>s . \<phi> \<kappa> \<kappa>')\<close>
  shows \<open>AOT_instance_of_cqt_2_enc_rel (\<lambda>\<kappa> :: 'a::AOT_\<kappa>s. AOT_lambda (\<lambda>\<kappa>'. \<phi> \<kappa> \<kappa>'))\<close>
proof -
  {
    fix x y :: 'a and z ::'b
    assume \<open>AOT_model_term_equiv x y\<close>
    moreover assume \<open>AOT_model_denotes x\<close>
    moreover assume \<open>AOT_model_denotes y\<close>
    ultimately have \<open>\<phi> x = \<phi> y\<close>
      using assms unfolding AOT_instance_of_cqt_2_def by blast
    hence \<open>AOT_enc z (AOT_lambda (\<phi> x)) = AOT_enc z (AOT_lambda (\<phi> y))\<close>
      by simp
  }
  thus ?thesis
    unfolding AOT_instance_of_cqt_2_enc_rel_def by auto
qed

text\<open>Further restrict unary individual variables to type @{typ \<kappa>} (rather
     than class @{class AOT_\<kappa>} only) and define being ordinary and being abstract.\<close>
AOT_register_type_constraints
  Individual: \<open>\<kappa>\<close> \<open>_::AOT_\<kappa>s\<close>

AOT_define AOT_ordinary :: \<open>\<Pi>\<close> (\<open>O!\<close>) \<open>O! =\<^sub>d\<^sub>f [\<lambda>x \<diamond>E!x]\<close>
declare AOT_ordinary[AOT del, AOT_defs del]
AOT_define AOT_abstract :: \<open>\<Pi>\<close> (\<open>A!\<close>) \<open>A! =\<^sub>d\<^sub>f [\<lambda>x \<not>\<diamond>E!x]\<close>
declare AOT_abstract[AOT del, AOT_defs del]

context AOT_meta_syntax
begin
notation AOT_ordinary (\<open>\<^bold>O\<^bold>!\<close>)
notation AOT_abstract (\<open>\<^bold>A\<^bold>!\<close>)
end
context AOT_no_meta_syntax
begin
no_notation AOT_ordinary (\<open>\<^bold>O\<^bold>!\<close>)
no_notation AOT_abstract (\<open>\<^bold>A\<^bold>!\<close>)
end

no_translations
  "_AOT_concrete" => "CONST AOT_term_of_var (CONST AOT_concrete)"
parse_translation\<open>
[(\<^syntax_const>\<open>_AOT_concrete\<close>, fn _ => fn [] =>
  Const (\<^const_name>\<open>AOT_term_of_var\<close>, dummyT)
  $ Const (\<^const_name>\<open>AOT_concrete\<close>, \<^typ>\<open><\<kappa>> AOT_var\<close>))]
\<close>

text\<open>Auxiliary lemmata.\<close>
lemma AOT_sem_ordinary: "\<guillemotleft>O!\<guillemotright> = \<guillemotleft>[\<lambda>x \<diamond>E!x]\<guillemotright>"
  using AOT_ordinary[THEN AOT_sem_id_def0E1] AOT_sem_ordinary_def_denotes
  by (auto simp: AOT_sem_eq)
lemma AOT_sem_abstract: "\<guillemotleft>A!\<guillemotright> = \<guillemotleft>[\<lambda>x \<not>\<diamond>E!x]\<guillemotright>"
  using AOT_abstract[THEN AOT_sem_id_def0E1]  AOT_sem_abstract_def_denotes
  by (auto simp: AOT_sem_eq)
lemma AOT_sem_ordinary_denotes: \<open>[w \<Turnstile> O!\<down>]\<close>
  by (simp add: AOT_sem_ordinary AOT_sem_ordinary_def_denotes)
lemma AOT_meta_abstract_denotes: \<open>[w \<Turnstile> A!\<down>]\<close>
  by (simp add: AOT_sem_abstract AOT_sem_abstract_def_denotes)
lemma AOT_model_abstract_\<alpha>\<kappa>: \<open>\<exists> a . \<kappa> = \<alpha>\<kappa> a\<close> if \<open>[v \<Turnstile> A!\<kappa>]\<close>
  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_\<omega>_concrete_in_some_world AOT_model_concrete_\<kappa>.simps(1)
            AOT_model_denotes_\<kappa>_def AOT_sem_denotes AOT_sem_exe \<kappa>.exhaust_disc
            is_\<alpha>\<kappa>_def is_\<omega>\<kappa>_def that)
lemma AOT_model_ordinary_\<omega>\<kappa>: \<open>\<exists> a . \<kappa> = \<omega>\<kappa> a\<close> if \<open>[v \<Turnstile> O!\<kappa>]\<close>
  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_\<kappa>.simps(2) AOT_model_concrete_\<kappa>.simps(3)
            \<kappa>.exhaust_disc is_\<alpha>\<kappa>_def is_\<omega>\<kappa>_def is_null\<kappa>_def)
lemma AOT_model_\<omega>\<kappa>_ordinary: \<open>[v \<Turnstile> O!\<guillemotleft>\<omega>\<kappa> x\<guillemotright>]\<close>
  by (metis AOT_model_abstract_\<alpha>\<kappa> AOT_model_denotes_\<kappa>_def AOT_sem_abstract
            AOT_sem_denotes AOT_sem_ind_eq AOT_sem_ordinary \<kappa>.disc(7) \<kappa>.distinct(1))
lemma AOT_model_\<alpha>\<kappa>_ordinary: \<open>[v \<Turnstile> A!\<guillemotleft>\<alpha>\<kappa> x\<guillemotright>]\<close>
  by (metis AOT_model_denotes_\<kappa>_def AOT_model_ordinary_\<omega>\<kappa> AOT_sem_abstract
            AOT_sem_denotes AOT_sem_ind_eq AOT_sem_ordinary \<kappa>.disc(8) \<kappa>.distinct(1))
AOT_theorem prod_denotesE: assumes \<open>\<guillemotleft>(\<kappa>\<^sub>1,\<kappa>\<^sub>2)\<guillemotright>\<down>\<close> shows \<open>\<kappa>\<^sub>1\<down> & \<kappa>\<^sub>2\<down>\<close>
  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 \<open>\<kappa>\<^sub>1\<down> & \<kappa>\<^sub>2\<down>\<close> shows \<open>\<guillemotleft>(\<kappa>\<^sub>1,\<kappa>\<^sub>2)\<guillemotright>\<down>\<close>
  using assms by (simp add: AOT_sem_denotes AOT_sem_conj AOT_model_denotes_prod_def)
declare prod_denotesI[AOT del]


text\<open>Prepare the derivation of the additional axioms that are validated by
     our extended models.\<close>
locale AOT_ExtendedModel =
  assumes AOT_ExtendedModel: \<open>AOT_ExtendedModel\<close>
begin
lemma AOT_sem_indistinguishable_ord_enc_all:
  assumes \<Pi>_den: \<open>[v \<Turnstile> \<Pi>\<down>]\<close>
  assumes Ax: \<open>[v \<Turnstile> A!x]\<close>
  assumes Ay: \<open>[v \<Turnstile> A!y]\<close>
  assumes indist: \<open>[v \<Turnstile> \<forall>F \<box>([F]x \<equiv> [F]y)]\<close>
  shows
  \<open>[v \<Turnstile> \<forall>G(\<forall>z(O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) \<rightarrow> x[G])] =
   [v \<Turnstile> \<forall>G(\<forall>z(O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) \<rightarrow> y[G])]\<close>
proof -
    have 0: \<open>[v \<Turnstile> [\<lambda>x \<not>\<diamond>[E!]x]x]\<close>
      using Ax by (simp add: AOT_sem_abstract)
    have 1: \<open>[v \<Turnstile> [\<lambda>x \<not>\<diamond>[E!]x]y]\<close>
      using Ay by (simp add: AOT_sem_abstract)
    {
      assume \<open>[v \<Turnstile> \<forall>G(\<forall>z (O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) \<rightarrow> x[G])]\<close>
      hence 3: \<open>[v \<Turnstile> \<forall>G(\<forall>z([\<lambda>x \<diamond>[E!]x]z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) \<rightarrow> x[G])]\<close>
        by (simp add: AOT_sem_ordinary)
      {
        fix \<Pi>' :: \<open><\<kappa>>\<close>
        assume 1: \<open>[v \<Turnstile> \<Pi>'\<down>]\<close>
        assume 2: \<open>[v \<Turnstile> [\<lambda>x \<diamond>[E!]x]z \<rightarrow> \<box>([\<Pi>']z \<equiv> [\<Pi>]z)]\<close> for z
        have \<open>[v \<Turnstile> x[\<Pi>']]\<close>
          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 \<Pi>' :: \<open><\<kappa>>\<close>
      assume \<Pi>_den: \<open>[v \<Turnstile> \<Pi>'\<down>]\<close>
      assume 4: \<open>[v \<Turnstile> \<forall>z (O!z \<rightarrow> \<box>([\<Pi>']z \<equiv> [\<Pi>]z))]\<close>
      {
        fix \<kappa>\<^sub>0
        assume \<open>[v \<Turnstile> [\<lambda>x \<diamond>[E!]x]\<kappa>\<^sub>0]\<close>
        hence \<open>[v \<Turnstile> O!\<kappa>\<^sub>0]\<close>
          using AOT_sem_ordinary by metis
        moreover have \<open>[v \<Turnstile> \<kappa>\<^sub>0\<down>]\<close>
          using calculation by (simp add: AOT_sem_exe)
        ultimately have \<open>[v \<Turnstile> \<box>([\<Pi>']\<kappa>\<^sub>0 \<equiv> [\<Pi>]\<kappa>\<^sub>0)]\<close>
          using 4 by (auto simp: AOT_sem_forall AOT_sem_imp)
      } note 4 = this
      {
        fix \<Pi>'' :: \<open><\<kappa>>\<close>
        assume \<open>[v \<Turnstile> \<Pi>''\<down>]\<close>
        moreover assume \<open>[w \<Turnstile> [\<Pi>'']\<kappa>\<^sub>0] = [w \<Turnstile> [\<Pi>']\<kappa>\<^sub>0]\<close> if \<open>[v \<Turnstile> [\<lambda>x \<diamond>E!x]\<kappa>\<^sub>0]\<close> for \<kappa>\<^sub>0 w
        ultimately have 5: \<open>[v \<Turnstile> x[\<Pi>'']]\<close>
          using 4 3
          by (auto simp: AOT_sem_imp AOT_sem_equiv AOT_sem_box)
      } note 5 = this
      have \<open>[v \<Turnstile> y[\<Pi>']]\<close>
        apply (rule AOT_sem_enc_indistinguishable_all[OF AOT_ExtendedModel])
        apply (fact 0)
        by (auto simp: 5 0 1 \<Pi>_den indist[simplified AOT_sem_forall
                       AOT_sem_box AOT_sem_equiv])
    }
    moreover {
    {
      assume \<open>[v \<Turnstile> \<forall>G(\<forall>z (O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) \<rightarrow> y[G])]\<close>
      hence 3: \<open>[v \<Turnstile> \<forall>G(\<forall>z ([\<lambda>x \<diamond>[E!]x]z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) \<rightarrow> y[G])]\<close>
        by (simp add: AOT_sem_ordinary)
      {
        fix \<Pi>' :: \<open><\<kappa>>\<close>
        assume 1: \<open>[v \<Turnstile> \<Pi>'\<down>]\<close>
        assume 2: \<open>[v \<Turnstile> [\<lambda>x \<diamond>[E!]x]z \<rightarrow> \<box>([\<Pi>']z \<equiv> [\<Pi>]z)]\<close> for z
        have \<open>[v \<Turnstile> y[\<Pi>']]\<close>
          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 \<Pi>' :: \<open><\<kappa>>\<close>
      assume \<Pi>_den: \<open>[v \<Turnstile> \<Pi>'\<down>]\<close>
      assume 4: \<open>[v \<Turnstile> \<forall>z (O!z \<rightarrow> \<box>([\<Pi>']z \<equiv> [\<Pi>]z))]\<close>
      {
        fix \<kappa>\<^sub>0
        assume \<open>[v \<Turnstile> [\<lambda>x \<diamond>[E!]x]\<kappa>\<^sub>0]\<close>
        hence \<open>[v \<Turnstile> O!\<kappa>\<^sub>0]\<close>
          using AOT_sem_ordinary by metis
        moreover have \<open>[v \<Turnstile> \<kappa>\<^sub>0\<down>]\<close>
          using calculation by (simp add: AOT_sem_exe)
        ultimately have \<open>[v \<Turnstile> \<box>([\<Pi>']\<kappa>\<^sub>0 \<equiv> [\<Pi>]\<kappa>\<^sub>0)]\<close>
          using 4 by (auto simp: AOT_sem_forall AOT_sem_imp)
      } note 4 = this
      {
        fix \<Pi>'' :: \<open><\<kappa>>\<close>
        assume \<open>[v \<Turnstile> \<Pi>''\<down>]\<close>
        moreover assume \<open>[w \<Turnstile> [\<Pi>'']\<kappa>\<^sub>0] = [w \<Turnstile> [\<Pi>']\<kappa>\<^sub>0]\<close> if \<open>[v \<Turnstile> [\<lambda>x \<diamond>E!x]\<kappa>\<^sub>0]\<close> for w \<kappa>\<^sub>0
        ultimately have \<open>[v \<Turnstile> y[\<Pi>'']]\<close>
          using 3 4 by (auto simp: AOT_sem_imp AOT_sem_equiv AOT_sem_box)
      } note 5 = this
      have \<open>[v \<Turnstile> x[\<Pi>']]\<close>
        apply (rule AOT_sem_enc_indistinguishable_all[OF AOT_ExtendedModel])
              apply (fact 1)
        by (auto simp: 5 0 1 \<Pi>_den indist[simplified AOT_sem_forall
                       AOT_sem_box AOT_sem_equiv])
    }
  }
  ultimately show \<open>[v \<Turnstile> \<forall>G (\<forall>z (O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) \<rightarrow> x[G])] =
        [v \<Turnstile> \<forall>G (\<forall>z (O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) \<rightarrow> y[G])]\<close>
    by (auto simp: AOT_sem_forall AOT_sem_imp)
qed

lemma AOT_sem_indistinguishable_ord_enc_ex:
  assumes \<Pi>_den: \<open>[v \<Turnstile> \<Pi>\<down>]\<close>
  assumes Ax: \<open>[v \<Turnstile> A!x]\<close>
  assumes Ay: \<open>[v \<Turnstile> A!y]\<close>
  assumes indist: \<open>[v \<Turnstile> \<forall>F \<box>([F]x \<equiv> [F]y)]\<close>
  shows \<open>[v \<Turnstile> \<exists>G(\<forall>z (O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) &an> x[G])] =
         [v \<Turnstile> \<exists>G(\<forall>z(O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) & y[G])]\<close>
proof -
  have Aux: \<open>[v \<Turnstile> [\<lambda>x \<diamond>[E!]x]\<kappa>] = ([v \<Turnstile> [\<lambda>x \<diamond>[E!]x]\<kappa>] \<and> [v \<Turnstile> \<kappa>\<down>])\<close> for v \<kappa>
    using AOT_sem_exe by blast
  AOT_modally_strict {
    fix x y
    AOT_assume \<Pi>_den: \<open>[\<Pi>]\<down>\<close>
    AOT_assume 2: \<open>\<forall>F \<box>([F]x \<equiv> [F]y)\<close>
    AOT_assume \<open>A!x\<close>
    AOT_hence 0: \<open>[\<lambda>x \<not>\<diamond>[E!]x]x\<close>
      by (simp add: AOT_sem_abstract)
    AOT_assume \<open>A!y\<close>
    AOT_hence 1: \<open>[\<lambda>x \<not>\<diamond>[E!]x]y\<close>
      by (simp add: AOT_sem_abstract)
    {
      AOT_assume \<open>\<exists>G(\<forall>z (O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) & x[G])\<close>
      then AOT_obtain \<Pi>'
        where \<Pi>'_den: \<open>\<Pi>'\<down>\<close>
          and \<Pi>'_indist: \<open>\<forall>z (O!z \<rightarrow> \<box>([\<Pi>']z \<equiv> [\<Pi>]z))\<close>
          and x_enc_\<Pi>': \<open>x[\<Pi>']\<close>
        by (meson AOT_sem_conj AOT_sem_exists)
      {
        fix \<kappa>\<^sub>0
        AOT_assume \<open>[\<lambda>x \<diamond>[E!]x]\<kappa>\<^sub>0\<close>
        AOT_hence \<open>\<box>([\<Pi>']\<kappa>\<^sub>0 \<equiv> [\<Pi>]\<kappa>\<^sub>0)\<close>
          using \<Pi>'_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 \<open>\<forall>z ([\<lambda>x \<diamond>[E!]x]z \<rightarrow> \<box>([\<Pi>']z \<equiv> [\<Pi>]z))\<close>
        using \<Pi>'_indist by (simp add: AOT_sem_ordinary)
      AOT_obtain \<Pi>'' where
          \<Pi>''_den: \<open>\<Pi>''\<down>\<close> and
          \<Pi>''_indist: \<open>[\<lambda>x \<diamond>[E!]x]\<kappa>\<^sub>0 \<rightarrow> \<box>([\<Pi>'']\<kappa>\<^sub>0 \<equiv> [\<Pi>]\<kappa>\<^sub>0)\<close> and
          y_enc_\<Pi>'': \<open>y[\<Pi>'']\<close> for \<kappa>\<^sub>0
        using AOT_sem_enc_indistinguishable_ex[OF AOT_ExtendedModel,
                OF 0, OF 1, rotated, OF \<Pi>_den,
                OF exI[where x=\<Pi>'], OF conjI, OF \<Pi>'_den, OF conjI,
                OF x_enc_\<Pi>', 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 \<open>\<Pi>''\<down>\<close>
            and \<open>\<forall>x ([\<lambda>x \<diamond>[E!]x]x \<rightarrow> \<box>([\<Pi>'']x \<equiv> [\<Pi>]x))\<close>
            and \<open>y[\<Pi>'']\<close>
          apply (simp add: \<Pi>''_den)
          apply (simp add: AOT_sem_forall \<Pi>''_indist)
          by (simp add: y_enc_\<Pi>'')
      } note 2 = this
      AOT_have \<open>\<exists>G(\<forall>z (O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) & y[G])\<close>
        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 \<Pi>_den: \<open>[\<Pi>]\<down>\<close>
      moreover AOT_assume \<open>\<forall>F \<box>([F]x \<equiv> [F]y)\<close>
      moreover AOT_have \<open>\<forall>F \<box>([F]y \<equiv> [F]x)\<close>
        using calculation(2)
        by (auto simp: AOT_sem_forall AOT_sem_box AOT_sem_equiv)
      moreover AOT_assume \<open>A!x\<close>
      moreover AOT_assume \<open>A!y\<close>
      ultimately AOT_have \<open>\<exists>G (\<forall>z (O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) &pan> x[G]) \<equiv>
                           \<exists>G (\<forall>z (O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) & y[G])\<close>
        using 0 by (auto simp: AOT_sem_equiv)
    }
    have 1: \<open>[v \<Turnstile> \<forall>F \<box>([F]y \<equiv> [F]x)]\<close>
 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)
 }
 
 


 
   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
(*>*)