Theory AOT_misc

1theory AOT_misc
2  imports AOT_NaturalNumbers
3begin
4
5AOT_theorem PossiblyNumbersEmptyPropertyImpliesZero:
6  Numbers(x,z O!z & z E z])  x = 0
7proof(rule "→I")
8  AOT_have Rigid(z O!z & z E z])
9  proof (safe intro!: "df-rigid-rel:1"[THEN "dfI"] "&I" "cqt:2";
10         rule RN; safe intro!: GEN "→I")
11    AOT_modally_strict {
12      fix x
13      AOT_assume z O!z & z E z]x
14      AOT_hence O!x & x E x by (rule "β→C")
15      moreover AOT_have x =E x using calculation[THEN "&E"(1)] 
16        by (metis "ord=Eequiv:1" "vdash-properties:10")
17      ultimately AOT_have x =E x & ¬x =E x
18        by (metis "con-dis-i-e:1" "con-dis-i-e:2:b" "intro-elim:3:a" "thm-neg=E")
19      AOT_thus z O!z & z E z]x using "raa-cor:1" by blast
20    }
21  qed
22  AOT_hence x (Numbers(x,z O!z & z E z])  Numbers(x,z O!z & z E z]))
23    by (safe intro!: "num-cont:2"[unvarify G, THEN "→E"] "cqt:2")
24  AOT_hence x (Numbers(x,z O!z & z E z])  Numbers(x,z O!z & z E z]))
25    using "BFs:2"[THEN "→E"] by blast
26  AOT_hence (Numbers(x,z O!z & z E z])  Numbers(x,z O!z & z E z]))
27    using "∀E"(2) by auto
28  moreover AOT_assume Numbers(x,z O!z & z E z])
29  ultimately AOT_have 𝒜Numbers(x,z O!z & z E z])
30    using "sc-eq-box-box:1"[THEN "≡E"(1), THEN "→E", THEN "nec-imp-act"[THEN "→E"]]
31    by blast
32  AOT_hence Numbers(x,z 𝒜z O!z & z E z]z])
33    by (safe intro!: "eq-num:1"[unvarify G, THEN "≡E"(1)] "cqt:2")
34  AOT_hence x = #z O!z & z E z]
35    by (safe intro!: "eq-num:2"[unvarify G, THEN "≡E"(1)] "cqt:2")
36  AOT_thus x = 0
37    using "cqt:2"(1) "rule-id-df:2:b[zero]" "rule=E" "zero:1" by blast
38qed
39
40AOT_define Numbers' :: τ  τ  φ (Numbers'''(_,_'))
41  Numbers'(x, G) df A!x & G & F (x[F]  F E G)
42AOT_theorem Numbers'equiv: Numbers'(x,G)  A!x & F (x[F]  F E G)
43  by (AOT_subst_def Numbers')
44     (auto intro!: "≡I" "→I" "&I" "cqt:2" dest: "&E")
45
46AOT_theorem Numbers'DistinctZeroes:
47  xy (Numbers'(x,z O!z & z E z]) & Numbers'(y,z O!z & z E z]) & x  y)
48proof -
49  AOT_obtain w1 where w w1  w
50    using "two-worlds-exist:4" "PossibleWorld.∃E"[rotated] by fast
51  then AOT_obtain w2 where distinct_worlds: w1  w2
52    using "PossibleWorld.∃E"[rotated] by blast
53  AOT_obtain x where x_prop:
54    A!x & F (x[F]  w1  F E z O!z & z E z])
55    using "A-objects"[axiom_inst] "∃E"[rotated] by fast
56  moreover AOT_obtain y where y_prop:
57    A!y & F (y[F]  w2  F E z O!z & z E z])
58    using "A-objects"[axiom_inst] "∃E"[rotated] by fast
59  moreover {
60    fix x w
61    AOT_assume x_prop: A!x & F (x[F]  w  F E z O!z & z E z])
62    AOT_have F w  (x[F]  F E z O!z & z E z])
63    proof(safe intro!: GEN "conj-dist-w:4"[unvarify p q, OF "log-prop-prop:2",
64                              OF "log-prop-prop:2",THEN "≡E"(2)] "≡I" "→I")
65      fix F
66      AOT_assume w  x[F]
67      AOT_hence x[F]
68        using "fund:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(2),
69                       OF "PossibleWorld.∃I"] by blast
70      AOT_hence x[F]
71        by (metis "en-eq:3[1]" "intro-elim:3:a")
72      AOT_thus w  (F E z O!z & z E z])
73        using x_prop[THEN "&E"(2), THEN "∀E"(2), THEN "≡E"(1)] by blast
74    next
75      fix F
76      AOT_assume w  (F E z O!z & z E z])
77      AOT_hence x[F]
78        using x_prop[THEN "&E"(2), THEN "∀E"(2), THEN "≡E"(2)] by blast
79      AOT_hence x[F]
80        using "pre-en-eq:1[1]"[THEN "→E"] by blast
81      AOT_thus w  x[F]
82        using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)]
83              "PossibleWorld.∀E" by fast
84    qed
85    AOT_hence w  F (x[F]  F E z O!z & z E z])
86      using "conj-dist-w:5"[THEN "≡E"(2)] by fast
87    moreover {
88      AOT_have z O!z & z E z]
89        by (safe intro!: RN "cqt:2")
90      AOT_hence w  z O!z & z E z]
91        using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1),
92                       THEN "PossibleWorld.∀E"] by blast
93    }
94    moreover {
95      AOT_have A!x
96        using x_prop[THEN "&E"(1)] by (metis "oa-facts:2" "→E")
97      AOT_hence w  A!x
98        using "fund:2"[unvarify p, OF "log-prop-prop:2",
99                       THEN "≡E"(1), THEN "PossibleWorld.∀E"] by blast
100    }
101    ultimately AOT_have w  (A!x & z O!z & z E z] &
102                               F (x[F]  F E z O!z & z E z]))
103      using "conj-dist-w:1"[unvarify p q, OF "log-prop-prop:2",
104              OF "log-prop-prop:2", THEN "≡E"(2), OF "&I"] by auto
105    AOT_hence w w  (A!x & z O!z & z E z] &
106                        F (x[F]  F E z O!z & z E z]))
107      using "PossibleWorld.∃I" by auto
108    AOT_hence (A!x & z O!z & z E z] & F (x[F]  F E z O!z & z E z]))
109      using "fund:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(2)] by blast
110    AOT_hence Numbers'(x,z O!z & z E z])
111      by (AOT_subst_def Numbers')
112  }
113  ultimately AOT_have Numbers'(x,z O!z & z E z])
114                  and Numbers'(y,z O!z & z E z])
115    by auto
116  moreover AOT_have x  y
117  proof (rule "ab-obey:2"[THEN "→E"])
118    AOT_have ¬u z O!z & z E z]u
119    proof (safe intro!: RN "raa-cor:2")
120      AOT_modally_strict {
121        AOT_assume u z O!z & z E z]u
122        then AOT_obtain u where z O!z & z E z]u
123          using "Ordinary.∃E"[rotated] by blast
124        AOT_hence O!u & u E u
125          by (rule "β→C")
126        AOT_hence ¬(u =E u)
127          by (metis "con-dis-taut:2" "intro-elim:3:d" "modus-tollens:1"
128                    "raa-cor:3" "thm-neg=E")
129        AOT_hence u =E u & ¬u =E u
130          by (metis "modus-tollens:1" "ord=Eequiv:1" "raa-cor:3" Ordinary.ψ)
131        AOT_thus p & ¬p for p
132          by (metis "raa-cor:1")
133      }
134    qed
135    AOT_hence nec_not_ex: w w  ¬u z O!z & z E z]u
136      using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] by blast
137    AOT_have (y p]x  p) for x p
138      by (safe intro!: RN "beta-C-meta"[THEN "→E"] "cqt:2")
139    AOT_hence w w  (y p]x  p) for x p
140      using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] by blast
141    AOT_hence world_prop_beta: w (w  y p]x  w  p) for x p
142      using "conj-dist-w:4"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)]
143            "PossibleWorld.∀E" "PossibleWorld.∀I" by meson
144
145    AOT_have p (w1  p & ¬w2  p)
146    proof(rule "raa-cor:1")
147      AOT_assume 0: ¬p (w1  p & ¬w2  p)
148      AOT_have 1: w1  p  w2  p for p
149      proof(safe intro!: GEN "→I")
150        AOT_assume w1  p
151        AOT_thus w2  p
152          using 0 "con-dis-i-e:1" "∃I"(2) "raa-cor:4" by fast
153      qed
154      moreover AOT_have w2  p  w1  p for p
155      proof(safe intro!: GEN "→I")
156        AOT_assume w2  p
157        AOT_hence ¬w2  ¬p
158          using "coherent:2" "intro-elim:3:a" by blast
159        AOT_hence ¬w1  ¬p
160          using 1["∀I" p, THEN "∀E"(1), OF "log-prop-prop:2"]
161          by (metis "modus-tollens:1")
162        AOT_thus w1  p
163          using "coherent:1" "intro-elim:3:b" "reductio-aa:1" by blast
164      qed
165      ultimately AOT_have w1  p  w2  p for p
166        by (metis "intro-elim:2")
167      AOT_hence w1 = w2
168        using "sit-identity"[unconstrain s, THEN "→E",
169            OF PossibleWorld.ψ[THEN "world:1"[THEN "dfE"], THEN "&E"(1)],
170            unconstrain s', THEN "→E",
171            OF PossibleWorld.ψ[THEN "world:1"[THEN "dfE"], THEN "&E"(1)],
172            THEN "≡E"(2)] GEN by fast
173      AOT_thus w1 = w2 & ¬w1 = w2
174        using  "=-infix" "dfE" "con-dis-i-e:1" distinct_worlds by blast
175    qed
176    then AOT_obtain p where 0: w1  p & ¬w2  p
177      using "∃E"[rotated] by blast
178    AOT_have yy p]
179    proof (safe intro!: y_prop[THEN "&E"(2), THEN "∀E"(1), THEN "≡E"(2)] "cqt:2")
180      AOT_show w2  y p] E z O!z & z E z]
181      proof (safe intro!:  "cqt:2" "empty-approx:1"[unvarify F H, THEN RN,
182                  THEN "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)],
183                  THEN "PossibleWorld.∀E",
184                  THEN "conj-dist-w:2"[unvarify p q, OF "log-prop-prop:2",
185                                       OF "log-prop-prop:2", THEN "≡E"(1)],
186                                       THEN "→E"]
187                  "conj-dist-w:1"[unvarify p q, OF "log-prop-prop:2",
188                                  OF "log-prop-prop:2", THEN "≡E"(2)] "&I")
189        AOT_have ¬w2  u y p]u
190        proof (rule "raa-cor:2")
191          AOT_assume w2  u y p]u
192          AOT_hence x w2  (O!x & y p]x)
193            by (metis "conj-dist-w:6" "intro-elim:3:a")
194          then AOT_obtain x where w2  (O!x & y p]x)
195            using "∃E"[rotated] by blast
196          AOT_hence w2  y p]x
197            using "conj-dist-w:1"[unvarify p q, OF "log-prop-prop:2",
198                    OF "log-prop-prop:2", THEN "≡E"(1), THEN "&E"(2)] by blast
199          AOT_hence w2  p
200            using world_prop_beta[THEN "PossibleWorld.∀E", THEN "≡E"(1)] by blast
201          AOT_thus w2  p & ¬w2  p
202            using 0[THEN "&E"(2)] "&I" by blast
203        qed
204        AOT_thus w2  ¬u y p]u
205          by (safe intro!: "coherent:1"[unvarify p, OF "log-prop-prop:2",
206                                        THEN "≡E"(2)])
207      next
208        AOT_show w2  ¬v z O!z & z E z]v
209          using nec_not_ex[THEN "PossibleWorld.∀E"] by blast
210      qed
211    qed
212    moreover AOT_have ¬xy p]
213    proof(rule "raa-cor:2")
214      AOT_assume xy p]
215      AOT_hence "w1  y p] E z O!z & z E z]"
216        using x_prop[THEN "&E"(2), THEN "∀E"(1), THEN "≡E"(1)]
217              "prop-prop2:2" by blast
218      AOT_hence "¬w1  ¬y p] E z O!z & z E z]"
219        using "coherent:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] by blast
220      moreover AOT_have "w1  ¬(y p] E z O!z & z E z])"
221      proof (safe intro!: "cqt:2" "empty-approx:2"[unvarify F H, THEN RN,
222                    THEN "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)],
223                    THEN "PossibleWorld.∀E",
224                    THEN "conj-dist-w:2"[unvarify p q, OF "log-prop-prop:2",
225                        OF "log-prop-prop:2", THEN "≡E"(1)], THEN "→E"]
226                    "conj-dist-w:1"[unvarify p q, OF "log-prop-prop:2",
227                                    OF "log-prop-prop:2", THEN "≡E"(2)] "&I")
228        fix u
229        AOT_have w1  O!u
230          using Ordinary.ψ[THEN RN,
231                  THEN "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)],
232                  THEN "PossibleWorld.∀E"] by simp
233        moreover AOT_have w1  y p]u
234          by (safe intro!: world_prop_beta[THEN "PossibleWorld.∀E", THEN "≡E"(2)]
235                           0[THEN "&E"(1)])
236        ultimately AOT_have w1  (O!u & y p]u)
237          using "conj-dist-w:1"[unvarify p q, OF "log-prop-prop:2",
238                                OF "log-prop-prop:2", THEN "≡E"(2),
239                                OF "&I"] by blast
240        AOT_hence x w1  (O!x & y p]x)
241          by (rule "∃I")
242        AOT_thus w1  u y p]u
243          by (metis "conj-dist-w:6" "intro-elim:3:b")
244      next
245        AOT_show w1  ¬v z O!z & z E z]v
246          using "PossibleWorld.∀E" nec_not_ex by fastforce
247      qed
248      ultimately AOT_show p & ¬p for p
249        using "raa-cor:3" by blast
250    qed
251    ultimately AOT_have yy p] & ¬xy p]
252      using "&I" by blast
253    AOT_hence F (y[F] & ¬x[F])
254      by (metis "existential:1" "prop-prop2:2")
255    AOT_thus F (x[F] & ¬y[F])  F (y[F] & ¬x[F])
256      by (rule "∨I")
257  qed
258  ultimately AOT_have Numbers'(x,z O!z & z E z]) &
259                       Numbers'(y,z O!z & z E z]) & x  y
260    using "&I" by blast
261  AOT_thus xy (Numbers'(x,z O!z & z E z]) &
262                  Numbers'(y,z O!z & z E z]) & x  y)
263    using "∃I"(2)[where β=x] "∃I"(2)[where β=y] by auto
264qed
265
266AOT_theorem restricted_identity:
267  x =⇩ y  (InDomainOf(x,) & InDomainOf(y,) & x = y)
268  by (auto intro!: "≡I" "→I" "&I"
269             dest: "id-R-thm:2"[THEN "→E"] "&E"
270                   "id-R-thm:3"[THEN "→E"]
271                   "id-R-thm:4"[THEN "→E", OF "∨I"(1), THEN "≡E"(2)])
272
273AOT_theorem induction': F ([F]0 & n([F]n  [F]n')  n [F]n)
274proof(rule GEN; rule "→I")
275  fix F n
276  AOT_assume A: [F]0 & n([F]n  [F]n')
277  AOT_have nm([]nm  ([F]n  [F]m))
278  proof(safe intro!: "Number.GEN" "→I")
279    fix n m
280    AOT_assume []nm
281    moreover AOT_have []n n'
282      using "suc-thm".
283    ultimately AOT_have m_eq_suc_n: m = n'
284      using "pred-func:1"[unvarify z, OF "def-suc[den2]", THEN "→E", OF "&I"]
285      by blast
286    AOT_assume [F]n
287    AOT_hence [F]n'
288      using A[THEN "&E"(2), THEN "Number.∀E", THEN "→E"] by blast
289    AOT_thus [F]m
290      using m_eq_suc_n[symmetric] "rule=E" by fast
291  qed
292  AOT_thus n[F]n
293    using induction[THEN "∀E"(2), THEN "→E", OF "&I", OF A[THEN "&E"(1)]]
294    by simp
295qed
296
297AOT_define ExtensionOf :: τ  Π  φ (ExtensionOf'(_,_'))
298  "exten-property:1": ExtensionOf(x,[G]) df A!x & G & F(x[F]  z([F]z  [G]z))
299
300AOT_define OrdinaryExtensionOf :: τ  Π  φ (OrdinaryExtensionOf'(_,_'))
301   OrdinaryExtensionOf(x,[G]) df A!x & G & F(x[F]  z(O!z  ([F]z  [G]z)))
302
303AOT_theorem BeingOrdinaryExtensionOfDenotes:
304  x OrdinaryExtensionOf(x,[G])]
305proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
306  AOT_show x A!x & G & x F(x[F]  z(O!z  ([F]z  [G]z)))]x]
307    by "cqt:2"
308next
309  AOT_show x (A!x & G & x F (x[F]  z (O!z  ([F]z  [G]z)))]x 
310            OrdinaryExtensionOf(x,[G]))
311  proof(safe intro!: RN GEN)
312    AOT_modally_strict {
313      fix x
314      AOT_modally_strict {
315        AOT_have x F (x[F]  z (O!z  ([F]z  [G]z)))]
316        proof (safe intro!: "Comprehension_3"[THEN "→E"] RN GEN
317                            "→I" "≡I" Ordinary.GEN)
318          AOT_modally_strict {
319            fix F H u
320            AOT_assume H E F
321            AOT_hence u([H]u  [F]u)
322              using eqE[THEN "dfE", THEN "&E"(2)] "qml:2"[axiom_inst, THEN "→E"]
323              by blast
324            AOT_hence 0: [H]u  [F]u using "Ordinary.∀E" by fast
325            {
326              AOT_assume u([F]u  [G]u)
327              AOT_hence 1: [F]u  [G]u using "Ordinary.∀E" by fast
328              AOT_show [G]u if [H]u using 0 1 "≡E"(1) that by blast
329              AOT_show [H]u if [G]u using 0 1 "≡E"(2) that by blast
330            }
331            {
332              AOT_assume u([H]u  [G]u)
333              AOT_hence 1: [H]u  [G]u using "Ordinary.∀E" by fast
334              AOT_show [G]u if [F]u using 0 1 "≡E"(1,2) that by blast 
335              AOT_show [F]u if [G]u using 0 1 "≡E"(1,2) that by blast 
336            }
337          }
338        qed
339      }
340      AOT_thus (A!x & G & x F (x[F]  z (O!z  ([F]z  [G]z)))]x) 
341                OrdinaryExtensionOf(x,[G])
342        apply (AOT_subst_def OrdinaryExtensionOf)
343        apply (AOT_subst x F (x[F]  z (O!z  ([F]z  [G]z)))]x
344                         F (x[F]  z (O!z  ([F]z  [G]z))))
345        by (auto intro!: "beta-C-meta"[THEN "→E"] simp: "oth-class-taut:3:a")
346    }
347  qed
348qed
349
350textFragments of PLM's theory of Concepts.
351
352AOT_define FimpG :: Π  Π  φ (infixl  50)
353  "F-imp-G": [G]  [F] df F & G & x ([G]x  [F]x)
354
355AOT_define concept :: Π (C!)
356  concepts: C! =df A!
357
358AOT_register_rigid_restricted_type
359  Concept: C!κ
360proof
361  AOT_modally_strict {
362    AOT_have x A!x
363      using "o-objects-exist:2" "qml:2"[axiom_inst] "→E" by blast
364    AOT_thus x C!x
365      using "rule-id-df:1[zero]"[OF concepts, OF "oa-exist:2"] "rule=E" id_sym
366      by fast
367  }
368next
369  AOT_modally_strict {
370    AOT_show C!κ  κ for κ
371      using "cqt:5:a"[axiom_inst, THEN "→E", THEN "&E"(2)] "→I"
372      by blast
373  }
374next
375  AOT_modally_strict {
376    AOT_have x(A!x  A!x)
377      by (simp add: "oa-facts:2" GEN)
378    AOT_thus x(C!x  C!x)
379      using "rule-id-df:1[zero]"[OF concepts, OF "oa-exist:2"] "rule=E" id_sym
380      by fast
381  }
382qed
383
384AOT_register_variable_names
385  Concept: c d e
386
387AOT_theorem "concept-comp:1": x(C!x & F(x[F]  φ{F}))
388    using concepts[THEN "rule-id-df:1[zero]", OF "oa-exist:2", symmetric]
389          "A-objects"[axiom_inst]
390          "rule=E" by fast
391
392AOT_theorem "concept-comp:2": ∃!x(C!x & F(x[F]  φ{F}))
393    using concepts[THEN "rule-id-df:1[zero]", OF "oa-exist:2", symmetric]
394          "A-objects!"
395          "rule=E" by fast
396
397AOT_theorem "concept-comp:3": ιx(C!x & F(x[F]  φ{F}))
398  using "concept-comp:2" "A-Exists:2"[THEN "≡E"(2)] "RA[2]" by blast
399
400AOT_theorem "concept-comp:4":
401  ιx(C!x & F(x[F]  φ{F})) = ιx(A!x & F(x[F]  φ{F}))
402    using "=I"(1)[OF "concept-comp:3"]
403          "rule=E"[rotated]
404          concepts[THEN "rule-id-df:1[zero]", OF "oa-exist:2"]
405          by fast
406
407AOT_define conceptInclusion :: τ  τ  φ (infixl  100)
408  "con:1": c  d df F(c[F]  d[F])
409
410
411AOT_define conceptOf :: τ  τ  φ (ConceptOf'(_,_'))
412  "concept-of-G": ConceptOf(c,G) df G & F (c[F]  [G]  [F])
413
414AOT_theorem ConceptOfOrdinaryProperty: ([H]  O!)  x ConceptOf(x,H)]
415proof(rule "→I")
416  AOT_assume [H]  O!
417  AOT_hence x([H]x  O!x)
418    using "F-imp-G"[THEN "dfE"] "&E" by blast
419  AOT_hence x([H]x  O!x)
420    using "S5Basic:6"[THEN "≡E"(1)] by blast
421  moreover AOT_have x([H]x  O!x) 
422                     FG((G E F)  ([H]  [F]  [H]  [G]))
423  proof(rule RM; safe intro!: "→I" GEN "≡I")
424    AOT_modally_strict {
425      fix F G
426      AOT_assume 0: x([H]x  O!x)
427      AOT_assume G E F
428      AOT_hence 1: u([G]u  [F]u)
429        by (AOT_subst_thm eqE[THEN "≡Df", THEN "≡S"(1), OF "&I",
430              OF "cqt:2[const_var]"[axiom_inst],
431              OF "cqt:2[const_var]"[axiom_inst], symmetric])
432      {
433        AOT_assume [H]  [F]
434        AOT_hence x([H]x  [F]x)
435          using "F-imp-G"[THEN "dfE"] "&E" by blast
436        moreover AOT_modally_strict {
437          AOT_assume x([H]x  O!x)
438          moreover AOT_assume u([G]u  [F]u)
439          moreover AOT_assume x([H]x  [F]x)
440          ultimately AOT_have [H]x  [G]x for x
441            by (auto intro!: "→I" dest!: "∀E"(2) dest: "→E" "≡E")
442          AOT_hence x([H]x  [G]x)
443            by (rule GEN)
444        }
445        ultimately AOT_have x([H]x  [G]x)
446          using "RN[prem]"[where
447              Γ="{«x([H]x  O!x)», «u([G]u  [F]u)», «x([H]x  [F]x)»}"]
448          using 0 1 by fast
449        AOT_thus [H]  [G]
450          by (AOT_subst_def "F-imp-G")
451             (safe intro!: "cqt:2" "&I")
452      }
453      {
454        AOT_assume [H]  [G]
455        AOT_hence x([H]x  [G]x)
456          using "F-imp-G"[THEN "dfE"] "&E" by blast
457        moreover AOT_modally_strict {
458          AOT_assume x([H]x  O!x)
459          moreover AOT_assume u([G]u  [F]u)
460          moreover AOT_assume x([H]x  [G]x)
461          ultimately AOT_have [H]x  [F]x for x
462            by (auto intro!: "→I" dest!: "∀E"(2) dest: "→E" "≡E")
463          AOT_hence x([H]x  [F]x)
464            by (rule GEN)
465        }
466        ultimately AOT_have x([H]x  [F]x)
467          using "RN[prem]"[where
468              Γ="{«x([H]x  O!x)», «u([G]u  [F]u)», «x([H]x  [G]x)»}"]
469          using 0 1 by fast
470        AOT_thus [H]  [F]
471          by (AOT_subst_def "F-imp-G")
472             (safe intro!: "cqt:2" "&I")
473      }
474    }
475  qed
476  ultimately AOT_have FG((G E F)  ([H]  [F]  [H]  [G]))
477    using "→E" by blast
478  AOT_hence 0: x F(x[F]  ([H]  [F]))]
479    using Comprehension_3[THEN "→E"] by blast
480  AOT_show x ConceptOf(x,H)]
481  proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
482    AOT_show x C!x & x F(x[F]  ([H]  [F]))]x] by "cqt:2"
483  next
484    AOT_show x (C!x & x F (x[F]  [H]  [F])]x  ConceptOf(x,H))
485    proof (rule "RN[prem]"[where Γ={«x F(x[F]  ([H]  [F]))]»}, simplified])
486      AOT_modally_strict {
487        AOT_assume 0: x F (x[F]  [H]  [F])]
488        AOT_show x (C!x & x F (x[F]  [H]  [F])]x  ConceptOf(x,H))
489        proof(safe intro!: GEN "≡I" "→I" "&I")
490          fix x
491          AOT_assume C!x & x F (x[F]  [H]  [F])]x
492          AOT_thus ConceptOf(x,H)
493            by (AOT_subst_def "concept-of-G")
494               (auto intro!: "&I" "cqt:2" dest: "&E" "β→C")
495        next
496          fix x
497          AOT_assume ConceptOf(x,H)
498          AOT_hence C!x & (H & F(x[F]  [H]  [F]))
499            by (AOT_subst_def (reverse) "concept-of-G")
500          AOT_thus C!x and x F(x[F]  [H]  [F])]x
501            by (auto intro!: "β←C" 0 "cqt:2" dest: "&E")
502        qed
503      }
504    next
505      AOT_show x F(x[F]  ([H]  [F]))]
506        using "exist-nec"[THEN "→E"] 0 by blast
507    qed
508  qed
509qed
510
511AOT_theorem "con-exists:1": c ConceptOf(c,G)
512proof -
513  AOT_obtain c where F (c[F]  [G]  [F])
514    using "concept-comp:1" "Concept.∃E"[rotated] by meson
515  AOT_hence ConceptOf(c,G)
516    by (auto intro!: "concept-of-G"[THEN "dfI"] "&I" "cqt:2" Concept.ψ)
517  thus ?thesis by (rule "Concept.∃I")
518qed
519
520AOT_theorem "con-exists:2": ∃!c ConceptOf(c,G)
521proof -
522  AOT_have ∃!c F (c[F]  [G]  [F])
523    using "concept-comp:2" by simp
524  moreover {
525    AOT_modally_strict {
526      fix x
527      AOT_assume F (x[F]  [G]  [F])
528      moreover AOT_have [G]  [G]
529        by (safe intro!: "F-imp-G"[THEN "dfI"] "&I" "cqt:2" RN GEN "→I")
530      ultimately AOT_have x[G]
531        using "∀E"(2) "≡E" by blast
532      AOT_hence A!x
533        using "encoders-are-abstract"[THEN "→E", OF "∃I"(2)] by simp
534      AOT_hence C!x
535        using concepts[THEN "rule-id-df:1[zero]", OF "oa-exist:2", symmetric]
536              "rule=E"[rotated]
537        by fast
538    }
539  }
540  ultimately show ?thesis
541    by (AOT_subst ConceptOf(c,G) F (c[F]  [G]  [F]) for: c;
542           AOT_subst_def "concept-of-G")
543       (auto intro!: "≡I" "→I" "&I" "cqt:2" Concept.ψ dest: "&E")
544qed
545
546AOT_theorem "con-exists:3": ιc ConceptOf(c,G)
547  by (safe intro!: "A-Exists:2"[THEN "≡E"(2)] "con-exists:2"[THEN "RA[2]"])
548
549
550AOT_define theConceptOfG :: τ  κs (c_)
551  "concept-G": cG =df ιc ConceptOf(c, G)
552
553AOT_theorem "concept-G[den]": cG
554  by (auto intro!: "rule-id-df:1"[OF "concept-G"]
555                   "t=t-proper:1"[THEN "→E"]
556                   "con-exists:3")
557
558
559AOT_theorem "concept-G[concept]": C!cG
560proof -
561  AOT_have 𝒜(C!cG & ConceptOf(cG, G))
562    by (auto intro!: "actual-desc:2"[unvarify x, THEN "→E"]
563                     "rule-id-df:1"[OF "concept-G"]
564                     "concept-G[den]"
565                     "con-exists:3")
566  AOT_hence 𝒜C!cG
567    by (metis "Act-Basic:2" "con-dis-i-e:2:a" "intro-elim:3:a")
568  AOT_hence 𝒜A!cG
569    using "rule-id-df:1[zero]"[OF concepts, OF "oa-exist:2"]
570          "rule=E" by fast
571  AOT_hence A!cG
572    using "oa-facts:8"[unvarify x, THEN "≡E"(2)] "concept-G[den]" by blast
573  thus ?thesis
574    using "rule-id-df:1[zero]"[OF concepts, OF "oa-exist:2", symmetric]
575          "rule=E" by fast
576qed
577
578AOT_theorem "conG-strict": cG = ιc F(c[F]  [G]  [F])
579proof (rule "id-eq:3"[unvarify α β γ, THEN "→E"])
580  AOT_have x (C!x & ConceptOf(x,G)  C!x & F (x[F]  [G]  [F]))
581    by (auto intro!: "concept-of-G"[THEN "dfI"] RN GEN "≡I" "→I" "&I" "cqt:2"
582               dest: "&E";
583        auto dest: "∀E"(2) "≡E"(1,2) dest!: "&E"(2) "concept-of-G"[THEN "dfE"])
584  AOT_thus cG = ιc ConceptOf(c, G) & ιc ConceptOf(c, G) = ιc F(c[F]  [G]  [F])
585    by (auto intro!: "&I" "rule-id-df:1"[OF "concept-G"] "con-exists:3"
586                      "equiv-desc-eq:3"[THEN "→E"])
587qed(auto simp: "concept-G[den]" "con-exists:3" "concept-comp:3")
588
589
590AOT_theorem "conG-lemma:1": F(cG[F]  [G]  [F])
591proof(safe intro!: GEN "≡I" "→I")
592  fix F
593  AOT_have 𝒜F(cG[F]  [G]  [F])
594    using "actual-desc:4"[THEN "→E", OF "concept-comp:3",
595                          THEN "Act-Basic:2"[THEN "≡E"(1)],
596                          THEN "&E"(2)]
597          "conG-strict"[symmetric] "rule=E" by fast
598  AOT_hence 𝒜(cG[F]  [G]  [F])
599    using "logic-actual-nec:3"[axiom_inst, THEN "≡E"(1)] "∀E"(2)
600    by blast
601  AOT_hence 0: 𝒜cG[F]  𝒜[G]  [F]
602    using "Act-Basic:5"[THEN "≡E"(1)] by blast
603  {
604    AOT_assume cG[F]
605    AOT_hence 𝒜cG[F]
606      by(safe intro!: "en-eq:10[1]"[unvarify x1, THEN "≡E"(2)]
607                      "concept-G[den]")
608    AOT_hence 𝒜[G]  [F]
609      using 0[THEN "≡E"(1)] by blast
610    AOT_hence 𝒜(F & G & x([G]x  [F]x))
611      by (AOT_subst_def (reverse) "F-imp-G")
612    AOT_hence 𝒜x([G]x  [F]x)
613      using "Act-Basic:2"[THEN "≡E"(1)] "&E" by blast
614    AOT_hence x([G]x  [F]x)
615      using "qml-act:2"[axiom_inst, THEN "≡E"(2)] by simp
616    AOT_thus [G]  [F]
617      by (AOT_subst_def "F-imp-G"; auto intro!: "&I" "cqt:2")
618  }
619  {
620    AOT_assume [G]  [F]
621    AOT_hence x([G]x  [F]x)
622      by (safe dest!: "F-imp-G"[THEN "dfE"] "&E"(2))
623    AOT_hence 𝒜x([G]x  [F]x)
624      using "qml-act:2"[axiom_inst, THEN "≡E"(1)] by simp
625    AOT_hence 𝒜(F & G & x([G]x  [F]x))
626      by (auto intro!: "Act-Basic:2"[THEN "≡E"(2)] "&I" "cqt:2"
627               intro: "RA[2]")
628    AOT_hence 𝒜([G]  [F])
629      by (AOT_subst_def "F-imp-G")
630    AOT_hence 𝒜cG[F]
631      using 0[THEN "≡E"(2)] by blast
632    AOT_thus cG[F]
633      by(safe intro!: "en-eq:10[1]"[unvarify x1, THEN "≡E"(1)]
634                      "concept-G[den]")
635  }
636qed
637
638AOT_theorem conH_enc_ord:
639  ([H]  O!)  F G (G E F  (cH[F]  cH[G]))
640proof(rule "→I")
641  AOT_assume 0: [H]  O!
642  AOT_have 0: ([H]  O!)
643    apply (AOT_subst_def "F-imp-G")
644    using 0[THEN "dfE"[OF "F-imp-G"]]
645    by (auto intro!: "KBasic:3"[THEN "≡E"(2)] "&I" "exist-nec"[THEN "→E"]
646               dest: "&E" 4[THEN "→E"])
647  moreover AOT_have ([H]  O!)  F G (G E F  (cH[F]  cH[G]))
648  proof(rule RM; safe intro!: "→I" GEN)
649    AOT_modally_strict {
650      fix F G
651      AOT_assume [H]  O!
652      AOT_hence 0: x ([H]x  O!x)
653        by (safe dest!: "F-imp-G"[THEN "dfE"] "&E"(2))
654      AOT_assume 1: G E F
655      AOT_assume cH[F]
656      AOT_hence [H]  [F]
657        using "conG-lemma:1"[THEN "∀E"(2), THEN "≡E"(1)] by simp
658      AOT_hence 2: x ([H]x  [F]x)
659        by (safe dest!: "F-imp-G"[THEN "dfE"] "&E"(2))
660      AOT_modally_strict {
661        AOT_assume 0: x ([H]x  O!x)
662        AOT_assume 1: x ([H]x  [F]x)
663        AOT_assume 2: G E F
664        AOT_have x ([H]x  [G]x)
665        proof(safe intro!: GEN "→I")
666          fix x
667          AOT_assume [H]x
668          AOT_hence O!x and [F]x
669            using 0 1 "∀E"(2) "→E" by blast+
670          AOT_thus [G]x
671            using 2[THEN eqE[THEN "dfE"], THEN "&E"(2)]
672                  "∀E"(2) "→E" "≡E"(2) calculation by blast
673        qed
674      }
675      AOT_hence x ([H]x  [G]x)
676        using "RN[prem]"[where Γ={«x ([H]x  O!x)»,
677                               «x ([H]x  [F]x)»,
678                               «G E F»}, simplified] 0 1 2 by fast
679      AOT_hence [H]  [G]
680        by (safe intro!: "F-imp-G"[THEN "dfI"] "&I" "cqt:2")
681      AOT_hence cH[G]
682        using "conG-lemma:1"[THEN "∀E"(2), THEN "≡E"(2)] by simp
683    } note 0 = this
684    AOT_modally_strict {
685      fix F G
686      AOT_assume [H]  O!
687      moreover AOT_assume G E F
688      moreover AOT_have F E G
689        by (AOT_subst F E G G E F)
690            (auto intro!: calculation(2)
691                          eqE[THEN "dfI"]
692                          "≡I" "→I" "&I" "cqt:2" Ordinary.GEN
693                  dest!: eqE[THEN "dfE"] "&E"(2)
694                  dest: "≡E"(1,2) "Ordinary.∀E")
695      ultimately AOT_show (cH[F]  cH[G])
696        using 0 "≡I" "→I" by auto
697    }
698  qed
699  ultimately AOT_show F G (G E F  (cH[F]  cH[G]))
700    using "→E" by blast
701qed
702
703AOT_theorem concept_inclusion_denotes_1:
704  ([H]  O!)  x cH  x]
705proof(rule "→I")
706  AOT_assume 0: [H]  O!
707  AOT_show x cH  x]
708  proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
709    AOT_show x C!x & F(cH[F]  x[F])]
710      by (safe intro!: conjunction_denotes[THEN "→E", OF "&I"]
711                       Comprehension_2'[THEN "→E"]
712                       conH_enc_ord[THEN "→E", OF 0]) "cqt:2"
713  next
714    AOT_show x (C!x & F (cH[F]  x[F])  cH  x)
715      by (safe intro!: RN GEN; AOT_subst_def "con:1")
716         (auto intro!: "≡I" "→I" "&I" "concept-G[concept]" dest: "&E")
717  qed
718qed
719
720AOT_theorem concept_inclusion_denotes_2:
721  ([H]  O!)  x x  cH]
722proof(rule "→I")
723  AOT_assume 0: [H]  O!
724  AOT_show x x  cH]
725  proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
726    AOT_show x C!x & F(x[F]  cH[F])]
727      by (safe intro!: conjunction_denotes[THEN "→E", OF "&I"]
728                       Comprehension_1'[THEN "→E"]
729                       conH_enc_ord[THEN "→E", OF 0]) "cqt:2"
730  next
731    AOT_show x (C!x & F (x[F]  cH[F])  x  cH)
732      by (safe intro!: RN GEN; AOT_subst_def "con:1")
733         (auto intro!: "≡I" "→I" "&I" "concept-G[concept]" dest: "&E")
734  qed
735qed
736
737AOT_define ThickForm :: τ  τ  φ (FormOf'(_,_'))
738  "tform-of": FormOf(x,G) df A!x & G & F(x[F]  [G]  [F])
739
740AOT_theorem FormOfOrdinaryProperty: ([H]  O!)  x FormOf(x,H)]
741proof(rule "→I")
742  AOT_assume 0: [H]  [O!]
743  AOT_show x FormOf(x,H)]
744  proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
745    AOT_show x ConceptOf(x,H)]
746      using 0 ConceptOfOrdinaryProperty[THEN "→E"] by blast
747    AOT_show x (ConceptOf(x,H)  FormOf(x,H))
748    proof(safe intro!: RN GEN)
749      AOT_modally_strict {
750        fix x
751        AOT_modally_strict {
752          AOT_have A!x  A!x
753            by (simp add: "oth-class-taut:3:a")
754          AOT_hence C!x  A!x
755            using "rule-id-df:1[zero]"[OF concepts, OF "oa-exist:2"]
756                  "rule=E" id_sym by fast
757        }
758        AOT_thus ConceptOf(x,H)  FormOf(x,H)
759          by (AOT_subst_def "tform-of";
760              AOT_subst_def "concept-of-G";
761              AOT_subst C!x A!x)
762             (auto intro!: "≡I" "→I" "&I" dest: "&E")
763      }
764    qed
765  qed
766qed
767
768AOT_theorem equal_E_rigid_one_to_one: Rigid1-1((=E))
769proof (safe intro!: "df-1-1:2"[THEN "dfI"] "&I" "df-1-1:1"[THEN "dfI"]
770                    GEN "→I" "df-rigid-rel:1"[THEN "dfI"] "=E[denotes]")
771  fix x y z
772  AOT_assume x =E z & y =E z
773  AOT_thus x = y
774    by (metis "rule=E" "&E"(1) "Conjunction Simplification"(2)
775              "=E-simple:2" id_sym "→E")
776next
777  AOT_have xy (x =E y  x =E y)
778  proof(rule GEN; rule GEN)
779    AOT_show (x =E y  x =E y) for x y
780      by (meson RN "deduction-theorem" "id-nec3:1" "≡E"(1))
781  qed
782  AOT_hence x1...∀xn ([(=E)]x1...xn  [(=E)]x1...xn)
783    by (rule tuple_forall[THEN "dfI"])
784  AOT_thus x1...∀xn ([(=E)]x1...xn  [(=E)]x1...xn)
785    using BF[THEN "→E"] by fast
786qed
787
788AOT_theorem equal_E_domain: InDomainOf(x,(=E))  O!x
789proof(safe intro!: "≡I" "→I")
790  AOT_assume InDomainOf(x,(=E))
791  AOT_hence y x =E y
792    by (metis "dfE" "df-1-1:5")
793  then AOT_obtain y where x =E y
794    using "∃E"[rotated] by blast
795  AOT_thus O!x
796    using "=E-simple:1"[THEN "≡E"(1)] "&E" by blast
797next
798  AOT_assume O!x
799  AOT_hence x =E x   
800    by (metis "ord=Eequiv:1"[THEN "→E"])
801  AOT_hence y x =E y
802    using "∃I"(2) by fast
803  AOT_thus InDomainOf(x,(=E))
804    by (metis "dfI" "df-1-1:5")
805qed
806
807AOT_theorem shared_urelement_projection_identity:
808  assumes y x (yz [R]zx])]
809  shows F([F]a  [F]b)  z [R]za] = z [R]zb]
810proof(rule "→I")
811  AOT_assume 0: F([F]a  [F]b)
812  {
813    fix z
814    AOT_have x (zz [R]zx])]
815      using assms[THEN "∀E"(2)].
816    AOT_hence 1: x y (F ([F]x  [F]y)  (zz [R]zx]  zz [R]zy]))
817      using "kirchner-thm-cor:1"[THEN "→E"]
818      by blast
819    AOT_have (zz [R]za]  zz [R]zb])
820      using 1[THEN "∀E"(2), THEN "∀E"(2), THEN "→E", OF 0] by blast
821  }
822  AOT_hence z (zz [R]za]  zz [R]zb])
823    by (rule GEN)
824  AOT_hence z(zz [R]za]  zz [R]zb])
825    by (rule BF[THEN "→E"])
826  AOT_thus z [R]za] = z [R]zb]
827    by (AOT_subst_def "identity:2")
828       (auto intro!: "&I" "cqt:2")
829qed
830
831AOT_theorem shared_urelement_exemplification_identity:
832  assumes y x (yz [G]x])]
833  shows F([F]a  [F]b)  ([G]a) = ([G]b)
834proof(rule "→I")
835  AOT_assume 0: F([F]a  [F]b)
836  {
837    fix z
838    AOT_have x (zz [G]x])]
839      using assms[THEN "∀E"(2)].
840    AOT_hence 1: x y (F ([F]x  [F]y)  (zz [G]x]  zz [G]y]))
841      using "kirchner-thm-cor:1"[THEN "→E"]
842      by blast
843    AOT_have (zz [G]a]  zz [G]b])
844      using 1[THEN "∀E"(2), THEN "∀E"(2), THEN "→E", OF 0] by blast
845  }
846  AOT_hence z (zz [G]a]  zz [G]b])
847    by (rule GEN)
848  AOT_hence z(zz [G]a]  zz [G]b])
849    by (rule BF[THEN "→E"])
850  AOT_hence z [G]a] = z [G]b]
851    by (AOT_subst_def "identity:2")
852       (auto intro!: "&I" "cqt:2")
853  AOT_thus ([G]a) = ([G]b)
854    by (safe intro!: "identity:4"[THEN "dfI"] "&I" "log-prop-prop:2")
855qed
856
857textThe assumptions of the theorems above are derivable, if the additional
858     introduction rules for the upcoming extension of @{thm "cqt:2[lambda]"}
859     are explicitly allowed (while they are currently not part of the
860     abstraction layer).
861notepad
862begin
863  AOT_modally_strict {
864    AOT_have Ry x (yz [R]zx])]
865      by (safe intro!: GEN "cqt:2" AOT_instance_of_cqt_2_intro_next)
866    AOT_have Gy x (yz [G]x])]
867      by (safe intro!: GEN "cqt:2" AOT_instance_of_cqt_2_intro_next)
868  }
869end
870
871end
872