Theory AOT_semantics

1(*<*)
2theory AOT_semantics
3  imports AOT_syntax
4begin
5(*>*)
6
7sectionAbstract 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  𝒜φ] = [w0  φ]
41  by (rule exI[where x=λ φ . ε𝗈 w . [w0  φ]])
42     (simp add: AOT_model_proposition_choice_simp)
43
44textDerived 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})] = (∃! κ . [w0  κ]  [w0  φ{κ}])
76  ― ‹Denoting descriptions satisfy their matrix in the actual world.
77  AOT_sem_desc_prop: [w  ιx(φ{x})]  [w0  φ{ιx(φ{x})}]
78  ― ‹Uniqueness of denoting descriptions.
79  AOT_sem_desc_unique: [w  ιx(φ{x})]  [w  κ]  [w0  φ{κ}] 
80                        [w  ιx(φ{x}) = κ]
81proof -
82  have x::'a . ¬AOT_model_denotes x
83    using AOT_model_nondenoting_ex
84    by blast
85  textNote 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 (∃! κ . [w0  κ]  [w0  φ{κ}])
93                   then (THE κ . [w0  κ]  [w0  φ{κ}])
94                   else nondenoting φ)
95  {
96    fix φ :: 'a  𝗈
97    assume ex1: ∃! κ . [w0  κ]  [w0  φ{κ}]
98    then obtain κ where x_prop: "[w0  κ]  [w0  φ{κ}]"
99      unfolding AOT_sem_denotes by blast
100    moreover have "(desc φ) = κ"
101      unfolding desc_def using x_prop ex1 by fastforce
102    ultimately have "[w0  «desc φ»]  [w0  «φ (desc φ)»]"
103      by blast
104  } note 1 = this
105  moreover {
106    fix φ :: 'a  𝗈
107    assume nex1: ∄! κ . [w0  κ]  [w0  φ{κ}]
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 φ»] = (∃! κ . [w0  κ]  [w0  φ{κ}]) for φ w
114    by (simp add: AOT_sem_denotes desc_def nondenoting)
115  have (φ w. [w  «desc φ»] = (∃!κ. [w0  κ]  [w0  φ{κ}])) 
116    (φ w. [w  «desc φ»]  [w0  «φ (desc φ)»]) 
117    (φ w κ. [w  «desc φ»]  [w  κ]  [w0  φ{κ}] 
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  [Π]κ1...κn] = ([w  Π]  [w  κ1...κn] 
129                                     [w  «Rep_rel Π κ1κn»])
130  ― ‹η-conversion for denoting terms; equivalent to AOT's axiom
131  AOT_sem_lambda_eta: [w  Π]  [w  ν1...νn [Π]ν1...νn] = Π]
132  ― ‹β-conversion; equivalent to AOT's axiom
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  ― ‹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  ν1...νn φ{ν1...νn}]] =
139    ( v κ1κn κ1n' . [v  κ1...κn]  [v  κ1'...κn'] 
140        ( Π v . [v  Π]  [v  [Π]κ1...κn] = [v  [Π]κ1'...κn']) 
141                 [v  φ{κ1...κn}] = [v  φ{κ1'...κn'}])
142  ― ‹Equivalent to AOT's coexistence axiom.
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  ― ‹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: «ν1...νn φ]» = «ν1...ν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 Π κ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 κ1n' . [v  κ1...κn]  [v  κ1'...κn'] 
207        ( Π v . [v  Π]  [v  «exe Π κ1κn»] = [v  «exe Π κ1n'»]) 
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 κ1n' . [v  κ1...κn]  [v  κ1'...κn'] 
220        ( Π v . [v  Π]  [v  «exe Π κ1κn»] = [v  «exe Π κ1n'»]) 
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 κ1n' . [v  κ1...κn]  [v  κ1'...κn'] 
226      ( Π v . [v  Π]  [v  «exe Π κ1κn»] = [v  «exe Π κ1n'»]) 
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 κ1n' 
278        (Π v. AOT_model_denotes Π  [v  [Π]κ1...κn] = [v  [Π]κ1'...κn']) 
279        [v  φ{κ1...κn}] = [v  φ{κ1'...κn'}] for κ1κn κ1n' v
280    using AOT_sem_lambda_denotes[simplified AOT_sem_denotes] by blast
281  {
282    fix v and κ1κn κ1n' :: 'a
283    assume d: AOT_model_denotes κ1κn  AOT_model_denotes κ1n' 
284               AOT_model_term_equiv κ1κn κ1n'
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 κ1n' :: 'a
300    assume den: AOT_model_denotes κ1κn
301    moreover assume den': AOT_model_denotes κ1n'
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 Π κ1n'»]
306      by (simp add: AOT_sem_denotes AOT_sem_exe den den')
307    hence "AOT_model_term_equiv κ1κn κ1n'"
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
405textRelation 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  textThis 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 (auto simp: Abs_rel_inverse AOT_meta_prod_equivI(2) AOT_sem_denotes
459                      that intro!: AOT_sem_exe_equiv)
460    apply (metis AOT_model_denotes_prod_def AOT_sem_exe case_prodD)
461    using AOT_model_unary_regular by blast
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 κ1n'
470               if [w  [Π]κ κ1'...κn'] for w κ1n'
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 κ1n' :: 'b and Π :: <'a×'b>
505    assume Π_denotes: AOT_model_denotes Π
506    assume β_denotes: AOT_model_denotes κ1n'
507    hence AOT_exe Π (x, κ1n') = AOT_exe Π (y, κ1n')
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,κ1n') = AOT_model_irregular (λz. AOT_exe Π (z,κ1n')) 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,κ1n')))
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 κ1n' :: 'b
548      assume Π = Π'
549      assume AOT_model_denotes (κ,κ1n')
550      hence AOT_model_denotes κ and beta_denotes: AOT_model_denotes κ1n'
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 κ1n' (λκ1n'. «[Π]κ κ1'...κn'»)
560                                                  (λκ1n'. «[Π']κ κ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 (κ,κ1n') (λ κ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 κ1n' 
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 κ1n' (λκ1κn. «[Π]κ κ1...κn»)
579                                          (λκ1κn. «[Π']κ κ1...κn»)»] for κ κ1n'
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 κ1n' (λκ1n'. «[Π]κ κ1'...κn'»)
590                                              (λκ1n'. «[Π']κ κ1'...κn'»)»]
591          if AOT_model_denotes κ1n' for κ1n'
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 κ1n' :: 'b
617        assume βden: AOT_model_denotes κ1n'
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, κ1n')) =
621               Abs_rel (λz. Rep_rel Π' (z, κ1n')) (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,κ1n') = Rep_rel Π' (x,κ1n') 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  z1...zn «φ z1zn»] = z1...zn «φ z1zn»]]
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
687textSanity-check to verify that n-ary relation identity follows.
688lemma [v  Π = Π'] = [v  Π & Π' & xy(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  Π & Π' & x1x2x3 (
695  z [Π]z x2 x3] = z [Π']z x2 x3] &
696  z [Π]x1 z x3] = z [Π']x1 z x3] &
697  z [Π]x1 x2 z] = z [Π']x1 x2 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  Π & Π' & x1x2x3x4 (
703    z [Π]z x2 x3 x4] = z [Π']z x2 x3 x4] &
704    z [Π]x1 z x3 x4] = z [Π']x1 z x3 x4] &
705    z [Π]x1 x2 z x4] = z [Π']x1 x2 z x4] &
706    z [Π]x1 x2 x3 z] = z [Π']x1 x2 x3 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
712textn-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  z1...zn φ{z1...zn}]]  [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
744textUnary 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  Π']  ( κ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
783textWe 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
793textWe 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
852textWe 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    ( κ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
1167textDefine 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 κ (λ κ1n'.  «[Π]κ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 κ1n' :: 'b where b_prop:
1211    [v  κ1'...κn']  ( φ . [v  ν1...νn «φ ν1νn»]] 
1212                                [v  «AOT_proj_enc κ1n' φ»])
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  «(κ,κ1n')»]
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 «z1...zn «φ (z1zn, κ1n')»]»
1229    if AOT_model_denotes «z1...zm φ{z1...zm}]» 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 «z1...zn «φ (κ, z1zn)»]»
1235    if AOT_model_denotes «z1...zm φ{z1...zm}]» 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  «(κ,κ1n')»]  ( φ . [v  z1...zn φ{z1...zn}]] 
1242                                   [v  «AOT_proj_enc (κ,κ1n') φ»])
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  z1...zn «φ z1zn»]] 
1249                             [v  «AOT_proj_enc κ1κn φ»])
1250    apply (rule exI[where x=(κ,κ1n')]) using 1 2 3 by blast
1251qed
1252end
1253
1254textSanity-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
1268textCombine 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
1281textWe 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
1301textProve 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