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) ≡⇩_d⇩_f 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!: "≡⇩_d⇩_fI"[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 "≡⇩_d⇩_fI"])
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 "≡⇩_d⇩_fE" "&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 "≡⇩_d⇩_fE"] 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 "≡⇩_d⇩_fE"] by blast
57  AOT_show ‹Situation(x)›
58  proof(rule "situations:1"[THEN "≡⇩_d⇩_fI"]; 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 "≡⇩_d⇩_fI" "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 "≡⇩_d⇩_fE"] 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 "≡⇩_d⇩_fI"] "&I" GEN "→I" "prop-prop1"[THEN "≡⇩_d⇩_fI"])
105  AOT_have ‹∃F ∘p[F]›
106    using "tv-id:2"[THEN "prop-enc"[THEN "≡⇩_d⇩_fE"], 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 "≡⇩_d⇩_fE"],
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 ≡⇩_d⇩_f 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 ≡ x[λy 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 "≡⇩_d⇩_fE"] "&E" by blast
217  AOT_thus ‹x[λy p]› using "prop-enc"[THEN "≡⇩_d⇩_fE"] "&E" by blast
218next
219  AOT_assume 1: ‹Situation(x)›
220  AOT_assume ‹x[λy p]›
221  AOT_hence ‹x❙Σp›
222    using "prop-enc"[THEN "≡⇩_d⇩_fI", OF "&I", OF "cqt:2"(1)] by blast
223  AOT_thus ‹x ⊨ p›
224    using "true-in-s"[THEN "≡⇩_d⇩_fI"] 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 ≡ s[λy p]›
232    using lem1[THEN "→E", OF sit] by blast
233  also AOT_have ‹… ≡ □s[λy 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 "≡⇩_d⇩_fE", 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 "≡⇩_d⇩_fE", 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.ψ "≡⇩_d⇩_fE" "&E"(1) situations by blast
278  next
279    AOT_show ‹A!s'› using Situation.ψ "≡⇩_d⇩_fE" "&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 "≡⇩_d⇩_fE"], THEN "&E"(2),
285                        THEN "∀E"(2)[where β=F], THEN "→E"]
286            "prop-prop1"[THEN "≡⇩_d⇩_fE"] by blast
287    then AOT_obtain p where F_def: ‹F = [λy p]›
288      using "∃E" by metis
289    AOT_hence ‹s[λy 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 "≡⇩_d⇩_fE"], THEN "&E"(2),
304                        THEN "∀E"(2)[where β=F], THEN "→E"]
305            "prop-prop1"[THEN "≡⇩_d⇩_fE"] 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 ‹s[λy 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' ≡⇩_d⇩_f ∀p (s ⊨ p → s' ⊨ p)›
323AOT_theorem "part:1": ‹s ⊴ s›
324  by (rule "sit-part-whole"[THEN "≡⇩_d⇩_fI"])
325     (safe intro!: "&I" Situation.ψ GEN "→I")
326
327AOT_theorem "part:2": ‹s ⊴ s' & s ≠ s' → ¬(s' ⊴ s)›
328proof(rule "→I"; frule "&E"(1); drule "&E"(2); rule "raa-cor:2")
329  AOT_assume 0: ‹s ⊴ s'›
330  AOT_hence a: ‹s ⊨ p → s' ⊨ p› for p
331    using "∀E"(2) "sit-part-whole"[THEN "≡⇩_d⇩_fE"] "&E" by blast
332  AOT_assume ‹s' ⊴ s›
333  AOT_hence b: ‹s' ⊨ p → s ⊨ p› for p
334    using "∀E"(2) "sit-part-whole"[THEN "≡⇩_d⇩_fE"] "&E" by blast
335  AOT_have ‹∀p (s ⊨ p ≡ s' ⊨ p)›
336    using a b by (simp add: "≡I" "universal-cor")
337  AOT_hence 1: ‹s = s'›
338    using "sit-identity"[THEN "≡E"(2)] by metis
339  AOT_assume ‹s ≠ s'›
340  AOT_hence ‹¬(s = s')›
341    by (metis "≡⇩_d⇩_fE" "=-infix")
342  AOT_thus ‹s = s' & ¬(s = s')›
343    using 1 "&I" by blast
344qed
345
346AOT_theorem "part:3": ‹s ⊴ s' & s' ⊴ s'' → s ⊴ s''›
347proof(rule "→I"; frule "&E"(1); drule "&E"(2);
348      safe intro!: "&I" GEN "→I" "sit-part-whole"[THEN "≡⇩_d⇩_fI"] Situation.ψ)
349  fix p
350  AOT_assume ‹s ⊨ p›
351  moreover AOT_assume ‹s ⊴ s'›
352  ultimately AOT_have ‹s' ⊨ p›
353    using "sit-part-whole"[THEN "≡⇩_d⇩_fE", THEN "&E"(2),
354                           THEN "∀E"(2)[where β=p], THEN "→E"] by blast
355  moreover AOT_assume ‹s' ⊴ s''›
356  ultimately AOT_show ‹s'' ⊨ p›
357    using "sit-part-whole"[THEN "≡⇩_d⇩_fE", THEN "&E"(2),
358                           THEN "∀E"(2)[where β=p], THEN "→E"] by blast
359qed
360
361AOT_theorem "sit-identity2:1": ‹s = s' ≡ s ⊴ s' & s' ⊴ s›
362proof (safe intro!: "≡I" "&I" "→I")
363  AOT_show ‹s ⊴ s'› if ‹s = s'›
364    using "rule=E" "part:1" that by blast
365next
366  AOT_show ‹s' ⊴ s› if ‹s = s'›
367    using "rule=E" "part:1" that[symmetric] by blast
368next
369  AOT_assume ‹s ⊴ s' & s' ⊴ s›
370  AOT_thus ‹s = s'› using "part:2"[THEN "→E", OF "&I"]
371    by (metis "≡⇩_d⇩_fI" "&E"(1) "&E"(2) "=-infix" "raa-cor:3")
372qed
373
374AOT_theorem "sit-identity2:2": ‹s = s' ≡ ∀s'' (s'' ⊴ s ≡ s'' ⊴ s')›
375proof(safe intro!: "≡I" "→I" Situation.GEN "sit-identity"[THEN "≡E"(2)]
376                   GEN[where 'a=𝗈])
377  AOT_show ‹s'' ⊴ s'› if ‹s'' ⊴ s› and ‹s = s'› for s''
378    using "rule=E" that by blast
379next
380  AOT_show ‹s'' ⊴ s› if ‹s'' ⊴ s'› and ‹s = s'› for s''
381    using "rule=E" id_sym that by blast
382next
383  AOT_show ‹s' ⊨ p› if ‹s ⊨ p› and ‹∀s'' (s'' ⊴ s ≡ s'' ⊴ s')› for p
384    using "sit-part-whole"[THEN "≡⇩_d⇩_fE", THEN "&E"(2),
385              OF that(2)[THEN "Situation.∀E", THEN "≡E"(1), OF "part:1"],
386              THEN "∀E"(2), THEN "→E", OF that(1)].
387next
388  AOT_show ‹s ⊨ p› if ‹s' ⊨ p› and ‹∀s'' (s'' ⊴ s ≡ s'' ⊴ s')› for p
389    using "sit-part-whole"[THEN "≡⇩_d⇩_fE", THEN "&E"(2),
390          OF that(2)[THEN "Situation.∀E", THEN "≡E"(2), OF "part:1"],
391          THEN "∀E"(2), THEN "→E", OF that(1)].
392qed
393
394(* TODO: removed in PLM *)
395AOT_define Persistent :: ‹φ ⇒ φ› (‹Persistent'(_')›)
396  persistent: ‹Persistent(p) ≡⇩_d⇩_f ∀s (s ⊨ p → ∀s' (s ⊴ s' → s' ⊨ p))›
397
398AOT_theorem "pers-prop": ‹∀p Persistent(p)›
399  by (safe intro!: GEN[where 'a=𝗈] Situation.GEN persistent[THEN "≡⇩_d⇩_fI"] "→I")
400     (simp add: "sit-part-whole"[THEN "≡⇩_d⇩_fE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"])
401
402(* TODO: put this at the correct place *)
403AOT_theorem "sit-comp-simp:1": ‹∃s∀p(s ⊨ p ≡ φ{p})›
404proof -
405  AOT_have ‹∃x (A!x & ∀F(x[F] ≡ ∃p (φ{p} & F = [λy p])))›
406    using "A-objects" "vdash-properties:1[2]" by force
407  then AOT_obtain c where c_prop: ‹A!c & ∀F(c[F] ≡ ∃p (φ{p} & F = [λy p]))›
408    using "∃E" by meson
409  AOT_have sit_c: ‹Situation(c)›
410  proof(safe intro!: "≡⇩_d⇩_fI"[OF situations] "&I" GEN "→I")
411    AOT_show ‹A!c›
412      using c_prop "&E" by blast
413  next
414    fix F
415    AOT_assume ‹c[F]›
416    AOT_hence F_eq: ‹∃p (φ{p} & F = [λy p])›
417      using "con-dis-i-e:2:b" "intro-elim:3:a" "rule-ui:3" c_prop by blast
418    then AOT_obtain q where q_prop: ‹φ{q} & F = [λy q]›
419      using "∃E" by meson
420    AOT_show ‹Propositional([F])›
421    proof(rule "prop-prop1"[THEN "≡⇩_d⇩_fI"])
422      AOT_show "∃p F = [λy p]"
423        using q_prop[THEN "&E"(2)] "∃I"(1)
424        by (metis "log-prop-prop:2")
425    qed
426  qed
427  moreover AOT_have ‹∀p(c ⊨ p ≡ φ{p})›
428  proof(safe intro!: GEN "≡I" "→I")
429    fix p
430    AOT_assume ‹c ⊨ p›
431    AOT_hence 1: ‹c[λy p]›
432      using "intro-elim:3:a" "vdash-properties:10" calculation lem1 by blast
433    AOT_have ‹∃q (φ{q} & [λy p] = [λy q])›
434      by (safe intro!: c_prop[THEN "&E"(2), THEN "∀E"(1)[where τ="«[λy p]»"], THEN "≡E"(1)] 1 "cqt:2")
435    then AOT_obtain q where 2: ‹φ{q} & [λy p] = [λy q]›
436      using "∃E" by meson
437    AOT_hence ‹p = q›
438      using "con-dis-i-e:2:b" "intro-elim:3:b" "p-identity-thm2:3" by blast
439    AOT_thus ‹φ{p}›
440      using 2
441      using "con-dis-i-e:2:a" "rule=E" id_sym by blast
442  next
443    fix p
444    AOT_assume ‹φ{p}›
445    moreover AOT_have ‹[λy p] = [λy p]›
446      by (simp add: "prop-prop2:2" "rule=I:1")
447    ultimately AOT_have ‹φ{p} & [λy p] = [λy p]› using "&I" by blast
448    AOT_hence ‹∃q (φ{q} & [λy p] = [λy q])›
449      using "∃I" by fast
450    AOT_hence ‹c[λy p]›
451      by (safe intro!: c_prop[THEN "&E"(2), THEN "∀E"(1)[where τ="«[λy p]»"], THEN "≡E"(2)] "cqt:2")
452    AOT_thus ‹c ⊨ p›
453      by (metis "intro-elim:3:b" "vdash-properties:10" sit_c lem1)
454  qed
455  ultimately AOT_show ‹∃s∀p(s ⊨ p ≡ φ{p})›
456    by (meson "con-dis-i-e:1" "existential:2[const_var]")
457qed
458
459AOT_theorem "sit-comp-simp:3": ‹❙ιs ∀p(s ⊨ p ≡ φ{p})↓›
460proof (safe intro!: "actual-desc:1"[THEN "≡E"(2)] "uniqueness:2"[THEN "≡E"(2)])
461  AOT_obtain s where s_prop: ‹∀p(s ⊨ p ≡ ❙𝒜φ{p})›
462    using "sit-comp-simp:1" Situation.instantiation[rotated] by meson
463  AOT_have ‹∀y (❙𝒜(Situation(y) & ∀p (y ⊨ p ≡ φ{p})) ≡ y = s)›
464  proof(safe intro!: GEN "≡I" "→I")
465    fix y
466    AOT_assume ‹❙𝒜(Situation(y) & ∀p (y ⊨ p ≡ φ{p}))›
467    AOT_hence ‹❙𝒜Situation(y)› and 2: ‹❙𝒜∀p (y ⊨ p ≡ φ{p})›
468      using "&E" "Act-Basic:2" "≡E"(1) by blast+
469    AOT_hence y_sit: ‹Situation(y)›
470      using "intro-elim:3:a" "possit-sit:4" by blast
471    AOT_have ‹∀p ❙𝒜(y ⊨ p ≡ φ{p})›
472      using 2 "≡E"(1) "logic-actual-nec:3"[axiom_inst] by blast
473    AOT_hence ‹❙𝒜(y ⊨ p ≡ φ{p})› for p using "∀E" by blast
474    AOT_hence 3: ‹❙𝒜y ⊨ p ≡ ❙𝒜φ{p}› for p
475      using "Act-Basic:5" "≡E"(1) by blast
476    AOT_show ‹y = s›
477    proof(safe intro!: "sit-identity"[unconstrain s, THEN "→E", OF y_sit, THEN "≡E"(2)] GEN "≡I" "→I")
478      fix p
479      AOT_assume ‹y ⊨ p›
480      AOT_hence ‹❙𝒜y ⊨ p›
481        using "lem2:4"[unconstrain s, THEN "→E", OF y_sit]
482        using "intro-elim:3:b" by blast
483      AOT_hence ‹❙𝒜φ{p}›
484        using 3 "intro-elim:3:a" by blast
485      AOT_thus ‹s ⊨ p›
486        using s_prop "intro-elim:3:b" "rule-ui:2[const_var]" by blast
487    next
488      fix p
489      AOT_assume ‹s ⊨ p›
490      AOT_hence ‹❙𝒜φ{p}›
491        using "intro-elim:3:a" "rule-ui:3" s_prop by blast
492      AOT_hence ‹❙𝒜y ⊨ p›
493        using "3" "intro-elim:3:b" by blast
494      AOT_thus ‹y ⊨ p›
495        using "lem2:4"[unconstrain s, THEN "→E", OF y_sit]
496        using "intro-elim:3:a" by blast
497    qed
498  next
499    fix y
500    AOT_assume ‹y = s›
501    moreover AOT_have ‹❙𝒜(Situation(s) & ∀p (s ⊨ p ≡ φ{p}))›
502    proof(safe intro!: "act-conj-act:3"[THEN "→E"] "&I" "logic-actual-nec:3"[axiom_inst, THEN "≡E"(2)] GEN)
503      AOT_show ‹❙𝒜Situation(s)›
504        using "≡E"(2) "possit-sit:4" "Situation.ψ" by blast
505    next
506      AOT_show ‹❙𝒜(s ⊨ p ≡ φ{p})› for p
507      proof(safe intro!: "Act-Basic:5"[THEN "≡E"(2)] "≡I" "→I")
508        AOT_assume ‹❙𝒜s ⊨ p›
509        AOT_hence ‹s ⊨ p›
510          using "intro-elim:3:a" "lem2:4" by blast
511        AOT_thus ‹❙𝒜φ{p}›
512          using s_prop "intro-elim:3:a" "rule-ui:3" by blast
513      next
514        AOT_assume ‹❙𝒜φ{p}›
515        AOT_hence ‹s ⊨ p›
516          using "intro-elim:3:b" "rule-ui:3" s_prop by blast
517        AOT_thus ‹❙𝒜s ⊨ p›
518          using "intro-elim:3:b" "lem2:4" by blast
519      qed
520    qed
521    ultimately AOT_show ‹❙𝒜(Situation(y) & ∀p (y ⊨ p ≡ φ{p}))›
522      using id_sym "l-identity"[axiom_inst, THEN "→E", THEN "→E"] by fast
523  qed
524  AOT_thus ‹∃x ∀y (❙𝒜(Situation(y) & ∀p (y ⊨ p ≡ φ{p})) ≡ y = x)›
525    using "∃I" by fast
526qed
527
528AOT_theorem "sit-comp-simp:4":
529  assumes ‹RIGID_CONDITION(φ)›
530  shows ‹y = ❙ιs ∀p(s ⊨ p ≡ φ{p}) → ∀p (y ⊨ p ≡ φ{p})›
531proof(rule "→I")
532  AOT_assume ‹y = ❙ιs(∀p (s ⊨ p ≡ φ{p}))›
533  AOT_hence 0: ‹❙𝒜(Situation(y) & ∀p (y ⊨ p ≡ φ{p}))›
534    using "actual-desc:2" "→E" by blast
535  AOT_hence ‹❙𝒜∀p (y ⊨ p ≡ φ{p})›
536    using "Act-Basic:2" "con-dis-i-e:2:b" "intro-elim:3:a" by blast
537  AOT_hence 1: ‹∀p ❙𝒜(y ⊨ p ≡ φ{p})›
538    using "intro-elim:3:a" "logic-actual-nec:3" "vdash-properties:1[2]" by blast
539
540  AOT_have sit_y: ‹Situation(y)›
541    using 0 "&E"(1) "Act-Basic:2" "intro-elim:3:a" "possit-sit:4" by blast
542
543  AOT_show ‹∀p (y ⊨ p ≡ φ{p})›
544  proof(rule GEN)
545    fix p
546    AOT_have ‹❙𝒜(y ⊨ p ≡ φ{p})›
547      using 1 "∀E" by blast
548    AOT_hence ‹❙𝒜y ⊨ p ≡ ❙𝒜φ{p}›
549      using "Act-Basic:5" "intro-elim:3:a" by blast
550    moreover {
551      AOT_have ‹□(φ{p} → □φ{p})›
552        using "strict-can:1[E]"[OF assms] RN "BFs:2" "→E" "∀E" by blast
553      AOT_hence ‹❙𝒜φ{p} ≡ φ{p}›
554        using "sc-eq-fur:2" "vdash-properties:10" by blast
555    }
556    ultimately AOT_show ‹y ⊨ p ≡ φ{p}›
557      using "lem2:4"[unconstrain s, THEN "→E", OF sit_y]
558      by (meson "intro-elim:3:f")
559  qed
560qed
561
562
563AOT_theorem "sit-comp-simp-unique": ‹∃!s∀p(s ⊨ p ≡ φ{p})›
564proof(safe intro!: "uniqueness:1"[THEN "≡⇩_d⇩_fI"])
565  AOT_obtain s where s_prop: ‹∀p(s ⊨ p ≡ φ{p})›
566    using "sit-comp-simp:1" Situation.instantiation[rotated] by meson
567  AOT_show ‹∃α (Situation(α) & ∀p (α ⊨ p ≡ φ{p}) & ∀β (Situation(β) & ∀p (β ⊨ p ≡ φ{p}) → β = α))›
568  proof(safe intro!: "∃I"(2) "&I")
569    AOT_show ‹Situation(s)›
570      using "Situation.ψ" by auto
571  next
572    AOT_show ‹∀p(s ⊨ p ≡ φ{p})› using s_prop.
573  next
574    AOT_show ‹∀β (Situation(β) & ∀p (β ⊨ p ≡ φ{p}) → β = s)›
575    proof(safe intro!: GEN "→I")
576      fix x
577      AOT_assume 1: ‹Situation(x) & ∀p (x ⊨ p ≡ φ{p})›
578      AOT_show ‹x = s›
579      proof (safe intro!: "sit-identity"[unconstrain s, THEN "→E", THEN "≡E"(2)] 1[THEN "&E"(1)] GEN "≡I" "→I")
580        fix p
581        AOT_assume ‹x ⊨ p›
582        AOT_hence ‹φ{p}›
583          using "1" "con-dis-i-e:2:b" "intro-elim:3:a" "log-prop-prop:2" "rule-ui:1" by blast
584        AOT_thus ‹s ⊨ p›
585          using s_prop  "intro-elim:3:b" "log-prop-prop:2" "rule-ui:1" by blast
586      next
587        fix p
588        AOT_assume ‹s ⊨ p›
589        AOT_hence ‹φ{p}›
590          using "intro-elim:3:a" "log-prop-prop:2" "rule-ui:1" s_prop by blast
591        AOT_thus ‹x ⊨ p›
592          using "1" "con-dis-i-e:2:b" "intro-elim:3:b" "log-prop-prop:2" "rule-ui:1" by blast
593      qed
594    qed
595  qed
596qed
597
598AOT_define NullSituation :: ‹τ ⇒ φ› (‹NullSituation'(_')›)
599  "df-null-trivial:1": ‹NullSituation(s) ≡⇩_d⇩_f ¬∃p s ⊨ p›
600
601AOT_define TrivialSituation :: ‹τ ⇒ φ› (‹TrivialSituation'(_')›)
602  "df-null-trivial:2": ‹TrivialSituation(s) ≡⇩_d⇩_f ∀p s ⊨ p›
603
604AOT_theorem "thm-null-trivial:1": ‹∃!x NullSituation(x)›
605proof (AOT_subst ‹NullSituation(x)› ‹A!x & ∀F (x[F] ≡ F ≠ F)› for: x)
606  AOT_modally_strict {
607    AOT_show ‹NullSituation(x) ≡ A!x & ∀F (x[F] ≡ F ≠ F)› for x
608    proof (safe intro!: "≡I" "→I" "df-null-trivial:1"[THEN "≡⇩_d⇩_fI"]
609                dest!: "df-null-trivial:1"[THEN "≡⇩_d⇩_fE"])
610      AOT_assume 0: ‹Situation(x) & ¬∃p x ⊨ p›
611      AOT_have 1: ‹A!x›
612        using 0[THEN "&E"(1), THEN situations[THEN "≡⇩_d⇩_fE"], THEN "&E"(1)].
613      AOT_have 2: ‹x[F] → ∃p F = [λy p]› for F
614        using 0[THEN "&E"(1), THEN situations[THEN "≡⇩_d⇩_fE"],
615                THEN "&E"(2), THEN "∀E"(2)]
616        by (metis "≡⇩_d⇩_fE" "→I" "prop-prop1" "→E")
617      AOT_show ‹A!x & ∀F (x[F] ≡ F ≠ F)›
618      proof (safe intro!: "&I" 1 GEN "≡I" "→I")
619        fix F
620        AOT_assume ‹x[F]›
621        moreover AOT_obtain p where ‹F = [λy p]›
622          using calculation 2[THEN "→E"] "∃E"[rotated] by blast
623        ultimately AOT_have ‹x[λy p]›
624          by (metis "rule=E")
625        AOT_hence ‹x ⊨ p›
626          using lem1[THEN "→E", OF 0[THEN "&E"(1)], THEN "≡E"(2)] by blast
627        AOT_hence ‹∃p (x ⊨ p)›
628          by (rule "∃I")
629        AOT_thus ‹F ≠ F›
630          using 0[THEN "&E"(2)] "raa-cor:1" "&I" by blast
631      next
632        fix F :: ‹<κ> AOT_var›
633        AOT_assume ‹F ≠ F›
634        AOT_hence ‹¬(F = F)› by (metis "≡⇩_d⇩_fE" "=-infix")
635        moreover AOT_have ‹F = F›
636          by (simp add: "id-eq:1")
637        ultimately AOT_show ‹x[F]› using "&I" "raa-cor:1" by blast
638      qed
639    next
640      AOT_assume 0: ‹A!x & ∀F (x[F] ≡ F ≠ F)›
641      AOT_hence ‹x[F] ≡ F ≠ F› for F
642        using "∀E" "&E" by blast
643      AOT_hence 1: ‹¬x[F]› for F
644        using "≡⇩_d⇩_fE" "id-eq:1" "=-infix" "reductio-aa:1" "≡E"(1) by blast
645      AOT_show ‹Situation(x) & ¬∃p x ⊨ p›
646      proof (safe intro!: "&I" situations[THEN "≡⇩_d⇩_fI"] 0[THEN "&E"(1)] GEN "→I")
647        AOT_show ‹Propositional([F])› if ‹x[F]› for F
648          using that 1 "&I" "raa-cor:1" by fast
649      next
650        AOT_show ‹¬∃p x ⊨ p›
651        proof(rule "raa-cor:2")
652          AOT_assume ‹∃p x ⊨ p›
653          then AOT_obtain p where ‹x ⊨ p› using "∃E"[rotated] by blast
654          AOT_hence ‹x[λy p]›
655            using "≡⇩_d⇩_fE" "&E"(1) "≡E"(1) lem1 "modus-tollens:1"
656                  "raa-cor:3" "true-in-s" by fast
657          moreover AOT_have ‹¬x[λy p]›
658            by (rule 1[unvarify F]) "cqt:2[lambda]"
659          ultimately AOT_show ‹p & ¬p› for p using "&I" "raa-cor:1" by blast
660        qed
661      qed
662    qed
663  }
664next
665  AOT_show ‹∃!x ([A!]x & ∀F (x[F] ≡ F ≠ F))›
666    by (simp add: "A-objects!")
667qed
668
669
670AOT_theorem "thm-null-trivial:2": ‹∃!x TrivialSituation(x)›
671proof (AOT_subst ‹TrivialSituation(x)› ‹A!x & ∀F (x[F] ≡ ∃p F = [λy p])› for: x)
672  AOT_modally_strict {
673    AOT_show ‹TrivialSituation(x) ≡ A!x & ∀F (x[F] ≡ ∃p F = [λy p])› for x
674    proof (safe intro!: "≡I" "→I" "df-null-trivial:2"[THEN "≡⇩_d⇩_fI"]
675                 dest!: "df-null-trivial:2"[THEN "≡⇩_d⇩_fE"])
676      AOT_assume 0: ‹Situation(x) & ∀p x ⊨ p›
677      AOT_have 1: ‹A!x›
678        using 0[THEN "&E"(1), THEN situations[THEN "≡⇩_d⇩_fE"], THEN "&E"(1)].
679      AOT_have 2: ‹x[F] → ∃p F = [λy p]› for F
680        using 0[THEN "&E"(1), THEN situations[THEN "≡⇩_d⇩_fE"],
681                THEN "&E"(2), THEN "∀E"(2)]
682        by (metis "≡⇩_d⇩_fE" "deduction-theorem" "prop-prop1" "→E")
683      AOT_show ‹A!x & ∀F (x[F] ≡ ∃p F = [λy p])›
684      proof (safe intro!: "&I" 1 GEN "≡I" "→I" 2)
685        fix F
686        AOT_assume ‹∃p F = [λy p]›
687        then AOT_obtain p where ‹F = [λy p]›
688          using "∃E"[rotated] by blast
689        moreover AOT_have ‹x ⊨ p›
690          using 0[THEN "&E"(2)] "∀E" by blast
691        ultimately AOT_show ‹x[F]›
692          by (metis 0 "rule=E" "&E"(1) id_sym "≡E"(2) lem1
693                    "Commutativity of ≡" "→E")
694      qed
695    next
696      AOT_assume 0: ‹A!x & ∀F (x[F] ≡ ∃p F = [λy p])›
697      AOT_hence 1: ‹x[F] ≡ ∃p F = [λy p]› for F
698        using "∀E" "&E" by blast
699      AOT_have 2: ‹Situation(x)›
700      proof (safe intro!: "&I" situations[THEN "≡⇩_d⇩_fI"] 0[THEN "&E"(1)] GEN "→I")
701        AOT_show ‹Propositional([F])› if ‹x[F]› for F
702          using 1[THEN "≡E"(1), OF that]
703          by (metis "≡⇩_d⇩_fI" "prop-prop1")
704      qed
705      AOT_show ‹Situation(x) & ∀p (x ⊨ p)›
706      proof (safe intro!: "&I" 2 0[THEN "&E"(1)] GEN "→I")
707        AOT_have ‹x[λy p] ≡ ∃q [λy p] = [λy q]› for p
708          by (rule 1[unvarify F, where τ="«[λy p]»"]) "cqt:2[lambda]"
709        moreover AOT_have ‹∃q [λy p] = [λy q]› for p
710          by (rule "∃I"(2)[where β=p])
711             (simp add: "rule=I:1" "prop-prop2:2")
712        ultimately AOT_have ‹x[λy p]› for p by (metis "≡E"(2))
713        AOT_thus ‹x ⊨ p› for p
714          by (metis "2" "≡E"(2) lem1 "→E")
715      qed
716    qed
717  }
718next
719  AOT_show ‹∃!x ([A!]x & ∀F (x[F] ≡ ∃p F = [λy p]))›
720    by (simp add: "A-objects!")
721qed
722
723AOT_theorem "thm-null-trivial:3": ‹❙ιx NullSituation(x)↓›
724  by (meson "A-Exists:2" "RA[2]" "≡E"(2) "thm-null-trivial:1")
725
726AOT_theorem "thm-null-trivial:4": ‹❙ιx TrivialSituation(x)↓›
727  using "A-Exists:2" "RA[2]" "≡E"(2) "thm-null-trivial:2" by blast
728
729AOT_define TheNullSituation :: ‹κ⇩_s› (‹❙s⇩_∅›)
730  "df-the-null-sit:1": ‹❙s⇩_∅ =⇩_d⇩_f ❙ιx NullSituation(x)›
731
732AOT_define TheTrivialSituation :: ‹κ⇩_s› (‹❙s⇩_V›)
733  "df-the-null-sit:2": ‹❙s⇩_V =⇩_d⇩_f ❙ιx TrivialSituation(x)›
734
735AOT_theorem "null-triv-sc:1": ‹NullSituation(x) → □NullSituation(x)›
736proof(safe intro!: "→I" dest!: "df-null-trivial:1"[THEN "≡⇩_d⇩_fE"];
737      frule "&E"(1); drule "&E"(2))
738  AOT_assume 1: ‹¬∃p (x ⊨ p)›
739  AOT_assume 0: ‹Situation(x)›
740  AOT_hence ‹□Situation(x)› by (metis "≡E"(1) "possit-sit:1")
741  moreover AOT_have ‹□¬∃p (x ⊨ p)›
742  proof(rule "raa-cor:1")
743    AOT_assume ‹¬□¬∃p (x ⊨ p)›
744    AOT_hence ‹◇∃p (x ⊨ p)›
745      by (metis "≡⇩_d⇩_fI" "conventions:5")
746    AOT_hence ‹∃p ◇(x ⊨ p)› by (metis "BF◇" "→E")
747    then AOT_obtain p where ‹◇(x ⊨ p)› using "∃E"[rotated] by blast
748    AOT_hence ‹x ⊨ p›
749      by (metis "≡E"(1) "lem2:2"[unconstrain s, THEN "→E", OF 0])
750    AOT_hence ‹∃p x ⊨ p› using "∃I" by fast
751    AOT_thus ‹∃p x ⊨ p & ¬∃p x ⊨ p› using 1 "&I" by blast
752  qed
753  ultimately AOT_have 2: ‹□(Situation(x) & ¬∃p x ⊨ p)›
754    by (metis "KBasic:3" "&I" "≡E"(2))
755  AOT_show ‹□NullSituation(x)›
756    by (AOT_subst ‹NullSituation(x)› ‹Situation(x) & ¬∃p x ⊨ p›)
757       (auto simp: "df-null-trivial:1" "≡Df" 2)
758qed
759
760
761AOT_theorem "null-triv-sc:2": ‹TrivialSituation(x) → □TrivialSituation(x)›
762proof(safe intro!: "→I" dest!: "df-null-trivial:2"[THEN "≡⇩_d⇩_fE"];
763      frule "&E"(1); drule "&E"(2))
764  AOT_assume 0: ‹Situation(x)›
765  AOT_hence 1: ‹□Situation(x)› by (metis "≡E"(1) "possit-sit:1")
766  AOT_assume ‹∀p x ⊨ p›
767  AOT_hence ‹x ⊨ p› for p
768    using "∀E" by blast
769  AOT_hence ‹□x ⊨ p› for p
770    using  0 "≡E"(1) "lem2:1"[unconstrain s, THEN "→E"] by blast
771  AOT_hence ‹∀p □x ⊨ p›
772    by (rule GEN)
773  AOT_hence ‹□∀p x ⊨ p›
774    by (rule BF[THEN "→E"])
775  AOT_hence 2: ‹□(Situation(x) & ∀p x ⊨ p)›
776    using 1 by (metis "KBasic:3" "&I" "≡E"(2))
777  AOT_show ‹□TrivialSituation(x)›
778    by (AOT_subst ‹TrivialSituation(x)› ‹Situation(x) & ∀p x ⊨ p›)
779       (auto simp: "df-null-trivial:2" "≡Df" 2)
780qed
781
782AOT_theorem "null-triv-sc:3": ‹NullSituation(❙s⇩_∅)›
783  by (safe intro!: "df-the-null-sit:1"[THEN "=⇩_d⇩_fI"(2)] "thm-null-trivial:3"
784       "rule=I:1"[OF "thm-null-trivial:3"]
785       "!box-desc:2"[THEN "→E", THEN "→E", rotated, OF "thm-null-trivial:1",
786                     OF "∀I", OF "null-triv-sc:1", THEN "∀E"(1), THEN "→E"])
787
788AOT_theorem "null-triv-sc:4": ‹TrivialSituation(❙s⇩_V)›
789  by (safe intro!: "df-the-null-sit:2"[THEN "=⇩_d⇩_fI"(2)] "thm-null-trivial:4"
790       "rule=I:1"[OF "thm-null-trivial:4"]
791       "!box-desc:2"[THEN "→E", THEN "→E", rotated, OF "thm-null-trivial:2",
792                     OF "∀I", OF "null-triv-sc:2", THEN "∀E"(1), THEN "→E"])
793
794AOT_theorem "null-triv-facts:1": ‹NullSituation(x) ≡ Null(x)›
795proof (safe intro!: "≡I" "→I" "df-null-uni:1"[THEN "≡⇩_d⇩_fI"]
796                    "df-null-trivial:1"[THEN "≡⇩_d⇩_fI"]
797            dest!: "df-null-uni:1"[THEN "≡⇩_d⇩_fE"] "df-null-trivial:1"[THEN "≡⇩_d⇩_fE"])
798  AOT_assume 0: ‹Situation(x) & ¬∃p x ⊨ p›
799  AOT_have 1: ‹x[F] → ∃p F = [λy p]› for F
800    using 0[THEN "&E"(1), THEN situations[THEN "≡⇩_d⇩_fE"], THEN "&E"(2), THEN "∀E"(2)]
801    by (metis "≡⇩_d⇩_fE" "deduction-theorem" "prop-prop1" "→E")
802  AOT_show ‹A!x & ¬∃F x[F]›
803  proof (safe intro!: "&I" 0[THEN "&E"(1), THEN situations[THEN "≡⇩_d⇩_fE"],
804                             THEN "&E"(1)];
805         rule "raa-cor:2")
806    AOT_assume ‹∃F x[F]›
807    then AOT_obtain F where F_prop: ‹x[F]›
808      using "∃E"[rotated] by blast
809    AOT_hence ‹∃p F = [λy p]›
810      using 1[THEN "→E"] by blast
811    then AOT_obtain p where ‹F = [λy p]›
812      using "∃E"[rotated] by blast
813    AOT_hence ‹x[λy p]›
814      by (metis "rule=E" F_prop)
815    AOT_hence ‹x ⊨ p›
816      using lem1[THEN "→E", OF 0[THEN "&E"(1)], THEN "≡E"(2)] by blast
817    AOT_hence ‹∃p x ⊨ p›
818      by (rule "∃I")
819    AOT_thus ‹∃p x ⊨ p & ¬∃p x ⊨ p›
820      using 0[THEN "&E"(2)] "&I" by blast
821  qed
822next
823  AOT_assume 0: ‹A!x & ¬∃F x[F]›
824  AOT_have ‹Situation(x)›
825    apply (rule situations[THEN "≡⇩_d⇩_fI", OF "&I", OF 0[THEN "&E"(1)]]; rule GEN)
826    using 0[THEN "&E"(2)] by (metis "→I" "existential:2[const_var]" "raa-cor:3") 
827  moreover AOT_have ‹¬∃p x ⊨ p›
828  proof (rule "raa-cor:2")
829    AOT_assume ‹∃p x ⊨ p›
830    then AOT_obtain p where ‹x ⊨ p› by (metis "instantiation")
831    AOT_hence ‹x[λy p]› by (metis "≡⇩_d⇩_fE" "&E"(2) "prop-enc" "true-in-s")
832    AOT_hence ‹∃F x[F]› by (rule "∃I") "cqt:2[lambda]"
833    AOT_thus ‹∃F x[F] & ¬∃F x[F]› using 0[THEN "&E"(2)] "&I" by blast
834  qed
835  ultimately AOT_show ‹Situation(x) & ¬∃p x ⊨ p› using "&I" by blast
836qed
837
838AOT_theorem "null-triv-facts:2": ‹❙s⇩_∅ = a⇩_∅›
839  apply (rule "=⇩_d⇩_fI"(2)[OF "df-the-null-sit:1"])
840   apply (fact "thm-null-trivial:3")
841  apply (rule "=⇩_d⇩_fI"(2)[OF "df-null-uni-terms:1"])
842   apply (fact "null-uni-uniq:3")
843  apply (rule "equiv-desc-eq:3"[THEN "→E"])
844  apply (rule "&I")
845   apply (fact "thm-null-trivial:3")
846  by (rule RN; rule GEN; rule "null-triv-facts:1")
847
848AOT_theorem "null-triv-facts:3": ‹❙s⇩_V ≠ a⇩_V›
849proof(rule "=-infix"[THEN "≡⇩_d⇩_fI"])
850  AOT_have ‹Universal(a⇩_V)›
851    by (simp add: "null-uni-facts:4")
852  AOT_hence 0: ‹a⇩_V[A!]›
853    using "df-null-uni:2"[THEN "≡⇩_d⇩_fE"] "&E" "∀E"(1)
854    by (metis "cqt:5:a" "vdash-properties:10" "vdash-properties:1[2]")
855  moreover AOT_have 1: ‹¬❙s⇩_V[A!]›
856  proof(rule "raa-cor:2")
857    AOT_have ‹Situation(❙s⇩_V)›
858      using "≡⇩_d⇩_fE" "&E"(1) "df-null-trivial:2" "null-triv-sc:4" by blast
859    AOT_hence ‹∀F (❙s⇩_V[F] → Propositional([F]))›
860      by (metis "≡⇩_d⇩_fE" "&E"(2) situations)
861    moreover AOT_assume ‹❙s⇩_V[A!]›
862    ultimately AOT_have ‹Propositional(A!)›
863      using "∀E"(1)[rotated, OF "oa-exist:2"] "→E" by blast
864    AOT_thus ‹Propositional(A!) & ¬Propositional(A!)›
865      using "prop-in-f:4:d" "&I" by blast
866  qed
867  AOT_show ‹¬(❙s⇩_V = a⇩_V)›
868  proof (rule "raa-cor:2")
869    AOT_assume ‹❙s⇩_V = a⇩_V›
870    AOT_hence ‹❙s⇩_V[A!]› using 0 "rule=E" id_sym by fast
871    AOT_thus ‹❙s⇩_V[A!] & ¬❙s⇩_V[A!]› using 1 "&I" by blast
872  qed
873qed
874
875definition ConditionOnPropositionalProperties :: ‹(<κ> ⇒ 𝗈) ⇒ bool› where
876  "cond-prop": ‹ConditionOnPropositionalProperties ≡ λ φ . ∀ v .
877                        [v ⊨ ∀F (φ{F} → Propositional([F]))]›
878
879syntax ConditionOnPropositionalProperties :: ‹id_position ⇒ AOT_prop›
880  ("CONDITION'_ON'_PROPOSITIONAL'_PROPERTIES'(_')")
881
882AOT_theorem "cond-prop[E]":
883  assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
884  shows ‹∀F (φ{F} → Propositional([F]))›
885  using assms[unfolded "cond-prop"] by auto
886
887AOT_theorem "cond-prop[I]":
888  assumes ‹❙⊢⇩_□ ∀F (φ{F} → Propositional([F]))›
889  shows ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
890  using assms "cond-prop" by metis
891
892AOT_theorem "pre-comp-sit":
893  assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
894  shows ‹(Situation(x) & ∀F (x[F] ≡ φ{F})) ≡ (A!x & ∀F (x[F] ≡ φ{F}))›
895proof(rule "≡I"; rule "→I")
896  AOT_assume ‹Situation(x) & ∀F (x[F] ≡ φ{F})›
897  AOT_thus ‹A!x & ∀F (x[F] ≡ φ{F})›
898    using "&E" situations[THEN "≡⇩_d⇩_fE"] "&I" by blast
899next
900  AOT_assume 0: ‹A!x & ∀F (x[F] ≡ φ{F})›
901  AOT_show ‹Situation(x) & ∀F (x[F] ≡ φ{F})›
902  proof (safe intro!: situations[THEN "≡⇩_d⇩_fI"] "&I")
903    AOT_show ‹A!x› using 0[THEN "&E"(1)].
904  next
905    AOT_show ‹∀F (x[F] → Propositional([F]))›
906    proof(rule GEN; rule "→I")
907      fix F
908      AOT_assume ‹x[F]›
909      AOT_hence ‹φ{F}›
910        using 0[THEN "&E"(2)] "∀E" "≡E" by blast
911      AOT_thus ‹Propositional([F])›
912        using "cond-prop[E]"[OF assms] "∀E" "→E" by blast
913    qed
914  next
915    AOT_show ‹∀F (x[F] ≡ φ{F})› using 0 "&E" by blast
916  qed
917qed
918
919AOT_theorem "comp-sit:1":
920  assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
921  shows ‹∃s ∀F(s[F] ≡ φ{F})›
922  by (AOT_subst ‹Situation(x) & ∀F(x[F] ≡ φ{F})› ‹A!x & ∀F (x[F] ≡ φ{F})› for: x)
923     (auto simp: "pre-comp-sit"[OF assms] "A-objects"[where φ=φ, axiom_inst])
924
925AOT_theorem "comp-sit:2":
926  assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
927  shows ‹∃!s ∀F(s[F] ≡ φ{F})›
928  by (AOT_subst ‹Situation(x) & ∀F(x[F] ≡ φ{F})› ‹A!x & ∀F (x[F] ≡ φ{F})› for: x)
929     (auto simp: assms "pre-comp-sit"  "pre-comp-sit"[OF assms] "A-objects!")
930
931AOT_theorem "can-sit-desc:1":
932  assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
933  shows ‹❙ιs(∀F (s[F] ≡ φ{F}))↓›
934  using "comp-sit:2"[OF assms] "A-Exists:2" "RA[2]" "≡E"(2) by blast
935
936AOT_theorem "can-sit-desc:2":
937  assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
938  shows ‹❙ιs(∀F (s[F] ≡ φ{F})) = ❙ιx(A!x & ∀F (x[F] ≡ φ{F}))›
939  by (auto intro!: "equiv-desc-eq:2"[THEN "→E", OF "&I",
940                                     OF "can-sit-desc:1"[OF assms]]
941                   "RA[2]" GEN "pre-comp-sit"[OF assms])
942
943AOT_theorem "strict-sit":
944  assumes ‹RIGID_CONDITION(φ)›
945      and ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
946    shows ‹y = ❙ιs(∀F (s[F] ≡ φ{F})) → ∀F (y[F] ≡ φ{F})›
947  using "rule=E"[rotated, OF "can-sit-desc:2"[OF assms(2), symmetric]]
948        "box-phi-a:2"[OF assms(1)] "→E" "→I" "&E" by fast
949
950(* TODO: exercise (479) sit-lit *)
951
952AOT_define actual :: ‹τ ⇒ φ› (‹Actual'(_')›)
953  ‹Actual(s) ≡⇩_d⇩_f ∀p (s ⊨ p → p)›
954
955AOT_theorem "act-and-not-pos": ‹∃s (Actual(s) & ◇¬Actual(s))›
956proof -
957  AOT_obtain q⇩₁ where q⇩₁_prop: ‹q⇩₁ & ◇¬q⇩₁›
958    by (metis "≡⇩_d⇩_fE" "instantiation" "cont-tf:1" "cont-tf-thm:1")
959  AOT_have ‹∃s (∀F (s[F] ≡ F = [λy q⇩₁]))›
960  proof (safe intro!: "comp-sit:1" "cond-prop[I]" GEN "→I")
961    AOT_modally_strict {
962      AOT_show ‹Propositional([F])› if ‹F = [λy q⇩₁]› for F
963        using "≡⇩_d⇩_fI" "existential:2[const_var]" "prop-prop1" that by fastforce
964    }
965  qed
966  then AOT_obtain s⇩₁ where s_prop: ‹∀F (s⇩₁[F] ≡ F = [λy q⇩₁])›
967    using "Situation.∃E"[rotated] by meson
968  AOT_have ‹Actual(s⇩₁)›
969  proof(safe intro!: actual[THEN "≡⇩_d⇩_fI"] "&I" GEN "→I" s_prop Situation.ψ)
970    fix p
971    AOT_assume ‹s⇩₁ ⊨ p›
972    AOT_hence ‹s⇩₁[λy p]›
973      by (metis "≡⇩_d⇩_fE" "&E"(2) "prop-enc" "true-in-s")
974    AOT_hence ‹[λy p] = [λy q⇩₁]›
975      by (rule s_prop[THEN "∀E"(1), THEN "≡E"(1), rotated]) "cqt:2[lambda]"
976    AOT_hence ‹p = q⇩₁› by (metis "≡E"(2) "p-identity-thm2:3")
977    AOT_thus ‹p› using q⇩₁_prop[THEN "&E"(1)] "rule=E" id_sym by fast
978  qed
979  moreover AOT_have ‹◇¬Actual(s⇩₁)›
980  proof(rule "raa-cor:1"; drule "KBasic:12"[THEN "≡E"(2)])
981    AOT_assume ‹□Actual(s⇩₁)›
982    AOT_hence ‹□(Situation(s⇩₁) & ∀p (s⇩₁ ⊨ p → p))›
983      using actual[THEN "≡Df", THEN "conventions:3"[THEN "≡⇩_d⇩_fE"],
984                   THEN "&E"(1), THEN RM, THEN "→E"] by blast
985    AOT_hence ‹□∀p (s⇩₁ ⊨ p → p)›
986      by (metis "RM:1" "Conjunction Simplification"(2) "→E")
987    AOT_hence ‹∀p □(s⇩₁ ⊨ p → p)›
988      by (metis "CBF" "vdash-properties:10")
989    AOT_hence ‹□(s⇩₁ ⊨ q⇩₁ → q⇩₁)›
990      using "∀E" by blast
991    AOT_hence ‹□s⇩₁ ⊨ q⇩₁ → □q⇩₁›
992      by (metis "→E" "qml:1" "vdash-properties:1[2]")
993    moreover AOT_have ‹s⇩₁ ⊨ q⇩₁›
994      using s_prop[THEN "∀E"(1), THEN "≡E"(2),
995                   THEN lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(2)]]
996            "rule=I:1" "prop-prop2:2" by blast
997    ultimately AOT_have ‹□q⇩₁›
998      using "≡⇩_d⇩_fE" "&E"(1) "≡E"(1) "lem2:1" "true-in-s" "→E" by fast
999    AOT_thus ‹◇¬q⇩₁ & ¬◇¬q⇩₁›
1000      using "KBasic:12"[THEN "≡E"(1)] q⇩₁_prop[THEN "&E"(2)] "&I" by blast
1001  qed
1002  ultimately AOT_have ‹(Actual(s⇩₁) & ◇¬Actual(s⇩₁))›
1003    using s_prop "&I" by blast
1004  thus ?thesis
1005    by (rule "Situation.∃I")
1006qed
1007
1008AOT_theorem "actual-s:1": ‹∃s Actual(s)›
1009proof -
1010  AOT_obtain s where ‹(Actual(s) & ◇¬Actual(s))›
1011    using "act-and-not-pos" "Situation.∃E"[rotated] by meson
1012  AOT_hence ‹Actual(s)› using "&E" "&I" by metis
1013  thus ?thesis by (rule "Situation.∃I")
1014qed
1015
1016AOT_theorem "actual-s:2": ‹∃s ¬Actual(s)›
1017proof(rule "∃I"(1)[where τ=‹«❙s⇩_V»›]; (rule "&I")?)
1018  AOT_show ‹Situation(❙s⇩_V)›
1019    using "≡⇩_d⇩_fE" "&E"(1) "df-null-trivial:2" "null-triv-sc:4" by blast
1020next
1021  AOT_show ‹¬Actual(❙s⇩_V)›
1022  proof(rule "raa-cor:2")
1023    AOT_assume 0: ‹Actual(❙s⇩_V)›
1024    AOT_obtain p⇩₁ where notp⇩₁: ‹¬p⇩₁›
1025      by (metis "∃E" "∃I"(1) "log-prop-prop:2" "non-contradiction")
1026    AOT_have ‹❙s⇩_V ⊨ p⇩₁›
1027      using "null-triv-sc:4"[THEN "≡⇩_d⇩_fE"[OF "df-null-trivial:2"], THEN "&E"(2)]
1028            "∀E" by blast
1029    AOT_hence ‹p⇩₁›
1030      using 0[THEN actual[THEN "≡⇩_d⇩_fE"], THEN "&E"(2), THEN "∀E"(2), THEN "→E"]
1031      by blast
1032    AOT_thus ‹p & ¬p› for p using notp⇩₁ by (metis "raa-cor:3")
1033  qed
1034next
1035  AOT_show ‹❙s⇩_V↓›
1036    using "df-the-null-sit:2" "rule-id-df:2:b[zero]" "thm-null-trivial:4" by blast
1037qed
1038
1039AOT_theorem "actual-s:3": ‹∃p∀s(Actual(s) → ¬s ⊨ p)›
1040proof -
1041  AOT_obtain p⇩₁ where notp⇩₁: ‹¬p⇩₁›
1042    by (metis "∃E" "∃I"(1) "log-prop-prop:2" "non-contradiction")
1043  AOT_have ‹∀s (Actual(s) → ¬(s ⊨ p⇩₁))›
1044  proof (rule Situation.GEN; rule "→I"; rule "raa-cor:2")
1045    fix s
1046    AOT_assume ‹Actual(s)›
1047    moreover AOT_assume ‹s ⊨ p⇩₁›
1048    ultimately AOT_have ‹p⇩₁›
1049      using actual[THEN "≡⇩_d⇩_fE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"] by blast
1050    AOT_thus ‹p⇩₁ & ¬p⇩₁›
1051      using notp⇩₁ "&I" by simp
1052  qed
1053  thus ?thesis by (rule "∃I")
1054qed
1055
1056AOT_theorem comp:
1057  ‹∃s (s' ⊴ s & s'' ⊴ s & ∀s''' (s' ⊴ s''' & s'' ⊴ s''' → s ⊴ s'''))›
1058proof -
1059  have cond_prop: ‹ConditionOnPropositionalProperties (λ Π . «s'[Π] ∨ s''[Π]»)›
1060  proof(safe intro!: "cond-prop[I]" GEN "oth-class-taut:8:c"[THEN "→E", THEN "→E"];
1061        rule "→I")
1062    AOT_modally_strict {
1063      fix F
1064      AOT_have ‹Situation(s')›
1065        by (simp add: Situation.restricted_var_condition)
1066      AOT_hence ‹s'[F] → Propositional([F])›
1067        using "situations"[THEN "≡⇩_d⇩_fE", THEN "&E"(2), THEN "∀E"(2)] by blast
1068      moreover AOT_assume ‹s'[F]›
1069      ultimately AOT_show ‹Propositional([F])›
1070        using "→E" by blast
1071    }
1072  next
1073    AOT_modally_strict {
1074      fix F
1075      AOT_have ‹Situation(s'')›
1076        by (simp add: Situation.restricted_var_condition)
1077      AOT_hence ‹s''[F] → Propositional([F])›
1078        using "situations"[THEN "≡⇩_d⇩_fE", THEN "&E"(2), THEN "∀E"(2)] by blast
1079      moreover AOT_assume ‹s''[F]›
1080      ultimately AOT_show ‹Propositional([F])›
1081        using "→E" by blast
1082    }
1083  qed
1084  AOT_obtain s⇩₃ where θ: ‹∀F (s⇩₃[F] ≡ s'[F] ∨ s''[F])›
1085    using "comp-sit:1"[OF cond_prop] "Situation.∃E"[rotated] by meson
1086  AOT_have ‹s' ⊴ s⇩₃ & s'' ⊴ s⇩₃ & ∀s''' (s' ⊴ s''' & s'' ⊴ s''' → s⇩₃ ⊴ s''')›
1087  proof(safe intro!: "&I" "≡⇩_d⇩_fI"[OF "true-in-s"] "≡⇩_d⇩_fI"[OF "prop-enc"]
1088                     "Situation.GEN" "GEN"[where 'a=𝗈] "→I"
1089                     "sit-part-whole"[THEN "≡⇩_d⇩_fI"]
1090                     Situation.ψ "cqt:2[const_var]"[axiom_inst])
1091    fix p
1092    AOT_assume ‹s' ⊨ p›
1093    AOT_hence ‹s'[λx p]›
1094      by (metis "&E"(2) "prop-enc" "≡⇩_d⇩_fE" "true-in-s")
1095    AOT_thus ‹s⇩₃[λx p]›
1096      using θ[THEN "∀E"(1),OF "prop-prop2:2", THEN "≡E"(2), OF "∨I"(1)] by blast
1097  next
1098    fix p
1099    AOT_assume ‹s'' ⊨ p›
1100    AOT_hence ‹s''[λx p]›
1101      by (metis "&E"(2) "prop-enc" "≡⇩_d⇩_fE" "true-in-s")
1102    AOT_thus ‹s⇩₃[λx p]›
1103      using θ[THEN "∀E"(1),OF "prop-prop2:2", THEN "≡E"(2), OF "∨I"(2)] by blast
1104  next
1105    fix s p
1106    AOT_assume 0: ‹s' ⊴ s & s'' ⊴ s›
1107    AOT_assume ‹s⇩₃ ⊨ p›
1108    AOT_hence ‹s⇩₃[λx p]›
1109      by (metis "&E"(2) "prop-enc" "≡⇩_d⇩_fE" "true-in-s")
1110    AOT_hence ‹s'[λx p] ∨ s''[λx p]›
1111      using θ[THEN "∀E"(1),OF "prop-prop2:2", THEN "≡E"(1)] by blast
1112    moreover {
1113      AOT_assume ‹s'[λx p]›
1114      AOT_hence ‹s' ⊨ p›
1115        by (safe intro!: "prop-enc"[THEN "≡⇩_d⇩_fI"] "true-in-s"[THEN "≡⇩_d⇩_fI"] "&I"
1116                         Situation.ψ "cqt:2[const_var]"[axiom_inst])
1117      moreover AOT_have ‹s' ⊨ p → s ⊨ p›
1118        using "sit-part-whole"[THEN "≡⇩_d⇩_fE", THEN "&E"(2)] 0[THEN "&E"(1)]
1119              "∀E"(2) by blast
1120      ultimately AOT_have ‹s ⊨ p›
1121        using "→E" by blast
1122      AOT_hence ‹s[λx p]›
1123        using "true-in-s"[THEN "≡⇩_d⇩_fE"] "prop-enc"[THEN "≡⇩_d⇩_fE"] "&E" by blast
1124    }
1125    moreover {
1126      AOT_assume ‹s''[λx p]›
1127      AOT_hence ‹s'' ⊨ p›
1128        by (safe intro!: "prop-enc"[THEN "≡⇩_d⇩_fI"] "true-in-s"[THEN "≡⇩_d⇩_fI"] "&I"
1129                         Situation.ψ "cqt:2[const_var]"[axiom_inst])
1130      moreover AOT_have ‹s'' ⊨ p → s ⊨ p›
1131        using "sit-part-whole"[THEN "≡⇩_d⇩_fE", THEN "&E"(2)] 0[THEN "&E"(2)]
1132              "∀E"(2) by blast
1133      ultimately AOT_have ‹s ⊨ p›
1134        using "→E" by blast
1135      AOT_hence ‹s[λx p]›
1136        using "true-in-s"[THEN "≡⇩_d⇩_fE"] "prop-enc"[THEN "≡⇩_d⇩_fE"] "&E" by blast
1137    }
1138    ultimately AOT_show ‹s[λx p]›
1139      by (metis "∨E"(1) "→I")
1140  qed
1141  thus ?thesis
1142    using "Situation.∃I" by fast
1143qed
1144
1145AOT_theorem "act-sit:1": ‹Actual(s) → (s ⊨ p → [λy p]s)›
1146proof (safe intro!: "→I")
1147  AOT_assume ‹Actual(s)›
1148  AOT_hence p if ‹s ⊨ p›
1149    using actual[THEN "≡⇩_d⇩_fE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"] that by blast
1150  moreover AOT_assume ‹s ⊨ p›
1151  ultimately AOT_have p by blast
1152  AOT_thus ‹[λy p]s›
1153    by (safe intro!: "β←C"(1) "cqt:2")
1154qed
1155
1156AOT_theorem "act-sit:2":
1157  ‹(Actual(s') & Actual(s'')) → ∃x (Actual(x) & s' ⊴ x & s'' ⊴ x)›
1158proof(rule "→I"; frule "&E"(1); drule "&E"(2))
1159  AOT_assume act_s': ‹Actual(s')›
1160  AOT_assume act_s'': ‹Actual(s'')›
1161  have "cond-prop": ‹ConditionOnPropositionalProperties
1162                     (λ Π . «∃p (Π = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))»)›
1163  proof (safe intro!: "cond-prop[I]"  "∀I" "→I" "prop-prop1"[THEN "≡⇩_d⇩_fI"])
1164    AOT_modally_strict {
1165      fix β
1166      AOT_assume ‹∃p (β = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))›
1167      then AOT_obtain p where ‹β = [λy p]› using "∃E"[rotated] "&E" by blast
1168      AOT_thus ‹∃p β = [λy p]› by (rule "∃I")
1169    }
1170  qed
1171  have rigid: ‹rigid_condition (λ Π . «∃p (Π = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))»)›
1172  proof(safe intro!: "strict-can:1[I]" "→I" GEN)
1173    AOT_modally_strict {
1174      fix F
1175      AOT_assume ‹∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))›
1176      then AOT_obtain p⇩₁ where p⇩₁_prop: ‹F = [λy p⇩₁] & (s' ⊨ p⇩₁ ∨ s'' ⊨ p⇩₁)›
1177        using "∃E"[rotated] by blast
1178      AOT_hence ‹□(F = [λy p⇩₁])›
1179        using "&E"(1) "id-nec:2" "vdash-properties:10" by blast
1180      moreover AOT_have ‹□(s' ⊨ p⇩₁ ∨ s'' ⊨ p⇩₁)›
1181      proof(rule "∨E"; (rule "→I"; rule "KBasic:15"[THEN "→E"])?)
1182        AOT_show ‹s' ⊨ p⇩₁ ∨ s'' ⊨ p⇩₁› using p⇩₁_prop "&E" by blast
1183      next
1184        AOT_show ‹□s' ⊨ p⇩₁ ∨ □s'' ⊨ p⇩₁› if ‹s' ⊨ p⇩₁›
1185          apply (rule "∨I"(1))
1186          using "≡⇩_d⇩_fE" "&E"(1) "≡E"(1) "lem2:1" that "true-in-s" by blast
1187      next
1188        AOT_show ‹□s' ⊨ p⇩₁ ∨ □s'' ⊨ p⇩₁› if ‹s'' ⊨ p⇩₁›
1189          apply (rule "∨I"(2))
1190          using "≡⇩_d⇩_fE" "&E"(1) "≡E"(1) "lem2:1" that "true-in-s" by blast
1191      qed
1192      ultimately AOT_have ‹□(F = [λy p⇩₁] & (s' ⊨ p⇩₁ ∨ s'' ⊨ p⇩₁))›
1193        by (metis "KBasic:3" "&I" "≡E"(2))
1194      AOT_hence ‹∃p □(F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))› by (rule "∃I")
1195      AOT_thus ‹□∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))›
1196        using Buridan[THEN "→E"] by fast
1197    }
1198  qed
1199
1200  AOT_have desc_den: ‹❙ιs(∀F (s[F] ≡ ∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))))↓›
1201    by (rule "can-sit-desc:1"[OF "cond-prop"])
1202  AOT_obtain x⇩₀
1203    where x⇩₀_prop1: ‹x⇩₀ = ❙ιs(∀F (s[F] ≡ ∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))))›
1204    by (metis (no_types, lifting) "∃E" "rule=I:1" desc_den "∃I"(1) id_sym)
1205  AOT_hence x⇩₀_sit: ‹Situation(x⇩₀)›
1206    using "actual-desc:3"[THEN "→E"] "Act-Basic:2" "&E"(1) "≡E"(1)
1207          "possit-sit:4" by blast
1208
1209  AOT_have 1: ‹∀F (x⇩₀[F] ≡ ∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p)))›
1210    using "strict-sit"[OF rigid, OF "cond-prop", THEN "→E", OF x⇩₀_prop1].
1211  AOT_have 2: ‹(x⇩₀ ⊨ p) ≡ (s' ⊨ p ∨ s'' ⊨ p)› for p
1212  proof (rule "≡I"; rule "→I")
1213    AOT_assume ‹x⇩₀ ⊨ p›
1214    AOT_hence ‹x⇩₀[λy p]› using lem1[THEN "→E", OF x⇩₀_sit, THEN "≡E"(1)] by blast
1215    then AOT_obtain q where ‹[λy p] = [λy q] & (s' ⊨ q ∨ s'' ⊨ q)›
1216      using 1[THEN "∀E"(1)[where τ="«[λy p]»"], OF "prop-prop2:2", THEN "≡E"(1)]
1217            "∃E"[rotated] by blast
1218    AOT_thus ‹s' ⊨ p ∨ s'' ⊨ p›
1219      by (metis "rule=E" "&E"(1) "&E"(2) "∨I"(1) "∨I"(2)
1220                "∨E"(1) "deduction-theorem" id_sym "≡E"(2) "p-identity-thm2:3")
1221  next
1222    AOT_assume ‹s' ⊨ p ∨ s'' ⊨ p›
1223    AOT_hence ‹[λy p] = [λy p] & (s' ⊨ p ∨ s'' ⊨ p)›
1224      by (metis "rule=I:1" "&I" "prop-prop2:2") 
1225    AOT_hence ‹∃q ([λy p] = [λy q] & (s' ⊨ q ∨ s'' ⊨ q))›
1226      by (rule "∃I")
1227    AOT_hence ‹x⇩₀[λy p]›
1228      using 1[THEN "∀E"(1), OF "prop-prop2:2", THEN "≡E"(2)] by blast
1229    AOT_thus ‹x⇩₀ ⊨ p›
1230      by (metis "≡⇩_d⇩_fI" "&I" "ex:1:a" "prop-enc" "rule-ui:2[const_var]"
1231                x⇩₀_sit "true-in-s")
1232  qed
1233
1234  AOT_have ‹Actual(x⇩₀) & s' ⊴ x⇩₀ & s'' ⊴ x⇩₀›
1235  proof(safe intro!: "→I" "&I" "∃I"(1) actual[THEN "≡⇩_d⇩_fI"] x⇩₀_sit GEN
1236                     "sit-part-whole"[THEN "≡⇩_d⇩_fI"])
1237    fix p
1238    AOT_assume ‹x⇩₀ ⊨ p›
1239    AOT_hence ‹s' ⊨ p ∨ s'' ⊨ p›
1240      using 2 "≡E"(1) by metis
1241    AOT_thus ‹p›
1242      using act_s' act_s''
1243            actual[THEN "≡⇩_d⇩_fE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"]
1244      by (metis "∨E"(3) "reductio-aa:1")
1245  next
1246    AOT_show ‹x⇩₀ ⊨ p› if ‹s' ⊨ p› for p
1247      using 2[THEN "≡E"(2), OF "∨I"(1), OF that].
1248  next
1249    AOT_show ‹x⇩₀ ⊨ p› if ‹s'' ⊨ p› for p
1250      using 2[THEN "≡E"(2), OF "∨I"(2), OF that].
1251  next
1252    AOT_show ‹Situation(s')›
1253      using act_s'[THEN actual[THEN "≡⇩_d⇩_fE"]] "&E" by blast
1254  next
1255    AOT_show ‹Situation(s'')›
1256      using act_s''[THEN actual[THEN "≡⇩_d⇩_fE"]] "&E" by blast
1257  qed
1258  AOT_thus ‹∃x (Actual(x) & s' ⊴ x & s'' ⊴ x)›
1259    by (rule "∃I")
1260qed
1261
1262AOT_define Consistent :: ‹τ ⇒ φ› (‹Consistent'(_')›)
1263  cons: ‹Consistent(s) ≡⇩_d⇩_f ¬∃p (s ⊨ p & s ⊨ ¬p)›
1264
1265AOT_theorem "sit-cons": ‹Actual(s) → Consistent(s)›
1266proof(safe intro!: "→I" cons[THEN "≡⇩_d⇩_fI"] "&I" Situation.ψ
1267            dest!: actual[THEN "≡⇩_d⇩_fE"]; frule "&E"(1); drule "&E"(2))
1268  AOT_assume 0: ‹∀p (s ⊨ p → p)›
1269  AOT_show ‹¬∃p (s ⊨ p & s ⊨ ¬p)›
1270  proof (rule "raa-cor:2")
1271    AOT_assume ‹∃p (s ⊨ p & s ⊨ ¬p)›
1272    then AOT_obtain p where ‹s ⊨ p & s ⊨ ¬p›
1273      using "∃E"[rotated] by blast
1274    AOT_hence ‹p & ¬p›
1275      using 0[THEN "∀E"(1)[where τ=‹«¬p»›, THEN "→E"], OF "log-prop-prop:2"]
1276            0[THEN "∀E"(2)[where β=p], THEN "→E"] "&E" "&I" by blast
1277    AOT_thus ‹p & ¬p› for p by (metis "raa-cor:1") 
1278  qed
1279qed
1280
1281AOT_theorem "cons-rigid:1": ‹¬Consistent(s) ≡ □¬Consistent(s)›
1282proof (rule "≡I"; rule "→I")
1283  AOT_assume ‹¬Consistent(s)›
1284  AOT_hence ‹∃p (s ⊨ p & s ⊨ ¬p)›
1285    using cons[THEN "≡⇩_d⇩_fI", OF "&I", OF Situation.ψ]
1286    by (metis "raa-cor:3")
1287  then AOT_obtain p where p_prop: ‹s ⊨ p & s ⊨ ¬p›
1288    using "∃E"[rotated] by blast
1289  AOT_hence ‹□s ⊨ p›
1290    using "&E"(1) "≡E"(1) "lem2:1" by blast
1291  moreover AOT_have ‹□s ⊨ ¬p›
1292    using p_prop "T◇" "&E" "≡E"(1)
1293      "modus-tollens:1" "raa-cor:3" "lem2:3"[unvarify p]
1294      "log-prop-prop:2" by metis
1295  ultimately AOT_have ‹□(s ⊨ p & s ⊨ ¬p)›
1296    by (metis "KBasic:3" "&I" "≡E"(2))
1297  AOT_hence ‹∃p □(s ⊨ p & s ⊨ ¬p)›
1298    by (rule "∃I")
1299  AOT_hence ‹□∃p(s ⊨ p & s ⊨ ¬p)›
1300    by (metis Buridan "vdash-properties:10") 
1301  AOT_thus ‹□¬Consistent(s)›
1302    apply (rule "qml:1"[axiom_inst, THEN "→E", THEN "→E", rotated])
1303    apply (rule RN)
1304    using "≡⇩_d⇩_fE" "&E"(2) cons "deduction-theorem" "raa-cor:3" by blast
1305next
1306  AOT_assume ‹□¬Consistent(s)›
1307  AOT_thus ‹¬Consistent(s)› using "qml:2"[axiom_inst, THEN "→E"] by auto
1308qed
1309
1310AOT_theorem "cons-rigid:2": ‹◇Consistent(x) ≡ Consistent(x)›
1311proof(rule "≡I"; rule "→I")
1312  AOT_assume 0: ‹◇Consistent(x)›
1313  AOT_have ‹◇(Situation(x) & ¬∃p (x ⊨ p & x ⊨ ¬p))›
1314    apply (AOT_subst ‹Situation(x) & ¬∃p (x ⊨ p & x ⊨ ¬p)› ‹Consistent(x)›)
1315     using cons "≡E"(2) "Commutativity of ≡" "≡Df" apply blast
1316    by (simp add: 0)
1317  AOT_hence ‹◇Situation(x)› and 1: ‹◇¬∃p (x ⊨ p & x ⊨ ¬p)›
1318    using "RM◇" "Conjunction Simplification"(1) "Conjunction Simplification"(2)
1319          "modus-tollens:1" "raa-cor:3" by blast+
1320  AOT_hence 2: ‹Situation(x)› by (metis "≡E"(1) "possit-sit:2")
1321  AOT_have 3: ‹¬□∃p (x ⊨ p & x ⊨ ¬p)›
1322    using 2 using 1 "KBasic:11" "≡E"(2) by blast
1323  AOT_show ‹Consistent(x)›
1324  proof (rule "raa-cor:1")
1325    AOT_assume ‹¬Consistent(x)›
1326    AOT_hence ‹∃p (x ⊨ p & x ⊨ ¬p)›
1327      using 0 "≡⇩_d⇩_fE" "conventions:5" 2 "cons-rigid:1"[unconstrain s, THEN "→E"]
1328            "modus-tollens:1" "raa-cor:3" "≡E"(4) by meson
1329    then AOT_obtain p where ‹x ⊨ p› and 4: ‹x ⊨ ¬p›
1330      using "∃E"[rotated] "&E" by blast
1331    AOT_hence ‹□x ⊨ p›
1332      by (metis "2" "≡E"(1) "lem2:1"[unconstrain s, THEN "→E"])
1333    moreover AOT_have ‹□x ⊨ ¬p›
1334      using 4 "lem2:1"[unconstrain s, unvarify p, THEN "→E"]
1335      by (metis 2 "≡E"(1) "log-prop-prop:2")
1336    ultimately AOT_have ‹□(x ⊨ p & x ⊨ ¬p)›
1337      by (metis "KBasic:3" "&I" "≡E"(3) "raa-cor:3")
1338    AOT_hence ‹∃p □(x ⊨ p & x ⊨ ¬p)›
1339      by (metis "existential:1" "log-prop-prop:2")
1340    AOT_hence ‹□∃p (x ⊨ p & x ⊨ ¬p)›
1341      by (metis Buridan "vdash-properties:10")
1342    AOT_thus ‹p & ¬p› for p
1343      using 3 "&I"  by (metis "raa-cor:3")
1344  qed
1345next
1346  AOT_show ‹◇Consistent(x)› if ‹Consistent(x)›
1347    using "T◇" that "vdash-properties:10" by blast
1348qed
1349
1350AOT_define possible :: ‹τ ⇒ φ› (‹Possible'(_')›)
1351  pos: ‹Possible(s) ≡⇩_d⇩_f ◇Actual(s)›
1352
1353AOT_theorem "sit-pos:1": ‹Actual(s) → Possible(s)›
1354  apply(rule "→I"; rule pos[THEN "≡⇩_d⇩_fI"]; rule "&I")
1355  apply (meson "≡⇩_d⇩_fE" actual "&E"(1))
1356  using "T◇" "vdash-properties:10" by blast
1357
1358AOT_theorem "sit-pos:2": ‹∃p ((s ⊨ p) & ¬◇p) → ¬Possible(s)›
1359proof(rule "→I")
1360  AOT_assume ‹∃p ((s ⊨ p) & ¬◇p)›
1361  then AOT_obtain p where a: ‹(s ⊨ p) & ¬◇p›
1362    using "∃E"[rotated] by blast
1363  AOT_hence ‹□(s ⊨ p)›
1364    using "&E" by (metis "T◇" "≡E"(1) "lem2:3" "vdash-properties:10")
1365  moreover AOT_have ‹□¬p›
1366    using a[THEN "&E"(2)] by (metis "KBasic2:1" "≡E"(2))
1367  ultimately AOT_have ‹□(s ⊨ p & ¬p)›
1368    by (metis "KBasic:3" "&I" "≡E"(3) "raa-cor:3")
1369  AOT_hence ‹∃p □(s ⊨ p & ¬p)›
1370    by (rule "∃I")
1371  AOT_hence 1: ‹□∃q (s ⊨ q & ¬q)›
1372    by (metis Buridan "vdash-properties:10")
1373  AOT_have ‹□¬∀q (s ⊨ q → q)›
1374    apply (AOT_subst ‹s ⊨ q → q› ‹¬(s ⊨ q & ¬q)› for: q)
1375     apply (simp add: "oth-class-taut:1:a")
1376    apply (AOT_subst ‹¬∀q ¬(s ⊨ q & ¬q)› ‹∃q (s ⊨ q & ¬q)›)
1377    by (auto simp: "conventions:4" "df-rules-formulas[3]" "df-rules-formulas[4]" "≡I" 1)
1378  AOT_hence 0: ‹¬◇∀q (s ⊨ q → q)›
1379    by (metis "≡⇩_d⇩_fE" "conventions:5" "raa-cor:3")
1380  AOT_show ‹¬Possible(s)›
1381    apply (AOT_subst ‹Possible(s)› ‹Situation(s) & ◇Actual(s)›)
1382     apply (simp add: pos "≡Df")
1383    apply (AOT_subst ‹Actual(s)› ‹Situation(s) & ∀q (s ⊨ q → q)›)
1384     using actual "≡Df" apply presburger
1385    by (metis "0" "KBasic2:3" "&E"(2) "raa-cor:3" "vdash-properties:10")
1386qed
1387
1388AOT_theorem "pos-cons-sit:1": ‹Possible(s) → Consistent(s)›
1389  by (auto simp: "sit-cons"[THEN "RM◇", THEN "→E",
1390                            THEN "cons-rigid:2"[THEN "≡E"(1)]]
1391           intro!: "→I" dest!: pos[THEN "≡⇩_d⇩_fE"] "&E"(2))
1392
1393AOT_theorem "pos-cons-sit:2": ‹∃s (Consistent(s) & ¬Possible(s))›
1394proof -
1395  AOT_obtain q⇩₁ where ‹q⇩₁ & ◇¬q⇩₁›
1396    using "≡⇩_d⇩_fE" "instantiation" "cont-tf:1" "cont-tf-thm:1" by blast
1397  have "cond-prop": ‹ConditionOnPropositionalProperties
1398                      (λ Π . «Π = [λy q⇩₁ & ¬q⇩₁]»)›
1399    by (auto intro!: "cond-prop[I]" GEN "→I" "prop-prop1"[THEN "≡⇩_d⇩_fI"]
1400                     "∃I"(1)[where τ=‹«q⇩₁ & ¬q⇩₁»›, rotated, OF "log-prop-prop:2"])
1401  have rigid: ‹rigid_condition (λ Π . «Π = [λy q⇩₁ & ¬q⇩₁]»)›
1402    by (auto intro!: "strict-can:1[I]" GEN "→I" simp: "id-nec:2"[THEN "→E"])
1403
1404  AOT_obtain x where x_prop: ‹x = ❙ιs (∀F (s[F] ≡ F = [λy q⇩₁ & ¬q⇩₁]))›
1405    using "ex:1:b"[THEN "∀E"(1), OF "can-sit-desc:1", OF "cond-prop"]
1406          "∃E"[rotated] by blast    
1407  AOT_hence 0: ‹❙𝒜(Situation(x) & ∀F (x[F] ≡ F = [λy q⇩₁ & ¬q⇩₁]))›
1408    using "→E" "actual-desc:2" by blast
1409  AOT_hence ‹❙𝒜(Situation(x))› by (metis "Act-Basic:2" "&E"(1) "≡E"(1))
1410  AOT_hence s_sit: ‹Situation(x)› by (metis "≡E"(1) "possit-sit:4")
1411  AOT_have s_enc_prop: ‹∀F (x[F] ≡ F = [λy q⇩₁ & ¬q⇩₁])›
1412    using "strict-sit"[OF rigid, OF "cond-prop", THEN "→E", OF x_prop].
1413  AOT_hence ‹x[λy q⇩₁ & ¬q⇩₁]›
1414    using "∀E"(1)[rotated, OF "prop-prop2:2"]
1415          "rule=I:1"[OF "prop-prop2:2"] "≡E" by blast
1416  AOT_hence ‹x ⊨ (q⇩₁ & ¬q⇩₁)›
1417    using lem1[THEN "→E", OF s_sit, unvarify p, THEN "≡E"(2), OF "log-prop-prop:2"]
1418    by blast
1419  AOT_hence ‹□(x ⊨ (q⇩₁ & ¬q⇩₁))›
1420    using "lem2:1"[unconstrain s, THEN "→E", OF s_sit, unvarify p,
1421                   OF "log-prop-prop:2", THEN "≡E"(1)] by blast
1422  moreover AOT_have ‹□(x ⊨ (q⇩₁ & ¬q⇩₁) → ¬Actual(x))›
1423  proof(rule RN; rule "→I"; rule "raa-cor:2")
1424    AOT_modally_strict {
1425      AOT_assume ‹Actual(x)›
1426      AOT_hence ‹∀p (x ⊨ p → p)›
1427        using actual[THEN "≡⇩_d⇩_fE", THEN "&E"(2)] by blast
1428      moreover AOT_assume ‹x ⊨ (q⇩₁ & ¬q⇩₁)›
1429      ultimately AOT_show ‹q⇩₁ & ¬q⇩₁›
1430        using "∀E"(1)[rotated, OF "log-prop-prop:2"] "→E" by metis
1431    }
1432  qed
1433  ultimately AOT_have nec_not_actual_s: ‹□¬Actual(x)›
1434    using "qml:1"[axiom_inst, THEN "→E", THEN "→E"] by blast
1435  AOT_have 1: ‹¬∃p (x ⊨ p & x ⊨ ¬p)›
1436  proof (rule "raa-cor:2")
1437    AOT_assume ‹∃p (x ⊨ p & x ⊨ ¬p)›
1438    then AOT_obtain p where ‹x ⊨ p & x ⊨ ¬p›
1439      using "∃E"[rotated] by blast
1440    AOT_hence ‹x[λy p] & x[λy ¬p]›
1441      using lem1[unvarify p, THEN "→E", OF "log-prop-prop:2",
1442                 OF s_sit, THEN "≡E"(1)] "&I" "&E" by metis
1443    AOT_hence ‹[λy p] = [λy q⇩₁ & ¬q⇩₁]› and ‹[λy ¬p] = [λy q⇩₁ & ¬q⇩₁]›
1444      by (auto intro!: "prop-prop2:2" s_enc_prop[THEN "∀E"(1), THEN "≡E"(1)]
1445               elim: "&E")
1446    AOT_hence i: ‹[λy p] = [λy ¬p]› by (metis "rule=E" id_sym)
1447    {
1448      AOT_assume 0: ‹p›
1449      AOT_have ‹[λy p]x› for x
1450        by (auto intro!: "β←C"(1) "cqt:2" 0)
1451      AOT_hence ‹[λy ¬p]x› for x using i "rule=E" by fast
1452      AOT_hence ‹¬p›
1453        using "β→C"(1) by auto
1454    }
1455    moreover {
1456      AOT_assume 0: ‹¬p›
1457      AOT_have ‹[λy ¬p]x› for x
1458        by (auto intro!: "β←C"(1) "cqt:2" 0)
1459      AOT_hence ‹[λy p]x› for x using i[symmetric] "rule=E" by fast
1460      AOT_hence ‹p›
1461        using "β→C"(1) by auto
1462    }
1463    ultimately AOT_show ‹p & ¬p› for p by (metis "raa-cor:1" "raa-cor:3")
1464  qed
1465  AOT_have 2: ‹¬Possible(x)›
1466  proof(rule "raa-cor:2")
1467    AOT_assume ‹Possible(x)›
1468    AOT_hence ‹◇Actual(x)›
1469      by (metis "≡⇩_d⇩_fE" "&E"(2) pos)
1470    moreover AOT_have ‹¬◇Actual(x)› using nec_not_actual_s
1471      using "≡⇩_d⇩_fE" "conventions:5" "reductio-aa:2" by blast
1472    ultimately AOT_show ‹◇Actual(x) & ¬◇Actual(x)› by (rule "&I")
1473  qed
1474  show ?thesis
1475    by(rule "∃I"(2)[where β=x]; safe intro!: "&I" 2 s_sit cons[THEN "≡⇩_d⇩_fI"] 1)
1476qed
1477
1478AOT_theorem "sit-classical:1": ‹∀p (s ⊨ p ≡ p) → ∀q(s ⊨ ¬q ≡ ¬s ⊨ q)›
1479proof(rule "→I"; rule GEN)
1480  fix q
1481  AOT_assume ‹∀p (s ⊨ p ≡ p)›
1482  AOT_hence ‹s ⊨ q ≡ q› and ‹s ⊨ ¬q ≡ ¬q›
1483    using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
1484  AOT_thus ‹s ⊨ ¬q ≡ ¬s ⊨ q›
1485    by (metis "deduction-theorem" "≡I" "≡E"(1) "≡E"(2) "≡E"(4))
1486qed
1487
1488AOT_theorem "sit-classical:2":
1489  ‹∀p (s ⊨ p ≡ p) → ∀q∀r((s ⊨ (q → r)) ≡ (s ⊨ q → s ⊨ r))›
1490proof(rule "→I"; rule GEN; rule GEN)
1491  fix q r
1492  AOT_assume ‹∀p (s ⊨ p ≡ p)›
1493  AOT_hence θ: ‹s ⊨ q ≡ q› and ξ: ‹s ⊨ r ≡ r› and ζ: ‹(s ⊨ (q → r)) ≡ (q → r)›
1494    using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
1495  AOT_show ‹(s ⊨ (q → r)) ≡ (s ⊨ q → s ⊨ r)›
1496  proof (safe intro!: "≡I" "→I")
1497    AOT_assume ‹s ⊨ (q → r)›
1498    moreover AOT_assume ‹s ⊨ q›
1499    ultimately AOT_show ‹s ⊨ r›
1500      using θ ξ ζ by (metis "≡E"(1) "≡E"(2) "vdash-properties:10")
1501  next
1502    AOT_assume ‹s ⊨ q → s ⊨ r›
1503    AOT_thus ‹s ⊨ (q → r)›
1504      using θ ξ ζ by (metis "deduction-theorem" "≡E"(1) "≡E"(2) "→E") 
1505  qed
1506qed
1507
1508AOT_theorem "sit-classical:3":
1509  ‹∀p (s ⊨ p ≡ p) → ((s ⊨ ∀α φ{α}) ≡ ∀α s ⊨ φ{α})›
1510proof (rule "→I")
1511  AOT_assume ‹∀p (s ⊨ p ≡ p)›
1512  AOT_hence θ: ‹s ⊨ φ{α} ≡ φ{α}› and ξ: ‹s ⊨ ∀α φ{α} ≡ ∀α φ{α}› for α
1513    using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
1514  AOT_show ‹s ⊨ ∀α φ{α} ≡ ∀α s ⊨ φ{α}›
1515  proof (safe intro!: "≡I" "→I" GEN)
1516    fix α
1517    AOT_assume ‹s ⊨ ∀α φ{α}›
1518    AOT_hence ‹φ{α}› using ξ "∀E"(2) "≡E"(1) by blast
1519    AOT_thus ‹s ⊨ φ{α}› using θ "≡E"(2) by blast
1520  next
1521    AOT_assume ‹∀α s ⊨ φ{α}›
1522    AOT_hence ‹s ⊨ φ{α}› for α using "∀E"(2) by blast
1523    AOT_hence ‹φ{α}› for α using θ "≡E"(1) by blast
1524    AOT_hence ‹∀α φ{α}› by (rule GEN)
1525    AOT_thus ‹s ⊨ ∀α φ{α}› using ξ "≡E"(2) by blast
1526  qed
1527qed
1528
1529AOT_theorem "sit-classical:4": ‹∀p (s ⊨ p ≡ p) → ∀q (s ⊨ □q → □s ⊨ q)›
1530proof(rule "→I"; rule GEN; rule "→I")
1531  fix q
1532  AOT_assume ‹∀p (s ⊨ p ≡ p)›
1533  AOT_hence θ: ‹s ⊨ q ≡ q› and ξ: ‹s ⊨ □q ≡ □q›
1534    using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
1535  AOT_assume ‹s ⊨ □q›
1536  AOT_hence ‹□q› using ξ "≡E"(1) by blast
1537  AOT_hence ‹q› using "qml:2"[axiom_inst, THEN "→E"] by blast
1538  AOT_hence ‹s ⊨ q› using θ "≡E"(2) by blast
1539  AOT_thus ‹□s ⊨ q› using "≡⇩_d⇩_fE" "&E"(1) "≡E"(1) "lem2:1" "true-in-s" by blast
1540qed
1541
1542AOT_theorem "sit-classical:5":
1543  ‹∀p (s ⊨ p ≡ p) → ∃q(□(s ⊨ q) & ¬(s ⊨ □ q))›
1544proof (rule "→I")
1545  AOT_obtain r where A: ‹r› and ‹◇¬r›
1546    by (metis "&E"(1) "&E"(2) "≡⇩_d⇩_fE" "instantiation" "cont-tf:1" "cont-tf-thm:1")
1547  AOT_hence B: ‹¬□r›
1548    using "KBasic:11" "≡E"(2) by blast
1549  moreover AOT_assume asm: ‹∀ p (s ⊨ p ≡ p)›
1550  AOT_hence ‹s ⊨ r›
1551    using "∀E"(2) A "≡E"(2) by blast
1552  AOT_hence 1: ‹□s ⊨ r›
1553    using "≡⇩_d⇩_fE" "&E"(1) "≡E"(1) "lem2:1" "true-in-s" by blast
1554  AOT_have ‹s ⊨ ¬□r›
1555    using asm[THEN "∀E"(1)[rotated, OF "log-prop-prop:2"], THEN "≡E"(2)] B by blast
1556  AOT_hence ‹¬s ⊨ □r›
1557    using "sit-classical:1"[THEN "→E", OF asm,
1558              THEN "∀E"(1)[rotated, OF "log-prop-prop:2"], THEN "≡E"(1)] by blast
1559  AOT_hence ‹□s ⊨ r & ¬s ⊨ □r›
1560    using 1 "&I" by blast
1561  AOT_thus ‹∃r (□s ⊨ r & ¬s ⊨ □r)›
1562    by (rule "∃I")
1563qed
1564
1565AOT_theorem "sit-classical:6":
1566  ‹∃s ∀p (s ⊨ p ≡ p)›
1567proof -
1568  have "cond-prop": ‹ConditionOnPropositionalProperties
1569                        (λ Π . «∃q (q & Π = [λy q])»)›
1570  proof (safe intro!: "cond-prop[I]" GEN "→I")
1571    fix F
1572    AOT_modally_strict {
1573      AOT_assume ‹∃q (q & F = [λy q])›
1574      then AOT_obtain q where ‹q & F = [λy q]›
1575        using "∃E"[rotated] by blast
1576      AOT_hence ‹F = [λy q]›
1577        using "&E" by blast
1578      AOT_hence ‹∃q F = [λy q]›
1579        by (rule "∃I")
1580      AOT_thus ‹Propositional([F])›
1581        by (metis "≡⇩_d⇩_fI" "prop-prop1")
1582    }
1583  qed
1584  AOT_have ‹∃s ∀F (s[F] ≡ ∃q (q & F = [λy q]))›
1585    using "comp-sit:1"[OF "cond-prop"].
1586  then AOT_obtain s⇩₀ where s⇩₀_prop: ‹∀F (s⇩₀[F] ≡ ∃q (q & F = [λy q]))›
1587    using "Situation.∃E"[rotated] by meson
1588  AOT_have ‹∀p (s⇩₀ ⊨ p ≡ p)›
1589  proof(safe intro!: GEN "≡I" "→I")
1590    fix p
1591    AOT_assume ‹s⇩₀ ⊨ p›
1592    AOT_hence ‹s⇩₀[λy p]›
1593      using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(1)] by blast
1594    AOT_hence ‹∃q (q & [λy p] = [λy q])›
1595      using s⇩₀_prop[THEN "∀E"(1)[rotated, OF "prop-prop2:2"], THEN "≡E"(1)] by blast
1596    then AOT_obtain q⇩₁ where q⇩₁_prop: ‹q⇩₁ & [λy p] = [λy q⇩₁]›
1597      using "∃E"[rotated] by blast
1598    AOT_hence ‹p = q⇩₁›
1599      by (metis "&E"(2) "≡E"(2) "p-identity-thm2:3")
1600    AOT_thus ‹p›
1601      using q⇩₁_prop[THEN "&E"(1)] "rule=E" id_sym by fast
1602  next
1603    fix p
1604    AOT_assume ‹p›
1605    moreover AOT_have ‹[λy p] = [λy p]›
1606      by (simp add: "rule=I:1"[OF "prop-prop2:2"])
1607    ultimately AOT_have ‹p & [λy p] = [λy p]›
1608      using "&I" by blast
1609    AOT_hence ‹∃q (q & [λy p] = [λy q])›
1610      by (rule "∃I")
1611    AOT_hence ‹s⇩₀[λy p]›
1612      using s⇩₀_prop[THEN "∀E"(1)[rotated, OF "prop-prop2:2"], THEN "≡E"(2)] by blast
1613    AOT_thus ‹s⇩₀ ⊨ p›
1614      using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(2)] by blast
1615  qed
1616  AOT_hence ‹∀p (s⇩₀ ⊨ p ≡ p)›
1617    using "&I" by blast
1618  AOT_thus ‹∃s ∀p (s ⊨ p ≡ p)›
1619    by (rule "Situation.∃I")
1620qed
1621
1622AOT_define PossibleWorld :: ‹τ ⇒ φ› (‹PossibleWorld'(_')›)
1623  "world:1": ‹PossibleWorld(x) ≡⇩_d⇩_f Situation(x) & ◇∀p(x ⊨ p ≡ p)›
1624
1625AOT_theorem "world:2": ‹∃x PossibleWorld(x)›
1626proof -
1627  AOT_obtain s where s_prop: ‹∀p (s ⊨ p ≡ p)›
1628    using "sit-classical:6" "Situation.∃E"[rotated] by meson
1629  AOT_have ‹∀p (s ⊨ p ≡ p)›
1630  proof(safe intro!: GEN "≡I" "→I")
1631    fix p
1632    AOT_assume ‹s ⊨ p›
1633    AOT_thus ‹p›
1634      using s_prop[THEN "∀E"(2), THEN "≡E"(1)] by blast
1635  next
1636    fix p
1637    AOT_assume ‹p›
1638    AOT_thus ‹s ⊨ p›
1639      using s_prop[THEN "∀E"(2), THEN "≡E"(2)] by blast
1640  qed
1641  AOT_hence ‹◇∀p (s ⊨ p ≡ p)›
1642    by (metis "T◇"[THEN "→E"])
1643  AOT_hence ‹◇∀p (s ⊨ p ≡ p)›
1644    using s_prop "&I" by blast
1645  AOT_hence ‹PossibleWorld(s)›
1646    using "world:1"[THEN "≡⇩_d⇩_fI"] Situation.ψ "&I" by blast
1647  AOT_thus ‹∃x PossibleWorld(x)›
1648    by (rule "∃I")
1649qed
1650
1651AOT_theorem "world:3": ‹PossibleWorld(κ) → κ↓›
1652proof (rule "→I")
1653  AOT_assume ‹PossibleWorld(κ)›
1654  AOT_hence ‹Situation(κ)›
1655    using "world:1"[THEN "≡⇩_d⇩_fE"] "&E" by blast
1656  AOT_hence ‹A!κ›
1657    by (metis "≡⇩_d⇩_fE" "&E"(1) situations)
1658  AOT_thus ‹κ↓›
1659    by (metis "russell-axiom[exe,1].ψ_denotes_asm")
1660qed
1661
1662AOT_theorem "rigid-pw:1": ‹PossibleWorld(x) ≡ □PossibleWorld(x)›
1663proof(safe intro!: "≡I" "→I")
1664  AOT_assume ‹PossibleWorld(x)›
1665  AOT_hence ‹Situation(x) & ◇∀p(x ⊨ p ≡ p)›
1666    using "world:1"[THEN "≡⇩_d⇩_fE"] by blast
1667  AOT_hence ‹□Situation(x) & □◇∀p(x ⊨ p ≡ p)›
1668    by (metis "S5Basic:1" "&I" "&E"(1) "&E"(2) "≡E"(1) "possit-sit:1")
1669  AOT_hence 0: ‹□(Situation(x) & ◇∀p(x ⊨ p ≡ p))›
1670    by (metis "KBasic:3" "≡E"(2))
1671  AOT_show ‹□PossibleWorld(x)›
1672    by (AOT_subst ‹PossibleWorld(x)› ‹Situation(x) & ◇∀p(x ⊨ p ≡ p)›)
1673       (auto simp: "≡Df" "world:1" 0)
1674next
1675  AOT_show ‹PossibleWorld(x)› if ‹□PossibleWorld(x)›
1676    using that "qml:2"[axiom_inst, THEN "→E"] by blast
1677qed
1678
1679AOT_theorem "rigid-pw:2": ‹◇PossibleWorld(x) ≡ PossibleWorld(x)›
1680  using "rigid-pw:1"
1681  by (meson "RE◇" "S5Basic:2" "≡E"(2) "≡E"(6) "Commutativity of ≡")
1682
1683AOT_theorem "rigid-pw:3": ‹◇PossibleWorld(x) ≡ □PossibleWorld(x)›
1684  using "rigid-pw:1" "rigid-pw:2" by (meson "≡E"(5))
1685
1686AOT_theorem "rigid-pw:4": ‹❙𝒜PossibleWorld(x) ≡ PossibleWorld(x)›
1687  by (metis "Act-Sub:3" "→I" "≡I" "≡E"(6) "nec-imp-act" "rigid-pw:1" "rigid-pw:2")
1688
1689AOT_register_rigid_restricted_type
1690  PossibleWorld: ‹PossibleWorld(κ)›
1691proof
1692  AOT_modally_strict {
1693    AOT_show ‹∃x PossibleWorld(x)› using "world:2".
1694  }
1695next
1696  AOT_modally_strict {
1697    AOT_show ‹PossibleWorld(κ) → κ↓› for κ using "world:3".
1698  }
1699next
1700  AOT_modally_strict {
1701    AOT_show ‹∀α(PossibleWorld(α) → □PossibleWorld(α))›
1702      by (meson GEN "→I" "≡E"(1) "rigid-pw:1")
1703  }
1704qed
1705AOT_register_variable_names
1706  PossibleWorld: w
1707
1708AOT_theorem "world-pos": ‹Possible(w)›
1709proof (safe intro!: "≡⇩_d⇩_fE"[OF "world:1", OF PossibleWorld.ψ, THEN "&E"(1)]
1710                    pos[THEN "≡⇩_d⇩_fI"] "&I" )
1711  AOT_have ‹◇∀p (w ⊨ p ≡ p)›
1712    using "world:1"[THEN "≡⇩_d⇩_fE", OF PossibleWorld.ψ, THEN "&E"(2)].
1713  AOT_hence ‹◇∀p (w ⊨ p → p)›
1714  proof (rule "RM◇"[THEN "→E", rotated]; safe intro!: "→I" GEN)
1715    AOT_modally_strict {
1716      fix p
1717      AOT_assume ‹∀p (w ⊨ p ≡ p)›
1718      AOT_hence ‹w ⊨ p ≡ p› using "∀E"(2) by blast
1719      moreover AOT_assume ‹w ⊨ p›
1720      ultimately AOT_show p using "≡E"(1) by blast
1721    }
1722  qed
1723  AOT_hence 0: ‹◇(Situation(w) & ∀p (w ⊨ p → p))›
1724    using "world:1"[THEN "≡⇩_d⇩_fE", OF PossibleWorld.ψ, THEN "&E"(1),
1725                    THEN "possit-sit:1"[THEN "≡E"(1)]]
1726    by (metis "KBasic:16" "&I" "vdash-properties:10")
1727  AOT_show ‹◇Actual(w)›
1728    by (AOT_subst ‹Actual(w)› ‹Situation(w) & ∀p (w ⊨ p → p)›)
1729       (auto simp: actual "≡Df" 0)
1730qed
1731
1732AOT_theorem "world-cons:1": ‹Consistent(w)›
1733  using "world-pos"
1734  using "pos-cons-sit:1"[unconstrain s, THEN "→E", THEN "→E"]
1735  by (meson "≡⇩_d⇩_fE" "&E"(1) pos)
1736
1737AOT_theorem "world-cons:2": ‹¬TrivialSituation(w)›
1738proof(rule "raa-cor:2")
1739  AOT_assume ‹TrivialSituation(w)›
1740  AOT_hence ‹Situation(w) & ∀p w ⊨ p›
1741    using "df-null-trivial:2"[THEN "≡⇩_d⇩_fE"] by blast
1742  AOT_hence 0: ‹□w ⊨ (∃p (p & ¬p))›
1743    using "&E"
1744    by (metis "Buridan◇" "T◇" "&E"(2) "≡E"(1) "lem2:3"[unconstrain s, THEN "→E"]
1745              "log-prop-prop:2" "rule-ui:1" "universal-cor" "→E")
1746  AOT_have ‹◇∀p (w ⊨ p ≡ p)›
1747    using PossibleWorld.ψ "world:1"[THEN "≡⇩_d⇩_fE", THEN "&E"(2)] by metis
1748  AOT_hence ‹∀p ◇(w ⊨ p ≡ p)›
1749    using "Buridan◇"[THEN "→E"] by blast
1750  AOT_hence ‹◇(w ⊨ (∃p (p & ¬p)) ≡ (∃p (p & ¬p)))›
1751    by (metis "log-prop-prop:2" "rule-ui:1")
1752  AOT_hence ‹◇(w ⊨ (∃p (p & ¬p)) → (∃p (p & ¬p)))›
1753    using "RM◇"[THEN "→E"] "→I" "≡E"(1) by meson
1754  AOT_hence ‹◇(∃p (p & ¬p))› using 0
1755    by (metis "KBasic2:4" "≡E"(1) "→E")
1756  moreover AOT_have ‹¬◇(∃p (p & ¬p))›
1757    by (metis "instantiation" "KBasic2:1" RN "≡E"(1) "raa-cor:2")
1758  ultimately AOT_show ‹◇(∃p (p & ¬p)) & ¬◇(∃p (p & ¬p))›
1759    using "&I" by blast
1760qed
1761
1762AOT_theorem "rigid-truth-at:1": ‹w ⊨ p ≡ □w ⊨ p›
1763  using "lem2:1"[unconstrain s, THEN "→E",
1764                 OF PossibleWorld.ψ[THEN "world:1"[THEN "≡⇩_d⇩_fE"], THEN "&E"(1)]].
1765
1766AOT_theorem "rigid-truth-at:2": ‹◇w ⊨ p ≡ w ⊨ p›
1767  using "lem2:2"[unconstrain s, THEN "→E",
1768                 OF PossibleWorld.ψ[THEN "world:1"[THEN "≡⇩_d⇩_fE"], THEN "&E"(1)]].
1769
1770AOT_theorem "rigid-truth-at:3": ‹◇w ⊨ p ≡ □w ⊨ p›
1771  using "lem2:3"[unconstrain s, THEN "→E",
1772                 OF PossibleWorld.ψ[THEN "world:1"[THEN "≡⇩_d⇩_fE"], THEN "&E"(1)]].
1773
1774AOT_theorem "rigid-truth-at:4": ‹❙𝒜w ⊨ p ≡ w ⊨ p›
1775  using "lem2:4"[unconstrain s, THEN "→E",
1776                 OF PossibleWorld.ψ[THEN "world:1"[THEN "≡⇩_d⇩_fE"], THEN "&E"(1)]].
1777
1778AOT_theorem "rigid-truth-at:5": ‹¬w ⊨ p ≡ □¬w ⊨ p›
1779  using "lem2:5"[unconstrain s, THEN "→E",
1780                 OF PossibleWorld.ψ[THEN "world:1"[THEN "≡⇩_d⇩_fE"], THEN "&E"(1)]].
1781
1782AOT_define Maximal :: ‹τ ⇒ φ› (‹Maximal'(_')›)
1783  max: ‹Maximal(s) ≡⇩_d⇩_f ∀p (s ⊨ p ∨ s ⊨ ¬p)›
1784
1785AOT_theorem "world-max": ‹Maximal(w)›
1786proof(safe intro!: PossibleWorld.ψ[THEN "≡⇩_d⇩_fE"[OF "world:1"], THEN "&E"(1)]
1787                   GEN "≡⇩_d⇩_fI"[OF max] "&I" )
1788  fix q
1789  AOT_have ‹◇(w ⊨ q ∨ w ⊨ ¬q)›
1790  proof(rule "RM◇"[THEN "→E"]; (rule "→I")?)
1791    AOT_modally_strict {
1792      AOT_assume ‹∀p (w ⊨ p ≡ p)›
1793      AOT_hence ‹w ⊨ q ≡ q› and ‹w ⊨ ¬q ≡ ¬q›
1794        using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
1795      AOT_thus ‹w ⊨ q ∨ w ⊨ ¬q›
1796        by (metis "∨I"(1) "∨I"(2) "≡E"(3) "reductio-aa:1")
1797    }
1798  next
1799    AOT_show ‹◇∀p (w ⊨ p ≡ p)›
1800      using PossibleWorld.ψ[THEN "≡⇩_d⇩_fE"[OF "world:1"], THEN "&E"(2)].
1801  qed
1802  AOT_hence ‹◇w ⊨ q ∨ ◇w ⊨ ¬q›
1803    using "KBasic2:2"[THEN "≡E"(1)] by blast
1804  AOT_thus ‹w ⊨ q ∨ w ⊨ ¬q›
1805    using "lem2:2"[unconstrain s, THEN "→E", unvarify p,
1806                   OF PossibleWorld.ψ[THEN "≡⇩_d⇩_fE"[OF "world:1"], THEN "&E"(1)],
1807                   THEN "≡E"(1), OF "log-prop-prop:2"]
1808    by (metis "∨I"(1) "∨I"(2) "∨E"(3) "raa-cor:2")
1809qed
1810
1811AOT_theorem "world=maxpos:1": ‹Maximal(x) → □Maximal(x)›
1812proof (AOT_subst ‹Maximal(x)› ‹Situation(x) & ∀p (x ⊨ p ∨ x ⊨ ¬p)›;
1813       safe intro!: max "≡Df" "→I"; frule "&E"(1); drule "&E"(2))
1814  AOT_assume sit_x: ‹Situation(x)›
1815  AOT_hence nec_sit_x: ‹□Situation(x)›
1816    by (metis "≡E"(1) "possit-sit:1")
1817  AOT_assume ‹∀p (x ⊨ p ∨ x ⊨ ¬p)›
1818  AOT_hence ‹x ⊨ p ∨ x ⊨ ¬p› for p
1819    using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast
1820  AOT_hence ‹□x ⊨ p ∨ □x ⊨ ¬p› for p
1821    using "lem2:1"[unconstrain s, THEN "→E", OF sit_x, unvarify p,
1822                   OF "log-prop-prop:2", THEN "≡E"(1)]
1823    by (metis "∨I"(1) "∨I"(2) "∨E"(2) "raa-cor:1")
1824  AOT_hence ‹□(x ⊨ p ∨ x ⊨ ¬p)› for p
1825    by (metis "KBasic:15" "→E")
1826  AOT_hence ‹∀p □(x ⊨ p ∨ x ⊨ ¬p)›
1827    by (rule GEN)
1828  AOT_hence ‹□∀p (x ⊨ p ∨ x ⊨ ¬p)›
1829    by (rule BF[THEN "→E"])
1830  AOT_thus ‹□(Situation(x) & ∀p (x ⊨ p ∨ x ⊨ ¬p))›
1831    using nec_sit_x by (metis "KBasic:3" "&I" "≡E"(2))
1832qed
1833
1834AOT_theorem "world=maxpos:2": ‹PossibleWorld(x) ≡ Maximal(x) & Possible(x)›
1835proof(safe intro!: "≡I" "→I" "&I" "world-pos"[unconstrain w, THEN "→E"]
1836                   "world-max"[unconstrain w, THEN "→E"];
1837      frule "&E"(2); drule "&E"(1))
1838  AOT_assume pos_x: ‹Possible(x)›
1839  AOT_have ‹◇(Situation(x) & ∀p(x ⊨ p → p))›
1840    apply (AOT_subst (reverse) ‹Situation(x) & ∀p(x ⊨ p → p)› ‹Actual(x)›)
1841     using actual "≡Df" apply presburger
1842    using "≡⇩_d⇩_fE" "&E"(2) pos pos_x by blast
1843  AOT_hence 0: ‹◇∀p(x ⊨ p → p)›
1844    by (metis "KBasic2:3" "&E"(2) "vdash-properties:6")
1845  AOT_assume max_x: ‹Maximal(x)›
1846  AOT_hence sit_x: ‹Situation(x)› by (metis "≡⇩_d⇩_fE" max_x "&E"(1) max)
1847  AOT_have ‹□Maximal(x)› using "world=maxpos:1"[THEN "→E", OF max_x] by simp
1848  moreover AOT_have ‹□Maximal(x) → □(∀p(x ⊨ p → p) → ∀p (x ⊨ p ≡ p))›
1849  proof(safe intro!: "→I" RM GEN)
1850    AOT_modally_strict {
1851      fix p
1852      AOT_assume 0: ‹Maximal(x)›
1853      AOT_assume 1: ‹∀p (x ⊨ p → p)›
1854      AOT_show ‹x ⊨ p ≡ p›
1855      proof(safe intro!: "≡I" "→I" 1[THEN "∀E"(2), THEN "→E"]; rule "raa-cor:1")
1856        AOT_assume ‹¬x ⊨ p›
1857        AOT_hence ‹x ⊨ ¬p›
1858          using 0[THEN "≡⇩_d⇩_fE"[OF max], THEN "&E"(2), THEN "∀E"(2)]
1859                1 by (metis "∨E"(2))
1860        AOT_hence ‹¬p›
1861          using 1[THEN "∀E"(1), OF "log-prop-prop:2", THEN "→E"] by blast
1862        moreover AOT_assume p
1863        ultimately AOT_show ‹p & ¬p› using "&I" by blast
1864      qed
1865    }
1866  qed
1867  ultimately AOT_have ‹□(∀p(x ⊨ p → p) → ∀p (x ⊨ p ≡ p))›
1868    using "→E" by blast
1869  AOT_hence ‹◇∀p(x ⊨ p → p) → ◇∀p(x ⊨ p ≡ p)›
1870    by (metis "KBasic:13"[THEN "→E"])
1871  AOT_hence ‹◇∀p(x ⊨ p ≡ p)›
1872    using 0 "→E" by blast
1873  AOT_thus ‹PossibleWorld(x)›
1874    using "≡⇩_d⇩_fI"[OF "world:1", OF "&I", OF sit_x] by blast
1875qed
1876
1877AOT_define NecImpl :: ‹φ ⇒ φ ⇒ φ› (infixl ‹⇒› 26)
1878  "nec-impl-p:1": ‹p ⇒ q ≡⇩_d⇩_f □(p → q)›
1879AOT_define NecEquiv :: ‹φ ⇒ φ ⇒ φ› (infixl ‹⇔› 21)
1880  "nec-impl-p:2": ‹p ⇔ q ≡⇩_d⇩_f (p ⇒ q) & (q ⇒ p)›
1881
1882AOT_theorem "nec-impl-p:3[rec]": ‹p ⇒ p›
1883  by (safe intro!: "nec-impl-p:1"[THEN "≡⇩_d⇩_fI"] RN "→I")
1884
1885AOT_theorem "nec-impl-p:3[trans]": ‹((p ⇒ q) & (q ⇒ r)) → p ⇒ r›
1886proof (safe intro!: "nec-impl-p:1"[THEN "≡⇩_d⇩_fI"] "→I")
1887  AOT_assume ‹(p ⇒ q) & (q ⇒ r)›
1888  AOT_hence ‹□((p → q) & (q → r))›
1889    by (metis "KBasic:3" "≡⇩_d⇩_fE" "con-dis-i-e:1" "con-dis-i-e:2:a" "con-dis-i-e:2:b" "intro-elim:3:b" "nec-impl-p:1")
1890  moreover AOT_modally_strict {
1891    AOT_have ‹((p → q) & (q → r)) → (p → r)›
1892      by (metis "con-dis-i-e:2:a" "con-dis-i-e:2:b" "deduction-theorem" "vdash-properties:10")
1893  }
1894  ultimately AOT_show ‹□(p → r)›
1895    using "RM:1" "→E" by blast
1896qed
1897
1898AOT_theorem "nec-equiv-nec-im": ‹p ⇔ q ≡ □(p ≡ q)›
1899proof(safe intro!: "≡I" "→I")
1900  AOT_assume ‹p ⇔ q›
1901  AOT_hence ‹(p ⇒ q)› and ‹(q ⇒ p)›
1902    using "nec-impl-p:2"[THEN "≡⇩_d⇩_fE"] "&E" by blast+
1903  AOT_hence ‹□(p → q)› and ‹□(q → p)›
1904    using "nec-impl-p:1"[THEN "≡⇩_d⇩_fE"] by blast+
1905  AOT_thus ‹□(p ≡ q)› by (metis "KBasic:4" "&I" "≡E"(2))
1906next
1907  AOT_assume ‹□(p ≡ q)›
1908  AOT_hence ‹□(p → q)› and ‹□(q → p)›
1909    using "KBasic:4" "&E" "≡E"(1) by blast+
1910  AOT_hence ‹(p ⇒ q)› and ‹(q ⇒ p)›
1911    using "nec-impl-p:1"[THEN "≡⇩_d⇩_fI"] by blast+
1912  AOT_thus ‹p ⇔ q›
1913    using "nec-impl-p:2"[THEN "≡⇩_d⇩_fI"] "&I" by blast
1914qed
1915
1916(* TODO: PLM: discuss these; still not in PLM *)
1917AOT_theorem world_closed_lem_1_a:
1918  ‹(s ⊨ (φ & ψ)) → (∀p (s ⊨ p ≡ p) → (s ⊨ φ & s ⊨ ψ))›
1919proof(safe intro!: "→I")
1920  AOT_assume ‹∀ p (s ⊨ p ≡ p)›
1921  AOT_hence ‹s ⊨ (φ & ψ) ≡ (φ & ψ)› and ‹s ⊨ φ ≡ φ› and ‹s ⊨ ψ ≡ ψ›
1922    using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
1923  moreover AOT_assume ‹s ⊨ (φ & ψ)›
1924  ultimately AOT_show ‹s ⊨ φ & s ⊨ ψ›
1925    by (metis "&I" "&E"(1) "&E"(2) "≡E"(1) "≡E"(2))
1926qed
1927
1928AOT_theorem world_closed_lem_1_b:
1929  ‹(s ⊨ φ & (φ → q)) → (∀p (s ⊨ p ≡ p) → s ⊨ q)›
1930proof(safe intro!: "→I")
1931  AOT_assume ‹∀ p (s ⊨ p ≡ p)›
1932  AOT_hence ‹s ⊨ φ ≡ φ› for φ
1933    using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast
1934  moreover AOT_assume ‹s ⊨ φ & (φ → q)›
1935  ultimately AOT_show ‹s ⊨ q›
1936    by (metis "&E"(1) "&E"(2) "≡E"(1) "≡E"(2) "→E")
1937qed
1938
1939AOT_theorem world_closed_lem_1_c:
1940  ‹(s ⊨ φ & s ⊨ (φ → ψ)) → (∀p (s ⊨ p ≡ p) → s ⊨ ψ)›
1941proof(safe intro!: "→I")
1942  AOT_assume ‹∀ p (s ⊨ p ≡ p)›
1943  AOT_hence ‹s ⊨ φ ≡ φ› for φ
1944    using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast
1945  moreover AOT_assume ‹s ⊨ φ & s ⊨ (φ → ψ)›
1946  ultimately AOT_show ‹s ⊨ ψ›
1947    by (metis "&E"(1) "&E"(2) "≡E"(1) "≡E"(2) "→E")
1948qed
1949
1950AOT_theorem "world-closed-lem:1[0]":
1951  ‹q → (∀p (s ⊨ p ≡ p) → s ⊨ q)›
1952  by (meson "→I" "≡E"(2) "log-prop-prop:2" "rule-ui:1")
1953
1954AOT_theorem "world-closed-lem:1[1]":
1955  ‹s ⊨ p⇩₁ & (p⇩₁ → q) → (∀p (s ⊨ p ≡ p) → s ⊨ q)›
1956  using world_closed_lem_1_b.
1957
1958AOT_theorem "world-closed-lem:1[2]":
1959  ‹s ⊨ p⇩₁ & s ⊨ p⇩₂ & ((p⇩₁ & p⇩₂) → q) → (∀p (s ⊨ p ≡ p) → s ⊨ q)›
1960  using world_closed_lem_1_b world_closed_lem_1_a
1961  by (metis (full_types) "&I" "&E" "→I" "→E")
1962
1963AOT_theorem "world-closed-lem:1[3]":
1964  ‹s ⊨ p⇩₁ & s ⊨ p⇩₂ & s ⊨ p⇩₃ & ((p⇩₁ & p⇩₂ & p⇩₃) → q) → (∀p (s ⊨ p ≡ p) → s ⊨ q)›
1965  using world_closed_lem_1_b world_closed_lem_1_a
1966  by (metis (full_types) "&I" "&E" "→I" "→E")
1967
1968AOT_theorem "world-closed-lem:1[4]":
1969  ‹s ⊨ p⇩₁ & s ⊨ p⇩₂ & s ⊨ p⇩₃ & s ⊨ p⇩₄ & ((p⇩₁ & p⇩₂ & p⇩₃ & p⇩₄) → q) →
1970   (∀p (s ⊨ p ≡ p) → s ⊨ q)›
1971  using world_closed_lem_1_b world_closed_lem_1_a
1972  by (metis (full_types) "&I" "&E" "→I" "→E")
1973
1974AOT_theorem "coherent:1": ‹w ⊨ ¬p ≡ ¬w ⊨ p›
1975proof(safe intro!: "≡I" "→I")
1976  AOT_assume 1: ‹w ⊨ ¬p›
1977  AOT_show ‹¬w ⊨ p›
1978  proof(rule "raa-cor:2")
1979    AOT_assume ‹w ⊨ p›
1980    AOT_hence ‹w ⊨ p & w ⊨ ¬p› using 1 "&I" by blast
1981    AOT_hence ‹∃q (w ⊨ q & w ⊨ ¬q)› by (rule "∃I")
1982    moreover AOT_have ‹¬∃q (w ⊨ q & w ⊨ ¬q)›
1983      using "world-cons:1"[THEN "≡⇩_d⇩_fE"[OF cons], THEN "&E"(2)].
1984    ultimately AOT_show ‹∃q (w ⊨ q & w ⊨ ¬q) & ¬∃q (w ⊨ q & w ⊨ ¬q)›
1985      using "&I" by blast
1986  qed
1987next
1988  AOT_assume ‹¬w ⊨ p›
1989  AOT_thus ‹w ⊨ ¬p›
1990    using "world-max"[THEN "≡⇩_d⇩_fE"[OF max], THEN "&E"(2)]
1991    by (metis "∨E"(2) "log-prop-prop:2" "rule-ui:1")
1992qed
1993
1994AOT_theorem "coherent:2": ‹w ⊨ p ≡ ¬w ⊨ ¬p›
1995  by (metis "coherent:1" "deduction-theorem" "≡I" "≡E"(1) "≡E"(2) "raa-cor:3")
1996
1997AOT_theorem "act-world:1": ‹∃w ∀p (w ⊨ p ≡ p)›
1998proof -
1999  AOT_obtain s where s_prop: ‹∀p (s ⊨ p ≡ p)›
2000    using "sit-classical:6" "Situation.∃E"[rotated] by meson
2001  AOT_hence ‹◇∀p (s ⊨ p ≡ p)›
2002    by (metis "T◇" "vdash-properties:10")
2003  AOT_hence ‹PossibleWorld(s)›
2004    using "world:1"[THEN "≡⇩_d⇩_fI"] Situation.ψ "&I" by blast
2005  AOT_hence ‹PossibleWorld(s) & ∀p (s ⊨ p ≡ p)›
2006    using "&I" s_prop by blast
2007  thus ?thesis by (rule "∃I")
2008qed
2009
2010AOT_theorem "act-world:2": ‹∃!w Actual(w)›
2011proof -
2012  AOT_obtain w where w_prop: ‹∀p (w ⊨ p ≡ p)›
2013    using "act-world:1" "PossibleWorld.∃E"[rotated] by meson
2014  AOT_have sit_s: ‹Situation(w)›
2015    using PossibleWorld.ψ "world:1"[THEN "≡⇩_d⇩_fE", THEN "&E"(1)] by blast
2016  show ?thesis
2017  proof (safe intro!: "uniqueness:1"[THEN "≡⇩_d⇩_fI"] "∃I"(2) "&I" GEN "→I"
2018                      PossibleWorld.ψ actual[THEN "≡⇩_d⇩_fI"] sit_s
2019                      "sit-identity"[unconstrain s, unconstrain s', THEN "→E",
2020                                     THEN "→E", THEN "≡E"(2)] "≡I"
2021                      w_prop[THEN "∀E"(2), THEN "≡E"(1)])
2022    AOT_show ‹PossibleWorld(w)› using PossibleWorld.ψ.
2023  next
2024    AOT_show ‹Situation(w)›
2025      by (simp add: sit_s)
2026  next
2027    fix y p
2028    AOT_assume w_asm: ‹PossibleWorld(y) & Actual(y)›
2029    AOT_assume ‹w ⊨ p›
2030    AOT_hence p: ‹p›
2031      using w_prop[THEN "∀E"(2), THEN "≡E"(1)] by blast
2032    AOT_show ‹y ⊨ p›
2033    proof(rule "raa-cor:1")
2034      AOT_assume ‹¬y ⊨ p›
2035      AOT_hence ‹y ⊨ ¬p›
2036        by (metis "coherent:1"[unconstrain w, THEN "→E"] "&E"(1) "≡E"(2) w_asm)
2037      AOT_hence ‹¬p›
2038        using w_asm[THEN "&E"(2), THEN actual[THEN "≡⇩_d⇩_fE"], THEN "&E"(2),
2039                    THEN "∀E"(1), rotated, OF "log-prop-prop:2"]
2040              "→E" by blast
2041      AOT_thus ‹p & ¬p› using p "&I" by blast
2042    qed
2043  next
2044    AOT_show ‹w ⊨ p› if ‹y ⊨ p› and ‹PossibleWorld(y) & Actual(y)› for p y
2045      using that(2)[THEN "&E"(2), THEN actual[THEN "≡⇩_d⇩_fE"], THEN "&E"(2),
2046                    THEN "∀E"(2), THEN "→E", OF that(1)]
2047            w_prop[THEN "∀E"(2), THEN "≡E"(2)] by blast
2048  next
2049    AOT_show ‹Situation(y)› if ‹PossibleWorld(y) & Actual(y)› for y
2050      using that[THEN "&E"(1)] "world:1"[THEN "≡⇩_d⇩_fE", THEN "&E"(1)] by blast
2051  next
2052    AOT_show ‹Situation(w)›
2053      using sit_s by blast
2054  qed(simp)
2055qed
2056
2057AOT_theorem "pre-walpha": ‹❙ιw Actual(w)↓›
2058  using "A-Exists:2" "RA[2]" "act-world:2" "≡E"(2) by blast
2059
2060AOT_define TheActualWorld :: ‹κ⇩_s› (‹❙w⇩_α›)
2061  "w-alpha": ‹❙w⇩_α =⇩_d⇩_f ❙ιw Actual(w)›
2062
2063(* TODO: not in PLM *)
2064AOT_theorem true_in_truth_act_true: ‹⊤ ⊨ p ≡ ❙𝒜p›
2065proof(safe intro!: "≡I" "→I")
2066  AOT_have true_def: ‹❙⊢⇩_□ ⊤ = ❙ιx (A!x & ∀F (x[F] ≡ ∃p(p & F = [λy p])))›
2067    by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:1")
2068  AOT_hence true_den: ‹❙⊢⇩_□ ⊤↓›
2069    using "t=t-proper:1" "vdash-properties:6" by blast
2070  {
2071    AOT_assume ‹⊤ ⊨ p›
2072    AOT_hence ‹⊤[λy p]›
2073      by (metis "≡⇩_d⇩_fE" "con-dis-i-e:2:b" "prop-enc" "true-in-s")
2074    AOT_hence ‹❙ιx(A!x & ∀F (x[F] ≡ ∃q (q & F = [λy q])))[λy p]›
2075      using "rule=E" true_def true_den by fast
2076    AOT_hence ‹❙𝒜∃q (q & [λy p] = [λy q])›
2077      using "≡E"(1) "desc-nec-encode:1"[unvarify F] "prop-prop2:2" by fast
2078    AOT_hence ‹∃q ❙𝒜(q & [λy p] = [λy q])›
2079      by (metis "Act-Basic:10" "≡E"(1))
2080    then AOT_obtain q where ‹❙𝒜(q & [λy p] = [λy q])›
2081      using "∃E"[rotated] by blast
2082    AOT_hence actq: ‹❙𝒜q› and ‹❙𝒜[λy p] = [λy q]›
2083      using "Act-Basic:2" "intro-elim:3:a" "&E" by blast+
2084    AOT_hence ‹[λy p] = [λy q]›
2085      using "id-act:1"[unvarify α β, THEN "≡E"(2)] "prop-prop2:2" by blast
2086    AOT_hence ‹p = q›
2087      by (metis "intro-elim:3:b" "p-identity-thm2:3")
2088    AOT_thus ‹❙𝒜p›
2089      using actq "rule=E" id_sym by blast
2090  }
2091  {
2092    AOT_assume ‹❙𝒜p›
2093    AOT_hence ‹❙𝒜(p & [λy p] = [λy p])›
2094      by (auto intro!: "Act-Basic:2"[THEN "≡E"(2)] "&I"
2095               intro: "RA[2]" "=I"(1)[OF "prop-prop2:2"])
2096    AOT_hence ‹∃q ❙𝒜(q & [λy p] = [λy q])›
2097      using "∃I" by fast
2098    AOT_hence ‹❙𝒜∃q (q & [λy p] = [λy q])›
2099      by (metis "Act-Basic:10" "≡E"(2))
2100    AOT_hence ‹❙ιx(A!x & ∀F (x[F] ≡ ∃q (q & F = [λy q])))[λy p]›
2101      using "≡E"(2) "desc-nec-encode:1"[unvarify F] "prop-prop2:2" by fast
2102    AOT_hence ‹⊤[λy p]›
2103      using "rule=E" true_def true_den id_sym by fast
2104    AOT_thus ‹⊤ ⊨ p›
2105      by (safe intro!: "true-in-s"[THEN "≡⇩_d⇩_fI"] "&I" "possit-sit:6"
2106                       "prop-enc"[THEN "≡⇩_d⇩_fI"] true_den)
2107  }
2108qed
2109
2110AOT_theorem "T-world": ‹⊤ = ❙w⇩_α›
2111proof -
2112  AOT_have true_den: ‹❙⊢⇩_□ ⊤↓›
2113    using "Situation.res-var:3" "possit-sit:6" "→E" by blast
2114  AOT_have ‹❙𝒜∀p (⊤ ⊨ p → p)›
2115  proof (safe intro!: "logic-actual-nec:3"[axiom_inst, THEN "≡E"(2)] GEN
2116                      "logic-actual-nec:2"[axiom_inst, THEN "≡E"(2)] "→I")
2117    fix p
2118    AOT_assume ‹❙𝒜⊤ ⊨ p›
2119    AOT_hence ‹⊤ ⊨ p›
2120      using "lem2:4"[unconstrain s, unvarify β, OF true_den,
2121                     THEN "→E", OF "possit-sit:6"] "≡E"(1) by blast
2122    AOT_thus ‹❙𝒜p› using true_in_truth_act_true "≡E"(1) by blast
2123  qed
2124  moreover AOT_have ‹❙𝒜(Situation(κ) & ∀p (κ ⊨ p → p)) → ❙𝒜Actual(κ)› for κ
2125    using actual[THEN "≡Df", THEN "conventions:3"[THEN "≡⇩_d⇩_fE", THEN "&E"(2)],
2126                 THEN "RA[2]", THEN "act-cond"[THEN "→E"]].
2127  ultimately AOT_have act_act_true: ‹❙𝒜Actual(⊤)›
2128    using "possit-sit:4"[unvarify x, OF true_den, THEN "≡E"(2), OF "possit-sit:6"]
2129          "Act-Basic:2"[THEN "≡E"(2), OF "&I"] "→E" by blast
2130  AOT_hence ‹◇Actual(⊤)› by (metis "Act-Sub:3" "vdash-properties:10")
2131  AOT_hence ‹Possible(⊤)›
2132    by (safe intro!: pos[THEN "≡⇩_d⇩_fI"] "&I" "possit-sit:6")
2133  moreover AOT_have ‹Maximal(⊤)›
2134  proof (safe intro!: max[THEN "≡⇩_d⇩_fI"] "&I" "possit-sit:6" GEN)
2135    fix p
2136    AOT_have ‹❙𝒜p ∨ ❙𝒜¬p›
2137      by (simp add: "Act-Basic:1")
2138    moreover AOT_have ‹⊤ ⊨ p› if ‹❙𝒜p›
2139        using that true_in_truth_act_true[THEN "≡E"(2)] by blast
2140    moreover AOT_have ‹⊤ ⊨ ¬p› if ‹❙𝒜¬p›
2141      using that true_in_truth_act_true[unvarify p, THEN "≡E"(2)]
2142            "log-prop-prop:2" by blast
2143    ultimately AOT_show ‹⊤ ⊨ p ∨ ⊤ ⊨ ¬p›
2144      using "∨I"(3) "→I" by blast
2145  qed
2146  ultimately AOT_have ‹PossibleWorld(⊤)›
2147    by (safe intro!: "world=maxpos:2"[unvarify x, OF true_den, THEN "≡E"(2)] "&I")
2148  AOT_hence ‹❙𝒜PossibleWorld(⊤)›
2149    using "rigid-pw:4"[unvarify x, OF true_den, THEN "≡E"(2)] by blast
2150  AOT_hence 1: ‹❙𝒜(PossibleWorld(⊤) & Actual(⊤))›
2151    using act_act_true "Act-Basic:2" "df-simplify:2" "intro-elim:3:b" by blast
2152  AOT_have ‹❙w⇩_α = ❙ιw(Actual(w))›
2153    using "rule-id-df:1[zero]"[OF "w-alpha", OF "pre-walpha"] by simp
2154  moreover AOT_have w_act_den: ‹❙w⇩_α↓›
2155    using calculation "t=t-proper:1" "→E" by blast
2156  ultimately AOT_have ‹∀z (❙𝒜(PossibleWorld(z) & Actual(z)) → z = ❙w⇩_α)›
2157    using "nec-hintikka-scheme"[unvarify x] "≡E"(1) "&E" by blast
2158  AOT_thus ‹⊤ = ❙w⇩_α›
2159    using "∀E"(1)[rotated, OF true_den] 1 "→E" by blast
2160qed
2161
2162AOT_act_theorem "truth-at-alpha:1": ‹p ≡ ❙w⇩_α = ❙ιx (ExtensionOf(x, p))›
2163  by (metis "rule=E" "T-world" "deduction-theorem" "ext-p-tv:3" id_sym "≡I"
2164            "≡E"(1) "≡E"(2) "q-True:1")
2165
2166AOT_act_theorem "truth-at-alpha:2": ‹p ≡ ❙w⇩_α ⊨ p›
2167proof -
2168  AOT_have ‹PossibleWorld(❙w⇩_α)›
2169    using "&E"(1) "pre-walpha" "rule-id-df:2:b[zero]" "→E"
2170          "w-alpha" "y-in:3" by blast
2171  AOT_hence sit_w_alpha: ‹Situation(❙w⇩_α)›
2172    by (metis "≡⇩_d⇩_fE" "&E"(1) "world:1")
2173  AOT_have w_alpha_den: ‹❙w⇩_α↓›
2174    using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" by blast
2175  AOT_have ‹p ≡ ⊤❙Σp›
2176    using "q-True:3" by force
2177  moreover AOT_have ‹⊤ = ❙w⇩_α›
2178    using "T-world" by auto
2179  ultimately AOT_have ‹p ≡ ❙w⇩_α❙Σp›
2180    using "rule=E" by fast
2181  moreover AOT_have ‹❙w⇩_α ❙Σ p ≡ ❙w⇩_α ⊨ p›
2182    using lem1[unvarify x, OF w_alpha_den, THEN "→E", OF sit_w_alpha]
2183    using "≡S"(1) "≡E"(1) "Commutativity of ≡" "≡Df" sit_w_alpha "true-in-s" by blast
2184  ultimately AOT_show ‹p ≡ ❙w⇩_α ⊨ p›
2185    by (metis "≡E"(5))
2186qed
2187
2188AOT_theorem "alpha-world:1": ‹PossibleWorld(❙w⇩_α)›
2189proof -
2190  AOT_have 0: ‹❙w⇩_α = ❙ιw Actual(w)›
2191    using "pre-walpha" "rule-id-df:1[zero]" "w-alpha" by blast
2192  AOT_hence walpha_den: ‹❙w⇩_α↓›
2193    by (metis "t=t-proper:1" "vdash-properties:6")
2194  AOT_have ‹❙𝒜(PossibleWorld(❙w⇩_α) & Actual(❙w⇩_α))›
2195    by (rule "actual-desc:2"[unvarify x, OF walpha_den, THEN "→E"]) (fact 0)
2196  AOT_hence ‹❙𝒜PossibleWorld(❙w⇩_α)›
2197    by (metis "Act-Basic:2" "&E"(1) "≡E"(1))
2198  AOT_thus ‹PossibleWorld(❙w⇩_α)›
2199    using "rigid-pw:4"[unvarify x, OF walpha_den, THEN "≡E"(1)]
2200    by blast
2201qed
2202
2203AOT_theorem "alpha-world:2": ‹Maximal(❙w⇩_α)›
2204proof -
2205  AOT_have ‹❙w⇩_α↓›
2206    using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" by blast
2207  then AOT_obtain x where x_def: ‹x = ❙w⇩_α›
2208    by (metis "instantiation" "rule=I:1" "existential:1" id_sym)
2209  AOT_hence ‹PossibleWorld(x)› using "alpha-world:1" "rule=E" id_sym by fast
2210  AOT_hence ‹Maximal(x)› by (metis "world-max"[unconstrain w, THEN "→E"]) 
2211  AOT_thus ‹Maximal(❙w⇩_α)› using x_def "rule=E" by blast
2212qed
2213
2214AOT_theorem "t-at-alpha-strict": ‹❙w⇩_α ⊨ p ≡ ❙𝒜p›
2215proof -
2216  AOT_have 0: ‹❙w⇩_α = ❙ιw Actual(w)›
2217    using "pre-walpha" "rule-id-df:1[zero]" "w-alpha" by blast
2218  AOT_hence walpha_den: ‹❙w⇩_α↓›
2219    by (metis "t=t-proper:1" "vdash-properties:6")
2220  AOT_have 1: ‹❙𝒜(PossibleWorld(❙w⇩_α) & Actual(❙w⇩_α))›
2221    by (rule "actual-desc:2"[unvarify x, OF walpha_den, THEN "→E"]) (fact 0)
2222  AOT_have walpha_sit: ‹Situation(❙w⇩_α)›
2223    by (meson "≡⇩_d⇩_fE" "alpha-world:2" "&E"(1) max)
2224  {
2225    fix p
2226    AOT_have 2: ‹Situation(x) → (❙𝒜x ⊨ p ≡ x ⊨ p)› for x
2227      using "lem2:4"[unconstrain s] by blast
2228    AOT_assume ‹❙w⇩_α ⊨ p›
2229    AOT_hence θ: ‹❙𝒜❙w⇩_α ⊨ p›
2230      using 2[unvarify x, OF walpha_den, THEN "→E", OF walpha_sit, THEN "≡E"(2)]
2231      by argo
2232    AOT_have 3: ‹❙𝒜Actual(❙w⇩_α)›
2233      using "1" "Act-Basic:2" "&E"(2) "≡E"(1) by blast
2234    AOT_have ‹❙𝒜(Situation(❙w⇩_α) & ∀q(❙w⇩_α ⊨ q → q))›
2235      apply (AOT_subst (reverse) ‹Situation(❙w⇩_α) & ∀q(❙w⇩_α ⊨ q → q)› ‹Actual(❙w⇩_α)›)
2236       using actual "≡Df" apply blast
2237      by (fact 3)
2238    AOT_hence ‹❙𝒜∀q(❙w⇩_α ⊨ q → q)› by (metis "Act-Basic:2" "&E"(2) "≡E"(1))
2239    AOT_hence ‹∀q ❙𝒜(❙w⇩_α ⊨ q → q)›
2240      using "logic-actual-nec:3"[axiom_inst, THEN "≡E"(1)] by blast
2241    AOT_hence ‹❙𝒜(❙w⇩_α ⊨ p → p)› using "∀E"(2) by blast
2242    AOT_hence ‹❙𝒜(❙w⇩_α ⊨ p) → ❙𝒜p› by (metis "act-cond" "vdash-properties:10")
2243    AOT_hence ‹❙𝒜p› using θ "→E" by blast
2244  }
2245  AOT_hence 2: ‹❙w⇩_α ⊨ p → ❙𝒜p› for p by (rule "→I")
2246  AOT_have walpha_sit: ‹Situation(❙w⇩_α)›
2247    using "≡⇩_d⇩_fE" "alpha-world:2" "&E"(1) max by blast
2248  show ?thesis
2249  proof(safe intro!: "≡I" "→I" 2)
2250    AOT_assume actp: ‹❙𝒜p›
2251    AOT_show ‹❙w⇩_α ⊨ p›
2252    proof(rule "raa-cor:1")
2253      AOT_assume ‹¬❙w⇩_α ⊨ p›
2254      AOT_hence ‹❙w⇩_α ⊨ ¬p›
2255        using "alpha-world:2"[THEN max[THEN "≡⇩_d⇩_fE"], THEN "&E"(2),
2256                              THEN "∀E"(1), OF "log-prop-prop:2"]
2257        by (metis "∨E"(2))
2258      AOT_hence ‹❙𝒜¬p›
2259        using 2[unvarify p, OF "log-prop-prop:2", THEN "→E"] by blast
2260      AOT_hence ‹¬❙𝒜p› by (metis "¬¬I" "Act-Sub:1" "≡E"(4))
2261      AOT_thus ‹❙𝒜p & ¬❙𝒜p› using actp "&I" by blast
2262    qed
2263  qed
2264qed
2265
2266AOT_act_theorem "not-act": ‹w ≠ ❙w⇩_α → ¬Actual(w)›
2267proof (rule "→I"; rule "raa-cor:2")
2268  AOT_assume ‹w ≠ ❙w⇩_α›
2269  AOT_hence 0: ‹¬(w = ❙w⇩_α)› by (metis "≡⇩_d⇩_fE" "=-infix")
2270  AOT_have walpha_den: ‹❙w⇩_α↓›
2271    using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" by blast
2272  AOT_have walpha_sit: ‹Situation(❙w⇩_α)›
2273    using "≡⇩_d⇩_fE" "alpha-world:2" "&E"(1) max by blast
2274  AOT_assume act_w: ‹Actual(w)›
2275  AOT_hence w_sit: ‹Situation(w)› by (metis "≡⇩_d⇩_fE" actual "&E"(1))
2276  AOT_have sid: ‹Situation(x') → (w = x' ≡ ∀p (w ⊨ p ≡ x' ⊨ p))› for x'
2277    using "sit-identity"[unconstrain s', unconstrain s, THEN "→E", OF w_sit]
2278    by blast
2279  AOT_have ‹w = ❙w⇩_α›
2280  proof(safe intro!: GEN sid[unvarify x', OF walpha_den, THEN "→E",
2281                             OF walpha_sit, THEN "≡E"(2)] "≡I" "→I")
2282    fix p
2283    AOT_assume ‹w ⊨ p›
2284    AOT_hence ‹p›
2285      using actual[THEN "≡⇩_d⇩_fE", OF act_w, THEN "&E"(2), THEN "∀E"(2), THEN "→E"]
2286      by blast
2287    AOT_hence ‹❙𝒜p›
2288      by (metis "RA[1]")
2289    AOT_thus ‹❙w⇩_α ⊨ p›
2290      using "t-at-alpha-strict"[THEN "≡E"(2)] by blast
2291  next
2292    fix p
2293    AOT_assume ‹❙w⇩_α ⊨ p›
2294    AOT_hence ‹❙𝒜p›
2295      using "t-at-alpha-strict"[THEN "≡E"(1)] by blast
2296    AOT_hence p: ‹p›
2297      using "logic-actual"[act_axiom_inst, THEN "→E"] by blast
2298    AOT_show ‹w ⊨ p›
2299    proof(rule "raa-cor:1")
2300      AOT_assume ‹¬w ⊨ p›
2301      AOT_hence ‹w ⊨ ¬p›
2302        by (metis "coherent:1" "≡E"(2))
2303      AOT_hence ‹¬p›
2304        using actual[THEN "≡⇩_d⇩_fE", OF act_w, THEN "&E"(2), THEN "∀E"(1),
2305                     OF "log-prop-prop:2", THEN "→E"] by blast
2306      AOT_thus ‹p & ¬p› using p "&I" by blast
2307    qed
2308  qed
2309  AOT_thus ‹w = ❙w⇩_α & ¬(w = ❙w⇩_α)› using 0 "&I" by blast
2310qed
2311
2312AOT_act_theorem "w-alpha-part": ‹Actual(s) ≡ s ⊴ ❙w⇩_α›
2313proof(safe intro!: "≡I" "→I" "sit-part-whole"[THEN "≡⇩_d⇩_fI"] "&I" GEN
2314           dest!:  "sit-part-whole"[THEN "≡⇩_d⇩_fE"])
2315  AOT_show ‹Situation(s)› if ‹Actual(s)›
2316    using "≡⇩_d⇩_fE" actual "&E"(1) that by blast
2317next
2318  AOT_show ‹Situation(❙w⇩_α)›
2319    using "≡⇩_d⇩_fE" "alpha-world:2" "&E"(1) max by blast
2320next
2321  fix p
2322  AOT_assume ‹Actual(s)›
2323  moreover AOT_assume ‹s ⊨ p›
2324  ultimately AOT_have ‹p›
2325    using actual[THEN "≡⇩_d⇩_fE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"] by blast
2326  AOT_thus ‹❙w⇩_α ⊨ p›
2327     by (metis "≡E"(1) "truth-at-alpha:2")
2328next
2329  AOT_assume 0: ‹Situation(s) & Situation(❙w⇩_α) & ∀p (s ⊨ p → ❙w⇩_α ⊨ p)›
2330  AOT_hence ‹s ⊨ p → ❙w⇩_α ⊨ p› for p
2331    using "&E" "∀E"(2) by blast
2332  AOT_hence ‹s ⊨ p → p› for p
2333    by (metis "→I" "≡E"(2) "truth-at-alpha:2" "→E")
2334  AOT_hence ‹∀p (s ⊨ p → p)› by (rule GEN)
2335  AOT_thus ‹Actual(s)›
2336    using actual[THEN "≡⇩_d⇩_fI", OF "&I", OF 0[THEN "&E"(1), THEN "&E"(1)]] by blast
2337qed
2338
2339AOT_act_theorem "act-world2:1": ‹❙w⇩_α ⊨ p ≡ [λy p]❙w⇩_α›
2340  apply (AOT_subst ‹[λy p]❙w⇩_α› p)
2341   apply (rule "beta-C-meta"[THEN "→E", OF "prop-prop2:2", unvarify ν⇩₁ν⇩_n])
2342  using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" apply blast
2343  using "≡E"(2) "Commutativity of ≡" "truth-at-alpha:2" by blast
2344
2345AOT_act_theorem "act-world2:2": ‹p ≡ ❙w⇩_α ⊨ [λy p]❙w⇩_α›
2346proof -
2347  AOT_have ‹p ≡ [λy p]❙w⇩_α›
2348    apply (rule "beta-C-meta"[THEN "→E", OF "prop-prop2:2",
2349                              unvarify ν⇩₁ν⇩_n, symmetric])
2350    using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" by blast
2351  also AOT_have ‹… ≡ ❙w⇩_α ⊨ [λy p]❙w⇩_α›
2352    by (meson "log-prop-prop:2" "rule-ui:1" "truth-at-alpha:2" "universal-cor")
2353  finally show ?thesis.
2354qed
2355
2356AOT_theorem "fund-lem:1": ‹◇p → ◇∃w (w ⊨ p)›
2357proof (rule "RM◇"; rule "→I"; rule "raa-cor:1")
2358  AOT_modally_strict {
2359    AOT_obtain w where w_prop: ‹∀q (w ⊨ q ≡ q)›
2360      using "act-world:1" "PossibleWorld.∃E"[rotated] by meson
2361    AOT_assume p: ‹p›
2362    AOT_assume 0: ‹¬∃w (w ⊨ p)›
2363    AOT_have ‹∀w ¬(w ⊨ p)›
2364      apply (AOT_subst ‹PossibleWorld(x) → ¬x ⊨ p›
2365                       ‹¬(PossibleWorld(x) & x ⊨ p)› for: x)
2366      apply (metis "&I" "&E"(1) "&E"(2) "→I" "≡I" "modus-tollens:2")
2367      using "0" "cqt-further:4" "vdash-properties:10" by blast
2368    AOT_hence ‹¬(w ⊨ p)›
2369      using PossibleWorld.ψ "rule-ui:3" "→E" by blast
2370    AOT_hence ‹¬p›
2371      using w_prop[THEN "∀E"(2), THEN "≡E"(2)] 
2372      by (metis "raa-cor:3")
2373    AOT_thus ‹p & ¬p›
2374      using p "&I" by blast
2375  }
2376qed
2377
2378AOT_theorem "fund-lem:2": ‹◇∃w (w ⊨ p) → ∃w (w ⊨ p)›
2379proof (rule "→I")
2380  AOT_assume ‹◇∃w (w ⊨ p)›
2381  AOT_hence ‹∃w ◇(w ⊨ p)›
2382    using "PossibleWorld.res-var-bound-reas[BF◇]"[THEN "→E"] by auto
2383  then AOT_obtain w where ‹◇(w ⊨ p)›
2384    using "PossibleWorld.∃E"[rotated] by meson
2385  moreover AOT_have ‹Situation(w)›
2386    by (metis "≡⇩_d⇩_fE" "&E"(1) pos "world-pos")
2387  ultimately AOT_have ‹w ⊨ p›
2388    using "lem2:2"[unconstrain s, THEN "→E"]  "≡E" by blast
2389  AOT_thus ‹∃w w ⊨ p›
2390    by (rule "PossibleWorld.∃I")
2391qed
2392
2393AOT_theorem "fund-lem:3": ‹p → ∀s(∀q (s ⊨ q ≡ q) → s ⊨ p)›
2394proof(safe intro!: "→I" Situation.GEN)
2395  fix s
2396  AOT_assume ‹p›
2397  moreover AOT_assume ‹∀q (s ⊨ q ≡ q)›
2398  ultimately AOT_show ‹s ⊨ p›
2399    using "∀E"(2) "≡E"(2) by blast
2400qed
2401
2402AOT_theorem "fund-lem:4": ‹□p → □∀s(∀q (s ⊨ q ≡ q) → s ⊨ p)›
2403  using "fund-lem:3" by (rule RM)
2404
2405AOT_theorem "fund-lem:5": ‹□∀s φ{s} → ∀s □φ{s}›
2406proof(safe intro!: "→I" Situation.GEN)
2407  fix s
2408  AOT_assume ‹□∀s φ{s}›
2409  AOT_hence ‹∀s □φ{s}›
2410    using "Situation.res-var-bound-reas[CBF]"[THEN "→E"] by blast
2411  AOT_thus ‹□φ{s}›
2412    using "Situation.∀E" by fast
2413qed
2414
2415text‹Note: not explicit in PLM.›
2416AOT_theorem "fund-lem:5[world]": ‹□∀w φ{w} → ∀w □φ{w}›
2417proof(safe intro!: "→I" PossibleWorld.GEN)
2418  fix w
2419  AOT_assume ‹□∀w φ{w}›
2420  AOT_hence ‹∀w □φ{w}›
2421    using "PossibleWorld.res-var-bound-reas[CBF]"[THEN "→E"] by blast
2422  AOT_thus ‹□φ{w}›
2423    using "PossibleWorld.∀E" by fast
2424qed
2425
2426AOT_theorem "fund-lem:6": ‹∀w w ⊨ p → □∀w w ⊨ p›
2427proof(rule "→I")
2428  AOT_assume ‹∀w (w ⊨ p)›
2429  AOT_hence 1: ‹PossibleWorld(w) → (w ⊨ p)› for w
2430    using "∀E"(2) by blast
2431  AOT_show ‹□∀w w ⊨ p›
2432  proof(rule "raa-cor:1")
2433    AOT_assume ‹¬□∀w w ⊨ p›
2434    AOT_hence ‹◇¬∀w w ⊨ p›
2435      by (metis "KBasic:11" "≡E"(1))
2436    AOT_hence ‹◇∃x (¬(PossibleWorld(x) → x ⊨ p))›
2437      apply (rule "RM◇"[THEN "→E", rotated])
2438      by (simp add: "cqt-further:2")
2439    AOT_hence ‹∃x ◇(¬(PossibleWorld(x) → x ⊨ p))›
2440      by (metis "BF◇" "vdash-properties:10")
2441    then AOT_obtain x where x_prop: ‹◇¬(PossibleWorld(x) → x ⊨ p)›
2442      using "∃E"[rotated] by blast
2443    AOT_have ‹◇(PossibleWorld(x) & ¬x ⊨ p)›
2444      apply (AOT_subst ‹PossibleWorld(x) & ¬x ⊨ p›
2445                       ‹¬(PossibleWorld(x) → x ⊨ p)›)
2446       apply (meson "≡E"(6) "oth-class-taut:1:b" "oth-class-taut:3:a")
2447      by(fact x_prop)
2448    AOT_hence 2: ‹◇PossibleWorld(x) & ◇¬x ⊨ p›
2449      by (metis "KBasic2:3" "vdash-properties:10")
2450    AOT_hence ‹PossibleWorld(x)›
2451      using "&E"(1) "≡E"(1) "rigid-pw:2" by blast
2452    AOT_hence ‹□(x ⊨ p)›
2453      using 2[THEN "&E"(2)]  1[unconstrain w, THEN "→E"] "→E"
2454            "rigid-truth-at:1"[unconstrain w, THEN "→E"]
2455      by (metis "≡E"(1))
2456    moreover AOT_have ‹¬□(x ⊨ p)›
2457      using 2[THEN "&E"(2)] by (metis "¬¬I" "KBasic:12" "≡E"(4))
2458    ultimately AOT_show ‹p & ¬p› for p
2459      by (metis "raa-cor:3")
2460  qed
2461qed
2462
2463AOT_theorem "fund-lem:7": ‹□∀w(w ⊨ p) → □p›
2464proof(rule RM; rule "→I")
2465  AOT_modally_strict {
2466    AOT_obtain w where w_prop: ‹∀p (w ⊨ p ≡ p)›
2467      using "act-world:1" "PossibleWorld.∃E"[rotated] by meson
2468    AOT_assume ‹∀w (w ⊨ p)›
2469    AOT_hence ‹w ⊨ p›
2470      using "PossibleWorld.∀E" by fast
2471    AOT_thus ‹p›
2472      using w_prop[THEN "∀E"(2), THEN "≡E"(1)] by blast
2473  }
2474qed
2475
2476AOT_theorem "fund:1": ‹◇p ≡ ∃w w ⊨ p›
2477proof (rule "≡I"; rule "→I")
2478  AOT_assume ‹◇p›
2479  AOT_thus ‹∃w w ⊨ p›
2480    by (metis "fund-lem:1" "fund-lem:2" "→E")
2481next
2482  AOT_assume ‹∃w w ⊨ p›
2483  then AOT_obtain w where w_prop: ‹w ⊨ p›
2484    using "PossibleWorld.∃E"[rotated] by meson
2485  AOT_hence ‹◇∀p (w ⊨ p ≡ p)›
2486    using "world:1"[THEN "≡⇩_d⇩_fE", THEN "&E"(2)] PossibleWorld.ψ "&E" by blast
2487  AOT_hence ‹∀p ◇(w ⊨ p ≡ p)›
2488    by (metis "Buridan◇" "→E")
2489  AOT_hence 1: ‹◇(w ⊨ p ≡ p)›
2490    by (metis "log-prop-prop:2" "rule-ui:1")
2491  AOT_have ‹◇((w ⊨ p → p) & (p → w ⊨ p))›
2492    apply (AOT_subst ‹(w ⊨ p → p) & (p → w ⊨ p)› ‹w ⊨ p ≡ p›)
2493     apply (meson "conventions:3" "≡E"(6) "oth-class-taut:3:a" "≡Df")
2494    by (fact 1)
2495  AOT_hence ‹◇(w ⊨ p → p)›
2496    by (metis "RM◇" "Conjunction Simplification"(1) "→E")
2497  moreover AOT_have ‹□(w ⊨ p)›
2498    using w_prop by (metis "≡E"(1) "rigid-truth-at:1")
2499  ultimately AOT_show ‹◇p›
2500    by (metis "KBasic2:4" "≡E"(1) "→E")
2501qed
2502
2503AOT_theorem "fund:2": ‹□p ≡ ∀w (w ⊨ p)›
2504proof -
2505  AOT_have 0: ‹∀w (w ⊨ ¬p ≡ ¬w ⊨ p)›
2506    apply (rule PossibleWorld.GEN)
2507    using "coherent:1" by blast
2508  AOT_have ‹◇¬p ≡ ∃w (w ⊨ ¬p)›
2509    using "fund:1"[unvarify p, OF "log-prop-prop:2"] by blast
2510  also AOT_have ‹… ≡ ∃w ¬(w ⊨ p)›
2511  proof(safe intro!: "≡I" "→I")
2512    AOT_assume ‹∃w w ⊨ ¬p›
2513    then AOT_obtain w where w_prop: ‹w ⊨ ¬p›
2514      using "PossibleWorld.∃E"[rotated] by meson
2515    AOT_hence ‹¬w ⊨ p›
2516      using 0[THEN "PossibleWorld.∀E", THEN "≡E"(1)] "&E" by blast
2517    AOT_thus ‹∃w ¬w ⊨ p›
2518      by (rule "PossibleWorld.∃I")
2519  next
2520    AOT_assume ‹∃w ¬w ⊨ p›
2521    then AOT_obtain w where w_prop: ‹¬w ⊨ p›
2522      using "PossibleWorld.∃E"[rotated] by meson
2523    AOT_hence ‹w ⊨ ¬p›
2524      using 0[THEN "∀E"(2), THEN "→E", THEN "≡E"(1)] "&E"
2525      by (metis "coherent:1" "≡E"(2))
2526    AOT_thus ‹∃w w ⊨ ¬p›
2527      by (rule "PossibleWorld.∃I")
2528  qed
2529  finally AOT_have ‹¬◇¬p ≡ ¬∃w ¬w ⊨ p›
2530    by (meson "≡E"(1) "oth-class-taut:4:b")
2531  AOT_hence ‹□p ≡ ¬∃w ¬w ⊨ p›
2532    by (metis "KBasic:12" "≡E"(5))
2533  also AOT_have ‹… ≡ ∀w w ⊨ p›
2534  proof(safe intro!: "≡I" "→I")
2535    AOT_assume ‹¬∃w ¬w ⊨ p›
2536    AOT_hence 0: ‹∀x (¬(PossibleWorld(x) & ¬x ⊨ p))›
2537      by (metis "cqt-further:4" "→E")
2538    AOT_show ‹∀w w ⊨ p›
2539      apply (AOT_subst ‹PossibleWorld(x) → x ⊨ p›
2540                       ‹¬(PossibleWorld(x) & ¬x ⊨ p)› for: x)
2541       using "oth-class-taut:1:a" apply presburger
2542      by (fact 0)
2543  next
2544    AOT_assume 0: ‹∀w w ⊨ p›
2545    AOT_have ‹∀x (¬(PossibleWorld(x) & ¬x ⊨ p))›
2546      by (AOT_subst (reverse) ‹¬(PossibleWorld(x) & ¬x ⊨ p)›
2547                              ‹PossibleWorld(x) → x ⊨ p› for: x)
2548         (auto simp: "oth-class-taut:1:a" 0)
2549    AOT_thus ‹¬∃w ¬w ⊨ p›
2550      by (metis "∃E" "raa-cor:3" "rule-ui:3")
2551  qed
2552  finally AOT_show ‹□p ≡ ∀w w ⊨ p›.
2553qed
2554
2555AOT_theorem "fund:3": ‹¬◇p ≡ ¬∃w w ⊨ p›
2556  by (metis (full_types) "contraposition:1[1]" "→I" "fund:1" "≡I" "≡E"(1,2))
2557
2558AOT_theorem "fund:4": ‹¬□p ≡ ∃w ¬w ⊨p›
2559  apply (AOT_subst ‹∃w ¬w ⊨ p› ‹¬ ∀w w ⊨ p›)
2560   apply (AOT_subst ‹PossibleWorld(x) → x ⊨ p›
2561                    ‹¬(PossibleWorld(x) & ¬x ⊨ p)› for: x)
2562  by (auto simp add: "oth-class-taut:1:a" "conventions:4" "≡Df" RN
2563                     "fund:2" "rule-sub-lem:1:a")
2564
2565AOT_theorem "nec-dia-w:1": ‹□p ≡ ∃w w ⊨ □p›
2566proof -
2567  AOT_have ‹□p ≡ ◇□p›
2568    using "S5Basic:2" by blast
2569  also AOT_have ‹... ≡ ∃w w ⊨ □p›
2570    using "fund:1"[unvarify p, OF "log-prop-prop:2"] by blast
2571  finally show ?thesis.
2572qed
2573
2574AOT_theorem "nec-dia-w:2": ‹□p ≡ ∀w w ⊨ □p›
2575proof -
2576  AOT_have ‹□p ≡ □□p›
2577    using 4 "qml:2"[axiom_inst] "≡I" by blast
2578  also AOT_have ‹... ≡ ∀w w ⊨ □p›
2579    using "fund:2"[unvarify p, OF "log-prop-prop:2"] by blast
2580  finally show ?thesis.
2581qed
2582
2583AOT_theorem "nec-dia-w:3": ‹◇p ≡ ∃w w ⊨ ◇p›
2584proof -
2585  AOT_have ‹◇p ≡ ◇◇p›
2586    by (simp add: "4◇" "T◇" "≡I")
2587  also AOT_have ‹... ≡ ∃w w ⊨ ◇p›
2588    using "fund:1"[unvarify p, OF "log-prop-prop:2"] by blast
2589  finally show ?thesis.
2590qed
2591
2592AOT_theorem "nec-dia-w:4": ‹◇p ≡ ∀w w ⊨ ◇p›
2593proof -
2594  AOT_have ‹◇p ≡ □◇p›
2595    by (simp add: "S5Basic:1")
2596  also AOT_have ‹... ≡ ∀w w ⊨ ◇p›
2597    using "fund:2"[unvarify p, OF "log-prop-prop:2"] by blast
2598  finally show ?thesis.
2599qed
2600
2601AOT_theorem "conj-dist-w:1": ‹w ⊨ (p & q) ≡ ((w ⊨ p) & (w ⊨ q))›
2602proof(safe intro!: "≡I" "→I")
2603  AOT_assume ‹w ⊨ (p & q)›
2604  AOT_hence 0: ‹□w ⊨ (p & q)›
2605    using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2606    by blast
2607  AOT_modally_strict {
2608    AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (φ & ψ)) → (w ⊨ φ & w ⊨ ψ))› for w φ ψ
2609    proof(safe intro!: "→I")
2610      AOT_assume ‹∀ p (w ⊨ p ≡ p)›
2611      AOT_hence ‹w ⊨ (φ & ψ) ≡ (φ & ψ)› and ‹w ⊨ φ ≡ φ› and ‹w ⊨ ψ ≡ ψ›
2612        using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
2613      moreover AOT_assume ‹w ⊨ (φ & ψ)›
2614      ultimately AOT_show ‹w ⊨ φ & w ⊨ ψ›
2615        by (metis "&I" "&E"(1) "&E"(2) "≡E"(1) "≡E"(2))
2616    qed
2617  }
2618  AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇(w ⊨ (φ & ψ) → w ⊨ φ & w ⊨ ψ)› for w φ ψ
2619    by (rule "RM◇")
2620  moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2621    using "world:1"[THEN "≡⇩_d⇩_fE", OF PossibleWorld.ψ] "&E" by blast
2622  ultimately AOT_have ‹◇(w ⊨ (p & q) → w ⊨ p & w ⊨ q)› using "→E" by blast
2623  AOT_hence ‹◇(w ⊨ p) & ◇(w ⊨ q)›
2624    by (metis 0 "KBasic2:3" "KBasic2:4" "≡E"(1) "vdash-properties:10")
2625  AOT_thus ‹w ⊨ p & w ⊨ q›
2626    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2627          "&E" "&I" by meson
2628next
2629  AOT_assume ‹w ⊨ p & w ⊨ q›
2630  AOT_hence ‹□w ⊨ p & □w ⊨ q›
2631    using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2632          "&E" "&I" by blast
2633  AOT_hence 0: ‹□(w ⊨ p & w ⊨ q)›
2634    by (metis "KBasic:3" "≡E"(2))
2635  AOT_modally_strict {
2636    AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ φ & w ⊨ ψ) → (w ⊨ (φ & ψ)))› for w φ ψ
2637    proof(safe intro!: "→I")
2638      AOT_assume ‹∀ p (w ⊨ p ≡ p)›
2639      AOT_hence ‹w ⊨ (φ & ψ) ≡ (φ & ψ)› and ‹w ⊨ φ ≡ φ› and ‹w ⊨ ψ ≡ ψ›
2640        using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
2641      moreover AOT_assume ‹w ⊨ φ & w ⊨ ψ›
2642      ultimately AOT_show ‹w ⊨ (φ & ψ)›
2643        by (metis "&I" "&E"(1) "&E"(2) "≡E"(1) "≡E"(2))
2644    qed
2645  }
2646  AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇((w ⊨ φ & w ⊨ ψ) → w ⊨ (φ & ψ))› for w φ ψ
2647    by (rule "RM◇")
2648  moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2649    using "world:1"[THEN "≡⇩_d⇩_fE", OF PossibleWorld.ψ] "&E" by blast
2650  ultimately AOT_have ‹◇((w ⊨ p & w ⊨ q) → w ⊨ (p & q))›
2651    using "→E" by blast
2652  AOT_hence ‹◇(w ⊨ (p & q))›
2653    by (metis 0 "KBasic2:4" "≡E"(1) "vdash-properties:10")
2654  AOT_thus ‹w ⊨ (p & q)›
2655    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2656    by blast
2657qed
2658
2659AOT_theorem "conj-dist-w:2": ‹w ⊨ (p → q) ≡ ((w ⊨ p) → (w ⊨ q))›
2660proof(safe intro!: "≡I" "→I")
2661  AOT_assume ‹w ⊨ (p → q)›
2662  AOT_hence 0: ‹□w ⊨ (p → q)›
2663    using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2664    by blast
2665  AOT_assume ‹w ⊨ p›
2666  AOT_hence 1: ‹□w ⊨ p›
2667    by (metis "T◇" "≡E"(1) "rigid-truth-at:3" "→E")
2668  AOT_modally_strict {
2669    AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (φ → ψ)) → (w ⊨ φ → w ⊨ ψ))› for w φ ψ
2670    proof(safe intro!: "→I")
2671      AOT_assume ‹∀ p (w ⊨ p ≡ p)›
2672      AOT_hence ‹w ⊨ (φ → ψ) ≡ (φ → ψ)› and ‹w ⊨ φ ≡ φ› and ‹w ⊨ ψ ≡ ψ›
2673        using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
2674      moreover AOT_assume ‹w ⊨ (φ → ψ)›
2675      moreover AOT_assume ‹w ⊨ φ›
2676      ultimately AOT_show ‹w ⊨ ψ›
2677        by (metis "≡E"(1) "≡E"(2) "→E")
2678    qed
2679  }
2680  AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇(w ⊨ (φ → ψ) → (w ⊨ φ → w ⊨ ψ))› for w φ ψ
2681    by (rule "RM◇")
2682  moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2683    using "world:1"[THEN "≡⇩_d⇩_fE", OF PossibleWorld.ψ] "&E" by blast
2684  ultimately AOT_have ‹◇(w ⊨ (p → q) → (w ⊨ p → w ⊨ q))›
2685    using "→E" by blast
2686  AOT_hence ‹◇(w ⊨ p → w ⊨ q)›
2687    by (metis 0 "KBasic2:4" "≡E"(1) "→E")
2688  AOT_hence ‹◇w ⊨ q› 
2689    by (metis 1 "KBasic2:4" "≡E"(1) "→E")
2690  AOT_thus ‹w ⊨ q›
2691    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2692          "&E" "&I" by meson
2693next
2694  AOT_assume ‹w ⊨ p → w ⊨ q›
2695  AOT_hence ‹¬(w ⊨ p) ∨ w ⊨ q›
2696    by (metis "∨I"(1) "∨I"(2) "reductio-aa:1" "→E")
2697  AOT_hence ‹w ⊨ ¬p ∨ w ⊨ q›
2698    by (metis "coherent:1" "∨I"(1) "∨I"(2) "∨E"(2) "≡E"(2) "reductio-aa:1")
2699  AOT_hence 0: ‹□(w ⊨ ¬p ∨ w ⊨ q)›
2700    using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2701    by (metis "KBasic:15" "∨I"(1) "∨I"(2) "∨E"(2) "reductio-aa:1" "→E")
2702  AOT_modally_strict {
2703    AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ ¬φ ∨ w ⊨ ψ) → (w ⊨ (φ → ψ)))› for w φ ψ
2704    proof(safe intro!: "→I")
2705      AOT_assume ‹∀ p (w ⊨ p ≡ p)›
2706      moreover AOT_assume ‹w ⊨ ¬φ ∨ w ⊨ ψ›
2707      ultimately AOT_show ‹w ⊨ (φ → ψ)›
2708        by (metis "∨E"(2) "→I" "≡E"(1) "≡E"(2) "log-prop-prop:2"
2709                  "reductio-aa:1" "rule-ui:1")
2710    qed
2711  }
2712  AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇((w ⊨ ¬φ ∨ w ⊨ ψ) → w ⊨ (φ → ψ))› for w φ ψ
2713    by (rule "RM◇")
2714  moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2715    using "world:1"[THEN "≡⇩_d⇩_fE", OF PossibleWorld.ψ] "&E" by blast
2716  ultimately AOT_have ‹◇((w ⊨ ¬p ∨ w ⊨ q) → w ⊨ (p → q))›
2717    using "→E" by blast
2718  AOT_hence ‹◇(w ⊨ (p → q))›
2719    by (metis 0 "KBasic2:4" "≡E"(1) "→E")
2720  AOT_thus ‹w ⊨ (p → q)›
2721    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2722    by blast
2723qed
2724
2725AOT_theorem "conj-dist-w:3": ‹w ⊨ (p ∨ q) ≡ ((w ⊨ p) ∨ (w ⊨ q))›
2726proof(safe intro!: "≡I" "→I")
2727  AOT_assume ‹w ⊨ (p ∨ q)›
2728  AOT_hence 0: ‹□w ⊨ (p ∨ q)›
2729    using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2730    by blast
2731  AOT_modally_strict {
2732    AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (φ ∨ ψ)) → (w ⊨ φ ∨ w ⊨ ψ))› for w φ ψ
2733    proof(safe intro!: "→I")
2734      AOT_assume ‹∀ p (w ⊨ p ≡ p)›
2735      AOT_hence ‹w ⊨ (φ ∨ ψ) ≡ (φ ∨ ψ)› and ‹w ⊨ φ ≡ φ› and ‹w ⊨ ψ ≡ ψ›
2736        using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
2737      moreover AOT_assume ‹w ⊨ (φ ∨ ψ)›
2738      ultimately AOT_show ‹w ⊨ φ ∨ w ⊨ ψ›
2739        by (metis "∨I"(1) "∨I"(2) "∨E"(3) "≡E"(1) "≡E"(2) "reductio-aa:1")
2740    qed
2741  }
2742  AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇(w ⊨ (φ ∨ ψ) → (w ⊨ φ ∨ w ⊨ ψ))› for w φ ψ
2743    by (rule "RM◇")
2744  moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2745    using "world:1"[THEN "≡⇩_d⇩_fE", OF PossibleWorld.ψ] "&E" by blast
2746  ultimately AOT_have ‹◇(w ⊨ (p ∨ q) → (w ⊨ p ∨ w ⊨ q))› using "→E" by blast
2747  AOT_hence ‹◇(w ⊨ p ∨ w ⊨ q)›
2748    by (metis 0 "KBasic2:4" "≡E"(1) "vdash-properties:10")
2749  AOT_hence ‹◇w ⊨ p ∨ ◇w ⊨ q›
2750    using "KBasic2:2"[THEN "≡E"(1)] by blast
2751  AOT_thus ‹w ⊨ p ∨ w ⊨ q›
2752    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2753    by (metis "∨I"(1) "∨I"(2) "∨E"(2) "reductio-aa:1")
2754next
2755  AOT_assume ‹w ⊨ p ∨ w ⊨ q›
2756  AOT_hence 0: ‹□(w ⊨ p ∨ w ⊨ q)›
2757    using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2758    by (metis "KBasic:15" "∨I"(1) "∨I"(2) "∨E"(2) "reductio-aa:1" "→E")
2759  AOT_modally_strict {
2760    AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ φ ∨ w ⊨ ψ) → (w ⊨ (φ ∨ ψ)))› for w φ ψ
2761    proof(safe intro!: "→I")
2762      AOT_assume ‹∀ p (w ⊨ p ≡ p)›
2763      moreover AOT_assume ‹w ⊨ φ ∨ w ⊨ ψ›
2764      ultimately AOT_show ‹w ⊨ (φ ∨ ψ)›
2765        by (metis "∨I"(1) "∨I"(2) "∨E"(2) "≡E"(1) "≡E"(2)
2766                  "log-prop-prop:2" "reductio-aa:1" "rule-ui:1")
2767    qed
2768  }
2769  AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇((w ⊨ φ ∨ w ⊨ ψ) → w ⊨ (φ ∨ ψ))› for w φ ψ
2770    by (rule "RM◇")
2771  moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2772    using "world:1"[THEN "≡⇩_d⇩_fE", OF PossibleWorld.ψ] "&E" by blast
2773  ultimately AOT_have ‹◇((w ⊨ p ∨ w ⊨ q) → w ⊨ (p ∨ q))›
2774    using "→E" by blast
2775  AOT_hence ‹◇(w ⊨ (p ∨ q))›
2776    by (metis 0 "KBasic2:4" "≡E"(1) "→E")
2777  AOT_thus ‹w ⊨ (p ∨ q)›
2778    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2779    by blast
2780qed
2781
2782AOT_theorem "conj-dist-w:4": ‹w ⊨ (p ≡ q) ≡ ((w ⊨ p) ≡ (w ⊨ q))›
2783proof(rule "≡I"; rule "→I")
2784  AOT_assume ‹w ⊨ (p ≡ q)›
2785  AOT_hence 0: ‹□w ⊨ (p ≡ q)›
2786    using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2787    by blast
2788  AOT_modally_strict {
2789    AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (φ ≡ ψ)) → (w ⊨ φ ≡ w ⊨ ψ))› for w φ ψ
2790    proof(safe intro!: "→I")
2791      AOT_assume ‹∀ p (w ⊨ p ≡ p)›
2792      AOT_hence ‹w ⊨ (φ ≡ ψ) ≡ (φ ≡ ψ)› and ‹w ⊨ φ ≡ φ› and ‹w ⊨ ψ ≡ ψ›
2793        using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
2794      moreover AOT_assume ‹w ⊨ (φ ≡ ψ)›
2795      ultimately AOT_show ‹w ⊨ φ ≡ w ⊨ ψ›
2796        by (metis "≡E"(2) "≡E"(5) "Commutativity of ≡")
2797    qed
2798  }
2799  AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇(w ⊨ (φ ≡ ψ) → (w ⊨ φ ≡ w ⊨ ψ))› for w φ ψ
2800    by (rule "RM◇")
2801  moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2802    using "world:1"[THEN "≡⇩_d⇩_fE", OF PossibleWorld.ψ] "&E" by blast
2803  ultimately AOT_have ‹◇(w ⊨ (p ≡ q) → (w ⊨ p ≡ w ⊨ q))›
2804    using "→E" by blast
2805  AOT_hence 1: ‹◇(w ⊨ p ≡ w ⊨ q)›
2806    by (metis 0 "KBasic2:4" "≡E"(1) "vdash-properties:10")
2807  AOT_have ‹◇((w ⊨ p → w ⊨ q) & (w ⊨ q → w ⊨ p))›
2808    apply (AOT_subst ‹(w ⊨ p → w ⊨ q) & (w ⊨ q → w ⊨ p)› ‹w ⊨ p ≡ w ⊨ q›)
2809     apply (meson "≡⇩_d⇩_fE" "conventions:3" "→I" "df-rules-formulas[4]" "≡I")
2810    by (fact 1)
2811  AOT_hence 2: ‹◇(w ⊨ p → w ⊨ q) & ◇(w ⊨ q → w ⊨ p)›
2812    by (metis "KBasic2:3" "vdash-properties:10")
2813  AOT_have ‹◇(¬w ⊨ p ∨ w ⊨ q)› and ‹◇(¬w ⊨ q ∨ w ⊨ p)›
2814     apply (AOT_subst (reverse) ‹¬w ⊨ p ∨ w ⊨ q› ‹w ⊨ p → w ⊨ q›)
2815      apply (simp add: "oth-class-taut:1:c")
2816     apply (fact 2[THEN "&E"(1)])
2817    apply (AOT_subst (reverse) ‹¬w ⊨ q ∨ w ⊨ p› ‹w ⊨ q → w ⊨ p›)
2818     apply (simp add: "oth-class-taut:1:c")
2819    by (fact 2[THEN "&E"(2)])
2820  AOT_hence ‹◇(¬w ⊨ p) ∨ ◇w ⊨ q› and ‹◇¬w ⊨ q ∨ ◇w ⊨ p›
2821    using "KBasic2:2" "≡E"(1) by blast+
2822  AOT_hence ‹¬□w ⊨ p ∨ ◇w ⊨ q› and ‹¬□w ⊨ q ∨ ◇w ⊨ p›
2823    by (metis "KBasic:11" "∨I"(1) "∨I"(2) "∨E"(2) "≡E"(2) "raa-cor:1")+
2824  AOT_thus ‹w ⊨ p ≡ w ⊨ q›
2825    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2826    by (metis "¬¬I" "T◇" "∨E"(2) "→I" "≡I" "≡E"(1) "rigid-truth-at:3")
2827next
2828  AOT_have ‹□PossibleWorld(w)›
2829    using "≡E"(1) "rigid-pw:1" PossibleWorld.ψ by blast
2830  moreover {
2831    fix p
2832    AOT_modally_strict {
2833      AOT_have ‹PossibleWorld(w) → (w ⊨ p → □w ⊨ p)›
2834        using "rigid-truth-at:1" "→I"
2835        by (metis "≡E"(1))
2836    }
2837    AOT_hence ‹□PossibleWorld(w) → □(w ⊨ p → □w ⊨ p)›
2838      by (rule RM)
2839  }
2840  ultimately AOT_have 1: ‹□(w ⊨ p → □w ⊨ p)› for p
2841    by (metis "→E")
2842  AOT_assume ‹w ⊨ p ≡ w ⊨ q›
2843  AOT_hence 0: ‹□(w ⊨ p ≡ w ⊨ q)›
2844    using "sc-eq-box-box:5"[THEN "→E", THEN "qml:2"[axiom_inst, THEN "→E"],
2845                            THEN "→E", OF "&I"]
2846          by (metis "1")
2847  AOT_modally_strict {
2848    AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ φ ≡ w ⊨ ψ) → (w ⊨ (φ ≡ ψ)))› for w φ ψ
2849    proof(safe intro!: "→I")
2850      AOT_assume ‹∀ p (w ⊨ p ≡ p)›
2851      moreover AOT_assume ‹w ⊨ φ ≡ w ⊨ ψ›
2852      ultimately AOT_show ‹w ⊨ (φ ≡ ψ)›
2853        by (metis "≡E"(2) "≡E"(6) "log-prop-prop:2" "rule-ui:1")
2854    qed
2855  }
2856  AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇((w ⊨ φ ≡ w ⊨ ψ) → w ⊨ (φ ≡ ψ))› for w φ ψ
2857    by (rule "RM◇")
2858  moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2859    using "world:1"[THEN "≡⇩_d⇩_fE", OF PossibleWorld.ψ] "&E" by blast
2860  ultimately AOT_have ‹◇((w ⊨ p ≡  w ⊨ q) → w ⊨ (p ≡ q))›
2861    using "→E" by blast
2862  AOT_hence ‹◇(w ⊨ (p ≡ q))›
2863    by (metis 0 "KBasic2:4" "≡E"(1) "→E")
2864  AOT_thus ‹w ⊨ (p ≡ q)›
2865    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2866    by blast
2867qed
2868
2869AOT_theorem "conj-dist-w:5": ‹w ⊨ (∀α φ{α}) ≡ (∀ α (w ⊨ φ{α}))›
2870proof(safe intro!: "≡I" "→I" GEN)
2871  AOT_assume ‹w ⊨ (∀α φ{α})›
2872  AOT_hence 0: ‹□w ⊨ (∀α φ{α})›
2873    using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2874    by blast
2875  AOT_modally_strict {
2876    AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (∀α φ{α})) → (∀α w ⊨ φ{α}))› for w
2877    proof(safe intro!: "→I" GEN)
2878      AOT_assume ‹∀p (w ⊨ p ≡ p)›
2879      moreover AOT_assume ‹w ⊨ (∀α φ{α})›
2880      ultimately AOT_show ‹w ⊨ φ{α}› for α
2881        by (metis "≡E"(1) "≡E"(2) "log-prop-prop:2" "rule-ui:1" "rule-ui:3")
2882    qed
2883  }
2884  AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇(w ⊨ (∀α φ{α}) → (∀α w ⊨ φ{α}))› for w
2885    by (rule "RM◇")
2886  moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2887    using "world:1"[THEN "≡⇩_d⇩_fE", OF PossibleWorld.ψ] "&E" by blast
2888  ultimately AOT_have ‹◇(w ⊨ (∀α φ{α}) → (∀α w ⊨ φ{α}))› using "→E" by blast
2889  AOT_hence ‹◇(∀α w ⊨ φ{α})›
2890    by (metis 0 "KBasic2:4" "≡E"(1) "→E")
2891  AOT_hence ‹∀α ◇w ⊨ φ{α}›
2892    by (metis "Buridan◇" "→E")
2893  AOT_thus ‹w ⊨ φ{α}› for α
2894    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2895          "∀E"(2) by blast
2896next
2897  AOT_assume ‹∀α w ⊨ φ{α}›
2898  AOT_hence ‹w ⊨ φ{α}› for α using "∀E"(2) by blast
2899  AOT_hence ‹□w ⊨ φ{α}› for α
2900    using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2901          "&E" "&I" by blast
2902  AOT_hence ‹∀α □w ⊨ φ{α}› by (rule GEN)
2903  AOT_hence 0: ‹□∀α w ⊨ φ{α}› by (rule BF[THEN "→E"])
2904  AOT_modally_strict {
2905    AOT_have ‹∀p (w ⊨ p ≡ p) → ((∀α w ⊨ φ{α}) → (w ⊨ (∀α φ{α})))› for w
2906    proof(safe intro!: "→I")
2907      AOT_assume ‹∀ p (w ⊨ p ≡ p)›
2908      moreover AOT_assume ‹∀α w ⊨ φ{α}›
2909      ultimately AOT_show ‹w ⊨ (∀α φ{α})›
2910        by (metis "≡E"(1) "≡E"(2) "log-prop-prop:2" "rule-ui:1"
2911                  "rule-ui:3" "universal-cor")
2912    qed
2913  }
2914  AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇((∀α w ⊨ φ{α}) → w ⊨ (∀α φ{α}))› for w
2915    by (rule "RM◇")
2916  moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2917    using "world:1"[THEN "≡⇩_d⇩_fE", OF PossibleWorld.ψ] "&E" by blast
2918  ultimately AOT_have ‹◇((∀α w ⊨ φ{α}) → w ⊨ (∀α φ{α}))›
2919    using "→E" by blast
2920  AOT_hence ‹◇(w ⊨ (∀α φ{α}))›
2921    by (metis 0 "KBasic2:4" "≡E"(1) "→E")
2922  AOT_thus ‹w ⊨ (∀α φ{α})›
2923    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2924    by blast
2925qed
2926
2927AOT_theorem "conj-dist-w:6": ‹w ⊨ (∃α φ{α}) ≡ (∃ α (w ⊨ φ{α}))›
2928proof(safe intro!: "≡I" "→I" GEN)
2929  AOT_assume ‹w ⊨ (∃α φ{α})›
2930  AOT_hence 0: ‹□w ⊨ (∃α φ{α})›
2931    using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2932    by blast
2933  AOT_modally_strict {
2934    AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (∃α φ{α})) → (∃α w ⊨ φ{α}))› for w
2935    proof(safe intro!: "→I" GEN)
2936      AOT_assume ‹∀p (w ⊨ p ≡ p)›
2937      moreover AOT_assume ‹w ⊨ (∃α φ{α})›
2938      ultimately AOT_show ‹∃ α (w ⊨ φ{α})›
2939        by (metis "∃E" "∃I"(2) "≡E"(1,2) "log-prop-prop:2" "rule-ui:1") 
2940    qed
2941  }
2942  AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇(w ⊨ (∃α φ{α}) → (∃α w ⊨ φ{α}))› for w
2943    by (rule "RM◇")
2944  moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2945    using "world:1"[THEN "≡⇩_d⇩_fE", OF PossibleWorld.ψ] "&E" by blast
2946  ultimately AOT_have ‹◇(w ⊨ (∃α φ{α}) → (∃α w ⊨ φ{α}))› using "→E" by blast
2947  AOT_hence ‹◇(∃α w ⊨ φ{α})›
2948    by (metis 0 "KBasic2:4" "≡E"(1) "→E")
2949  AOT_hence ‹∃α ◇w ⊨ φ{α}›
2950    by (metis "BF◇" "→E")
2951  then AOT_obtain α where ‹◇w ⊨ φ{α}›
2952    using "∃E"[rotated] by blast
2953  AOT_hence ‹w ⊨ φ{α}›
2954    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"] by blast
2955  AOT_thus ‹∃ α w ⊨ φ{α}› by (rule "∃I")
2956next
2957  AOT_assume ‹∃α w ⊨ φ{α}›
2958  then AOT_obtain α where ‹w ⊨ φ{α}› using "∃E"[rotated] by blast
2959  AOT_hence ‹□w ⊨ φ{α}›
2960    using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2961          "&E" "&I" by blast
2962  AOT_hence ‹∃α □w ⊨ φ{α}›
2963    by (rule "∃I")
2964  AOT_hence 0: ‹□∃α w ⊨ φ{α}›
2965    by (metis Buridan "→E")
2966  AOT_modally_strict {
2967    AOT_have ‹∀p (w ⊨ p ≡ p) → ((∃α w ⊨ φ{α}) → (w ⊨ (∃α φ{α})))› for w
2968    proof(safe intro!: "→I")
2969      AOT_assume ‹∀ p (w ⊨ p ≡ p)›
2970      moreover AOT_assume ‹∃α w ⊨ φ{α}›
2971      then AOT_obtain α where ‹w ⊨ φ{α}›
2972        using "∃E"[rotated] by blast
2973      ultimately AOT_show ‹w ⊨ (∃α φ{α})›
2974        by (metis "∃I"(2) "≡E"(1,2) "log-prop-prop:2" "rule-ui:1")
2975    qed
2976  }
2977  AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇((∃α w ⊨ φ{α}) → w ⊨ (∃α φ{α}))› for w
2978    by (rule "RM◇")
2979  moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2980    using "world:1"[THEN "≡⇩_d⇩_fE", OF PossibleWorld.ψ] "&E" by blast
2981  ultimately AOT_have ‹◇((∃α w ⊨ φ{α}) → w ⊨ (∃α φ{α}))›
2982    using "→E" by blast
2983  AOT_hence ‹◇(w ⊨ (∃α φ{α}))›
2984    by (metis 0 "KBasic2:4" "≡E"(1) "→E")
2985  AOT_thus ‹w ⊨ (∃α φ{α})›
2986    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2987    by blast
2988qed
2989
2990AOT_theorem "conj-dist-w:7": ‹(w ⊨ □p) → □w ⊨ p›
2991proof(rule "→I")
2992  AOT_assume ‹w ⊨ □p›
2993  AOT_hence ‹∃w w ⊨ □p› by (rule "PossibleWorld.∃I")
2994  AOT_hence ‹◇□p› using "fund:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(2)]
2995    by blast
2996  AOT_hence ‹□p›
2997    by (metis "5◇" "→E")
2998  AOT_hence 1: ‹□□p›
2999    by (metis "S5Basic:6" "≡E"(1))
3000  AOT_have ‹□∀w w ⊨ p›
3001    by (AOT_subst (reverse) ‹∀w w ⊨ p› ‹□p›)
3002       (auto simp add: "fund:2" 1)
3003  AOT_hence ‹∀w □w ⊨ p›
3004    using "fund-lem:5[world]"[THEN "→E"] by simp
3005  AOT_thus ‹□w ⊨ p›
3006    using "→E" "PossibleWorld.∀E" by fast
3007qed
3008
3009AOT_theorem "conj-dist-w:8": ‹∃w∃p((□w ⊨ p) & ¬w ⊨ □p)›
3010proof -
3011  AOT_obtain r where A: r and ‹◇¬r›
3012    by (metis "&E"(1) "&E"(2) "≡⇩_d⇩_fE" "∃E" "cont-tf:1" "cont-tf-thm:1")
3013  AOT_hence B: ‹¬□r›
3014    by (metis "KBasic:11" "≡E"(2))
3015  AOT_have ‹◇r›
3016    using A "T◇"[THEN "→E"] by simp
3017  AOT_hence ‹∃w w ⊨ r›
3018    using "fund:1"[THEN "≡E"(1)] by blast
3019  then AOT_obtain w where w: ‹w ⊨ r›
3020    using "PossibleWorld.∃E"[rotated] by meson
3021  AOT_hence ‹□w ⊨ r›
3022    by (metis "T◇" "≡E"(1) "rigid-truth-at:3" "vdash-properties:10")
3023  moreover AOT_have ‹¬w ⊨ □r›
3024  proof(rule "raa-cor:2")
3025    AOT_assume ‹w ⊨ □r›
3026    AOT_hence ‹∃w w ⊨ □r›
3027      by (rule "PossibleWorld.∃I")
3028    AOT_hence ‹□r›
3029      by (metis "≡E"(2) "nec-dia-w:1")
3030    AOT_thus ‹□r & ¬□r›
3031      using B "&I" by blast
3032  qed
3033  ultimately AOT_have ‹□w ⊨ r & ¬w ⊨ □r›
3034    by (rule "&I")
3035  AOT_hence ‹∃p (□w ⊨ p & ¬w ⊨ □p)›
3036    by (rule "∃I")
3037  thus ?thesis
3038    by (rule "PossibleWorld.∃I")
3039qed
3040
3041AOT_theorem "conj-dist-w:9": ‹(◇w ⊨ p) → w ⊨ ◇p›
3042proof(rule "→I"; rule "raa-cor:1")
3043  AOT_assume ‹◇w ⊨ p›
3044  AOT_hence 0: ‹w ⊨ p›
3045    by (metis "≡E"(1) "rigid-truth-at:2")
3046  AOT_assume ‹¬w ⊨ ◇p›
3047  AOT_hence 1: ‹w ⊨ ¬◇p›
3048    using "coherent:1"[unvarify p, THEN "≡E"(2), OF "log-prop-prop:2"] by blast
3049  moreover AOT_have ‹w ⊨ (¬◇p → ¬p)›
3050    using "T◇"[THEN "contraposition:1[1]", THEN RN]
3051          "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1), THEN "∀E"(2),
3052                   THEN "→E", rotated, OF PossibleWorld.ψ]
3053          by blast
3054  ultimately AOT_have ‹w ⊨ ¬p›
3055    using "conj-dist-w:2"[unvarify p q, OF "log-prop-prop:2", OF "log-prop-prop:2",
3056                          THEN "≡E"(1), THEN "→E"]
3057    by blast
3058  AOT_hence ‹w ⊨ p & w ⊨ ¬p› using 0 "&I" by blast
3059  AOT_thus ‹p & ¬p›
3060    by (metis "coherent:1" "Conjunction Simplification"(1,2) "≡E"(4)
3061              "modus-tollens:1" "raa-cor:3")
3062qed
3063
3064AOT_theorem "conj-dist-w:10": ‹∃w∃p((w ⊨ ◇p) & ¬◇w ⊨ p)›
3065proof -
3066  AOT_obtain w where w: ‹∀p (w ⊨ p ≡ p)›
3067    using "act-world:1" "PossibleWorld.∃E"[rotated] by meson
3068  AOT_obtain r where ‹¬r› and ‹◇r›
3069    using "cont-tf-thm:2" "cont-tf:2"[THEN "≡⇩_d⇩_fE"] "&E" "∃E"[rotated] by metis
3070  AOT_hence ‹w ⊨ ¬r› and 0: ‹w ⊨ ◇r›
3071    using w[THEN "∀E"(1), OF "log-prop-prop:2", THEN "≡E"(2)] by blast+
3072  AOT_hence ‹¬w ⊨ r› using "coherent:1"[THEN "≡E"(1)] by blast
3073  AOT_hence ‹¬◇w ⊨ r› by (metis "≡E"(4) "rigid-truth-at:2")
3074  AOT_hence ‹w ⊨ ◇r & ¬◇w ⊨ r› using 0 "&I" by blast
3075  AOT_hence ‹∃p (w ⊨ ◇p & ¬◇w ⊨ p)› by (rule "∃I")
3076  thus ?thesis by (rule "PossibleWorld.∃I")
3077qed
3078
3079AOT_theorem "two-worlds-exist:1": ‹∃p(ContingentlyTrue(p)) → ∃w (¬Actual(w))›
3080proof(rule "→I")
3081  AOT_assume ‹∃p ContingentlyTrue(p)›
3082  then AOT_obtain p where ‹ContingentlyTrue(p)›
3083    using "∃E"[rotated] by blast
3084  AOT_hence p: ‹p & ◇¬p›
3085    by (metis "≡⇩_d⇩_fE" "cont-tf:1")
3086  AOT_hence ‹∃w w ⊨ ¬p›
3087    using "fund:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] "&E" by blast
3088  then AOT_obtain w where w: ‹w ⊨ ¬p›
3089    using "PossibleWorld.∃E"[rotated] by meson
3090  AOT_have ‹¬Actual(w)›
3091  proof(rule "raa-cor:2")
3092    AOT_assume ‹Actual(w)›
3093    AOT_hence ‹w ⊨ p›
3094      using p[THEN "&E"(1)] actual[THEN "≡⇩_d⇩_fE", THEN "&E"(2)]
3095      by (metis "log-prop-prop:2" "raa-cor:3" "rule-ui:1" "→E" w)
3096    moreover AOT_have ‹¬(w ⊨ p)›
3097      by (metis "coherent:1" "≡E"(4) "reductio-aa:2" w) 
3098    ultimately AOT_show ‹w ⊨ p & ¬(w ⊨ p)›
3099      using "&I" by blast
3100  qed
3101  AOT_thus ‹∃w ¬Actual(w)›
3102    by (rule "PossibleWorld.∃I")
3103qed
3104
3105
3106AOT_theorem "two-worlds-exist:2": ‹∃p(ContingentlyFalse(p)) → ∃w (¬Actual(w))›
3107proof(rule "→I")
3108  AOT_assume ‹∃p ContingentlyFalse(p)›
3109  then AOT_obtain p where ‹ContingentlyFalse(p)›
3110    using "∃E"[rotated] by blast
3111  AOT_hence p: ‹¬p & ◇p›
3112    by (metis "≡⇩_d⇩_fE" "cont-tf:2")
3113  AOT_hence ‹∃w w ⊨ p›
3114    using "fund:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] "&E" by blast
3115  then AOT_obtain w where w: ‹w ⊨ p›
3116    using "PossibleWorld.∃E"[rotated] by meson
3117  moreover AOT_have ‹¬Actual(w)›
3118  proof(rule "raa-cor:2")
3119    AOT_assume ‹Actual(w)›
3120    AOT_hence ‹w ⊨ ¬p›
3121      using p[THEN "&E"(1)] actual[THEN "≡⇩_d⇩_fE", THEN "&E"(2)]
3122      by (metis "log-prop-prop:2" "raa-cor:3" "rule-ui:1" "→E" w)
3123    moreover AOT_have ‹¬(w ⊨ p)›
3124      using calculation by (metis "coherent:1" "≡E"(4) "reductio-aa:2") 
3125    AOT_thus ‹w ⊨ p & ¬(w ⊨ p)›
3126      using "&I" w by metis
3127  qed
3128  AOT_thus ‹∃w ¬Actual(w)›
3129    by (rule "PossibleWorld.∃I")
3130qed
3131
3132AOT_theorem "two-worlds-exist:3": ‹∃w ¬Actual(w)›
3133  using "cont-tf-thm:1" "two-worlds-exist:1" "→E" by blast
3134
3135AOT_theorem "two-worlds-exist:4": ‹∃w∃w'(w ≠ w')›
3136proof -
3137  AOT_obtain w where w: ‹Actual(w)›
3138    using "act-world:2"[THEN "uniqueness:1"[THEN "≡⇩_d⇩_fE"],
3139                        THEN "cqt-further:5"[THEN "→E"]]
3140          "PossibleWorld.∃E"[rotated] "&E"
3141    by blast
3142  moreover AOT_obtain w' where w': ‹¬Actual(w')›
3143    using "two-worlds-exist:3" "PossibleWorld.∃E"[rotated] by meson
3144  AOT_have ‹¬(w = w')›
3145  proof(rule "raa-cor:2")
3146    AOT_assume ‹w = w'›
3147    AOT_thus ‹p & ¬p› for p
3148      using w w' "&E" by (metis "rule=E" "raa-cor:3")
3149  qed
3150  AOT_hence ‹w ≠ w'›
3151    by (metis "≡⇩_d⇩_fI" "=-infix")
3152  AOT_hence ‹∃w' w ≠ w'›
3153    by (rule "PossibleWorld.∃I")
3154  thus ?thesis
3155    by (rule "PossibleWorld.∃I")
3156qed
3157
3158(* TODO: more theorems *)
3159
3160AOT_theorem "w-rel:1": ‹[λx φ{x}]↓ → [λx w ⊨ φ{x}]↓›
3161proof(rule "→I")
3162  AOT_assume ‹[λx φ{x}]↓›
3163  AOT_hence ‹□[λx φ{x}]↓›
3164    by (metis "exist-nec" "→E")
3165  moreover AOT_have
3166    ‹□[λx φ{x}]↓ → □∀x∀y(∀F([F]x ≡ [F]y) → ((w ⊨ φ{x}) ≡ ( w ⊨ φ{y})))›
3167  proof (rule RM; rule "→I"; rule GEN; rule GEN; rule "→I")
3168    AOT_modally_strict {
3169      fix x y
3170      AOT_assume ‹[λx φ{x}]↓›
3171      AOT_hence ‹∀x∀y (∀F ([F]x ≡ [F]y) → □(φ{x} ≡ φ{y}))›
3172        using "&E" "kirchner-thm-cor:1"[THEN "→E"] by blast
3173      AOT_hence ‹∀F ([F]x ≡ [F]y) → □(φ{x} ≡ φ{y})›
3174        using "∀E"(2) by blast
3175      moreover AOT_assume ‹∀F ([F]x ≡ [F]y)›
3176      ultimately AOT_have ‹□(φ{x} ≡ φ{y})›
3177        using "→E" by blast
3178      AOT_hence ‹∀w (w ⊨ (φ{x} ≡ φ{y}))›
3179        using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] by blast
3180      AOT_hence ‹w ⊨ (φ{x} ≡ φ{y})›
3181        using "∀E"(2) using PossibleWorld.ψ "→E" by blast
3182      AOT_thus ‹(w ⊨ φ{x}) ≡ (w ⊨ φ{y})›
3183        using "conj-dist-w:4"[unvarify p q, OF "log-prop-prop:2",
3184                              OF "log-prop-prop:2", THEN "≡E"(1)] by blast
3185    }
3186  qed
3187  ultimately AOT_have ‹□∀x∀y(∀F([F]x ≡ [F]y) → ((w ⊨ φ{x}) ≡ ( w ⊨ φ{y})))›
3188    using "→E" by blast
3189  AOT_thus ‹[λx w ⊨ φ{x}]↓›
3190    using "kirchner-thm:1"[THEN "≡E"(2)] by fast
3191qed
3192
3193AOT_theorem "w-rel:2": ‹[λx⇩₁...x⇩_n φ{x⇩₁...x⇩_n}]↓ → [λx⇩₁...x⇩_n w ⊨ φ{x⇩₁...x⇩_n}]↓›
3194proof(rule "→I")
3195  AOT_assume ‹[λx⇩₁...x⇩_n φ{x⇩₁...x⇩_n}]↓›
3196  AOT_hence ‹□[λx⇩₁...x⇩_n φ{x⇩₁...x⇩_n}]↓›
3197    by (metis "exist-nec" "→E")
3198  moreover AOT_have ‹□[λx⇩₁...x⇩_n φ{x⇩₁...x⇩_n}]↓ → □∀x⇩₁...∀x⇩_n∀y⇩₁...∀y⇩_n(
3199    ∀F([F]x⇩₁...x⇩_n ≡ [F]y⇩₁...y⇩_n) → ((w ⊨ φ{x⇩₁...x⇩_n}) ≡ ( w ⊨ φ{y⇩₁...y⇩_n})))›
3200  proof (rule RM; rule "→I"; rule GEN; rule GEN; rule "→I")
3201    AOT_modally_strict {
3202      fix x⇩₁x⇩_n y⇩₁y⇩_n
3203      AOT_assume ‹[λx⇩₁...x⇩_n φ{x⇩₁...x⇩_n}]↓›
3204      AOT_hence ‹∀x⇩₁...∀x⇩_n∀y⇩₁...∀y⇩_n (
3205        ∀F ([F]x⇩₁...x⇩_n ≡ [F]y⇩₁...y⇩_n) → □(φ{x⇩₁...x⇩_n} ≡ φ{y⇩₁...y⇩_n}))›
3206        using "&E" "kirchner-thm-cor:2"[THEN "→E"] by blast
3207      AOT_hence ‹∀F ([F]x⇩₁...x⇩_n ≡ [F]y⇩₁...y⇩_n) → □(φ{x⇩₁...x⇩_n} ≡ φ{y⇩₁...y⇩_n})›
3208        using "∀E"(2) by blast
3209      moreover AOT_assume ‹∀F ([F]x⇩₁...x⇩_n ≡ [F]y⇩₁...y⇩_n)›
3210      ultimately AOT_have ‹□(φ{x⇩₁...x⇩_n} ≡ φ{y⇩₁...y⇩_n})›
3211        using "→E" by blast
3212      AOT_hence ‹∀w (w ⊨ (φ{x⇩₁...x⇩_n} ≡ φ{y⇩₁...y⇩_n}))›
3213        using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] by blast
3214      AOT_hence ‹w ⊨ (φ{x⇩₁...x⇩_n} ≡ φ{y⇩₁...y⇩_n})›
3215        using "∀E"(2) using PossibleWorld.ψ "→E" by blast
3216      AOT_thus ‹(w ⊨ φ{x⇩₁...x⇩_n}) ≡ (w ⊨ φ{y⇩₁...y⇩_n})›
3217        using "conj-dist-w:4"[unvarify p q, OF "log-prop-prop:2",
3218                              OF "log-prop-prop:2", THEN "≡E"(1)] by blast
3219    }
3220  qed
3221  ultimately AOT_have ‹□∀x⇩₁...∀x⇩_n∀y⇩₁...∀y⇩_n(
3222      ∀F([F]x⇩₁...x⇩_n ≡ [F]y⇩₁...y⇩_n) → ((w ⊨ φ{x⇩₁...x⇩_n}) ≡ ( w ⊨ φ{y⇩₁...y⇩_n})))›
3223    using "→E" by blast
3224  AOT_thus ‹[λx⇩₁...x⇩_n w ⊨ φ{x⇩₁...x⇩_n}]↓›
3225    using "kirchner-thm:2"[THEN "≡E"(2)] by fast
3226qed
3227
3228AOT_theorem "w-rel:3": ‹[λx⇩₁...x⇩_n w ⊨ [F]x⇩₁...x⇩_n]↓›
3229  by (rule "w-rel:2"[THEN "→E"]) "cqt:2[lambda]"
3230
3231AOT_define WorldIndexedRelation :: ‹Π ⇒ τ ⇒ Π› (‹_⇩_›)
3232  "w-index": ‹[F]⇩w =⇩_d⇩_f [λx⇩₁...x⇩_n w ⊨ [F]x⇩₁...x⇩_n]›
3233
3234AOT_define Rigid :: ‹τ ⇒ φ› (‹Rigid'(_')›)
3235  "df-rigid-rel:1":
3236‹Rigid(F) ≡⇩_d⇩_f F↓ & □∀x⇩₁...∀x⇩_n([F]x⇩₁...x⇩_n → □[F]x⇩₁...x⇩_n)›
3237
3238AOT_define Rigidifies :: ‹τ ⇒ τ ⇒ φ› (‹Rigidifies'(_,_')›)
3239  "df-rigid-rel:2":
3240‹Rigidifies(F, G) ≡⇩_d⇩_f Rigid(F) & ∀x⇩₁...∀x⇩_n([F]x⇩₁...x⇩_n ≡ [G]x⇩₁...x⇩_n)›
3241
3242AOT_theorem "rigid-der:1": ‹[[F]⇩w]x⇩₁...x⇩_n ≡ w ⊨ [F]x⇩₁...x⇩_n›
3243  apply (rule "rule-id-df:2:b[2]"[where τ="λ (Π, κ). «[Π]⇩κ»" and
3244                                        σ="λ(Π, κ). «[λx⇩₁...x⇩_n κ ⊨ [Π]x⇩₁...x⇩_n]»",
3245                                  simplified, OF "w-index"])
3246   apply (fact "w-rel:3")
3247  apply (rule "beta-C-meta"[THEN "→E"])
3248  by (fact "w-rel:3")
3249
3250AOT_theorem "rigid-der:2": ‹Rigid([G]⇩w)›
3251proof(safe intro!: "≡⇩_d⇩_fI"[OF "df-rigid-rel:1"] "&I")
3252  AOT_show ‹[G]⇩w↓›
3253    by (rule "rule-id-df:2:b[2]"[where τ="λ (Π, κ). «[Π]⇩κ»" and
3254                                       σ="λ(Π, κ). «[λx⇩₁...x⇩_n κ ⊨ [Π]x⇩₁...x⇩_n]»",
3255                                 simplified, OF "w-index"])
3256       (fact "w-rel:3")+
3257next
3258  AOT_have ‹□∀x⇩₁...∀x⇩_n ([[G]⇩w]x⇩₁...x⇩_n → □[[G]⇩w]x⇩₁...x⇩_n)›
3259  proof(rule RN; safe intro!: "→I" GEN)
3260    AOT_modally_strict {
3261      AOT_have assms: ‹PossibleWorld(w)› using PossibleWorld.ψ.
3262      AOT_hence nec_pw_w: ‹□PossibleWorld(w)›
3263        using "≡E"(1) "rigid-pw:1" by blast
3264      fix x⇩₁x⇩_n
3265      AOT_assume ‹[[G]⇩w]x⇩₁...x⇩_n›
3266      AOT_hence ‹[λx⇩₁...x⇩_n w ⊨ [G]x⇩₁...x⇩_n]x⇩₁...x⇩_n›
3267        using "rule-id-df:2:a[2]"[where τ="λ (Π, κ). «[Π]⇩κ»" and
3268                                        σ="λ(Π, κ). «[λx⇩₁...x⇩_n κ ⊨ [Π]x⇩₁...x⇩_n]»",
3269                                        simplified, OF "w-index", OF "w-rel:3"]
3270        by fast
3271      AOT_hence ‹w ⊨ [G]x⇩₁...x⇩_n›
3272        by (metis "β→C"(1))
3273      AOT_hence ‹□w ⊨ [G]x⇩₁...x⇩_n›
3274        using "rigid-truth-at:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)]
3275        by blast
3276      moreover AOT_have ‹□w ⊨ [G]x⇩₁...x⇩_n → □[λx⇩₁...x⇩_n w ⊨ [G]x⇩₁...x⇩_n]x⇩₁...x⇩_n›
3277      proof (rule RM; rule "→I")
3278        AOT_modally_strict {
3279          AOT_assume ‹w ⊨ [G]x⇩₁...x⇩_n›
3280          AOT_thus ‹[λx⇩₁...x⇩_n w ⊨ [G]x⇩₁...x⇩_n]x⇩₁...x⇩_n›
3281            by (auto intro!: "β←C"(1) simp: "w-rel:3" "cqt:2")
3282        }
3283      qed
3284      ultimately AOT_have 1: ‹□[λx⇩₁...x⇩_n w ⊨ [G]x⇩₁...x⇩_n]x⇩₁...x⇩_n›
3285        using "→E" by blast
3286      AOT_show ‹□[[G]⇩w]x⇩₁...x⇩_n›
3287        by (rule "rule-id-df:2:b[2]"[where τ="λ (Π, κ). «[Π]⇩κ»" and
3288                                           σ="λ(Π, κ). «[λx⇩₁...x⇩_n κ ⊨ [Π]x⇩₁...x⇩_n]»",
3289                                     simplified, OF "w-index"])
3290           (auto simp: 1 "w-rel:3")
3291    }
3292  qed
3293  AOT_thus ‹□∀x⇩₁...∀x⇩_n ([[G]⇩w]x⇩₁...x⇩_n → □[[G]⇩w]x⇩₁...x⇩_n)›
3294    using "→E" by blast
3295qed
3296
3297AOT_theorem "rigid-der:3": ‹∃F Rigidifies(F, G)›
3298proof -
3299  AOT_obtain w where w: ‹∀p (w ⊨ p ≡ p)›
3300    using "act-world:1" "PossibleWorld.∃E"[rotated] by meson
3301  show ?thesis
3302  proof (rule "∃I"(1)[where τ=‹«[G]⇩w»›])
3303    AOT_show ‹Rigidifies([G]⇩w, [G])›
3304    proof(safe intro!: "≡⇩_d⇩_fI"[OF "df-rigid-rel:2"] "&I" GEN)
3305      AOT_show ‹Rigid([G]⇩w)›
3306        using "rigid-der:2" by blast
3307    next
3308      fix x⇩₁x⇩_n
3309      AOT_have ‹[[G]⇩w]x⇩₁...x⇩_n ≡ [λx⇩₁...x⇩_n w ⊨ [G]x⇩₁...x⇩_n]x⇩₁...x⇩_n›
3310      proof(rule "≡I"; rule "→I")
3311        AOT_assume ‹[[G]⇩w]x⇩₁...x⇩_n›
3312        AOT_thus ‹[λx⇩₁...x⇩_n w ⊨ [G]x⇩₁...x⇩_n]x⇩₁...x⇩_n›
3313          by (rule "rule-id-df:2:a[2]"
3314                      [where τ="λ (Π, κ). «[Π]⇩κ»" and
3315                             σ="λ(Π, κ). «[λx⇩₁...x⇩_n κ ⊨ [Π]x⇩₁...x⇩_n]»",
3316                       simplified, OF "w-index", OF "w-rel:3"])
3317      next
3318        AOT_assume ‹[λx⇩₁...x⇩_n w ⊨ [G]x⇩₁...x⇩_n]x⇩₁...x⇩_n›
3319        AOT_thus ‹[[G]⇩w]x⇩₁...x⇩_n›
3320          by (rule "rule-id-df:2:b[2]"
3321                      [where τ="λ (Π, κ). «[Π]⇩κ»" and
3322                             σ="λ(Π, κ). «[λx⇩₁...x⇩_n κ ⊨ [Π]x⇩₁...x⇩_n]»",
3323                       simplified, OF "w-index", OF "w-rel:3"])
3324      qed
3325      also AOT_have ‹… ≡ w ⊨ [G]x⇩₁...x⇩_n›
3326        by (rule "beta-C-meta"[THEN "→E"])
3327           (fact "w-rel:3")
3328      also AOT_have ‹… ≡ [G]x⇩₁...x⇩_n›
3329        using w[THEN "∀E"(1), OF "log-prop-prop:2"] by blast
3330      finally AOT_show ‹[[G]⇩w]x⇩₁...x⇩_n ≡ [G]x⇩₁...x⇩_n›.
3331    qed
3332  next
3333    AOT_show ‹[G]⇩w↓›
3334      by (rule "rule-id-df:2:b[2]"[where τ="λ (Π, κ). «[Π]⇩κ»"
3335                                     and σ="λ(Π, κ). «[λx⇩₁...x⇩_n κ ⊨ [Π]x⇩₁...x⇩_n]»",
3336                                   simplified, OF "w-index"])
3337         (auto simp: "w-rel:3")
3338  qed
3339qed
3340
3341AOT_theorem "rigid-rel-thms:1":
3342  ‹□(∀x⇩₁...∀x⇩_n ([F]x⇩₁...x⇩_n → □[F]x⇩₁...x⇩_n)) ≡ ∀x⇩₁...∀x⇩_n(◇[F]x⇩₁...x⇩_n → □[F]x⇩₁...x⇩_n)›
3343proof(safe intro!: "≡I" "→I" GEN)
3344  fix x⇩₁x⇩_n
3345  AOT_assume ‹□∀x⇩₁...∀x⇩_n ([F]x⇩₁...x⇩_n → □[F]x⇩₁...x⇩_n)›
3346  AOT_hence ‹∀x⇩₁...∀x⇩_n □([F]x⇩₁...x⇩_n → □[F]x⇩₁...x⇩_n)›
3347    by (metis "→E" GEN RM "cqt-orig:3")
3348  AOT_hence ‹□([F]x⇩₁...x⇩_n → □[F]x⇩₁...x⇩_n)›
3349    using "∀E"(2) by blast
3350  AOT_hence ‹◇[F]x⇩₁...x⇩_n → □[F]x⇩₁...x⇩_n›
3351    by (metis "≡E"(1) "sc-eq-box-box:1")
3352  moreover AOT_assume ‹◇[F]x⇩₁...x⇩_n›
3353  ultimately AOT_show ‹□[F]x⇩₁...x⇩_n›
3354    using "→E" by blast
3355next
3356  AOT_assume ‹∀x⇩₁...∀x⇩_n (◇[F]x⇩₁...x⇩_n → □[F]x⇩₁...x⇩_n)›
3357  AOT_hence ‹◇[F]x⇩₁...x⇩_n → □[F]x⇩₁...x⇩_n› for x⇩₁x⇩_n
3358    using "∀E"(2) by blast
3359  AOT_hence ‹□([F]x⇩₁...x⇩_n → □[F]x⇩₁...x⇩_n)› for x⇩₁x⇩_n
3360    by (metis "≡E"(2) "sc-eq-box-box:1")
3361  AOT_hence 0: ‹∀x⇩₁...∀x⇩_n □([F]x⇩₁...x⇩_n → □[F]x⇩₁...x⇩_n)›
3362    by (rule GEN)
3363  AOT_thus ‹□(∀x⇩₁...∀x⇩_n ([F]x⇩₁...x⇩_n → □[F]x⇩₁...x⇩_n))›
3364    using "BF" "vdash-properties:10" by blast
3365qed
3366
3367AOT_theorem "rigid-rel-thms:2":
3368  ‹□(∀x⇩₁...∀x⇩_n ([F]x⇩₁...x⇩_n → □[F]x⇩₁...x⇩_n)) ≡ ∀x⇩₁...∀x⇩_n(□[F]x⇩₁...x⇩_n ∨ □¬[F]x⇩₁...x⇩_n)›
3369proof(safe intro!: "≡I" "→I")
3370  AOT_assume ‹□(∀x⇩₁...∀x⇩_n ([F]x⇩₁...x⇩_n → □[F]x⇩₁...x⇩_n))›
3371  AOT_hence 0: ‹∀x⇩₁...∀x⇩_n □([F]x⇩₁...x⇩_n → □[F]x⇩₁...x⇩_n)›
3372    using CBF[THEN "→E"] by blast
3373  AOT_show ‹∀x⇩₁...∀x⇩_n(□[F]x⇩₁...x⇩_n ∨ □¬[F]x⇩₁...x⇩_n)›
3374  proof(rule GEN)
3375    fix x⇩₁x⇩_n
3376    AOT_have 1: ‹□([F]x⇩₁...x⇩_n → □[F]x⇩₁...x⇩_n)›
3377      using 0[THEN "∀E"(2)].
3378    AOT_hence 2: ‹◇[F]x⇩₁...x⇩_n → [F]x⇩₁...x⇩_n›
3379      using "B◇" "Hypothetical Syllogism" "K◇" "vdash-properties:10" by blast
3380    AOT_have ‹[F]x⇩₁...x⇩_n ∨ ¬[F]x⇩₁...x⇩_n›
3381      using "exc-mid".
3382    moreover {
3383      AOT_assume ‹[F]x⇩₁...x⇩_n›
3384      AOT_hence ‹□[F]x⇩₁...x⇩_n›
3385        using 1[THEN "qml:2"[axiom_inst, THEN "→E"], THEN "→E"] by blast
3386    }
3387    moreover {
3388      AOT_assume 3: ‹¬[F]x⇩₁...x⇩_n›
3389      AOT_have ‹□¬[F]x⇩₁...x⇩_n›
3390      proof(rule "raa-cor:1")
3391        AOT_assume ‹¬□¬[F]x⇩₁...x⇩_n›
3392        AOT_hence ‹◇[F]x⇩₁...x⇩_n›
3393          by (AOT_subst_def "conventions:5")
3394        AOT_hence ‹[F]x⇩₁...x⇩_n› using 2[THEN "→E"] by blast
3395        AOT_thus ‹[F]x⇩₁...x⇩_n & ¬[F]x⇩₁...x⇩_n›
3396          using 3 "&I" by blast
3397      qed
3398    }
3399    ultimately AOT_show ‹□[F]x⇩₁...x⇩_n ∨ □¬[F]x⇩₁...x⇩_n›
3400      by (metis "∨I"(1,2) "raa-cor:1")
3401  qed
3402next
3403  AOT_assume 0: ‹∀x⇩₁...∀x⇩_n(□[F]x⇩₁...x⇩_n ∨ □¬[F]x⇩₁...x⇩_n)›
3404  {
3405    fix x⇩₁x⇩_n
3406    AOT_have ‹□[F]x⇩₁...x⇩_n ∨ □¬[F]x⇩₁...x⇩_n› using 0[THEN "∀E"(2)] by blast
3407    moreover {
3408      AOT_assume ‹□[F]x⇩₁...x⇩_n›
3409      AOT_hence ‹□□[F]x⇩₁...x⇩_n›
3410        using "S5Basic:6"[THEN "≡E"(1)] by blast
3411      AOT_hence ‹□([F]x⇩₁...x⇩_n → □[F]x⇩₁...x⇩_n)›
3412        using "KBasic:1"[THEN "→E"] by blast
3413    }
3414    moreover {
3415      AOT_assume ‹□¬[F]x⇩₁...x⇩_n›
3416      AOT_hence ‹□([F]x⇩₁...x⇩_n → □[F]x⇩₁...x⇩_n)›
3417        using "KBasic:2"[THEN "→E"] by blast
3418    }
3419    ultimately AOT_have ‹□([F]x⇩₁...x⇩_n → □[F]x⇩₁...x⇩_n)›
3420      using "con-dis-i-e:4:b" "raa-cor:1" by blast
3421  }
3422  AOT_hence ‹∀x⇩₁...∀x⇩_n □([F]x⇩₁...x⇩_n → □[F]x⇩₁...x⇩_n)›
3423    by (rule GEN)
3424  AOT_thus ‹□(∀x⇩₁...∀x⇩_n ([F]x⇩₁...x⇩_n → □[F]x⇩₁...x⇩_n))›
3425    using BF[THEN "→E"] by fast
3426qed
3427
3428AOT_theorem "rigid-rel-thms:3": ‹Rigid(F) ≡ ∀x⇩₁...∀x⇩_n (□[F]x⇩₁...x⇩_n ∨ □¬[F]x⇩₁...x⇩_n)›
3429  by (AOT_subst_thm "df-rigid-rel:1"[THEN "≡Df", THEN "≡S"(1), OF "cqt:2"(1)];
3430      AOT_subst_thm "rigid-rel-thms:2")
3431     (simp add: "oth-class-taut:3:a")
3432
3433AOT_theorem "poss-sit-part-w:1": ‹Possible(s) ≡ ∃w(s ⊴ w)›
3434proof(safe intro!: "≡I" "→I")
3435  AOT_assume ‹Possible(s)›
3436  AOT_hence ‹◇Actual(s)›
3437    using "≡⇩_d⇩_fE" "con-dis-i-e:2:b" pos by blast
3438  AOT_hence ‹◇∀p (s ⊨ p → p)›
3439    apply (AOT_subst (reverse) ‹∀p (s ⊨ p → p)› ‹Actual(s)›)
3440    using "df-simplify:1" "rule-eq-df:1" Situation.restricted_var_condition actual apply blast
3441    by auto
3442  AOT_hence ‹∃w w ⊨ ∀p (s ⊨ p → p)›
3443    by (safe intro!: "fund:1"[unvarify p, THEN "≡E"(1)] "log-prop-prop:2")
3444  then AOT_obtain w where ‹w ⊨ ∀p (s ⊨ p → p)›
3445    using PossibleWorld.instantiation by meson
3446  AOT_hence 1: ‹∀p w ⊨ (s ⊨ p → p)›
3447    using "conj-dist-w:5"
3448    using "intro-elim:3:a" by blast
3449  AOT_have ‹s ⊴ w›
3450  proof(safe intro!: "sit-part-whole"[THEN "≡⇩_d⇩_fI"] "&I" "Situation.ψ" GEN "→I")
3451    AOT_show ‹Situation(w)›
3452      using "≡⇩_d⇩_fE" "con-dis-i-e:2:a" "world-pos" pos by blast
3453  next
3454    fix p
3455    AOT_assume ‹s ⊨ p›
3456    AOT_hence ‹□s ⊨ p›
3457      using "intro-elim:3:a" "lem2:1" by blast
3458    AOT_hence ‹∀w w ⊨ s ⊨ p›
3459      by (safe intro!: "fund:2"[unvarify p, THEN "≡E"(1)] "log-prop-prop:2")
3460    AOT_hence ‹w ⊨ s ⊨ p›
3461      using "rule-ui:3" "vdash-properties:10" PossibleWorld.restricted_var_condition by blast
3462    moreover AOT_have ‹w ⊨ (s ⊨ p → p)›
3463      using 1 "∀E" by blast
3464    ultimately AOT_show ‹w ⊨ p›
3465      using "conj-dist-w:2"[unvarify p, THEN "≡E"(1)] "log-prop-prop:2" "→E" by blast
3466  qed
3467  AOT_thus ‹∃w(s ⊴ w)›
3468    using "PossibleWorld.∃I" by blast
3469next
3470  AOT_assume ‹∃w(s ⊴ w)›
3471  then AOT_obtain w where ‹s ⊴ w›
3472    using "PossibleWorld.∃E" by meson
3473  AOT_hence 1: ‹∀p (s ⊨ p → w ⊨ p)›
3474    using "sit-part-whole"[THEN "≡⇩_d⇩_fE"] "&E" by blast
3475  AOT_have ‹∀p (w ⊨ (s ⊨ p → p))›
3476  proof (safe intro!: GEN "conj-dist-w:2"[unvarify p, THEN "≡E"(2)] "log-prop-prop:2" "→I")
3477    fix p
3478    AOT_assume ‹w ⊨ s ⊨ p›
3479    AOT_hence ‹◇s ⊨ p›
3480      by (auto intro!: "fund:1"[unvarify p, THEN "≡E"(2)] "log-prop-prop:2" "PossibleWorld.∃I")
3481    AOT_hence ‹s ⊨ p›
3482      using "intro-elim:3:a" "lem2:2" by blast
3483    AOT_thus ‹w ⊨ p›
3484      using 1 "log-prop-prop:2" "rule-ui:1" "vdash-properties:10" by blast
3485  qed
3486  AOT_hence ‹w ⊨ ∀p (s ⊨ p → p)›
3487    by (metis "≡E"(2) "conj-dist-w:5")
3488  AOT_hence ‹◇∀p (s ⊨ p → p)›
3489    by (safe intro!: "fund:1"[unvarify p, THEN "≡E"(2)] "log-prop-prop:2" PossibleWorld.existential)
3490  AOT_hence ‹◇Actual(s)›
3491    by (AOT_subst_def actual)
3492       (metis "KBasic:16" "&I" "→E" RN "Situation.ψ")
3493  AOT_thus ‹Possible(s)›
3494    by(safe intro!: "pos"[THEN "≡⇩_d⇩_fI"] "&I" "Situation.ψ")
3495qed
3496
3497AOT_define GapOn :: ‹τ ⇒ φ ⇒ φ› (‹GapOn'(_,_')›)
3498  "routley-star:5": ‹GapOn(s,p) ≡⇩_d⇩_f ¬s ⊨ p & ¬s ⊨ ¬p›
3499
3500(*<*)
3501end
3502(*>*)
3503