Theory AOT_PossibleWorlds

1(*<*)
2theory AOT_PossibleWorlds
3  imports AOT_PLM AOT_BasicLogicalObjects AOT_RestrictedVariables
4begin
5(*>*)
6
7section‹Possible Worlds›
8
9AOT_define Situation :: τ  φ (Situation'(_'))
10  "situations:1": Situation(x) df A!x & F (x[F]  Propositional([F]))
11
12(* TODO: temporary alias to keep the old key used for the definition working *)
13lemmas "situations" = "situations:1"
14
15AOT_theorem "situations:2": x Situation(x)
16proof -
17  AOT_have x (A!x & F (x[F]  F = y [R]ab]))
18    using "A-objects" "vdash-properties:1[2]" by auto
19  then AOT_obtain c where c_prop: A!c & F (c[F]  F = y [R]ab])
20    using "∃E" by meson
21  AOT_have Situation(c)
22  proof(safe intro!: "dfI"[OF "situations:1"] "&I" GEN "→I")
23    AOT_show A!c
24      using c_prop "&E" by blast
25  next
26    fix F
27    AOT_assume c[F]
28    AOT_hence F_eq: F = y [R]ab]
29      using "con-dis-i-e:2:b" "intro-elim:3:a" "rule-ui:3" c_prop by blast
30    AOT_find_theorems Propositional([Π])
31    AOT_show Propositional([F])
32    proof(rule "prop-prop1"[THEN "dfI"])
33      AOT_show "p F = y p]"
34        using F_eq "∃I"(1)
35        using "log-prop-prop:2" by fastforce
36    qed
37  qed
38  AOT_thus x Situation(x)
39    using "∃I" by blast
40qed
41
42AOT_theorem "situations:3": Situation(κ)  κ
43proof (rule "→I")
44  AOT_assume Situation(κ)
45  AOT_hence A!κ by (metis "dfE" "&E"(1) "situations:1")
46  AOT_thus κ by (metis "russell-axiom[exe,1].ψ_denotes_asm")
47qed
48
49AOT_theorem "T-sit": TruthValue(x)  Situation(x)
50proof(rule "→I")
51  AOT_assume TruthValue(x)
52  AOT_hence p TruthValueOf(x,p)
53    using "T-value"[THEN "dfE"] by blast
54  then AOT_obtain p where TruthValueOf(x,p) using "∃E"[rotated] by blast
55  AOT_hence θ: A!x & F (x[F]  q((q  p) & F = y q]))
56    using "tv-p"[THEN "dfE"] by blast
57  AOT_show Situation(x)
58  proof(rule "situations:1"[THEN "dfI"]; safe intro!: "&I" GEN "→I" θ[THEN "&E"(1)])
59    fix F
60    AOT_assume x[F]
61    AOT_hence q((q  p) & F = y q])
62      using θ[THEN "&E"(2), THEN "∀E"(2)[where β=F], THEN "≡E"(1)] by argo
63    then AOT_obtain q where (q  p) & F = y q] using "∃E"[rotated] by blast
64    AOT_hence p F = y p] using "&E"(2) "∃I"(2) by metis
65    AOT_thus Propositional([F])
66      by (metis "dfI" "prop-prop1")
67  qed
68qed
69
70AOT_theorem "possit-sit:1": Situation(x)  Situation(x)
71proof(rule "≡I"; rule "→I")
72  AOT_assume Situation(x)
73  AOT_hence 0: A!x & F (x[F]  Propositional([F]))
74    using "situations:1"[THEN "dfE"] by blast
75  AOT_have 1: (A!x & F (x[F]  Propositional([F])))
76  proof(rule "KBasic:3"[THEN "≡E"(2)]; rule "&I")
77    AOT_show A!x using 0[THEN "&E"(1)] by (metis "oa-facts:2"[THEN "→E"])
78  next
79    AOT_have F (x[F]  Propositional([F]))  F (x[F]  Propositional([F]))
80      by (AOT_subst Propositional([F]) p (F = y p]) for: F :: ‹<κ>›)
81         (auto simp: "prop-prop1" "≡Df" "enc-prop-nec:2")
82    AOT_thus F (x[F]  Propositional([F]))
83      using 0[THEN "&E"(2)] "→E" by blast
84  qed
85  AOT_show Situation(x)
86    by (AOT_subst Situation(x) A!x & F (x[F]  Propositional([F])))
87       (auto simp: 1 "≡Df" "situations:1")
88next
89  AOT_show Situation(x) if Situation(x)
90    using "qml:2"[axiom_inst, THEN "→E", OF that].
91qed
92
93AOT_theorem "possit-sit:2": Situation(x)  Situation(x)
94  using "possit-sit:1"
95  by (metis "RE◇" "S5Basic:2" "≡E"(1) "≡E"(5) "Commutativity of ≡")
96
97AOT_theorem "possit-sit:3": Situation(x)  Situation(x)
98  using "possit-sit:1" "possit-sit:2" by (meson "≡E"(5))
99
100AOT_theorem "possit-sit:4": 𝒜Situation(x)  Situation(x)
101  by (meson "Act-Basic:5" "Act-Sub:2" "RA[2]" "≡E"(1) "≡E"(6) "possit-sit:2")
102
103AOT_theorem "possit-sit:5": Situation(p)
104proof (safe intro!: "situations:1"[THEN "dfI"] "&I" GEN "→I" "prop-prop1"[THEN "dfI"])
105  AOT_have F p[F]
106    using "tv-id:2"[THEN "prop-enc"[THEN "dfE"], THEN "&E"(2)]
107          "existential:1" "prop-prop2:2" by blast
108  AOT_thus A!p
109    by (safe intro!: "encoders-are-abstract"[unvarify x, THEN "→E"]
110                     "t=t-proper:2"[THEN "→E", OF "ext-p-tv:3"])
111next
112  fix F
113  AOT_assume p[F]
114  AOT_hence ιx(A!x & F (x[F]  q ((q  p) & F = y q])))[F]
115    using "tv-id:1" "rule=E" by fast
116  AOT_hence 𝒜q ((q  p) & F = y q])
117    using "≡E"(1) "desc-nec-encode:1" by fast
118  AOT_hence q 𝒜((q  p) & F = y q])
119    by (metis "Act-Basic:10" "≡E"(1))
120  then AOT_obtain q where 𝒜((q  p) & F = y q]) using "∃E"[rotated] by blast
121  AOT_hence 𝒜F = y q] by (metis "Act-Basic:2" "con-dis-i-e:2:b" "intro-elim:3:a")
122  AOT_hence F = y q]
123    using "id-act:1"[unvarify β, THEN "≡E"(2)] by (metis "prop-prop2:2")
124  AOT_thus p F = y p]
125    using "∃I" by fast
126qed
127
128AOT_theorem "possit-sit:6": Situation()
129proof -
130  AOT_have true_def:   = ιx (A!x & F (x[F]  p(p & F = y p])))
131    by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:1")
132  AOT_hence true_den:  
133    using "t=t-proper:1" "vdash-properties:6" by blast
134  AOT_have 𝒜TruthValue()
135    using "actual-desc:2"[unvarify x, OF true_den, THEN "→E", OF true_def]
136    using "TV-lem2:1"[unvarify x, OF true_den, THEN "RA[2]",
137                      THEN "act-cond"[THEN "→E"], THEN "→E"]
138    by blast
139  AOT_hence 𝒜Situation()
140    using "T-sit"[unvarify x, OF true_den, THEN "RA[2]",
141                  THEN "act-cond"[THEN "→E"], THEN "→E"] by blast
142  AOT_thus Situation()
143    using "possit-sit:4"[unvarify x, OF true_den, THEN "≡E"(1)] by blast
144qed
145
146AOT_theorem "possit-sit:7": Situation()
147proof -
148  AOT_have true_def:   = ιx (A!x & F (x[F]  p(¬p & F = y p])))
149    by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:2")
150  AOT_hence true_den:  
151    using "t=t-proper:1" "vdash-properties:6" by blast
152  AOT_have 𝒜TruthValue()
153    using "actual-desc:2"[unvarify x, OF true_den, THEN "→E", OF true_def]
154    using "TV-lem2:2"[unvarify x, OF true_den, THEN "RA[2]",
155                      THEN "act-cond"[THEN "→E"], THEN "→E"]
156    by blast
157  AOT_hence 𝒜Situation()
158    using "T-sit"[unvarify x, OF true_den, THEN "RA[2]",
159                  THEN "act-cond"[THEN "→E"], THEN "→E"] by blast
160  AOT_thus Situation()
161    using "possit-sit:4"[unvarify x, OF true_den, THEN "≡E"(1)] by blast
162qed
163
164AOT_register_rigid_restricted_type
165  Situation: Situation(κ)
166proof
167  AOT_modally_strict {
168    AOT_show x Situation(x)
169      using "situations:2".
170  }
171next
172  AOT_modally_strict {
173    AOT_show Situation(κ)  κ for κ
174      using "situations:3".
175  }
176next
177  AOT_modally_strict {
178    AOT_show α(Situation(α)  Situation(α))
179      using "possit-sit:1"[THEN "conventions:3"[THEN "dfE"],
180                           THEN "&E"(1)] GEN by fast
181  }
182qed
183
184AOT_register_variable_names
185  Situation: s
186
187AOT_define TruthInSituation :: τ  φ  φ ("(_ / _)" [100, 40] 100)
188  "true-in-s": s  p df sΣp
189
190notepad
191begin
192  (* Verify precedence. *)
193  fix x p q
194  have «x  p  q» = «(x  p)  q»
195    by simp
196  have «x  p & q» = «(x  p) & q»
197    by simp
198  have «x  ¬p» = «x  (¬p)»
199    by simp
200  have «x  p» = «x  (p)»
201    by simp
202  have «x  𝒜p» = «x  (𝒜p)»
203    by simp
204  have «x  p» = «(x  p)»
205    by simp
206  have «¬x  p» = «¬(x  p)»
207    by simp
208end
209
210
211AOT_theorem lem1: Situation(x)  (x  p  xy p])
212proof (rule "→I"; rule "≡I"; rule "→I")
213  AOT_assume Situation(x)
214  AOT_assume x  p
215  AOT_hence xΣp
216    using "true-in-s"[THEN "dfE"] "&E" by blast
217  AOT_thus xy p] using "prop-enc"[THEN "dfE"] "&E" by blast
218next
219  AOT_assume 1: Situation(x)
220  AOT_assume xy p]
221  AOT_hence xΣp
222    using "prop-enc"[THEN "dfI", OF "&I", OF "cqt:2"(1)] by blast
223  AOT_thus x  p
224    using "true-in-s"[THEN "dfI"] 1 "&I" by blast
225qed
226
227AOT_theorem "lem2:1": s  p  s  p
228proof -
229  AOT_have sit: Situation(s)
230    by (simp add: Situation.ψ)
231  AOT_have s  p  sy p]
232    using lem1[THEN "→E", OF sit] by blast
233  also AOT_have   sy p]
234    by (rule "en-eq:2[1]"[unvarify F]) "cqt:2[lambda]"
235  also AOT_have   s  p
236    using lem1[THEN RM, THEN "→E", OF "possit-sit:1"[THEN "≡E"(1), OF sit]]
237    by (metis "KBasic:6" "≡E"(2) "Commutativity of ≡" "→E")
238  finally show ?thesis.
239qed
240
241AOT_theorem "lem2:2": s  p  s  p
242proof -
243  AOT_have (s  p  s  p)
244    using "possit-sit:1"[THEN "≡E"(1), OF Situation.ψ]
245          "lem2:1"[THEN "conventions:3"[THEN "dfE", THEN "&E"(1)]]
246          RM[OF "→I", THEN "→E"] by blast
247  thus ?thesis by (metis "B◇" "S5Basic:13" "T◇" "≡I" "≡E"(1) "→E")
248qed
249
250AOT_theorem "lem2:3": s  p  s  p
251  using "lem2:1" "lem2:2" by (metis "≡E"(5))
252
253AOT_theorem "lem2:4": 𝒜(s  p)  s  p
254proof -
255  AOT_have (s  p  s  p)
256    using "possit-sit:1"[THEN "≡E"(1), OF Situation.ψ]
257      "lem2:1"[THEN "conventions:3"[THEN "dfE", THEN "&E"(1)]]
258      RM[OF "→I", THEN "→E"] by blast
259  thus ?thesis
260    using "sc-eq-fur:2"[THEN "→E"] by blast
261qed
262
263AOT_theorem "lem2:5": ¬s  p  ¬s  p
264  by (metis "KBasic2:1" "contraposition:1[2]" "→I" "≡I" "≡E"(3) "≡E"(4) "lem2:2")
265
266AOT_theorem "sit-identity": s = s'  p(s  p  s'  p)
267proof(rule "≡I"; rule "→I")
268  AOT_assume s = s'
269  moreover AOT_have p(s  p  s  p)
270    by (simp add: "oth-class-taut:3:a" "universal-cor")
271  ultimately AOT_show p(s  p  s'  p)
272    using "rule=E" by fast
273next
274  AOT_assume a: p (s  p  s'  p)
275  AOT_show s = s'
276  proof(safe intro!: "ab-obey:1"[THEN "→E", THEN "→E"] "&I" GEN "≡I" "→I")
277    AOT_show A!s using Situation.ψ "dfE" "&E"(1) situations by blast
278  next
279    AOT_show A!s' using Situation.ψ "dfE" "&E"(1) situations by blast
280  next
281    fix F
282    AOT_assume 0: s[F]
283    AOT_hence p (F = y p])
284      using Situation.ψ[THEN situations[THEN "dfE"], THEN "&E"(2),
285                        THEN "∀E"(2)[where β=F], THEN "→E"]
286            "prop-prop1"[THEN "dfE"] by blast
287    then AOT_obtain p where F_def: F = y p]
288      using "∃E" by metis
289    AOT_hence sy p]
290      using 0 "rule=E" by blast
291    AOT_hence s  p
292      using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(2)] by blast
293    AOT_hence s'  p
294      using a[THEN "∀E"(2)[where β=p], THEN "≡E"(1)] by blast
295    AOT_hence s'y p]
296      using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(1)] by blast
297    AOT_thus s'[F]
298      using F_def[symmetric] "rule=E" by blast
299  next
300    fix F
301    AOT_assume 0: s'[F]
302    AOT_hence p (F = y p])
303      using Situation.ψ[THEN situations[THEN "dfE"], THEN "&E"(2),
304                        THEN "∀E"(2)[where β=F], THEN "→E"]
305            "prop-prop1"[THEN "dfE"] by blast
306    then AOT_obtain p where F_def: F = y p]
307      using "∃E" by metis
308    AOT_hence s'y p]
309      using 0 "rule=E" by blast
310    AOT_hence s'  p
311      using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(2)] by blast
312    AOT_hence s  p
313      using a[THEN "∀E"(2)[where β=p], THEN "≡E"(2)] by blast
314    AOT_hence sy p]
315      using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(1)] by blast
316    AOT_thus s[F]
317      using F_def[symmetric] "rule=E" by blast
318  qed
319qed
320
321AOT_define PartOfSituation :: τ  τ  φ (infixl  80)
322  "sit-part-whole": s  s' df p (s  p  s'  p)
323AOT_theorem "part:1": s  s
324  by (rule "sit-part-whole"[THEN "dfI"])
325     (safe intro!: "&I" Situation.ψ GEN "→I")
326
327AOT_theorem "part:2": s  s' & s  s'  ¬(s'  s)
328proof(rule "→I"; frule "&E"(1); drule "&E"(2); rule "raa-cor:2")
329  AOT_assume 0: s  s'
330  AOT_hence a: s  p  s'  p for p
331    using "∀E"(2) "sit-part-whole"[THEN "dfE"] "&E" by blast
332  AOT_assume s'  s
333  AOT_hence b: s'  p  s  p for p
334    using "∀E"(2) "sit-part-whole"[THEN "dfE"] "&E" by blast
335  AOT_have p (s  p  s'  p)
336    using a b by (simp add: "≡I" "universal-cor")
337  AOT_hence 1: s = s'
338    using "sit-identity"[THEN "≡E"(2)] by metis
339  AOT_assume s  s'
340  AOT_hence ¬(s = s')
341    by (metis "dfE" "=-infix")
342  AOT_thus s = s' & ¬(s = s')
343    using 1 "&I" by blast
344qed
345
346AOT_theorem "part:3": s  s' & s'  s''  s  s''
347proof(rule "→I"; frule "&E"(1); drule "&E"(2);
348      safe intro!: "&I" GEN "→I" "sit-part-whole"[THEN "dfI"] Situation.ψ)
349  fix p
350  AOT_assume s  p
351  moreover AOT_assume s  s'
352  ultimately AOT_have s'  p
353    using "sit-part-whole"[THEN "dfE", THEN "&E"(2),
354                           THEN "∀E"(2)[where β=p], THEN "→E"] by blast
355  moreover AOT_assume s'  s''
356  ultimately AOT_show s''  p
357    using "sit-part-whole"[THEN "dfE", THEN "&E"(2),
358                           THEN "∀E"(2)[where β=p], THEN "→E"] by blast
359qed
360
361AOT_theorem "sit-identity2:1": s = s'  s  s' & s'  s
362proof (safe intro!: "≡I" "&I" "→I")
363  AOT_show s  s' if s = s'
364    using "rule=E" "part:1" that by blast
365next
366  AOT_show s'  s if s = s'
367    using "rule=E" "part:1" that[symmetric] by blast
368next
369  AOT_assume s  s' & s'  s
370  AOT_thus s = s' using "part:2"[THEN "→E", OF "&I"]
371    by (metis "dfI" "&E"(1) "&E"(2) "=-infix" "raa-cor:3")
372qed
373
374AOT_theorem "sit-identity2:2": s = s'  s'' (s''  s  s''  s')
375proof(safe intro!: "≡I" "→I" Situation.GEN "sit-identity"[THEN "≡E"(2)]
376                   GEN[where 'a=𝗈])
377  AOT_show s''  s' if s''  s and s = s' for s''
378    using "rule=E" that by blast
379next
380  AOT_show s''  s if s''  s' and s = s' for s''
381    using "rule=E" id_sym that by blast
382next
383  AOT_show s'  p if s  p and s'' (s''  s  s''  s') for p
384    using "sit-part-whole"[THEN "dfE", THEN "&E"(2),
385              OF that(2)[THEN "Situation.∀E", THEN "≡E"(1), OF "part:1"],
386              THEN "∀E"(2), THEN "→E", OF that(1)].
387next
388  AOT_show s  p if s'  p and s'' (s''  s  s''  s') for p
389    using "sit-part-whole"[THEN "dfE", THEN "&E"(2),
390          OF that(2)[THEN "Situation.∀E", THEN "≡E"(2), OF "part:1"],
391          THEN "∀E"(2), THEN "→E", OF that(1)].
392qed
393
394(* TODO: removed in PLM *)
395AOT_define Persistent :: φ  φ (Persistent'(_'))
396  persistent: Persistent(p) df s (s  p  s' (s  s'  s'  p))
397
398AOT_theorem "pers-prop": p Persistent(p)
399  by (safe intro!: GEN[where 'a=𝗈] Situation.GEN persistent[THEN "dfI"] "→I")
400     (simp add: "sit-part-whole"[THEN "dfE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"])
401
402(* TODO: put this at the correct place *)
403AOT_theorem "sit-comp-simp:1": sp(s  p  φ{p})
404proof -
405  AOT_have x (A!x & F(x[F]  p (φ{p} & F = y p])))
406    using "A-objects" "vdash-properties:1[2]" by force
407  then AOT_obtain c where c_prop: A!c & F(c[F]  p (φ{p} & F = y p]))
408    using "∃E" by meson
409  AOT_have sit_c: Situation(c)
410  proof(safe intro!: "dfI"[OF situations] "&I" GEN "→I")
411    AOT_show A!c
412      using c_prop "&E" by blast
413  next
414    fix F
415    AOT_assume c[F]
416    AOT_hence F_eq: p (φ{p} & F = y p])
417      using "con-dis-i-e:2:b" "intro-elim:3:a" "rule-ui:3" c_prop by blast
418    then AOT_obtain q where q_prop: φ{q} & F = y q]
419      using "∃E" by meson
420    AOT_show Propositional([F])
421    proof(rule "prop-prop1"[THEN "dfI"])
422      AOT_show "p F = y p]"
423        using q_prop[THEN "&E"(2)] "∃I"(1)
424        by (metis "log-prop-prop:2")
425    qed
426  qed
427  moreover AOT_have p(c  p  φ{p})
428  proof(safe intro!: GEN "≡I" "→I")
429    fix p
430    AOT_assume c  p
431    AOT_hence 1: cy p]
432      using "intro-elim:3:a" "vdash-properties:10" calculation lem1 by blast
433    AOT_have q (φ{q} & y p] = y q])
434      by (safe intro!: c_prop[THEN "&E"(2), THEN "∀E"(1)[where τ="«y p]»"], THEN "≡E"(1)] 1 "cqt:2")
435    then AOT_obtain q where 2: φ{q} & y p] = y q]
436      using "∃E" by meson
437    AOT_hence p = q
438      using "con-dis-i-e:2:b" "intro-elim:3:b" "p-identity-thm2:3" by blast
439    AOT_thus φ{p}
440      using 2
441      using "con-dis-i-e:2:a" "rule=E" id_sym by blast
442  next
443    fix p
444    AOT_assume φ{p}
445    moreover AOT_have y p] = y p]
446      by (simp add: "prop-prop2:2" "rule=I:1")
447    ultimately AOT_have φ{p} & y p] = y p] using "&I" by blast
448    AOT_hence q (φ{q} & y p] = y q])
449      using "∃I" by fast
450    AOT_hence cy p]
451      by (safe intro!: c_prop[THEN "&E"(2), THEN "∀E"(1)[where τ="«y p]»"], THEN "≡E"(2)] "cqt:2")
452    AOT_thus c  p
453      by (metis "intro-elim:3:b" "vdash-properties:10" sit_c lem1)
454  qed
455  ultimately AOT_show sp(s  p  φ{p})
456    by (meson "con-dis-i-e:1" "existential:2[const_var]")
457qed
458
459AOT_theorem "sit-comp-simp:3": ιs p(s  p  φ{p})
460proof (safe intro!: "actual-desc:1"[THEN "≡E"(2)] "uniqueness:2"[THEN "≡E"(2)])
461  AOT_obtain s where s_prop: p(s  p  𝒜φ{p})
462    using "sit-comp-simp:1" Situation.instantiation[rotated] by meson
463  AOT_have y (𝒜(Situation(y) & p (y  p  φ{p}))  y = s)
464  proof(safe intro!: GEN "≡I" "→I")
465    fix y
466    AOT_assume 𝒜(Situation(y) & p (y  p  φ{p}))
467    AOT_hence 𝒜Situation(y) and 2: 𝒜p (y  p  φ{p})
468      using "&E" "Act-Basic:2" "≡E"(1) by blast+
469    AOT_hence y_sit: Situation(y)
470      using "intro-elim:3:a" "possit-sit:4" by blast
471    AOT_have p 𝒜(y  p  φ{p})
472      using 2 "≡E"(1) "logic-actual-nec:3"[axiom_inst] by blast
473    AOT_hence 𝒜(y  p  φ{p}) for p using "∀E" by blast
474    AOT_hence 3: 𝒜y  p  𝒜φ{p} for p
475      using "Act-Basic:5" "≡E"(1) by blast
476    AOT_show y = s
477    proof(safe intro!: "sit-identity"[unconstrain s, THEN "→E", OF y_sit, THEN "≡E"(2)] GEN "≡I" "→I")
478      fix p
479      AOT_assume y  p
480      AOT_hence 𝒜y  p
481        using "lem2:4"[unconstrain s, THEN "→E", OF y_sit]
482        using "intro-elim:3:b" by blast
483      AOT_hence 𝒜φ{p}
484        using 3 "intro-elim:3:a" by blast
485      AOT_thus s  p
486        using s_prop "intro-elim:3:b" "rule-ui:2[const_var]" by blast
487    next
488      fix p
489      AOT_assume s  p
490      AOT_hence 𝒜φ{p}
491        using "intro-elim:3:a" "rule-ui:3" s_prop by blast
492      AOT_hence 𝒜y  p
493        using "3" "intro-elim:3:b" by blast
494      AOT_thus y  p
495        using "lem2:4"[unconstrain s, THEN "→E", OF y_sit]
496        using "intro-elim:3:a" by blast
497    qed
498  next
499    fix y
500    AOT_assume y = s
501    moreover AOT_have 𝒜(Situation(s) & p (s  p  φ{p}))
502    proof(safe intro!: "act-conj-act:3"[THEN "→E"] "&I" "logic-actual-nec:3"[axiom_inst, THEN "≡E"(2)] GEN)
503      AOT_show 𝒜Situation(s)
504        using "≡E"(2) "possit-sit:4" "Situation.ψ" by blast
505    next
506      AOT_show 𝒜(s  p  φ{p}) for p
507      proof(safe intro!: "Act-Basic:5"[THEN "≡E"(2)] "≡I" "→I")
508        AOT_assume 𝒜s  p
509        AOT_hence s  p
510          using "intro-elim:3:a" "lem2:4" by blast
511        AOT_thus 𝒜φ{p}
512          using s_prop "intro-elim:3:a" "rule-ui:3" by blast
513      next
514        AOT_assume 𝒜φ{p}
515        AOT_hence s  p
516          using "intro-elim:3:b" "rule-ui:3" s_prop by blast
517        AOT_thus 𝒜s  p
518          using "intro-elim:3:b" "lem2:4" by blast
519      qed
520    qed
521    ultimately AOT_show 𝒜(Situation(y) & p (y  p  φ{p}))
522      using id_sym "l-identity"[axiom_inst, THEN "→E", THEN "→E"] by fast
523  qed
524  AOT_thus x y (𝒜(Situation(y) & p (y  p  φ{p}))  y = x)
525    using "∃I" by fast
526qed
527
528AOT_theorem "sit-comp-simp:4":
529  assumes RIGID_CONDITION(φ)
530  shows y = ιs p(s  p  φ{p})  p (y  p  φ{p})
531proof(rule "→I")
532  AOT_assume y = ιs(p (s  p  φ{p}))
533  AOT_hence 0: 𝒜(Situation(y) & p (y  p  φ{p}))
534    using "actual-desc:2" "→E" by blast
535  AOT_hence 𝒜p (y  p  φ{p})
536    using "Act-Basic:2" "con-dis-i-e:2:b" "intro-elim:3:a" by blast
537  AOT_hence 1: p 𝒜(y  p  φ{p})
538    using "intro-elim:3:a" "logic-actual-nec:3" "vdash-properties:1[2]" by blast
539
540  AOT_have sit_y: Situation(y)
541    using 0 "&E"(1) "Act-Basic:2" "intro-elim:3:a" "possit-sit:4" by blast
542
543  AOT_show p (y  p  φ{p})
544  proof(rule GEN)
545    fix p
546    AOT_have 𝒜(y  p  φ{p})
547      using 1 "∀E" by blast
548    AOT_hence 𝒜y  p  𝒜φ{p}
549      using "Act-Basic:5" "intro-elim:3:a" by blast
550    moreover {
551      AOT_have (φ{p}  φ{p})
552        using "strict-can:1[E]"[OF assms] RN "BFs:2" "→E" "∀E" by blast
553      AOT_hence 𝒜φ{p}  φ{p}
554        using "sc-eq-fur:2" "vdash-properties:10" by blast
555    }
556    ultimately AOT_show y  p  φ{p}
557      using "lem2:4"[unconstrain s, THEN "→E", OF sit_y]
558      by (meson "intro-elim:3:f")
559  qed
560qed
561
562
563AOT_theorem "sit-comp-simp-unique": ∃!sp(s  p  φ{p})
564proof(safe intro!: "uniqueness:1"[THEN "dfI"])
565  AOT_obtain s where s_prop: p(s  p  φ{p})
566    using "sit-comp-simp:1" Situation.instantiation[rotated] by meson
567  AOT_show α (Situation(α) & p (α  p  φ{p}) & β (Situation(β) & p (β  p  φ{p})  β = α))
568  proof(safe intro!: "∃I"(2) "&I")
569    AOT_show Situation(s)
570      using "Situation.ψ" by auto
571  next
572    AOT_show p(s  p  φ{p}) using s_prop.
573  next
574    AOT_show β (Situation(β) & p (β  p  φ{p})  β = s)
575    proof(safe intro!: GEN "→I")
576      fix x
577      AOT_assume 1: Situation(x) & p (x  p  φ{p})
578      AOT_show x = s
579      proof (safe intro!: "sit-identity"[unconstrain s, THEN "→E", THEN "≡E"(2)] 1[THEN "&E"(1)] GEN "≡I" "→I")
580        fix p
581        AOT_assume x  p
582        AOT_hence φ{p}
583          using "1" "con-dis-i-e:2:b" "intro-elim:3:a" "log-prop-prop:2" "rule-ui:1" by blast
584        AOT_thus s  p
585          using s_prop  "intro-elim:3:b" "log-prop-prop:2" "rule-ui:1" by blast
586      next
587        fix p
588        AOT_assume s  p
589        AOT_hence φ{p}
590          using "intro-elim:3:a" "log-prop-prop:2" "rule-ui:1" s_prop by blast
591        AOT_thus x  p
592          using "1" "con-dis-i-e:2:b" "intro-elim:3:b" "log-prop-prop:2" "rule-ui:1" by blast
593      qed
594    qed
595  qed
596qed
597
598AOT_define NullSituation :: τ  φ (NullSituation'(_'))
599  "df-null-trivial:1": NullSituation(s) df ¬p s  p
600
601AOT_define TrivialSituation :: τ  φ (TrivialSituation'(_'))
602  "df-null-trivial:2": TrivialSituation(s) df p s  p
603
604AOT_theorem "thm-null-trivial:1": ∃!x NullSituation(x)
605proof (AOT_subst NullSituation(x) A!x & F (x[F]  F  F) for: x)
606  AOT_modally_strict {
607    AOT_show NullSituation(x)  A!x & F (x[F]  F  F) for x
608    proof (safe intro!: "≡I" "→I" "df-null-trivial:1"[THEN "dfI"]
609                dest!: "df-null-trivial:1"[THEN "dfE"])
610      AOT_assume 0: Situation(x) & ¬p x  p
611      AOT_have 1: A!x
612        using 0[THEN "&E"(1), THEN situations[THEN "dfE"], THEN "&E"(1)].
613      AOT_have 2: x[F]  p F = y p] for F
614        using 0[THEN "&E"(1), THEN situations[THEN "dfE"],
615                THEN "&E"(2), THEN "∀E"(2)]
616        by (metis "dfE" "→I" "prop-prop1" "→E")
617      AOT_show A!x & F (x[F]  F  F)
618      proof (safe intro!: "&I" 1 GEN "≡I" "→I")
619        fix F
620        AOT_assume x[F]
621        moreover AOT_obtain p where F = y p]
622          using calculation 2[THEN "→E"] "∃E"[rotated] by blast
623        ultimately AOT_have xy p]
624          by (metis "rule=E")
625        AOT_hence x  p
626          using lem1[THEN "→E", OF 0[THEN "&E"(1)], THEN "≡E"(2)] by blast
627        AOT_hence p (x  p)
628          by (rule "∃I")
629        AOT_thus F  F
630          using 0[THEN "&E"(2)] "raa-cor:1" "&I" by blast
631      next
632        fix F :: <κ> AOT_var
633        AOT_assume F  F
634        AOT_hence ¬(F = F) by (metis "dfE" "=-infix")
635        moreover AOT_have F = F
636          by (simp add: "id-eq:1")
637        ultimately AOT_show x[F] using "&I" "raa-cor:1" by blast
638      qed
639    next
640      AOT_assume 0: A!x & F (x[F]  F  F)
641      AOT_hence x[F]  F  F for F
642        using "∀E" "&E" by blast
643      AOT_hence 1: ¬x[F] for F
644        using "dfE" "id-eq:1" "=-infix" "reductio-aa:1" "≡E"(1) by blast
645      AOT_show Situation(x) & ¬p x  p
646      proof (safe intro!: "&I" situations[THEN "dfI"] 0[THEN "&E"(1)] GEN "→I")
647        AOT_show Propositional([F]) if x[F] for F
648          using that 1 "&I" "raa-cor:1" by fast
649      next
650        AOT_show ¬p x  p
651        proof(rule "raa-cor:2")
652          AOT_assume p x  p
653          then AOT_obtain p where x  p using "∃E"[rotated] by blast
654          AOT_hence xy p]
655            using "dfE" "&E"(1) "≡E"(1) lem1 "modus-tollens:1"
656                  "raa-cor:3" "true-in-s" by fast
657          moreover AOT_have ¬xy p]
658            by (rule 1[unvarify F]) "cqt:2[lambda]"
659          ultimately AOT_show p & ¬p for p using "&I" "raa-cor:1" by blast
660        qed
661      qed
662    qed
663  }
664next
665  AOT_show ∃!x ([A!]x & F (x[F]  F  F))
666    by (simp add: "A-objects!")
667qed
668
669
670AOT_theorem "thm-null-trivial:2": ∃!x TrivialSituation(x)
671proof (AOT_subst TrivialSituation(x) A!x & F (x[F]  p F = y p]) for: x)
672  AOT_modally_strict {
673    AOT_show TrivialSituation(x)  A!x & F (x[F]  p F = y p]) for x
674    proof (safe intro!: "≡I" "→I" "df-null-trivial:2"[THEN "dfI"]
675                 dest!: "df-null-trivial:2"[THEN "dfE"])
676      AOT_assume 0: Situation(x) & p x  p
677      AOT_have 1: A!x
678        using 0[THEN "&E"(1), THEN situations[THEN "dfE"], THEN "&E"(1)].
679      AOT_have 2: x[F]  p F = y p] for F
680        using 0[THEN "&E"(1), THEN situations[THEN "dfE"],
681                THEN "&E"(2), THEN "∀E"(2)]
682        by (metis "dfE" "deduction-theorem" "prop-prop1" "→E")
683      AOT_show A!x & F (x[F]  p F = y p])
684      proof (safe intro!: "&I" 1 GEN "≡I" "→I" 2)
685        fix F
686        AOT_assume p F = y p]
687        then AOT_obtain p where F = y p]
688          using "∃E"[rotated] by blast
689        moreover AOT_have x  p
690          using 0[THEN "&E"(2)] "∀E" by blast
691        ultimately AOT_show x[F]
692          by (metis 0 "rule=E" "&E"(1) id_sym "≡E"(2) lem1
693                    "Commutativity of ≡" "→E")
694      qed
695    next
696      AOT_assume 0: A!x & F (x[F]  p F = y p])
697      AOT_hence 1: x[F]  p F = y p] for F
698        using "∀E" "&E" by blast
699      AOT_have 2: Situation(x)
700      proof (safe intro!: "&I" situations[THEN "dfI"] 0[THEN "&E"(1)] GEN "→I")
701        AOT_show Propositional([F]) if x[F] for F
702          using 1[THEN "≡E"(1), OF that]
703          by (metis "dfI" "prop-prop1")
704      qed
705      AOT_show Situation(x) & p (x  p)
706      proof (safe intro!: "&I" 2 0[THEN "&E"(1)] GEN "→I")
707        AOT_have xy p]  q y p] = y q] for p
708          by (rule 1[unvarify F, where τ="«y p]»"]) "cqt:2[lambda]"
709        moreover AOT_have q y p] = y q] for p
710          by (rule "∃I"(2)[where β=p])
711             (simp add: "rule=I:1" "prop-prop2:2")
712        ultimately AOT_have xy p] for p by (metis "≡E"(2))
713        AOT_thus x  p for p
714          by (metis "2" "≡E"(2) lem1 "→E")
715      qed
716    qed
717  }
718next
719  AOT_show ∃!x ([A!]x & F (x[F]  p F = y p]))
720    by (simp add: "A-objects!")
721qed
722
723AOT_theorem "thm-null-trivial:3": ιx NullSituation(x)
724  by (meson "A-Exists:2" "RA[2]" "≡E"(2) "thm-null-trivial:1")
725
726AOT_theorem "thm-null-trivial:4": ιx TrivialSituation(x)
727  using "A-Exists:2" "RA[2]" "≡E"(2) "thm-null-trivial:2" by blast
728
729AOT_define TheNullSituation :: κs (s)
730  "df-the-null-sit:1": s =df ιx NullSituation(x)
731
732AOT_define TheTrivialSituation :: κs (sV)
733  "df-the-null-sit:2": sV =df ιx TrivialSituation(x)
734
735AOT_theorem "null-triv-sc:1": NullSituation(x)  NullSituation(x)
736proof(safe intro!: "→I" dest!: "df-null-trivial:1"[THEN "dfE"];
737      frule "&E"(1); drule "&E"(2))
738  AOT_assume 1: ¬p (x  p)
739  AOT_assume 0: Situation(x)
740  AOT_hence Situation(x) by (metis "≡E"(1) "possit-sit:1")
741  moreover AOT_have ¬p (x  p)
742  proof(rule "raa-cor:1")
743    AOT_assume ¬¬p (x  p)
744    AOT_hence p (x  p)
745      by (metis "dfI" "conventions:5")
746    AOT_hence p (x  p) by (metis "BF◇" "→E")
747    then AOT_obtain p where (x  p) using "∃E"[rotated] by blast
748    AOT_hence x  p
749      by (metis "≡E"(1) "lem2:2"[unconstrain s, THEN "→E", OF 0])
750    AOT_hence p x  p using "∃I" by fast
751    AOT_thus p x  p & ¬p x  p using 1 "&I" by blast
752  qed
753  ultimately AOT_have 2: (Situation(x) & ¬p x  p)
754    by (metis "KBasic:3" "&I" "≡E"(2))
755  AOT_show NullSituation(x)
756    by (AOT_subst NullSituation(x) Situation(x) & ¬p x  p)
757       (auto simp: "df-null-trivial:1" "≡Df" 2)
758qed
759
760
761AOT_theorem "null-triv-sc:2": TrivialSituation(x)  TrivialSituation(x)
762proof(safe intro!: "→I" dest!: "df-null-trivial:2"[THEN "dfE"];
763      frule "&E"(1); drule "&E"(2))
764  AOT_assume 0: Situation(x)
765  AOT_hence 1: Situation(x) by (metis "≡E"(1) "possit-sit:1")
766  AOT_assume p x  p
767  AOT_hence x  p for p
768    using "∀E" by blast
769  AOT_hence x  p for p
770    using  0 "≡E"(1) "lem2:1"[unconstrain s, THEN "→E"] by blast
771  AOT_hence p x  p
772    by (rule GEN)
773  AOT_hence p x  p
774    by (rule BF[THEN "→E"])
775  AOT_hence 2: (Situation(x) & p x  p)
776    using 1 by (metis "KBasic:3" "&I" "≡E"(2))
777  AOT_show TrivialSituation(x)
778    by (AOT_subst TrivialSituation(x) Situation(x) & p x  p)
779       (auto simp: "df-null-trivial:2" "≡Df" 2)
780qed
781
782AOT_theorem "null-triv-sc:3": NullSituation(s)
783  by (safe intro!: "df-the-null-sit:1"[THEN "=dfI"(2)] "thm-null-trivial:3"
784       "rule=I:1"[OF "thm-null-trivial:3"]
785       "!box-desc:2"[THEN "→E", THEN "→E", rotated, OF "thm-null-trivial:1",
786                     OF "∀I", OF "null-triv-sc:1", THEN "∀E"(1), THEN "→E"])
787
788AOT_theorem "null-triv-sc:4": TrivialSituation(sV)
789  by (safe intro!: "df-the-null-sit:2"[THEN "=dfI"(2)] "thm-null-trivial:4"
790       "rule=I:1"[OF "thm-null-trivial:4"]
791       "!box-desc:2"[THEN "→E", THEN "→E", rotated, OF "thm-null-trivial:2",
792                     OF "∀I", OF "null-triv-sc:2", THEN "∀E"(1), THEN "→E"])
793
794AOT_theorem "null-triv-facts:1": NullSituation(x)  Null(x)
795proof (safe intro!: "≡I" "→I" "df-null-uni:1"[THEN "dfI"]
796                    "df-null-trivial:1"[THEN "dfI"]
797            dest!: "df-null-uni:1"[THEN "dfE"] "df-null-trivial:1"[THEN "dfE"])
798  AOT_assume 0: Situation(x) & ¬p x  p
799  AOT_have 1: x[F]  p F = y p] for F
800    using 0[THEN "&E"(1), THEN situations[THEN "dfE"], THEN "&E"(2), THEN "∀E"(2)]
801    by (metis "dfE" "deduction-theorem" "prop-prop1" "→E")
802  AOT_show A!x & ¬F x[F]
803  proof (safe intro!: "&I" 0[THEN "&E"(1), THEN situations[THEN "dfE"],
804                             THEN "&E"(1)];
805         rule "raa-cor:2")
806    AOT_assume F x[F]
807    then AOT_obtain F where F_prop: x[F]
808      using "∃E"[rotated] by blast
809    AOT_hence p F = y p]
810      using 1[THEN "→E"] by blast
811    then AOT_obtain p where F = y p]
812      using "∃E"[rotated] by blast
813    AOT_hence xy p]
814      by (metis "rule=E" F_prop)
815    AOT_hence x  p
816      using lem1[THEN "→E", OF 0[THEN "&E"(1)], THEN "≡E"(2)] by blast
817    AOT_hence p x  p
818      by (rule "∃I")
819    AOT_thus p x  p & ¬p x  p
820      using 0[THEN "&E"(2)] "&I" by blast
821  qed
822next
823  AOT_assume 0: A!x & ¬F x[F]
824  AOT_have Situation(x)
825    apply (rule situations[THEN "dfI", OF "&I", OF 0[THEN "&E"(1)]]; rule GEN)
826    using 0[THEN "&E"(2)] by (metis "→I" "existential:2[const_var]" "raa-cor:3") 
827  moreover AOT_have ¬p x  p
828  proof (rule "raa-cor:2")
829    AOT_assume p x  p
830    then AOT_obtain p where x  p by (metis "instantiation")
831    AOT_hence xy p] by (metis "dfE" "&E"(2) "prop-enc" "true-in-s")
832    AOT_hence F x[F] by (rule "∃I") "cqt:2[lambda]"
833    AOT_thus F x[F] & ¬F x[F] using 0[THEN "&E"(2)] "&I" by blast
834  qed
835  ultimately AOT_show Situation(x) & ¬p x  p using "&I" by blast
836qed
837
838AOT_theorem "null-triv-facts:2": s = a
839  apply (rule "=dfI"(2)[OF "df-the-null-sit:1"])
840   apply (fact "thm-null-trivial:3")
841  apply (rule "=dfI"(2)[OF "df-null-uni-terms:1"])
842   apply (fact "null-uni-uniq:3")
843  apply (rule "equiv-desc-eq:3"[THEN "→E"])
844  apply (rule "&I")
845   apply (fact "thm-null-trivial:3")
846  by (rule RN; rule GEN; rule "null-triv-facts:1")
847
848AOT_theorem "null-triv-facts:3": sV  aV
849proof(rule "=-infix"[THEN "dfI"])
850  AOT_have Universal(aV)
851    by (simp add: "null-uni-facts:4")
852  AOT_hence 0: aV[A!]
853    using "df-null-uni:2"[THEN "dfE"] "&E" "∀E"(1)
854    by (metis "cqt:5:a" "vdash-properties:10" "vdash-properties:1[2]")
855  moreover AOT_have 1: ¬sV[A!]
856  proof(rule "raa-cor:2")
857    AOT_have Situation(sV)
858      using "dfE" "&E"(1) "df-null-trivial:2" "null-triv-sc:4" by blast
859    AOT_hence F (sV[F]  Propositional([F]))
860      by (metis "dfE" "&E"(2) situations)
861    moreover AOT_assume sV[A!]
862    ultimately AOT_have Propositional(A!)
863      using "∀E"(1)[rotated, OF "oa-exist:2"] "→E" by blast
864    AOT_thus Propositional(A!) & ¬Propositional(A!)
865      using "prop-in-f:4:d" "&I" by blast
866  qed
867  AOT_show ¬(sV = aV)
868  proof (rule "raa-cor:2")
869    AOT_assume sV = aV
870    AOT_hence sV[A!] using 0 "rule=E" id_sym by fast
871    AOT_thus sV[A!] & ¬sV[A!] using 1 "&I" by blast
872  qed
873qed
874
875definition ConditionOnPropositionalProperties :: (<κ>  𝗈)  bool where
876  "cond-prop": ConditionOnPropositionalProperties  λ φ .  v .
877                        [v  F (φ{F}  Propositional([F]))]
878
879syntax ConditionOnPropositionalProperties :: id_position  AOT_prop
880  ("CONDITION'_ON'_PROPOSITIONAL'_PROPERTIES'(_')")
881
882AOT_theorem "cond-prop[E]":
883  assumes CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)
884  shows F (φ{F}  Propositional([F]))
885  using assms[unfolded "cond-prop"] by auto
886
887AOT_theorem "cond-prop[I]":
888  assumes  F (φ{F}  Propositional([F]))
889  shows CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)
890  using assms "cond-prop" by metis
891
892AOT_theorem "pre-comp-sit":
893  assumes CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)
894  shows (Situation(x) & F (x[F]  φ{F}))  (A!x & F (x[F]  φ{F}))
895proof(rule "≡I"; rule "→I")
896  AOT_assume Situation(x) & F (x[F]  φ{F})
897  AOT_thus A!x & F (x[F]  φ{F})
898    using "&E" situations[THEN "dfE"] "&I" by blast
899next
900  AOT_assume 0: A!x & F (x[F]  φ{F})
901  AOT_show Situation(x) & F (x[F]  φ{F})
902  proof (safe intro!: situations[THEN "dfI"] "&I")
903    AOT_show A!x using 0[THEN "&E"(1)].
904  next
905    AOT_show F (x[F]  Propositional([F]))
906    proof(rule GEN; rule "→I")
907      fix F
908      AOT_assume x[F]
909      AOT_hence φ{F}
910        using 0[THEN "&E"(2)] "∀E" "≡E" by blast
911      AOT_thus Propositional([F])
912        using "cond-prop[E]"[OF assms] "∀E" "→E" by blast
913    qed
914  next
915    AOT_show F (x[F]  φ{F}) using 0 "&E" by blast
916  qed
917qed
918
919AOT_theorem "comp-sit:1":
920  assumes CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)
921  shows s F(s[F]  φ{F})
922  by (AOT_subst Situation(x) & F(x[F]  φ{F}) A!x & F (x[F]  φ{F}) for: x)
923     (auto simp: "pre-comp-sit"[OF assms] "A-objects"[where φ=φ, axiom_inst])
924
925AOT_theorem "comp-sit:2":
926  assumes CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)
927  shows ∃!s F(s[F]  φ{F})
928  by (AOT_subst Situation(x) & F(x[F]  φ{F}) A!x & F (x[F]  φ{F}) for: x)
929     (auto simp: assms "pre-comp-sit"  "pre-comp-sit"[OF assms] "A-objects!")
930
931AOT_theorem "can-sit-desc:1":
932  assumes CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)
933  shows ιs(F (s[F]  φ{F}))
934  using "comp-sit:2"[OF assms] "A-Exists:2" "RA[2]" "≡E"(2) by blast
935
936AOT_theorem "can-sit-desc:2":
937  assumes CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)
938  shows ιs(F (s[F]  φ{F})) = ιx(A!x & F (x[F]  φ{F}))
939  by (auto intro!: "equiv-desc-eq:2"[THEN "→E", OF "&I",
940                                     OF "can-sit-desc:1"[OF assms]]
941                   "RA[2]" GEN "pre-comp-sit"[OF assms])
942
943AOT_theorem "strict-sit":
944  assumes RIGID_CONDITION(φ)
945      and CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)
946    shows y = ιs(F (s[F]  φ{F}))  F (y[F]  φ{F})
947  using "rule=E"[rotated, OF "can-sit-desc:2"[OF assms(2), symmetric]]
948        "box-phi-a:2"[OF assms(1)] "→E" "→I" "&E" by fast
949
950(* TODO: exercise (479) sit-lit *)
951
952AOT_define actual :: τ  φ (Actual'(_'))
953  Actual(s) df p (s  p  p)
954
955AOT_theorem "act-and-not-pos": s (Actual(s) & ¬Actual(s))
956proof -
957  AOT_obtain q1 where q1_prop: q1 & ¬q1
958    by (metis "dfE" "instantiation" "cont-tf:1" "cont-tf-thm:1")
959  AOT_have s (F (s[F]  F = y q1]))
960  proof (safe intro!: "comp-sit:1" "cond-prop[I]" GEN "→I")
961    AOT_modally_strict {
962      AOT_show Propositional([F]) if F = y q1] for F
963        using "dfI" "existential:2[const_var]" "prop-prop1" that by fastforce
964    }
965  qed
966  then AOT_obtain s1 where s_prop: F (s1[F]  F = y q1])
967    using "Situation.∃E"[rotated] by meson
968  AOT_have Actual(s1)
969  proof(safe intro!: actual[THEN "dfI"] "&I" GEN "→I" s_prop Situation.ψ)
970    fix p
971    AOT_assume s1  p
972    AOT_hence s1y p]
973      by (metis "dfE" "&E"(2) "prop-enc" "true-in-s")
974    AOT_hence y p] = y q1]
975      by (rule s_prop[THEN "∀E"(1), THEN "≡E"(1), rotated]) "cqt:2[lambda]"
976    AOT_hence p = q1 by (metis "≡E"(2) "p-identity-thm2:3")
977    AOT_thus p using q1_prop[THEN "&E"(1)] "rule=E" id_sym by fast
978  qed
979  moreover AOT_have ¬Actual(s1)
980  proof(rule "raa-cor:1"; drule "KBasic:12"[THEN "≡E"(2)])
981    AOT_assume Actual(s1)
982    AOT_hence (Situation(s1) & p (s1  p  p))
983      using actual[THEN "≡Df", THEN "conventions:3"[THEN "dfE"],
984                   THEN "&E"(1), THEN RM, THEN "→E"] by blast
985    AOT_hence p (s1  p  p)
986      by (metis "RM:1" "Conjunction Simplification"(2) "→E")
987    AOT_hence p (s1  p  p)
988      by (metis "CBF" "vdash-properties:10")
989    AOT_hence (s1  q1  q1)
990      using "∀E" by blast
991    AOT_hence s1  q1  q1
992      by (metis "→E" "qml:1" "vdash-properties:1[2]")
993    moreover AOT_have s1  q1
994      using s_prop[THEN "∀E"(1), THEN "≡E"(2),
995                   THEN lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(2)]]
996            "rule=I:1" "prop-prop2:2" by blast
997    ultimately AOT_have q1
998      using "dfE" "&E"(1) "≡E"(1) "lem2:1" "true-in-s" "→E" by fast
999    AOT_thus ¬q1 & ¬¬q1
1000      using "KBasic:12"[THEN "≡E"(1)] q1_prop[THEN "&E"(2)] "&I" by blast
1001  qed
1002  ultimately AOT_have (Actual(s1) & ¬Actual(s1))
1003    using s_prop "&I" by blast
1004  thus ?thesis
1005    by (rule "Situation.∃I")
1006qed
1007
1008AOT_theorem "actual-s:1": s Actual(s)
1009proof -
1010  AOT_obtain s where (Actual(s) & ¬Actual(s))
1011    using "act-and-not-pos" "Situation.∃E"[rotated] by meson
1012  AOT_hence Actual(s) using "&E" "&I" by metis
1013  thus ?thesis by (rule "Situation.∃I")
1014qed
1015
1016AOT_theorem "actual-s:2": s ¬Actual(s)
1017proof(rule "∃I"(1)[where τ=«sV»]; (rule "&I")?)
1018  AOT_show Situation(sV)
1019    using "dfE" "&E"(1) "df-null-trivial:2" "null-triv-sc:4" by blast
1020next
1021  AOT_show ¬Actual(sV)
1022  proof(rule "raa-cor:2")
1023    AOT_assume 0: Actual(sV)
1024    AOT_obtain p1 where notp1: ¬p1
1025      by (metis "∃E" "∃I"(1) "log-prop-prop:2" "non-contradiction")
1026    AOT_have sV  p1
1027      using "null-triv-sc:4"[THEN "dfE"[OF "df-null-trivial:2"], THEN "&E"(2)]
1028            "∀E" by blast
1029    AOT_hence p1
1030      using 0[THEN actual[THEN "dfE"], THEN "&E"(2), THEN "∀E"(2), THEN "→E"]
1031      by blast
1032    AOT_thus p & ¬p for p using notp1 by (metis "raa-cor:3")
1033  qed
1034next
1035  AOT_show sV
1036    using "df-the-null-sit:2" "rule-id-df:2:b[zero]" "thm-null-trivial:4" by blast
1037qed
1038
1039AOT_theorem "actual-s:3": ps(Actual(s)  ¬s  p)
1040proof -
1041  AOT_obtain p1 where notp1: ¬p1
1042    by (metis "∃E" "∃I"(1) "log-prop-prop:2" "non-contradiction")
1043  AOT_have s (Actual(s)  ¬(s  p1))
1044  proof (rule Situation.GEN; rule "→I"; rule "raa-cor:2")
1045    fix s
1046    AOT_assume Actual(s)
1047    moreover AOT_assume s  p1
1048    ultimately AOT_have p1
1049      using actual[THEN "dfE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"] by blast
1050    AOT_thus p1 & ¬p1
1051      using notp1 "&I" by simp
1052  qed
1053  thus ?thesis by (rule "∃I")
1054qed
1055
1056AOT_theorem comp:
1057  s (s'  s & s''  s & s''' (s'  s''' & s''  s'''  s  s'''))
1058proof -
1059  have cond_prop: ConditionOnPropositionalProperties (λ Π . «s'[Π]  s''[Π]»)
1060  proof(safe intro!: "cond-prop[I]" GEN "oth-class-taut:8:c"[THEN "→E", THEN "→E"];
1061        rule "→I")
1062    AOT_modally_strict {
1063      fix F
1064      AOT_have Situation(s')
1065        by (simp add: Situation.restricted_var_condition)
1066      AOT_hence s'[F]  Propositional([F])
1067        using "situations"[THEN "dfE", THEN "&E"(2), THEN "∀E"(2)] by blast
1068      moreover AOT_assume s'[F]
1069      ultimately AOT_show Propositional([F])
1070        using "→E" by blast
1071    }
1072  next
1073    AOT_modally_strict {
1074      fix F
1075      AOT_have Situation(s'')
1076        by (simp add: Situation.restricted_var_condition)
1077      AOT_hence s''[F]  Propositional([F])
1078        using "situations"[THEN "dfE", THEN "&E"(2), THEN "∀E"(2)] by blast
1079      moreover AOT_assume s''[F]
1080      ultimately AOT_show Propositional([F])
1081        using "→E" by blast
1082    }
1083  qed
1084  AOT_obtain s3 where θ: F (s3[F]  s'[F]  s''[F])
1085    using "comp-sit:1"[OF cond_prop] "Situation.∃E"[rotated] by meson
1086  AOT_have s'  s3 & s''  s3 & s''' (s'  s''' & s''  s'''  s3  s''')
1087  proof(safe intro!: "&I" "dfI"[OF "true-in-s"] "dfI"[OF "prop-enc"]
1088                     "Situation.GEN" "GEN"[where 'a=𝗈] "→I"
1089                     "sit-part-whole"[THEN "dfI"]
1090                     Situation.ψ "cqt:2[const_var]"[axiom_inst])
1091    fix p
1092    AOT_assume s'  p
1093    AOT_hence s'x p]
1094      by (metis "&E"(2) "prop-enc" "dfE" "true-in-s")
1095    AOT_thus s3x p]
1096      using θ[THEN "∀E"(1),OF "prop-prop2:2", THEN "≡E"(2), OF "∨I"(1)] by blast
1097  next
1098    fix p
1099    AOT_assume s''  p
1100    AOT_hence s''x p]
1101      by (metis "&E"(2) "prop-enc" "dfE" "true-in-s")
1102    AOT_thus s3x p]
1103      using θ[THEN "∀E"(1),OF "prop-prop2:2", THEN "≡E"(2), OF "∨I"(2)] by blast
1104  next
1105    fix s p
1106    AOT_assume 0: s'  s & s''  s
1107    AOT_assume s3  p
1108    AOT_hence s3x p]
1109      by (metis "&E"(2) "prop-enc" "dfE" "true-in-s")
1110    AOT_hence s'x p]  s''x p]
1111      using θ[THEN "∀E"(1),OF "prop-prop2:2", THEN "≡E"(1)] by blast
1112    moreover {
1113      AOT_assume s'x p]
1114      AOT_hence s'  p
1115        by (safe intro!: "prop-enc"[THEN "dfI"] "true-in-s"[THEN "dfI"] "&I"
1116                         Situation.ψ "cqt:2[const_var]"[axiom_inst])
1117      moreover AOT_have s'  p  s  p
1118        using "sit-part-whole"[THEN "dfE", THEN "&E"(2)] 0[THEN "&E"(1)]
1119              "∀E"(2) by blast
1120      ultimately AOT_have s  p
1121        using "→E" by blast
1122      AOT_hence sx p]
1123        using "true-in-s"[THEN "dfE"] "prop-enc"[THEN "dfE"] "&E" by blast
1124    }
1125    moreover {
1126      AOT_assume s''x p]
1127      AOT_hence s''  p
1128        by (safe intro!: "prop-enc"[THEN "dfI"] "true-in-s"[THEN "dfI"] "&I"
1129                         Situation.ψ "cqt:2[const_var]"[axiom_inst])
1130      moreover AOT_have s''  p  s  p
1131        using "sit-part-whole"[THEN "dfE", THEN "&E"(2)] 0[THEN "&E"(2)]
1132              "∀E"(2) by blast
1133      ultimately AOT_have s  p
1134        using "→E" by blast
1135      AOT_hence sx p]
1136        using "true-in-s"[THEN "dfE"] "prop-enc"[THEN "dfE"] "&E" by blast
1137    }
1138    ultimately AOT_show sx p]
1139      by (metis "∨E"(1) "→I")
1140  qed
1141  thus ?thesis
1142    using "Situation.∃I" by fast
1143qed
1144
1145AOT_theorem "act-sit:1": Actual(s)  (s  p  y p]s)
1146proof (safe intro!: "→I")
1147  AOT_assume Actual(s)
1148  AOT_hence p if s  p
1149    using actual[THEN "dfE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"] that by blast
1150  moreover AOT_assume s  p
1151  ultimately AOT_have p by blast
1152  AOT_thus y p]s
1153    by (safe intro!: "β←C"(1) "cqt:2")
1154qed
1155
1156AOT_theorem "act-sit:2":
1157  (Actual(s') & Actual(s''))  x (Actual(x) & s'  x & s''  x)
1158proof(rule "→I"; frule "&E"(1); drule "&E"(2))
1159  AOT_assume act_s': Actual(s')
1160  AOT_assume act_s'': Actual(s'')
1161  have "cond-prop": ConditionOnPropositionalProperties
1162                     (λ Π . «p (Π = y p] & (s'  p  s''  p))»)
1163  proof (safe intro!: "cond-prop[I]"  "∀I" "→I" "prop-prop1"[THEN "dfI"])
1164    AOT_modally_strict {
1165      fix β
1166      AOT_assume p (β = y p] & (s'  p  s''  p))
1167      then AOT_obtain p where β = y p] using "∃E"[rotated] "&E" by blast
1168      AOT_thus p β = y p] by (rule "∃I")
1169    }
1170  qed
1171  have rigid: rigid_condition (λ Π . «p (Π = y p] & (s'  p  s''  p))»)
1172  proof(safe intro!: "strict-can:1[I]" "→I" GEN)
1173    AOT_modally_strict {
1174      fix F
1175      AOT_assume p (F = y p] & (s'  p  s''  p))
1176      then AOT_obtain p1 where p1_prop: F = y p1] & (s'  p1  s''  p1)
1177        using "∃E"[rotated] by blast
1178      AOT_hence (F = y p1])
1179        using "&E"(1) "id-nec:2" "vdash-properties:10" by blast
1180      moreover AOT_have (s'  p1  s''  p1)
1181      proof(rule "∨E"; (rule "→I"; rule "KBasic:15"[THEN "→E"])?)
1182        AOT_show s'  p1  s''  p1 using p1_prop "&E" by blast
1183      next
1184        AOT_show s'  p1  s''  p1 if s'  p1
1185          apply (rule "∨I"(1))
1186          using "dfE" "&E"(1) "≡E"(1) "lem2:1" that "true-in-s" by blast
1187      next
1188        AOT_show s'  p1  s''  p1 if s''  p1
1189          apply (rule "∨I"(2))
1190          using "dfE" "&E"(1) "≡E"(1) "lem2:1" that "true-in-s" by blast
1191      qed
1192      ultimately AOT_have (F = y p1] & (s'  p1  s''  p1))
1193        by (metis "KBasic:3" "&I" "≡E"(2))
1194      AOT_hence p (F = y p] & (s'  p  s''  p)) by (rule "∃I")
1195      AOT_thus p (F = y p] & (s'  p  s''  p))
1196        using Buridan[THEN "→E"] by fast
1197    }
1198  qed
1199
1200  AOT_have desc_den: ιs(F (s[F]  p (F = y p] & (s'  p  s''  p))))
1201    by (rule "can-sit-desc:1"[OF "cond-prop"])
1202  AOT_obtain x0
1203    where x0_prop1: x0 = ιs(F (s[F]  p (F = y p] & (s'  p  s''  p))))
1204    by (metis (no_types, lifting) "∃E" "rule=I:1" desc_den "∃I"(1) id_sym)
1205  AOT_hence x0_sit: Situation(x0)
1206    using "actual-desc:3"[THEN "→E"] "Act-Basic:2" "&E"(1) "≡E"(1)
1207          "possit-sit:4" by blast
1208
1209  AOT_have 1: F (x0[F]  p (F = y p] & (s'  p  s''  p)))
1210    using "strict-sit"[OF rigid, OF "cond-prop", THEN "→E", OF x0_prop1].
1211  AOT_have 2: (x0  p)  (s'  p  s''  p) for p
1212  proof (rule "≡I"; rule "→I")
1213    AOT_assume x0  p
1214    AOT_hence x0y p] using lem1[THEN "→E", OF x0_sit, THEN "≡E"(1)] by blast
1215    then AOT_obtain q where y p] = y q] & (s'  q  s''  q)
1216      using 1[THEN "∀E"(1)[where τ="«y p]»"], OF "prop-prop2:2", THEN "≡E"(1)]
1217            "∃E"[rotated] by blast
1218    AOT_thus s'  p  s''  p
1219      by (metis "rule=E" "&E"(1) "&E"(2) "∨I"(1) "∨I"(2)
1220                "∨E"(1) "deduction-theorem" id_sym "≡E"(2) "p-identity-thm2:3")
1221  next
1222    AOT_assume s'  p  s''  p
1223    AOT_hence y p] = y p] & (s'  p  s''  p)
1224      by (metis "rule=I:1" "&I" "prop-prop2:2") 
1225    AOT_hence q (y p] = y q] & (s'  q  s''  q))
1226      by (rule "∃I")
1227    AOT_hence x0y p]
1228      using 1[THEN "∀E"(1), OF "prop-prop2:2", THEN "≡E"(2)] by blast
1229    AOT_thus x0  p
1230      by (metis "dfI" "&I" "ex:1:a" "prop-enc" "rule-ui:2[const_var]"
1231                x0_sit "true-in-s")
1232  qed
1233
1234  AOT_have Actual(x0) & s'  x0 & s''  x0
1235  proof(safe intro!: "→I" "&I" "∃I"(1) actual[THEN "dfI"] x0_sit GEN
1236                     "sit-part-whole"[THEN "dfI"])
1237    fix p
1238    AOT_assume x0  p
1239    AOT_hence s'  p  s''  p
1240      using 2 "≡E"(1) by metis
1241    AOT_thus p
1242      using act_s' act_s''
1243            actual[THEN "dfE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"]
1244      by (metis "∨E"(3) "reductio-aa:1")
1245  next
1246    AOT_show x0  p if s'  p for p
1247      using 2[THEN "≡E"(2), OF "∨I"(1), OF that].
1248  next
1249    AOT_show x0  p if s''  p for p
1250      using 2[THEN "≡E"(2), OF "∨I"(2), OF that].
1251  next
1252    AOT_show Situation(s')
1253      using act_s'[THEN actual[THEN "dfE"]] "&E" by blast
1254  next
1255    AOT_show Situation(s'')
1256      using act_s''[THEN actual[THEN "dfE"]] "&E" by blast
1257  qed
1258  AOT_thus x (Actual(x) & s'  x & s''  x)
1259    by (rule "∃I")
1260qed
1261
1262AOT_define Consistent :: τ  φ (Consistent'(_'))
1263  cons: Consistent(s) df ¬p (s  p & s  ¬p)
1264
1265AOT_theorem "sit-cons": Actual(s)  Consistent(s)
1266proof(safe intro!: "→I" cons[THEN "dfI"] "&I" Situation.ψ
1267            dest!: actual[THEN "dfE"]; frule "&E"(1); drule "&E"(2))
1268  AOT_assume 0: p (s  p