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