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 "≡⇩d⇩fI"] "&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) ≡⇩d⇩f 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 ‹∃x∃y (◇Numbers'(x,[λz O!z & z ≠⇩E z]) & ◇Numbers'(y,[λz O!z & z ≠⇩E z]) & x ≠ y)›
50proof -
51 AOT_obtain w⇩1 where ‹∃w w⇩1 ≠ w›
52 using "two-worlds-exist:4" "PossibleWorld.∃E"[rotated] by fast
53 then AOT_obtain w⇩2 where distinct_worlds: ‹w⇩1 ≠ w⇩2›
54 using "PossibleWorld.∃E"[rotated] by blast
55 AOT_obtain x where x_prop:
56 ‹A!x & ∀F (x[F] ≡ w⇩1 ⊨ 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] ≡ w⇩2 ⊨ 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 (w⇩1 ⊨ p & ¬w⇩2 ⊨ p)›
148 proof(rule "raa-cor:1")
149 AOT_assume 0: ‹¬∃p (w⇩1 ⊨ p & ¬w⇩2 ⊨ p)›
150 AOT_have 1: ‹w⇩1 ⊨ p → w⇩2 ⊨ p› for p
151 proof(safe intro!: GEN "→I")
152 AOT_assume ‹w⇩1 ⊨ p›
153 AOT_thus ‹w⇩2 ⊨ p›
154 using 0 "con-dis-i-e:1" "∃I"(2) "raa-cor:4" by fast
155 qed
156 moreover AOT_have ‹w⇩2 ⊨ p → w⇩1 ⊨ p› for p
157 proof(safe intro!: GEN "→I")
158 AOT_assume ‹w⇩2 ⊨ p›
159 AOT_hence ‹¬w⇩2 ⊨ ¬p›
160 using "coherent:2" "intro-elim:3:a" by blast
161 AOT_hence ‹¬w⇩1 ⊨ ¬p›
162 using 1["∀I" p, THEN "∀E"(1), OF "log-prop-prop:2"]
163 by (metis "modus-tollens:1")
164 AOT_thus ‹w⇩1 ⊨ p›
165 using "coherent:1" "intro-elim:3:b" "reductio-aa:1" by blast
166 qed
167 ultimately AOT_have ‹w⇩1 ⊨ p ≡ w⇩2 ⊨ p› for p
168 by (metis "intro-elim:2")
169 AOT_hence ‹w⇩1 = w⇩2›
170 using "sit-identity"[unconstrain s, THEN "→E",
171 OF PossibleWorld.ψ[THEN "world:1"[THEN "≡⇩d⇩fE"], THEN "&E"(1)],
172 unconstrain s', THEN "→E",
173 OF PossibleWorld.ψ[THEN "world:1"[THEN "≡⇩d⇩fE"], THEN "&E"(1)],
174 THEN "≡E"(2)] GEN by fast
175 AOT_thus ‹w⇩1 = w⇩2 & ¬w⇩1 = w⇩2›
176 using "=-infix" "≡⇩d⇩fE" "con-dis-i-e:1" distinct_worlds by blast
177 qed
178 then AOT_obtain p where 0: ‹w⇩1 ⊨ p & ¬w⇩2 ⊨ p›
179 using "∃E"[rotated] by blast
180 AOT_have ‹y[λy p]›
181 proof (safe intro!: y_prop[THEN "&E"(2), THEN "∀E"(1), THEN "≡E"(2)] "cqt:2")
182 AOT_show ‹w⇩2 ⊨ [λ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 ‹¬w⇩2 ⊨ ∃u [λy p]u›
192 proof (rule "raa-cor:2")
193 AOT_assume ‹w⇩2 ⊨ ∃u [λy p]u›
194 AOT_hence ‹∃x w⇩2 ⊨ (O!x & [λy p]x)›
195 by (metis "conj-dist-w:6" "intro-elim:3:a")
196 then AOT_obtain x where ‹w⇩2 ⊨ (O!x & [λy p]x)›
197 using "∃E"[rotated] by blast
198 AOT_hence ‹w⇩2 ⊨ [λ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 ‹w⇩2 ⊨ p›
202 using world_prop_beta[THEN "PossibleWorld.∀E", THEN "≡E"(1)] by blast
203 AOT_thus ‹w⇩2 ⊨ p & ¬w⇩2 ⊨ p›
204 using 0[THEN "&E"(2)] "&I" by blast
205 qed
206 AOT_thus ‹w⇩2 ⊨ ¬∃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 ‹w⇩2 ⊨ ¬∃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 ‹¬x[λy p]›
215 proof(rule "raa-cor:2")
216 AOT_assume ‹x[λy p]›
217 AOT_hence "w⇩1 ⊨ [λ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 "¬w⇩1 ⊨ ¬[λ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 "w⇩1 ⊨ ¬([λ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 ‹w⇩1 ⊨ 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 ‹w⇩1 ⊨ [λ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 ‹w⇩1 ⊨ (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 w⇩1 ⊨ (O!x & [λy p]x)›
243 by (rule "∃I")
244 AOT_thus ‹w⇩1 ⊨ ∃u [λy p]u›
245 by (metis "conj-dist-w:6" "intro-elim:3:b")
246 next
247 AOT_show ‹w⇩1 ⊨ ¬∃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 ‹y[λy p] & ¬x[λy 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 ‹∃x∃y (◇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 ‹∀n∀m([ℙ]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]) ≡⇩d⇩f A!x & G↓ & ∀F(x[F] ≡ ∀z([F]z ≡ [G]z))›
301
302AOT_define OrdinaryExtensionOf :: ‹τ ⇒ Π ⇒ φ› (‹OrdinaryExtensionOf'(_,_')›)
303 ‹OrdinaryExtensionOf(x,[G]) ≡⇩d⇩f 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 "≡⇩d⇩fE", 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] ≡⇩d⇩f F↓ & G↓ & □∀x ([G]x → [F]x)›
356
357AOT_define concept :: ‹Π› (‹C!›)
358 concepts: ‹C! =⇩d⇩f 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 ≡⇩d⇩f ∀F(c[F] → d[F])›
411
412
413AOT_define conceptOf :: ‹τ ⇒ τ ⇒ φ› (‹ConceptOf'(_,_')›)
414 "concept-of-G": ‹ConceptOf(c,G) ≡⇩d⇩f 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 "≡⇩d⇩fE"] "&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 □∀F∀G(□(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 "≡⇩d⇩fE"] "&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 "≡⇩d⇩fE"] "&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 ‹□∀F∀G(□(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 "≡⇩d⇩fI"] "&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 "≡⇩d⇩fI"] "&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": ‹❙c⇩G =⇩d⇩f ❙ιc ConceptOf(c, G)›
554
555AOT_theorem "concept-G[den]": ‹❙c⇩G↓›
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!❙c⇩G›
562proof -
563 AOT_have ‹❙𝒜(C!❙c⇩G & ConceptOf(❙c⇩G, 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!❙c⇩G›
569 by (metis "Act-Basic:2" "con-dis-i-e:2:a" "intro-elim:3:a")
570 AOT_hence ‹❙𝒜A!❙c⇩G›
571 using "rule-id-df:1[zero]"[OF concepts, OF "oa-exist:2"]
572 "rule=E" by fast
573 AOT_hence ‹A!❙c⇩G›
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": ‹❙c⇩G = ❙ι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 "≡⇩d⇩fI"] 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 "≡⇩d⇩fE"])
586 AOT_thus ‹❙c⇩G = ❙ι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(❙c⇩G[F] ≡ [G] ⇒ [F])›
593proof(safe intro!: GEN "≡I" "→I")
594 fix F
595 AOT_have ‹❙𝒜∀F(❙c⇩G[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 ‹❙𝒜(❙c⇩G[F] ≡ [G] ⇒ [F])›
601 using "logic-actual-nec:3"[axiom_inst, THEN "≡E"(1)] "∀E"(2)
602 by blast
603 AOT_hence 0: ‹❙𝒜❙c⇩G[F] ≡ ❙𝒜[G] ⇒ [F]›
604 using "Act-Basic:5"[THEN "≡E"(1)] by blast
605 {
606 AOT_assume ‹❙c⇩G[F]›
607 AOT_hence ‹❙𝒜❙c⇩G[F]›
608 by(safe intro!: "en-eq:10[1]"[unvarify x⇩1, 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 "≡⇩d⇩fE"] "&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 ‹❙𝒜❙c⇩G[F]›
633 using 0[THEN "≡E"(2)] by blast
634 AOT_thus ‹❙c⇩G[F]›
635 by(safe intro!: "en-eq:10[1]"[unvarify x⇩1, THEN "≡E"(1)]
636 "concept-G[den]")
637 }
638qed
639
640AOT_theorem conH_enc_ord:
641 ‹([H] ⇒ O!) → □∀F ∀G (□G ≡⇩E F → (❙c⇩H[F] ≡ ❙c⇩H[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 "≡⇩d⇩fE"[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 → (❙c⇩H[F] ≡ ❙c⇩H[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 "≡⇩d⇩fE"] "&E"(2))
656 AOT_assume 1: ‹□G ≡⇩E F›
657 AOT_assume ‹❙c⇩H[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 "≡⇩d⇩fE"] "&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 "≡⇩d⇩fE"], 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 "≡⇩d⇩fI"] "&I" "cqt:2")
683 AOT_hence ‹❙c⇩H[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 "≡⇩d⇩fI"]
694 "≡I" "→I" "&I" "cqt:2" Ordinary.GEN
695 dest!: eqE[THEN "≡⇩d⇩fE"] "&E"(2)
696 dest: "≡E"(1,2) "Ordinary.∀E")
697 ultimately AOT_show ‹(❙c⇩H[F] ≡ ❙c⇩H[G])›
698 using 0 "≡I" "→I" by auto
699 }
700 qed
701 ultimately AOT_show ‹□∀F ∀G (□G ≡⇩E F → (❙c⇩H[F] ≡ ❙c⇩H[G]))›
702 using "→E" by blast
703qed
704
705AOT_theorem concept_inclusion_denotes_1:
706 ‹([H] ⇒ O!) → [λx ❙c⇩H ≼ x]↓›
707proof(rule "→I")
708 AOT_assume 0: ‹[H] ⇒ O!›
709 AOT_show ‹[λx ❙c⇩H ≼ x]↓›
710 proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
711 AOT_show ‹[λx C!x & ∀F(❙c⇩H[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 (❙c⇩H[F] → x[F]) ≡ ❙c⇩H ≼ 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 ≼ ❙c⇩H]↓›
724proof(rule "→I")
725 AOT_assume 0: ‹[H] ⇒ O!›
726 AOT_show ‹[λx x ≼ ❙c⇩H]↓›
727 proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
728 AOT_show ‹[λx C!x & ∀F(x[F] → ❙c⇩H[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] → ❙c⇩H[F]) ≡ x ≼ ❙c⇩H)›
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) ≡⇩d⇩f 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: ‹Rigid⇩1⇩-⇩1((=⇩E))›
771proof (safe intro!: "df-1-1:2"[THEN "≡⇩d⇩fI"] "&I" "df-1-1:1"[THEN "≡⇩d⇩fI"]
772 GEN "→I" "df-rigid-rel:1"[THEN "≡⇩d⇩fI"] "=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 ‹∀x∀y □(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 ‹∀x⇩1...∀x⇩n □([(=⇩E)]x⇩1...x⇩n → □[(=⇩E)]x⇩1...x⇩n)›
785 by (rule tuple_forall[THEN "≡⇩d⇩fI"])
786 AOT_thus ‹□∀x⇩1...∀x⇩n ([(=⇩E)]x⇩1...x⇩n → □[(=⇩E)]x⇩1...x⇩n)›
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 "≡⇩d⇩fE" "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 "≡⇩d⇩fI" "df-1-1:5")
807qed
808
809AOT_theorem shared_urelement_projection_identity:
810 assumes ‹∀y [λx (y[λz [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 (z[λz [R]zx])]↓›
817 using assms[THEN "∀E"(2)].
818 AOT_hence 1: ‹∀x ∀y (∀F ([F]x ≡ [F]y) → □(z[λz [R]zx] ≡ z[λz [R]zy]))›
819 using "kirchner-thm-cor:1"[THEN "→E"]
820 by blast
821 AOT_have ‹□(z[λz [R]za] ≡ z[λz [R]zb])›
822 using 1[THEN "∀E"(2), THEN "∀E"(2), THEN "→E", OF 0] by blast
823 }
824 AOT_hence ‹∀z □(z[λz [R]za] ≡ z[λz [R]zb])›
825 by (rule GEN)
826 AOT_hence ‹□∀z(z[λz [R]za] ≡ z[λz [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 (y[λz [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 (z[λz [G]x])]↓›
841 using assms[THEN "∀E"(2)].
842 AOT_hence 1: ‹∀x ∀y (∀F ([F]x ≡ [F]y) → □(z[λz [G]x] ≡ z[λz [G]y]))›
843 using "kirchner-thm-cor:1"[THEN "→E"]
844 by blast
845 AOT_have ‹□(z[λz [G]a] ≡ z[λz [G]b])›
846 using 1[THEN "∀E"(2), THEN "∀E"(2), THEN "→E", OF 0] by blast
847 }
848 AOT_hence ‹∀z □(z[λz [G]a] ≡ z[λz [G]b])›
849 by (rule GEN)
850 AOT_hence ‹□∀z(z[λz [G]a] ≡ z[λz [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 "≡⇩d⇩fI"] "&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 ‹∀R∀y [λx (y[λz [R]zx])]↓›
867 by (safe intro!: GEN "cqt:2" AOT_instance_of_cqt_2_intro_next)
868 AOT_have ‹∀G∀y [λx (y[λz [G]x])]↓›
869 by (safe intro!: GEN "cqt:2" AOT_instance_of_cqt_2_intro_next)
870 }
871end
872
873end
874