Theory AOT_ExtendedRelationComprehension

1theory AOT_ExtendedRelationComprehension
2  imports AOT_RestrictedVariables
3begin
4
5sectionExtended Relation Comprehension
6
7textThis theory depends on choosing extended models.
8interpretation AOT_ExtendedModel by (standard; auto)
9
10textAuxiliary lemma: negations of denoting relations denote.
11AOT_theorem negation_denotes: x φ{x}]  x ¬φ{x}]
12proof(rule "→I")
13  AOT_assume 0: x φ{x}]
14  AOT_show x ¬φ{x}]
15  proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
16    AOT_show x ¬x φ{x}]x] by "cqt:2"
17  next
18    AOT_have x φ{x}]
19      using 0 "exist-nec"[THEN "→E"] by blast
20    moreover AOT_have x φ{x}]  x (¬x φ{x}]x  ¬φ{x})
21      by(rule RM; safe intro!: GEN "≡I" "→I" "β→C"(2) "β←C"(2) "cqt:2")
22    ultimately AOT_show x (¬x φ{x}]x  ¬φ{x})
23      using "→E" by blast
24  qed
25qed
26
27textAuxiliary lemma: conjunctions of denoting relations denote.
28AOT_theorem conjunction_denotes: x φ{x}] & x ψ{x}]  x φ{x} & ψ{x}]
29proof(rule "→I")
30  AOT_assume 0: x φ{x}] & x ψ{x}]
31  AOT_show x φ{x} & ψ{x}]
32  proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
33    AOT_show x x φ{x}]x & x ψ{x}]x] by "cqt:2"
34  next
35    AOT_have (x φ{x}] & x ψ{x}])
36      using 0 "exist-nec"[THEN "→E"] "&E"
37            "KBasic:3" "df-simplify:2" "intro-elim:3:b" by blast
38    moreover AOT_have
39      (x φ{x}] & x ψ{x}])  x (x φ{x}]x & x ψ{x}]x  φ{x} & ψ{x})
40      by(rule RM; auto intro!: GEN "≡I" "→I" "cqt:2" "&I"
41                        intro: "β←C"
42                         dest: "&E" "β→C")
43    ultimately AOT_show x (x φ{x}]x & x ψ{x}]x  φ{x} & ψ{x})
44      using "→E" by blast
45  qed
46qed
47
48AOT_register_rigid_restricted_type
49  Ordinary: O!κ
50proof
51  AOT_modally_strict {
52    AOT_show x O!x
53      by (meson "B◇" "T◇" "o-objects-exist:1" "→E")
54  }
55next
56  AOT_modally_strict {
57    AOT_show O!κ  κ for κ
58      by (simp add: "→I" "cqt:5:a[1]"[axiom_inst, THEN "→E", THEN "&E"(2)])
59  }
60next
61  AOT_modally_strict {
62    AOT_show α(O!α  O!α)
63      by (simp add: GEN "oa-facts:1")
64  }
65qed
66
67AOT_register_variable_names
68  Ordinary: u v r t s
69
70textIn PLM this is defined in the Natural Numbers chapter,
71     but since it is helpful for stating the comprehension principles,
72     we already define it here.
73AOT_define eqE :: τ  τ  φ (infixl E 50)
74  eqE: F E G df F & G & u ([F]u  [G]u)
75
76textDerive existence claims about relations from the axioms.
77AOT_theorem denotes_all: x G (G E F  x[G])]
78    and denotes_all_neg: x G (G E F  ¬x[G])]
79proof -
80  AOT_have Aux: F (F E G  (x[F]  x[G])), ¬(x[G]  y[G])
81     F([F]x & ¬[F]y) for x y G
82  proof -
83    AOT_modally_strict {
84    AOT_assume 0: F (F E G  (x[F]  x[G]))
85    AOT_assume G_prop: ¬(x[G]  y[G])
86    {
87      AOT_assume ¬F([F]x & ¬[F]y)
88      AOT_hence 0: F ¬([F]x & ¬[F]y)
89        by (metis "cqt-further:4" "→E")
90      AOT_have F ([F]x  [F]y)
91      proof (rule GEN; rule "≡I"; rule "→I")
92        fix F
93        AOT_assume [F]x
94        moreover AOT_have ¬([F]x & ¬[F]y)
95          using 0[THEN "∀E"(2)] by blast
96        ultimately AOT_show [F]y
97          by (metis "&I" "raa-cor:1") 
98      next
99        fix F
100        AOT_assume [F]y
101        AOT_hence ¬x ¬[F]x]y
102          by (metis "¬¬I" "β→C"(2))
103        moreover AOT_have ¬(x ¬[F]x]x & ¬x ¬[F]x]y)
104          apply (rule 0[THEN "∀E"(1)]) by "cqt:2[lambda]"
105        ultimately AOT_have 1: ¬x ¬[F]x]x
106          by (metis "&I" "raa-cor:3")
107        {
108          AOT_assume ¬[F]x
109          AOT_hence x ¬[F]x]x
110            by (auto intro!: "β←C"(1) "cqt:2")
111          AOT_hence p & ¬p for p
112            using 1 by (metis "raa-cor:3")
113        }
114        AOT_thus [F]x by (metis "raa-cor:1")
115      qed
116      AOT_hence F ([F]x  [F]y)
117        using "ind-nec"[THEN "→E"] by blast
118      AOT_hence F ([F]x  [F]y)
119        by (metis "CBF" "→E")
120    } note indistI = this
121    {
122      AOT_assume G_prop: x[G] & ¬y[G]
123      AOT_hence Ax: A!x
124        using "&E"(1) "∃I"(2) "→E" "encoders-are-abstract" by blast
125  
126      {
127        AOT_assume Ay: A!y
128        {
129          fix F
130          {
131            AOT_assume u([F]u  [G]u)
132            AOT_hence u([F]u  [G]u)
133              using "Ordinary.res-var-bound-reas[BF]"[THEN "→E"] by simp
134            AOT_hence F E G
135              by (AOT_subst F E G u ([F]u  [G]u))
136                 (auto intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
137            AOT_hence x[F]  x[G]
138              using 0[THEN "∀E"(2)] "≡E" "→E" by meson
139            AOT_hence x[F]
140              using G_prop "&E" "≡E" by blast
141          }
142          AOT_hence u([F]u  [G]u)  x[F]
143            by (rule "→I")
144        }
145        AOT_hence xprop: F(u([F]u  [G]u)  x[F])
146          by (rule GEN)
147        moreover AOT_have yprop: ¬F(u([F]u  [G]u)  y[F])
148        proof (rule "raa-cor:2")
149          AOT_assume F(u([F]u  [G]u)  y[F])
150          AOT_hence F(u([F]u  [G]u)  y[F])
151            apply (AOT_subst u([F]u  [G]u) u([F]u  [G]u) for: F)
152            using "Ordinary.res-var-bound-reas[BF]"
153                  "Ordinary.res-var-bound-reas[CBF]"
154                  "intro-elim:2" apply presburger
155            by simp
156          AOT_hence A: F(F E G  y[F])
157            by (AOT_subst F E G u ([F]u  [G]u) for: F)
158               (auto intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
159          moreover AOT_have G E G
160            by (auto intro!: "eqE"[THEN "dfI"] "cqt:2" RN "&I" GEN "→I" "≡I")
161          ultimately AOT_have y[G] using "∀E"(2) "→E" by blast
162          AOT_thus p & ¬p for p using G_prop "&E" by (metis "raa-cor:3")
163        qed
164        AOT_have F([F]x & ¬[F]y)
165        proof(rule "raa-cor:1")
166          AOT_assume ¬F([F]x & ¬[F]y)
167          AOT_hence indist: F ([F]x  [F]y) using indistI by blast
168          AOT_have F(u([F]u  [G]u)  y[F])
169            using indistinguishable_ord_enc_all[axiom_inst, THEN "→E", OF "&I",
170                      OF "&I", OF "&I", OF "cqt:2[const_var]"[axiom_inst],
171                      OF Ax, OF Ay, OF indist, THEN "≡E"(1), OF xprop].
172          AOT_thus F(u([F]u  [G]u)  y[F]) & ¬F(u([F]u  [G]u)  y[F])
173            using yprop "&I" by blast
174        qed
175      }
176      moreover {
177        AOT_assume notAy: ¬A!y
178        AOT_have F([F]x & ¬[F]y)
179          apply (rule "∃I"(1)[where τ=«A!»])
180          using Ax notAy "&I" apply blast
181          by (simp add: "oa-exist:2")
182      }
183      ultimately AOT_have F([F]x & ¬[F]y)
184        by (metis "raa-cor:1")
185    }
186    moreover {
187      AOT_assume G_prop: ¬x[G] & y[G]
188      AOT_hence Ay: A!y
189        by (meson "&E"(2) "encoders-are-abstract" "existential:2[const_var]" "→E")
190      AOT_hence notOy: ¬O!y
191        using "≡E"(1) "oa-contingent:3" by blast
192      {
193        AOT_assume Ax: A!x
194        {
195          fix F
196          {
197            AOT_assume u([F]u  [G]u)
198            AOT_hence F E G
199              by (AOT_subst F E G u([F]u  [G]u))
200                 (auto intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
201            AOT_hence x[F]  x[G]
202              using 0[THEN "∀E"(2)] "≡E" "→E" by meson
203            AOT_hence ¬x[F]
204              using G_prop "&E" "≡E" by blast
205          }
206          AOT_hence u([F]u  [G]u)  ¬x[F]
207            by (rule "→I")
208        }
209        AOT_hence x_prop: F(u([F]u  [G]u)  ¬x[F])
210          by (rule GEN)
211        AOT_have x_prop: ¬F(u([F]u  [G]u) & x[F]) 
212        proof (rule "raa-cor:2")
213          AOT_assume F(u ([F]u  [G]u) & x[F])
214          then AOT_obtain F where F_prop: u ([F]u  [G]u) & x[F]
215            using "∃E"[rotated] by blast
216          AOT_have ([F]u  [G]u) for u
217            using F_prop[THEN "&E"(1), THEN "Ordinary.∀E"].
218          AOT_hence u ([F]u  [G]u)
219            by (rule Ordinary.GEN)
220          AOT_hence u([F]u  [G]u)
221            by (metis "Ordinary.res-var-bound-reas[BF]" "→E")
222          AOT_hence ¬x[F]
223            using x_prop[THEN "∀E"(2), THEN "→E"] by blast
224          AOT_thus p & ¬p for p
225            using F_prop[THEN "&E"(2)] by (metis "raa-cor:3")
226        qed
227        AOT_have y_prop: F(u ([F]u  [G]u) & y[F])
228        proof (rule "raa-cor:1")
229          AOT_assume ¬F (u ([F]u  [G]u) & y[F])
230          AOT_hence 0: F ¬(u ([F]u  [G]u) & y[F])
231            using "cqt-further:4"[THEN "→E"] by blast
232          {
233            fix F
234            {
235              AOT_assume u ([F]u  [G]u)
236              AOT_hence ¬y[F]
237                using 0[THEN "∀E"(2)] "&I" "raa-cor:1" by meson
238            }
239            AOT_hence (u ([F]u  [G]u)  ¬y[F])
240              by (rule "→I")
241          }
242          AOT_hence A: F(u ([F]u  [G]u)  ¬y[F])
243            by (rule GEN)
244          moreover AOT_have u ([G]u  [G]u)
245            by (simp add: RN "oth-class-taut:3:a" "universal-cor" "→I")
246          ultimately AOT_have ¬y[G]
247            using "∀E"(2) "→E" by blast
248          AOT_thus p & ¬p for p
249            using G_prop "&E" by (metis "raa-cor:3")
250        qed
251        AOT_have F([F]x & ¬[F]y)
252        proof(rule "raa-cor:1")
253          AOT_assume ¬F([F]x & ¬[F]y)
254          AOT_hence indist: F ([F]x  [F]y)
255            using indistI by blast
256          AOT_thus F(u ([F]u  [G]u) & x[F]) & ¬F(u ([F]u  [G]u) & x[F])
257            using indistinguishable_ord_enc_ex[axiom_inst, THEN "→E", OF "&I",
258                    OF "&I", OF "&I", OF "cqt:2[const_var]"[axiom_inst],
259                    OF Ax, OF Ay, OF indist, THEN "≡E"(2), OF y_prop]
260                x_prop "&I" by blast
261        qed
262      }
263      moreover {
264        AOT_assume notAx: ¬A!x
265        AOT_hence Ox: O!x
266          using "∨E"(3) "oa-exist:3" by blast
267        AOT_have F([F]x & ¬[F]y)
268          apply (rule "∃I"(1)[where τ=«O!»])
269          using Ox notOy "&I" apply blast
270          by (simp add: "oa-exist:1")
271      }
272      ultimately AOT_have F([F]x & ¬[F]y)
273        by (metis "raa-cor:1")
274    }
275    ultimately AOT_show F([F]x & ¬[F]y)
276      using G_prop by (metis "&I" "→I" "≡I" "raa-cor:1")
277  }
278  qed
279
280  AOT_modally_strict {
281    fix x y
282    AOT_assume indist: F ([F]x  [F]y)
283    AOT_hence nec_indist: F ([F]x  [F]y) 
284      using "ind-nec" "vdash-properties:10" by blast
285    AOT_hence indist_nec: F ([F]x  [F]y)
286      using "CBF" "vdash-properties:10" by blast
287    AOT_assume 0: G (G E F  x[G])
288    AOT_hence 1: G (u ([G]u  [F]u)  x[G])
289      by (AOT_subst (reverse) u ([G]u  [F]u) G E F for: G)
290         (auto intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
291    AOT_have x[F]
292      by (safe intro!: 1[THEN "∀E"(2), THEN "→E"] GEN "→I" RN "≡I")
293    AOT_have G (G E F  y[G])
294    proof(rule "raa-cor:1")
295      AOT_assume ¬G (G E F  y[G])
296      AOT_hence G ¬(G E F  y[G])
297        using "cqt-further:2" "→E" by blast
298      then AOT_obtain G where G_prop: ¬(G E F  y[G])
299        using "∃E"[rotated] by blast
300      AOT_hence 1: G E F & ¬y[G]
301        by (metis "≡E"(1) "oth-class-taut:1:b")
302      AOT_have xG: x[G]
303        using 0[THEN "∀E"(2), THEN "→E"] 1[THEN "&E"(1)] by blast
304      AOT_hence x[G] & ¬y[G]
305        using 1[THEN "&E"(2)] "&I" by blast
306      AOT_hence B: ¬(x[G]  y[G])
307        using "&E"(2) "≡E"(1) "reductio-aa:1" xG by blast
308      {
309        fix H
310        {
311          AOT_assume H E G
312          AOT_hence (H E G & G E F)
313            using 1 by (metis "KBasic:3" "con-dis-i-e:1" "con-dis-i-e:2:a"
314                              "intro-elim:3:b")
315          moreover AOT_have (H E G & G E F)  (H E F)
316          proof(rule RM)
317            AOT_modally_strict {
318              AOT_show H E G & G E F  H E F
319              proof (safe intro!: "→I" "eqE"[THEN "dfI"] "&I" "cqt:2" Ordinary.GEN)
320                fix u
321                AOT_assume H E G & G E F
322                AOT_hence u ([H]u  [G]u) and u ([G]u  [F]u)
323                  using "eqE"[THEN "dfE"] "&E" by blast+
324                AOT_thus [H]u  [F]u
325                  by (auto dest!: "Ordinary.∀E" dest: "≡E")
326              qed
327            }
328          qed
329          ultimately AOT_have (H E F)
330            using "→E" by blast
331          AOT_hence x[H]
332            using 0[THEN "∀E"(2)] "→E" by blast
333          AOT_hence x[H]  x[G]
334            using xG "≡I" "→I" by blast
335        }
336        AOT_hence H E G  (x[H]  x[G]) by (rule "→I")
337      }
338      AOT_hence A: H(H E G  (x[H]  x[G]))
339        by (rule GEN)
340      then AOT_obtain F where F_prop: [F]x & ¬[F]y
341        using Aux[OF A, OF B] "∃E"[rotated] by blast
342      moreover AOT_have [F]y
343        using indist[THEN "∀E"(2), THEN "≡E"(1), OF F_prop[THEN "&E"(1)]].
344      AOT_thus p & ¬p for p
345        using F_prop[THEN "&E"(2)] by (metis "raa-cor:3")
346    qed
347  } note 0 = this
348  AOT_modally_strict {
349    fix x y
350    AOT_assume F ([F]x  [F]y)
351    moreover AOT_have F ([F]y  [F]x)
352      by (metis calculation "cqt-basic:11" "≡E"(2))
353    ultimately AOT_have G (G E F  x[G])  G (G E F  y[G])
354      using 0 "≡I" "→I" by auto
355  } note 1 = this
356  AOT_show x G (G E F  x[G])]
357    by (safe intro!: RN GEN "→I" 1 "kirchner-thm:2"[THEN "≡E"(2)])
358
359  AOT_modally_strict {
360    fix x y
361    AOT_assume indist: F ([F]x  [F]y)
362    AOT_hence nec_indist: F ([F]x  [F]y) 
363      using "ind-nec" "vdash-properties:10" by blast
364    AOT_hence indist_nec: F ([F]x  [F]y)
365      using "CBF" "vdash-properties:10" by blast
366    AOT_assume 0: G (G E F  ¬x[G])
367    AOT_hence 1: G (u ([G]u  [F]u)  ¬x[G])
368      by (AOT_subst (reverse) u ([G]u  [F]u) G E F for: G)
369         (auto intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
370    AOT_have ¬x[F]
371      by (safe intro!: 1[THEN "∀E"(2), THEN "→E"] GEN "→I" RN "≡I")
372    AOT_have G (G E F  ¬y[G])
373    proof(rule "raa-cor:1")
374      AOT_assume ¬G (G E F  ¬y[G])
375      AOT_hence G ¬(G E F  ¬y[G])
376        using "cqt-further:2" "→E" by blast
377      then AOT_obtain G where G_prop: ¬(G E F  ¬y[G])
378        using "∃E"[rotated] by blast
379      AOT_hence 1: G E F & ¬¬y[G]
380        by (metis "≡E"(1) "oth-class-taut:1:b")
381      AOT_hence yG: y[G]
382        using G_prop "→I" "raa-cor:3" by blast
383      moreover AOT_hence 12: ¬x[G]
384        using 0[THEN "∀E"(2), THEN "→E"] 1[THEN "&E"(1)] by blast
385      ultimately AOT_have ¬x[G] & y[G]
386        using "&I" by blast
387      AOT_hence B: ¬(x[G]  y[G])
388        by (metis "12" "≡E"(3) "raa-cor:3" yG)
389      {
390        fix H
391        {
392          AOT_assume 3: H E G
393          AOT_hence (H E G & G E F)
394            using 1
395            by (metis "KBasic:3" "con-dis-i-e:1" "→I" "intro-elim:3:b"
396                      "reductio-aa:1" G_prop)
397          moreover AOT_have (H E G & G E F)  (H E F)
398          proof (rule RM)
399            AOT_modally_strict {
400              AOT_show H E G & G E F  H E F
401              proof (safe intro!: "→I" "eqE"[THEN "dfI"] "&I" "cqt:2" Ordinary.GEN)
402                fix u
403                AOT_assume H E G & G E F
404                AOT_hence u ([H]u  [G]u) and u ([G]u  [F]u)
405                  using "eqE"[THEN "dfE"] "&E" by blast+
406                AOT_thus [H]u  [F]u
407                  by (auto dest!: "Ordinary.∀E" dest: "≡E")
408              qed
409            }
410          qed
411          ultimately AOT_have (H E F)
412            using "→E" by blast
413          AOT_hence ¬x[H]
414            using 0[THEN "∀E"(2)] "→E" by blast
415          AOT_hence x[H]  x[G]
416            using 12 "≡I" "→I" by (metis "raa-cor:3")
417        }
418        AOT_hence H E G  (x[H]  x[G])
419          by (rule "→I")
420      }
421      AOT_hence A: H(H E G  (x[H]  x[G]))
422        by (rule GEN)
423      then AOT_obtain F where F_prop: [F]x & ¬[F]y
424        using Aux[OF A, OF B] "∃E"[rotated] by blast
425      moreover AOT_have [F]y
426        using indist[THEN "∀E"(2), THEN "≡E"(1), OF F_prop[THEN "&E"(1)]].
427      AOT_thus p & ¬p for p
428        using F_prop[THEN "&E"(2)] by (metis "raa-cor:3")
429    qed
430  } note 0 = this
431  AOT_modally_strict {
432    fix x y
433    AOT_assume F ([F]x  [F]y)
434    moreover AOT_have F ([F]y  [F]x)
435      by (metis calculation "cqt-basic:11" "≡E"(2))
436    ultimately AOT_have G (G E F  ¬x[G])  G (G E F  ¬y[G])
437      using 0 "≡I" "→I" by auto
438  } note 1 = this
439  AOT_show x G (G E F  ¬x[G])]
440    by (safe intro!: RN GEN "→I" 1 "kirchner-thm:2"[THEN "≡E"(2)])
441qed
442
443textReformulate the existence claims in terms of their negations.
444
445AOT_theorem denotes_ex: x G (G E F & x[G])]
446proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
447  AOT_show x ¬G (G E F  ¬x[G])]
448    using denotes_all_neg[THEN negation_denotes[THEN "→E"]].
449next
450  AOT_show x (¬G (G E F  ¬x[G])  G (G E F & x[G]))
451    by (AOT_subst  G E F & x[G] ¬(G E F  ¬x[G]) for: G x)
452       (auto simp: "conventions:1" "rule-eq-df:1"
453             intro: "oth-class-taut:4:b"[THEN "≡E"(2)]
454                    "intro-elim:3:f"[OF "cqt-further:3", OF "oth-class-taut:3:b"]
455             intro!: RN GEN)
456qed
457
458AOT_theorem denotes_ex_neg: x G (G E F & ¬x[G])]
459proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
460  AOT_show x ¬G (G E F  x[G])]
461    using denotes_all[THEN negation_denotes[THEN "→E"]].
462next
463  AOT_show x (¬G (G E F  x[G])  G (G E F & ¬x[G]))
464    by (AOT_subst (reverse) G E F & ¬x[G] ¬(G E F  x[G]) for: G x)
465       (auto simp: "oth-class-taut:1:b"
466             intro: "oth-class-taut:4:b"[THEN "≡E"(2)]
467                    "intro-elim:3:f"[OF "cqt-further:3", OF "oth-class-taut:3:b"]
468             intro!: RN GEN)
469qed
470
471textDerive comprehension principles.
472
473AOT_theorem Comprehension_1:
474  shows FG(G E F  (φ{F}  φ{G}))  x F (φ{F} & x[F])]
475proof(rule "→I")
476  AOT_assume assm: FG(G E F  (φ{F}  φ{G}))
477  AOT_modally_strict {
478    fix x y
479    AOT_assume 0: FG (G E F  (φ{F}  φ{G}))
480    AOT_assume indist: F ([F]x  [F]y)
481    AOT_assume x_prop: F (φ{F} & x[F])
482    then AOT_obtain F where F_prop: φ{F} & x[F]
483      using "∃E"[rotated] by blast
484    AOT_hence F E F & x[F]
485      by (auto intro!: RN eqE[THEN "dfI"] "&I" "cqt:2" GEN "≡I" "→I" dest: "&E")
486    AOT_hence G(G E F & x[G])
487      by (rule "∃I")
488    AOT_hence x G(G E F & x[G])]x
489      by (safe intro!: "β←C" denotes_ex "cqt:2")
490    AOT_hence x G(G E F & x[G])]y
491      using indist[THEN "∀E"(1), OF denotes_ex, THEN "≡E"(1)] by blast
492    AOT_hence G(G E F & y[G])
493      using "β→C" by blast
494    then AOT_obtain G where G E F & y[G]
495      using "∃E"[rotated] by blast
496    AOT_hence φ{G} & y[G]
497      using 0[THEN "∀E"(2), THEN "∀E"(2), THEN "→E", THEN "≡E"(1)]
498            F_prop[THEN "&E"(1)] "&E" "&I" by blast
499    AOT_hence F (φ{F} & y[F])
500      by (rule "∃I")
501  } note 1 = this
502  AOT_modally_strict {
503    AOT_assume 0: FG (G E F  (φ{F}  φ{G}))
504    {
505      fix x y
506      {
507        AOT_assume F ([F]x  [F]y)
508        moreover AOT_have F ([F]y  [F]x)
509          by (metis calculation "cqt-basic:11" "≡E"(1))
510        ultimately AOT_have F (φ{F} & x[F])  F (φ{F} & y[F])
511          using 0 1[OF 0] "≡I" "→I" by simp
512      }
513      AOT_hence F ([F]x  [F]y)  (F (φ{F} & x[F])  F (φ{F} & y[F]))
514        using "→I" by blast
515    }
516    AOT_hence xy(F ([F]x  [F]y)  (F (φ{F} & x[F])   F (φ{F} & y[F])))
517      by (auto intro!: GEN)
518  } note 1 = this
519  AOT_hence  FG (G E F  (φ{F}  φ{G})) 
520                xy(F ([F]x  [F]y)  (F (φ{F} & x[F])  F (φ{F} & y[F])))
521    by (rule "→I")
522  AOT_hence FG (G E F  (φ{F}  φ{G})) 
523             xy(F ([F]x  [F]y)  (F (φ{F} & x[F])  F (φ{F} & y[F])))
524    by (rule RM)
525  AOT_hence xy(F ([F]x  [F]y)  (F (φ{F} & x[F])  F (φ{F} & y[F])))
526    using "→E" assm by blast
527  AOT_thus x F (φ{F} & x[F])]
528    by (safe intro!: "kirchner-thm:2"[THEN "≡E"(2)])
529qed
530
531AOT_theorem Comprehension_2:
532  shows FG(G E F  (φ{F}  φ{G}))  x F (φ{F} & ¬x[F])]
533proof(rule "→I")
534  AOT_assume assm: FG(G E F  (φ{F}  φ{G}))
535  AOT_modally_strict {
536    fix x y
537    AOT_assume 0: FG (G E F  (φ{F}  φ{G}))
538    AOT_assume indist: F ([F]x  [F]y)
539    AOT_assume x_prop: F (φ{F} & ¬x[F])
540    then AOT_obtain F where F_prop: φ{F} & ¬x[F]
541      using "∃E"[rotated] by blast
542    AOT_hence F E F & ¬x[F]
543      by (auto intro!: RN eqE[THEN "dfI"] "&I" "cqt:2" GEN "≡I" "→I" dest: "&E")
544    AOT_hence G(G E F & ¬x[G])
545      by (rule "∃I")
546    AOT_hence x G(G E F & ¬x[G])]x
547      by (safe intro!: "β←C" denotes_ex_neg "cqt:2")
548    AOT_hence x G(G E F & ¬x[G])]y
549      using indist[THEN "∀E"(1), OF denotes_ex_neg, THEN "≡E"(1)] by blast
550    AOT_hence G(G E F & ¬y[G])
551      using "β→C" by blast
552    then AOT_obtain G where G E F & ¬y[G]
553      using "∃E"[rotated] by blast
554    AOT_hence φ{G} & ¬y[G]
555      using 0[THEN "∀E"(2), THEN "∀E"(2), THEN "→E", THEN "≡E"(1)]
556            F_prop[THEN "&E"(1)] "&E" "&I" by blast
557    AOT_hence F (φ{F} & ¬y[F])
558      by (rule "∃I")
559  } note 1 = this
560  AOT_modally_strict {
561    AOT_assume 0: FG (G E F  (φ{F}  φ{G}))
562    {
563      fix x y
564      {
565        AOT_assume F ([F]x  [F]y)
566        moreover AOT_have F ([F]y  [F]x)
567          by (metis calculation "cqt-basic:11" "≡E"(1))
568        ultimately AOT_have F (φ{F} & ¬x[F])  F (φ{F} & ¬y[F])
569          using 0 1[OF 0] "≡I" "→I" by simp
570      }
571      AOT_hence F ([F]x  [F]y)  (F (φ{F} & ¬x[F])  F (φ{F} & ¬y[F]))
572        using "→I" by blast
573    }
574    AOT_hence xy(F ([F]x  [F]y)  (F (φ{F} & ¬x[F])   F (φ{F} & ¬y[F])))
575      by (auto intro!: GEN)
576  } note 1 = this
577  AOT_hence  FG (G E F  (φ{F}  φ{G})) 
578                xy(F ([F]x  [F]y)  (F (φ{F} & ¬x[F])  F (φ{F} & ¬y[F])))
579    by (rule "→I")
580  AOT_hence FG (G E F  (φ{F}  φ{G})) 
581             xy(F ([F]x  [F]y)  (F (φ{F} & ¬x[F])  F (φ{F} & ¬y[F])))
582    by (rule RM)
583  AOT_hence xy(F ([F]x  [F]y)  (F (φ{F} & ¬x[F])  F (φ{F} & ¬y[F])))
584    using "→E" assm by blast
585  AOT_thus x F (φ{F} & ¬x[F])]
586    by (safe intro!: "kirchner-thm:2"[THEN "≡E"(2)])
587qed
588
589textDerived variants of the comprehension principles above.
590
591AOT_theorem Comprehension_1':
592  shows FG(G E F  (φ{F}  φ{G}))  x F (x[F]  φ{F})]
593proof(rule "→I")
594  AOT_assume FG(G E F  (φ{F}  φ{G}))
595  AOT_hence 0: FG(G E F  (¬φ{F}  ¬φ{G}))
596    by (AOT_subst (reverse) ¬φ{F}  ¬φ{G} φ{F}  φ{G} for: F G)
597       (auto simp: "oth-class-taut:4:b")
598  AOT_show x F (x[F]  φ{F})]
599  proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
600    AOT_show x ¬F(¬φ{F} & x[F])]
601      using Comprehension_1[THEN "→E", OF 0, THEN negation_denotes[THEN "→E"]].
602  next
603    AOT_show x (¬F (¬φ{F} & x[F])  F (x[F]  φ{F}))
604      by (AOT_subst (reverse) ¬φ{F} & x[F] ¬(x[F]  φ{F}) for: F x)
605         (auto simp: "oth-class-taut:1:b"[THEN "intro-elim:3:e",
606                                          OF "oth-class-taut:2:a"]
607             intro: "intro-elim:3:f"[OF "cqt-further:3", OF "oth-class-taut:3:a",
608                                     symmetric]
609             intro!: RN GEN)
610  qed
611qed
612
613AOT_theorem Comprehension_2':
614  shows FG(G E F  (φ{F}  φ{G}))  x F (φ{F}  x[F])]
615proof(rule "→I")
616  AOT_assume 0: FG(G E F  (φ{F}  φ{G}))
617  AOT_show x F (φ{F}  x[F])]
618  proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
619    AOT_show x ¬F(φ{F} & ¬x[F])]
620      using Comprehension_2[THEN "→E", OF 0, THEN negation_denotes[THEN "→E"]].
621  next
622    AOT_show x (¬F (φ{F} & ¬x[F])  F (φ{F}  x[F]))
623      by (AOT_subst (reverse) φ{F} & ¬x[F] ¬(φ{F}  x[F]) for: F x)
624         (auto simp: "oth-class-taut:1:b"
625             intro: "intro-elim:3:f"[OF "cqt-further:3", OF "oth-class-taut:3:a",
626                                     symmetric]
627             intro!: RN GEN)
628  qed
629qed
630
631textDerive a combined comprehension principles.
632
633AOT_theorem Comprehension_3:
634  FG(G E F  (φ{F}  φ{G}))  x F (x[F]  φ{F})]
635proof(rule "→I")
636  AOT_assume 0: FG(G E F  (φ{F}  φ{G}))
637  AOT_show x F (x[F]  φ{F})]
638  proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
639    AOT_show x F (x[F]  φ{F}) & F (φ{F}  x[F])]
640      by (safe intro!: conjunction_denotes[THEN "→E", OF "&I"]
641                       Comprehension_1'[THEN "→E"]
642                       Comprehension_2'[THEN "→E"] 0)
643  next
644    AOT_show x (F (x[F]  φ{F}) & F (φ{F}  x[F])  F (x[F]  φ{F}))
645      by (auto intro!: RN GEN "≡I" "→I" "&I" dest: "&E" "∀E"(2) "→E" "≡E"(1,2))
646  qed
647qed
648
649notepad
650begin
651textVerify that the original axioms are equivalent to @{thm denotes_ex}
652     and @{thm denotes_ex_neg}.
653AOT_modally_strict {
654  fix x y H
655  AOT_have A!x & A!y & F ([F]x  [F]y) 
656  (G (z (O!z  ([G]z  [H]z))  x[G]) 
657   G (z (O!z  ([G]z  [H]z))  y[G]))
658  proof(rule "→I")
659    {
660      fix x y
661      AOT_assume A!x
662      AOT_assume A!y
663      AOT_assume indist: F ([F]x  [F]y)
664      AOT_assume G (u ([G]u  [H]u)  x[G])
665      AOT_hence G (u ([G]u  [H]u)  x[G])
666        using "Ordinary.res-var-bound-reas[BF]" "Ordinary.res-var-bound-reas[CBF]"
667              "intro-elim:2"
668        by (AOT_subst u ([G]u  [H]u) u ([G]u  [H]u) for: G) auto
669      AOT_hence G (G E H  x[G])
670        by (AOT_subst G E H u ([G]u  [H]u) for: G)
671            (safe intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
672      AOT_hence ¬G (G E H & ¬x[G])
673        by (AOT_subst (reverse) (G E H & ¬x[G]) ¬(G E H  x[G]) for: G)
674           (auto simp: "oth-class-taut:1:b" "cqt-further:3"[THEN "≡E"(1)])
675      AOT_hence ¬x G (G E H & ¬x[G])]x
676        by (auto intro: "β→C")
677      AOT_hence ¬x G (G E H & ¬x[G])]y
678        using indist[THEN "∀E"(1), OF denotes_ex_neg,
679                     THEN "qml:2"[axiom_inst, THEN "→E"],
680                     THEN "≡E"(3)] by blast
681      AOT_hence ¬G (G E H & ¬y[G])
682        by (safe intro!: "β←C" denotes_ex_neg "cqt:2")
683      AOT_hence G ¬(G E H & ¬y[G])
684        using "cqt-further:4"[THEN "→E"] by blast
685      AOT_hence G(G E H  y[G])
686        by (AOT_subst G E H  y[G] ¬(G E H & ¬y[G]) for: G)
687           (auto simp: "oth-class-taut:1:a")
688      AOT_hence G (u([G]u  [H]u)  y[G])
689        by (AOT_subst (reverse) u ([G]u  [H]u) G E H for: G)
690           (safe intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2") 
691      AOT_hence G (u ([G]u  [H]u)  y[G])
692        using "Ordinary.res-var-bound-reas[BF]" "Ordinary.res-var-bound-reas[CBF]"
693              "intro-elim:2"
694        by (AOT_subst u ([G]u  [H]u) u ([G]u  [H]u) for: G) auto
695    } note 0 = this
696    AOT_assume A!x & A!y & F ([F]x  [F]y)
697    AOT_hence A!x and A!y and F ([F]x  [F]y)
698      using "&E" by blast+
699    moreover AOT_have F ([F]y  [F]x)
700      using calculation(3)
701      apply (safe intro!: CBF[THEN "→E"] dest!: BF[THEN "→E"])
702      using "RM:3" "cqt-basic:11" "intro-elim:3:b" by fast
703    ultimately AOT_show G (u ([G]u  [H]u)  x[G]) 
704                         G (u ([G]u  [H]u)  y[G])
705      using 0 by (auto intro!: "≡I" "→I")
706  qed
707  
708  AOT_have A!x & A!y & F ([F]x  [F]y) 
709  (G (z (O!z  ([G]z  [H]z)) & x[G])  G (z (O!z  ([G]z  [H]z)) & y[G]))
710  proof(rule "→I")
711    {
712      fix x y
713      AOT_assume A!x
714      AOT_assume A!y
715      AOT_assume indist: F ([F]x  [F]y)
716      AOT_assume x_prop: G (u ([G]u  [H]u) & x[G])
717      AOT_hence G (u ([G]u  [H]u) & x[G])
718        using "Ordinary.res-var-bound-reas[BF]" "Ordinary.res-var-bound-reas[CBF]"
719              "intro-elim:2"
720        by (AOT_subst u ([G]u  [H]u) u ([G]u  [H]u) for: G) auto
721      AOT_hence G (G E H & x[G])
722        by (AOT_subst G E H u ([G]u  [H]u) for: G)
723           (safe intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2") 
724      AOT_hence x G (G E H & x[G])]x
725        by (safe intro!: "β←C" denotes_ex "cqt:2")
726      AOT_hence x G (G E H & x[G])]y
727        using indist[THEN "∀E"(1), OF denotes_ex,
728                     THEN "qml:2"[axiom_inst, THEN "→E"],
729                     THEN "≡E"(1)] by blast
730      AOT_hence G (G E H & y[G])
731        by (rule "β→C")
732      AOT_hence G (u ([G]u  [H]u) & y[G])
733        by (AOT_subst (reverse) u ([G]u  [H]u) G E H for: G)
734           (safe intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2") 
735      AOT_hence G (u ([G]u  [H]u) & y[G])
736        using "Ordinary.res-var-bound-reas[BF]"
737              "Ordinary.res-var-bound-reas[CBF]"
738              "intro-elim:2"
739        by (AOT_subst u ([G]u  [H]u) u ([G]u  [H]u) for: G) auto 
740    } note 0 = this
741    AOT_assume A!x & A!y & F ([F]x  [F]y)
742    AOT_hence A!x and A!y and F ([F]x  [F]y)
743      using "&E" by blast+
744    moreover AOT_have F ([F]y  [F]x)
745      using calculation(3)
746      apply (safe intro!: CBF[THEN "→E"] dest!: BF[THEN "→E"])
747      using "RM:3" "cqt-basic:11" "intro-elim:3:b" by fast
748    ultimately AOT_show G (u ([G]u  [H]u) & x[G]) 
749                         G (u ([G]u  [H]u) & y[G])
750      using 0 by (auto intro!: "≡I" "→I")
751  qed
752}
753end
754end