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)
323
324AOT_theorem "part:1": s  s
325  by (rule "sit-part-whole"[THEN "dfI"])
326     (safe intro!: "&I" Situation.ψ GEN "→I")
327
328AOT_theorem "part:2": s  s' & s  s'  ¬(s'  s)
329proof(rule "→I"; frule "&E"(1); drule "&E"(2); rule "raa-cor:2")
330  AOT_assume 0: s  s'
331  AOT_hence a: s  p  s'  p for p
332    using "∀E"(2) "sit-part-whole"[THEN "dfE"] "&E" by blast
333  AOT_assume s'  s
334  AOT_hence b: s'  p  s  p for p
335    using "∀E"(2) "sit-part-whole"[THEN "dfE"] "&E" by blast
336  AOT_have p (s  p  s'  p)
337    using a b by (simp add: "≡I" "universal-cor")
338  AOT_hence 1: s = s'
339    using "sit-identity"[THEN "≡E"(2)] by metis
340  AOT_assume s  s'
341  AOT_hence ¬(s = s')
342    by (metis "dfE" "=-infix")
343  AOT_thus s = s' & ¬(s = s')
344    using 1 "&I" by blast
345qed
346
347AOT_theorem "part:3": s  s' & s'  s''  s  s''
348proof(rule "→I"; frule "&E"(1); drule "&E"(2);
349      safe intro!: "&I" GEN "→I" "sit-part-whole"[THEN "dfI"] Situation.ψ)
350  fix p
351  AOT_assume s  p
352  moreover AOT_assume s  s'
353  ultimately AOT_have s'  p
354    using "sit-part-whole"[THEN "dfE", THEN "&E"(2),
355                           THEN "∀E"(2)[where β=p], THEN "→E"] by blast
356  moreover AOT_assume s'  s''
357  ultimately AOT_show s''  p
358    using "sit-part-whole"[THEN "dfE", THEN "&E"(2),
359                           THEN "∀E"(2)[where β=p], THEN "→E"] by blast
360qed
361
362AOT_theorem "sit-identity2:1": s = s'  s  s' & s'  s
363proof (safe intro!: "≡I" "&I" "→I")
364  AOT_show s  s' if s = s'
365    using "rule=E" "part:1" that by blast
366next
367  AOT_show s'  s if s = s'
368    using "rule=E" "part:1" that[symmetric] by blast
369next
370  AOT_assume s  s' & s'  s
371  AOT_thus s = s' using "part:2"[THEN "→E", OF "&I"]
372    by (metis "dfI" "&E"(1) "&E"(2) "=-infix" "raa-cor:3")
373qed
374
375AOT_theorem "sit-identity2:2": s = s'  s'' (s''  s  s''  s')
376proof(safe intro!: "≡I" "→I" Situation.GEN "sit-identity"[THEN "≡E"(2)]
377                   GEN[where 'a=𝗈])
378  AOT_show s''  s' if s''  s and s = s' for s''
379    using "rule=E" that by blast
380next
381  AOT_show s''  s if s''  s' and s = s' for s''
382    using "rule=E" id_sym that by blast
383next
384  AOT_show s'  p if s  p and s'' (s''  s  s''  s') for p
385    using "sit-part-whole"[THEN "dfE", THEN "&E"(2),
386              OF that(2)[THEN "Situation.∀E", THEN "≡E"(1), OF "part:1"],
387              THEN "∀E"(2), THEN "→E", OF that(1)].
388next
389  AOT_show s  p if s'  p and s'' (s''  s  s''  s') for p
390    using "sit-part-whole"[THEN "dfE", THEN "&E"(2),
391          OF that(2)[THEN "Situation.∀E", THEN "≡E"(2), OF "part:1"],
392          THEN "∀E"(2), THEN "→E", OF that(1)].
393qed
394
395(* TODO: removed in PLM *)
396AOT_define Persistent :: φ  φ (Persistent'(_'))
397  persistent: Persistent(p) df s (s  p  s' (s  s'  s'  p))
398
399AOT_theorem "pers-prop": p Persistent(p)
400  by (safe intro!: GEN[where 'a=𝗈] Situation.GEN persistent[THEN "dfI"] "→I")
401     (simp add: "sit-part-whole"[THEN "dfE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"])
402
403(* TODO: put this at the correct place *)
404AOT_theorem "sit-comp-simp": sp(s  p  φ{p})
405proof -
406  AOT_have x (A!x & F(x[F]  p (φ{p} & F = y p])))
407    using "A-objects" "vdash-properties:1[2]" by force
408  then AOT_obtain c where c_prop: A!c & F(c[F]  p (φ{p} & F = y p]))
409    using "∃E" by meson
410  AOT_have sit_c: Situation(c)
411  proof(safe intro!: "dfI"[OF situations] "&I" GEN "→I")
412    AOT_show A!c
413      using c_prop "&E" by blast
414  next
415    fix F
416    AOT_assume c[F]
417    AOT_hence F_eq: p (φ{p} & F = y p])
418      using "con-dis-i-e:2:b" "intro-elim:3:a" "rule-ui:3" c_prop by blast
419    then AOT_obtain q where q_prop: φ{q} & F = y q]
420      using "∃E" by meson
421    AOT_show Propositional([F])
422    proof(rule "prop-prop1"[THEN "dfI"])
423      AOT_show "p F = y p]"
424        using q_prop[THEN "&E"(2)] "∃I"(1)
425        by (metis "log-prop-prop:2")
426    qed
427  qed
428  moreover AOT_have p(c  p  φ{p})
429  proof(safe intro!: GEN "≡I" "→I")
430    fix p
431    AOT_assume c  p
432    AOT_hence 1: cy p]
433      using "intro-elim:3:a" "vdash-properties:10" calculation lem1 by blast
434    AOT_have q (φ{q} & y p] = y q])
435      by (safe intro!: c_prop[THEN "&E"(2), THEN "∀E"(1)[where τ="«y p]»"], THEN "≡E"(1)] 1 "cqt:2")
436    then AOT_obtain q where 2: φ{q} & y p] = y q]
437      using "∃E" by meson
438    AOT_hence p = q
439      using "con-dis-i-e:2:b" "intro-elim:3:b" "p-identity-thm2:3" by blast
440    AOT_thus φ{p}
441      using 2
442      using "con-dis-i-e:2:a" "rule=E" id_sym by blast
443  next
444    fix p
445    AOT_assume φ{p}
446    moreover AOT_have y p] = y p]
447      by (simp add: "prop-prop2:2" "rule=I:1")
448    ultimately AOT_have φ{p} & y p] = y p] using "&I" by blast
449    AOT_hence q (φ{q} & y p] = y q])
450      using "∃I" by fast
451    AOT_hence cy p]
452      by (safe intro!: c_prop[THEN "&E"(2), THEN "∀E"(1)[where τ="«y p]»"], THEN "≡E"(2)] "cqt:2")
453    AOT_thus c  p
454      by (metis "intro-elim:3:b" "vdash-properties:10" sit_c lem1)
455  qed
456  ultimately AOT_show sp(s  p  φ{p})
457    by (meson "con-dis-i-e:1" "existential:2[const_var]")
458qed
459
460AOT_theorem "sit-comp-simp-unique": ∃!sp(s  p  φ{p})
461proof(safe intro!: "uniqueness:1"[THEN "dfI"])
462  AOT_obtain s where s_prop: p(s  p  φ{p})
463    using "sit-comp-simp" Situation.instantiation[rotated] by meson
464  AOT_show α (Situation(α) & p (α  p  φ{p}) & β (Situation(β) & p (β  p  φ{p})  β = α))
465  proof(safe intro!: "∃I"(2) "&I")
466    AOT_show Situation(s)
467      using "Situation.ψ" by auto
468  next
469    AOT_show p(s  p  φ{p}) using s_prop.
470  next
471    AOT_show β (Situation(β) & p (β  p  φ{p})  β = s)
472    proof(safe intro!: GEN "→I")
473      fix x
474      AOT_assume 1: Situation(x) & p (x  p  φ{p})
475      AOT_show x = s
476      proof (safe intro!: "sit-identity"[unconstrain s, THEN "→E", THEN "≡E"(2)] 1[THEN "&E"(1)] GEN "≡I" "→I")
477        fix p
478        AOT_assume x  p
479        AOT_hence φ{p}
480          using "1" "con-dis-i-e:2:b" "intro-elim:3:a" "log-prop-prop:2" "rule-ui:1" by blast
481        AOT_thus s  p
482          using s_prop  "intro-elim:3:b" "log-prop-prop:2" "rule-ui:1" by blast
483      next
484        fix p
485        AOT_assume s  p
486        AOT_hence φ{p}
487          using "intro-elim:3:a" "log-prop-prop:2" "rule-ui:1" s_prop by blast
488        AOT_thus x  p
489          using "1" "con-dis-i-e:2:b" "intro-elim:3:b" "log-prop-prop:2" "rule-ui:1" by blast
490      qed
491    qed
492  qed
493qed
494
495AOT_define NullSituation :: τ  φ (NullSituation'(_'))
496  "df-null-trivial:1": NullSituation(s) df ¬p s  p
497
498AOT_define TrivialSituation :: τ  φ (TrivialSituation'(_'))
499  "df-null-trivial:2": TrivialSituation(s) df p s  p
500
501AOT_theorem "thm-null-trivial:1": ∃!x NullSituation(x)
502proof (AOT_subst NullSituation(x) A!x & F (x[F]  F  F) for: x)
503  AOT_modally_strict {
504    AOT_show NullSituation(x)  A!x & F (x[F]  F  F) for x
505    proof (safe intro!: "≡I" "→I" "df-null-trivial:1"[THEN "dfI"]
506                dest!: "df-null-trivial:1"[THEN "dfE"])
507      AOT_assume 0: Situation(x) & ¬p x  p
508      AOT_have 1: A!x
509        using 0[THEN "&E"(1), THEN situations[THEN "dfE"], THEN "&E"(1)].
510      AOT_have 2: x[F]  p F = y p] for F
511        using 0[THEN "&E"(1), THEN situations[THEN "dfE"],
512                THEN "&E"(2), THEN "∀E"(2)]
513        by (metis "dfE" "→I" "prop-prop1" "→E")
514      AOT_show A!x & F (x[F]  F  F)
515      proof (safe intro!: "&I" 1 GEN "≡I" "→I")
516        fix F
517        AOT_assume x[F]
518        moreover AOT_obtain p where F = y p]
519          using calculation 2[THEN "→E"] "∃E"[rotated] by blast
520        ultimately AOT_have xy p]
521          by (metis "rule=E")
522        AOT_hence x  p
523          using lem1[THEN "→E", OF 0[THEN "&E"(1)], THEN "≡E"(2)] by blast
524        AOT_hence p (x  p)
525          by (rule "∃I")
526        AOT_thus F  F
527          using 0[THEN "&E"(2)] "raa-cor:1" "&I" by blast
528      next
529        fix F :: <κ> AOT_var
530        AOT_assume F  F
531        AOT_hence ¬(F = F) by (metis "dfE" "=-infix")
532        moreover AOT_have F = F
533          by (simp add: "id-eq:1")
534        ultimately AOT_show x[F] using "&I" "raa-cor:1" by blast
535      qed
536    next
537      AOT_assume 0: A!x & F (x[F]  F  F)
538      AOT_hence x[F]  F  F for F
539        using "∀E" "&E" by blast
540      AOT_hence 1: ¬x[F] for F
541        using "dfE" "id-eq:1" "=-infix" "reductio-aa:1" "≡E"(1) by blast
542      AOT_show Situation(x) & ¬p x  p
543      proof (safe intro!: "&I" situations[THEN "dfI"] 0[THEN "&E"(1)] GEN "→I")
544        AOT_show Propositional([F]) if x[F] for F
545          using that 1 "&I" "raa-cor:1" by fast
546      next
547        AOT_show ¬p x  p
548        proof(rule "raa-cor:2")
549          AOT_assume p x  p
550          then AOT_obtain p where x  p using "∃E"[rotated] by blast
551          AOT_hence xy p]
552            using "dfE" "&E"(1) "≡E"(1) lem1 "modus-tollens:1"
553                  "raa-cor:3" "true-in-s" by fast
554          moreover AOT_have ¬xy p]
555            by (rule 1[unvarify F]) "cqt:2[lambda]"
556          ultimately AOT_show p & ¬p for p using "&I" "raa-cor:1" by blast
557        qed
558      qed
559    qed
560  }
561next
562  AOT_show ∃!x ([A!]x & F (x[F]  F  F))
563    by (simp add: "A-objects!")
564qed
565
566
567AOT_theorem "thm-null-trivial:2": ∃!x TrivialSituation(x)
568proof (AOT_subst TrivialSituation(x) A!x & F (x[F]  p F = y p]) for: x)
569  AOT_modally_strict {
570    AOT_show TrivialSituation(x)  A!x & F (x[F]  p F = y p]) for x
571    proof (safe intro!: "≡I" "→I" "df-null-trivial:2"[THEN "dfI"]
572                 dest!: "df-null-trivial:2"[THEN "dfE"])
573      AOT_assume 0: Situation(x) & p x  p
574      AOT_have 1: A!x
575        using 0[THEN "&E"(1), THEN situations[THEN "dfE"], THEN "&E"(1)].
576      AOT_have 2: x[F]  p F = y p] for F
577        using 0[THEN "&E"(1), THEN situations[THEN "dfE"],
578                THEN "&E"(2), THEN "∀E"(2)]
579        by (metis "dfE" "deduction-theorem" "prop-prop1" "→E")
580      AOT_show A!x & F (x[F]  p F = y p])
581      proof (safe intro!: "&I" 1 GEN "≡I" "→I" 2)
582        fix F
583        AOT_assume p F = y p]
584        then AOT_obtain p where F = y p]
585          using "∃E"[rotated] by blast
586        moreover AOT_have x  p
587          using 0[THEN "&E"(2)] "∀E" by blast
588        ultimately AOT_show x[F]
589          by (metis 0 "rule=E" "&E"(1) id_sym "≡E"(2) lem1
590                    "Commutativity of ≡" "→E")
591      qed
592    next
593      AOT_assume 0: A!x & F (x[F]  p F = y p])
594      AOT_hence 1: x[F]  p F = y p] for F
595        using "∀E" "&E" by blast
596      AOT_have 2: Situation(x)
597      proof (safe intro!: "&I" situations[THEN "dfI"] 0[THEN "&E"(1)] GEN "→I")
598        AOT_show Propositional([F]) if x[F] for F
599          using 1[THEN "≡E"(1), OF that]
600          by (metis "dfI" "prop-prop1")
601      qed
602      AOT_show Situation(x) & p (x  p)
603      proof (safe intro!: "&I" 2 0[THEN "&E"(1)] GEN "→I")
604        AOT_have xy p]  q y p] = y q] for p
605          by (rule 1[unvarify F, where τ="«y p]»"]) "cqt:2[lambda]"
606        moreover AOT_have q y p] = y q] for p
607          by (rule "∃I"(2)[where β=p])
608             (simp add: "rule=I:1" "prop-prop2:2")
609        ultimately AOT_have xy p] for p by (metis "≡E"(2))
610        AOT_thus x  p for p
611          by (metis "2" "≡E"(2) lem1 "→E")
612      qed
613    qed
614  }
615next
616  AOT_show ∃!x ([A!]x & F (x[F]  p F = y p]))
617    by (simp add: "A-objects!")
618qed
619
620AOT_theorem "thm-null-trivial:3": ιx NullSituation(x)
621  by (meson "A-Exists:2" "RA[2]" "≡E"(2) "thm-null-trivial:1")
622
623AOT_theorem "thm-null-trivial:4": ιx TrivialSituation(x)
624  using "A-Exists:2" "RA[2]" "≡E"(2) "thm-null-trivial:2" by blast
625
626AOT_define TheNullSituation :: κs (s)
627  "df-the-null-sit:1": s =df ιx NullSituation(x)
628
629AOT_define TheTrivialSituation :: κs (sV)
630  "df-the-null-sit:2": sV =df ιx TrivialSituation(x)
631
632AOT_theorem "null-triv-sc:1": NullSituation(x)  NullSituation(x)
633proof(safe intro!: "→I" dest!: "df-null-trivial:1"[THEN "dfE"];
634      frule "&E"(1); drule "&E"(2))
635  AOT_assume 1: ¬p (x  p)
636  AOT_assume 0: Situation(x)
637  AOT_hence Situation(x) by (metis "≡E"(1) "possit-sit:1")
638  moreover AOT_have ¬p (x  p)
639  proof(rule "raa-cor:1")
640    AOT_assume ¬¬p (x  p)
641    AOT_hence p (x  p)
642      by (metis "dfI" "conventions:5")
643    AOT_hence p (x  p) by (metis "BF◇" "→E")
644    then AOT_obtain p where (x  p) using "∃E"[rotated] by blast
645    AOT_hence x  p
646      by (metis "≡E"(1) "lem2:2"[unconstrain s, THEN "→E", OF 0])
647    AOT_hence p x  p using "∃I" by fast
648    AOT_thus p x  p & ¬p x  p using 1 "&I" by blast
649  qed
650  ultimately AOT_have 2: (Situation(x) & ¬p x  p)
651    by (metis "KBasic:3" "&I" "≡E"(2))
652  AOT_show NullSituation(x)
653    by (AOT_subst NullSituation(x) Situation(x) & ¬p x  p)
654       (auto simp: "df-null-trivial:1" "≡Df" 2)
655qed
656
657
658AOT_theorem "null-triv-sc:2": TrivialSituation(x)  TrivialSituation(x)
659proof(safe intro!: "→I" dest!: "df-null-trivial:2"[THEN "dfE"];
660      frule "&E"(1); drule "&E"(2))
661  AOT_assume 0: Situation(x)
662  AOT_hence 1: Situation(x) by (metis "≡E"(1) "possit-sit:1")
663  AOT_assume p x  p
664  AOT_hence x  p for p
665    using "∀E" by blast
666  AOT_hence x  p for p
667    using  0 "≡E"(1) "lem2:1"[unconstrain s, THEN "→E"] by blast
668  AOT_hence p x  p
669    by (rule GEN)
670  AOT_hence p x  p
671    by (rule BF[THEN "→E"])
672  AOT_hence 2: (Situation(x) & p x  p)
673    using 1 by (metis "KBasic:3" "&I" "≡E"(2))
674  AOT_show TrivialSituation(x)
675    by (AOT_subst TrivialSituation(x) Situation(x) & p x  p)
676       (auto simp: "df-null-trivial:2" "≡Df" 2)
677qed
678
679AOT_theorem "null-triv-sc:3": NullSituation(s)
680  by (safe intro!: "df-the-null-sit:1"[THEN "=dfI"(2)] "thm-null-trivial:3"
681       "rule=I:1"[OF "thm-null-trivial:3"]
682       "!box-desc:2"[THEN "→E", THEN "→E", rotated, OF "thm-null-trivial:1",
683                     OF "∀I", OF "null-triv-sc:1", THEN "∀E"(1), THEN "→E"])
684
685AOT_theorem "null-triv-sc:4": TrivialSituation(sV)
686  by (safe intro!: "df-the-null-sit:2"[THEN "=dfI"(2)] "thm-null-trivial:4"
687       "rule=I:1"[OF "thm-null-trivial:4"]
688       "!box-desc:2"[THEN "→E", THEN "→E", rotated, OF "thm-null-trivial:2",
689                     OF "∀I", OF "null-triv-sc:2", THEN "∀E"(1), THEN "→E"])
690
691AOT_theorem "null-triv-facts:1": NullSituation(x)  Null(x)
692proof (safe intro!: "≡I" "→I" "df-null-uni:1"[THEN "dfI"]
693                    "df-null-trivial:1"[THEN "dfI"]
694            dest!: "df-null-uni:1"[THEN "dfE"] "df-null-trivial:1"[THEN "dfE"])
695  AOT_assume 0: Situation(x) & ¬p x  p
696  AOT_have 1: x[F]  p F = y p] for F
697    using 0[THEN "&E"(1), THEN situations[THEN "dfE"], THEN "&E"(2), THEN "∀E"(2)]
698    by (metis "dfE" "deduction-theorem" "prop-prop1" "→E")
699  AOT_show A!x & ¬F x[F]
700  proof (safe intro!: "&I" 0[THEN "&E"(1), THEN situations[THEN "dfE"],
701                             THEN "&E"(1)];
702         rule "raa-cor:2")
703    AOT_assume F x[F]
704    then AOT_obtain F where F_prop: x[F]
705      using "∃E"[rotated] by blast
706    AOT_hence p F = y p]
707      using 1[THEN "→E"] by blast
708    then AOT_obtain p where F = y p]
709      using "∃E"[rotated] by blast
710    AOT_hence xy p]
711      by (metis "rule=E" F_prop)
712    AOT_hence x  p
713      using lem1[THEN "→E", OF 0[THEN "&E"(1)], THEN "≡E"(2)] by blast
714    AOT_hence p x  p
715      by (rule "∃I")
716    AOT_thus p x  p & ¬p x  p
717      using 0[THEN "&E"(2)] "&I" by blast
718  qed
719next
720  AOT_assume 0: A!x & ¬F x[F]
721  AOT_have Situation(x)
722    apply (rule situations[THEN "dfI", OF "&I", OF 0[THEN "&E"(1)]]; rule GEN)
723    using 0[THEN "&E"(2)] by (metis "→I" "existential:2[const_var]" "raa-cor:3") 
724  moreover AOT_have ¬p x  p
725  proof (rule "raa-cor:2")
726    AOT_assume p x  p
727    then AOT_obtain p where x  p by (metis "instantiation")
728    AOT_hence xy p] by (metis "dfE" "&E"(2) "prop-enc" "true-in-s")
729    AOT_hence F x[F] by (rule "∃I") "cqt:2[lambda]"
730    AOT_thus F x[F] & ¬F x[F] using 0[THEN "&E"(2)] "&I" by blast
731  qed
732  ultimately AOT_show Situation(x) & ¬p x  p using "&I" by blast
733qed
734
735AOT_theorem "null-triv-facts:2": s = a
736  apply (rule "=dfI"(2)[OF "df-the-null-sit:1"])
737   apply (fact "thm-null-trivial:3")
738  apply (rule "=dfI"(2)[OF "df-null-uni-terms:1"])
739   apply (fact "null-uni-uniq:3")
740  apply (rule "equiv-desc-eq:3"[THEN "→E"])
741  apply (rule "&I")
742   apply (fact "thm-null-trivial:3")
743  by (rule RN; rule GEN; rule "null-triv-facts:1")
744
745AOT_theorem "null-triv-facts:3": sV  aV
746proof(rule "=-infix"[THEN "dfI"])
747  AOT_have Universal(aV)
748    by (simp add: "null-uni-facts:4")
749  AOT_hence 0: aV[A!]
750    using "df-null-uni:2"[THEN "dfE"] "&E" "∀E"(1)
751    by (metis "cqt:5:a" "vdash-properties:10" "vdash-properties:1[2]")
752  moreover AOT_have 1: ¬sV[A!]
753  proof(rule "raa-cor:2")
754    AOT_have Situation(sV)
755      using "dfE" "&E"(1) "df-null-trivial:2" "null-triv-sc:4" by blast
756    AOT_hence F (sV[F]  Propositional([F]))
757      by (metis "dfE" "&E"(2) situations)
758    moreover AOT_assume sV[A!]
759    ultimately AOT_have Propositional(A!)
760      using "∀E"(1)[rotated, OF "oa-exist:2"] "→E" by blast
761    AOT_thus Propositional(A!) & ¬Propositional(A!)
762      using "prop-in-f:4:d" "&I" by blast
763  qed
764  AOT_show ¬(sV = aV)
765  proof (rule "raa-cor:2")
766    AOT_assume sV = aV
767    AOT_hence sV[A!] using 0 "rule=E" id_sym by fast
768    AOT_thus sV[A!] & ¬sV[A!] using 1 "&I" by blast
769  qed
770qed
771
772definition ConditionOnPropositionalProperties :: (<κ>  𝗈)  bool where
773  "cond-prop": ConditionOnPropositionalProperties  λ φ .  v .
774                        [v  F (φ{F}  Propositional([F]))]
775
776syntax ConditionOnPropositionalProperties :: id_position  AOT_prop
777  ("CONDITION'_ON'_PROPOSITIONAL'_PROPERTIES'(_')")
778
779AOT_theorem "cond-prop[E]":
780  assumes CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)
781  shows F (φ{F}  Propositional([F]))
782  using assms[unfolded "cond-prop"] by auto
783
784AOT_theorem "cond-prop[I]":
785  assumes  F (φ{F}  Propositional([F]))
786  shows CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)
787  using assms "cond-prop" by metis
788
789AOT_theorem "pre-comp-sit":
790  assumes CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)
791  shows (Situation(x) & F (x[F]  φ{F}))  (A!x & F (x[F]  φ{F}))
792proof(rule "≡I"; rule "→I")
793  AOT_assume Situation(x) & F (x[F]  φ{F})
794  AOT_thus A!x & F (x[F]  φ{F})
795    using "&E" situations[THEN "dfE"] "&I" by blast
796next
797  AOT_assume 0: A!x & F (x[F]  φ{F})
798  AOT_show Situation(x) & F (x[F]  φ{F})
799  proof (safe intro!: situations[THEN "dfI"] "&I")
800    AOT_show A!x using 0[THEN "&E"(1)].
801  next
802    AOT_show F (x[F]  Propositional([F]))
803    proof(rule GEN; rule "→I")
804      fix F
805      AOT_assume x[F]
806      AOT_hence φ{F}
807        using 0[THEN "&E"(2)] "∀E" "≡E" by blast
808      AOT_thus Propositional([F])
809        using "cond-prop[E]"[OF assms] "∀E" "→E" by blast
810    qed
811  next
812    AOT_show F (x[F]  φ{F}) using 0 "&E" by blast
813  qed
814qed
815
816AOT_theorem "comp-sit:1":
817  assumes CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)
818  shows s F(s[F]  φ{F})
819  by (AOT_subst Situation(x) & F(x[F]  φ{F}) A!x & F (x[F]  φ{F}) for: x)
820     (auto simp: "pre-comp-sit"[OF assms] "A-objects"[where φ=φ, axiom_inst])
821
822AOT_theorem "comp-sit:2":
823  assumes CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)
824  shows ∃!s F(s[F]  φ{F})
825  by (AOT_subst Situation(x) & F(x[F]  φ{F}) A!x & F (x[F]  φ{F}) for: x)
826     (auto simp: assms "pre-comp-sit"  "pre-comp-sit"[OF assms] "A-objects!")
827
828AOT_theorem "can-sit-desc:1":
829  assumes CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)
830  shows ιs(F (s[F]  φ{F}))
831  using "comp-sit:2"[OF assms] "A-Exists:2" "RA[2]" "≡E"(2) by blast
832
833AOT_theorem "can-sit-desc:2":
834  assumes CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)
835  shows ιs(F (s[F]  φ{F})) = ιx(A!x & F (x[F]  φ{F}))
836  by (auto intro!: "equiv-desc-eq:2"[THEN "→E", OF "&I",
837                                     OF "can-sit-desc:1"[OF assms]]
838                   "RA[2]" GEN "pre-comp-sit"[OF assms])
839
840AOT_theorem "strict-sit":
841  assumes RIGID_CONDITION(φ)
842      and CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)
843    shows y = ιs(F (s[F]  φ{F}))  F (y[F]  φ{F})
844  using "rule=E"[rotated, OF "can-sit-desc:2"[OF assms(2), symmetric]]
845        "box-phi-a:2"[OF assms(1)] "→E" "→I" "&E" by fast
846
847(* TODO: exercise (479) sit-lit *)
848
849AOT_define actual :: τ  φ (Actual'(_'))
850  Actual(s) df p (s  p  p)
851
852AOT_theorem "act-and-not-pos": s (Actual(s) & ¬Actual(s))
853proof -
854  AOT_obtain q1 where q1_prop: q1 & ¬q1
855    by (metis "dfE" "instantiation" "cont-tf:1" "cont-tf-thm:1")
856  AOT_have s (F (s[F]  F = y q1]))
857  proof (safe intro!: "comp-sit:1" "cond-prop[I]" GEN "→I")
858    AOT_modally_strict {
859      AOT_show Propositional([F]) if F = y q1] for F
860        using "dfI" "existential:2[const_var]" "prop-prop1" that by fastforce
861    }
862  qed
863  then AOT_obtain s1 where s_prop: F (s1[F]  F = y q1])
864    using "Situation.∃E"[rotated] by meson
865  AOT_have Actual(s1)
866  proof(safe intro!: actual[THEN "dfI"] "&I" GEN "→I" s_prop Situation.ψ)
867    fix p
868    AOT_assume s1  p
869    AOT_hence s1y p]
870      by (metis "dfE" "&E"(2) "prop-enc" "true-in-s")
871    AOT_hence y p] = y q1]
872      by (rule s_prop[THEN "∀E"(1), THEN "≡E"(1), rotated]) "cqt:2[lambda]"
873    AOT_hence p = q1 by (metis "≡E"(2) "p-identity-thm2:3")
874    AOT_thus p using q1_prop[THEN "&E"(1)] "rule=E" id_sym by fast
875  qed
876  moreover AOT_have ¬Actual(s1)
877  proof(rule "raa-cor:1"; drule "KBasic:12"[THEN "≡E"(2)])
878    AOT_assume Actual(s1)
879    AOT_hence (Situation(s1) & p (s1  p  p))
880      using actual[THEN "≡Df", THEN "conventions:3"[THEN "dfE"],
881                   THEN "&E"(1), THEN RM, THEN "→E"] by blast
882    AOT_hence p (s1  p  p)
883      by (metis "RM:1" "Conjunction Simplification"(2) "→E")
884    AOT_hence p (s1  p  p)
885      by (metis "CBF" "vdash-properties:10")
886    AOT_hence (s1  q1  q1)
887      using "∀E" by blast
888    AOT_hence s1  q1  q1
889      by (metis "→E" "qml:1" "vdash-properties:1[2]")
890    moreover AOT_have s1  q1
891      using s_prop[THEN "∀E"(1), THEN "≡E"(2),
892                   THEN lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(2)]]
893            "rule=I:1" "prop-prop2:2" by blast
894    ultimately AOT_have q1
895      using "dfE" "&E"(1) "≡E"(1) "lem2:1" "true-in-s" "→E" by fast
896    AOT_thus ¬q1 & ¬¬q1
897      using "KBasic:12"[THEN "≡E"(1)] q1_prop[THEN "&E"(2)] "&I" by blast
898  qed
899  ultimately AOT_have (Actual(s1) & ¬Actual(s1))
900    using s_prop "&I" by blast
901  thus ?thesis
902    by (rule "Situation.∃I")
903qed
904
905AOT_theorem "actual-s:1": s Actual(s)
906proof -
907  AOT_obtain s where (Actual(s) & ¬Actual(s))
908    using "act-and-not-pos" "Situation.∃E"[rotated] by meson
909  AOT_hence Actual(s) using "&E" "&I" by metis
910  thus ?thesis by (rule "Situation.∃I")
911qed
912
913AOT_theorem "actual-s:2": s ¬Actual(s)
914proof(rule "∃I"(1)[where τ=«sV»]; (rule "&I")?)
915  AOT_show Situation(sV)
916    using "dfE" "&E"(1) "df-null-trivial:2" "null-triv-sc:4" by blast
917next
918  AOT_show ¬Actual(sV)
919  proof(rule "raa-cor:2")
920    AOT_assume 0: Actual(sV)
921    AOT_obtain p1 where notp1: ¬p1
922      by (metis "∃E" "∃I"(1) "log-prop-prop:2" "non-contradiction")
923    AOT_have sV  p1
924      using "null-triv-sc:4"[THEN "dfE"[OF "df-null-trivial:2"], THEN "&E"(2)]
925            "∀E" by blast
926    AOT_hence p1
927      using 0[THEN actual[THEN "dfE"], THEN "&E"(2), THEN "∀E"(2), THEN "→E"]
928      by blast
929    AOT_thus p & ¬p for p using notp1 by (metis "raa-cor:3")
930  qed
931next
932  AOT_show sV
933    using "df-the-null-sit:2" "rule-id-df:2:b[zero]" "thm-null-trivial:4" by blast
934qed
935
936AOT_theorem "actual-s:3": ps(Actual(s)  ¬s  p)
937proof -
938  AOT_obtain p1 where notp1: ¬p1
939    by (metis "∃E" "∃I"(1) "log-prop-prop:2" "non-contradiction")
940  AOT_have s (Actual(s)  ¬(s  p1))
941  proof (rule Situation.GEN; rule "→I"; rule "raa-cor:2")
942    fix s
943    AOT_assume Actual(s)
944    moreover AOT_assume s  p1
945    ultimately AOT_have p1
946      using actual[THEN "dfE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"] by blast
947    AOT_thus p1 & ¬p1
948      using notp1 "&I" by simp
949  qed
950  thus ?thesis by (rule "∃I")
951qed
952
953AOT_theorem comp:
954  s (s'  s & s''  s & s''' (s'  s''' & s''  s'''  s  s'''))
955proof -
956  have cond_prop: ConditionOnPropositionalProperties (λ Π . «s'[Π]  s''[Π]»)
957  proof(safe intro!: "cond-prop[I]" GEN "oth-class-taut:8:c"[THEN "→E", THEN "→E"];
958        rule "→I")
959    AOT_modally_strict {
960      fix F
961      AOT_have Situation(s')
962        by (simp add: Situation.restricted_var_condition)
963      AOT_hence s'[F]  Propositional([F])
964        using "situations"[THEN "dfE", THEN "&E"(2), THEN "∀E"(2)] by blast
965      moreover AOT_assume s'[F]
966      ultimately AOT_show Propositional([F])
967        using "→E" by blast
968    }
969  next
970    AOT_modally_strict {
971      fix F
972      AOT_have Situation(s'')
973        by (simp add: Situation.restricted_var_condition)
974      AOT_hence s''[F]  Propositional([F])
975        using "situations"[THEN "dfE", THEN "&E"(2), THEN "∀E"(2)] by blast
976      moreover AOT_assume s''[F]
977      ultimately AOT_show Propositional([F])
978        using "→E" by blast
979    }
980  qed
981  AOT_obtain s3 where θ: F (s3[F]  s'[F]  s''[F])
982    using "comp-sit:1"[OF cond_prop] "Situation.∃E"[rotated] by meson
983  AOT_have s'  s3 & s''  s3 & s''' (s'  s''' & s''  s'''  s3  s''')
984  proof(safe intro!: "&I" "dfI"[OF "true-in-s"] "dfI"[OF "prop-enc"]
985                     "Situation.GEN" "GEN"[where 'a=𝗈] "→I"
986                     "sit-part-whole"[THEN "dfI"]
987                     Situation.ψ "cqt:2[const_var]"[axiom_inst])
988    fix p
989    AOT_assume s'  p
990    AOT_hence s'x p]
991      by (metis "&E"(2) "prop-enc" "dfE" "true-in-s")
992    AOT_thus s3x p]
993      using θ[THEN "∀E"(1),OF "prop-prop2:2", THEN "≡E"(2), OF "∨I"(1)] by blast
994  next
995    fix p
996    AOT_assume s''  p
997    AOT_hence s''x p]
998      by (metis "&E"(2) "prop-enc" "dfE" "true-in-s")
999    AOT_thus s3x p]
1000      using θ[THEN "∀E"(1),OF "prop-prop2:2", THEN "≡E"(2), OF "∨I"(2)] by blast
1001  next
1002    fix s p
1003    AOT_assume 0: s'  s & s''  s
1004    AOT_assume s3  p
1005    AOT_hence s3x p]
1006      by (metis "&E"(2) "prop-enc" "dfE" "true-in-s")
1007    AOT_hence s'x p]  s''x p]
1008      using θ[THEN "∀E"(1),OF "prop-prop2:2", THEN "≡E"(1)] by blast
1009    moreover {
1010      AOT_assume s'x p]
1011      AOT_hence s'  p
1012        by (safe intro!: "prop-enc"[THEN "dfI"] "true-in-s"[THEN "dfI"] "&I"
1013                         Situation.ψ "cqt:2[const_var]"[axiom_inst])
1014      moreover AOT_have s'  p  s  p
1015        using "sit-part-whole"[THEN "dfE", THEN "&E"(2)] 0[THEN "&E"(1)]
1016              "∀E"(2) by blast
1017      ultimately AOT_have s  p
1018        using "→E" by blast
1019      AOT_hence sx p]
1020        using "true-in-s"[THEN "dfE"] "prop-enc"[THEN "dfE"] "&E" by blast
1021    }
1022    moreover {
1023      AOT_assume s''x p]
1024      AOT_hence s''  p
1025        by (safe intro!: "prop-enc"[THEN "dfI"] "true-in-s"[THEN "dfI"] "&I"
1026                         Situation.ψ "cqt:2[const_var]"[axiom_inst])
1027      moreover AOT_have s''  p  s  p
1028        using "sit-part-whole"[THEN "dfE", THEN "&E"(2)] 0[THEN "&E"(2)]
1029              "∀E"(2) by blast
1030      ultimately AOT_have s  p
1031        using "→E" by blast
1032      AOT_hence sx p]
1033        using "true-in-s"[THEN "dfE"] "prop-enc"[THEN "dfE"] "&E" by blast
1034    }
1035    ultimately AOT_show sx p]
1036      by (metis "∨E"(1) "→I")
1037  qed
1038  thus ?thesis
1039    using "Situation.∃I" by fast
1040qed
1041
1042AOT_theorem "act-sit:1": Actual(s)  (s  p  y p]s)
1043proof (safe intro!: "→I")
1044  AOT_assume Actual(s)
1045  AOT_hence p if s  p
1046    using actual[THEN "dfE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"] that by blast
1047  moreover AOT_assume s  p
1048  ultimately AOT_have p by blast
1049  AOT_thus y p]s
1050    by (safe intro!: "β←C"(1) "cqt:2")
1051qed
1052
1053AOT_theorem "act-sit:2":
1054  (Actual(s') & Actual(s''))  x (Actual(x) & s'  x & s''  x)
1055proof(rule "→I"; frule "&E"(1); drule "&E"(2))
1056  AOT_assume act_s': Actual(s')
1057  AOT_assume act_s'': Actual(s'')
1058  have "cond-prop": ConditionOnPropositionalProperties
1059                     (λ Π . «p (Π = y p] & (s'  p  s''  p))»)
1060  proof (safe intro!: "cond-prop[I]"  "∀I" "→I" "prop-prop1"[THEN "dfI"])
1061    AOT_modally_strict {
1062      fix β
1063      AOT_assume p (β = y p] & (s'  p  s''  p))
1064      then AOT_obtain p where β = y p] using "∃E"[rotated] "&E" by blast
1065      AOT_thus p β = y p] by (rule "∃I")
1066    }
1067  qed
1068  have rigid: rigid_condition (λ Π . «p (Π = y p] & (s'  p  s''  p))»)
1069  proof(safe intro!: "strict-can:1[I]" "→I" GEN)
1070    AOT_modally_strict {
1071      fix F
1072      AOT_assume p (F = y p] & (s'  p  s''  p))
1073      then AOT_obtain p1 where p1_prop: F = y p1] & (s'  p1  s''  p1)
1074        using "∃E"[rotated] by blast
1075      AOT_hence (F = y p1])
1076        using "&E"(1) "id-nec:2" "vdash-properties:10" by blast
1077      moreover AOT_have (s'  p1  s''  p1)
1078      proof(rule "∨E"; (rule "→I"; rule "KBasic:15"[THEN "→E"])?)
1079        AOT_show s'  p1  s''  p1 using p1_prop "&E" by blast
1080      next
1081        AOT_show s'  p1  s''  p1 if s'  p1
1082          apply (rule "∨I"(1))
1083          using "dfE" "&E"(1) "≡E"(1) "lem2:1" that "true-in-s" by blast
1084      next
1085        AOT_show s'  p1  s''  p1 if s''  p1
1086          apply (rule "∨I"(2))
1087          using "dfE" "&E"(1) "≡E"(1) "lem2:1" that "true-in-s" by blast
1088      qed
1089      ultimately AOT_have (F = y p1] & (s'  p1  s''  p1))
1090        by (metis "KBasic:3" "&I" "≡E"(2))
1091      AOT_hence p (F = y p] & (s'  p  s''  p)) by (rule "∃I")
1092      AOT_thus p (F = y p] & (s'  p  s''  p))
1093        using Buridan[THEN "→E"] by fast
1094    }
1095  qed
1096
1097  AOT_have desc_den: ιs(F (s[F]  p (F = y p] & (s'  p  s''  p))))
1098    by (rule "can-sit-desc:1"[OF "cond-prop"])
1099  AOT_obtain x0
1100    where x0_prop1: x0 = ιs(F (s[F]  p (F = y p] & (s'  p  s''  p))))
1101    by (metis (no_types, lifting) "∃E" "rule=I:1" desc_den "∃I"(1) id_sym)
1102  AOT_hence x0_sit: Situation(x0)
1103    using "actual-desc:3"[THEN "→E"] "Act-Basic:2" "&E"(1) "≡E"(1)
1104          "possit-sit:4" by blast
1105
1106  AOT_have 1: F (x0[F]  p (F = y p] & (s'  p  s''  p)))
1107    using "strict-sit"[OF rigid, OF "cond-prop", THEN "→E", OF x0_prop1].
1108  AOT_have 2: (x0  p)  (s'  p  s''  p) for p
1109  proof (rule "≡I"; rule "→I")
1110    AOT_assume x0  p
1111    AOT_hence x0y p] using lem1[THEN "→E", OF x0_sit, THEN "≡E"(1)] by blast
1112    then AOT_obtain q where y p] = y q] & (s'  q  s''  q)
1113      using 1[THEN "∀E"(1)[where τ="«y p]»"], OF "prop-prop2:2", THEN "≡E"(1)]
1114            "∃E"[rotated] by blast
1115    AOT_thus s'  p  s''  p
1116      by (metis "rule=E" "&E"(1) "&E"(2) "∨I"(1) "∨I"(2)
1117                "∨E"(1) "deduction-theorem" id_sym "≡E"(2) "p-identity-thm2:3")
1118  next
1119    AOT_assume s'  p  s''  p
1120    AOT_hence y p] = y p] & (s'  p  s''  p)
1121      by (metis "rule=I:1" "&I" "prop-prop2:2") 
1122    AOT_hence q (y p] = y q] & (s'  q  s''  q))
1123      by (rule "∃I")
1124    AOT_hence x0y p]
1125      using 1[THEN "∀E"(1), OF "prop-prop2:2", THEN "≡E"(2)] by blast
1126    AOT_thus x0  p
1127      by (metis "dfI" "&I" "ex:1:a" "prop-enc" "rule-ui:2[const_var]"
1128                x0_sit "true-in-s")
1129  qed
1130
1131  AOT_have Actual(x0) & s'  x0 & s''  x0
1132  proof(safe intro!: "→I" "&I" "∃I"(1) actual[THEN "dfI"] x0_sit GEN
1133                     "sit-part-whole"[THEN "dfI"])
1134    fix p
1135    AOT_assume x0  p
1136    AOT_hence s'  p  s''  p
1137      using 2 "≡E"(1) by metis
1138    AOT_thus p
1139      using act_s' act_s''
1140            actual[THEN "dfE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"]
1141      by (metis "∨E"(3) "reductio-aa:1")
1142  next
1143    AOT_show x0  p if s'  p for p
1144      using 2[THEN "≡E"(2), OF "∨I"(1), OF that].
1145  next
1146    AOT_show x0  p if s''  p for p
1147      using 2[THEN "≡E"(2), OF "∨I"(2), OF that].
1148  next
1149    AOT_show Situation(s')
1150      using act_s'[THEN actual[THEN "dfE"]] "&E" by blast
1151  next
1152    AOT_show Situation(s'')
1153      using act_s''[THEN actual[THEN "dfE"]] "&E" by blast
1154  qed
1155  AOT_thus x (Actual(x) & s'  x & s''  x)
1156    by (rule "∃I")
1157qed
1158
1159AOT_define Consistent :: τ  φ (Consistent'(_'))
1160  cons: Consistent(s) df ¬p (s  p & s  ¬p)
1161
1162AOT_theorem "sit-cons": Actual(s)  Consistent(s)
1163proof(safe intro!: "→I" cons[THEN "dfI"] "&I" Situation.ψ
1164            dest!: actual[THEN "dfE"]; frule "&E"(1); drule "&E"(2))
1165  AOT_assume 0: p (s  p  p)
1166  AOT_show ¬p (s  p & s  ¬p)
1167  proof (rule "raa-cor:2")
1168    AOT_assume p (s  p & s  ¬p)
1169    then AOT_obtain p where s  p & s  ¬p
1170      using "∃E"[rotated] by blast
1171    AOT_hence p & ¬p
1172      using 0[THEN "∀E"(1)[where τ=«¬p», THEN "→E"], OF "log-prop-prop:2"]
1173            0[THEN "∀E"(2)[where β=p], THEN "→E"] "&E" "&I" by blast
1174    AOT_thus p & ¬p for p by (metis "raa-cor:1") 
1175  qed
1176qed
1177
1178AOT_theorem "cons-rigid:1": ¬Consistent(s)  ¬Consistent(s)
1179proof (rule "≡I"; rule "→I")
1180  AOT_assume ¬Consistent(s)
1181  AOT_hence p (s  p & s  ¬p)
1182    using cons[THEN "dfI", OF "&I", OF Situation.ψ]
1183    by (metis "raa-cor:3")
1184  then AOT_obtain p where p_prop: s  p & s  ¬p
1185    using "∃E"[rotated] by blast
1186  AOT_hence s  p
1187    using "&E"(1) "≡E"(1) "lem2:1" by blast
1188  moreover AOT_have s  ¬p
1189    using p_prop "T◇" "&E" "≡E"(1)
1190      "modus-tollens:1" "raa-cor:3" "lem2:3"[unvarify p]
1191      "log-prop-prop:2" by metis
1192  ultimately AOT_have (s  p & s  ¬p)
1193    by (metis "KBasic:3" "&I" "≡E"(2))
1194  AOT_hence p (s  p & s  ¬p)
1195    by (rule "∃I")
1196  AOT_hence p(s  p & s  ¬p)
1197    by (metis Buridan "vdash-properties:10") 
1198  AOT_thus ¬Consistent(s)
1199    apply (rule "qml:1"[axiom_inst, THEN "→E", THEN "→E", rotated])
1200    apply (rule RN)
1201    using "dfE" "&E"(2) cons "deduction-theorem" "raa-cor:3" by blast
1202next
1203  AOT_assume ¬Consistent(s)
1204  AOT_thus ¬Consistent(s) using "qml:2"[axiom_inst, THEN "→E"] by auto
1205qed
1206
1207AOT_theorem "cons-rigid:2": Consistent(x)  Consistent(x)
1208proof(rule "≡I"; rule "→I")
1209  AOT_assume 0: Consistent(x)
1210  AOT_have (Situation(x) & ¬p (x  p & x  ¬p))
1211    apply (AOT_subst Situation(x) & ¬p (x  p & x  ¬p) Consistent(x))
1212     using cons "≡E"(2) "Commutativity of ≡" "≡Df" apply blast
1213    by (simp add: 0)
1214  AOT_hence Situation(x) and 1: ¬p (x  p & x  ¬p)
1215    using "RM◇" "Conjunction Simplification"(1) "Conjunction Simplification"(2)
1216          "modus-tollens:1" "raa-cor:3" by blast+
1217  AOT_hence 2: Situation(x) by (metis "≡E"(1) "possit-sit:2")
1218  AOT_have 3: ¬p (x  p & x  ¬p)
1219    using 2 using 1 "KBasic:11" "≡E"(2) by blast
1220  AOT_show Consistent(x)
1221  proof (rule "raa-cor:1")
1222    AOT_assume ¬Consistent(x)
1223    AOT_hence p (x  p & x  ¬p)
1224      using 0 "dfE" "conventions:5" 2 "cons-rigid:1"[unconstrain s, THEN "→E"]
1225            "modus-tollens:1" "raa-cor:3" "≡E"(4) by meson
1226    then AOT_obtain p where x  p and 4: x  ¬p
1227      using "∃E"[rotated] "&E" by blast
1228    AOT_hence x  p
1229      by (metis "2" "≡E"(1) "lem2:1"[unconstrain s, THEN "→E"])
1230    moreover AOT_have x  ¬p
1231      using 4 "lem2:1"[unconstrain s, unvarify p, THEN "→E"]
1232      by (metis 2 "≡E"(1) "log-prop-prop:2")
1233    ultimately AOT_have (x  p & x  ¬p)
1234      by (metis "KBasic:3" "&I" "≡E"(3) "raa-cor:3")
1235    AOT_hence p (x  p & x  ¬p)
1236      by (metis "existential:1" "log-prop-prop:2")
1237    AOT_hence p (x  p & x  ¬p)
1238      by (metis Buridan "vdash-properties:10")
1239    AOT_thus p & ¬p for p
1240      using 3 "&I"  by (metis "raa-cor:3")
1241  qed
1242next
1243  AOT_show Consistent(x) if Consistent(x)
1244    using "T◇" that "vdash-properties:10" by blast
1245qed
1246
1247AOT_define possible :: τ  φ (Possible'(_'))
1248  pos: Possible(s) df Actual(s)
1249
1250AOT_theorem "sit-pos:1": Actual(s)  Possible(s)
1251  apply(rule "→I"; rule pos[THEN "dfI"]; rule "&I")
1252  apply (meson "dfE" actual "&E"(1))
1253  using "T◇" "vdash-properties:10" by blast
1254
1255AOT_theorem "sit-pos:2": p ((s  p) & ¬p)  ¬Possible(s)
1256proof(rule "→I")
1257  AOT_assume p ((s  p) & ¬p)
1258  then AOT_obtain p where a: (s  p) & ¬p
1259    using "∃E"[rotated] by blast
1260  AOT_hence (s  p)
1261    using "&E" by (metis "T◇" "≡E"(1) "lem2:3" "vdash-properties:10")
1262  moreover AOT_have ¬p
1263    using a[THEN "&E"(2)] by (metis "KBasic2:1" "≡E"(2))
1264  ultimately AOT_have (s  p & ¬p)
1265    by (metis "KBasic:3" "&I" "≡E"(3) "raa-cor:3")
1266  AOT_hence p (s  p & ¬p)
1267    by (rule "∃I")
1268  AOT_hence 1: q (s  q & ¬q)
1269    by (metis Buridan "vdash-properties:10")
1270  AOT_have ¬q (s  q  q)
1271    apply (AOT_subst s  q  q ¬(s  q & ¬q) for: q)
1272     apply (simp add: "oth-class-taut:1:a")
1273    apply (AOT_subst ¬q ¬(s  q & ¬q) q (s  q & ¬q))
1274    by (auto simp: "conventions:4" "df-rules-formulas[3]" "df-rules-formulas[4]" "≡I" 1)
1275  AOT_hence 0: ¬q (s  q  q)
1276    by (metis "dfE" "conventions:5" "raa-cor:3")
1277  AOT_show ¬Possible(s)
1278    apply (AOT_subst Possible(s) Situation(s) & Actual(s))
1279     apply (simp add: pos "≡Df")
1280    apply (AOT_subst Actual(s) Situation(s) & q (s  q  q))
1281     using actual "≡Df" apply presburger
1282    by (metis "0" "KBasic2:3" "&E"(2) "raa-cor:3" "vdash-properties:10")
1283qed
1284
1285AOT_theorem "pos-cons-sit:1": Possible(s)  Consistent(s)
1286  by (auto simp: "sit-cons"[THEN "RM◇"