author | wenzelm |
Wed, 09 Oct 2019 22:52:34 +0200 | |
changeset 70814 | a6644dfe8e26 |
parent 69593 | 3dda49e08b9d |
child 71085 | 950e1cfe0fe4 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/Ordinal.thy |
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
435 | 3 |
Copyright 1994 University of Cambridge |
4 |
*) |
|
5 |
||
60770 | 6 |
section\<open>Transitive Sets and Ordinals\<close> |
13356 | 7 |
|
16417 | 8 |
theory Ordinal imports WF Bool equalities begin |
13155 | 9 |
|
24893 | 10 |
definition |
11 |
Memrel :: "i=>i" where |
|
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
12 |
"Memrel(A) == {z\<in>A*A . \<exists>x y. z=<x,y> & x\<in>y }" |
13155 | 13 |
|
24893 | 14 |
definition |
15 |
Transset :: "i=>o" where |
|
46820 | 16 |
"Transset(i) == \<forall>x\<in>i. x<=i" |
13155 | 17 |
|
24893 | 18 |
definition |
19 |
Ord :: "i=>o" where |
|
46820 | 20 |
"Ord(i) == Transset(i) & (\<forall>x\<in>i. Transset(x))" |
13155 | 21 |
|
24893 | 22 |
definition |
69587 | 23 |
lt :: "[i,i] => o" (infixl \<open><\<close> 50) (*less-than on ordinals*) where |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
24 |
"i<j == i\<in>j & Ord(j)" |
13155 | 25 |
|
24893 | 26 |
definition |
27 |
Limit :: "i=>o" where |
|
46820 | 28 |
"Limit(i) == Ord(i) & 0<i & (\<forall>y. y<i \<longrightarrow> succ(y)<i)" |
2539 | 29 |
|
22808 | 30 |
abbreviation |
69587 | 31 |
le (infixl \<open>\<le>\<close> 50) where |
61397 | 32 |
"x \<le> y == x < succ(y)" |
435 | 33 |
|
13155 | 34 |
|
60770 | 35 |
subsection\<open>Rules for Transset\<close> |
13155 | 36 |
|
60770 | 37 |
subsubsection\<open>Three Neat Characterisations of Transset\<close> |
13155 | 38 |
|
39 |
lemma Transset_iff_Pow: "Transset(A) <-> A<=Pow(A)" |
|
40 |
by (unfold Transset_def, blast) |
|
41 |
||
46820 | 42 |
lemma Transset_iff_Union_succ: "Transset(A) <-> \<Union>(succ(A)) = A" |
13155 | 43 |
apply (unfold Transset_def) |
44 |
apply (blast elim!: equalityE) |
|
45 |
done |
|
46 |
||
46820 | 47 |
lemma Transset_iff_Union_subset: "Transset(A) <-> \<Union>(A) \<subseteq> A" |
13155 | 48 |
by (unfold Transset_def, blast) |
49 |
||
60770 | 50 |
subsubsection\<open>Consequences of Downwards Closure\<close> |
13155 | 51 |
|
46820 | 52 |
lemma Transset_doubleton_D: |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
53 |
"[| Transset(C); {a,b}: C |] ==> a\<in>C & b\<in>C" |
13155 | 54 |
by (unfold Transset_def, blast) |
55 |
||
56 |
lemma Transset_Pair_D: |
|
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
57 |
"[| Transset(C); <a,b>\<in>C |] ==> a\<in>C & b\<in>C" |
13155 | 58 |
apply (simp add: Pair_def) |
59 |
apply (blast dest: Transset_doubleton_D) |
|
60 |
done |
|
61 |
||
62 |
lemma Transset_includes_domain: |
|
46953 | 63 |
"[| Transset(C); A*B \<subseteq> C; b \<in> B |] ==> A \<subseteq> C" |
13155 | 64 |
by (blast dest: Transset_Pair_D) |
65 |
||
66 |
lemma Transset_includes_range: |
|
46953 | 67 |
"[| Transset(C); A*B \<subseteq> C; a \<in> A |] ==> B \<subseteq> C" |
13155 | 68 |
by (blast dest: Transset_Pair_D) |
69 |
||
60770 | 70 |
subsubsection\<open>Closure Properties\<close> |
13155 | 71 |
|
72 |
lemma Transset_0: "Transset(0)" |
|
73 |
by (unfold Transset_def, blast) |
|
74 |
||
46820 | 75 |
lemma Transset_Un: |
76 |
"[| Transset(i); Transset(j) |] ==> Transset(i \<union> j)" |
|
13155 | 77 |
by (unfold Transset_def, blast) |
78 |
||
46820 | 79 |
lemma Transset_Int: |
80 |
"[| Transset(i); Transset(j) |] ==> Transset(i \<inter> j)" |
|
13155 | 81 |
by (unfold Transset_def, blast) |
82 |
||
83 |
lemma Transset_succ: "Transset(i) ==> Transset(succ(i))" |
|
84 |
by (unfold Transset_def, blast) |
|
85 |
||
86 |
lemma Transset_Pow: "Transset(i) ==> Transset(Pow(i))" |
|
87 |
by (unfold Transset_def, blast) |
|
88 |
||
46820 | 89 |
lemma Transset_Union: "Transset(A) ==> Transset(\<Union>(A))" |
13155 | 90 |
by (unfold Transset_def, blast) |
91 |
||
46820 | 92 |
lemma Transset_Union_family: |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
93 |
"[| !!i. i\<in>A ==> Transset(i) |] ==> Transset(\<Union>(A))" |
13155 | 94 |
by (unfold Transset_def, blast) |
95 |
||
46820 | 96 |
lemma Transset_Inter_family: |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
97 |
"[| !!i. i\<in>A ==> Transset(i) |] ==> Transset(\<Inter>(A))" |
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
98 |
by (unfold Inter_def Transset_def, blast) |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
99 |
|
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
100 |
lemma Transset_UN: |
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13544
diff
changeset
|
101 |
"(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (\<Union>x\<in>A. B(x))" |
46820 | 102 |
by (rule Transset_Union_family, auto) |
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
103 |
|
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
104 |
lemma Transset_INT: |
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13544
diff
changeset
|
105 |
"(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (\<Inter>x\<in>A. B(x))" |
46820 | 106 |
by (rule Transset_Inter_family, auto) |
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
107 |
|
13155 | 108 |
|
60770 | 109 |
subsection\<open>Lemmas for Ordinals\<close> |
13155 | 110 |
|
111 |
lemma OrdI: |
|
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
112 |
"[| Transset(i); !!x. x\<in>i ==> Transset(x) |] ==> Ord(i)" |
46820 | 113 |
by (simp add: Ord_def) |
13155 | 114 |
|
115 |
lemma Ord_is_Transset: "Ord(i) ==> Transset(i)" |
|
46820 | 116 |
by (simp add: Ord_def) |
13155 | 117 |
|
46820 | 118 |
lemma Ord_contains_Transset: |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
119 |
"[| Ord(i); j\<in>i |] ==> Transset(j) " |
13155 | 120 |
by (unfold Ord_def, blast) |
121 |
||
122 |
||
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
123 |
lemma Ord_in_Ord: "[| Ord(i); j\<in>i |] ==> Ord(j)" |
13155 | 124 |
by (unfold Ord_def Transset_def, blast) |
125 |
||
13243 | 126 |
(*suitable for rewriting PROVIDED i has been fixed*) |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
127 |
lemma Ord_in_Ord': "[| j\<in>i; Ord(i) |] ==> Ord(j)" |
13243 | 128 |
by (blast intro: Ord_in_Ord) |
129 |
||
13155 | 130 |
(* Ord(succ(j)) ==> Ord(j) *) |
131 |
lemmas Ord_succD = Ord_in_Ord [OF _ succI1] |
|
132 |
||
133 |
lemma Ord_subset_Ord: "[| Ord(i); Transset(j); j<=i |] ==> Ord(j)" |
|
134 |
by (simp add: Ord_def Transset_def, blast) |
|
135 |
||
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
136 |
lemma OrdmemD: "[| j\<in>i; Ord(i) |] ==> j<=i" |
13155 | 137 |
by (unfold Ord_def Transset_def, blast) |
138 |
||
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
139 |
lemma Ord_trans: "[| i\<in>j; j\<in>k; Ord(k) |] ==> i\<in>k" |
13155 | 140 |
by (blast dest: OrdmemD) |
141 |
||
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
142 |
lemma Ord_succ_subsetI: "[| i\<in>j; Ord(j) |] ==> succ(i) \<subseteq> j" |
13155 | 143 |
by (blast dest: OrdmemD) |
144 |
||
145 |
||
60770 | 146 |
subsection\<open>The Construction of Ordinals: 0, succ, Union\<close> |
13155 | 147 |
|
148 |
lemma Ord_0 [iff,TC]: "Ord(0)" |
|
149 |
by (blast intro: OrdI Transset_0) |
|
150 |
||
151 |
lemma Ord_succ [TC]: "Ord(i) ==> Ord(succ(i))" |
|
152 |
by (blast intro: OrdI Transset_succ Ord_is_Transset Ord_contains_Transset) |
|
153 |
||
154 |
lemmas Ord_1 = Ord_0 [THEN Ord_succ] |
|
155 |
||
156 |
lemma Ord_succ_iff [iff]: "Ord(succ(i)) <-> Ord(i)" |
|
157 |
by (blast intro: Ord_succ dest!: Ord_succD) |
|
158 |
||
46820 | 159 |
lemma Ord_Un [intro,simp,TC]: "[| Ord(i); Ord(j) |] ==> Ord(i \<union> j)" |
13155 | 160 |
apply (unfold Ord_def) |
161 |
apply (blast intro!: Transset_Un) |
|
162 |
done |
|
163 |
||
46820 | 164 |
lemma Ord_Int [TC]: "[| Ord(i); Ord(j) |] ==> Ord(i \<inter> j)" |
13155 | 165 |
apply (unfold Ord_def) |
166 |
apply (blast intro!: Transset_Int) |
|
167 |
done |
|
168 |
||
60770 | 169 |
text\<open>There is no set of all ordinals, for then it would contain itself\<close> |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
170 |
lemma ON_class: "~ (\<forall>i. i\<in>X <-> Ord(i))" |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
171 |
proof (rule notI) |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
172 |
assume X: "\<forall>i. i \<in> X \<longleftrightarrow> Ord(i)" |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
173 |
have "\<forall>x y. x\<in>X \<longrightarrow> y\<in>x \<longrightarrow> y\<in>X" |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
174 |
by (simp add: X, blast intro: Ord_in_Ord) |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
175 |
hence "Transset(X)" |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
176 |
by (auto simp add: Transset_def) |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
177 |
moreover have "\<And>x. x \<in> X \<Longrightarrow> Transset(x)" |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
178 |
by (simp add: X Ord_def) |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
179 |
ultimately have "Ord(X)" by (rule OrdI) |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
180 |
hence "X \<in> X" by (simp add: X) |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
181 |
thus "False" by (rule mem_irrefl) |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
182 |
qed |
13155 | 183 |
|
60770 | 184 |
subsection\<open>< is 'less Than' for Ordinals\<close> |
13155 | 185 |
|
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
186 |
lemma ltI: "[| i\<in>j; Ord(j) |] ==> i<j" |
13155 | 187 |
by (unfold lt_def, blast) |
188 |
||
189 |
lemma ltE: |
|
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
190 |
"[| i<j; [| i\<in>j; Ord(i); Ord(j) |] ==> P |] ==> P" |
13155 | 191 |
apply (unfold lt_def) |
192 |
apply (blast intro: Ord_in_Ord) |
|
193 |
done |
|
194 |
||
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
195 |
lemma ltD: "i<j ==> i\<in>j" |
13155 | 196 |
by (erule ltE, assumption) |
197 |
||
198 |
lemma not_lt0 [simp]: "~ i<0" |
|
199 |
by (unfold lt_def, blast) |
|
200 |
||
201 |
lemma lt_Ord: "j<i ==> Ord(j)" |
|
202 |
by (erule ltE, assumption) |
|
203 |
||
204 |
lemma lt_Ord2: "j<i ==> Ord(i)" |
|
205 |
by (erule ltE, assumption) |
|
206 |
||
46820 | 207 |
(* @{term"ja \<le> j ==> Ord(j)"} *) |
13155 | 208 |
lemmas le_Ord2 = lt_Ord2 [THEN Ord_succD] |
209 |
||
210 |
(* i<0 ==> R *) |
|
211 |
lemmas lt0E = not_lt0 [THEN notE, elim!] |
|
212 |
||
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
213 |
lemma lt_trans [trans]: "[| i<j; j<k |] ==> i<k" |
13155 | 214 |
by (blast intro!: ltI elim!: ltE intro: Ord_trans) |
215 |
||
216 |
lemma lt_not_sym: "i<j ==> ~ (j<i)" |
|
217 |
apply (unfold lt_def) |
|
218 |
apply (blast elim: mem_asym) |
|
219 |
done |
|
220 |
||
221 |
(* [| i<j; ~P ==> j<i |] ==> P *) |
|
222 |
lemmas lt_asym = lt_not_sym [THEN swap] |
|
223 |
||
224 |
lemma lt_irrefl [elim!]: "i<i ==> P" |
|
225 |
by (blast intro: lt_asym) |
|
226 |
||
227 |
lemma lt_not_refl: "~ i<i" |
|
228 |
apply (rule notI) |
|
229 |
apply (erule lt_irrefl) |
|
230 |
done |
|
231 |
||
232 |
||
69593 | 233 |
text\<open>Recall that \<^term>\<open>i \<le> j\<close> abbreviates \<^term>\<open>i<succ(j)\<close> !!\<close> |
13155 | 234 |
|
46820 | 235 |
lemma le_iff: "i \<le> j <-> i<j | (i=j & Ord(j))" |
13155 | 236 |
by (unfold lt_def, blast) |
237 |
||
238 |
(*Equivalently, i<j ==> i < succ(j)*) |
|
46820 | 239 |
lemma leI: "i<j ==> i \<le> j" |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
240 |
by (simp add: le_iff) |
13155 | 241 |
|
46820 | 242 |
lemma le_eqI: "[| i=j; Ord(j) |] ==> i \<le> j" |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
243 |
by (simp add: le_iff) |
13155 | 244 |
|
245 |
lemmas le_refl = refl [THEN le_eqI] |
|
246 |
||
46820 | 247 |
lemma le_refl_iff [iff]: "i \<le> i <-> Ord(i)" |
13155 | 248 |
by (simp (no_asm_simp) add: lt_not_refl le_iff) |
249 |
||
46820 | 250 |
lemma leCI: "(~ (i=j & Ord(j)) ==> i<j) ==> i \<le> j" |
13155 | 251 |
by (simp add: le_iff, blast) |
252 |
||
253 |
lemma leE: |
|
46820 | 254 |
"[| i \<le> j; i<j ==> P; [| i=j; Ord(j) |] ==> P |] ==> P" |
13155 | 255 |
by (simp add: le_iff, blast) |
256 |
||
46820 | 257 |
lemma le_anti_sym: "[| i \<le> j; j \<le> i |] ==> i=j" |
13155 | 258 |
apply (simp add: le_iff) |
259 |
apply (blast elim: lt_asym) |
|
260 |
done |
|
261 |
||
46820 | 262 |
lemma le0_iff [simp]: "i \<le> 0 <-> i=0" |
13155 | 263 |
by (blast elim!: leE) |
264 |
||
265 |
lemmas le0D = le0_iff [THEN iffD1, dest!] |
|
266 |
||
60770 | 267 |
subsection\<open>Natural Deduction Rules for Memrel\<close> |
13155 | 268 |
|
269 |
(*The lemmas MemrelI/E give better speed than [iff] here*) |
|
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
270 |
lemma Memrel_iff [simp]: "<a,b> \<in> Memrel(A) <-> a\<in>b & a\<in>A & b\<in>A" |
13155 | 271 |
by (unfold Memrel_def, blast) |
272 |
||
46953 | 273 |
lemma MemrelI [intro!]: "[| a \<in> b; a \<in> A; b \<in> A |] ==> <a,b> \<in> Memrel(A)" |
13155 | 274 |
by auto |
275 |
||
276 |
lemma MemrelE [elim!]: |
|
46820 | 277 |
"[| <a,b> \<in> Memrel(A); |
46953 | 278 |
[| a \<in> A; b \<in> A; a\<in>b |] ==> P |] |
13155 | 279 |
==> P" |
280 |
by auto |
|
281 |
||
46820 | 282 |
lemma Memrel_type: "Memrel(A) \<subseteq> A*A" |
13155 | 283 |
by (unfold Memrel_def, blast) |
284 |
||
46820 | 285 |
lemma Memrel_mono: "A<=B ==> Memrel(A) \<subseteq> Memrel(B)" |
13155 | 286 |
by (unfold Memrel_def, blast) |
287 |
||
288 |
lemma Memrel_0 [simp]: "Memrel(0) = 0" |
|
289 |
by (unfold Memrel_def, blast) |
|
290 |
||
291 |
lemma Memrel_1 [simp]: "Memrel(1) = 0" |
|
292 |
by (unfold Memrel_def, blast) |
|
293 |
||
13269 | 294 |
lemma relation_Memrel: "relation(Memrel(A))" |
14864 | 295 |
by (simp add: relation_def Memrel_def) |
13269 | 296 |
|
13155 | 297 |
(*The membership relation (as a set) is well-founded. |
298 |
Proof idea: show A<=B by applying the foundation axiom to A-B *) |
|
299 |
lemma wf_Memrel: "wf(Memrel(A))" |
|
300 |
apply (unfold wf_def) |
|
46820 | 301 |
apply (rule foundation [THEN disjE, THEN allI], erule disjI1, blast) |
13155 | 302 |
done |
303 |
||
69593 | 304 |
text\<open>The premise \<^term>\<open>Ord(i)\<close> does not suffice.\<close> |
46820 | 305 |
lemma trans_Memrel: |
13155 | 306 |
"Ord(i) ==> trans(Memrel(i))" |
307 |
by (unfold Ord_def Transset_def trans_def, blast) |
|
308 |
||
60770 | 309 |
text\<open>However, the following premise is strong enough.\<close> |
46820 | 310 |
lemma Transset_trans_Memrel: |
13396 | 311 |
"\<forall>j\<in>i. Transset(j) ==> trans(Memrel(i))" |
312 |
by (unfold Transset_def trans_def, blast) |
|
313 |
||
13155 | 314 |
(*If Transset(A) then Memrel(A) internalizes the membership relation below A*) |
46820 | 315 |
lemma Transset_Memrel_iff: |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
316 |
"Transset(A) ==> <a,b> \<in> Memrel(A) <-> a\<in>b & b\<in>A" |
13155 | 317 |
by (unfold Transset_def, blast) |
318 |
||
319 |
||
60770 | 320 |
subsection\<open>Transfinite Induction\<close> |
13155 | 321 |
|
322 |
(*Epsilon induction over a transitive set*) |
|
46820 | 323 |
lemma Transset_induct: |
46953 | 324 |
"[| i \<in> k; Transset(k); |
325 |
!!x.[| x \<in> k; \<forall>y\<in>x. P(y) |] ==> P(x) |] |
|
13155 | 326 |
==> P(i)" |
46820 | 327 |
apply (simp add: Transset_def) |
13269 | 328 |
apply (erule wf_Memrel [THEN wf_induct2], blast+) |
13155 | 329 |
done |
330 |
||
331 |
(*Induction over an ordinal*) |
|
46935 | 332 |
lemmas Ord_induct [consumes 2] = Transset_induct [rule_format, OF _ Ord_is_Transset] |
13155 | 333 |
|
334 |
(*Induction over the class of ordinals -- a useful corollary of Ord_induct*) |
|
335 |
||
46935 | 336 |
lemma trans_induct [rule_format, consumes 1, case_names step]: |
46820 | 337 |
"[| Ord(i); |
338 |
!!x.[| Ord(x); \<forall>y\<in>x. P(y) |] ==> P(x) |] |
|
13155 | 339 |
==> P(i)" |
340 |
apply (rule Ord_succ [THEN succI1 [THEN Ord_induct]], assumption) |
|
46820 | 341 |
apply (blast intro: Ord_succ [THEN Ord_in_Ord]) |
13155 | 342 |
done |
343 |
||
13534 | 344 |
|
60770 | 345 |
section\<open>Fundamental properties of the epsilon ordering (< on ordinals)\<close> |
13155 | 346 |
|
347 |
||
60770 | 348 |
subsubsection\<open>Proving That < is a Linear Ordering on the Ordinals\<close> |
13155 | 349 |
|
46993 | 350 |
lemma Ord_linear: |
351 |
"Ord(i) \<Longrightarrow> Ord(j) \<Longrightarrow> i\<in>j | i=j | j\<in>i" |
|
352 |
proof (induct i arbitrary: j rule: trans_induct) |
|
353 |
case (step i) |
|
354 |
note step_i = step |
|
60770 | 355 |
show ?case using \<open>Ord(j)\<close> |
46993 | 356 |
proof (induct j rule: trans_induct) |
357 |
case (step j) |
|
358 |
thus ?case using step_i |
|
359 |
by (blast dest: Ord_trans) |
|
360 |
qed |
|
361 |
qed |
|
13155 | 362 |
|
60770 | 363 |
text\<open>The trichotomy law for ordinals\<close> |
13155 | 364 |
lemma Ord_linear_lt: |
46935 | 365 |
assumes o: "Ord(i)" "Ord(j)" |
46953 | 366 |
obtains (lt) "i<j" | (eq) "i=j" | (gt) "j<i" |
46820 | 367 |
apply (simp add: lt_def) |
46935 | 368 |
apply (rule_tac i1=i and j1=j in Ord_linear [THEN disjE]) |
369 |
apply (blast intro: o)+ |
|
13155 | 370 |
done |
371 |
||
372 |
lemma Ord_linear2: |
|
46935 | 373 |
assumes o: "Ord(i)" "Ord(j)" |
46953 | 374 |
obtains (lt) "i<j" | (ge) "j \<le> i" |
13784 | 375 |
apply (rule_tac i = i and j = j in Ord_linear_lt) |
46935 | 376 |
apply (blast intro: leI le_eqI sym o) + |
13155 | 377 |
done |
378 |
||
379 |
lemma Ord_linear_le: |
|
46935 | 380 |
assumes o: "Ord(i)" "Ord(j)" |
46953 | 381 |
obtains (le) "i \<le> j" | (ge) "j \<le> i" |
13784 | 382 |
apply (rule_tac i = i and j = j in Ord_linear_lt) |
46935 | 383 |
apply (blast intro: leI le_eqI o) + |
13155 | 384 |
done |
385 |
||
46820 | 386 |
lemma le_imp_not_lt: "j \<le> i ==> ~ i<j" |
13155 | 387 |
by (blast elim!: leE elim: lt_asym) |
388 |
||
46820 | 389 |
lemma not_lt_imp_le: "[| ~ i<j; Ord(i); Ord(j) |] ==> j \<le> i" |
13784 | 390 |
by (rule_tac i = i and j = j in Ord_linear2, auto) |
13155 | 391 |
|
61402 | 392 |
|
61798 | 393 |
subsubsection \<open>Some Rewrite Rules for \<open><\<close>, \<open>\<le>\<close>\<close> |
13155 | 394 |
|
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
395 |
lemma Ord_mem_iff_lt: "Ord(j) ==> i\<in>j <-> i<j" |
13155 | 396 |
by (unfold lt_def, blast) |
397 |
||
46820 | 398 |
lemma not_lt_iff_le: "[| Ord(i); Ord(j) |] ==> ~ i<j <-> j \<le> i" |
13155 | 399 |
by (blast dest: le_imp_not_lt not_lt_imp_le) |
2540 | 400 |
|
46820 | 401 |
lemma not_le_iff_lt: "[| Ord(i); Ord(j) |] ==> ~ i \<le> j <-> j<i" |
13155 | 402 |
by (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym]) |
403 |
||
404 |
(*This is identical to 0<succ(i) *) |
|
46820 | 405 |
lemma Ord_0_le: "Ord(i) ==> 0 \<le> i" |
13155 | 406 |
by (erule not_lt_iff_le [THEN iffD1], auto) |
407 |
||
46820 | 408 |
lemma Ord_0_lt: "[| Ord(i); i\<noteq>0 |] ==> 0<i" |
13155 | 409 |
apply (erule not_le_iff_lt [THEN iffD1]) |
410 |
apply (rule Ord_0, blast) |
|
411 |
done |
|
412 |
||
46820 | 413 |
lemma Ord_0_lt_iff: "Ord(i) ==> i\<noteq>0 <-> 0<i" |
13155 | 414 |
by (blast intro: Ord_0_lt) |
415 |
||
416 |
||
60770 | 417 |
subsection\<open>Results about Less-Than or Equals\<close> |
13155 | 418 |
|
46820 | 419 |
(** For ordinals, @{term"j\<subseteq>i"} implies @{term"j \<le> i"} (less-than or equals) **) |
13155 | 420 |
|
46820 | 421 |
lemma zero_le_succ_iff [iff]: "0 \<le> succ(x) <-> Ord(x)" |
13155 | 422 |
by (blast intro: Ord_0_le elim: ltE) |
423 |
||
46820 | 424 |
lemma subset_imp_le: "[| j<=i; Ord(i); Ord(j) |] ==> j \<le> i" |
13269 | 425 |
apply (rule not_lt_iff_le [THEN iffD1], assumption+) |
13155 | 426 |
apply (blast elim: ltE mem_irrefl) |
427 |
done |
|
428 |
||
46820 | 429 |
lemma le_imp_subset: "i \<le> j ==> i<=j" |
13155 | 430 |
by (blast dest: OrdmemD elim: ltE leE) |
431 |
||
46820 | 432 |
lemma le_subset_iff: "j \<le> i <-> j<=i & Ord(i) & Ord(j)" |
13155 | 433 |
by (blast dest: subset_imp_le le_imp_subset elim: ltE) |
434 |
||
46820 | 435 |
lemma le_succ_iff: "i \<le> succ(j) <-> i \<le> j | i=succ(j) & Ord(i)" |
13155 | 436 |
apply (simp (no_asm) add: le_iff) |
437 |
apply blast |
|
438 |
done |
|
439 |
||
440 |
(*Just a variant of subset_imp_le*) |
|
46820 | 441 |
lemma all_lt_imp_le: "[| Ord(i); Ord(j); !!x. x<j ==> x<i |] ==> j \<le> i" |
13155 | 442 |
by (blast intro: not_lt_imp_le dest: lt_irrefl) |
443 |
||
60770 | 444 |
subsubsection\<open>Transitivity Laws\<close> |
13155 | 445 |
|
46820 | 446 |
lemma lt_trans1: "[| i \<le> j; j<k |] ==> i<k" |
13155 | 447 |
by (blast elim!: leE intro: lt_trans) |
448 |
||
46820 | 449 |
lemma lt_trans2: "[| i<j; j \<le> k |] ==> i<k" |
13155 | 450 |
by (blast elim!: leE intro: lt_trans) |
451 |
||
46820 | 452 |
lemma le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> k" |
13155 | 453 |
by (blast intro: lt_trans1) |
454 |
||
46820 | 455 |
lemma succ_leI: "i<j ==> succ(i) \<le> j" |
456 |
apply (rule not_lt_iff_le [THEN iffD1]) |
|
13155 | 457 |
apply (blast elim: ltE leE lt_asym)+ |
458 |
done |
|
459 |
||
460 |
(*Identical to succ(i) < succ(j) ==> i<j *) |
|
46820 | 461 |
lemma succ_leE: "succ(i) \<le> j ==> i<j" |
13155 | 462 |
apply (rule not_le_iff_lt [THEN iffD1]) |
463 |
apply (blast elim: ltE leE lt_asym)+ |
|
464 |
done |
|
465 |
||
46820 | 466 |
lemma succ_le_iff [iff]: "succ(i) \<le> j <-> i<j" |
13155 | 467 |
by (blast intro: succ_leI succ_leE) |
468 |
||
46820 | 469 |
lemma succ_le_imp_le: "succ(i) \<le> succ(j) ==> i \<le> j" |
13155 | 470 |
by (blast dest!: succ_leE) |
471 |
||
46820 | 472 |
lemma lt_subset_trans: "[| i \<subseteq> j; j<k; Ord(i) |] ==> i<k" |
473 |
apply (rule subset_imp_le [THEN lt_trans1]) |
|
13155 | 474 |
apply (blast intro: elim: ltE) + |
475 |
done |
|
476 |
||
13172 | 477 |
lemma lt_imp_0_lt: "j<i ==> 0<i" |
46820 | 478 |
by (blast intro: lt_trans1 Ord_0_le [OF lt_Ord]) |
13172 | 479 |
|
13243 | 480 |
lemma succ_lt_iff: "succ(i) < j <-> i<j & succ(i) \<noteq> j" |
46820 | 481 |
apply auto |
482 |
apply (blast intro: lt_trans le_refl dest: lt_Ord) |
|
483 |
apply (frule lt_Ord) |
|
484 |
apply (rule not_le_iff_lt [THEN iffD1]) |
|
13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
485 |
apply (blast intro: lt_Ord2) |
46820 | 486 |
apply blast |
487 |
apply (simp add: lt_Ord lt_Ord2 le_iff) |
|
488 |
apply (blast dest: lt_asym) |
|
13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
489 |
done |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
490 |
|
13243 | 491 |
lemma Ord_succ_mem_iff: "Ord(j) ==> succ(i) \<in> succ(j) <-> i\<in>j" |
46820 | 492 |
apply (insert succ_le_iff [of i j]) |
493 |
apply (simp add: lt_def) |
|
13243 | 494 |
done |
495 |
||
60770 | 496 |
subsubsection\<open>Union and Intersection\<close> |
13155 | 497 |
|
46820 | 498 |
lemma Un_upper1_le: "[| Ord(i); Ord(j) |] ==> i \<le> i \<union> j" |
13155 | 499 |
by (rule Un_upper1 [THEN subset_imp_le], auto) |
500 |
||
46820 | 501 |
lemma Un_upper2_le: "[| Ord(i); Ord(j) |] ==> j \<le> i \<union> j" |
13155 | 502 |
by (rule Un_upper2 [THEN subset_imp_le], auto) |
503 |
||
504 |
(*Replacing k by succ(k') yields the similar rule for le!*) |
|
46820 | 505 |
lemma Un_least_lt: "[| i<k; j<k |] ==> i \<union> j < k" |
13784 | 506 |
apply (rule_tac i = i and j = j in Ord_linear_le) |
46820 | 507 |
apply (auto simp add: Un_commute le_subset_iff subset_Un_iff lt_Ord) |
13155 | 508 |
done |
509 |
||
46820 | 510 |
lemma Un_least_lt_iff: "[| Ord(i); Ord(j) |] ==> i \<union> j < k <-> i<k & j<k" |
13155 | 511 |
apply (safe intro!: Un_least_lt) |
512 |
apply (rule_tac [2] Un_upper2_le [THEN lt_trans1]) |
|
46820 | 513 |
apply (rule Un_upper1_le [THEN lt_trans1], auto) |
13155 | 514 |
done |
515 |
||
516 |
lemma Un_least_mem_iff: |
|
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
517 |
"[| Ord(i); Ord(j); Ord(k) |] ==> i \<union> j \<in> k <-> i\<in>k & j\<in>k" |
46820 | 518 |
apply (insert Un_least_lt_iff [of i j k]) |
13155 | 519 |
apply (simp add: lt_def) |
520 |
done |
|
521 |
||
522 |
(*Replacing k by succ(k') yields the similar rule for le!*) |
|
46820 | 523 |
lemma Int_greatest_lt: "[| i<k; j<k |] ==> i \<inter> j < k" |
13784 | 524 |
apply (rule_tac i = i and j = j in Ord_linear_le) |
46820 | 525 |
apply (auto simp add: Int_commute le_subset_iff subset_Int_iff lt_Ord) |
13155 | 526 |
done |
527 |
||
13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
528 |
lemma Ord_Un_if: |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
529 |
"[| Ord(i); Ord(j) |] ==> i \<union> j = (if j<i then i else j)" |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
530 |
by (simp add: not_lt_iff_le le_imp_subset leI |
46820 | 531 |
subset_Un_iff [symmetric] subset_Un_iff2 [symmetric]) |
13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
532 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
533 |
lemma succ_Un_distrib: |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
534 |
"[| Ord(i); Ord(j) |] ==> succ(i \<union> j) = succ(i) \<union> succ(j)" |
46820 | 535 |
by (simp add: Ord_Un_if lt_Ord le_Ord2) |
13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
536 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
537 |
lemma lt_Un_iff: |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
538 |
"[| Ord(i); Ord(j) |] ==> k < i \<union> j <-> k < i | k < j" |
46820 | 539 |
apply (simp add: Ord_Un_if not_lt_iff_le) |
540 |
apply (blast intro: leI lt_trans2)+ |
|
13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
541 |
done |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
542 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
543 |
lemma le_Un_iff: |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
544 |
"[| Ord(i); Ord(j) |] ==> k \<le> i \<union> j <-> k \<le> i | k \<le> j" |
46820 | 545 |
by (simp add: succ_Un_distrib lt_Un_iff [symmetric]) |
13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
546 |
|
46820 | 547 |
lemma Un_upper1_lt: "[|k < i; Ord(j)|] ==> k < i \<union> j" |
548 |
by (simp add: lt_Un_iff lt_Ord2) |
|
13172 | 549 |
|
46820 | 550 |
lemma Un_upper2_lt: "[|k < j; Ord(i)|] ==> k < i \<union> j" |
551 |
by (simp add: lt_Un_iff lt_Ord2) |
|
13172 | 552 |
|
553 |
(*See also Transset_iff_Union_succ*) |
|
554 |
lemma Ord_Union_succ_eq: "Ord(i) ==> \<Union>(succ(i)) = i" |
|
555 |
by (blast intro: Ord_trans) |
|
556 |
||
13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
557 |
|
60770 | 558 |
subsection\<open>Results about Limits\<close> |
13155 | 559 |
|
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
560 |
lemma Ord_Union [intro,simp,TC]: "[| !!i. i\<in>A ==> Ord(i) |] ==> Ord(\<Union>(A))" |
13155 | 561 |
apply (rule Ord_is_Transset [THEN Transset_Union_family, THEN OrdI]) |
562 |
apply (blast intro: Ord_contains_Transset)+ |
|
563 |
done |
|
564 |
||
13172 | 565 |
lemma Ord_UN [intro,simp,TC]: |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
566 |
"[| !!x. x\<in>A ==> Ord(B(x)) |] ==> Ord(\<Union>x\<in>A. B(x))" |
13155 | 567 |
by (rule Ord_Union, blast) |
568 |
||
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
569 |
lemma Ord_Inter [intro,simp,TC]: |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
570 |
"[| !!i. i\<in>A ==> Ord(i) |] ==> Ord(\<Inter>(A))" |
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
571 |
apply (rule Transset_Inter_family [THEN OrdI]) |
46820 | 572 |
apply (blast intro: Ord_is_Transset) |
573 |
apply (simp add: Inter_def) |
|
574 |
apply (blast intro: Ord_contains_Transset) |
|
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
575 |
done |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
576 |
|
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
577 |
lemma Ord_INT [intro,simp,TC]: |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
578 |
"[| !!x. x\<in>A ==> Ord(B(x)) |] ==> Ord(\<Inter>x\<in>A. B(x))" |
46820 | 579 |
by (rule Ord_Inter, blast) |
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
580 |
|
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
581 |
|
46820 | 582 |
(* No < version of this theorem: consider that @{term"(\<Union>i\<in>nat.i)=nat"}! *) |
13155 | 583 |
lemma UN_least_le: |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
584 |
"[| Ord(i); !!x. x\<in>A ==> b(x) \<le> i |] ==> (\<Union>x\<in>A. b(x)) \<le> i" |
13155 | 585 |
apply (rule le_imp_subset [THEN UN_least, THEN subset_imp_le]) |
586 |
apply (blast intro: Ord_UN elim: ltE)+ |
|
587 |
done |
|
588 |
||
589 |
lemma UN_succ_least_lt: |
|
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
590 |
"[| j<i; !!x. x\<in>A ==> b(x)<j |] ==> (\<Union>x\<in>A. succ(b(x))) < i" |
13155 | 591 |
apply (rule ltE, assumption) |
592 |
apply (rule UN_least_le [THEN lt_trans2]) |
|
593 |
apply (blast intro: succ_leI)+ |
|
594 |
done |
|
595 |
||
13172 | 596 |
lemma UN_upper_lt: |
597 |
"[| a\<in>A; i < b(a); Ord(\<Union>x\<in>A. b(x)) |] ==> i < (\<Union>x\<in>A. b(x))" |
|
46820 | 598 |
by (unfold lt_def, blast) |
13172 | 599 |
|
13155 | 600 |
lemma UN_upper_le: |
46953 | 601 |
"[| a \<in> A; i \<le> b(a); Ord(\<Union>x\<in>A. b(x)) |] ==> i \<le> (\<Union>x\<in>A. b(x))" |
13155 | 602 |
apply (frule ltD) |
603 |
apply (rule le_imp_subset [THEN subset_trans, THEN subset_imp_le]) |
|
604 |
apply (blast intro: lt_Ord UN_upper)+ |
|
605 |
done |
|
606 |
||
13172 | 607 |
lemma lt_Union_iff: "\<forall>i\<in>A. Ord(i) ==> (j < \<Union>(A)) <-> (\<exists>i\<in>A. j<i)" |
608 |
by (auto simp: lt_def Ord_Union) |
|
609 |
||
610 |
lemma Union_upper_le: |
|
46953 | 611 |
"[| j \<in> J; i\<le>j; Ord(\<Union>(J)) |] ==> i \<le> \<Union>J" |
46820 | 612 |
apply (subst Union_eq_UN) |
13172 | 613 |
apply (rule UN_upper_le, auto) |
614 |
done |
|
615 |
||
13155 | 616 |
lemma le_implies_UN_le_UN: |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
617 |
"[| !!x. x\<in>A ==> c(x) \<le> d(x) |] ==> (\<Union>x\<in>A. c(x)) \<le> (\<Union>x\<in>A. d(x))" |
13155 | 618 |
apply (rule UN_least_le) |
619 |
apply (rule_tac [2] UN_upper_le) |
|
46820 | 620 |
apply (blast intro: Ord_UN le_Ord2)+ |
13155 | 621 |
done |
622 |
||
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13544
diff
changeset
|
623 |
lemma Ord_equality: "Ord(i) ==> (\<Union>y\<in>i. succ(y)) = i" |
13155 | 624 |
by (blast intro: Ord_trans) |
625 |
||
626 |
(*Holds for all transitive sets, not just ordinals*) |
|
46820 | 627 |
lemma Ord_Union_subset: "Ord(i) ==> \<Union>(i) \<subseteq> i" |
13155 | 628 |
by (blast intro: Ord_trans) |
629 |
||
630 |
||
60770 | 631 |
subsection\<open>Limit Ordinals -- General Properties\<close> |
13155 | 632 |
|
46820 | 633 |
lemma Limit_Union_eq: "Limit(i) ==> \<Union>(i) = i" |
13155 | 634 |
apply (unfold Limit_def) |
635 |
apply (fast intro!: ltI elim!: ltE elim: Ord_trans) |
|
636 |
done |
|
637 |
||
638 |
lemma Limit_is_Ord: "Limit(i) ==> Ord(i)" |
|
639 |
apply (unfold Limit_def) |
|
640 |
apply (erule conjunct1) |
|
641 |
done |
|
642 |
||
643 |
lemma Limit_has_0: "Limit(i) ==> 0 < i" |
|
644 |
apply (unfold Limit_def) |
|
645 |
apply (erule conjunct2 [THEN conjunct1]) |
|
646 |
done |
|
647 |
||
46820 | 648 |
lemma Limit_nonzero: "Limit(i) ==> i \<noteq> 0" |
13544 | 649 |
by (drule Limit_has_0, blast) |
650 |
||
13155 | 651 |
lemma Limit_has_succ: "[| Limit(i); j<i |] ==> succ(j) < i" |
652 |
by (unfold Limit_def, blast) |
|
653 |
||
13544 | 654 |
lemma Limit_succ_lt_iff [simp]: "Limit(i) ==> succ(j) < i <-> (j<i)" |
655 |
apply (safe intro!: Limit_has_succ) |
|
656 |
apply (frule lt_Ord) |
|
46820 | 657 |
apply (blast intro: lt_trans) |
13544 | 658 |
done |
659 |
||
13172 | 660 |
lemma zero_not_Limit [iff]: "~ Limit(0)" |
661 |
by (simp add: Limit_def) |
|
662 |
||
663 |
lemma Limit_has_1: "Limit(i) ==> 1 < i" |
|
664 |
by (blast intro: Limit_has_0 Limit_has_succ) |
|
665 |
||
666 |
lemma increasing_LimitI: "[| 0<l; \<forall>x\<in>l. \<exists>y\<in>l. x<y |] ==> Limit(l)" |
|
13544 | 667 |
apply (unfold Limit_def, simp add: lt_Ord2, clarify) |
46820 | 668 |
apply (drule_tac i=y in ltD) |
13172 | 669 |
apply (blast intro: lt_trans1 [OF _ ltI] lt_Ord2) |
670 |
done |
|
671 |
||
46820 | 672 |
lemma non_succ_LimitI: |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
673 |
assumes i: "0<i" and nsucc: "\<And>y. succ(y) \<noteq> i" |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
674 |
shows "Limit(i)" |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
675 |
proof - |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
676 |
have Oi: "Ord(i)" using i by (simp add: lt_def) |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
677 |
{ fix y |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
678 |
assume yi: "y<i" |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
679 |
hence Osy: "Ord(succ(y))" by (simp add: lt_Ord Ord_succ) |
46953 | 680 |
have "~ i \<le> y" using yi by (blast dest: le_imp_not_lt) |
681 |
hence "succ(y) < i" using nsucc [of y] |
|
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
682 |
by (blast intro: Ord_linear_lt [OF Osy Oi]) } |
46953 | 683 |
thus ?thesis using i Oi by (auto simp add: Limit_def) |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
684 |
qed |
13155 | 685 |
|
686 |
lemma succ_LimitE [elim!]: "Limit(succ(i)) ==> P" |
|
687 |
apply (rule lt_irrefl) |
|
688 |
apply (rule Limit_has_succ, assumption) |
|
689 |
apply (erule Limit_is_Ord [THEN Ord_succD, THEN le_refl]) |
|
690 |
done |
|
691 |
||
692 |
lemma not_succ_Limit [simp]: "~ Limit(succ(i))" |
|
693 |
by blast |
|
694 |
||
46820 | 695 |
lemma Limit_le_succD: "[| Limit(i); i \<le> succ(j) |] ==> i \<le> j" |
13155 | 696 |
by (blast elim!: leE) |
697 |
||
13172 | 698 |
|
60770 | 699 |
subsubsection\<open>Traditional 3-Way Case Analysis on Ordinals\<close> |
13155 | 700 |
|
46820 | 701 |
lemma Ord_cases_disj: "Ord(i) ==> i=0 | (\<exists>j. Ord(j) & i=succ(j)) | Limit(i)" |
13155 | 702 |
by (blast intro!: non_succ_LimitI Ord_0_lt) |
703 |
||
704 |
lemma Ord_cases: |
|
46935 | 705 |
assumes i: "Ord(i)" |
46954 | 706 |
obtains ("0") "i=0" | (succ) j where "Ord(j)" "i=succ(j)" | (limit) "Limit(i)" |
46935 | 707 |
by (insert Ord_cases_disj [OF i], auto) |
13155 | 708 |
|
46927 | 709 |
lemma trans_induct3_raw: |
46820 | 710 |
"[| Ord(i); |
711 |
P(0); |
|
712 |
!!x. [| Ord(x); P(x) |] ==> P(succ(x)); |
|
713 |
!!x. [| Limit(x); \<forall>y\<in>x. P(y) |] ==> P(x) |
|
13155 | 714 |
|] ==> P(i)" |
715 |
apply (erule trans_induct) |
|
716 |
apply (erule Ord_cases, blast+) |
|
717 |
done |
|
718 |
||
46927 | 719 |
lemmas trans_induct3 = trans_induct3_raw [rule_format, case_names 0 succ limit, consumes 1] |
13534 | 720 |
|
60770 | 721 |
text\<open>A set of ordinals is either empty, contains its own union, or its |
722 |
union is a limit ordinal.\<close> |
|
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
723 |
|
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
724 |
lemma Union_le: "[| !!x. x\<in>I ==> x\<le>j; Ord(j) |] ==> \<Union>(I) \<le> j" |
46953 | 725 |
by (auto simp add: le_subset_iff Union_least) |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
726 |
|
13172 | 727 |
lemma Ord_set_cases: |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
728 |
assumes I: "\<forall>i\<in>I. Ord(i)" |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
729 |
shows "I=0 \<or> \<Union>(I) \<in> I \<or> (\<Union>(I) \<notin> I \<and> Limit(\<Union>(I)))" |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
730 |
proof (cases "\<Union>(I)" rule: Ord_cases) |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
731 |
show "Ord(\<Union>I)" using I by (blast intro: Ord_Union) |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
732 |
next |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
733 |
assume "\<Union>I = 0" thus ?thesis by (simp, blast intro: subst_elem) |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
734 |
next |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
735 |
fix j |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
736 |
assume j: "Ord(j)" and UIj:"\<Union>(I) = succ(j)" |
46953 | 737 |
{ assume "\<forall>i\<in>I. i\<le>j" |
738 |
hence "\<Union>(I) \<le> j" |
|
739 |
by (simp add: Union_le j) |
|
740 |
hence False |
|
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
741 |
by (simp add: UIj lt_not_refl) } |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
742 |
then obtain i where i: "i \<in> I" "succ(j) \<le> i" using I j |
46953 | 743 |
by (atomize, auto simp add: not_le_iff_lt) |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
744 |
have "\<Union>(I) \<le> succ(j)" using UIj j by auto |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
745 |
hence "i \<le> succ(j)" using i |
46953 | 746 |
by (simp add: le_subset_iff Union_subset_iff) |
747 |
hence "succ(j) = i" using i |
|
748 |
by (blast intro: le_anti_sym) |
|
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
749 |
hence "succ(j) \<in> I" by (simp add: i) |
46953 | 750 |
thus ?thesis by (simp add: UIj) |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
751 |
next |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
752 |
assume "Limit(\<Union>I)" thus ?thesis by auto |
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
753 |
qed |
13172 | 754 |
|
60770 | 755 |
text\<open>If the union of a set of ordinals is a successor, then it is an element of that set.\<close> |
13172 | 756 |
lemma Ord_Union_eq_succD: "[|\<forall>x\<in>X. Ord(x); \<Union>X = succ(j)|] ==> succ(j) \<in> X" |
46841
49b91b716cbe
Structured and calculation-based proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset
|
757 |
by (drule Ord_set_cases, auto) |
13172 | 758 |
|
759 |
lemma Limit_Union [rule_format]: "[| I \<noteq> 0; \<forall>i\<in>I. Limit(i) |] ==> Limit(\<Union>I)" |
|
760 |
apply (simp add: Limit_def lt_def) |
|
761 |
apply (blast intro!: equalityI) |
|
762 |
done |
|
763 |
||
435 | 764 |
end |