Theory AOT_semantics

1(*<*)
2theory AOT_semantics
3  imports AOT_syntax
4begin
5(*>*)
6
7section‹Abstract Semantics for AOT›
8
9specification(AOT_denotes)
10  ― ‹Relate object level denoting to meta-denoting. AOT's definitions of
11      denoting will become derivable at each type.›
12  AOT_sem_denotes: ‹[w ⊨ τ↓] = AOT_model_denotes τ›
13  by (rule exI[where x=‹λ τ . ε⇩_𝗈 w . AOT_model_denotes τ›])
14     (simp add: AOT_model_proposition_choice_simp)
15
16lemma AOT_sem_var_induct[induct type: AOT_var]:
17  assumes AOT_denoting_term_case: ‹⋀ τ . [v ⊨ τ↓] ⟹ [v ⊨ φ{τ}]›
18  shows ‹[v ⊨ φ{α}]›
19  by (simp add: AOT_denoting_term_case AOT_sem_denotes AOT_term_of_var)
20
21text‹\linelabel{AOT_imp_spec}›
22specification(AOT_imp)
23  AOT_sem_imp: ‹[w ⊨ φ → ψ] = ([w ⊨ φ] ⟶ [w ⊨ ψ])›
24  by (rule exI[where x=‹λ φ ψ . ε⇩_𝗈 w . ([w ⊨ φ] ⟶ [w ⊨ ψ])›])
25    (simp add: AOT_model_proposition_choice_simp)
26
27specification(AOT_not)
28  AOT_sem_not: ‹[w ⊨ ¬φ] = (¬[w ⊨ φ])›
29  by (rule exI[where x=‹λ φ . ε⇩_𝗈 w . ¬[w ⊨ φ]›])
30     (simp add: AOT_model_proposition_choice_simp)
31
32text‹\linelabel{AOT_box_spec}›
33specification(AOT_box)
34  AOT_sem_box: ‹[w ⊨ □φ] = (∀ w . [w ⊨ φ])›
35  by (rule exI[where x=‹λ φ . ε⇩_𝗈 w . ∀ w . [w ⊨ φ]›])
36     (simp add: AOT_model_proposition_choice_simp)
37
38text‹\linelabel{AOT_act_spec}›
39specification(AOT_act)
40  AOT_sem_act: ‹[w ⊨ ❙𝒜φ] = [w⇩₀ ⊨ φ]›
41  by (rule exI[where x=‹λ φ . ε⇩_𝗈 w . [w⇩₀ ⊨ φ]›])
42     (simp add: AOT_model_proposition_choice_simp)
43
44text‹Derived semantics for basic defined connectives.›
45lemma AOT_sem_conj: ‹[w ⊨ φ & ψ] = ([w ⊨ φ] ∧ [w ⊨ ψ])›
46  using AOT_conj AOT_model_equiv_def AOT_sem_imp AOT_sem_not by auto
47lemma AOT_sem_equiv: ‹[w ⊨ φ ≡ ψ] = ([w ⊨ φ] = [w ⊨ ψ])›
48  using AOT_equiv AOT_sem_conj AOT_model_equiv_def AOT_sem_imp by auto
49lemma AOT_sem_disj: ‹[w ⊨ φ ∨ ψ] = ([w ⊨ φ] ∨ [w ⊨ ψ])›
50  using AOT_disj AOT_model_equiv_def AOT_sem_imp AOT_sem_not by auto
51lemma AOT_sem_dia: ‹[w ⊨ ◇φ] = (∃ w . [w ⊨ φ])›
52  using AOT_dia AOT_sem_box AOT_model_equiv_def AOT_sem_not by auto
53
54specification(AOT_forall)
55  AOT_sem_forall: ‹[w ⊨ ∀α φ{α}] = (∀ τ . [w ⊨ τ↓] ⟶ [w ⊨ φ{τ}])›
56  by (rule exI[where x=‹λ op . ε⇩_𝗈 w . ∀ τ . [w ⊨ τ↓] ⟶ [w ⊨ «op τ»]›])
57     (simp add: AOT_model_proposition_choice_simp)
58
59lemma AOT_sem_exists: ‹[w ⊨ ∃α φ{α}] = (∃ τ . [w ⊨ τ↓] ∧ [w ⊨ φ{τ}])›
60  unfolding AOT_exists[unfolded AOT_model_equiv_def, THEN spec]
61  by (simp add: AOT_sem_forall AOT_sem_not)
62
63text‹\linelabel{AOT_eq_spec}›
64specification(AOT_eq)
65  ― ‹Relate identity to denoting identity in the meta-logic. AOT's definitions
66      of identity will become derivable at each type.›
67  AOT_sem_eq: ‹[w ⊨ τ = τ'] = ([w ⊨ τ↓] ∧ [w ⊨ τ'↓] ∧ τ = τ')›
68  by (rule exI[where x=‹λ τ τ' . ε⇩_𝗈 w . [w ⊨ τ↓] ∧ [w ⊨ τ'↓] ∧ τ = τ'›])
69     (simp add: AOT_model_proposition_choice_simp)
70
71text‹\linelabel{AOT_desc_spec}›
72specification(AOT_desc)
73  ― ‹Descriptions denote, if there is a unique denoting object satisfying the
74      matrix in the actual world.›
75  AOT_sem_desc_denotes: ‹[w ⊨ ❙ιx(φ{x})↓] = (∃! κ . [w⇩₀ ⊨ κ↓] ∧ [w⇩₀ ⊨ φ{κ}])›
76  ― ‹Denoting descriptions satisfy their matrix in the actual world.›
77  AOT_sem_desc_prop: ‹[w ⊨ ❙ιx(φ{x})↓] ⟹ [w⇩₀ ⊨ φ{❙ιx(φ{x})}]›
78  ― ‹Uniqueness of denoting descriptions.›
79  AOT_sem_desc_unique: ‹[w ⊨ ❙ιx(φ{x})↓] ⟹ [w ⊨ κ↓] ⟹ [w⇩₀ ⊨ φ{κ}] ⟹
80                        [w ⊨ ❙ιx(φ{x}) = κ]›
81proof -
82  have ‹∃x::'a . ¬AOT_model_denotes x›
83    using AOT_model_nondenoting_ex
84    by blast
85  text‹Note that we may choose a distinct non-denoting object for each matrix.
86       We do this explicitly merely to convince ourselves that our specification
87       can still be satisfied.›
88  then obtain nondenoting :: ‹('a ⇒ 𝗈) ⇒ 'a› where
89    nondenoting: ‹∀ φ . ¬AOT_model_denotes (nondenoting φ)›
90    by fast
91  define desc where
92    ‹desc = (λ φ . if (∃! κ . [w⇩₀ ⊨ κ↓] ∧ [w⇩₀ ⊨ φ{κ}])
93                   then (THE κ . [w⇩₀ ⊨ κ↓] ∧ [w⇩₀ ⊨ φ{κ}])
94                   else nondenoting φ)›
95  {
96    fix φ :: ‹'a ⇒ 𝗈›
97    assume ex1: ‹∃! κ . [w⇩₀ ⊨ κ↓] ∧ [w⇩₀ ⊨ φ{κ}]›
98    then obtain κ where x_prop: "[w⇩₀ ⊨ κ↓] ∧ [w⇩₀ ⊨ φ{κ}]"
99      unfolding AOT_sem_denotes by blast
100    moreover have "(desc φ) = κ"
101      unfolding desc_def using x_prop ex1 by fastforce
102    ultimately have "[w⇩₀ ⊨ «desc φ»↓] ∧ [w⇩₀ ⊨ «φ (desc φ)»]"
103      by blast
104  } note 1 = this
105  moreover {
106    fix φ :: ‹'a ⇒ 𝗈›
107    assume nex1: ‹∄! κ . [w⇩₀ ⊨ κ↓] ∧ [w⇩₀ ⊨ φ{κ}]›
108    hence "(desc φ) = nondenoting φ" by (simp add: desc_def AOT_sem_denotes)
109    hence "[w ⊨ ¬«desc φ»↓]" for w
110      by (simp add: AOT_sem_denotes nondenoting AOT_sem_not)
111  }
112  ultimately have desc_denotes_simp:
113    ‹[w ⊨ «desc φ»↓] = (∃! κ . [w⇩₀ ⊨ κ↓] ∧ [w⇩₀ ⊨ φ{κ}])› for φ w
114    by (simp add: AOT_sem_denotes desc_def nondenoting)
115  have ‹(∀φ w. [w ⊨ «desc φ»↓] = (∃!κ. [w⇩₀ ⊨ κ↓] ∧ [w⇩₀ ⊨ φ{κ}])) ∧
116    (∀φ w. [w ⊨ «desc φ»↓] ⟶ [w⇩₀ ⊨ «φ (desc φ)»]) ∧
117    (∀φ w κ. [w ⊨ «desc φ»↓] ⟶ [w ⊨ κ↓] ⟶ [w⇩₀ ⊨ φ{κ}] ⟶
118             [w ⊨ «desc φ» = κ])›
119    by (insert 1; auto simp: desc_denotes_simp AOT_sem_eq AOT_sem_denotes
120                             desc_def nondenoting)
121  thus ?thesis
122    by (safe intro!: exI[where x=desc]; presburger)
123qed
124
125text‹\linelabel{AOT_exe_lambda_spec}›
126specification(AOT_exe AOT_lambda)
127  ― ‹Truth conditions of exemplification formulas.›
128  AOT_sem_exe: ‹[w ⊨ [Π]κ⇩₁...κ⇩_n] = ([w ⊨ Π↓] ∧ [w ⊨ κ⇩₁...κ⇩_n↓] ∧
129                                     [w ⊨ «Rep_rel Π κ⇩₁κ⇩_n»])›
130  ― ‹\eta-conversion for denoting terms; equivalent to AOT's axiom›
131  AOT_sem_lambda_eta: ‹[w ⊨ Π↓] ⟹ [w ⊨ [λν⇩₁...ν⇩_n [Π]ν⇩₁...ν⇩_n] = Π]›
132  ― ‹\beta-conversion; equivalent to AOT's axiom›
133  AOT_sem_lambda_beta: ‹[w ⊨ [λν⇩₁...ν⇩_n φ{ν⇩₁...ν⇩_n}]↓] ⟹ [w ⊨ κ⇩₁...κ⇩_n↓] ⟹
134                        [w ⊨ [λν⇩₁...ν⇩_n φ{ν⇩₁...ν⇩_n}]κ⇩₁...κ⇩_n] = [w ⊨ φ{κ⇩₁...κ⇩_n}]›
135  ― ‹Necessary and sufficient conditions for relations to denote. Equivalent
136      to a theorem of AOT and used to derive the base cases of denoting relations
137      (cqt.2).›
138  AOT_sem_lambda_denotes: ‹[w ⊨ [λν⇩₁...ν⇩_n φ{ν⇩₁...ν⇩_n}]↓] =
139    (∀ v κ⇩₁κ⇩_n κ⇩₁'κ⇩_n' . [v ⊨ κ⇩₁...κ⇩_n↓] ∧ [v ⊨ κ⇩₁'...κ⇩_n'↓] ∧
140        (∀ Π v . [v ⊨ Π↓] ⟶ [v ⊨ [Π]κ⇩₁...κ⇩_n] = [v ⊨ [Π]κ⇩₁'...κ⇩_n']) ⟶
141                 [v ⊨ φ{κ⇩₁...κ⇩_n}] = [v ⊨ φ{κ⇩₁'...κ⇩_n'}])›
142  ― ‹Equivalent to AOT's coexistence axiom.›
143  AOT_sem_lambda_coex: ‹[w ⊨ [λν⇩₁...ν⇩_n φ{ν⇩₁...ν⇩_n}]↓] ⟹
144    (∀ w κ⇩₁κ⇩_n . [w ⊨ κ⇩₁...κ⇩_n↓] ⟶ [w ⊨ φ{κ⇩₁...κ⇩_n}] = [w ⊨ ψ{κ⇩₁...κ⇩_n}]) ⟹
145    [w ⊨ [λν⇩₁...ν⇩_n ψ{ν⇩₁...ν⇩_n}]↓]›
146  ― ‹Only the unary case of the following should hold, but our specification
147      has to range over all types. We might move @{const AOT_exe} and
148      @{const AOT_lambda} to type classes in the future to solve this.›
149  AOT_sem_lambda_eq_prop_eq: ‹«[λν⇩₁...ν⇩_n φ]» = «[λν⇩₁...ν⇩_n ψ]» ⟹ φ = ψ›
150  ― ‹The following is solely required for validating n-ary relation identity
151      and has the danger of implying artifactual theorems. Possibly avoidable
152      by moving @{const AOT_exe} and @{const AOT_lambda} to type classes.›
153  AOT_sem_exe_denoting: ‹[w ⊨ Π↓] ⟹ AOT_exe Π κs = Rep_rel Π κs›
154  ― ‹The following is required for validating the base cases of denoting
155      relations (cqt.2). A version of this meta-logical identity will
156      become derivable in future versions of AOT, so this will ultimately not
157      result in artifactual theorems.›
158  AOT_sem_exe_equiv: ‹AOT_model_term_equiv x y ⟹ AOT_exe Π x = AOT_exe Π y›
159proof -
160  have ‹∃ x :: <'a> . ¬AOT_model_denotes x›
161    by (rule exI[where x=‹Abs_rel (λ x . ε⇩_𝗈 w. True)›])
162       (meson AOT_model_denotes_rel.abs_eq AOT_model_nondenoting_ex
163              AOT_model_proposition_choice_simp)
164  define exe :: ‹<'a> ⇒ 'a ⇒ 𝗈› where
165    ‹exe ≡ λ Π κs . if AOT_model_denotes Π
166                     then Rep_rel Π κs
167                     else (ε⇩_𝗈 w . False)›
168  define lambda :: ‹('a⇒𝗈) ⇒ <'a>› where
169    ‹lambda ≡ λ φ . if AOT_model_denotes (Abs_rel φ)
170      then (Abs_rel φ)
171      else
172        if (∀ κ κ' w . (AOT_model_denotes κ ∧ AOT_model_term_equiv κ κ') ⟶
173                       [w ⊨ «φ κ»] = [w ⊨ «φ κ'»])
174        then
175          Abs_rel (fix_irregular (λ x . if AOT_model_denotes x
176                                        then φ (SOME y . AOT_model_term_equiv x y)
177                                        else  (ε⇩_𝗈 w . False)))
178        else 
179          Abs_rel φ›
180  have fix_irregular_denoting_simp[simp]:
181    ‹fix_irregular (λx. if AOT_model_denotes x then φ x else ψ x) κ = φ κ›
182    if ‹AOT_model_denotes κ›
183    for κ :: 'a and φ ψ
184    by (simp add: that fix_irregular_denoting)
185  have denoting_eps_cong[cong]:
186    ‹[w ⊨ «φ (Eps (AOT_model_term_equiv κ))»] = [w ⊨ «φ κ»]›
187    if ‹AOT_model_denotes κ›
188    and ‹∀ κ κ'. AOT_model_denotes κ ∧ AOT_model_term_equiv κ κ' ⟶
189                 (∀w. [w ⊨ «φ κ»] = [w ⊨ «φ κ'»])›
190    for w :: w and κ :: 'a and φ :: ‹'a⇒𝗈›
191    using that AOT_model_term_equiv_eps(2) by blast
192  have exe_rep_rel: ‹[w ⊨ «exe Π κ⇩₁κ⇩_n»] = ([w ⊨ Π↓] ∧ [w ⊨ κ⇩₁...κ⇩_n↓] ∧
193                                            [w ⊨ «Rep_rel Π κ⇩₁κ⇩_n»])› for w Π κ⇩₁κ⇩_n
194    by (metis AOT_model_denotes_rel.rep_eq exe_def AOT_sem_denotes
195              AOT_model_proposition_choice_simp)
196  moreover have ‹[w ⊨ «Π»↓] ⟹ [w ⊨ «lambda (exe Π)» = «Π»]› for Π w
197    by (auto simp: Rep_rel_inverse lambda_def AOT_sem_denotes AOT_sem_eq
198                   AOT_model_denotes_rel_def Abs_rel_inverse exe_def)
199  moreover have lambda_denotes_beta:
200    ‹[w ⊨ «exe (lambda φ) κ »] = [w ⊨ «φ κ»]›
201    if ‹[w ⊨ «lambda φ»↓]› and ‹[w ⊨ «κ»↓]›
202    for φ κ w
203    using that unfolding exe_def AOT_sem_denotes
204    by (auto simp: lambda_def Abs_rel_inverse split: if_split_asm)
205  moreover have lambda_denotes_simp:
206    ‹[w ⊨ «lambda φ»↓] = (∀ v κ⇩₁κ⇩_n κ⇩₁'κ⇩_n' . [v ⊨ κ⇩₁...κ⇩_n↓] ∧ [v ⊨ κ⇩₁'...κ⇩_n'↓] ∧
207        (∀ Π v . [v ⊨ Π↓] ⟶ [v ⊨ «exe Π κ⇩₁κ⇩_n»] = [v ⊨ «exe Π κ⇩₁'κ⇩_n'»]) ⟶
208        [v ⊨ φ{κ⇩₁...κ⇩_n}] = [v ⊨ φ{κ⇩₁'...κ⇩_n'}])› for φ w
209  proof
210    assume ‹[w ⊨ «lambda φ»↓]›
211    hence ‹AOT_model_denotes (lambda φ)›
212      unfolding AOT_sem_denotes by simp
213    moreover have ‹[w ⊨ «φ κ»] ⟹ [w ⊨ «φ κ'»]›
214      and ‹[w ⊨ «φ κ'»] ⟹ [w ⊨ «φ κ»]›
215      if ‹AOT_model_denotes κ› and ‹AOT_model_term_equiv κ κ'›
216      for w κ κ'
217      by (metis (no_types, lifting) AOT_model_denotes_rel.abs_eq lambda_def
218                                    that calculation)+
219    ultimately show ‹∀ v κ⇩₁κ⇩_n κ⇩₁'κ⇩_n' . [v ⊨ κ⇩₁...κ⇩_n↓] ∧ [v ⊨ κ⇩₁'...κ⇩_n'↓] ∧
220        (∀ Π v . [v ⊨ Π↓] ⟶ [v ⊨ «exe Π κ⇩₁κ⇩_n»] = [v ⊨ «exe Π κ⇩₁'κ⇩_n'»]) ⟶
221        [v ⊨ φ{κ⇩₁...κ⇩_n}] = [v ⊨ φ{κ⇩₁'...κ⇩_n'}]›
222      unfolding AOT_sem_denotes
223      by (metis (no_types) AOT_sem_denotes lambda_denotes_beta)
224  next
225    assume ‹∀ v κ⇩₁κ⇩_n κ⇩₁'κ⇩_n' . [v ⊨ κ⇩₁...κ⇩_n↓] ∧ [v ⊨ κ⇩₁'...κ⇩_n'↓] ∧
226      (∀ Π v . [v ⊨ Π↓] ⟶ [v ⊨ «exe Π κ⇩₁κ⇩_n»] = [v ⊨ «exe Π κ⇩₁'κ⇩_n'»]) ⟶
227      [v ⊨ φ{κ⇩₁...κ⇩_n}] = [v ⊨ φ{κ⇩₁'...κ⇩_n'}]›
228    hence ‹[w ⊨ «φ κ»] = [w ⊨ «φ κ'»]›
229      if ‹AOT_model_denotes κ ∧ AOT_model_denotes κ' ∧ AOT_model_term_equiv κ κ'›
230      for w κ κ'
231      using that
232      by (auto simp: AOT_sem_denotes)
233         (meson AOT_model_term_equiv_rel_equiv AOT_sem_denotes exe_rep_rel)+
234    hence ‹[w ⊨ «φ κ»] = [w ⊨ «φ κ'»]›
235      if ‹AOT_model_denotes κ ∧ AOT_model_term_equiv κ κ'›
236      for w κ κ'
237      using that AOT_model_term_equiv_denotes by blast
238    hence ‹AOT_model_denotes (lambda φ)›
239      by (auto simp: lambda_def Abs_rel_inverse AOT_model_denotes_rel.abs_eq
240                     AOT_model_irregular_equiv AOT_model_term_equiv_eps(3)
241                     AOT_model_term_equiv_regular fix_irregular_def AOT_sem_denotes
242                     AOT_model_term_equiv_denotes AOT_model_proposition_choice_simp
243                     AOT_model_irregular_false
244               split: if_split_asm
245               intro: AOT_model_irregular_eqI)
246    thus ‹[w ⊨ «lambda φ»↓]›
247      by (simp add: AOT_sem_denotes)
248  qed
249  moreover have ‹[w ⊨ «lambda ψ»↓]›
250    if ‹[w ⊨ «lambda φ»↓]›
251    and ‹∀ w κ⇩₁κ⇩_n . [w ⊨ κ⇩₁...κ⇩_n↓] ⟶ [w ⊨ φ{κ⇩₁...κ⇩_n}] = [w ⊨ ψ{κ⇩₁...κ⇩_n}]›
252    for φ ψ w using that unfolding lambda_denotes_simp by auto
253  moreover have ‹[w ⊨ Π↓] ⟹ exe Π κs = Rep_rel Π κs› for Π κs w
254    by (simp add: exe_def AOT_sem_denotes)
255  moreover have ‹lambda (λx. p) = lambda (λx. q) ⟹ p = q› for p q
256    unfolding lambda_def
257    by (auto split: if_split_asm simp: Abs_rel_inject fix_irregular_def)
258       (meson AOT_model_irregular_nondenoting AOT_model_denoting_ex)+
259  moreover have ‹AOT_model_term_equiv x y ⟹ exe Π x = exe Π y› for x y Π
260    unfolding exe_def
261    by (meson AOT_model_denotes_rel.rep_eq)
262  note calculation = calculation this
263  show ?thesis
264    apply (safe intro!: exI[where x=exe] exI[where x=lambda])
265    using calculation apply simp_all
266    using lambda_denotes_simp by blast+
267qed
268
269lemma AOT_model_lambda_denotes:
270  ‹AOT_model_denotes (AOT_lambda φ) = (∀ v κ κ' .
271    AOT_model_denotes κ ∧ AOT_model_denotes κ' ∧ AOT_model_term_equiv κ κ' ⟶
272    [v ⊨ «φ κ»] = [v ⊨ «φ κ'»])›
273proof(safe)
274  fix v and κ κ' :: 'a
275  assume ‹AOT_model_denotes (AOT_lambda φ)›
276  hence 1: ‹AOT_model_denotes κ⇩₁κ⇩_n ∧
277        AOT_model_denotes κ⇩₁'κ⇩_n' ∧
278        (∀Π v. AOT_model_denotes Π ⟶ [v ⊨ [Π]κ⇩₁...κ⇩_n] = [v ⊨ [Π]κ⇩₁'...κ⇩_n']) ⟶
279        [v ⊨ φ{κ⇩₁...κ⇩_n}] = [v ⊨ φ{κ⇩₁'...κ⇩_n'}]› for κ⇩₁κ⇩_n κ⇩₁'κ⇩_n' v
280    using AOT_sem_lambda_denotes[simplified AOT_sem_denotes] by blast
281  {
282    fix v and κ⇩₁κ⇩_n κ⇩₁'κ⇩_n' :: 'a
283    assume d: ‹AOT_model_denotes κ⇩₁κ⇩_n ∧ AOT_model_denotes κ⇩₁'κ⇩_n' ∧
284               AOT_model_term_equiv κ⇩₁κ⇩_n κ⇩₁'κ⇩_n'›
285    hence ‹∀Π w. AOT_model_denotes Π ⟶ [w ⊨ [Π]κ⇩₁...κ⇩_n] = [w ⊨ [Π]κ⇩₁'...κ⇩_n']›
286      by (metis AOT_sem_exe_equiv)
287    hence ‹[v ⊨ φ{κ⇩₁...κ⇩_n}] = [v ⊨ φ{κ⇩₁'...κ⇩_n'}]› using d 1 by auto
288  }
289  moreover assume ‹AOT_model_denotes κ›
290  moreover assume ‹AOT_model_denotes κ'›
291  moreover assume ‹AOT_model_term_equiv κ κ'›
292  ultimately show ‹[v ⊨ «φ κ»] ⟹ [v ⊨ «φ κ'»]›
293              and ‹[v ⊨ «φ κ'»] ⟹ [v ⊨ «φ κ»]›
294    by auto
295next
296  assume 0: ‹∀ v κ κ' . AOT_model_denotes κ ∧ AOT_model_denotes κ' ∧
297                        AOT_model_term_equiv κ κ' ⟶ [v ⊨ «φ κ»] = [v ⊨ «φ κ'»]›
298  {
299    fix κ⇩₁κ⇩_n κ⇩₁'κ⇩_n' :: 'a
300    assume den: ‹AOT_model_denotes κ⇩₁κ⇩_n›
301    moreover assume den': ‹AOT_model_denotes κ⇩₁'κ⇩_n'›
302    assume ‹∀Π v . AOT_model_denotes Π ⟶
303                   [v ⊨ [Π]κ⇩₁...κ⇩_n] = [v ⊨ [Π]κ⇩₁'...κ⇩_n']›
304    hence ‹∀Π v . AOT_model_denotes Π ⟶
305                   [v ⊨ «Rep_rel Π κ⇩₁κ⇩_n»] = [v ⊨ «Rep_rel Π κ⇩₁'κ⇩_n'»]›
306      by (simp add: AOT_sem_denotes AOT_sem_exe den den')
307    hence "AOT_model_term_equiv κ⇩₁κ⇩_n κ⇩₁'κ⇩_n'"
308      unfolding AOT_model_term_equiv_rel_equiv[OF den, OF den']
309      by argo
310    hence ‹[v ⊨ φ{κ⇩₁...κ⇩_n}] = [v ⊨ φ{κ⇩₁'...κ⇩_n'}]› for v
311      using den den' 0 by blast
312  }
313  thus ‹AOT_model_denotes (AOT_lambda φ)›
314    unfolding AOT_sem_lambda_denotes[simplified AOT_sem_denotes]
315    by blast
316qed
317
318specification (AOT_lambda0)
319  AOT_sem_lambda0: "AOT_lambda0 φ = φ"
320  by (rule exI[where x=‹λx. x›]) simp
321
322specification(AOT_concrete)
323  AOT_sem_concrete: ‹[w ⊨ [E!]κ] =
324                     AOT_model_concrete w κ›
325  by (rule exI[where x=‹AOT_var_of_term (Abs_rel
326                          (λ x . ε⇩_𝗈 w . AOT_model_concrete w x))›];
327      subst AOT_var_of_term_inverse)
328     (auto simp: AOT_model_unary_regular AOT_model_concrete_denotes
329                 AOT_model_concrete_equiv AOT_model_regular_κ_def
330                 AOT_model_proposition_choice_simp AOT_sem_exe Abs_rel_inverse
331                 AOT_model_denotes_rel_def AOT_sem_denotes)
332
333lemma AOT_sem_equiv_defI:
334  assumes ‹⋀ v . [v ⊨ φ] ⟹ [v ⊨ ψ]›
335      and ‹⋀ v . [v ⊨ ψ] ⟹ [v ⊨ φ]›
336    shows ‹AOT_model_equiv_def φ ψ›
337  using AOT_model_equiv_def assms by blast
338
339lemma AOT_sem_id_defI:
340  assumes ‹⋀ α v . [v ⊨ «σ α»↓] ⟹ [v ⊨ «τ α» = «σ α»]›
341  assumes ‹⋀ α v . ¬[v ⊨ «σ α»↓] ⟹ [v ⊨ ¬«τ α»↓]›
342  shows ‹AOT_model_id_def τ σ›
343  using assms
344  unfolding AOT_sem_denotes AOT_sem_eq AOT_sem_not
345  using AOT_model_id_def[THEN iffD2]
346  by metis
347
348lemma AOT_sem_id_def2I:
349  assumes ‹⋀ α β v . [v ⊨ «σ α β»↓] ⟹ [v ⊨ «τ α β» = «σ α β»]›
350  assumes ‹⋀ α β v . ¬[v ⊨ «σ α β»↓] ⟹ [v ⊨ ¬«τ α β»↓]›
351  shows ‹AOT_model_id_def (case_prod τ) (case_prod σ)›
352  apply (rule AOT_sem_id_defI)
353  using assms by (auto simp: AOT_sem_conj AOT_sem_not AOT_sem_eq AOT_sem_denotes
354      AOT_model_denotes_prod_def)
355
356lemma AOT_sem_id_defE1:
357  assumes ‹AOT_model_id_def τ σ›
358      and ‹[v ⊨ «σ α»↓]›
359    shows ‹[v ⊨ «τ α» = «σ α»]›
360  using assms by (simp add: AOT_model_id_def AOT_sem_denotes AOT_sem_eq)
361
362lemma AOT_sem_id_defE2:
363  assumes ‹AOT_model_id_def τ σ›
364      and ‹¬[v ⊨ «σ α»↓]›
365    shows ‹¬[v ⊨ «τ α»↓]›
366  using assms by (simp add: AOT_model_id_def AOT_sem_denotes AOT_sem_eq)
367
368lemma AOT_sem_id_def0I:
369  assumes ‹⋀ v . [v ⊨ σ↓] ⟹ [v ⊨ τ = σ]›
370      and ‹⋀ v . ¬[v ⊨ σ↓] ⟹ [v ⊨ ¬τ↓]›
371  shows ‹AOT_model_id_def (case_unit τ) (case_unit σ)›
372  apply (rule AOT_sem_id_defI)
373  using assms
374  by (simp_all add: AOT_sem_conj AOT_sem_eq AOT_sem_not AOT_sem_denotes
375                    AOT_model_denotes_unit_def case_unit_Unity)
376
377lemma AOT_sem_id_def0E1:
378  assumes ‹AOT_model_id_def (case_unit τ) (case_unit σ)›
379      and ‹[v ⊨ σ↓]›
380    shows ‹[v ⊨ τ = σ]›
381  by (metis (full_types) AOT_sem_id_defE1 assms(1) assms(2) case_unit_Unity)
382
383lemma AOT_sem_id_def0E2:
384  assumes ‹AOT_model_id_def (case_unit τ) (case_unit σ)›
385      and ‹¬[v ⊨ σ↓]›
386    shows ‹¬[v ⊨ τ↓]›
387  by (metis AOT_sem_id_defE2 assms(1) assms(2) case_unit_Unity)
388
389lemma AOT_sem_id_def0E3:
390  assumes ‹AOT_model_id_def (case_unit τ) (case_unit σ)›
391      and ‹[v ⊨ σ↓]›
392    shows ‹[v ⊨ τ↓]›
393  using AOT_sem_id_def0E1[OF assms]
394  by (simp add: AOT_sem_eq AOT_sem_denotes)
395
396lemma AOT_sem_ordinary_def_denotes: ‹[w ⊨ [λx ◇[E!]x]↓]›
397  unfolding AOT_sem_denotes AOT_model_lambda_denotes
398  by (auto simp: AOT_sem_dia AOT_model_concrete_equiv
399                 AOT_sem_concrete AOT_sem_denotes)
400lemma AOT_sem_abstract_def_denotes: ‹[w ⊨ [λx ¬◇[E!]x]↓]›
401  unfolding AOT_sem_denotes AOT_model_lambda_denotes
402  by (auto simp: AOT_sem_dia AOT_model_concrete_equiv
403                 AOT_sem_concrete AOT_sem_denotes AOT_sem_not)
404
405text‹Relation identity is constructed using an auxiliary abstract projection
406     mechanism with suitable instantiations for @{typ κ} and products.›
407class AOT_RelationProjection = 
408  fixes AOT_sem_proj_id :: ‹'a::AOT_IndividualTerm ⇒ ('a ⇒ 𝗈) ⇒ ('a ⇒ 𝗈) ⇒ 𝗈›
409  assumes AOT_sem_proj_id_prop:
410    ‹[v ⊨ Π = Π'] =
411     [v ⊨ Π↓ & Π'↓ & ∀α («AOT_sem_proj_id α (λ τ . «[Π]τ») (λ τ . «[Π']τ»)»)]›
412      and AOT_sem_proj_id_refl:
413    ‹[v ⊨ τ↓] ⟹ [v ⊨ [λν⇩₁...ν⇩_n φ{ν⇩₁...ν⇩_n}] = [λν⇩₁...ν⇩_n φ{ν⇩₁...ν⇩_n}]] ⟹
414     [v ⊨ «AOT_sem_proj_id τ φ φ»]›
415
416class AOT_UnaryRelationProjection = AOT_RelationProjection +
417  assumes AOT_sem_unary_proj_id:
418    ‹AOT_sem_proj_id κ φ ψ = «[λν⇩₁...ν⇩_n φ{ν⇩₁...ν⇩_n}] = [λν⇩₁...ν⇩_n ψ{ν⇩₁...ν⇩_n}]»›
419
420instantiation κ :: AOT_UnaryRelationProjection
421begin
422definition AOT_sem_proj_id_κ :: ‹κ ⇒ (κ ⇒ 𝗈) ⇒ (κ ⇒ 𝗈) ⇒ 𝗈› where
423  ‹AOT_sem_proj_id_κ κ φ ψ = «[λz φ{z}] = [λz ψ{z}]»›
424instance proof
425  show ‹[v ⊨ Π = Π'] =
426        [v ⊨ Π↓ & Π'↓ & ∀α («AOT_sem_proj_id α (λ τ . «[Π]τ») (λ τ . «[Π']τ»)»)]›
427    for v and Π Π' :: ‹<κ>›
428    unfolding AOT_sem_proj_id_κ_def
429    by (simp add: AOT_sem_eq AOT_sem_conj AOT_sem_denotes AOT_sem_forall)
430       (metis AOT_sem_denotes AOT_model_denoting_ex AOT_sem_eq AOT_sem_lambda_eta)
431next
432  show ‹AOT_sem_proj_id κ φ ψ = «[λν⇩₁...ν⇩_n φ{ν⇩₁...ν⇩_n}] = [λν⇩₁...ν⇩_n ψ{ν⇩₁...ν⇩_n}]»›
433    for κ :: κ and φ ψ
434    unfolding AOT_sem_proj_id_κ_def ..
435next
436  show ‹[v ⊨ «AOT_sem_proj_id τ φ φ»]›
437    if ‹[v ⊨ τ↓]› and ‹[v ⊨ [λν⇩₁...ν⇩_n φ{ν⇩₁...ν⇩_n}] = [λν⇩₁...ν⇩_n φ{ν⇩₁...ν⇩_n}]]›
438    for τ :: κ and v φ
439    using that by (simp add: AOT_sem_proj_id_κ_def AOT_sem_eq)
440qed
441end
442
443instantiation prod ::
444  ("{AOT_UnaryRelationProjection, AOT_UnaryIndividualTerm}", AOT_RelationProjection)
445  AOT_RelationProjection
446begin
447definition AOT_sem_proj_id_prod :: ‹'a×'b ⇒ ('a×'b ⇒ 𝗈) ⇒ ('a×'b ⇒ 𝗈) ⇒ 𝗈› where
448  ‹AOT_sem_proj_id_prod ≡ λ (x,y) φ ψ . «[λz «φ (z,y)»] = [λz «ψ (z,y)»] &
449    «AOT_sem_proj_id y (λ a . φ (x,a)) (λ a . ψ (x,a))»»›
450instance proof
451  text‹This is the main proof that allows to derive the definition of n-ary
452       relation identity. We need to show that our defined projection identity
453       implies relation identity for relations on pairs of individual terms.›
454  fix v and Π Π' :: ‹<'a×'b>›
455  have AOT_meta_proj_denotes1: ‹AOT_model_denotes (Abs_rel (λz. AOT_exe Π (z, β)))›
456    if ‹AOT_model_denotes Π› for Π :: ‹<'a×'b>› and β
457    using that unfolding AOT_model_denotes_rel.rep_eq
458    apply (simp add: Abs_rel_inverse AOT_meta_prod_equivI(2) AOT_sem_denotes
459                      that)
460    by (metis (no_types, lifting) AOT_meta_prod_equivI(2) AOT_model_denotes_prod_def
461              AOT_model_unary_regular AOT_sem_exe AOT_sem_exe_equiv case_prodD)
462  {
463    fix κ :: 'a and Π :: ‹<'a×'b>›
464    assume Π_denotes: ‹AOT_model_denotes Π›
465    assume α_denotes: ‹AOT_model_denotes κ›
466    hence ‹AOT_exe Π (κ, x) = AOT_exe Π (κ, y)›
467      if ‹AOT_model_term_equiv x y› for x y :: 'b
468      by (simp add: AOT_meta_prod_equivI(1) AOT_sem_exe_equiv that)
469    moreover have ‹AOT_model_denotes κ⇩₁'κ⇩_n'›
470               if ‹[w ⊨ [Π]κ κ⇩₁'...κ⇩_n']› for w κ⇩₁'κ⇩_n'
471      by (metis that AOT_model_denotes_prod_def AOT_sem_exe
472                AOT_sem_denotes case_prodD)
473    moreover {
474      fix x :: 'b
475      assume x_irregular: ‹¬AOT_model_regular x›
476      hence prod_irregular: ‹¬AOT_model_regular (κ, x)›
477        by (metis (no_types, lifting) AOT_model_irregular_nondenoting
478                                      AOT_model_regular_prod_def case_prodD)
479      hence ‹(¬AOT_model_denotes κ ∨ ¬AOT_model_regular x) ∧
480             (AOT_model_denotes κ ∨ ¬AOT_model_denotes x)›
481        unfolding AOT_model_regular_prod_def by blast
482      hence x_nonden: ‹¬AOT_model_regular x›
483        by (simp add: α_denotes)
484      have ‹Rep_rel Π (κ, x) = AOT_model_irregular (Rep_rel Π) (κ, x)›
485        using AOT_model_denotes_rel.rep_eq Π_denotes prod_irregular by blast
486      moreover have ‹AOT_model_irregular (Rep_rel Π) (κ, x) =
487                     AOT_model_irregular (λz. Rep_rel Π (κ, z)) x›
488        using Π_denotes x_irregular prod_irregular x_nonden
489        using AOT_model_irregular_prod_generic
490        apply (induct arbitrary: Π x rule: AOT_model_irregular_prod.induct)
491        by (auto simp: α_denotes AOT_model_irregular_nondenoting
492                       AOT_model_regular_prod_def AOT_meta_prod_equivI(2)
493                       AOT_model_denotes_rel.rep_eq AOT_model_term_equiv_eps(1)
494                 intro!: AOT_model_irregular_eqI)
495      ultimately have
496        ‹AOT_exe Π (κ, x) = AOT_model_irregular (λz. AOT_exe Π (κ, z)) x›
497        unfolding AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π_denotes]
498        by auto
499    }
500    ultimately have ‹AOT_model_denotes (Abs_rel (λz. AOT_exe Π (κ, z)))›
501      by (simp add: Abs_rel_inverse AOT_model_denotes_rel.rep_eq)
502  } note AOT_meta_proj_denotes2 = this
503  {
504    fix κ⇩₁'κ⇩_n' :: 'b and Π :: ‹<'a×'b>›
505    assume Π_denotes: ‹AOT_model_denotes Π›
506    assume β_denotes: ‹AOT_model_denotes κ⇩₁'κ⇩_n'›
507    hence ‹AOT_exe Π (x, κ⇩₁'κ⇩_n') = AOT_exe Π (y, κ⇩₁'κ⇩_n')›
508      if ‹AOT_model_term_equiv x y› for x y :: 'a
509      by (simp add: AOT_meta_prod_equivI(2) AOT_sem_exe_equiv that)
510    moreover have ‹AOT_model_denotes κ›
511               if ‹[w ⊨ [Π]κ κ⇩₁'...κ⇩_n']› for w κ
512      by (metis that AOT_model_denotes_prod_def AOT_sem_exe
513                AOT_sem_denotes case_prodD)
514    moreover {
515      fix x :: 'a
516      assume ‹¬AOT_model_regular x›
517      hence ‹False›
518        using AOT_model_unary_regular by blast
519      hence
520        ‹AOT_exe Π (x,κ⇩₁'κ⇩_n') = AOT_model_irregular (λz. AOT_exe Π (z,κ⇩₁'κ⇩_n')) x›
521        unfolding AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π_denotes]
522        by auto
523    }
524    ultimately have ‹AOT_model_denotes (Abs_rel (λz. AOT_exe Π (z,κ⇩₁'κ⇩_n')))›
525      by (simp add: Abs_rel_inverse AOT_model_denotes_rel.rep_eq)
526  } note AOT_meta_proj_denotes1 = this
527  {
528    assume Π_denotes: ‹AOT_model_denotes Π›
529    assume Π'_denotes: ‹AOT_model_denotes Π'›
530    have Π_proj2_den: ‹AOT_model_denotes (Abs_rel (λz. Rep_rel Π (α, z)))›
531      if ‹AOT_model_denotes α› for α
532      using that AOT_meta_proj_denotes2[OF Π_denotes]
533            AOT_sem_exe_denoting[simplified AOT_sem_denotes,OF Π_denotes] by simp
534    have Π'_proj2_den: ‹AOT_model_denotes (Abs_rel (λz. Rep_rel Π' (α, z)))›
535      if ‹AOT_model_denotes α› for α
536      using that AOT_meta_proj_denotes2[OF Π'_denotes]
537            AOT_sem_exe_denoting[simplified AOT_sem_denotes,OF Π'_denotes] by simp
538    have Π_proj1_den: ‹AOT_model_denotes (Abs_rel (λz. Rep_rel Π (z, α)))›
539      if ‹AOT_model_denotes α› for α
540      using that AOT_meta_proj_denotes1[OF Π_denotes]
541            AOT_sem_exe_denoting[simplified AOT_sem_denotes,OF Π_denotes] by simp
542    have Π'_proj1_den: ‹AOT_model_denotes (Abs_rel (λz. Rep_rel Π' (z, α)))›
543      if ‹AOT_model_denotes α› for α
544      using that AOT_meta_proj_denotes1[OF Π'_denotes]
545            AOT_sem_exe_denoting[simplified AOT_sem_denotes,OF Π'_denotes] by simp
546    {
547      fix κ :: 'a and κ⇩₁'κ⇩_n' :: 'b
548      assume ‹Π = Π'›
549      assume ‹AOT_model_denotes (κ,κ⇩₁'κ⇩_n')›
550      hence ‹AOT_model_denotes κ› and beta_denotes: ‹AOT_model_denotes κ⇩₁'κ⇩_n'›
551        by (auto simp: AOT_model_denotes_prod_def)
552      have ‹AOT_model_denotes «[λz [Π]z κ⇩₁'...κ⇩_n']»›
553        by (rule AOT_model_lambda_denotes[THEN iffD2])
554           (metis AOT_sem_exe_denoting AOT_meta_prod_equivI(2)
555                  AOT_model_denotes_rel.rep_eq AOT_sem_denotes
556                  AOT_sem_exe_denoting Π_denotes)
557      moreover have ‹«[λz [Π]z κ⇩₁'...κ⇩_n']» = «[λz [Π']z κ⇩₁'...κ⇩_n']»›
558        by (simp add: ‹Π = Π'›)
559      moreover have ‹[v ⊨ «AOT_sem_proj_id κ⇩₁'κ⇩_n' (λκ⇩₁'κ⇩_n'. «[Π]κ κ⇩₁'...κ⇩_n'»)
560                                                  (λκ⇩₁'κ⇩_n'. «[Π']κ κ⇩₁'...κ⇩_n'»)»]›
561        unfolding ‹Π = Π'› using beta_denotes
562        by (rule AOT_sem_proj_id_refl[unfolded AOT_sem_denotes];
563            simp add: AOT_sem_denotes AOT_sem_eq AOT_model_lambda_denotes)
564           (metis AOT_meta_prod_equivI(1) AOT_model_denotes_rel.rep_eq
565                  AOT_sem_exe AOT_sem_exe_denoting Π'_denotes)
566      ultimately have ‹[v ⊨ «AOT_sem_proj_id (κ,κ⇩₁'κ⇩_n') (λ κ⇩₁κ⇩_n . «[Π]κ⇩₁...κ⇩_n»)
567                                                         (λ κ⇩₁κ⇩_n . «[Π']κ⇩₁...κ⇩_n»)»]›
568        unfolding AOT_sem_proj_id_prod_def
569        by (simp add: AOT_sem_denotes AOT_sem_conj AOT_sem_eq)
570    }
571    moreover {
572      assume ‹⋀ α . AOT_model_denotes α ⟹
573        [v ⊨ «AOT_sem_proj_id α (λ κ⇩₁κ⇩_n . «[Π]κ⇩₁...κ⇩_n») (λ κ⇩₁κ⇩_n . «[Π']κ⇩₁...κ⇩_n»)»]›
574      hence 0: ‹AOT_model_denotes κ ⟹ AOT_model_denotes κ⇩₁'κ⇩_n' ⟹
575             AOT_model_denotes «[λz [Π]z κ⇩₁'...κ⇩_n']» ∧
576             AOT_model_denotes «[λz [Π']z κ⇩₁'...κ⇩_n']» ∧
577             «[λz [Π]z κ⇩₁'...κ⇩_n']» = «[λz [Π']z κ⇩₁'...κ⇩_n']» ∧
578             [v ⊨ «AOT_sem_proj_id κ⇩₁'κ⇩_n' (λκ⇩₁κ⇩_n. «[Π]κ κ⇩₁...κ⇩_n»)
579                                          (λκ⇩₁κ⇩_n. «[Π']κ κ⇩₁...κ⇩_n»)»]› for κ κ⇩₁'κ⇩_n'
580        unfolding AOT_sem_proj_id_prod_def
581        by (auto simp: AOT_sem_denotes AOT_sem_conj AOT_sem_eq
582                       AOT_model_denotes_prod_def)
583      obtain αden :: 'a and βden :: 'b where
584        αden: ‹AOT_model_denotes αden› and βden: ‹AOT_model_denotes βden›
585        using AOT_model_denoting_ex by metis
586      {
587        fix κ :: 'a
588        assume αdenotes: ‹AOT_model_denotes κ›
589        have 1: ‹[v ⊨ «AOT_sem_proj_id κ⇩₁'κ⇩_n' (λκ⇩₁'κ⇩_n'. «[Π]κ κ⇩₁'...κ⇩_n'»)
590                                              (λκ⇩₁'κ⇩_n'. «[Π']κ κ⇩₁'...κ⇩_n'»)»]›
591          if ‹AOT_model_denotes κ⇩₁'κ⇩_n'› for κ⇩₁'κ⇩_n'
592          using that 0 using αdenotes by blast
593        hence ‹[v ⊨ «AOT_sem_proj_id β (λz. Rep_rel Π (κ, z))
594                                        (λz. Rep_rel Π' (κ, z))»]›
595          if ‹AOT_model_denotes β› for β
596          using that
597          unfolding AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π_denotes]
598                    AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π'_denotes]
599          by blast
600        hence ‹Abs_rel (λz. Rep_rel Π (κ, z)) = Abs_rel (λz. Rep_rel Π' (κ, z))›
601          using AOT_sem_proj_id_prop[of v ‹Abs_rel (λz. Rep_rel Π (κ, z))›
602                                          ‹Abs_rel (λz. Rep_rel Π' (κ, z))›,
603                  simplified AOT_sem_eq AOT_sem_conj AOT_sem_forall
604                             AOT_sem_denotes, THEN iffD2]
605                Π_proj2_den[OF αdenotes] Π'_proj2_den[OF αdenotes]
606          unfolding AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π_denotes]
607                    AOT_sem_exe_denoting[simplified AOT_sem_denotes,
608                                         OF Π_proj2_den[OF αdenotes]]
609                    AOT_sem_exe_denoting[simplified AOT_sem_denotes,
610                                         OF Π'_proj2_den[OF αdenotes]]
611          by (metis Abs_rel_inverse UNIV_I)
612        hence "Rep_rel Π (κ,β) = Rep_rel Π' (κ,β)" for β
613          by (simp add: Abs_rel_inject[simplified]) meson
614      } note αdenotes = this
615      {
616        fix κ⇩₁'κ⇩_n' :: 'b
617        assume βden: ‹AOT_model_denotes κ⇩₁'κ⇩_n'›
618        have 1: ‹«[λz [Π]z κ⇩₁'...κ⇩_n']» = «[λz [Π']z κ⇩₁'...κ⇩_n']»›
619          using 0 βden AOT_model_denoting_ex by blast
620        hence ‹Abs_rel (λz. Rep_rel Π (z, κ⇩₁'κ⇩_n')) =
621               Abs_rel (λz. Rep_rel Π' (z, κ⇩₁'κ⇩_n'))› (is ‹?a = ?b›)
622          apply (safe intro!: AOT_sem_proj_id_prop[of v ‹?a› ‹?b›,
623                  simplified AOT_sem_eq AOT_sem_conj AOT_sem_forall
624                  AOT_sem_denotes, THEN iffD2, THEN conjunct2, THEN conjunct2]
625                  Π_proj1_den[OF βden] Π'_proj1_den[OF βden])
626          unfolding AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π_denotes]
627                    AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π'_denotes]
628                    AOT_sem_exe_denoting[simplified AOT_sem_denotes,
629                                         OF Π_proj1_den[OF βden]]
630                    AOT_sem_exe_denoting[simplified AOT_sem_denotes,
631                                         OF Π'_proj1_den[OF βden]]
632          by (subst (0 1) Abs_rel_inverse; simp?)
633             (metis (no_types, lifting) AOT_model_denotes_rel.abs_eq
634                            AOT_model_lambda_denotes AOT_sem_denotes AOT_sem_eq
635                            AOT_sem_unary_proj_id Π_proj1_den[OF βden])
636        hence ‹Rep_rel Π (x,κ⇩₁'κ⇩_n') = Rep_rel Π' (x,κ⇩₁'κ⇩_n')› for x
637          by (simp add: Abs_rel_inject)
638             metis
639      } note βdenotes = this
640      {
641        fix α :: 'a and β :: 'b
642        assume ‹AOT_model_regular (α, β)›
643        moreover {
644          assume ‹AOT_model_denotes α ∧ AOT_model_regular β›
645          hence ‹Rep_rel Π (α,β) = Rep_rel Π' (α,β)›
646            using αdenotes by presburger
647        }
648        moreover {
649          assume ‹¬AOT_model_denotes α ∧ AOT_model_denotes β›
650          hence ‹Rep_rel Π (α,β) = Rep_rel Π' (α,β)›
651            by (simp add: βdenotes)
652        }
653        ultimately have ‹Rep_rel Π (α,β) = Rep_rel Π' (α,β)›
654          by (metis (no_types, lifting) AOT_model_regular_prod_def case_prodD)
655      }
656      hence ‹Rep_rel Π = Rep_rel Π'›
657        using Π_denotes[unfolded AOT_model_denotes_rel.rep_eq,
658                        THEN conjunct2, THEN conjunct2, THEN spec, THEN mp]
659        using Π'_denotes[unfolded AOT_model_denotes_rel.rep_eq,
660                         THEN conjunct2, THEN conjunct2, THEN spec, THEN mp]
661        using AOT_model_irregular_eqI[of ‹Rep_rel Π› ‹Rep_rel Π'› ‹(_,_)›]
662        using AOT_model_irregular_nondenoting by fastforce
663      hence ‹Π = Π'›
664        by (rule Rep_rel_inject[THEN iffD1])
665    }
666    ultimately have ‹Π = Π' = (∀ κ . AOT_model_denotes κ ⟶
667        [v ⊨ «AOT_sem_proj_id κ (λ κ⇩₁κ⇩_n . «[Π]κ⇩₁...κ⇩_n»)
668                                (λ κ⇩₁κ⇩_n . «[Π']κ⇩₁...κ⇩_n»)»])›
669      by auto
670  }
671  thus ‹[v ⊨ Π = Π'] = [v ⊨ Π↓ & Π'↓ &
672      ∀α («AOT_sem_proj_id α (λ κ⇩₁κ⇩_n . «[Π]κ⇩₁...κ⇩_n») (λ κ⇩₁κ⇩_n . «[Π']κ⇩₁...κ⇩_n»)»)]›
673    by (auto simp: AOT_sem_eq AOT_sem_denotes AOT_sem_forall AOT_sem_conj)
674next
675  fix v and φ :: ‹'a×'b⇒𝗈› and τ :: ‹'a×'b›
676  assume ‹[v ⊨ τ↓]›
677  moreover assume ‹[v ⊨ [λz⇩₁...z⇩_n «φ z⇩₁z⇩_n»] = [λz⇩₁...z⇩_n «φ z⇩₁z⇩_n»]]›
678  ultimately show ‹[v ⊨ «AOT_sem_proj_id τ φ φ»]›
679    unfolding AOT_sem_proj_id_prod_def
680    using AOT_sem_proj_id_refl[of v "snd τ" "λb. φ (fst τ, b)"]
681    by (auto simp: AOT_sem_eq AOT_sem_conj AOT_sem_denotes
682                   AOT_model_denotes_prod_def AOT_model_lambda_denotes
683                   AOT_meta_prod_equivI)
684qed
685end
686
687text‹Sanity-check to verify that n-ary relation identity follows.›
688lemma ‹[v ⊨ Π = Π'] = [v ⊨ Π↓ & Π'↓ & ∀x∀y([λz [Π]z y] = [λz [Π']z y] &
689                                              [λz [Π]x z] = [λz [Π']x z])]›
690  for Π :: ‹<κ×κ>›
691  by (auto simp: AOT_sem_proj_id_prop[of v Π Π'] AOT_sem_proj_id_prod_def
692                 AOT_sem_conj AOT_sem_denotes AOT_sem_forall AOT_sem_unary_proj_id
693                 AOT_model_denotes_prod_def)
694lemma ‹[v ⊨ Π = Π'] = [v ⊨ Π↓ & Π'↓ & ∀x⇩₁∀x⇩₂∀x⇩₃ (
695  [λz [Π]z x⇩₂ x⇩₃] = [λz [Π']z x⇩₂ x⇩₃] &
696  [λz [Π]x⇩₁ z x⇩₃] = [λz [Π']x⇩₁ z x⇩₃] &
697  [λz [Π]x⇩₁ x⇩₂ z] = [λz [Π']x⇩₁ x⇩₂ z])]›
698  for Π :: ‹<κ×κ×κ>›
699  by (auto simp: AOT_sem_proj_id_prop[of v Π Π'] AOT_sem_proj_id_prod_def
700                 AOT_sem_conj AOT_sem_denotes AOT_sem_forall AOT_sem_unary_proj_id
701                 AOT_model_denotes_prod_def)
702lemma ‹[v ⊨ Π = Π'] = [v ⊨ Π↓ & Π'↓ & ∀x⇩₁∀x⇩₂∀x⇩₃∀x⇩₄ (
703    [λz [Π]z x⇩₂ x⇩₃ x⇩₄] = [λz [Π']z x⇩₂ x⇩₃ x⇩₄] &
704    [λz [Π]x⇩₁ z x⇩₃ x⇩₄] = [λz [Π']x⇩₁ z x⇩₃ x⇩₄] &
705    [λz [Π]x⇩₁ x⇩₂ z x⇩₄] = [λz [Π']x⇩₁ x⇩₂ z x⇩₄] &
706    [λz [Π]x⇩₁ x⇩₂ x⇩₃ z] = [λz [Π']x⇩₁ x⇩₂ x⇩₃ z])]›
707  for Π :: ‹<κ×κ×κ×κ>›
708  by (auto simp: AOT_sem_proj_id_prop[of v Π Π'] AOT_sem_proj_id_prod_def
709                 AOT_sem_conj AOT_sem_denotes AOT_sem_forall AOT_sem_unary_proj_id
710                 AOT_model_denotes_prod_def)
711
712text‹n-ary Encoding is constructed using a similar mechanism as n-ary relation
713     identity using an auxiliary notion of projection-encoding.›
714class AOT_Enc =
715  fixes AOT_enc :: ‹'a ⇒ <'a::AOT_IndividualTerm> ⇒ 𝗈›
716    and AOT_proj_enc :: ‹'a ⇒ ('a ⇒ 𝗈) ⇒ 𝗈›
717  assumes AOT_sem_enc_denotes:
718    ‹[v ⊨ «AOT_enc κ⇩₁κ⇩_n Π»] ⟹ [v ⊨ κ⇩₁...κ⇩_n↓] ∧ [v ⊨ Π↓]›
719  assumes AOT_sem_enc_proj_enc:
720    ‹[v ⊨ «AOT_enc κ⇩₁κ⇩_n Π»] =
721     [v ⊨ Π↓ & «AOT_proj_enc κ⇩₁κ⇩_n (λ κ⇩₁κ⇩_n.  «[Π]κ⇩₁...κ⇩_n»)»]›
722  assumes AOT_sem_proj_enc_denotes:
723    ‹[v ⊨ «AOT_proj_enc κ⇩₁κ⇩_n φ»] ⟹ [v ⊨ κ⇩₁...κ⇩_n↓]›
724  assumes AOT_sem_enc_nec:
725    ‹[v ⊨ «AOT_enc κ⇩₁κ⇩_n Π»] ⟹ [w ⊨ «AOT_enc κ⇩₁κ⇩_n Π»]›
726  assumes AOT_sem_proj_enc_nec:
727    ‹[v ⊨ «AOT_proj_enc κ⇩₁κ⇩_n φ»] ⟹ [w ⊨ «AOT_proj_enc κ⇩₁κ⇩_n φ»]›
728  assumes AOT_sem_universal_encoder:
729    ‹∃ κ⇩₁κ⇩_n. [v ⊨ κ⇩₁...κ⇩_n↓] ∧ (∀ Π . [v ⊨ Π↓] ⟶ [v ⊨ «AOT_enc κ⇩₁κ⇩_n Π»]) ∧
730             (∀ φ . [v ⊨ [λz⇩₁...z⇩_n φ{z⇩₁...z⇩_n}]↓] ⟶ [v ⊨ «AOT_proj_enc κ⇩₁κ⇩_n φ»])›
731
732AOT_syntax_print_translations
733  "_AOT_enc (_AOT_individual_term κ) (_AOT_relation_term Π)" <= "CONST AOT_enc κ Π"
734
735context AOT_meta_syntax
736begin
737notation AOT_enc ("❙⦃_,_❙⦄")
738end
739context AOT_no_meta_syntax
740begin
741no_notation AOT_enc ("❙⦃_,_❙⦄")
742end
743
744text‹Unary encoding additionally has to satisfy the axioms of unary encoding and
745     the definition of property identity.›
746class AOT_UnaryEnc = AOT_UnaryIndividualTerm +
747  assumes AOT_sem_enc_eq: ‹[v ⊨ Π↓ & Π'↓ & □∀ν (ν[Π] ≡ ν[Π']) → Π = Π']›
748      and AOT_sem_A_objects: ‹[v ⊨ ∃x (¬◇[E!]x & ∀F (x[F] ≡ φ{F}))]›
749      and AOT_sem_unary_proj_enc: ‹AOT_proj_enc x ψ = AOT_enc x «[λz ψ{z}]»›
750      and AOT_sem_nocoder: ‹[v ⊨ [E!]κ] ⟹ ¬[w ⊨ «AOT_enc κ Π»]›
751      and AOT_sem_ind_eq: ‹([v ⊨ κ↓] ∧ [v ⊨ κ'↓] ∧ κ = (κ')) =
752       (([v ⊨ [λx ◇[E!]x]κ] ∧
753         [v ⊨ [λx ◇[E!]x]κ'] ∧
754         (∀ v Π . [v ⊨ Π↓] ⟶ [v ⊨ [Π]κ] = [v ⊨ [Π]κ']))
755        ∨ ([v ⊨ [λx ¬◇[E!]x]κ] ∧
756           [v ⊨ [λx ¬◇[E!]x]κ'] ∧
757           (∀ v Π . [v ⊨ Π↓] ⟶ [v ⊨ κ[Π]] = [v ⊨ κ'[Π]])))›
758
759      (* only extended models *)
760      and AOT_sem_enc_indistinguishable_all:
761          ‹AOT_ExtendedModel ⟹
762           [v ⊨ [λx ¬◇[E!]x]κ] ⟹
763           [v ⊨ [λx ¬◇[E!]x]κ'] ⟹
764           (⋀ Π' . [v ⊨ Π'↓] ⟹ (⋀ w . [w ⊨ [Π']κ] = [w ⊨ [Π']κ'])) ⟹
765           [v ⊨ Π↓] ⟹
766           (⋀ Π' . [v ⊨ Π'↓] ⟹ (⋀ κ⇩₀ . [v ⊨ [λx ◇[E!]x]κ⇩₀] ⟹
767              (⋀ w . [w ⊨ [Π']κ⇩₀] = [w ⊨ [Π]κ⇩₀])) ⟹ [v ⊨ κ[Π']]) ⟹
768           (⋀ Π' . [v ⊨ Π'↓] ⟹ (⋀ κ⇩₀ . [v ⊨ [λx ◇[E!]x]κ⇩₀] ⟹
769              (⋀ w . [w ⊨ [Π']κ⇩₀] = [w ⊨ [Π]κ⇩₀])) ⟹ [v ⊨ κ'[Π']])›
770      and AOT_sem_enc_indistinguishable_ex:
771          ‹AOT_ExtendedModel ⟹
772           [v ⊨ [λx ¬◇[E!]x]κ] ⟹
773           [v ⊨ [λx ¬◇[E!]x]κ'] ⟹
774           (⋀ Π' . [v ⊨ Π'↓] ⟹ (⋀ w . [w ⊨ [Π']κ] = [w ⊨ [Π']κ'])) ⟹
775           [v ⊨ Π↓] ⟹
776           ∃ Π' . [v ⊨ Π'↓] ∧ [v ⊨ κ[Π']] ∧
777                  (∀ κ⇩₀ . [v ⊨ [λx ◇[E!]x]κ⇩₀] ⟶
778                          (∀ w . [w ⊨ [Π']κ⇩₀] = [w ⊨ [Π]κ⇩₀])) ⟹
779           ∃ Π' . [v ⊨ Π'↓] ∧ [v ⊨ κ'[Π']] ∧
780                  (∀ κ⇩₀ . [v ⊨ [λx ◇[E!]x]κ⇩₀] ⟶
781                          (∀ w . [w ⊨ [Π']κ⇩₀] = [w ⊨ [Π]κ⇩₀]))›
782
783text‹We specify encoding to align with the model-construction of encoding.›
784consts AOT_sem_enc_κ :: ‹κ ⇒ <κ> ⇒ 𝗈›
785specification(AOT_sem_enc_κ)
786  AOT_sem_enc_κ:
787  ‹[v ⊨ «AOT_sem_enc_κ κ Π»] =
788   (AOT_model_denotes κ ∧ AOT_model_denotes Π ∧ AOT_model_enc κ Π)›
789  by (rule exI[where x=‹λ κ Π . ε⇩_𝗈 w . AOT_model_denotes κ ∧ AOT_model_denotes Π ∧
790                                       AOT_model_enc κ Π›])
791     (simp add: AOT_model_proposition_choice_simp AOT_model_enc_κ_def κ.case_eq_if)
792
793text‹We show that @{typ κ} satisfies the generic properties of n-ary encoding.›
794instantiation κ :: AOT_Enc
795begin
796definition AOT_enc_κ :: ‹κ ⇒ <κ> ⇒ 𝗈› where
797  ‹AOT_enc_κ ≡ AOT_sem_enc_κ›
798definition AOT_proj_enc_κ :: ‹κ ⇒ (κ ⇒ 𝗈) ⇒ 𝗈› where
799  ‹AOT_proj_enc_κ ≡ λ κ φ . AOT_enc κ «[λz «φ z»]»›
800lemma AOT_enc_κ_meta:
801  ‹[v ⊨ κ[Π]] = (AOT_model_denotes κ ∧ AOT_model_denotes Π ∧ AOT_model_enc κ Π)›
802  for κ::κ
803  using AOT_sem_enc_κ unfolding AOT_enc_κ_def by auto
804instance proof
805  fix v and κ :: κ and Π
806  show ‹[v ⊨ «AOT_enc κ Π»] ⟹ [v ⊨ κ↓] ∧ [v ⊨ Π↓]›
807    unfolding AOT_sem_denotes
808    using AOT_enc_κ_meta by blast
809next
810  fix v and κ :: κ and Π
811  show ‹[v ⊨ κ[Π]] = [v ⊨ Π↓ & «AOT_proj_enc κ (λ κ'.  «[Π]κ'»)»]›
812  proof
813    assume enc: ‹[v ⊨ κ[Π]]›
814    hence Π_denotes: ‹AOT_model_denotes Π›
815      by (simp add: AOT_enc_κ_meta)
816    hence Π_eta_denotes: ‹AOT_model_denotes «[λz [Π]z]»›
817      using AOT_sem_denotes AOT_sem_eq AOT_sem_lambda_eta by metis
818    show ‹[v ⊨ Π↓ & «AOT_proj_enc κ (λ κ.  «[Π]κ»)»]›
819      using AOT_sem_lambda_eta[simplified AOT_sem_denotes AOT_sem_eq, OF Π_denotes]
820      using Π_eta_denotes Π_denotes
821      by (simp add: AOT_sem_conj AOT_sem_denotes AOT_proj_enc_κ_def enc)
822  next
823    assume ‹[v ⊨ Π↓ & «AOT_proj_enc κ (λ κ.  «[Π]κ»)»]›
824    hence Π_denotes: "AOT_model_denotes Π" and eta_enc: "[v ⊨ κ[λz [Π]z]]" 
825      by (auto simp: AOT_sem_conj AOT_sem_denotes AOT_proj_enc_κ_def)
826    thus ‹[v ⊨ κ[Π]]›
827      using AOT_sem_lambda_eta[simplified AOT_sem_denotes AOT_sem_eq, OF Π_denotes]
828      by auto
829  qed
830next
831  show ‹[v ⊨ «AOT_proj_enc κ φ»] ⟹ [v ⊨ κ↓]› for v and κ :: κ and φ
832    by (simp add: AOT_enc_κ_meta AOT_sem_denotes AOT_proj_enc_κ_def)
833next
834  fix v w and κ :: κ and Π
835  assume ‹[v ⊨ κ[Π]]›
836  thus ‹[w ⊨ κ[Π]]›
837    by (simp add: AOT_enc_κ_meta)
838next
839  fix v w and κ :: κ and φ
840  assume ‹[v ⊨ «AOT_proj_enc κ φ»]›
841  thus ‹[w ⊨ «AOT_proj_enc κ φ»]›
842    by (simp add: AOT_enc_κ_meta AOT_proj_enc_κ_def)
843next
844  show ‹∃κ::κ. [v ⊨ κ↓] ∧ (∀ Π . [v ⊨ Π↓] ⟶  [v ⊨ κ[Π]]) ∧
845               (∀ φ . [v ⊨ [λz φ{z}]↓] ⟶  [v ⊨ «AOT_proj_enc κ φ»])› for v
846    by (rule exI[where x=‹ακ UNIV›])
847       (simp add: AOT_sem_denotes AOT_enc_κ_meta AOT_model_enc_κ_def
848                  AOT_model_denotes_κ_def  AOT_proj_enc_κ_def)
849qed
850end
851
852text‹We show that @{typ κ} satisfies the properties of unary encoding.›
853instantiation κ :: AOT_UnaryEnc
854begin
855instance proof
856  fix v and Π Π' :: ‹<κ>›
857  show ‹[v ⊨ Π↓ & Π'↓ & □∀ν (ν[Π] ≡ ν[Π']) → Π = Π']›
858    apply (simp add: AOT_sem_forall AOT_sem_eq AOT_sem_imp AOT_sem_equiv
859                     AOT_enc_κ_meta AOT_sem_conj AOT_sem_denotes AOT_sem_box)
860    using AOT_meta_A_objects_κ by fastforce
861next
862  fix v and φ:: ‹<κ> ⇒ 𝗈›
863  show ‹[v ⊨ ∃x (¬◇[E!]x & ∀F (x[F] ≡ φ{F}))]›
864    using AOT_model_A_objects[of "λ Π . [v ⊨ φ{Π}]"]
865    by (auto simp: AOT_sem_denotes AOT_sem_exists AOT_sem_conj AOT_sem_not
866                   AOT_sem_dia AOT_sem_concrete AOT_enc_κ_meta AOT_sem_equiv
867                   AOT_sem_forall)
868next
869  show ‹AOT_proj_enc x ψ = AOT_enc x (AOT_lambda ψ)› for x :: κ and ψ
870    by (simp add: AOT_proj_enc_κ_def)
871next
872  show ‹[v ⊨ [E!]κ] ⟹ ¬ [w ⊨ κ[Π]]› for v w and κ :: κ and Π
873    by (simp add: AOT_enc_κ_meta AOT_sem_concrete AOT_model_nocoder)
874next
875  fix v and κ κ' :: κ
876  show ‹([v ⊨ κ↓] ∧ [v ⊨ κ'↓] ∧ κ = κ') =
877         (([v ⊨ [λx ◇[E!]x]κ] ∧
878           [v ⊨ [λx ◇[E!]x]κ'] ∧
879           (∀ v Π . [v ⊨ Π↓] ⟶ [v ⊨ [Π]κ] = [v ⊨ [Π]κ']))
880          ∨ ([v ⊨ [λx ¬◇[E!]x]κ] ∧
881             [v ⊨ [λx ¬◇[E!]x]κ'] ∧
882             (∀ v Π . [v ⊨ Π↓] ⟶ [v ⊨ κ[Π]] = [v ⊨ κ'[Π]])))›
883    (is ‹?lhs = (?ordeq ∨ ?abseq)›)
884  proof -
885  {
886    assume 0: ‹[v ⊨ κ↓] ∧ [v ⊨ κ'↓] ∧ κ = κ'›
887    {
888      assume ‹is_ωκ κ'›
889      hence ‹[v ⊨ [λx ◇[E!]x]κ']›
890        apply (subst AOT_sem_lambda_beta[OF AOT_sem_ordinary_def_denotes, of v κ'])
891         apply (simp add: "0")
892        apply (simp add: AOT_sem_dia)
893        using AOT_sem_concrete AOT_model_ω_concrete_in_some_world is_ωκ_def by force
894      hence ‹?ordeq› unfolding 0[THEN conjunct2, THEN conjunct2] by auto
895    }
896    moreover {
897      assume ‹is_ακ κ'›
898      hence ‹[v ⊨ [λx ¬◇[E!]x]κ']›
899        apply (subst AOT_sem_lambda_beta[OF AOT_sem_abstract_def_denotes, of v κ'])
900         apply (simp add: "0")
901        apply (simp add: AOT_sem_not AOT_sem_dia)
902        using AOT_sem_concrete is_ακ_def by force
903      hence ‹?abseq› unfolding 0[THEN conjunct2, THEN conjunct2] by auto
904    }
905    ultimately have ‹?ordeq ∨ ?abseq›
906      by (meson "0" AOT_sem_denotes AOT_model_denotes_κ_def κ.exhaust_disc)
907  }
908  moreover {
909    assume ordeq: ‹?ordeq›
910    hence κ_denotes: ‹[v ⊨ κ↓]› and κ'_denotes: ‹[v ⊨ κ'↓]› 
911      by (simp add: AOT_sem_denotes AOT_sem_exe)+
912    hence ‹is_ωκ κ› and ‹is_ωκ κ'›
913      by (metis AOT_model_concrete_κ.simps(2) AOT_model_denotes_κ_def
914                AOT_sem_concrete AOT_sem_denotes AOT_sem_dia AOT_sem_lambda_beta
915                AOT_sem_ordinary_def_denotes κ.collapse(2) κ.exhaust_disc ordeq)+
916    have denotes: ‹[v ⊨ [λz «ε⇩_𝗈 w . κυ z = κυ κ»]↓]›
917      unfolding AOT_sem_denotes AOT_model_lambda_denotes
918      by (simp add: AOT_model_term_equiv_κ_def)
919    hence "[v ⊨ [λz «ε⇩_𝗈 w . κυ z = κυ κ»]κ] = [v ⊨ [λz «ε⇩_𝗈 w . κυ z = κυ κ»]κ']"
920      using ordeq by (simp add: AOT_sem_denotes)
921    hence ‹[v ⊨ «κ»↓] ∧ [v ⊨ «κ'»↓] ∧ κ = κ'›
922      unfolding AOT_sem_lambda_beta[OF denotes, OF κ_denotes]
923                AOT_sem_lambda_beta[OF denotes, OF κ'_denotes]
924      using κ'_denotes ‹is_ωκ κ'› ‹is_ωκ κ› is_ωκ_def
925            AOT_model_proposition_choice_simp by force
926  }
927  moreover {
928    assume 0: ‹?abseq›
929    hence κ_denotes: ‹[v ⊨ κ↓]› and κ'_denotes: ‹[v ⊨ κ'↓]› 
930      by (simp add: AOT_sem_denotes AOT_sem_exe)+
931    hence ‹¬is_ωκ κ› and ‹¬is_ωκ κ'›
932      by (metis AOT_model_ω_concrete_in_some_world AOT_model_concrete_κ.simps(1)
933                AOT_sem_concrete AOT_sem_dia AOT_sem_exe AOT_sem_lambda_beta
934                AOT_sem_not κ.collapse(1) 0)+
935    hence ‹is_ακ κ› and ‹is_ακ κ'›
936      by (meson AOT_sem_denotes AOT_model_denotes_κ_def κ.exhaust_disc
937                κ_denotes κ'_denotes)+
938    then obtain x y where κ_def: ‹κ = ακ x› and κ'_def: ‹κ' = ακ y›
939      using is_ακ_def by auto
940    {
941      fix r
942      assume ‹r ∈ x›
943      hence ‹[v ⊨ κ[«urrel_to_rel r»]]›
944        unfolding κ_def
945        unfolding AOT_enc_κ_meta
946        unfolding AOT_model_enc_κ_def
947        apply (simp add: AOT_model_denotes_κ_def)
948        by (metis (mono_tags) AOT_rel_equiv_def Quotient_def urrel_quotient)
949      hence ‹[v ⊨ κ'[«urrel_to_rel r»]]›
950        using AOT_enc_κ_meta 0 by (metis AOT_sem_enc_denotes)
951      hence ‹r ∈ y›
952        unfolding κ'_def
953        unfolding AOT_enc_κ_meta
954        unfolding AOT_model_enc_κ_def
955        apply (simp add: AOT_model_denotes_κ_def)
956        using Quotient_abs_rep urrel_quotient by fastforce
957    }
958    moreover {
959      fix r
960      assume ‹r ∈ y›
961      hence ‹[v ⊨ κ'[«urrel_to_rel r»]]›
962        unfolding κ'_def
963        unfolding AOT_enc_κ_meta
964        unfolding AOT_model_enc_κ_def
965        apply (simp add: AOT_model_denotes_κ_def)
966        by (metis (mono_tags) AOT_rel_equiv_def Quotient_def urrel_quotient)
967      hence ‹[v ⊨ κ[«urrel_to_rel r»]]›
968        using AOT_enc_κ_meta 0 by (metis AOT_sem_enc_denotes)
969      hence ‹r ∈ x›
970        unfolding κ_def
971        unfolding AOT_enc_κ_meta
972        unfolding AOT_model_enc_κ_def
973        apply (simp add: AOT_model_denotes_κ_def)
974        using Quotient_abs_rep urrel_quotient by fastforce
975    }
976    ultimately have "x = y" by blast
977    hence ‹[v ⊨ κ↓] ∧ [v ⊨ κ'↓] ∧ κ = κ'›
978      using κ'_def κ'_denotes κ_def by blast
979  }
980  ultimately show ?thesis
981    unfolding AOT_sem_denotes
982    by auto
983  qed
984(* Only extended model *)
985next
986  fix v and κ κ' :: κ and Π Π' :: ‹<κ>›
987  assume ext: ‹AOT_ExtendedModel›
988  assume ‹[v ⊨ [λx ¬◇[E!]x]κ]›
989  hence ‹is_ακ κ›
990    by (metis AOT_model_ω_concrete_in_some_world AOT_model_concrete_κ.simps(1)
991              AOT_model_denotes_κ_def AOT_sem_concrete AOT_sem_denotes AOT_sem_dia
992              AOT_sem_exe AOT_sem_lambda_beta AOT_sem_not κ.collapse(1) κ.exhaust_disc)
993  hence κ_abs: ‹¬(∃ w . AOT_model_concrete w κ)›
994    using is_ακ_def by fastforce
995  have κ_den: ‹AOT_model_denotes κ›
996    by (simp add: AOT_model_denotes_κ_def κ.distinct_disc(5) ‹is_ακ κ›)
997  assume ‹[v ⊨ [λx ¬◇[E!]x]κ']›
998  hence ‹is_ακ κ'›
999    by (metis AOT_model_ω_concrete_in_some_world AOT_model_concrete_κ.simps(1)
1000              AOT_model_denotes_κ_def AOT_sem_concrete AOT_sem_denotes AOT_sem_dia
1001              AOT_sem_exe AOT_sem_lambda_beta AOT_sem_not κ.collapse(1)
1002              κ.exhaust_disc)
1003  hence κ'_abs: ‹¬(∃ w . AOT_model_concrete w κ')›
1004    using is_ακ_def by fastforce
1005  have κ'_den: ‹AOT_model_denotes κ'›
1006    by (meson AOT_model_denotes_κ_def κ.distinct_disc(6) ‹is_ακ κ'›)
1007  assume ‹[v ⊨ Π'↓] ⟹ [w ⊨ [Π']κ] = [w ⊨ [Π']κ']› for Π' w
1008  hence indist: ‹[v ⊨ «Rep_rel Π' κ»] = [v ⊨ «Rep_rel Π' κ'»]›
1009    if ‹AOT_model_denotes Π'› for Π' v
1010    by (metis AOT_sem_denotes AOT_sem_exe κ'_den κ_den that)
1011  assume κ_enc_cond: ‹[v ⊨ Π'↓] ⟹
1012    (⋀ κ⇩₀ w. [v ⊨ [λx ◇[E!]x]κ⇩₀] ⟹
1013             [w ⊨ [Π']κ⇩₀] = [w ⊨ [Π]κ⇩₀]) ⟹
1014    [v ⊨ κ[Π']]› for Π'
1015  assume Π_den': ‹[v ⊨ Π↓]›
1016  hence Π_den: ‹AOT_model_denotes Π›
1017    using AOT_sem_denotes by blast
1018  {
1019    fix Π' :: ‹<κ>›
1020    assume Π'_den: ‹AOT_model_denotes Π'›
1021    hence Π'_den': ‹[v ⊨ Π'↓]›
1022      by (simp add: AOT_sem_denotes)
1023    assume 1: ‹∃w. AOT_model_concrete w x ⟹
1024               [v ⊨ «Rep_rel Π' x»] = [v ⊨ «Rep_rel Π x»]› for v x
1025    {
1026      fix κ⇩₀ :: κ and w
1027      assume ‹[v ⊨ [λx ◇[E!]x]κ⇩₀]›
1028      hence ‹is_ωκ κ⇩₀›
1029        by (smt (z3) AOT_model_concrete_κ.simps(2) AOT_model_denotes_κ_def
1030                     AOT_sem_concrete AOT_sem_denotes AOT_sem_dia AOT_sem_exe
1031                     AOT_sem_lambda_beta κ.exhaust_disc is_ακ_def)
1032      then obtain x where x_prop: ‹κ⇩₀ = ωκ x›
1033        using is_ωκ_def by blast
1034      have ‹∃w . AOT_model_concrete w (ωκ x)›
1035        by (simp add: AOT_model_ω_concrete_in_some_world)
1036      hence ‹[v ⊨ «Rep_rel Π' (ωκ x)»] = [v ⊨ «Rep_rel Π (ωκ x)»]› for v
1037        using 1 by blast
1038      hence ‹[w ⊨ [Π']κ⇩₀] = [w ⊨ [Π]κ⇩₀]› unfolding x_prop
1039        by (simp add: AOT_sem_exe AOT_sem_denotes AOT_model_denotes_κ_def
1040                      Π'_den Π_den)
1041    } note 2 = this
1042    have ‹[v ⊨ κ[Π']]›
1043      using κ_enc_cond[OF Π'_den', OF 2]
1044      by metis
1045    hence ‹AOT_model_enc κ Π'›
1046      using AOT_enc_κ_meta by blast
1047  } note κ_enc_cond = this
1048  hence ‹AOT_model_denotes Π' ⟹
1049       (⋀v x. ∃w. AOT_model_concrete w x ⟹
1050              [v ⊨ «Rep_rel Π' x»] = [v ⊨ «Rep_rel Π x»]) ⟹
1051       AOT_model_enc κ Π'› for Π'
1052    by blast
1053  assume Π'_den': ‹[v ⊨ Π'↓]›
1054  hence Π'_den: ‹AOT_model_denotes Π'›
1055    using AOT_sem_denotes by blast
1056  assume ord_indist: ‹[v ⊨ [λx ◇[E!]x]κ⇩₀] ⟹
1057                      [w ⊨ [Π']κ⇩₀] = [w ⊨ [Π]κ⇩₀]› for κ⇩₀ w
1058  {
1059    fix w and κ⇩₀ :: κ
1060    assume 0: ‹∃w. AOT_model_concrete w κ⇩₀›
1061    hence ‹[v ⊨ [λx ◇[E!]x]κ⇩₀]›
1062      using AOT_model_concrete_denotes AOT_sem_concrete AOT_sem_denotes AOT_sem_dia
1063            AOT_sem_lambda_beta AOT_sem_ordinary_def_denotes by blast
1064    hence ‹[w ⊨ [Π']κ⇩₀] = [w ⊨ [Π]κ⇩₀]›
1065      using ord_indist by metis 
1066    hence ‹[w ⊨ «Rep_rel Π' κ⇩₀»] = [w ⊨ «Rep_rel Π κ⇩₀»]›
1067      by (metis AOT_model_concrete_denotes AOT_sem_denotes AOT_sem_exe Π'_den Π_den 0)
1068  } note ord_indist = this
1069  have ‹AOT_model_enc κ' Π'›
1070    using AOT_model_enc_indistinguishable_all
1071            [OF ext, OF κ_den, OF κ_abs, OF κ'_den, OF κ'_abs, OF Π_den]
1072          indist κ_enc_cond Π'_den ord_indist by blast
1073  thus ‹[v ⊨ κ'[Π']]›
1074    using AOT_enc_κ_meta Π'_den κ'_den by blast
1075next
1076  fix v and κ κ' :: κ and Π Π' :: ‹<κ>›
1077  assume ext: ‹AOT_ExtendedModel›
1078  assume ‹[v ⊨ [λx ¬◇[E!]x]κ]›
1079  hence ‹is_ακ κ›
1080    by (metis AOT_model_ω_concrete_in_some_world AOT_model_concrete_κ.simps(1)
1081              AOT_model_denotes_κ_def AOT_sem_concrete AOT_sem_denotes AOT_sem_dia
1082              AOT_sem_exe AOT_sem_lambda_beta AOT_sem_not κ.collapse(1)
1083              κ.exhaust_disc)
1084  hence κ_abs: ‹¬(∃ w . AOT_model_concrete w κ)›
1085    using is_ακ_def by fastforce
1086  have κ_den: ‹AOT_model_denotes κ›
1087    by (simp add: AOT_model_denotes_κ_def κ.distinct_disc(5) ‹is_ακ κ›)
1088  assume ‹[v ⊨ [λx ¬◇[E!]x]κ']›
1089  hence ‹is_ακ κ'›
1090    by (metis AOT_model_ω_concrete_in_some_world AOT_model_concrete_κ.simps(1)
1091              AOT_model_denotes_κ_def AOT_sem_concrete AOT_sem_denotes AOT_sem_dia
1092              AOT_sem_exe AOT_sem_lambda_beta AOT_sem_not κ.collapse(1)
1093              κ.exhaust_disc)
1094  hence κ'_abs: ‹¬(∃ w . AOT_model_concrete w κ')›
1095    using is_ακ_def by fastforce
1096  have κ'_den: ‹AOT_model_denotes κ'›
1097    by (meson AOT_model_denotes_κ_def κ.distinct_disc(6) ‹is_ακ κ'›)
1098  assume ‹[v ⊨ Π'↓] ⟹ [w ⊨ [Π']κ] = [w ⊨ [Π']κ']› for Π' w
1099  hence indist: ‹[v ⊨ «Rep_rel Π' κ»] = [v ⊨ «Rep_rel Π' κ'»]›
1100    if ‹AOT_model_denotes Π'› for Π' v
1101    by (metis AOT_sem_denotes AOT_sem_exe κ'_den κ_den that)
1102  assume Π_den': ‹[v ⊨ Π↓]›
1103  hence Π_den: ‹AOT_model_denotes Π›
1104    using AOT_sem_denotes by blast
1105  assume ‹∃Π'. [v ⊨ Π'↓] ∧ [v ⊨ κ[Π']] ∧
1106               (∀κ⇩₀. [v ⊨ [λx ◇[E!]x]κ⇩₀] ⟶
1107                     (∀w. [w ⊨ [Π']κ⇩₀] = [w ⊨ [Π]κ⇩₀]))›
1108  then obtain Π' where
1109      Π'_den: ‹[v ⊨ Π'↓]› and
1110      Π'_enc: ‹[v ⊨ κ[Π']]› and
1111      Π'_prop: ‹∀κ⇩₀. [v ⊨ [λx ◇[E!]x]κ⇩₀] ⟶
1112                     (∀w. [w ⊨ [Π']κ⇩₀] = [w ⊨ [Π]κ⇩₀])›
1113    by blast
1114  have ‹AOT_model_denotes Π'›
1115    using AOT_enc_κ_meta Π'_enc by force
1116  moreover have ‹AOT_model_enc κ Π'›
1117    using AOT_enc_κ_meta Π'_enc by blast
1118  moreover have ‹(∃w. AOT_model_concrete w κ⇩₀) ⟹
1119                 [v ⊨ «Rep_rel Π' κ⇩₀»] = [v ⊨ «Rep_rel Π κ⇩₀»]› for κ⇩₀ v
1120  proof -
1121    assume 0: ‹∃w. AOT_model_concrete w κ⇩₀›
1122    hence ‹[v ⊨ [λx ◇[E!]x]κ⇩₀]› for v
1123      using AOT_model_concrete_denotes AOT_sem_concrete AOT_sem_denotes AOT_sem_dia
1124            AOT_sem_lambda_beta AOT_sem_ordinary_def_denotes by blast
1125    hence ‹∀w. [w ⊨ [Π']κ⇩₀] = [w ⊨ [Π]κ⇩₀]› using Π'_prop by blast
1126    thus ‹[v ⊨ «Rep_rel Π' κ⇩₀»] = [v ⊨ «Rep_rel Π κ⇩₀»]›
1127      by (meson "0" AOT_model_concrete_denotes AOT_sem_denotes AOT_sem_exe Π_den
1128                calculation(1))
1129  qed
1130  ultimately have ‹∃Π'. AOT_model_denotes Π' ∧ AOT_model_enc κ Π' ∧
1131                        (∀v x. (∃w. AOT_model_concrete w x) ⟶
1132                         [v ⊨ «Rep_rel Π' x»] = [v ⊨ «Rep_rel Π x»])›
1133    by blast
1134  hence ‹∃Π'. AOT_model_denotes Π' ∧ AOT_model_enc κ' Π' ∧
1135              (∀v x. (∃w. AOT_model_concrete w x) ⟶
1136               [v ⊨ «Rep_rel Π' x»] = [v ⊨ «Rep_rel Π x»])›
1137    using AOT_model_enc_indistinguishable_ex
1138            [OF ext, OF κ_den, OF κ_abs, OF κ'_den, OF κ'_abs, OF Π_den]
1139          indist by blast
1140  then obtain Π'' where
1141      Π''_den: ‹AOT_model_denotes Π''›
1142      and Π''_enc: ‹AOT_model_enc κ' Π''›
1143      and Π''_prop: ‹(∃w. AOT_model_concrete w x) ⟹
1144                      [v ⊨ «Rep_rel Π'' x»] = [v ⊨ «Rep_rel Π x»]› for v x
1145    by blast
1146  have ‹[v ⊨ Π''↓]›
1147    by (simp add: AOT_sem_denotes Π''_den)
1148  moreover have ‹[v ⊨ κ'[Π'']]›
1149    by (simp add: AOT_enc_κ_meta Π''_den Π''_enc κ'_den)
1150  moreover have ‹[v ⊨ [λx ◇[E!]x]κ⇩₀] ⟹
1151                 (∀w. [w ⊨ [Π'']κ⇩₀] = [w ⊨ [Π]κ⇩₀])› for κ⇩₀
1152  proof -
1153    assume ‹[v ⊨ [λx ◇[E!]x]κ⇩₀]›
1154    hence ‹∃w. AOT_model_concrete w κ⇩₀›
1155      by (metis AOT_sem_concrete AOT_sem_dia AOT_sem_exe AOT_sem_lambda_beta)
1156    thus ‹∀w. [w ⊨ [Π'']κ⇩₀] = [w ⊨ [Π]κ⇩₀]›
1157      using Π''_prop
1158      by (metis AOT_sem_denotes AOT_sem_exe Π''_den Π_den)
1159  qed
1160  ultimately show ‹∃Π'. [v ⊨ Π'↓] ∧ [v ⊨ κ'[Π']] ∧
1161                         (∀κ⇩₀. [v ⊨ [λx ◇[E!]x]κ⇩₀] ⟶
1162                               (∀w. [w ⊨ [Π']κ⇩₀] = [w ⊨ [Π]κ⇩₀]))›
1163    by (safe intro!: exI[where x=Π'']) blast+
1164qed
1165end
1166
1167text‹Define encoding for products using projection-encoding.›
1168instantiation prod :: (AOT_UnaryEnc, AOT_Enc) AOT_Enc
1169begin
1170definition AOT_proj_enc_prod :: ‹'a×'b ⇒ ('a×'b ⇒ 𝗈) ⇒ 𝗈› where
1171  ‹AOT_proj_enc_prod ≡ λ (κ,κ') φ . «κ[λν «φ (ν,κ')»] &
1172                                     «AOT_proj_enc κ' (λν. φ (κ,ν))»»›
1173definition AOT_enc_prod :: ‹'a×'b ⇒ <'a×'b> ⇒ 𝗈› where
1174  ‹AOT_enc_prod ≡ λ κ Π . «Π↓ & «AOT_proj_enc κ (λ κ⇩₁'κ⇩_n'.  «[Π]κ⇩₁'...κ⇩_n'»)»»›
1175instance proof
1176  show ‹[v ⊨ κ⇩₁...κ⇩_n[Π]] ⟹ [v ⊨ κ⇩₁...κ⇩_n↓] ∧ [v ⊨ Π↓]›
1177    for v and κ⇩₁κ⇩_n :: ‹'a×'b› and Π
1178    unfolding AOT_enc_prod_def
1179    apply (induct κ⇩₁κ⇩_n; simp add: AOT_sem_conj AOT_sem_denotes AOT_proj_enc_prod_def)
1180    by (metis AOT_sem_denotes AOT_model_denotes_prod_def AOT_sem_enc_denotes
1181              AOT_sem_proj_enc_denotes case_prodI)
1182next
1183  show ‹[v ⊨ κ⇩₁...κ⇩_n[Π]] =
1184        [v ⊨ «Π»↓ & «AOT_proj_enc κ⇩₁κ⇩_n (λ κ⇩₁κ⇩_n.  «[Π]κ⇩₁...κ⇩_n»)»]›
1185    for v and κ⇩₁κ⇩_n :: ‹'a×'b› and Π
1186    unfolding AOT_enc_prod_def ..
1187next
1188  show ‹[v ⊨ «AOT_proj_enc κs φ»] ⟹ [v ⊨ «κs»↓]›
1189    for v and κs :: ‹'a×'b› and φ
1190    by (metis (mono_tags, lifting)
1191          AOT_sem_conj AOT_sem_denotes AOT_model_denotes_prod_def
1192          AOT_sem_enc_denotes AOT_sem_proj_enc_denotes
1193          AOT_proj_enc_prod_def case_prod_unfold)
1194next
1195  fix v w Π and κ⇩₁κ⇩_n :: ‹'a×'b›
1196  show ‹[w ⊨ κ⇩₁...κ⇩_n[Π]]› if ‹[v ⊨ κ⇩₁...κ⇩_n[Π]]› for v w Π and κ⇩₁κ⇩_n :: ‹'a×'b›
1197    by (metis (mono_tags, lifting)
1198          AOT_enc_prod_def AOT_sem_enc_proj_enc AOT_sem_conj AOT_sem_denotes
1199          AOT_sem_proj_enc_nec AOT_proj_enc_prod_def case_prod_unfold that)
1200next
1201  show ‹[w ⊨ «AOT_proj_enc κ⇩₁κ⇩_n φ»]› if ‹[v ⊨ «AOT_proj_enc κ⇩₁κ⇩_n φ»]›
1202    for v w φ and κ⇩₁κ⇩_n :: ‹'a×'b›
1203    by (metis (mono_tags, lifting)
1204          that AOT_sem_enc_proj_enc AOT_sem_conj AOT_sem_denotes
1205          AOT_sem_proj_enc_nec AOT_proj_enc_prod_def case_prod_unfold)
1206next
1207  fix v
1208  obtain κ :: 'a where a_prop: ‹[v ⊨ κ↓] ∧ (∀ Π . [v ⊨ Π↓] ⟶  [v ⊨ κ[Π]])›
1209    using AOT_sem_universal_encoder by blast
1210  obtain κ⇩₁'κ⇩_n' :: 'b where b_prop:
1211    ‹[v ⊨ κ⇩₁'...κ⇩_n'↓] ∧ (∀ φ . [v ⊨ [λν⇩₁...ν⇩_n «φ ν⇩₁ν⇩_n»]↓] ⟶
1212                                [v ⊨ «AOT_proj_enc κ⇩₁'κ⇩_n' φ»])›
1213    using AOT_sem_universal_encoder by blast
1214  have ‹AOT_model_denotes «[λν⇩₁...ν⇩_n [«Π»]ν⇩₁...ν⇩_n κ⇩₁'...κ⇩_n']»›
1215    if ‹AOT_model_denotes Π› for Π :: ‹<'a×'b>›
1216    unfolding AOT_model_lambda_denotes
1217    by (metis AOT_meta_prod_equivI(2) AOT_sem_exe_equiv)
1218  moreover have ‹AOT_model_denotes  «[λν⇩₁...ν⇩_n [«Π»]κ ν⇩₁...ν⇩_n]»›
1219    if ‹AOT_model_denotes Π› for Π :: ‹<'a×'b>›
1220    unfolding AOT_model_lambda_denotes
1221    by (metis AOT_meta_prod_equivI(1) AOT_sem_exe_equiv)
1222  ultimately have 1: ‹[v ⊨ «(κ,κ⇩₁'κ⇩_n')»↓]›
1223              and 2: ‹(∀ Π . [v ⊨ Π↓] ⟶  [v ⊨ κ κ⇩₁'...κ⇩_n'[Π]])›
1224    using a_prop b_prop
1225    by (auto simp: AOT_sem_denotes AOT_enc_κ_meta AOT_model_enc_κ_def
1226                   AOT_model_denotes_κ_def AOT_model_denotes_prod_def
1227                   AOT_enc_prod_def AOT_proj_enc_prod_def AOT_sem_conj)
1228  have ‹AOT_model_denotes «[λz⇩₁...z⇩_n «φ (z⇩₁z⇩_n, κ⇩₁'κ⇩_n')»]»›
1229    if ‹AOT_model_denotes «[λz⇩₁...z⇩_m φ{z⇩₁...z⇩_m}]»› for φ :: ‹'a×'b ⇒ 𝗈›
1230    using that
1231    unfolding AOT_model_lambda_denotes
1232    by (metis (no_types, lifting) AOT_sem_denotes AOT_model_denotes_prod_def
1233                                  AOT_meta_prod_equivI(2) b_prop case_prodI)
1234  moreover have ‹AOT_model_denotes «[λz⇩₁...z⇩_n «φ (κ, z⇩₁z⇩_n)»]»›
1235    if ‹AOT_model_denotes «[λz⇩₁...z⇩_m φ{z⇩₁...z⇩_m}]»› for φ :: ‹'a×'b ⇒ 𝗈›
1236    using that
1237    unfolding AOT_model_lambda_denotes
1238    by (metis (no_types, lifting) AOT_sem_denotes AOT_model_denotes_prod_def
1239                                  AOT_meta_prod_equivI(1) a_prop case_prodI)
1240  ultimately have 3:
1241    ‹[v ⊨ «(κ,κ⇩₁'κ⇩_n')»↓] ∧ (∀ φ . [v ⊨ [λz⇩₁...z⇩_n φ{z⇩₁...z⇩_n}]↓] ⟶
1242                                   [v ⊨ «AOT_proj_enc (κ,κ⇩₁'κ⇩_n') φ»])›
1243    using a_prop b_prop
1244    by (auto simp: AOT_sem_denotes AOT_enc_κ_meta AOT_model_enc_κ_def
1245                   AOT_model_denotes_κ_def AOT_enc_prod_def AOT_proj_enc_prod_def
1246                   AOT_sem_conj AOT_model_denotes_prod_def)
1247  show ‹∃κ⇩₁κ⇩_n::'a×'b. [v ⊨ κ⇩₁...κ⇩_n↓] ∧ (∀ Π . [v ⊨ Π↓] ⟶ [v ⊨ κ⇩₁...κ⇩_n[Π]]) ∧
1248                      (∀ φ . [v ⊨ [λz⇩₁...z⇩_n «φ z⇩₁z⇩_n»]↓] ⟶
1249                             [v ⊨ «AOT_proj_enc κ⇩₁κ⇩_n φ»])›
1250    apply (rule exI[where x=‹(κ,κ⇩₁'κ⇩_n')›]) using 1 2 3 by blast
1251qed
1252end
1253
1254text‹Sanity-check to verify that n-ary encoding follows.›
1255lemma ‹[v ⊨ κ⇩₁κ⇩₂[Π]] = [v ⊨ Π↓ & κ⇩₁[λν [Π]νκ⇩₂] & κ⇩₂[λν [Π]κ⇩₁ν]]›
1256  for κ⇩₁ :: "'a::AOT_UnaryEnc" and κ⇩₂ :: "'b::AOT_UnaryEnc"
1257  by (simp add: AOT_sem_conj AOT_enc_prod_def AOT_proj_enc_prod_def
1258                AOT_sem_unary_proj_enc)
1259lemma ‹[v ⊨ κ⇩₁κ⇩₂κ⇩₃[Π]] =
1260       [v ⊨ Π↓ & κ⇩₁[λν [Π]νκ⇩₂κ⇩₃] & κ⇩₂[λν [Π]κ⇩₁νκ⇩₃] & κ⇩₃[λν [Π]κ⇩₁κ⇩₂ν]]›
1261  for κ⇩₁ κ⇩₂ κ⇩₃ :: "'a::AOT_UnaryEnc"
1262  by (simp add: AOT_sem_conj AOT_enc_prod_def AOT_proj_enc_prod_def
1263                AOT_sem_unary_proj_enc)
1264
1265lemma AOT_sem_vars_denote: ‹[v ⊨ α⇩₁...α⇩_n↓]›
1266  by induct simp
1267
1268text‹Combine the introduced type classes and register them as
1269     type constraints for individual terms.›
1270class AOT_κs = AOT_IndividualTerm + AOT_RelationProjection + AOT_Enc
1271class AOT_κ = AOT_κs + AOT_UnaryIndividualTerm +
1272  AOT_UnaryRelationProjection + AOT_UnaryEnc
1273
1274instance κ :: AOT_κ by standard
1275instance prod :: (AOT_κ, AOT_κs) AOT_κs by standard
1276
1277AOT_register_type_constraints
1278  Individual: ‹_::AOT_κ› ‹_::AOT_κs› and
1279  Relation: ‹<_::AOT_κs>›
1280
1281text‹We define semantic predicates to capture the conditions of cqt.2 (i.e.
1282     the base cases of denoting terms) on matrices of @{text λ}-expressions.›
1283definition AOT_instance_of_cqt_2 :: ‹('a::AOT_κs ⇒ 𝗈) ⇒ bool› where
1284  ‹AOT_instance_of_cqt_2 ≡ λ φ . ∀ x y . AOT_model_denotes x ∧ AOT_model_denotes y ∧
1285                                          AOT_model_term_equiv x y ⟶ φ x = φ y›
1286definition AOT_instance_of_cqt_2_exe_arg :: ‹('a::AOT_κs ⇒ 'b::AOT_κs) ⇒ bool› where
1287  ‹AOT_instance_of_cqt_2_exe_arg ≡ λ φ . ∀ x y .
1288      AOT_model_denotes x ∧ AOT_model_denotes y ∧ AOT_model_term_equiv x y ⟶
1289      AOT_model_term_equiv (φ x) (φ y)›
1290
1291text‹@{text λ}-expressions with a matrix that satisfies our predicate denote.›
1292lemma AOT_sem_cqt_2:
1293  assumes ‹AOT_instance_of_cqt_2 φ›
1294  shows ‹[v ⊨ [λν⇩₁...ν⇩_n φ{ν⇩₁...ν⇩_n}]↓]›
1295  using assms
1296  by (metis AOT_instance_of_cqt_2_def AOT_model_lambda_denotes AOT_sem_denotes)
1297
1298syntax AOT_instance_of_cqt_2 :: ‹id_position ⇒ AOT_prop›
1299  ("INSTANCE'_OF'_CQT'_2'(_')")
1300
1301text‹Prove introduction rules for the predicates that match the natural language
1302     restrictions of the axiom.›
1303named_theorems AOT_instance_of_cqt_2_intro
1304lemma AOT_instance_of_cqt_2_intros_const[AOT_instance_of_cqt_2_intro]:
1305  ‹AOT_instance_of_cqt_2 (λα. φ)›
1306  by (simp add: AOT_instance_of_cqt_2_def AOT_sem_denotes AOT_model_lambda_denotes)
1307lemma AOT_instance_of_cqt_2_intros_not[AOT_instance_of_cqt_2_intro]:
1308  assumes ‹AOT_instance_of_cqt_2 φ›
1309  shows ‹AOT_instance_of_cqt_2 (λτ. «¬φ{τ}»)›
1310  using assms
1311  by (metis (no_types, lifting) AOT_instance_of_cqt_2_def)
1312lemma AOT_instance_of_cqt_2_intros_imp[AOT_instance_of_cqt_2_intro]:
1313  assumes ‹AOT_instance_of_cqt_2 φ› and ‹AOT_instance_of_cqt_2 ψ›
1314  shows ‹AOT_instance_of_cqt_2 (λτ. «φ{τ} → ψ{τ}»)›
1315  using assms
1316  by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes
1317                 AOT_model_lambda_denotes AOT_sem_imp)
1318lemma AOT_instance_of_cqt_2_intros_box[AOT_instance_of_cqt_2_intro]:
1319  assumes ‹AOT_instance_of_cqt_2 φ›
1320  shows ‹AOT_instance_of_cqt_2 (λτ. «□φ{τ}»)›
1321  using assms
1322  by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes
1323                 AOT_model_lambda_denotes AOT_sem_box)
1324lemma AOT_instance_of_cqt_2_intros_act[AOT_instance_of_cqt_2_intro]:
1325  assumes ‹AOT_instance_of_cqt_2 φ›
1326  shows ‹AOT_instance_of_cqt_2 (λτ. «❙𝒜φ{τ}»)›
1327  using assms
1328  by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes
1329                 AOT_model_lambda_denotes AOT_sem_act)
1330lemma AOT_instance_of_cqt_2_intros_diamond[AOT_instance_of_cqt_2_intro]:
1331  assumes ‹AOT_instance_of_cqt_2 φ›
1332  shows ‹AOT_instance_of_cqt_2 (λτ. «◇φ{τ}»)›
1333  using assms
1334  by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes
1335                 AOT_model_lambda_denotes AOT_sem_dia)
1336lemma AOT_instance_of_cqt_2_intros_conj[AOT_instance_of_cqt_2_intro]:
1337  assumes ‹AOT_instance_of_cqt_2 φ› and ‹AOT_instance_of_cqt_2 ψ›
1338  shows ‹AOT_instance_of_cqt_2 (λτ. «φ{τ} & ψ{τ}»)›
1339  using assms
1340  by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes
1341                 AOT_model_lambda_denotes AOT_sem_conj)
1342lemma AOT_instance_of_cqt_2_intros_disj[AOT_instance_of_cqt_2_intro]:
1343  assumes ‹AOT_instance_of_cqt_2 φ› and ‹AOT_instance_of_cqt_2 ψ›
1344  shows ‹AOT_instance_of_cqt_2 (λτ. «φ{τ} ∨ ψ{τ}»)›
1345  using assms
1346  by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes
1347                 AOT_model_lambda_denotes AOT_sem_disj)
1348lemma AOT_instance_of_cqt_2_intros_equib[AOT_instance_of_cqt_2_intro]:
1349  assumes ‹AOT_instance_of_cqt_2 φ› and ‹AOT_instance_of_cqt_2 ψ›
1350  shows ‹AOT_instance_of_cqt_2 (λτ. «φ{τ} ≡ ψ{τ}»)›
1351  using assms
1352  by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes
1353                 AOT_model_lambda_denotes AOT_sem_equiv)
1354lemma AOT_instance_of_cqt_2_intros_forall[AOT_instance_of_cqt_2_intro]:
1355  assumes ‹⋀ α . AOT_instance_of_cqt_2 (Φ α)›
1356  shows ‹AOT_instance_of_cqt_2 (λτ. «∀α Φ{α,τ}»)›
1357  using assms
1358  by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes
1359                 AOT_model_lambda_denotes AOT_sem_forall)
1360lemma AOT_instance_of_cqt_2_intros_exists[AOT_instance_of_cqt_2_intro]:
1361  assumes ‹⋀ α . AOT_instance_of_cqt_2 (Φ α)›
1362  shows ‹AOT_instance_of_cqt_2 (λτ. «∃α Φ{α,τ}»)›
1363  using assms
1364  by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes
1365                 AOT_model_lambda_denotes AOT_sem_exists)
1366lemma AOT_instance_of_cqt_2_intros_exe_arg_self[AOT_instance_of_cqt_2_intro]:
1367   ‹AOT_instance_of_cqt_2_exe_arg (λx. x)›
1368  unfolding AOT_instance_of_cqt_2_exe_arg_def AOT_instance_of_cqt_2_def
1369            AOT_sem_lambda_denotes
1370  by (auto simp: AOT_model_term_equiv_part_equivp equivp_reflp AOT_sem_denotes)
1371lemma AOT_instance_of_cqt_2_intros_exe_arg_const[AOT_instance_of_cqt_2_intro]:
1372     ‹AOT_instance_of_cqt_2_exe_arg (λx. κ)›
1373  unfolding AOT_instance_of_cqt_2_exe_arg_def AOT_instance_of_cqt_2_def
1374  by (auto simp: AOT_model_term_equiv_part_equivp equivp_reflp
1375                 AOT_sem_denotes AOT_sem_lambda_denotes)
1376lemma AOT_instance_of_cqt_2_intros_exe_arg_fst[AOT_instance_of_cqt_2_intro]:
1377   ‹AOT_instance_of_cqt_2_exe_arg fst›
1378  unfolding AOT_instance_of_cqt_2_exe_arg_def AOT_instance_of_cqt_2_def
1379  by (simp add: AOT_model_term_equiv_prod_def case_prod_beta)
1380lemma AOT_instance_of_cqt_2_intros_exe_arg_snd[AOT_instance_of_cqt_2_intro]:
1381   ‹AOT_instance_of_cqt_2_exe_arg snd›
1382  unfolding AOT_instance_of_cqt_2_exe_arg_def AOT_instance_of_cqt_2_def
1383  by (simp add: AOT_model_term_equiv_prod_def AOT_sem_denotes AOT_sem_lambda_denotes)
1384lemma AOT_instance_of_cqt_2_intros_exe_arg_Pair[AOT_instance_of_cqt_2_intro]:
1385  assumes ‹AOT_instance_of_cqt_2_exe_arg φ› and ‹AOT_instance_of_cqt_2_exe_arg ψ›
1386  shows ‹AOT_instance_of_cqt_2_exe_arg (λτ. Pair (φ τ) (ψ τ))›
1387  using assms
1388  unfolding AOT_instance_of_cqt_2_exe_arg_def AOT_instance_of_cqt_2_def
1389            AOT_sem_denotes AOT_sem_lambda_denotes AOT_model_term_equiv_prod_def
1390            AOT_model_denotes_prod_def
1391  by auto
1392lemma AOT_instance_of_cqt_2_intros_desc[AOT_instance_of_cqt_2_intro]:
1393  assumes ‹⋀z :: 'a::AOT_κ. AOT_instance_of_cqt_2 (Φ z)›
1394  shows ‹AOT_instance_of_cqt_2_exe_arg (λ κ :: 'b::AOT_κ . «❙ιz(Φ{z,κ})»)›
1395proof -
1396  have 0: ‹⋀ κ κ'. AOT_model_denotes κ ∧ AOT_model_denotes κ' ∧
1397                   AOT_model_term_equiv κ κ' ⟹
1398                   Φ z κ = Φ z κ'› for z
1399    using assms
1400    unfolding AOT_instance_of_cqt_2_def
1401              AOT_sem_denotes AOT_model_lambda_denotes by force
1402  {
1403    fix κ κ'
1404    have ‹«❙ιz(Φ{z,κ})» = «❙ιz(Φ{z,κ'})»›
1405      if ‹AOT_model_denotes κ ∧ AOT_model_denotes κ' ∧ AOT_model_term_equiv κ κ'›
1406      using 0[OF that]
1407      by auto
1408    moreover have ‹AOT_model_term_equiv x x› for x :: ‹'a::AOT_κ›
1409      by (metis AOT_instance_of_cqt_2_exe_arg_def
1410                AOT_instance_of_cqt_2_intros_exe_arg_const
1411                AOT_model_A_objects AOT_model_term_equiv_denotes
1412                AOT_model_term_equiv_eps(1))
1413    ultimately have ‹AOT_model_term_equiv «❙ιz(Φ{z,κ})» «❙ιz(Φ{z,κ'})»›
1414      if ‹AOT_model_denotes κ ∧ AOT_model_denotes κ' ∧ AOT_model_term_equiv κ κ'›
1415      using that by simp
1416  }
1417  thus ?thesis using 0
1418    unfolding AOT_instance_of_cqt_2_exe_arg_def
1419    by simp
1420qed
1421
1422lemma AOT_instance_of_cqt_2_intros_exe_const[AOT_instance_of_cqt_2_intro]:
1423  assumes ‹AOT_instance_of_cqt_2_exe_arg κs›
1424  shows ‹AOT_instance_of_cqt_2 (λx :: 'b::AOT_κs. AOT_exe Π (κs x))›
1425  using assms
1426  unfolding AOT_instance_of_cqt_2_def AOT_sem_denotes AOT_model_lambda_denotes
1427            AOT_sem_disj AOT_sem_conj
1428            AOT_sem_not AOT_sem_box AOT_sem_act AOT_instance_of_cqt_2_exe_arg_def
1429            AOT_sem_equiv AOT_sem_imp AOT_sem_forall AOT_sem_exists AOT_sem_dia
1430  by (auto intro!: AOT_sem_exe_equiv)
1431lemma AOT_instance_of_cqt_2_intros_exe_lam[AOT_instance_of_cqt_2_intro]:
1432  assumes ‹⋀ y . AOT_instance_of_cqt_2 (λx. φ x y)›
1433      and ‹AOT_instance_of_cqt_2_exe_arg κs›
1434    shows ‹AOT_instance_of_cqt_2 (λκ⇩₁κ⇩_n :: 'b::AOT_κs.
1435              «[λν⇩₁...ν⇩_n φ{κ⇩₁...κ⇩_n,ν⇩₁...ν⇩_n}]«κs κ⇩₁κ⇩_n»»)›
1436proof -
1437  {
1438    fix x y :: 'b
1439    assume ‹AOT_model_denotes x›
1440    moreover assume ‹AOT_model_denotes y›
1441    moreover assume ‹AOT_model_term_equiv x y›
1442    moreover have 1: ‹φ x = φ y›
1443      using assms calculation unfolding AOT_instance_of_cqt_2_def by blast
1444    ultimately have ‹AOT_exe (AOT_lambda (φ x)) (κs x) =
1445                     AOT_exe (AOT_lambda (φ y)) (κs y)›
1446      unfolding 1
1447      apply (safe intro!: AOT_sem_exe_equiv)
1448      by (metis AOT_instance_of_cqt_2_exe_arg_def assms(2))
1449  }
1450  thus ?thesis
1451  unfolding AOT_instance_of_cqt_2_def
1452            AOT_instance_of_cqt_2_exe_arg_def
1453  by blast
1454qed
1455lemma AOT_instance_of_cqt_2_intro_prod[AOT_instance_of_cqt_2_intro]:
1456  assumes ‹⋀ x . AOT_instance_of_cqt_2 (φ x)›
1457      and ‹⋀ x . AOT_instance_of_cqt_2 (λ z . φ z x)›
1458  shows ‹AOT_instance_of_cqt_2 (λ(x,y) . φ x y)›
1459  using assms unfolding AOT_instance_of_cqt_2_def
1460  by (auto simp add: AOT_model_lambda_denotes AOT_sem_denotes
1461                AOT_model_denotes_prod_def
1462                AOT_model_term_equiv_prod_def)
1463
1464text‹The following are already derivable semantically, but not yet added
1465     to @{attribute AOT_instance_of_cqt_2_intro}. They will be added with the
1466     next planned extension of axiom cqt:2.›
1467named_theorems AOT_instance_of_cqt_2_intro_next
1468definition AOT_instance_of_cqt_2_enc_arg :: ‹('a::AOT_κs ⇒ 'b::AOT_κs) ⇒ bool› where
1469  ‹AOT_instance_of_cqt_2_enc_arg ≡ λ φ . ∀ x y z .
1470      AOT_model_denotes x ∧ AOT_model_denotes y ∧ AOT_model_term_equiv x y ⟶
1471      AOT_enc (φ x) z = AOT_enc (φ y) z›
1472definition AOT_instance_of_cqt_2_enc_rel :: ‹('a::AOT_κs ⇒ <'b::AOT_κs>) ⇒ bool› where
1473  ‹AOT_instance_of_cqt_2_enc_rel ≡ λ φ . ∀ x y z .
1474      AOT_model_denotes x ∧ AOT_model_denotes y ∧ AOT_model_term_equiv x y ⟶
1475      AOT_enc z (φ x) = AOT_enc z (φ y)›
1476lemma AOT_instance_of_cqt_2_intros_enc[AOT_instance_of_cqt_2_intro_next]:
1477  assumes ‹AOT_instance_of_cqt_2_enc_rel Π› and ‹AOT_instance_of_cqt_2_enc_arg κs›
1478  shows ‹AOT_instance_of_cqt_2 (λx . AOT_enc (κs x) «[«Π x»]»)›
1479  using assms
1480  unfolding AOT_instance_of_cqt_2_def AOT_sem_denotes AOT_model_lambda_denotes
1481            AOT_instance_of_cqt_2_enc_rel_def AOT_sem_not AOT_sem_box AOT_sem_act
1482            AOT_sem_dia AOT_sem_conj AOT_sem_disj AOT_sem_equiv AOT_sem_imp
1483            AOT_sem_forall AOT_sem_exists AOT_instance_of_cqt_2_enc_arg_def
1484  by fastforce+
1485lemma AOT_instance_of_cqt_2_enc_arg_intro_const[AOT_instance_of_cqt_2_intro_next]:
1486  ‹AOT_instance_of_cqt_2_enc_arg (λx. c)›
1487  unfolding AOT_instance_of_cqt_2_enc_arg_def by simp
1488lemma AOT_instance_of_cqt_2_enc_arg_intro_desc[AOT_instance_of_cqt_2_intro_next]:
1489  assumes ‹⋀z :: 'a::AOT_κ. AOT_instance_of_cqt_2 (Φ z)›
1490  shows ‹AOT_instance_of_cqt_2_enc_arg (λ κ :: 'b::AOT_κ . «❙ιz(Φ{z,κ})»)›
1491proof -
1492  have 0: ‹⋀ κ κ'. AOT_model_denotes κ ∧ AOT_model_denotes κ' ∧
1493                   AOT_model_term_equiv κ κ' ⟹
1494                   Φ z κ = Φ z κ'› for z
1495    using assms
1496    unfolding AOT_instance_of_cqt_2_def
1497              AOT_sem_denotes AOT_model_lambda_denotes by force
1498  {
1499    fix κ κ'
1500    have ‹«❙ιz(Φ{z,κ})» = «❙ιz(Φ{z,κ'})»›
1501      if ‹AOT_model_denotes κ ∧ AOT_model_denotes κ' ∧ AOT_model_term_equiv κ κ'›
1502      using 0[OF that]
1503      by auto
1504  }
1505  thus ?thesis using 0
1506    unfolding AOT_instance_of_cqt_2_enc_arg_def by meson
1507qed
1508lemma AOT_instance_of_cqt_2_enc_rel_intro[AOT_instance_of_cqt_2_intro_next]:
1509  assumes ‹⋀ κ . AOT_instance_of_cqt_2 (λκ' :: 'b::AOT_κs . φ κ κ')›
1510  assumes ‹⋀ κ' . AOT_instance_of_cqt_2 (λκ :: 'a::AOT_κs . φ κ κ')›
1511  shows ‹AOT_instance_of_cqt_2_enc_rel (λκ :: 'a::AOT_κs. AOT_lambda (λκ'. φ κ κ'))›
1512proof -
1513  {
1514    fix x y :: 'a and z ::'b
1515    assume ‹AOT_model_term_equiv x y›
1516    moreover assume ‹AOT_model_denotes x›
1517    moreover assume ‹AOT_model_denotes y›
1518    ultimately have ‹φ x = φ y›
1519      using assms unfolding AOT_instance_of_cqt_2_def by blast
1520    hence ‹AOT_enc z (AOT_lambda (φ x)) = AOT_enc z (AOT_lambda (φ y))›
1521      by simp
1522  }
1523  thus ?thesis
1524    unfolding AOT_instance_of_cqt_2_enc_rel_def by auto
1525qed
1526
1527text‹Further restrict unary individual variables to type @{typ κ} (rather
1528     than class @{class AOT_κ} only) and define being ordinary and being abstract.›
1529AOT_register_type_constraints
1530  Individual: ‹κ› ‹_::AOT_κs›
1531
1532AOT_define AOT_ordinary :: ‹Π› (‹O!›) ‹O! =⇩_d⇩_f [λx ◇E!x]›
1533declare AOT_ordinary[AOT del, AOT_defs del]
1534AOT_define AOT_abstract :: ‹Π› (‹A!›) ‹A! =⇩_d⇩_f [λx ¬◇E!x]›
1535declare AOT_abstract[AOT del, AOT_defs del]
1536
1537context AOT_meta_syntax
1538begin
1539notation AOT_ordinary ("❙O❙!")
1540notation AOT_abstract ("❙A❙!")
1541end
1542context AOT_no_meta_syntax
1543begin
1544no_notation AOT_ordinary ("❙O❙!")
1545no_notation AOT_abstract ("❙A❙!")
1546end
1547
1548no_translations
1549  "_AOT_concrete" => "CONST AOT_term_of_var (CONST AOT_concrete)"
1550parse_translation‹
1551[(\<^syntax_const>‹_AOT_concrete›, fn _ => fn [] =>
1552  Const (\<^const_name>‹AOT_term_of_var›, dummyT)
1553  $ Const (\<^const_name>‹AOT_concrete›, \<^typ>‹<κ> AOT_var›))]
1554›
1555
1556text‹Auxiliary lemmata.›
1557lemma AOT_sem_ordinary: "«O!» = «[λx ◇E!x]»"
1558  using AOT_ordinary[THEN AOT_sem_id_def0E1] AOT_sem_ordinary_def_denotes
1559  by (auto simp: AOT_sem_eq)
1560lemma AOT_sem_abstract: "«A!» = «[λx ¬◇E!x]»"
1561  using AOT_abstract[THEN AOT_sem_id_def0E1]  AOT_sem_abstract_def_denotes
1562  by (auto simp: AOT_sem_eq)
1563lemma AOT_sem_ordinary_denotes: ‹[w ⊨ O!↓]›
1564  by (simp add: AOT_sem_ordinary AOT_sem_ordinary_def_denotes)
1565lemma AOT_meta_abstract_denotes: ‹[w ⊨ A!↓]›
1566  by (simp add: AOT_sem_abstract AOT_sem_abstract_def_denotes)
1567lemma AOT_model_abstract_ακ: ‹∃ a . κ = ακ a› if ‹[v ⊨ A!κ]›
1568  using that[unfolded AOT_sem_abstract, simplified
1569      AOT_meta_abstract_denotes[unfolded AOT_sem_abstract, THEN AOT_sem_lambda_beta,
1570          OF that[simplified AOT_sem_exe, THEN conjunct2, THEN conjunct1]]]
1571  apply (simp add: AOT_sem_not AOT_sem_dia AOT_sem_concrete)
1572  by (metis AOT_model_ω_concrete_in_some_world AOT_model_concrete_κ.simps(1)
1573            AOT_model_denotes_κ_def AOT_sem_denotes AOT_sem_exe κ.exhaust_disc
1574            is_ακ_def is_ωκ_def that)
1575lemma AOT_model_ordinary_ωκ: ‹∃ a . κ = ωκ a› if ‹[v ⊨ O!κ]›
1576  using that[unfolded AOT_sem_ordinary, simplified
1577      AOT_sem_ordinary_denotes[unfolded AOT_sem_ordinary, THEN AOT_sem_lambda_beta,
1578        OF that[simplified AOT_sem_exe, THEN conjunct2, THEN conjunct1]]]
1579  apply (simp add: AOT_sem_dia AOT_sem_concrete)
1580  by (metis AOT_model_concrete_κ.simps(2) AOT_model_concrete_κ.simps(3)
1581            κ.exhaust_disc is_ακ_def is_ωκ_def is_nullκ_def)
1582lemma AOT_model_ωκ_ordinary: ‹[v ⊨ O!«ωκ x»]›
1583  by (metis AOT_model_abstract_ακ AOT_model_denotes_κ_def AOT_sem_abstract
1584            AOT_sem_denotes AOT_sem_ind_eq AOT_sem_ordinary κ.disc(7) κ.distinct(1))
1585lemma AOT_model_ακ_ordinary: ‹[v ⊨ A!«ακ x»]›
1586  by (metis AOT_model_denotes_κ_def AOT_model_ordinary_ωκ AOT_sem_abstract
1587            AOT_sem_denotes AOT_sem_ind_eq AOT_sem_ordinary κ.disc(8) κ.distinct(1))
1588AOT_theorem prod_denotesE: assumes ‹«(κ⇩₁,κ⇩₂)»↓› shows ‹κ⇩₁↓ & κ⇩₂↓›
1589  using assms by (simp add: AOT_sem_denotes AOT_sem_conj AOT_model_denotes_prod_def)
1590declare prod_denotesE[AOT del]
1591AOT_theorem prod_denotesI: assumes ‹κ⇩₁↓ & κ⇩₂↓› shows ‹«(κ⇩₁,κ⇩₂)»↓›
1592  using assms by (simp add: AOT_sem_denotes AOT_sem_conj AOT_model_denotes_prod_def)
1593declare prod_denotesI[AOT del]
1594
1595
1596text‹Prepare the derivation of the additional axioms that are validated by
1597     our extended models.›
1598locale AOT_ExtendedModel =
1599  assumes AOT_ExtendedModel: ‹AOT_ExtendedModel›
1600begin
1601lemma AOT_sem_indistinguishable_ord_enc_all:
1602  assumes Π_den: ‹[v ⊨ Π↓]›
1603  assumes Ax: ‹[v ⊨ A!x]›
1604  assumes Ay: ‹[v ⊨ A!y]›
1605  assumes indist: ‹[v ⊨ ∀F □([F]x ≡ [F]y)]›
1606  shows
1607  ‹[v ⊨ ∀G(∀z(O!z → □([G]z ≡ [Π]z)) → x[G])] =
1608   [v ⊨ ∀G(∀z(O!z → □([G]z ≡ [Π]z)) → y[G])]›
1609proof -
1610    have 0: ‹[v ⊨ [λx ¬◇[E!]x]x]›
1611      using Ax by (simp add: AOT_sem_abstract)
1612    have 1: ‹[v ⊨ [λx ¬◇[E!]x]y]›
1613      using Ay by (simp add: AOT_sem_abstract)
1614    {
1615      assume ‹[v ⊨ ∀G(∀z (O!z → □([G]z ≡ [Π]z)) → x[G])]›
1616      hence 3: ‹[v ⊨ ∀G(∀z([λx ◇[E!]x]z → □([G]z ≡ [Π]z)) → x[G])]›
1617        by (simp add: AOT_sem_ordinary)
1618      {
1619        fix Π' :: ‹<κ>›
1620        assume 1: ‹[v ⊨ Π'↓]›
1621        assume 2: ‹[v ⊨ [λx ◇[E!]x]z → □([Π']z ≡ [Π]z)]› for z
1622        have ‹[v ⊨ x[Π']]›
1623          using 3
1624          by (auto simp: AOT_sem_forall AOT_sem_imp AOT_sem_box AOT_sem_denotes)
1625             (metis (no_types, lifting) 1 2 AOT_term_of_var_cases AOT_sem_box
1626                                        AOT_sem_denotes AOT_sem_imp)
1627      } note 3 = this
1628      fix Π' :: ‹<κ>›
1629      assume Π_den: ‹[v ⊨ Π'↓]›
1630      assume 4: ‹[v ⊨ ∀z (O!z → □([Π']z ≡ [Π]z))]›
1631      {
1632        fix κ⇩₀
1633        assume ‹[v ⊨ [λx ◇[E!]x]κ⇩₀]›
1634        hence ‹[v ⊨ O!κ⇩₀]›
1635          using AOT_sem_ordinary by metis
1636        moreover have ‹[v ⊨ κ⇩₀↓]›
1637          using calculation by (simp add: AOT_sem_exe)
1638        ultimately have ‹[v ⊨ □([Π']κ⇩₀ ≡ [Π]κ⇩₀)]›
1639          using 4 by (auto simp: AOT_sem_forall AOT_sem_imp)
1640      } note 4 = this
1641      {
1642        fix Π'' :: ‹<κ>›
1643        assume ‹[v ⊨ Π''↓]›
1644        moreover assume ‹[w ⊨ [Π'']κ⇩₀] = [w ⊨ [Π']κ⇩₀]› if ‹[v ⊨ [λx ◇E!x]κ⇩₀]› for κ⇩₀ w
1645        ultimately have 5: ‹[v ⊨ x[Π'']]›
1646          using 4 3
1647          by (auto simp: AOT_sem_imp AOT_sem_equiv AOT_sem_box)
1648      } note 5 = this
1649      have ‹[v ⊨ y[Π']]›
1650        apply (rule AOT_sem_enc_indistinguishable_all[OF AOT_ExtendedModel])
1651        apply (fact 0)
1652        by (auto simp: 5 0 1 Π_den indist[simplified AOT_sem_forall
1653                       AOT_sem_box AOT_sem_equiv])
1654    }
1655    moreover {
1656    {
1657      assume ‹[v ⊨ ∀G(∀z (O!z → □([G]z ≡ [Π]z)) → y[G])]›
1658      hence 3: ‹[v ⊨ ∀G(∀z ([λx ◇[E!]x]z → □([G]z ≡ [Π]z)) → y[G])]›
1659        by (simp add: AOT_sem_ordinary)
1660      {
1661        fix Π' :: ‹<κ>›
1662        assume 1: ‹[v ⊨ Π'↓]›
1663        assume 2: ‹[v ⊨ [λx ◇[E!]x]z → □([Π']z ≡ [Π]z)]› for z
1664        have ‹[v ⊨ y[Π']]›
1665          using 3
1666          apply (simp add: AOT_sem_forall AOT_sem_imp AOT_sem_box AOT_sem_denotes)
1667          by (metis (no_types, lifting) 1 2 AOT_model.AOT_term_of_var_cases
1668                                        AOT_sem_box AOT_sem_denotes AOT_sem_imp)
1669      } note 3 = this
1670      fix Π' :: ‹<κ>›
1671      assume Π_den: ‹[v ⊨ Π'↓]›
1672      assume 4: ‹[v ⊨ ∀z (O!z → □([Π']z ≡ [Π]z))]›
1673      {
1674        fix κ⇩₀
1675        assume ‹[v ⊨ [λx ◇[E!]x]κ⇩₀]›
1676        hence ‹[v ⊨ O!κ⇩₀]›
1677          using AOT_sem_ordinary by metis
1678        moreover have ‹[v ⊨ κ⇩₀↓]›
1679          using calculation by (simp add: AOT_sem_exe)
1680        ultimately have ‹[v ⊨ □([Π']κ⇩₀ ≡ [Π]κ⇩₀)]›
1681          using 4 by (auto simp: AOT_sem_forall AOT_sem_imp)
1682      } note 4 = this
1683      {
1684        fix Π'' :: ‹<κ>›
1685        assume ‹[v ⊨ Π''↓]›
1686        moreover assume ‹[w ⊨ [Π'']κ⇩₀] = [w ⊨ [Π']κ⇩₀]› if ‹[v ⊨ [λx ◇E!x]κ⇩₀]› for w κ⇩₀
1687        ultimately have ‹[v ⊨ y[Π'']]›
1688          using 3 4 by (auto simp: AOT_sem_imp AOT_sem_equiv AOT_sem_box)
1689      } note 5 = this
1690      have ‹[v ⊨ x[Π']]›
1691        apply (rule AOT_sem_enc_indistinguishable_all[OF AOT_ExtendedModel])
1692              apply (fact 1)
1693        by (auto simp: 5 0 1 Π_den indist[simplified AOT_sem_forall
1694                       AOT_sem_box AOT_sem_equiv])
1695    }
1696  }
1697  ultimately show ‹[v ⊨ ∀G (∀z (O!z → □([G]z ≡ [Π]z)) → x[G])] =
1698        [v ⊨ ∀G (∀z (O!z → □([G]z ≡ [Π]z)) → y[G])]›
1699    by (auto simp: AOT_sem_forall AOT_sem_imp)
1700qed
1701
1702lemma AOT_sem_indistinguishable_ord_enc_ex:
1703  assumes Π_den: ‹[v ⊨ Π↓]›
1704  assumes Ax: ‹[v ⊨ A!x]›
1705  assumes Ay: ‹[v ⊨ A!y]›
1706  assumes indist: ‹[v ⊨ ∀F □([F]x ≡ [F]y)]›
1707  shows ‹[v ⊨ ∃G(∀z (O!z → □([G]z ≡ [Π]z)) & x[G])] =
1708         [v ⊨ ∃G(∀z(O!z → □([G]z ≡ [Π]z)) & y[G])]›
1709proof -
1710  have Aux: ‹[v ⊨ [λx ◇[E!]x]κ] = ([v ⊨ [λx ◇[E!]x]κ] ∧ [v ⊨ κ↓])› for v κ
1711    using AOT_sem_exe by blast
1712  AOT_modally_strict {
1713    fix x y
1714    AOT_assume Π_den: ‹[Π]↓›
1715    AOT_assume 2: ‹∀F □([F]x ≡ [F]y)›
1716    AOT_assume ‹A!x›
1717    AOT_hence 0: ‹[λx ¬◇[E!]x]x›
1718      by (simp add: AOT_sem_abstract)
1719    AOT_assume ‹A!y›
1720    AOT_hence 1: ‹[λx ¬◇[E!]x]y›
1721      by (simp add: AOT_sem_abstract)
1722    {
1723      AOT_assume ‹∃G(∀z (O!z → □([G]z ≡ [Π]z)) & x[G])›
1724      then AOT_obtain Π'
1725        where Π'_den: ‹Π'↓›
1726          and Π'_indist: ‹∀z (O!z → □([Π']z ≡ [Π]z))›
1727          and x_enc_Π': ‹x[Π']›
1728        by (meson AOT_sem_conj AOT_sem_exists)
1729      {
1730        fix κ⇩₀
1731        AOT_assume ‹[λx ◇[E!]x]κ⇩₀›
1732        AOT_hence ‹□([Π']κ⇩₀ ≡ [Π]κ⇩₀)›
1733          using Π'_indist
1734          by (auto simp: AOT_sem_exe AOT_sem_imp AOT_sem_exists AOT_sem_conj
1735                         AOT_sem_ordinary AOT_sem_forall)
1736      } note 3 = this
1737      AOT_have ‹∀z ([λx ◇[E!]x]z → □([Π']z ≡ [Π]z))›
1738        using Π'_indist by (simp add: AOT_sem_ordinary)
1739      AOT_obtain Π'' where
1740          Π''_den: ‹Π''↓› and
1741          Π''_indist: ‹[λx ◇[E!]x]κ⇩₀ → □([Π'']κ⇩₀ ≡ [Π]κ⇩₀)› and
1742          y_enc_Π'': ‹y[Π'']› for κ⇩₀
1743        using AOT_sem_enc_indistinguishable_ex[OF AOT_ExtendedModel,
1744                OF 0, OF 1, rotated, OF Π_den,
1745                OF exI[where x=Π'], OF conjI, OF Π'_den, OF conjI,
1746                OF x_enc_Π', OF allI, OF impI,
1747                OF 3[simplified AOT_sem_box AOT_sem_equiv], simplified, OF
1748                2[simplified AOT_sem_forall AOT_sem_equiv AOT_sem_box,
1749                  THEN spec, THEN mp, THEN spec], simplified]
1750        unfolding AOT_sem_imp AOT_sem_box AOT_sem_equiv by blast
1751      {
1752        AOT_have ‹Π''↓›
1753            and ‹∀x ([λx ◇[E!]x]x → □([Π'']x ≡ [Π]x))›
1754            and ‹y[Π'']›
1755          apply (simp add: Π''_den)
1756          apply (simp add: AOT_sem_forall Π''_indist)
1757          by (simp add: y_enc_Π'')
1758      } note 2 = this
1759      AOT_have ‹∃G(∀z (O!z → □([G]z ≡ [Π]z)) & y[G])›
1760        apply (simp add: AOT_sem_exists AOT_sem_ordinary
1761            AOT_sem_imp AOT_sem_box AOT_sem_forall AOT_sem_equiv AOT_sem_conj)
1762        using 2[simplified AOT_sem_box AOT_sem_equiv AOT_sem_imp AOT_sem_forall]
1763        by blast
1764    }
1765  } note 0 = this
1766  AOT_modally_strict {
1767    {
1768      fix x y
1769      AOT_assume Π_den: ‹[Π]↓›
1770      moreover AOT_assume ‹∀F □([F]x ≡ [F]y)›
1771      moreover AOT_have ‹∀F □([F]y ≡ [F]x)›
1772        using calculation(2)
1773        by (auto simp: AOT_sem_forall AOT_sem_box AOT_sem_equiv)
1774      moreover AOT_assume ‹A!x›
1775      moreover AOT_assume ‹A!y›
1776      ultimately AOT_have ‹∃G (∀z (O!z → □([G]z ≡ [Π]z)) & x[G]) ≡
1777                           ∃G (∀z (O!z → □([G]z ≡ [Π]z)) & y[G])›
1778        using 0 by (auto simp: AOT_sem_equiv)
1779    }
1780    have 1: ‹[v ⊨ ∀F □([F]y ≡ [F]x)]›
1781      using indist
1782      by (auto simp: AOT_sem_forall AOT_sem_box AOT_sem_equiv)
1783    thus ‹[v ⊨ ∃G (∀z (O!z → □([G]z ≡ [Π]z)) & x[G])] =
1784        [v ⊨ ∃G (∀z (O!z → □([G]z ≡ [Π]z)) & y[G])]›
1785      using assms
1786      by (auto simp: AOT_sem_imp AOT_sem_conj AOT_sem_equiv 0)
1787  }
1788qed
1789end
1790
1791
1792(* Collect all theorems that are not in Main and not declared [AOT]
1793   and store them in a blacklist. *)
1794setup‹setup_AOT_no_atp›
1795bundle AOT_no_atp begin declare AOT_no_atp[no_atp] end
1796(* Can be used as: "including AOT_no_atp sledgehammer" or
1797   "sledgehammer(del: AOT_no_atp) *)
1798
1799(*<*)
1800end
1801(*>*)