Theory AOT_model

1(*<*)
2theory AOT_model
3  imports Main "HOL-Cardinals.Cardinals"
4begin
5
6declare[[typedef_overloaded]]
7(*>*)
8
9sectionModel for the Logic of AOT
10
11textWe introduce a primitive type for hyperintensional propositions.
12typedecl 𝗈
13
14textTo be able to model modal operators following Kripke semantics,
15     we introduce a primitive type for possible worlds and assert, by axiom,
16     that there is a surjective function mapping propositions to the
17     boolean-valued functions acting on possible worlds. We call the result
18     of applying this function to a proposition the Kripke-extension
19     of the proposition.
20typedecl w ―‹The primtive type of possible worlds.
21axiomatization AOT_model_d𝗈 :: 𝗈(wbool) where
22  d𝗈_surj: surj AOT_model_d𝗈
23
24textThe axioms of PLM require the existence of a non-actual world.
25consts w0 :: w ―‹The designated actual world.
26axiomatization where AOT_model_nonactual_world: w . w  w0
27
28textValidity of a proposition in a given world can now be modelled as the result
29     of applying that world to the Kripke-extension of the proposition.
30definition AOT_model_valid_in :: w𝗈bool where
31  AOT_model_valid_in w φ  AOT_model_d𝗈 φ w
32
33textBy construction, we can choose a proposition for any given Kripke-extension,
34     s.t. the proposition is valid in a possible world iff the Kripke-extension
35     evaluates to true at that world.
36definition AOT_model_proposition_choice :: (wbool)  𝗈 (binder ε𝗈  8)
37  where ε𝗈 w. φ w  (inv AOT_model_d𝗈) φ
38lemma AOT_model_proposition_choice_simp: AOT_model_valid_in w (ε𝗈 w. φ w) = φ w
39  by (simp add: surj_f_inv_f[OF d𝗈_surj] AOT_model_valid_in_def
40                AOT_model_proposition_choice_def)
41
42textNitpick can trivially show that there are models for the axioms above.
43lemma True nitpick[satisfy, user_axioms, expect = genuine] ..
44
45typedecl ω ―‹The primtive type of ordinary objects/urelements.
46
47textValidating extended relation comprehension requires a large set of
48     special urelements. For simple models that do not validate extended
49     relation comprehension (and consequently the predecessor axiom in the
50     theory of natural numbers), it suffices to use a primitive type as @{text σ},
51     i.e. @{theory_text typedecl σ›}.
52typedecl σ'
53typedef σ = UNIV::((ω  w  bool) set × (ω  w  bool) set × σ') set ..
54
55typedecl null ― ‹Null-urelements representing non-denoting terms.
56
57datatype υ = ωυ ω | συ σ | is_nullυ: nullυ null ― ‹Type of urelements
58
59textUrrelations are proposition-valued functions on urelements.
60     Urrelations are required to evaluate to necessarily false propositions for
61     null-urelements (note that there may be several distinct necessarily false
62     propositions).
63typedef urrel = { φ .  x w . ¬AOT_model_valid_in w (φ (nullυ x)) }
64  by (rule exI[where x=λ x . (ε𝗈 w . ¬is_nullυ x)])
65     (auto simp: AOT_model_proposition_choice_simp)
66
67textAbstract objects will be modelled as sets of urrelations and will
68     have to be mapped surjectively into the set of special urelements.
69     We show that any mapping from abstract objects to special urelements
70     has to involve at least one large set of collapsed abstract objects.
71     We will use this fact to extend arbitrary mappings from abstract objects
72     to special urelements to surjective mappings.
73lemma ασ_pigeonhole:
74  ― ‹For any arbitrary mapping @{term ασ} from sets of urrelations to special
75     urelements, there exists an abstract object x, s.t. the cardinal of the set
76     of special urelements is strictly smaller than the cardinal of the set of
77     abstract objects that are mapped to the same urelement as x under @{term ασ}.
78  x . |UNIV::σ set| <o |{y . ασ x = ασ y}|
79  for ασ :: urrel set  σ
80proof(rule ccontr)
81  have card_σ_set_set_bound: |UNIV::σ set set| ≤o |UNIV::urrel set|
82  proof -
83    let ?pick = λu s . ε𝗈 w . case u of (συ s')  s'  s | _  False
84    have f :: σ set  urrel . inj f
85    proof
86      show inj (λs . Abs_urrel (λu . ?pick u s))
87      proof(rule injI)
88        fix x y
89        assume Abs_urrel (λu. ?pick u x) = Abs_urrel (λu. ?pick u y)
90        hence (λu. ?pick u x) = (λu. ?pick u y)
91          by (auto intro!: Abs_urrel_inject[THEN iffD1]
92                     simp: AOT_model_proposition_choice_simp)
93        hence AOT_model_valid_in w0 (?pick (συ s) x) =
94               AOT_model_valid_in w0 (?pick (συ s) y)
95          for s by metis
96        hence (s  x) = (s  y) for s
97          by (auto simp: AOT_model_proposition_choice_simp)
98        thus x = y
99          by blast
100      qed
101    qed
102    thus ?thesis
103      by (metis card_of_image inj_imp_surj_inv)
104  qed
105
106  textAssume, for a proof by contradiction, that there is no large collapsed set.
107  assume x . |UNIV::σ set| <o |{y . ασ x = ασ y}|
108  hence A: x . |{y . ασ x = ασ y}| ≤o |UNIV::σ set|
109    by auto
110  have union_univ: (x  range(inv ασ) . {y . ασ x = ασ y}) = UNIV
111    by auto (meson f_inv_into_f range_eqI)
112
113  textWe refute by case distinction: there is either finitely many or
114       infinitely many special urelements and in both cases we can derive
115       a contradiction from the assumption above.
116  {
117    textFinite case.
118    assume finite_σ_set: finite (UNIV::σ set)
119    hence finite_collapsed: finite {y . ασ x = ασ y} for x
120      using A card_of_ordLeq_infinite by blast
121    hence 0: x . card {y . ασ x = ασ y}  card (UNIV::σ set)
122      by (metis A finite_σ_set card_of_ordLeq inj_on_iff_card_le)
123    have 1: card (range (inv ασ))  card (UNIV::σ set)
124      using finite_σ_set card_image_le by blast
125    hence 2: finite (range (inv ασ))
126      using finite_σ_set by blast
127
128    define n where n = card (UNIV::urrel set set)
129    define m where m = card (UNIV::σ set)
130
131    have n = card (x  range(inv ασ) . {y . ασ x = ασ y})
132      unfolding n_def using union_univ by argo
133    also have   (irange (inv ασ). card {y. ασ i = ασ y})
134      using card_UN_le 2 by blast
135    also have   (irange (inv ασ). card (UNIV::σ set))
136      by (metis (no_types, lifting) 0 sum_mono)
137    also have   card (range (inv ασ)) * card (UNIV::σ set)
138      using sum_bounded_above by auto
139    also have   card (UNIV::σ set) * card (UNIV::σ set)
140      using 1 by force
141    also have  = m*m
142      unfolding m_def by blast
143    finally have n_upper: n  m*m.
144
145    have finite (x  range(inv ασ) . {y . ασ x = ασ y})
146      using 2 finite_collapsed by blast
147    hence finite_αset: finite (UNIV::urrel set set)
148      using union_univ by argo
149
150    have 2^2^m = (2::nat)^(card (UNIV::σ set set))
151      by (metis Pow_UNIV card_Pow finite_σ_set m_def)
152    moreover have card (UNIV::σ set set)  (card (UNIV::urrel set))
153      using card_σ_set_set_bound
154      by (meson Finite_Set.finite_set card_of_ordLeq finite_αset
155                finite_σ_set inj_on_iff_card_le)
156    ultimately have 2^2^m  (2::nat)^(card (UNIV:: urrel set))
157      by simp
158    also have  = n
159      unfolding n_def
160      by (metis Finite_Set.finite_set Pow_UNIV card_Pow finite_αset)
161    finally have 2^2^m  n by blast
162    hence 2^2^m  m*m using n_upper by linarith
163    moreover {
164      have (2::nat)^(2^m)  (2^(m + 1))
165        by (metis Suc_eq_plus1 Suc_leI less_exp one_le_numeral power_increasing)
166      also have (2^(m + 1)) = (2::nat) * 2^m
167        by auto
168      have m < 2^m
169        by (simp add: less_exp)
170      hence m*m < (2^m)*(2^m)
171        by (simp add: mult_strict_mono)
172      moreover have  = 2^(m+m)
173        by (simp add: power_add)
174      ultimately have m*m < 2 ^ (m + m) by presburger
175      moreover have m+m  2^m
176      proof (induct m)
177        case 0
178        thus ?case by auto
179      next
180        case (Suc m)
181        thus ?case
182          by (metis Suc_leI less_exp mult_2 mult_le_mono2 power_Suc)
183      qed
184      ultimately have m*m < 2^2^m
185        by (meson less_le_trans one_le_numeral power_increasing)
186    }
187    ultimately have False by auto
188  }
189  moreover {
190    textInfinite case.
191    assume infinite (UNIV::σ set)
192    hence Cinfσ: Cinfinite |UNIV::σ set|
193      by (simp add: cinfinite_def)
194    have 1: |range (inv ασ)| ≤o |UNIV::σ set|
195      by auto
196    have 2: irange (inv ασ). |{y . ασ i = ασ y}| ≤o |UNIV::σ set|
197    proof
198      fix i :: urrel set
199      assume i  range (inv ασ)
200      show |{y . ασ i = ασ y}| ≤o |UNIV::σ set|
201        using A by blast
202    qed
203    have | ((λi. {y. ασ i = ασ y}) ` (range (inv ασ)))| ≤o
204                   |Sigma (range (inv ασ)) (λi. {y. ασ i = ασ y})|
205      using card_of_UNION_Sigma by blast
206    hence |UNIV::urrel set set| ≤o
207           |Sigma (range (inv ασ)) (λi. {y. ασ i = ασ y})|
208      using union_univ by argo
209    moreover have |Sigma (range (inv ασ)) (λi. {y. ασ i = ασ y})| ≤o |UNIV::σ set|
210      using card_of_Sigma_ordLeq_Cinfinite[OF Cinfσ, OF 1, OF 2] by blast
211    ultimately have |UNIV::urrel set set| ≤o |UNIV::σ set|
212      using ordLeq_transitive by blast
213    moreover {
214      have |UNIV::σ set| <o |UNIV::σ set set|
215        by auto
216      moreover have |UNIV::σ set set| ≤o |UNIV::urrel set|
217        using card_σ_set_set_bound by blast
218      moreover have |UNIV::urrel set| <o |UNIV::urrel set set|
219        by auto
220      ultimately have |UNIV::σ set| <o |UNIV::urrel set set|
221        by (metis ordLess_imp_ordLeq ordLess_ordLeq_trans)
222    }
223    ultimately have False
224      using not_ordLeq_ordLess by blast
225  }
226  ultimately show False by blast
227qed
228
229textWe introduce a mapping from abstract objects (i.e. sets of urrelations) to
230     special urelements @{text ‹ασ›} that is surjective and distinguishes all
231     abstract objects that are distinguished by a (not necessarily surjective)
232     mapping @{text ‹ασ'›}. @{text ‹ασ'›} will be used to model extended relation
233     comprehension.
234consts ασ' :: urrel set  σ
235consts ασ :: urrel set  σ
236
237specification(ασ)
238  ασ_surj: surj ασ
239  ασ_ασ': ασ x = ασ y  ασ' x = ασ' y
240proof -
241  obtain x where x_prop: |UNIV::σ set| <o |{y. ασ' x = ασ' y}|
242    using ασ_pigeonhole by blast
243  have f :: urrel set  σ . f ` {y. ασ' x = ασ' y} = UNIV  f x = ασ' x
244  proof -
245    have f :: urrel set  σ . f ` {y. ασ' x = ασ' y} = UNIV
246      by (simp add: x_prop card_of_ordLeq2 ordLess_imp_ordLeq)
247    then obtain f :: urrel set  σ where f ` {y. ασ' x = ασ' y} = UNIV
248      by presburger
249    moreover obtain a where f a = ασ' x and ασ' a = ασ' x
250      by (smt (verit, best) calculation UNIV_I image_iff mem_Collect_eq)
251    ultimately have (f (a := f x, x := f a)) ` {y. ασ' x = ασ' y} = UNIV 
252                      (f (a := f x, x := f a)) x = ασ' x
253      by (auto simp: image_def)
254    thus ?thesis by blast
255  qed
256  then obtain f where fimage: f ` {y. ασ' x = ασ' y} = UNIV
257                  and fx: f x = ασ' x
258    by blast
259
260  define ασ :: urrel set  σ where
261    ασ  λ urrels . if ασ' urrels = ασ' x  f urrels  range ασ'
262                      then f urrels
263                      else ασ' urrels
264  have surj ασ
265  proof -
266    {
267    fix s :: σ
268    {
269      assume s  range ασ'
270      hence 0: ασ' (inv ασ' s) = s
271        by (meson f_inv_into_f)
272      {
273        assume s = ασ' x
274        hence ασ x = s
275          using ασ_def fx by presburger
276        hence f . ασ (f s) = s
277          by auto
278      }
279      moreover {
280        assume s  ασ' x
281        hence ασ (inv ασ' s) = s
282          unfolding ασ_def 0 by presburger
283        hence f . ασ (f s) = s
284          by blast
285      }
286      ultimately have f . ασ (f s) = s
287        by blast
288    }
289    moreover {
290      assume s  range ασ'
291      moreover obtain urrels where f urrels = s and ασ' x = ασ' urrels
292        by (smt (verit, best) UNIV_I fimage image_iff mem_Collect_eq)
293      ultimately have ασ urrels = s
294        using ασ_def by presburger
295      hence f . ασ (f s) = s
296        by (meson f_inv_into_f range_eqI)
297    }
298    ultimately have f . ασ (f s) = s
299      by blast
300    }
301    thus ?thesis
302      by (metis surj_def)
303  qed
304  moreover have x y. ασ x = ασ y  ασ' x = ασ' y
305    by (metis ασ_def rangeI)
306  ultimately show ?thesis
307    by blast
308qed
309
310textFor extended models that validate extended relation comprehension
311     (and consequently the predecessor axiom), we specify which
312     abstract objects are distinguished by @{const ασ'}.
313
314definition urrel_to_ωrel :: urrel  (ω  w  bool) where
315  urrel_to_ωrel  λ r u w . AOT_model_valid_in w (Rep_urrel r (ωυ u))
316definition ωrel_to_urrel :: (ω  w  bool)  urrel where
317  ωrel_to_urrel  λ φ . Abs_urrel
318    (λ u . ε𝗈 w . case u of ωυ x  φ x w | _  False)
319
320definition AOT_urrel_ωequiv :: urrel  urrel  bool where
321  AOT_urrel_ωequiv  λ r s .  u v . AOT_model_valid_in v (Rep_urrel r (ωυ u)) =
322                                       AOT_model_valid_in v (Rep_urrel s (ωυ u))
323
324lemma urrel_ωrel_quot: Quotient3 AOT_urrel_ωequiv urrel_to_ωrel ωrel_to_urrel
325proof(rule Quotient3I)
326  show urrel_to_ωrel (ωrel_to_urrel a) = a for a
327    unfolding ωrel_to_urrel_def urrel_to_ωrel_def
328    apply (rule ext)
329    apply (subst Abs_urrel_inverse)
330    by (auto simp: AOT_model_proposition_choice_simp)
331next
332  show AOT_urrel_ωequiv (ωrel_to_urrel a) (ωrel_to_urrel a) for a
333    unfolding ωrel_to_urrel_def AOT_urrel_ωequiv_def
334    apply (subst (1 2) Abs_urrel_inverse)
335    by (auto simp: AOT_model_proposition_choice_simp)
336next
337  show AOT_urrel_ωequiv r s = (AOT_urrel_ωequiv r r  AOT_urrel_ωequiv s s 
338                                urrel_to_ωrel r = urrel_to_ωrel s) for r s
339  proof
340    assume AOT_urrel_ωequiv r s
341    hence AOT_model_valid_in v (Rep_urrel r (ωυ u)) =
342           AOT_model_valid_in v (Rep_urrel s (ωυ u)) for u v
343      using AOT_urrel_ωequiv_def by metis
344    hence urrel_to_ωrel r = urrel_to_ωrel s
345      unfolding urrel_to_ωrel_def
346      by simp
347    thus AOT_urrel_ωequiv r r  AOT_urrel_ωequiv s s 
348          urrel_to_ωrel r = urrel_to_ωrel s
349      unfolding AOT_urrel_ωequiv_def
350      by auto
351  next
352    assume AOT_urrel_ωequiv r r  AOT_urrel_ωequiv s s 
353            urrel_to_ωrel r = urrel_to_ωrel s
354    hence AOT_model_valid_in v (Rep_urrel r (ωυ u)) =
355           AOT_model_valid_in v (Rep_urrel s (ωυ u)) for u v
356      by (metis urrel_to_ωrel_def)
357    thus AOT_urrel_ωequiv r s
358      using AOT_urrel_ωequiv_def by presburger
359  qed
360qed
361
362specification (ασ')
363  ασ_eq_ord_exts_all:
364    ασ' a = ασ' b  (s . urrel_to_ωrel s = urrel_to_ωrel r  s  a)
365       ( s . urrel_to_ωrel s = urrel_to_ωrel r  s  b)
366  ασ_eq_ord_exts_ex:
367    ασ' a = ασ' b  ( s . s  a  urrel_to_ωrel s = urrel_to_ωrel r)
368       (s . s  b  urrel_to_ωrel s = urrel_to_ωrel r)
369proof -
370  define ασ_wit_intersection where
371      ασ_wit_intersection  λ urrels .
372        {ordext . urrel . urrel_to_ωrel urrel = ordext  urrel  urrels}
373  define ασ_wit_union where
374      ασ_wit_union  λ urrels .
375        {ordext . urrelurrels . urrel_to_ωrel urrel = ordext}
376
377  let ?ασ_wit = λ urrels . 
378    let ordexts = ασ_wit_intersection urrels in
379    let ordexts' = ασ_wit_union urrels in
380    (ordexts, ordexts', undefined)
381  define ασ_wit :: urrel set  σ where
382    ασ_wit  λ urrels . Abs_σ (?ασ_wit urrels)
383  {
384    fix a b :: urrel set and r s
385    assume ασ_wit a = ασ_wit b
386    hence 0: {ordext. urrel. urrel_to_ωrel urrel = ordext  urrel  a} =
387              {ordext. urrel. urrel_to_ωrel urrel = ordext  urrel  b}
388      unfolding ασ_wit_def Let_def
389      apply (subst (asm) Abs_σ_inject)
390      by (auto simp: ασ_wit_intersection_def ασ_wit_union_def)
391    assume urrel_to_ωrel s = urrel_to_ωrel r  s  a for s
392    hence urrel_to_ωrel r 
393           {ordext. urrel. urrel_to_ωrel urrel = ordext  urrel  a}
394      by auto
395    hence urrel_to_ωrel r 
396           {ordext. urrel. urrel_to_ωrel urrel = ordext  urrel  b}
397      using 0 by blast
398    moreover assume urrel_to_ωrel s = urrel_to_ωrel r
399    ultimately have s  b
400      by blast
401  }
402  moreover {
403    fix a b :: urrel set and s r
404    assume ασ_wit a = ασ_wit b
405    hence 0: {ordext. urrel  a. urrel_to_ωrel urrel = ordext} =
406              {ordext. urrel  b. urrel_to_ωrel urrel = ordext}
407      unfolding ασ_wit_def
408      apply (subst (asm) Abs_σ_inject)
409      by (auto simp: Let_def ασ_wit_intersection_def ασ_wit_union_def)
410    assume s  a
411    hence urrel_to_ωrel s  {ordext. urrel  a. urrel_to_ωrel urrel = ordext}
412      by blast
413    moreover assume urrel_to_ωrel s = urrel_to_ωrel r
414    ultimately have urrel_to_ωrel r 
415                     {ordext. urrel  b. urrel_to_ωrel urrel = ordext}
416      using "0" by argo
417    hence s. s  b  urrel_to_ωrel s = urrel_to_ωrel r
418      by blast
419  }
420  ultimately show ?thesis
421    by (safe intro!: exI[where x=ασ_wit]; metis)
422qed
423
424textWe enable the extended model version.
425abbreviation (input) AOT_ExtendedModel where AOT_ExtendedModel  True
426
427textIndividual terms are either ordinary objects, represented by ordinary urelements,
428     abstract objects, modelled as sets of urrelations, or null objects, used to
429     represent non-denoting definite descriptions.
430datatype κ = ωκ ω | ακ urrel set | is_nullκ: nullκ null
431
432textThe mapping from abstract objects to urelements can be naturally
433     lifted to a surjective mapping from individual terms to urelements.
434primrec κυ :: κυ where
435  κυ (ωκ x) = ωυ x
436| κυ (ακ x) = συ (ασ x)
437| κυ (nullκ x) = nullυ x
438
439lemma κυ_surj: surj κυ
440  using ασ_surj by (metis κυ.simps(1) κυ.simps(2) κυ.simps(3) υ.exhaust surj_def)
441
442textBy construction if the urelement of an individual term is exemplified by
443     an urrelation, it cannot be a null-object.
444lemma urrel_null_false:
445  assumes AOT_model_valid_in w (Rep_urrel f (κυ x))
446  shows ¬is_nullκ x
447  by (metis (mono_tags, lifting) assms Rep_urrel κ.collapse(3) κυ.simps(3)
448        mem_Collect_eq)
449
450textAOT requires any ordinary object to be @{emph possibly concrete} and that
451     there is an object that is not actually, but possibly concrete.
452consts AOT_model_concreteω :: ω  w   bool
453specification (AOT_model_concreteω)
454  AOT_model_ω_concrete_in_some_world:
455   w . AOT_model_concreteω x w
456  AOT_model_contingent_object:
457   x w . AOT_model_concreteω x w  ¬AOT_model_concreteω x w0
458  by (rule exI[where x=λ_ w. w  w0]) (auto simp: AOT_model_nonactual_world)
459
460textWe define a type class for AOT's terms specifying the conditions under which
461     objects of that type denote and require the set of denoting terms to be
462     non-empty.
463class AOT_Term =
464  fixes AOT_model_denotes :: 'a  bool
465  assumes AOT_model_denoting_ex:  x . AOT_model_denotes x
466
467textAll types except the type of propositions involve non-denoting terms. We
468     define a refined type class for those.
469class AOT_IncompleteTerm = AOT_Term +
470  assumes AOT_model_nondenoting_ex:  x . ¬AOT_model_denotes x
471
472textGeneric non-denoting term.
473definition AOT_model_nondenoting :: 'a::AOT_IncompleteTerm where
474  AOT_model_nondenoting  SOME τ . ¬AOT_model_denotes τ
475lemma AOT_model_nondenoing: ¬AOT_model_denotes (AOT_model_nondenoting)
476  using someI_ex[OF AOT_model_nondenoting_ex]
477  unfolding AOT_model_nondenoting_def by blast
478
479text@{const AOT_model_denotes} can trivially be extended to products of types.
480instantiation prod :: (AOT_Term, AOT_Term) AOT_Term
481begin
482definition AOT_model_denotes_prod :: 'a×'b  bool where
483  AOT_model_denotes_prod  λ(x,y) . AOT_model_denotes x  AOT_model_denotes y
484instance proof
485  show x::'a×'b. AOT_model_denotes x
486    by (simp add: AOT_model_denotes_prod_def AOT_model_denoting_ex)
487qed
488end
489
490textWe specify a transformation of proposition-valued functions on terms, s.t.
491     the result is fully determined by @{emph regular} terms. This will be required
492     for modelling n-ary relations as functions on tuples while preserving AOT's
493     definition of n-ary relation identity.
494locale AOT_model_irregular_spec =
495  fixes AOT_model_irregular :: ('a  𝗈)  'a  𝗈
496    and AOT_model_regular :: 'a  bool
497    and AOT_model_term_equiv :: 'a  'a  bool
498  assumes AOT_model_irregular_false:
499    ¬AOT_model_valid_in w (AOT_model_irregular φ x)
500  assumes AOT_model_irregular_equiv:
501    AOT_model_term_equiv x y 
502     AOT_model_irregular φ x = AOT_model_irregular φ y
503  assumes AOT_model_irregular_eqI:
504    ( x . AOT_model_regular x  φ x = ψ x) 
505     AOT_model_irregular φ x = AOT_model_irregular ψ x
506
507textWe introduce a type class for individual terms that specifies being regular,
508     being equivalent (i.e. conceptually @{emph sharing urelements}) and the
509     transformation on proposition-valued functions as specified above.
510class AOT_IndividualTerm = AOT_IncompleteTerm +
511  fixes AOT_model_regular :: 'a  bool
512  fixes AOT_model_term_equiv :: 'a  'a  bool
513  fixes AOT_model_irregular :: ('a  𝗈)  'a  𝗈
514  assumes AOT_model_irregular_nondenoting:
515    ¬AOT_model_regular x  ¬AOT_model_denotes x
516  assumes AOT_model_term_equiv_part_equivp:
517    equivp AOT_model_term_equiv
518  assumes AOT_model_term_equiv_denotes:
519    AOT_model_term_equiv x y  (AOT_model_denotes x = AOT_model_denotes y)
520  assumes AOT_model_term_equiv_regular:
521    AOT_model_term_equiv x y  (AOT_model_regular x = AOT_model_regular y)
522  assumes AOT_model_irregular:
523    AOT_model_irregular_spec AOT_model_irregular AOT_model_regular
524                              AOT_model_term_equiv
525
526interpretation AOT_model_irregular_spec AOT_model_irregular AOT_model_regular
527                                        AOT_model_term_equiv
528  using AOT_model_irregular .
529
530textOur concrete type for individual terms satisfies the type class of
531     individual terms.
532     Note that all unary individuals are regular. In general, an individual term
533     may be a tuple and is regular, if at most one tuple element does not denote.
534instantiation κ :: AOT_IndividualTerm
535begin
536definition AOT_model_term_equiv_κ :: κ  κ  bool where
537  AOT_model_term_equiv_κ  λ x y . κυ x = κυ y
538definition AOT_model_denotes_κ :: κ  bool where
539  AOT_model_denotes_κ  λ x . ¬is_nullκ x
540definition AOT_model_regular_κ :: κ  bool where
541  AOT_model_regular_κ  λ x . True
542definition AOT_model_irregular_κ :: (κ  𝗈)  κ  𝗈 where
543  AOT_model_irregular_κ  SOME φ . AOT_model_irregular_spec φ
544                                        AOT_model_regular AOT_model_term_equiv
545instance proof
546  show x :: κ. AOT_model_denotes x
547    by (rule exI[where x=ωκ undefined])
548       (simp add: AOT_model_denotes_κ_def)
549next
550  show x :: κ. ¬AOT_model_denotes x
551    by (rule exI[where x=nullκ undefined])
552       (simp add: AOT_model_denotes_κ_def AOT_model_regular_κ_def)
553next
554  show "¬AOT_model_regular x  ¬ AOT_model_denotes x" for x :: κ
555    by (simp add: AOT_model_regular_κ_def)
556next
557  show equivp (AOT_model_term_equiv :: κ  κ  bool)
558    by (rule equivpI; rule reflpI exI sympI transpI)
559       (simp_all add: AOT_model_term_equiv_κ_def)
560next
561  fix x y :: κ
562  show AOT_model_term_equiv x y  AOT_model_denotes x = AOT_model_denotes y
563    by (metis AOT_model_denotes_κ_def AOT_model_term_equiv_κ_def κ.exhaust_disc
564              κυ.simps υ.disc(1,3,5,6) is_ακ_def is_ωκ_def is_nullκ_def)
565next
566  fix x y :: κ
567  show AOT_model_term_equiv x y  AOT_model_regular x = AOT_model_regular y
568    by (simp add: AOT_model_regular_κ_def)
569next
570  have "AOT_model_irregular_spec (λ φ (x::κ) .  ε𝗈 w . False)
571          AOT_model_regular AOT_model_term_equiv"
572    by standard (auto simp: AOT_model_proposition_choice_simp)
573  thus AOT_model_irregular_spec (AOT_model_irregular::(κ𝗈)  κ  𝗈)
574          AOT_model_regular AOT_model_term_equiv
575    unfolding AOT_model_irregular_κ_def by (metis (no_types, lifting) someI_ex)
576qed
577end
578
579textWe define relations among individuals as proposition valued functions.
580     @{emph Denoting} unary relations (among @{typ κ}) will match the
581     urrelations introduced above.
582typedef 'a rel (<_>) = UNIV::('a::AOT_IndividualTerm  𝗈) set ..
583setup_lifting type_definition_rel
584
585textWe will use the transformation specified above to "fix" the behaviour of
586     functions on irregular terms when defining @{text ‹λ›}-expressions.
587definition fix_irregular :: ('a::AOT_IndividualTerm  𝗈)  ('a  𝗈) where
588  fix_irregular  λ φ x . if AOT_model_regular x
589                            then φ x else AOT_model_irregular φ x
590lemma fix_irregular_denoting:
591  AOT_model_denotes x  fix_irregular φ x = φ x
592  by (meson AOT_model_irregular_nondenoting fix_irregular_def)
593lemma fix_irregular_regular:
594  AOT_model_regular x  fix_irregular φ x = φ x
595  by (meson AOT_model_irregular_nondenoting fix_irregular_def)
596lemma fix_irregular_irregular:
597  ¬AOT_model_regular x  fix_irregular φ x = AOT_model_irregular φ x
598  by (simp add: fix_irregular_def)
599
600textRelations among individual terms are (potentially non-denoting) terms.
601     A relation denotes, if it agrees on all equivalent terms (i.e. terms sharing
602     urelements), is necessarily false on all non-denoting terms and is
603     well-behaved on irregular terms.
604instantiation rel :: (AOT_IndividualTerm) AOT_IncompleteTerm
605begin
606text\linelabel{AOT_model_denotes_rel}
607lift_definition AOT_model_denotes_rel :: <'a>  bool is
608  λ φ . ( x y . AOT_model_term_equiv x y  φ x = φ y) 
609         ( w x . AOT_model_valid_in w (φ x)  AOT_model_denotes x) 
610         ( x . ¬AOT_model_regular x  φ x = AOT_model_irregular φ x) .
611instance proof
612  have AOT_model_irregular (fix_irregular φ) x = AOT_model_irregular φ x
613    for φ and x :: 'a
614    by (rule AOT_model_irregular_eqI) (simp add: fix_irregular_def)
615  thus  x :: <'a> . AOT_model_denotes x
616    by (safe intro!: exI[where x=Abs_rel (fix_irregular (λx. ε𝗈 w . False))])
617       (transfer; auto simp: AOT_model_proposition_choice_simp fix_irregular_def
618                             AOT_model_irregular_equiv AOT_model_term_equiv_regular
619                             AOT_model_irregular_false)
620next
621  show f :: <'a> . ¬AOT_model_denotes f
622    by (rule exI[where x=Abs_rel (λx. ε𝗈 w . True)];
623        auto simp: AOT_model_denotes_rel.abs_eq AOT_model_nondenoting_ex
624                   AOT_model_proposition_choice_simp)
625qed
626end
627
628textAuxiliary lemmata.
629
630lemma AOT_model_term_equiv_eps:
631  shows AOT_model_term_equiv (Eps (AOT_model_term_equiv κ)) κ
632    and AOT_model_term_equiv κ (Eps (AOT_model_term_equiv κ))
633    and AOT_model_term_equiv κ κ' 
634         (Eps (AOT_model_term_equiv κ)) = (Eps (AOT_model_term_equiv κ'))
635  apply (metis AOT_model_term_equiv_part_equivp equivp_def someI_ex)
636  apply (metis AOT_model_term_equiv_part_equivp equivp_def someI_ex)
637  by (metis AOT_model_term_equiv_part_equivp equivp_def)
638
639lemma AOT_model_denotes_Abs_rel_fix_irregularI:
640  assumes  x y . AOT_model_term_equiv x y  φ x = φ y
641      and  w x . AOT_model_valid_in w (φ x)  AOT_model_denotes x
642    shows AOT_model_denotes (Abs_rel (fix_irregular φ))
643proof -
644  have AOT_model_irregular φ x = AOT_model_irregular
645          (λx. if AOT_model_regular x then φ x else AOT_model_irregular φ x) x
646    if ¬ AOT_model_regular x
647    for x
648    by (rule AOT_model_irregular_eqI) auto
649  thus ?thesis
650  unfolding AOT_model_denotes_rel.rep_eq
651  using assms by (auto simp: AOT_model_irregular_false Abs_rel_inverse
652                             AOT_model_irregular_equiv fix_irregular_def
653                             AOT_model_term_equiv_regular)
654qed
655
656lemma AOT_model_term_equiv_rel_equiv:
657  assumes AOT_model_denotes x
658      and AOT_model_denotes y
659    shows AOT_model_term_equiv x y = ( Π w . AOT_model_denotes Π 
660            AOT_model_valid_in w (Rep_rel Π x) = AOT_model_valid_in w (Rep_rel Π y))
661proof
662  assume AOT_model_term_equiv x y
663  thus  Π w . AOT_model_denotes Π  AOT_model_valid_in w (Rep_rel Π x) =
664                                         AOT_model_valid_in w (Rep_rel Π y)
665    by (simp add: AOT_model_denotes_rel.rep_eq)
666next
667  have 0: (AOT_model_denotes x'  AOT_model_term_equiv x' y) =
668           (AOT_model_denotes y'  AOT_model_term_equiv y' y)
669    if AOT_model_term_equiv x' y' for x' y'
670    by (metis that AOT_model_term_equiv_denotes AOT_model_term_equiv_part_equivp
671              equivp_def)
672  assume  Π w . AOT_model_denotes Π  AOT_model_valid_in w (Rep_rel Π x) =
673                                           AOT_model_valid_in w (Rep_rel Π y)
674  moreover have AOT_model_denotes (Abs_rel (fix_irregular
675    (λ x . ε𝗈 w . AOT_model_denotes x  AOT_model_term_equiv x y)))
676    (is "AOT_model_denotes ?r")
677    by (rule AOT_model_denotes_Abs_rel_fix_irregularI)
678       (auto simp: 0 AOT_model_denotes_rel.rep_eq Abs_rel_inverse fix_irregular_def
679                   AOT_model_proposition_choice_simp AOT_model_irregular_false)
680  ultimately have AOT_model_valid_in w (Rep_rel ?r x) =
681                   AOT_model_valid_in w (Rep_rel ?r y) for w
682    by blast
683  thus AOT_model_term_equiv x y
684    by (simp add: Abs_rel_inverse AOT_model_proposition_choice_simp
685                  fix_irregular_denoting[OF assms(1)] AOT_model_term_equiv_part_equivp
686                  fix_irregular_denoting[OF assms(2)] assms equivp_reflp)
687qed
688
689textDenoting relations among terms of type @{typ κ} correspond to urrelations.
690
691definition rel_to_urrel :: <κ>  urrel where
692  rel_to_urrel  λ Π . Abs_urrel (λ u . Rep_rel Π (SOME x . κυ x = u))
693definition urrel_to_rel :: urrel  <κ> where
694  urrel_to_rel  λ φ . Abs_rel (λ x . Rep_urrel φ (κυ x))
695definition AOT_rel_equiv :: <'a::AOT_IndividualTerm>  <'a>  bool where
696  AOT_rel_equiv  λ f g . AOT_model_denotes f  AOT_model_denotes g  f = g
697
698lemma urrel_quotient3: Quotient3 AOT_rel_equiv rel_to_urrel urrel_to_rel
699proof (rule Quotient3I)
700  have (λu. Rep_urrel a (κυ (SOME x. κυ x = u))) = (λu. Rep_urrel a u) for a
701    by (rule ext) (metis (mono_tags, lifting) κυ_surj surj_f_inv_f verit_sko_ex')
702  thus rel_to_urrel (urrel_to_rel a) = a for a
703    by (simp add: Abs_rel_inverse rel_to_urrel_def urrel_to_rel_def
704                  Rep_urrel_inverse)
705next
706  show AOT_rel_equiv (urrel_to_rel a) (urrel_to_rel a) for a
707    unfolding AOT_rel_equiv_def urrel_to_rel_def
708    by transfer (simp add: AOT_model_regular_κ_def AOT_model_denotes_κ_def
709                           AOT_model_term_equiv_κ_def urrel_null_false)
710next
711  {
712    fix a
713    assume w x. AOT_model_valid_in w (a x)  ¬ is_nullκ x
714    hence (λu. a (SOME x. κυ x = u)) 
715           {φ. x w. ¬ AOT_model_valid_in w (φ (nullυ x))}
716      by (simp; metis (mono_tags, lifting) κ.exhaust_disc κυ.simps υ.disc(1,3,5)
717                                           υ.disc(6) is_ακ_def is_ωκ_def someI_ex)
718  } note 1 = this
719  {
720    fix r s :: κ  𝗈
721    assume A: x y. AOT_model_term_equiv x y  r x = r y
722    assume w x. AOT_model_valid_in w (r x)  AOT_model_denotes x
723    hence 2: (λu. r (SOME x. κυ x = u)) 
724              {φ. x w. ¬ AOT_model_valid_in w (φ (nullυ x))}
725      using 1 AOT_model_denotes_κ_def by meson
726    assume B: x y. AOT_model_term_equiv x y  s x = s y
727    assume w x. AOT_model_valid_in w (s x)  AOT_model_denotes x
728    hence 3: (λu. s (SOME x. κυ x = u)) 
729              {φ. x w. ¬ AOT_model_valid_in w (φ (nullυ x))}
730      using 1 AOT_model_denotes_κ_def by meson
731    assume Abs_urrel (λu. r (SOME x. κυ x = u)) =
732            Abs_urrel (λu. s (SOME x. κυ x = u))
733    hence 4: r (SOME x. κυ x = u) = s (SOME x::κ. κυ x = u) for u
734      unfolding Abs_urrel_inject[OF 2 3] by metis
735    have r x = s x for x
736      using 4[of κυ x]
737      by (metis (mono_tags, lifting) A B AOT_model_term_equiv_κ_def someI_ex)
738    hence r = s by auto
739  } 
740  thus AOT_rel_equiv r s = (AOT_rel_equiv r r  AOT_rel_equiv s s 
741                             rel_to_urrel r = rel_to_urrel s) for r s
742    unfolding AOT_rel_equiv_def rel_to_urrel_def
743    by transfer auto
744qed
745
746lemma urrel_quotient:
747  Quotient AOT_rel_equiv rel_to_urrel urrel_to_rel
748            (λx y. AOT_rel_equiv x x  rel_to_urrel x = y)
749  using Quotient3_to_Quotient[OF urrel_quotient3] by auto
750
751textUnary individual terms are always regular and equipped with encoding and
752     concreteness. The specification of the type class anticipates the required
753     properties for deriving the axiom system.
754class AOT_UnaryIndividualTerm =
755  fixes AOT_model_enc :: 'a  <'a::AOT_IndividualTerm>  bool
756    and AOT_model_concrete :: w  'a  bool
757  assumes AOT_model_unary_regular:
758      AOT_model_regular x ― ‹All unary individual terms are regular.
759      and AOT_model_enc_relid:
760        AOT_model_denotes F 
761         AOT_model_denotes G 
762         ( x . AOT_model_enc x F  AOT_model_enc x G)
763          F = G
764      and AOT_model_A_objects:
765        x . AOT_model_denotes x 
766              (w. ¬ AOT_model_concrete w x) 
767              (F. AOT_model_denotes F  AOT_model_enc x F = φ F)
768      and AOT_model_contingent:
769         x w. AOT_model_concrete w x  ¬ AOT_model_concrete w0 x
770      and AOT_model_nocoder:
771        AOT_model_concrete w x  ¬AOT_model_enc x F
772      and AOT_model_concrete_equiv:
773        AOT_model_term_equiv x y 
774          AOT_model_concrete w x = AOT_model_concrete w y
775      and AOT_model_concrete_denotes:
776        AOT_model_concrete w x  AOT_model_denotes x
777      ― ‹The following are properties that will only hold in the extended models.
778      and AOT_model_enc_indistinguishable_all:
779       AOT_ExtendedModel 
780        AOT_model_denotes a  ¬( w . AOT_model_concrete w a) 
781        AOT_model_denotes b  ¬( w . AOT_model_concrete w b) 
782        AOT_model_denotes Π 
783        ( Π' . AOT_model_denotes Π' 
784          ( v . AOT_model_valid_in v (Rep_rel Π' a) =
785                 AOT_model_valid_in v (Rep_rel Π' b))) 
786        ( Π' . AOT_model_denotes Π' 
787            ( v x .  w . AOT_model_concrete w x 
788                AOT_model_valid_in v (Rep_rel Π' x) =
789                AOT_model_valid_in v (Rep_rel Π x)) 
790            AOT_model_enc a Π') 
791        ( Π' . AOT_model_denotes Π' 
792            ( v x .  w . AOT_model_concrete w x 
793                AOT_model_valid_in v (Rep_rel Π' x) =
794                AOT_model_valid_in v (Rep_rel Π x)) 
795            AOT_model_enc b Π')
796      and AOT_model_enc_indistinguishable_ex:
797       AOT_ExtendedModel 
798        AOT_model_denotes a  ¬( w . AOT_model_concrete w a) 
799        AOT_model_denotes b  ¬( w . AOT_model_concrete w b) 
800        AOT_model_denotes Π 
801        ( Π' . AOT_model_denotes Π' 
802          ( v . AOT_model_valid_in v (Rep_rel Π' a) =
803                 AOT_model_valid_in v (Rep_rel Π' b))) 
804        ( Π' . AOT_model_denotes Π'  AOT_model_enc a Π' 
805            ( v x . ( w . AOT_model_concrete w x) 
806                AOT_model_valid_in v (Rep_rel Π' x) =
807                AOT_model_valid_in v (Rep_rel Π x))) 
808        ( Π' . AOT_model_denotes Π'  AOT_model_enc b Π' 
809            ( v x . ( w . AOT_model_concrete w x) 
810                AOT_model_valid_in v (Rep_rel Π' x) =
811                AOT_model_valid_in v (Rep_rel Π x)))
812
813textInstantiate the class of unary individual terms for our concrete type of
814     individual terms @{typ κ}.
815instantiation κ :: AOT_UnaryIndividualTerm
816begin                          
817
818definition AOT_model_enc_κ :: κ  <κ>  bool where
819  AOT_model_enc_κ  λ x F .
820      case x of ακ a  AOT_model_denotes F  rel_to_urrel F  a
821              | _  False
822primrec AOT_model_concrete_κ :: w  κ  bool where
823  AOT_model_concrete_κ w (ωκ x) = AOT_model_concreteω x w
824| AOT_model_concrete_κ w (ακ x) = False
825| AOT_model_concrete_κ w (nullκ x) = False
826
827lemma AOT_meta_A_objects_κ:
828  x :: κ. AOT_model_denotes x 
829            (w. ¬ AOT_model_concrete w x) 
830            (F. AOT_model_denotes F  AOT_model_enc x F = φ F) for φ
831  apply (rule exI[where x=ακ {f . φ (urrel_to_rel f)}])
832  apply (simp add: AOT_model_enc_κ_def AOT_model_denotes_κ_def)
833  by (metis (no_types, lifting) AOT_rel_equiv_def urrel_quotient
834                                Quotient_rep_abs_fold_unmap)
835
836instance proof
837  show AOT_model_regular x for x :: κ
838    by (simp add: AOT_model_regular_κ_def)
839next
840  fix F G :: <κ>
841  assume AOT_model_denotes F
842  moreover assume AOT_model_denotes G
843  moreover assume x. AOT_model_enc x F = AOT_model_enc x G
844  moreover obtain x where G. AOT_model_denotes G  AOT_model_enc x G = (F = G)
845    using AOT_meta_A_objects_κ by blast
846  ultimately show F = G by blast
847next
848  show x :: κ. AOT_model_denotes x 
849                 (w. ¬ AOT_model_concrete w x) 
850                 (F. AOT_model_denotes F  AOT_model_enc x F = φ F) for φ
851    using AOT_meta_A_objects_κ .
852next
853  show  (x::κ) w. AOT_model_concrete w x  ¬ AOT_model_concrete w0 x
854    using AOT_model_concrete_κ.simps(1) AOT_model_contingent_object by blast
855next
856  show AOT_model_concrete w x  ¬ AOT_model_enc x F for w and x :: κ and F
857    by (metis AOT_model_concrete_κ.simps(2) AOT_model_enc_κ_def κ.case_eq_if
858              κ.collapse(2))
859next
860  show AOT_model_concrete w x = AOT_model_concrete w y
861    if AOT_model_term_equiv x y
862    for x y :: κ and w
863    using that by (induct x; induct y; auto simp: AOT_model_term_equiv_κ_def)
864next
865  show AOT_model_concrete w x  AOT_model_denotes x for w and x :: κ
866    by (metis AOT_model_concrete_κ.simps(3) AOT_model_denotes_κ_def κ.collapse(3))
867(* Extended models only *)
868next
869  fix κ κ' :: κ and Π Π' :: <κ> and w :: w
870  assume ext: AOT_ExtendedModel
871  assume AOT_model_denotes κ
872  moreover assume w. AOT_model_concrete w κ
873  ultimately obtain a where a_def: ακ a = κ
874    by (metis AOT_model_ω_concrete_in_some_world AOT_model_concrete_κ.simps(1)
875              AOT_model_denotes_κ_def κ.discI(3) κ.exhaust_sel)
876  assume AOT_model_denotes κ'
877  moreover assume w. AOT_model_concrete w κ'
878  ultimately obtain b where b_def: ακ b = κ'
879    by (metis AOT_model_ω_concrete_in_some_world AOT_model_concrete_κ.simps(1)
880              AOT_model_denotes_κ_def κ.discI(3) κ.exhaust_sel)
881  assume AOT_model_denotes Π'  AOT_model_valid_in w (Rep_rel Π' κ) =
882                                   AOT_model_valid_in w (Rep_rel Π' κ') for Π' w
883  hence AOT_model_valid_in w (Rep_urrel r (κυ κ)) =
884         AOT_model_valid_in w (Rep_urrel r (κυ κ')) for r
885    by (metis AOT_rel_equiv_def Abs_rel_inverse Quotient3_rel_rep
886              iso_tuple_UNIV_I urrel_quotient3 urrel_to_rel_def)
887  hence let r = (Abs_urrel (λ u . ε𝗈 w . u = κυ κ)) in
888         AOT_model_valid_in w (Rep_urrel r (κυ κ)) =
889         AOT_model_valid_in w (Rep_urrel r (κυ κ'))
890    by presburger
891  hence ασ_eq: ασ a = ασ b
892    unfolding Let_def
893    apply (subst (asm) (1 2) Abs_urrel_inverse)
894    using AOT_model_proposition_choice_simp a_def b_def by force+
895  assume Π_den: AOT_model_denotes Π
896  have r .  x . Rep_rel Π (ωκ x) = Rep_urrel r (ωυ x)
897    apply (rule exI[where x=rel_to_urrel Π])
898    apply auto
899    unfolding rel_to_urrel_def
900    apply (subst Abs_urrel_inverse)
901    apply auto
902     apply (metis (mono_tags, lifting) AOT_model_denotes_κ_def
903              AOT_model_denotes_rel.rep_eq κ.exhaust_disc κυ.simps(1,2,3)
904              AOT_model_denotes Π υ.disc(8,9) υ.distinct(3)
905              is_ακ_def is_ωκ_def verit_sko_ex')
906    by (metis (mono_tags, lifting) AOT_model_denotes_rel.rep_eq
907          AOT_model_term_equiv_κ_def κυ.simps(1) Π_den verit_sko_ex')
908  then obtain r where r_prop: Rep_rel Π (ωκ x) = Rep_urrel r (ωυ x) for x
909    by blast
910  assume AOT_model_denotes Π' 
911    (v x. w. AOT_model_concrete w x 
912        AOT_model_valid_in v (Rep_rel Π' x) =
913        AOT_model_valid_in v (Rep_rel Π x))  AOT_model_enc κ Π' for Π'
914  hence AOT_model_denotes Π' 
915    (v x. AOT_model_valid_in v (Rep_rel Π' (ωκ x)) =
916            AOT_model_valid_in v (Rep_rel Π (ωκ x)))  AOT_model_enc κ Π' for Π'
917    by (metis AOT_model_concrete_κ.simps(2) AOT_model_concrete_κ.simps(3)
918              κ.exhaust_disc is_ακ_def is_ωκ_def is_nullκ_def)
919  hence (v x. AOT_model_valid_in v (Rep_urrel r (ωυ x)) =
920                 AOT_model_valid_in v (Rep_rel Π (ωκ x)))  r  a for r
921    unfolding a_def[symmetric] AOT_model_enc_κ_def apply simp
922    by (smt (verit, best) AOT_rel_equiv_def Abs_rel_inverse Quotient3_def
923            κυ.simps(1) iso_tuple_UNIV_I urrel_quotient3 urrel_to_rel_def)
924  hence (v x. AOT_model_valid_in v (Rep_urrel r' (ωυ x)) =
925                 AOT_model_valid_in v (Rep_urrel r (ωυ x)))  r'  a for r'
926    unfolding r_prop.
927  hence s. urrel_to_ωrel s = urrel_to_ωrel r  s  a
928    by (metis urrel_to_ωrel_def)
929  hence 0: s. urrel_to_ωrel s = urrel_to_ωrel r  s  b
930    using ασ_eq_ord_exts_all ασ_eq ext ασ_ασ' by blast
931
932  assume Π'_den: AOT_model_denotes Π'
933  assume w. AOT_model_concrete w x  AOT_model_valid_in v (Rep_rel Π' x) =
934                                         AOT_model_valid_in v (Rep_rel Π x) for v x
935  hence AOT_model_valid_in v (Rep_rel Π' (ωκ x)) =
936         AOT_model_valid_in v (Rep_rel Π (ωκ x)) for v x
937    using AOT_model_ω_concrete_in_some_world AOT_model_concrete_κ.simps(1)
938    by presburger
939  hence AOT_model_valid_in v (Rep_urrel (rel_to_urrel Π') (ωυ x)) =
940         AOT_model_valid_in v (Rep_urrel r (ωυ x)) for v x
941    by (smt (verit, best) AOT_rel_equiv_def Abs_rel_inverse Quotient3_def
942          κυ.simps(1) iso_tuple_UNIV_I r_prop urrel_quotient3 urrel_to_rel_def Π'_den)
943  hence urrel_to_ωrel (rel_to_urrel Π') = urrel_to_ωrel r
944    by (metis (full_types) AOT_urrel_ωequiv_def Quotient3_def urrel_ωrel_quot)
945  hence rel_to_urrel Π'  b using 0 by blast
946  thus AOT_model_enc κ' Π'
947    unfolding b_def[symmetric] AOT_model_enc_κ_def by (auto simp: Π'_den)
948next
949  fix κ κ' :: κ and Π Π' :: <κ> and w :: w
950  assume ext: AOT_ExtendedModel
951  assume AOT_model_denotes κ
952  moreover assume w. AOT_model_concrete w κ
953  ultimately obtain a where a_def: ακ a = κ
954    by (metis AOT_model_ω_concrete_in_some_world AOT_model_concrete_κ.simps(1)
955          AOT_model_denotes_κ_def κ.discI(3) κ.exhaust_sel)
956  assume AOT_model_denotes κ'
957  moreover assume w. AOT_model_concrete w κ'
958  ultimately obtain b where b_def: ακ b = κ'
959    by (metis AOT_model_ω_concrete_in_some_world AOT_model_concrete_κ.simps(1)
960              AOT_model_denotes_κ_def κ.discI(3) κ.exhaust_sel)
961  assume AOT_model_denotes Π'  AOT_model_valid_in w (Rep_rel Π' κ) =
962                                   AOT_model_valid_in w (Rep_rel Π' κ') for Π' w
963  hence AOT_model_valid_in w (Rep_urrel r (κυ κ)) =
964         AOT_model_valid_in w (Rep_urrel r (κυ κ')) for r
965    by (metis AOT_rel_equiv_def Abs_rel_inverse Quotient3_rel_rep
966              iso_tuple_UNIV_I urrel_quotient3 urrel_to_rel_def)
967  hence let r = (Abs_urrel (λ u . ε𝗈 w . u = κυ κ)) in
968         AOT_model_valid_in w (Rep_urrel r (κυ κ)) =
969         AOT_model_valid_in w (Rep_urrel r (κυ κ'))
970    by presburger
971  hence ασ_eq: ασ a = ασ b
972    unfolding Let_def
973    apply (subst (asm) (1 2) Abs_urrel_inverse)
974    using AOT_model_proposition_choice_simp a_def b_def by force+
975  assume Π_den: AOT_model_denotes Π
976  have r .  x . Rep_rel Π (ωκ x) = Rep_urrel r (ωυ x)
977    apply (rule exI[where x=rel_to_urrel Π])
978    apply auto
979    unfolding rel_to_urrel_def
980    apply (subst Abs_urrel_inverse)
981    apply auto
982     apply (metis (mono_tags, lifting) AOT_model_denotes_κ_def
983          AOT_model_denotes_rel.rep_eq κ.exhaust_disc κυ.simps(1,2,3)
984          AOT_model_denotes Π υ.disc(8) υ.disc(9) υ.distinct(3)
985          is_ακ_def is_ωκ_def verit_sko_ex')
986    by (metis (mono_tags, lifting) AOT_model_denotes_rel.rep_eq
987          AOT_model_term_equiv_κ_def κυ.simps(1) Π_den verit_sko_ex')
988  then obtain r where r_prop: Rep_rel Π (ωκ x) = Rep_urrel r (ωυ x) for x
989    by blast
990
991  assume Π'. AOT_model_denotes Π' 
992    AOT_model_enc κ Π' 
993    (v x. (w. AOT_model_concrete w x)  AOT_model_valid_in v (Rep_rel Π' x) =
994                                            AOT_model_valid_in v (Rep_rel Π x))
995  then obtain Π' where
996      Π'_den: AOT_model_denotes Π' and
997      κ_enc_Π': AOT_model_enc κ Π' and
998      Π'_prop: w. AOT_model_concrete w x 
999                    AOT_model_valid_in v (Rep_rel Π' x) =
1000                    AOT_model_valid_in v (Rep_rel Π x) for v x
1001    by blast
1002  have AOT_model_valid_in v (Rep_rel Π' (ωκ x)) =
1003        AOT_model_valid_in v (Rep_rel Π (ωκ x)) for x v
1004    by (simp add: AOT_model_ω_concrete_in_some_world Π'_prop)
1005  hence 0: AOT_urrel_ωequiv (rel_to_urrel Π') (rel_to_urrel Π)
1006    unfolding AOT_urrel_ωequiv_def
1007    by (smt (verit) AOT_rel_equiv_def Abs_rel_inverse Quotient3_def
1008                    κυ.simps(1) iso_tuple_UNIV_I urrel_quotient3 urrel_to_rel_def
1009                    Π_den Π'_den)
1010  have rel_to_urrel Π'  a
1011   and urrel_to_ωrel (rel_to_urrel Π') = urrel_to_ωrel (rel_to_urrel Π)
1012    apply (metis AOT_model_enc_κ_def κ.simps(11) κ_enc_Π' a_def)
1013    by (metis Quotient3_rel 0 urrel_ωrel_quot)
1014  hence s. s  b  urrel_to_ωrel s = urrel_to_ωrel (rel_to_urrel Π)
1015    using ασ_eq_ord_exts_ex ασ_eq ext ασ_ασ' by blast
1016  then obtain s where
1017    s_prop: s  b  urrel_to_ωrel s = urrel_to_ωrel (rel_to_urrel Π)
1018    by blast
1019  then obtain Π'' where
1020    Π''_prop: rel_to_urrel Π'' = s and Π''_den: AOT_model_denotes Π''
1021    by (metis AOT_rel_equiv_def Quotient3_def urrel_quotient3)
1022  moreover have AOT_model_enc κ' Π''
1023    by (metis AOT_model_enc_κ_def Π''_den Π''_prop κ.simps(11) b_def s_prop)
1024  moreover have AOT_model_valid_in v (Rep_rel Π'' x) =
1025                 AOT_model_valid_in v (Rep_rel Π x)
1026             if w. AOT_model_concrete w x for v x
1027  proof(insert that)
1028    assume w. AOT_model_concrete w x
1029    then obtain u where x_def: x = ωκ u
1030      by (metis AOT_model_concrete_κ.simps(2,3) κ.exhaust)
1031    show AOT_model_valid_in v (Rep_rel Π'' x) =
1032          AOT_model_valid_in v (Rep_rel Π x)
1033      unfolding x_def
1034      by (smt (verit, best) AOT_rel_equiv_def Abs_rel_inverse Quotient3_def
1035            Π''_den Π''_prop Π_den κυ.simps(1) iso_tuple_UNIV_I s_prop
1036            urrel_quotient3 urrel_to_ωrel_def urrel_to_rel_def)
1037  qed
1038  ultimately show Π'. AOT_model_denotes Π'  AOT_model_enc κ' Π' 
1039     (v x. (w. AOT_model_concrete w x)  AOT_model_valid_in v (Rep_rel Π' x) =
1040                                             AOT_model_valid_in v (Rep_rel Π x))
1041    apply (safe intro!: exI[where x=Π''])
1042    by auto
1043qed
1044end
1045
1046textProducts of unary individual terms and individual terms are individual terms.
1047     A tuple is regular, if at most one element does not denote. I.e. a pair is
1048     regular, if the first (unary) element denotes and the second is regular (i.e.
1049     at most one of its recursive tuple elements does not denote), or the first does
1050     not denote, but the second denotes (i.e. all its recursive tuple elements
1051     denote).
1052instantiation prod :: (AOT_UnaryIndividualTerm, AOT_IndividualTerm) AOT_IndividualTerm
1053begin
1054definition AOT_model_regular_prod :: 'a×'b  bool where
1055  AOT_model_regular_prod  λ (x,y) . AOT_model_denotes x  AOT_model_regular y 
1056                                      ¬AOT_model_denotes x  AOT_model_denotes y
1057definition AOT_model_term_equiv_prod :: 'a×'b  'a×'b  bool where
1058  AOT_model_term_equiv_prod   λ (x1,y1) (x2,y2) .
1059    AOT_model_term_equiv x1 x2  AOT_model_term_equiv y1 y2
1060function AOT_model_irregular_prod :: ('a×'b  𝗈)  'a×'b  𝗈 where
1061  AOT_model_irregular_proj2: AOT_model_denotes x 
1062    AOT_model_irregular φ (x,y) =
1063    AOT_model_irregular (λy. φ (SOME x' . AOT_model_term_equiv x x', y)) y
1064| AOT_model_irregular_proj1: ¬AOT_model_denotes x  AOT_model_denotes y 
1065    AOT_model_irregular φ (x,y) =
1066    AOT_model_irregular (λx. φ (x, SOME y' . AOT_model_term_equiv y y')) x
1067| AOT_model_irregular_prod_generic: ¬AOT_model_denotes x  ¬AOT_model_denotes y 
1068    AOT_model_irregular φ (x,y) =
1069    (SOME Φ . AOT_model_irregular_spec Φ AOT_model_regular AOT_model_term_equiv)
1070      φ (x,y)
1071  by auto blast
1072termination using "termination" by blast
1073
1074instance proof
1075  obtain x :: 'a and y :: 'b where
1076    ¬AOT_model_denotes x and ¬AOT_model_denotes y
1077    by (meson AOT_model_nondenoting_ex AOT_model_denoting_ex)
1078  thus x::'a×'b. ¬AOT_model_denotes x
1079    by (auto simp: AOT_model_denotes_prod_def AOT_model_regular_prod_def)
1080next
1081  show equivp (AOT_model_term_equiv :: 'a×'b  'a×'b  bool)
1082    by (rule equivpI; rule reflpI sympI transpI;
1083        simp add: AOT_model_term_equiv_prod_def AOT_model_term_equiv_part_equivp
1084                  equivp_reflp prod.case_eq_if case_prod_unfold equivp_symp)
1085       (metis equivp_transp[OF AOT_model_term_equiv_part_equivp])
1086next
1087  show ¬AOT_model_regular x  ¬ AOT_model_denotes x for x :: 'a×'b
1088    by (metis (mono_tags, lifting) AOT_model_denotes_prod_def case_prod_unfold
1089          AOT_model_irregular_nondenoting AOT_model_regular_prod_def)
1090next
1091  fix x y :: 'a×'b
1092  show AOT_model_term_equiv x y  AOT_model_denotes x = AOT_model_denotes y
1093    by (metis (mono_tags, lifting) AOT_model_denotes_prod_def case_prod_beta
1094        AOT_model_term_equiv_denotes AOT_model_term_equiv_prod_def )
1095next
1096  fix x y :: 'a×'b
1097  show AOT_model_term_equiv x y  AOT_model_regular x = AOT_model_regular y
1098    by (induct x; induct y;
1099        simp add: AOT_model_term_equiv_prod_def AOT_model_regular_prod_def)
1100       (meson AOT_model_term_equiv_denotes AOT_model_term_equiv_regular)
1101next
1102  interpret sp: AOT_model_irregular_spec λφ (x::'a×'b) . ε𝗈 w . False
1103                    AOT_model_regular AOT_model_term_equiv
1104    by (simp add: AOT_model_irregular_spec_def AOT_model_proposition_choice_simp)
1105  have ex_spec:  φ :: ('a×'b  𝗈)  'a×'b  𝗈 .
1106    AOT_model_irregular_spec φ AOT_model_regular AOT_model_term_equiv
1107    using sp.AOT_model_irregular_spec_axioms by blast
1108  have some_spec: AOT_model_irregular_spec
1109    (SOME φ :: ('a×'b  𝗈)  'a×'b  𝗈 .
1110        AOT_model_irregular_spec φ AOT_model_regular AOT_model_term_equiv)
1111    AOT_model_regular AOT_model_term_equiv
1112    using someI_ex[OF ex_spec] by argo
1113  interpret sp_some: AOT_model_irregular_spec
1114    SOME φ :: ('a×'b  𝗈)  'a×'b  𝗈 .
1115        AOT_model_irregular_spec φ AOT_model_regular AOT_model_term_equiv
1116    AOT_model_regular AOT_model_term_equiv
1117    using some_spec by blast
1118  show AOT_model_irregular_spec (AOT_model_irregular :: ('a×'b  𝗈)  'a×'b  𝗈)
1119          AOT_model_regular AOT_model_term_equiv
1120  proof
1121    have ¬AOT_model_valid_in w (AOT_model_irregular φ (a, b))
1122      for w φ and a :: 'a and b :: 'b
1123      by (induct arbitrary: φ rule: AOT_model_irregular_prod.induct)
1124         (auto simp: AOT_model_irregular_false sp_some.AOT_model_irregular_false)
1125    thus "¬AOT_model_valid_in w (AOT_model_irregular φ x)" for w φ and x :: 'a×'b
1126      by (induct x)
1127  next
1128    {
1129      fix x1 y1 :: 'a and x2 y2 :: 'b and φ :: 'a×'b𝗈
1130      assume x1y1_equiv: AOT_model_term_equiv x1 y1
1131      moreover assume x2y2_equiv: AOT_model_term_equiv x2 y2
1132      ultimately have xy_equiv: AOT_model_term_equiv (x1,x2) (y1,y2)
1133        by (simp add: AOT_model_term_equiv_prod_def)
1134      {
1135        assume AOT_model_denotes x1
1136        moreover hence AOT_model_denotes y1
1137          using AOT_model_term_equiv_denotes AOT_model_term_equiv_regular
1138                x1y1_equiv x2y2_equiv by blast
1139        ultimately have AOT_model_irregular φ (x1,x2) =
1140                         AOT_model_irregular φ (y1,y2)
1141          using AOT_model_irregular_equiv AOT_model_term_equiv_eps(3)
1142                x1y1_equiv x2y2_equiv by fastforce
1143      }
1144      moreover {
1145        assume ~AOT_model_denotes x1  AOT_model_denotes x2
1146        moreover hence ~AOT_model_denotes y1  AOT_model_denotes y2
1147          by (meson AOT_model_term_equiv_denotes x1y1_equiv x2y2_equiv)
1148        ultimately have AOT_model_irregular φ (x1,x2) =
1149                         AOT_model_irregular φ (y1,y2)
1150          using AOT_model_irregular_equiv AOT_model_term_equiv_eps(3)
1151                x1y1_equiv x2y2_equiv by fastforce
1152      }
1153      moreover {
1154        assume denotes_x: (¬AOT_model_denotes x1  ¬AOT_model_denotes x2)
1155        hence denotes_y: (¬AOT_model_denotes y1  ¬AOT_model_denotes y2)
1156          by (meson AOT_model_term_equiv_denotes AOT_model_term_equiv_regular
1157                    x1y1_equiv x2y2_equiv)
1158        have eps_eq: Eps (AOT_model_term_equiv x1) = Eps (AOT_model_term_equiv y1)
1159          by (simp add: AOT_model_term_equiv_eps(3) x1y1_equiv)
1160        have AOT_model_irregular φ (x1,x2) = AOT_model_irregular φ (y1,y2)
1161          using denotes_x denotes_y
1162          using sp_some.AOT_model_irregular_equiv xy_equiv by auto
1163      }
1164      moreover {
1165        assume denotes_x: ¬AOT_model_denotes x1  AOT_model_denotes x2
1166        hence denotes_y: ¬AOT_model_denotes y1  AOT_model_denotes y2
1167          by (meson AOT_model_term_equiv_denotes x1y1_equiv x2y2_equiv)
1168        have eps_eq: Eps (AOT_model_term_equiv x2) = Eps (AOT_model_term_equiv y2)
1169          by (simp add: AOT_model_term_equiv_eps(3) x2y2_equiv)
1170        have AOT_model_irregular φ (x1,x2) = AOT_model_irregular φ (y1,y2)
1171          using denotes_x denotes_y
1172          using AOT_model_irregular_nondenoting calculation(2) by blast
1173      }
1174      ultimately have AOT_model_irregular φ (x1,x2) = AOT_model_irregular φ (y1,y2)
1175        using AOT_model_term_equiv_denotes AOT_model_term_equiv_regular
1176              sp_some.AOT_model_irregular_equiv x1y1_equiv x2y2_equiv xy_equiv
1177        by blast
1178    } note 0 = this
1179    show AOT_model_term_equiv x y 
1180          AOT_model_irregular φ x = AOT_model_irregular φ y
1181      for x y :: 'a×'b and φ
1182      by (induct x; induct y; simp add: AOT_model_term_equiv_prod_def 0)
1183  next
1184    fix φ ψ :: 'a×'b  𝗈
1185    assume AOT_model_regular x  φ x = ψ x for x
1186    hence φ (x, y) = ψ (x, y)
1187      if AOT_model_denotes x  AOT_model_regular y 
1188          ¬AOT_model_denotes x  AOT_model_denotes y for x y
1189      using that unfolding AOT_model_regular_prod_def by simp
1190    hence AOT_model_irregular φ (x,y) = AOT_model_irregular ψ (x,y)
1191      for x :: 'a and y :: 'b
1192    proof (induct arbitrary: ψ φ rule: AOT_model_irregular_prod.induct)
1193      case (1 x y φ)
1194      thus ?case
1195        apply simp
1196        by (meson AOT_model_irregular_eqI AOT_model_irregular_nondenoting
1197                  AOT_model_term_equiv_denotes AOT_model_term_equiv_eps(1))
1198    next
1199      case (2 x y φ)
1200      thus ?case
1201        apply simp
1202        by (meson AOT_model_irregular_nondenoting AOT_model_term_equiv_denotes
1203                  AOT_model_term_equiv_eps(1))
1204    next
1205      case (3 x y φ)
1206      thus ?case
1207        apply simp
1208        by (metis (mono_tags, lifting) AOT_model_regular_prod_def case_prod_conv
1209                                       sp_some.AOT_model_irregular_eqI surj_pair)
1210    qed
1211    thus AOT_model_irregular φ x = AOT_model_irregular ψ x for  x :: 'a×'b
1212      by (metis surjective_pairing)
1213  qed
1214qed
1215end
1216
1217textIntroduction rules for term equivalence on tuple terms.
1218lemma AOT_meta_prod_equivI:
1219  shows " (a::'a::AOT_UnaryIndividualTerm) x (y :: 'b::AOT_IndividualTerm) .
1220            AOT_model_term_equiv x y  AOT_model_term_equiv (a,x) (a,y)"
1221    and " (x::'a::AOT_UnaryIndividualTerm) y (b :: 'b::AOT_IndividualTerm) .
1222            AOT_model_term_equiv x y  AOT_model_term_equiv (x,b) (y,b)"
1223    unfolding AOT_model_term_equiv_prod_def
1224    by (simp add: AOT_model_term_equiv_part_equivp equivp_reflp)+
1225
1226textThe type of propositions are trivial instances of terms.
1227
1228instantiation 𝗈 :: AOT_Term
1229begin
1230definition AOT_model_denotes_𝗈 :: 𝗈  bool where
1231  AOT_model_denotes_𝗈  λ_. True
1232instance proof
1233  show x::𝗈. AOT_model_denotes x
1234    by (simp add: AOT_model_denotes_𝗈_def)
1235qed
1236end
1237
1238textAOT's variables are modelled by restricting the type of terms to those terms
1239     that denote.
1240typedef 'a AOT_var = { x :: 'a::AOT_Term . AOT_model_denotes x }
1241  morphisms AOT_term_of_var AOT_var_of_term
1242  by (simp add: AOT_model_denoting_ex)
1243
1244textSimplify automatically generated theorems and rules.
1245declare AOT_var_of_term_induct[induct del]
1246        AOT_var_of_term_cases[cases del]
1247        AOT_term_of_var_induct[induct del]
1248        AOT_term_of_var_cases[cases del]
1249lemmas AOT_var_of_term_inverse = AOT_var_of_term_inverse[simplified]
1250   and AOT_var_of_term_inject = AOT_var_of_term_inject[simplified]
1251   and AOT_var_of_term_induct =
1252          AOT_var_of_term_induct[simplified, induct type: AOT_var]
1253   and AOT_var_of_term_cases =
1254          AOT_var_of_term_cases[simplified, cases type: AOT_var]
1255   and AOT_term_of_var = AOT_term_of_var[simplified]
1256   and AOT_term_of_var_cases =
1257          AOT_term_of_var_cases[simplified, induct pred: AOT_term_of_var]
1258   and AOT_term_of_var_induct =
1259          AOT_term_of_var_induct[simplified, induct pred: AOT_term_of_var]
1260   and AOT_term_of_var_inverse = AOT_term_of_var_inverse[simplified]
1261   and AOT_term_of_var_inject = AOT_term_of_var_inject[simplified]
1262
1263textEquivalence by definition is modelled as necessary equivalence.
1264consts AOT_model_equiv_def :: 𝗈  𝗈  bool
1265specification(AOT_model_equiv_def)
1266  AOT_model_equiv_def: AOT_model_equiv_def φ ψ = ( v . AOT_model_valid_in v φ =
1267                                                         AOT_model_valid_in v ψ)
1268  by (rule exI[where x=λ φ ψ .  v . AOT_model_valid_in v φ =
1269                                       AOT_model_valid_in v ψ]) simp
1270
1271textIdentity by definition is modelled as identity for denoting terms plus
1272     co-denoting.
1273consts AOT_model_id_def :: ('b  'a::AOT_Term)  ('b  'a)  bool
1274specification(AOT_model_id_def)
1275  AOT_model_id_def: (AOT_model_id_def τ σ) = ( α . if AOT_model_denotes (σ α)
1276                                                     then τ α = σ α
1277                                                     else ¬AOT_model_denotes (τ α))
1278  by (rule exI[where x="λ τ σ .  α . if AOT_model_denotes (σ α)
1279                                      then τ α = σ α
1280                                      else ¬AOT_model_denotes (τ α)"])
1281     blast
1282textTo reduce definitions by identity without free variables to definitions
1283     by identity with free variables acting on the unit type, we give the unit type
1284     a trivial instantiation to @{class AOT_Term}.
1285instantiation unit :: AOT_Term
1286begin
1287definition AOT_model_denotes_unit :: unit  bool where
1288  AOT_model_denotes_unit  λ_. True
1289instance proof qed(simp add: AOT_model_denotes_unit_def)
1290end
1291
1292textModally-strict and modally-fragile axioms are as necessary,
1293     resp. actually valid propositions.
1294definition AOT_model_axiom where
1295  AOT_model_axiom  λ φ .  v . AOT_model_valid_in v φ
1296definition AOT_model_act_axiom where
1297  AOT_model_act_axiom  λ φ . AOT_model_valid_in w0 φ
1298
1299lemma AOT_model_axiomI:
1300  assumes v . AOT_model_valid_in v φ
1301  shows AOT_model_axiom φ
1302  unfolding AOT_model_axiom_def using assms ..
1303
1304lemma AOT_model_act_axiomI:
1305  assumes AOT_model_valid_in w0 φ
1306  shows AOT_model_act_axiom φ
1307  unfolding AOT_model_act_axiom_def using assms .
1308
1309(*<*)
1310end
1311(*>*)