Theory AOT_PossibleWorlds

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