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 "≡⇩d⇩fI"] "&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) ≡⇩d⇩f 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 ‹∃x∃y (◇Numbers'(x,[λz O!z & z ≠⇩E z]) & ◇Numbers'(y,[λz O!z & z ≠⇩E z]) & x ≠ y)›
48proof -
49 AOT_obtain w⇩1 where ‹∃w w⇩1 ≠ w›
50 using "two-worlds-exist:4" "PossibleWorld.∃E"[rotated] by fast
51 then AOT_obtain w⇩2 where distinct_worlds: ‹w⇩1 ≠ w⇩2›
52 using "PossibleWorld.∃E"[rotated] by blast
53 AOT_obtain x where x_prop:
54 ‹A!x & ∀F (x[F] ≡ w⇩1 ⊨ 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] ≡ w⇩2 ⊨ 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 (w⇩1 ⊨ p & ¬w⇩2 ⊨ p)›
146 proof(rule "raa-cor:1")
147 AOT_assume 0: ‹¬∃p (w⇩1 ⊨ p & ¬w⇩2 ⊨ p)›
148 AOT_have 1: ‹w⇩1 ⊨ p → w⇩2 ⊨ p› for p
149 proof(safe intro!: GEN "→I")
150 AOT_assume ‹w⇩1 ⊨ p›
151 AOT_thus ‹w⇩2 ⊨ p›
152 using 0 "con-dis-i-e:1" "∃I"(2) "raa-cor:4" by fast
153 qed
154 moreover AOT_have ‹w⇩2 ⊨ p → w⇩1 ⊨ p› for p
155 proof(safe intro!: GEN "→I")
156 AOT_assume ‹w⇩2 ⊨ p›
157 AOT_hence ‹¬w⇩2 ⊨ ¬p›
158 using "coherent:2" "intro-elim:3:a" by blast
159 AOT_hence ‹¬w⇩1 ⊨ ¬p›
160 using 1["∀I" p, THEN "∀E"(1), OF "log-prop-prop:2"]
161 by (metis "modus-tollens:1")
162 AOT_thus ‹w⇩1 ⊨ p›
163 using "coherent:1" "intro-elim:3:b" "reductio-aa:1" by blast
164 qed
165 ultimately AOT_have ‹w⇩1 ⊨ p ≡ w⇩2 ⊨ p› for p
166 by (metis "intro-elim:2")
167 AOT_hence ‹w⇩1 = w⇩2›
168 using "sit-identity"[unconstrain s, THEN "→E",
169 OF PossibleWorld.ψ[THEN "world:1"[THEN "≡⇩d⇩fE"], THEN "&E"(1)],
170 unconstrain s', THEN "→E",
171 OF PossibleWorld.ψ[THEN "world:1"[THEN "≡⇩d⇩fE"], THEN "&E"(1)],
172 THEN "≡E"(2)] GEN by fast
173 AOT_thus ‹w⇩1 = w⇩2 & ¬w⇩1 = w⇩2›
174 using "=-infix" "≡⇩d⇩fE" "con-dis-i-e:1" distinct_worlds by blast
175 qed
176 then AOT_obtain p where 0: ‹w⇩1 ⊨ p & ¬w⇩2 ⊨ p›
177 using "∃E"[rotated] by blast
178 AOT_have ‹y[λy p]›
179 proof (safe intro!: y_prop[THEN "&E"(2), THEN "∀E"(1), THEN "≡E"(2)] "cqt:2")
180 AOT_show ‹w⇩2 ⊨ [λ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 ‹¬w⇩2 ⊨ ∃u [λy p]u›
190 proof (rule "raa-cor:2")
191 AOT_assume ‹w⇩2 ⊨ ∃u [λy p]u›
192 AOT_hence ‹∃x w⇩2 ⊨ (O!x & [λy p]x)›
193 by (metis "conj-dist-w:6" "intro-elim:3:a")
194 then AOT_obtain x where ‹w⇩2 ⊨ (O!x & [λy p]x)›
195 using "∃E"[rotated] by blast
196 AOT_hence ‹w⇩2 ⊨ [λ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 ‹w⇩2 ⊨ p›
200 using world_prop_beta[THEN "PossibleWorld.∀E", THEN "≡E"(1)] by blast
201 AOT_thus ‹w⇩2 ⊨ p & ¬w⇩2 ⊨ p›
202 using 0[THEN "&E"(2)] "&I" by blast
203 qed
204 AOT_thus ‹w⇩2 ⊨ ¬∃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 ‹w⇩2 ⊨ ¬∃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 ‹¬x[λy p]›
213 proof(rule "raa-cor:2")
214 AOT_assume ‹x[λy p]›
215 AOT_hence "w⇩1 ⊨ [λ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 "¬w⇩1 ⊨ ¬[λ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 "w⇩1 ⊨ ¬([λ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 ‹w⇩1 ⊨ 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 ‹w⇩1 ⊨ [λ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 ‹w⇩1 ⊨ (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 w⇩1 ⊨ (O!x & [λy p]x)›
241 by (rule "∃I")
242 AOT_thus ‹w⇩1 ⊨ ∃u [λy p]u›
243 by (metis "conj-dist-w:6" "intro-elim:3:b")
244 next
245 AOT_show ‹w⇩1 ⊨ ¬∃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 ‹y[λy p] & ¬x[λy 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 ‹∃x∃y (◇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 ‹∀n∀m([ℙ]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]) ≡⇩d⇩f A!x & G↓ & ∀F(x[F] ≡ ∀z([F]z ≡ [G]z))›
299
300AOT_define OrdinaryExtensionOf :: ‹τ ⇒ Π ⇒ φ› (‹OrdinaryExtensionOf'(_,_')›)
301 ‹OrdinaryExtensionOf(x,[G]) ≡⇩d⇩f 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 "≡⇩d⇩fE", 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
350text‹Fragments of PLM's theory of Concepts.›
351
352AOT_define FimpG :: ‹Π ⇒ Π ⇒ φ› (infixl ‹⇒› 50)
353 "F-imp-G": ‹[G] ⇒ [F] ≡⇩d⇩f F↓ & G↓ & □∀x ([G]x → [F]x)›
354
355AOT_define concept :: ‹Π› (‹C!›)
356 concepts: ‹C! =⇩d⇩f 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 ≡⇩d⇩f ∀F(c[F] → d[F])›
409
410
411AOT_define conceptOf :: ‹τ ⇒ τ ⇒ φ› (‹ConceptOf'(_,_')›)
412 "concept-of-G": ‹ConceptOf(c,G) ≡⇩d⇩f 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 "≡⇩d⇩fE"] "&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 □∀F∀G(□(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 "≡⇩d⇩fE"] "&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 "≡⇩d⇩fE"] "&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 ‹□∀F∀G(□(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 "≡⇩d⇩fI"] "&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 "≡⇩d⇩fI"] "&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": ‹❙c⇩G =⇩d⇩f ❙ιc ConceptOf(c, G)›
552
553AOT_theorem "concept-G[den]": ‹❙c⇩G↓›
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!❙c⇩G›
560proof -
561 AOT_have ‹❙𝒜(C!❙c⇩G & ConceptOf(❙c⇩G, 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!❙c⇩G›
567 by (metis "Act-Basic:2" "con-dis-i-e:2:a" "intro-elim:3:a")
568 AOT_hence ‹❙𝒜A!❙c⇩G›
569 using "rule-id-df:1[zero]"[OF concepts, OF "oa-exist:2"]
570 "rule=E" by fast
571 AOT_hence ‹A!❙c⇩G›
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": ‹❙c⇩G = ❙ι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 "≡⇩d⇩fI"] 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 "≡⇩d⇩fE"])
584 AOT_thus ‹❙c⇩G = ❙ι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(❙c⇩G[F] ≡ [G] ⇒ [F])›
591proof(safe intro!: GEN "≡I" "→I")
592 fix F
593 AOT_have ‹❙𝒜∀F(❙c⇩G[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 ‹❙𝒜(❙c⇩G[F] ≡ [G] ⇒ [F])›
599 using "logic-actual-nec:3"[axiom_inst, THEN "≡E"(1)] "∀E"(2)
600 by blast
601 AOT_hence 0: ‹❙𝒜❙c⇩G[F] ≡ ❙𝒜[G] ⇒ [F]›
602 using "Act-Basic:5"[THEN "≡E"(1)] by blast
603 {
604 AOT_assume ‹❙c⇩G[F]›
605 AOT_hence ‹❙𝒜❙c⇩G[F]›
606 by(safe intro!: "en-eq:10[1]"[unvarify x⇩1, 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 "≡⇩d⇩fE"] "&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 ‹❙𝒜❙c⇩G[F]›
631 using 0[THEN "≡E"(2)] by blast
632 AOT_thus ‹❙c⇩G[F]›
633 by(safe intro!: "en-eq:10[1]"[unvarify x⇩1, THEN "≡E"(1)]
634 "concept-G[den]")
635 }
636qed
637
638AOT_theorem conH_enc_ord:
639 ‹([H] ⇒ O!) → □∀F ∀G (□G ≡⇩E F → (❙c⇩H[F] ≡ ❙c⇩H[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 "≡⇩d⇩fE"[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 → (❙c⇩H[F] ≡ ❙c⇩H[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 "≡⇩d⇩fE"] "&E"(2))
654 AOT_assume 1: ‹□G ≡⇩E F›
655 AOT_assume ‹❙c⇩H[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 "≡⇩d⇩fE"] "&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 "≡⇩d⇩fE"], 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 "≡⇩d⇩fI"] "&I" "cqt:2")
681 AOT_hence ‹❙c⇩H[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 "≡⇩d⇩fI"]
692 "≡I" "→I" "&I" "cqt:2" Ordinary.GEN
693 dest!: eqE[THEN "≡⇩d⇩fE"] "&E"(2)
694 dest: "≡E"(1,2) "Ordinary.∀E")
695 ultimately AOT_show ‹(❙c⇩H[F] ≡ ❙c⇩H[G])›
696 using 0 "≡I" "→I" by auto
697 }
698 qed
699 ultimately AOT_show ‹□∀F ∀G (□G ≡⇩E F → (❙c⇩H[F] ≡ ❙c⇩H[G]))›
700 using "→E" by blast
701qed
702
703AOT_theorem concept_inclusion_denotes_1:
704 ‹([H] ⇒ O!) → [λx ❙c⇩H ≼ x]↓›
705proof(rule "→I")
706 AOT_assume 0: ‹[H] ⇒ O!›
707 AOT_show ‹[λx ❙c⇩H ≼ x]↓›
708 proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
709 AOT_show ‹[λx C!x & ∀F(❙c⇩H[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 (❙c⇩H[F] → x[F]) ≡ ❙c⇩H ≼ 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 ≼ ❙c⇩H]↓›
722proof(rule "→I")
723 AOT_assume 0: ‹[H] ⇒ O!›
724 AOT_show ‹[λx x ≼ ❙c⇩H]↓›
725 proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
726 AOT_show ‹[λx C!x & ∀F(x[F] → ❙c⇩H[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] → ❙c⇩H[F]) ≡ x ≼ ❙c⇩H)›
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) ≡⇩d⇩f 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: ‹Rigid⇩1⇩-⇩1((=⇩E))›
769proof (safe intro!: "df-1-1:2"[THEN "≡⇩d⇩fI"] "&I" "df-1-1:1"[THEN "≡⇩d⇩fI"]
770 GEN "→I" "df-rigid-rel:1"[THEN "≡⇩d⇩fI"] "=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 ‹∀x∀y □(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 ‹∀x⇩1...∀x⇩n □([(=⇩E)]x⇩1...x⇩n → □[(=⇩E)]x⇩1...x⇩n)›
783 by (rule tuple_forall[THEN "≡⇩d⇩fI"])
784 AOT_thus ‹□∀x⇩1...∀x⇩n ([(=⇩E)]x⇩1...x⇩n → □[(=⇩E)]x⇩1...x⇩n)›
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 "≡⇩d⇩fE" "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 "≡⇩d⇩fI" "df-1-1:5")
805qed
806
807AOT_theorem shared_urelement_projection_identity:
808 assumes ‹∀y [λx (y[λz [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 (z[λz [R]zx])]↓›
815 using assms[THEN "∀E"(2)].
816 AOT_hence 1: ‹∀x ∀y (∀F ([F]x ≡ [F]y) → □(z[λz [R]zx] ≡ z[λz [R]zy]))›
817 using "kirchner-thm-cor:1"[THEN "→E"]
818 by blast
819 AOT_have ‹□(z[λz [R]za] ≡ z[λz [R]zb])›
820 using 1[THEN "∀E"(2), THEN "∀E"(2), THEN "→E", OF 0] by blast
821 }
822 AOT_hence ‹∀z □(z[λz [R]za] ≡ z[λz [R]zb])›
823 by (rule GEN)
824 AOT_hence ‹□∀z(z[λz [R]za] ≡ z[λz [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 (y[λz [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 (z[λz [G]x])]↓›
839 using assms[THEN "∀E"(2)].
840 AOT_hence 1: ‹∀x ∀y (∀F ([F]x ≡ [F]y) → □(z[λz [G]x] ≡ z[λz [G]y]))›
841 using "kirchner-thm-cor:1"[THEN "→E"]
842 by blast
843 AOT_have ‹□(z[λz [G]a] ≡ z[λz [G]b])›
844 using 1[THEN "∀E"(2), THEN "∀E"(2), THEN "→E", OF 0] by blast
845 }
846 AOT_hence ‹∀z □(z[λz [G]a] ≡ z[λz [G]b])›
847 by (rule GEN)
848 AOT_hence ‹□∀z(z[λz [G]a] ≡ z[λz [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 "≡⇩d⇩fI"] "&I" "log-prop-prop:2")
855qed
856
857text‹The 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 ‹∀R∀y [λx (y[λz [R]zx])]↓›
865 by (safe intro!: GEN "cqt:2" AOT_instance_of_cqt_2_intro_next)
866 AOT_have ‹∀G∀y [λx (y[λz [G]x])]↓›
867 by (safe intro!: GEN "cqt:2" AOT_instance_of_cqt_2_intro_next)
868 }
869end
870
871end
872