Theory AOT_misc

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