Theory AOT_semantics
1
2theory AOT_semantics
3 imports AOT_syntax
4begin
5
6
7section‹Abstract Semantics for AOT›
8
9specification(AOT_denotes)
10
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⇩0 ⊨ φ]›
41 by (rule exI[where x=‹λ φ . ε⇩𝗈 w . [w⇩0 ⊨ φ]›])
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
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
75 AOT_sem_desc_denotes: ‹[w ⊨ ❙ιx(φ{x})↓] = (∃! κ . [w⇩0 ⊨ κ↓] ∧ [w⇩0 ⊨ φ{κ}])›
76
77 AOT_sem_desc_prop: ‹[w ⊨ ❙ιx(φ{x})↓] ⟹ [w⇩0 ⊨ φ{❙ιx(φ{x})}]›
78
79 AOT_sem_desc_unique: ‹[w ⊨ ❙ιx(φ{x})↓] ⟹ [w ⊨ κ↓] ⟹ [w⇩0 ⊨ φ{κ}] ⟹
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⇩0 ⊨ κ↓] ∧ [w⇩0 ⊨ φ{κ}])
93 then (THE κ . [w⇩0 ⊨ κ↓] ∧ [w⇩0 ⊨ φ{κ}])
94 else nondenoting φ)›
95 {
96 fix φ :: ‹'a ⇒ 𝗈›
97 assume ex1: ‹∃! κ . [w⇩0 ⊨ κ↓] ∧ [w⇩0 ⊨ φ{κ}]›
98 then obtain κ where x_prop: "[w⇩0 ⊨ κ↓] ∧ [w⇩0 ⊨ φ{κ}]"
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⇩0 ⊨ «desc φ»↓] ∧ [w⇩0 ⊨ «φ (desc φ)»]"
103 by blast
104 } note 1 = this
105 moreover {
106 fix φ :: ‹'a ⇒ 𝗈›
107 assume nex1: ‹∄! κ . [w⇩0 ⊨ κ↓] ∧ [w⇩0 ⊨ φ{κ}]›
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⇩0 ⊨ κ↓] ∧ [w⇩0 ⊨ φ{κ}])› for φ w
114 by (simp add: AOT_sem_denotes desc_def nondenoting)
115 have ‹(∀φ w. [w ⊨ «desc φ»↓] = (∃!κ. [w⇩0 ⊨ κ↓] ∧ [w⇩0 ⊨ φ{κ}])) ∧
116 (∀φ w. [w ⊨ «desc φ»↓] ⟶ [w⇩0 ⊨ «φ (desc φ)»]) ∧
117 (∀φ w κ. [w ⊨ «desc φ»↓] ⟶ [w ⊨ κ↓] ⟶ [w⇩0 ⊨ φ{κ}] ⟶
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
128 AOT_sem_exe: ‹[w ⊨ [Π]κ⇩1...κ⇩n] = ([w ⊨ Π↓] ∧ [w ⊨ κ⇩1...κ⇩n↓] ∧
129 [w ⊨ «Rep_rel Π κ⇩1κ⇩n»])›
130
131 AOT_sem_lambda_eta: ‹[w ⊨ Π↓] ⟹ [w ⊨ [λν⇩1...ν⇩n [Π]ν⇩1...ν⇩n] = Π]›
132
133 AOT_sem_lambda_beta: ‹[w ⊨ [λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}]↓] ⟹ [w ⊨ κ⇩1...κ⇩n↓] ⟹
134 [w ⊨ [λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}]κ⇩1...κ⇩n] = [w ⊨ φ{κ⇩1...κ⇩n}]›
135
138 AOT_sem_lambda_denotes: ‹[w ⊨ [λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}]↓] =
139 (∀ v κ⇩1κ⇩n κ⇩1'κ⇩n' . [v ⊨ κ⇩1...κ⇩n↓] ∧ [v ⊨ κ⇩1'...κ⇩n'↓] ∧
140 (∀ Π v . [v ⊨ Π↓] ⟶ [v ⊨ [Π]κ⇩1...κ⇩n] = [v ⊨ [Π]κ⇩1'...κ⇩n']) ⟶
141 [v ⊨ φ{κ⇩1...κ⇩n}] = [v ⊨ φ{κ⇩1'...κ⇩n'}])›
142
143 AOT_sem_lambda_coex: ‹[w ⊨ [λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}]↓] ⟹
144 (∀ w κ⇩1κ⇩n . [w ⊨ κ⇩1...κ⇩n↓] ⟶ [w ⊨ φ{κ⇩1...κ⇩n}] = [w ⊨ ψ{κ⇩1...κ⇩n}]) ⟹
145 [w ⊨ [λν⇩1...ν⇩n ψ{ν⇩1...ν⇩n}]↓]›
146
149 AOT_sem_lambda_eq_prop_eq: ‹«[λν⇩1...ν⇩n φ]» = «[λν⇩1...ν⇩n ψ]» ⟹ φ = ψ›
150
153 AOT_sem_exe_denoting: ‹[w ⊨ Π↓] ⟹ AOT_exe Π κs = Rep_rel Π κs›
154
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 Π κ⇩1κ⇩n»] = ([w ⊨ Π↓] ∧ [w ⊨ κ⇩1...κ⇩n↓] ∧
193 [w ⊨ «Rep_rel Π κ⇩1κ⇩n»])› for w Π κ⇩1κ⇩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 κ⇩1κ⇩n κ⇩1'κ⇩n' . [v ⊨ κ⇩1...κ⇩n↓] ∧ [v ⊨ κ⇩1'...κ⇩n'↓] ∧
207 (∀ Π v . [v ⊨ Π↓] ⟶ [v ⊨ «exe Π κ⇩1κ⇩n»] = [v ⊨ «exe Π κ⇩1'κ⇩n'»]) ⟶
208 [v ⊨ φ{κ⇩1...κ⇩n}] = [v ⊨ φ{κ⇩1'...κ⇩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 κ⇩1κ⇩n κ⇩1'κ⇩n' . [v ⊨ κ⇩1...κ⇩n↓] ∧ [v ⊨ κ⇩1'...κ⇩n'↓] ∧
220 (∀ Π v . [v ⊨ Π↓] ⟶ [v ⊨ «exe Π κ⇩1κ⇩n»] = [v ⊨ «exe Π κ⇩1'κ⇩n'»]) ⟶
221 [v ⊨ φ{κ⇩1...κ⇩n}] = [v ⊨ φ{κ⇩1'...κ⇩n'}]›
222 unfolding AOT_sem_denotes
223 by (metis (no_types) AOT_sem_denotes lambda_denotes_beta)
224 next
225 assume ‹∀ v κ⇩1κ⇩n κ⇩1'κ⇩n' . [v ⊨ κ⇩1...κ⇩n↓] ∧ [v ⊨ κ⇩1'...κ⇩n'↓] ∧
226 (∀ Π v . [v ⊨ Π↓] ⟶ [v ⊨ «exe Π κ⇩1κ⇩n»] = [v ⊨ «exe Π κ⇩1'κ⇩n'»]) ⟶
227 [v ⊨ φ{κ⇩1...κ⇩n}] = [v ⊨ φ{κ⇩1'...κ⇩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 κ⇩1κ⇩n . [w ⊨ κ⇩1...κ⇩n↓] ⟶ [w ⊨ φ{κ⇩1...κ⇩n}] = [w ⊨ ψ{κ⇩1...κ⇩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 κ⇩1κ⇩n ∧
277 AOT_model_denotes κ⇩1'κ⇩n' ∧
278 (∀Π v. AOT_model_denotes Π ⟶ [v ⊨ [Π]κ⇩1...κ⇩n] = [v ⊨ [Π]κ⇩1'...κ⇩n']) ⟶
279 [v ⊨ φ{κ⇩1...κ⇩n}] = [v ⊨ φ{κ⇩1'...κ⇩n'}]› for κ⇩1κ⇩n κ⇩1'κ⇩n' v
280 using AOT_sem_lambda_denotes[simplified AOT_sem_denotes] by blast
281 {
282 fix v and κ⇩1κ⇩n κ⇩1'κ⇩n' :: 'a
283 assume d: ‹AOT_model_denotes κ⇩1κ⇩n ∧ AOT_model_denotes κ⇩1'κ⇩n' ∧
284 AOT_model_term_equiv κ⇩1κ⇩n κ⇩1'κ⇩n'›
285 hence ‹∀Π w. AOT_model_denotes Π ⟶ [w ⊨ [Π]κ⇩1...κ⇩n] = [w ⊨ [Π]κ⇩1'...κ⇩n']›
286 by (metis AOT_sem_exe_equiv)
287 hence ‹[v ⊨ φ{κ⇩1...κ⇩n}] = [v ⊨ φ{κ⇩1'...κ⇩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 κ⇩1κ⇩n κ⇩1'κ⇩n' :: 'a
300 assume den: ‹AOT_model_denotes κ⇩1κ⇩n›
301 moreover assume den': ‹AOT_model_denotes κ⇩1'κ⇩n'›
302 assume ‹∀Π v . AOT_model_denotes Π ⟶
303 [v ⊨ [Π]κ⇩1...κ⇩n] = [v ⊨ [Π]κ⇩1'...κ⇩n']›
304 hence ‹∀Π v . AOT_model_denotes Π ⟶
305 [v ⊨ «Rep_rel Π κ⇩1κ⇩n»] = [v ⊨ «Rep_rel Π κ⇩1'κ⇩n'»]›
306 by (simp add: AOT_sem_denotes AOT_sem_exe den den')
307 hence "AOT_model_term_equiv κ⇩1κ⇩n κ⇩1'κ⇩n'"
308 unfolding AOT_model_term_equiv_rel_equiv[OF den, OF den']
309 by argo
310 hence ‹[v ⊨ φ{κ⇩1...κ⇩n}] = [v ⊨ φ{κ⇩1'...κ⇩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 ⊨ [λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}] = [λν⇩1...ν⇩n φ{ν⇩1...ν⇩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 κ φ ψ = «[λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}] = [λν⇩1...ν⇩n ψ{ν⇩1...ν⇩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 κ φ ψ = «[λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}] = [λν⇩1...ν⇩n ψ{ν⇩1...ν⇩n}]»›
433 for κ :: κ and φ ψ
434 unfolding AOT_sem_proj_id_κ_def ..
435next
436 show ‹[v ⊨ «AOT_sem_proj_id τ φ φ»]›
437 if ‹[v ⊨ τ↓]› and ‹[v ⊨ [λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}] = [λν⇩1...ν⇩n φ{ν⇩1...ν⇩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 κ⇩1'κ⇩n'›
470 if ‹[w ⊨ [Π]κ κ⇩1'...κ⇩n']› for w κ⇩1'κ⇩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 κ⇩1'κ⇩n' :: 'b and Π :: ‹<'a×'b>›
505 assume Π_denotes: ‹AOT_model_denotes Π›
506 assume β_denotes: ‹AOT_model_denotes κ⇩1'κ⇩n'›
507 hence ‹AOT_exe Π (x, κ⇩1'κ⇩n') = AOT_exe Π (y, κ⇩1'κ⇩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 ⊨ [Π]κ κ⇩1'...κ⇩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,κ⇩1'κ⇩n') = AOT_model_irregular (λz. AOT_exe Π (z,κ⇩1'κ⇩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,κ⇩1'κ⇩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 κ⇩1'κ⇩n' :: 'b
548 assume ‹Π = Π'›
549 assume ‹AOT_model_denotes (κ,κ⇩1'κ⇩n')›
550 hence ‹AOT_model_denotes κ› and beta_denotes: ‹AOT_model_denotes κ⇩1'κ⇩n'›
551 by (auto simp: AOT_model_denotes_prod_def)
552 have ‹AOT_model_denotes «[λz [Π]z κ⇩1'...κ⇩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 κ⇩1'...κ⇩n']» = «[λz [Π']z κ⇩1'...κ⇩n']»›
558 by (simp add: ‹Π = Π'›)
559 moreover have ‹[v ⊨ «AOT_sem_proj_id κ⇩1'κ⇩n' (λκ⇩1'κ⇩n'. «[Π]κ κ⇩1'...κ⇩n'»)
560 (λκ⇩1'κ⇩n'. «[Π']κ κ⇩1'...κ⇩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 (κ,κ⇩1'κ⇩n') (λ κ⇩1κ⇩n . «[Π]κ⇩1...κ⇩n»)
567 (λ κ⇩1κ⇩n . «[Π']κ⇩1...κ⇩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 α (λ κ⇩1κ⇩n . «[Π]κ⇩1...κ⇩n») (λ κ⇩1κ⇩n . «[Π']κ⇩1...κ⇩n»)»]›
574 hence 0: ‹AOT_model_denotes κ ⟹ AOT_model_denotes κ⇩1'κ⇩n' ⟹
575 AOT_model_denotes «[λz [Π]z κ⇩1'...κ⇩n']» ∧
576 AOT_model_denotes «[λz [Π']z κ⇩1'...κ⇩n']» ∧
577 «[λz [Π]z κ⇩1'...κ⇩n']» = «[λz [Π']z κ⇩1'...κ⇩n']» ∧
578 [v ⊨ «AOT_sem_proj_id κ⇩1'κ⇩n' (λκ⇩1κ⇩n. «[Π]κ κ⇩1...κ⇩n»)
579 (λκ⇩1κ⇩n. «[Π']κ κ⇩1...κ⇩n»)»]› for κ κ⇩1'κ⇩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 κ⇩1'κ⇩n' (λκ⇩1'κ⇩n'. «[Π]κ κ⇩1'...κ⇩n'»)
590 (λκ⇩1'κ⇩n'. «[Π']κ κ⇩1'...κ⇩n'»)»]›
591 if ‹AOT_model_denotes κ⇩1'κ⇩n'› for κ⇩1'κ⇩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 κ⇩1'κ⇩n' :: 'b
617 assume βden: ‹AOT_model_denotes κ⇩1'κ⇩n'›
618 have 1: ‹«[λz [Π]z κ⇩1'...κ⇩n']» = «[λz [Π']z κ⇩1'...κ⇩n']»›
619 using 0 βden AOT_model_denoting_ex by blast
620 hence ‹Abs_rel (λz. Rep_rel Π (z, κ⇩1'κ⇩n')) =
621 Abs_rel (λz. Rep_rel Π' (z, κ⇩1'κ⇩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,κ⇩1'κ⇩n') = Rep_rel Π' (x,κ⇩1'κ⇩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 κ (λ κ⇩1κ⇩n . «[Π]κ⇩1...κ⇩n»)
668 (λ κ⇩1κ⇩n . «[Π']κ⇩1...κ⇩n»)»])›
669 by auto
670 }
671 thus ‹[v ⊨ Π = Π'] = [v ⊨ Π↓ & Π'↓ &
672 ∀α («AOT_sem_proj_id α (λ κ⇩1κ⇩n . «[Π]κ⇩1...κ⇩n») (λ κ⇩1κ⇩n . «[Π']κ⇩1...κ⇩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⇩1...z⇩n «φ z⇩1z⇩n»] = [λz⇩1...z⇩n «φ z⇩1z⇩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⇩1∀x⇩2∀x⇩3 (
695 [λz [Π]z x⇩2 x⇩3] = [λz [Π']z x⇩2 x⇩3] &
696 [λz [Π]x⇩1 z x⇩3] = [λz [Π']x⇩1 z x⇩3] &
697 [λz [Π]x⇩1 x⇩2 z] = [λz [Π']x⇩1 x⇩2 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⇩1∀x⇩2∀x⇩3∀x⇩4 (
703 [λz [Π]z x⇩2 x⇩3 x⇩4] = [λz [Π']z x⇩2 x⇩3 x⇩4] &
704 [λz [Π]x⇩1 z x⇩3 x⇩4] = [λz [Π']x⇩1 z x⇩3 x⇩4] &
705 [λz [Π]x⇩1 x⇩2 z x⇩4] = [λz [Π']x⇩1 x⇩2 z x⇩4] &
706 [λz [Π]x⇩1 x⇩2 x⇩3 z] = [λz [Π']x⇩1 x⇩2 x⇩3 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 κ⇩1κ⇩n Π»] ⟹ [v ⊨ κ⇩1...κ⇩n↓] ∧ [v ⊨ Π↓]›
719 assumes AOT_sem_enc_proj_enc:
720 ‹[v ⊨ «AOT_enc κ⇩1κ⇩n Π»] =
721 [v ⊨ Π↓ & «AOT_proj_enc κ⇩1κ⇩n (λ κ⇩1κ⇩n. «[Π]κ⇩1...κ⇩n»)»]›
722 assumes AOT_sem_proj_enc_denotes:
723 ‹[v ⊨ «AOT_proj_enc κ⇩1κ⇩n φ»] ⟹ [v ⊨ κ⇩1...κ⇩n↓]›
724 assumes AOT_sem_enc_nec:
725 ‹[v ⊨ «AOT_enc κ⇩1κ⇩n Π»] ⟹ [w ⊨ «AOT_enc κ⇩1κ⇩n Π»]›
726 assumes AOT_sem_proj_enc_nec:
727 ‹[v ⊨ «AOT_proj_enc κ⇩1κ⇩n φ»] ⟹ [w ⊨ «AOT_proj_enc κ⇩1κ⇩n φ»]›
728 assumes AOT_sem_universal_encoder:
729 ‹∃ κ⇩1κ⇩n. [v ⊨ κ⇩1...κ⇩n↓] ∧ (∀ Π . [v ⊨ Π↓] ⟶ [v ⊨ «AOT_enc κ⇩1κ⇩n Π»]) ∧
730 (∀ φ . [v ⊨ [λz⇩1...z⇩n φ{z⇩1...z⇩n}]↓] ⟶ [v ⊨ «AOT_proj_enc κ⇩1κ⇩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
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 ⊨ Π'↓] ⟹ (⋀ κ⇩0 . [v ⊨ [λx ◇[E!]x]κ⇩0] ⟹
767 (⋀ w . [w ⊨ [Π']κ⇩0] = [w ⊨ [Π]κ⇩0])) ⟹ [v ⊨ κ[Π']]) ⟹
768 (⋀ Π' . [v ⊨ Π'↓] ⟹ (⋀ κ⇩0 . [v ⊨ [λx ◇[E!]x]κ⇩0] ⟹
769 (⋀ w . [w ⊨ [Π']κ⇩0] = [w ⊨ [Π]κ⇩0])) ⟹ [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 (∀ κ⇩0 . [v ⊨ [λx ◇[E!]x]κ⇩0] ⟶
778 (∀ w . [w ⊨ [Π']κ⇩0] = [w ⊨ [Π]κ⇩0])) ⟹
779 ∃ Π' . [v ⊨ Π'↓] ∧ [v ⊨ κ'[Π']] ∧
780 (∀ κ⇩0 . [v ⊨ [λx ◇[E!]x]κ⇩0] ⟶
781 (∀ w . [w ⊨ [Π']κ⇩0] = [w ⊨ [Π]κ⇩0]))›
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
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 (⋀ κ⇩0 w. [v ⊨ [λx ◇[E!]x]κ⇩0] ⟹
1013 [w ⊨ [Π']κ⇩0] = [w ⊨ [Π]κ⇩0]) ⟹
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 κ⇩0 :: κ and w
1027 assume ‹[v ⊨ [λx ◇[E!]x]κ⇩0]›
1028 hence ‹is_ωκ κ⇩0›
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: ‹κ⇩0 = ωκ 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 ⊨ [Π']κ⇩0] = [w ⊨ [Π]κ⇩0]› 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]κ⇩0] ⟹
1057 [w ⊨ [Π']κ⇩0] = [w ⊨ [Π]κ⇩0]› for κ⇩0 w
1058 {
1059 fix w and κ⇩0 :: κ
1060 assume 0: ‹∃w. AOT_model_concrete w κ⇩0›
1061 hence ‹[v ⊨ [λx ◇[E!]x]κ⇩0]›
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 ⊨ [Π']κ⇩0] = [w ⊨ [Π]κ⇩0]›
1065 using ord_indist by metis
1066 hence ‹[w ⊨ «Rep_rel Π' κ⇩0»] = [w ⊨ «Rep_rel Π κ⇩0»]›
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 (∀κ⇩0. [v ⊨ [λx ◇[E!]x]κ⇩0] ⟶
1107 (∀w. [w ⊨ [Π']κ⇩0] = [w ⊨ [Π]κ⇩0]))›
1108 then obtain Π' where
1109 Π'_den: ‹[v ⊨ Π'↓]› and
1110 Π'_enc: ‹[v ⊨ κ[Π']]› and
1111 Π'_prop: ‹∀κ⇩0. [v ⊨ [λx ◇[E!]x]κ⇩0] ⟶
1112 (∀w. [w ⊨ [Π']κ⇩0] = [w ⊨ [Π]κ⇩0])›
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 κ⇩0) ⟹
1119 [v ⊨ «Rep_rel Π' κ⇩0»] = [v ⊨ «Rep_rel Π κ⇩0»]› for κ⇩0 v
1120 proof -
1121 assume 0: ‹∃w. AOT_model_concrete w κ⇩0›
1122 hence ‹[v ⊨ [λx ◇[E!]x]κ⇩0]› 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 ⊨ [Π']κ⇩0] = [w ⊨ [Π]κ⇩0]› using Π'_prop by blast
1126 thus ‹[v ⊨ «Rep_rel Π' κ⇩0»] = [v ⊨ «Rep_rel Π κ⇩0»]›
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]κ⇩0] ⟹
1151 (∀w. [w ⊨ [Π'']κ⇩0] = [w ⊨ [Π]κ⇩0])› for κ⇩0
1152 proof -
1153 assume ‹[v ⊨ [λx ◇[E!]x]κ⇩0]›
1154 hence ‹∃w. AOT_model_concrete w κ⇩0›
1155 by (metis AOT_sem_concrete AOT_sem_dia AOT_sem_exe AOT_sem_lambda_beta)
1156 thus ‹∀w. [w ⊨ [Π'']κ⇩0] = [w ⊨ [Π]κ⇩0]›
1157 using Π''_prop
1158 by (metis AOT_sem_denotes AOT_sem_exe Π''_den Π_den)
1159 qed
1160 ultimately show ‹∃Π'. [v ⊨ Π'↓] ∧ [v ⊨ κ'[Π']] ∧
1161 (∀κ⇩0. [v ⊨ [λx ◇[E!]x]κ⇩0] ⟶
1162 (∀w. [w ⊨ [Π']κ⇩0] = [w ⊨ [Π]κ⇩0]))›
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 κ (λ κ⇩1'κ⇩n'. «[Π]κ⇩1'...κ⇩n'»)»»›
1175instance proof
1176 show ‹[v ⊨ κ⇩1...κ⇩n[Π]] ⟹ [v ⊨ κ⇩1...κ⇩n↓] ∧ [v ⊨ Π↓]›
1177 for v and κ⇩1κ⇩n :: ‹'a×'b› and Π
1178 unfolding AOT_enc_prod_def
1179 apply (induct κ⇩1κ⇩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 ⊨ κ⇩1...κ⇩n[Π]] =
1184 [v ⊨ «Π»↓ & «AOT_proj_enc κ⇩1κ⇩n (λ κ⇩1κ⇩n. «[Π]κ⇩1...κ⇩n»)»]›
1185 for v and κ⇩1κ⇩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 κ⇩1κ⇩n :: ‹'a×'b›
1196 show ‹[w ⊨ κ⇩1...κ⇩n[Π]]› if ‹[v ⊨ κ⇩1...κ⇩n[Π]]› for v w Π and κ⇩1κ⇩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 κ⇩1κ⇩n φ»]› if ‹[v ⊨ «AOT_proj_enc κ⇩1κ⇩n φ»]›
1202 for v w φ and κ⇩1κ⇩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 κ⇩1'κ⇩n' :: 'b where b_prop:
1211 ‹[v ⊨ κ⇩1'...κ⇩n'↓] ∧ (∀ φ . [v ⊨ [λν⇩1...ν⇩n «φ ν⇩1ν⇩n»]↓] ⟶
1212 [v ⊨ «AOT_proj_enc κ⇩1'κ⇩n' φ»])›
1213 using AOT_sem_universal_encoder by blast
1214 have ‹AOT_model_denotes «[λν⇩1...ν⇩n [«Π»]ν⇩1...ν⇩n κ⇩1'...κ⇩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 «[λν⇩1...ν⇩n [«Π»]κ ν⇩1...ν⇩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 ⊨ «(κ,κ⇩1'κ⇩n')»↓]›
1223 and 2: ‹(∀ Π . [v ⊨ Π↓] ⟶ [v ⊨ κ κ⇩1'...κ⇩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⇩1...z⇩n «φ (z⇩1z⇩n, κ⇩1'κ⇩n')»]»›
1229 if ‹AOT_model_denotes «[λz⇩1...z⇩m φ{z⇩1...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⇩1...z⇩n «φ (κ, z⇩1z⇩n)»]»›
1235 if ‹AOT_model_denotes «[λz⇩1...z⇩m φ{z⇩1...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 ⊨ «(κ,κ⇩1'κ⇩n')»↓] ∧ (∀ φ . [v ⊨ [λz⇩1...z⇩n φ{z⇩1...z⇩n}]↓] ⟶
1242 [v ⊨ «AOT_proj_enc (κ,κ⇩1'κ⇩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 ‹∃κ⇩1κ⇩n::'a×'b. [v ⊨ κ⇩1...κ⇩n↓] ∧ (∀ Π . [v ⊨ Π↓] ⟶ [v ⊨ κ⇩1...κ⇩n[Π]]) ∧
1248 (∀ φ . [v ⊨ [λz⇩1...z⇩n «φ z⇩1z⇩n»]↓] ⟶
1249 [v ⊨ «AOT_proj_enc κ⇩1κ⇩n φ»])›
1250 apply (rule exI[where x=‹(κ,κ⇩1'κ⇩n')›]) using 1 2 3 by blast
1251qed
1252end
1253
1254text‹Sanity-check to verify that n-ary encoding follows.›
1255lemma ‹[v ⊨ κ⇩1κ⇩2[Π]] = [v ⊨ Π↓ & κ⇩1[λν [Π]νκ⇩2] & κ⇩2[λν [Π]κ⇩1ν]]›
1256 for κ⇩1 :: "'a::AOT_UnaryEnc" and κ⇩2 :: "'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 ⊨ κ⇩1κ⇩2κ⇩3[Π]] =
1260 [v ⊨ Π↓ & κ⇩1[λν [Π]νκ⇩2κ⇩3] & κ⇩2[λν [Π]κ⇩1νκ⇩3] & κ⇩3[λν [Π]κ⇩1κ⇩2ν]]›
1261 for κ⇩1 κ⇩2 κ⇩3 :: "'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 ⊨ α⇩1...α⇩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 ⊨ [λν⇩1...ν⇩n φ{ν⇩1...ν⇩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 (λκ⇩1κ⇩n :: 'b::AOT_κs.
1435 «[λν⇩1...ν⇩n φ{κ⇩1...κ⇩n,ν⇩1...ν⇩n}]«κs κ⇩1κ⇩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 ‹«(κ⇩1,κ⇩2)»↓› shows ‹κ⇩1↓ & κ⇩2↓›
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 ‹κ⇩1↓ & κ⇩2↓› shows ‹«(κ⇩1,κ⇩2)»↓›
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 κ⇩0
1633 assume ‹[v ⊨ [λx ◇[E!]x]κ⇩0]›
1634 hence ‹[v ⊨ O!κ⇩0]›
1635 using AOT_sem_ordinary by metis
1636 moreover have ‹[v ⊨ κ⇩0↓]›
1637 using calculation by (simp add: AOT_sem_exe)
1638 ultimately have ‹[v ⊨ □([Π']κ⇩0 ≡ [Π]κ⇩0)]›
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 ⊨ [Π'']κ⇩0] = [w ⊨ [Π']κ⇩0]› if ‹[v ⊨ [λx ◇E!x]κ⇩0]› for κ⇩0 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 κ⇩0
1675 assume ‹[v ⊨ [λx ◇[E!]x]κ⇩0]›
1676 hence ‹[v ⊨ O!κ⇩0]›
1677 using AOT_sem_ordinary by metis
1678 moreover have ‹[v ⊨ κ⇩0↓]›
1679 using calculation by (simp add: AOT_sem_exe)
1680 ultimately have ‹[v ⊨ □([Π']κ⇩0 ≡ [Π]κ⇩0)]›
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 ⊨ [Π'']κ⇩0] = [w ⊨ [Π']κ⇩0]› if ‹[v ⊨ [λx ◇E!x]κ⇩0]› for w κ⇩0
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 κ⇩0
1731 AOT_assume ‹[λx ◇[E!]x]κ⇩0›
1732 AOT_hence ‹□([Π']κ⇩0 ≡ [Π]κ⇩0)›
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]κ⇩0 → □([Π'']κ⇩0 ≡ [Π]κ⇩0)› and
1742 y_enc_Π'': ‹y[Π'']› for κ⇩0
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
1794setup‹setup_AOT_no_atp›
1795bundle AOT_no_atp begin declare AOT_no_atp[no_atp] end
1796
1798
1799
1800end
1801