author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46993  7371429c527d 
child 58871  c399ae4b836f 
permissions  rwrr 
1478  1 
(* Title: ZF/Ordinal.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

435  3 
Copyright 1994 University of Cambridge 
4 
*) 

5 

13356  6 
header{*Transitive Sets and Ordinals*} 
7 

16417  8 
theory Ordinal imports WF Bool equalities begin 
13155  9 

24893  10 
definition 
11 
Memrel :: "i=>i" where 

46841
49b91b716cbe
Structured and calculationbased 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 
23 
lt :: "[i,i] => o" (infixl "<" 50) (*lessthan on ordinals*) where 

46841
49b91b716cbe
Structured and calculationbased 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 
31 
le (infixl "le" 50) where 

32 
"x le y == x < succ(y)" 

435  33 

22808  34 
notation (xsymbols) 
35 
le (infixl "\<le>" 50) 

435  36 

22808  37 
notation (HTML output) 
38 
le (infixl "\<le>" 50) 

13155  39 

40 

13356  41 
subsection{*Rules for Transset*} 
13155  42 

13356  43 
subsubsection{*Three Neat Characterisations of Transset*} 
13155  44 

45 
lemma Transset_iff_Pow: "Transset(A) <> A<=Pow(A)" 

46 
by (unfold Transset_def, blast) 

47 

46820  48 
lemma Transset_iff_Union_succ: "Transset(A) <> \<Union>(succ(A)) = A" 
13155  49 
apply (unfold Transset_def) 
50 
apply (blast elim!: equalityE) 

51 
done 

52 

46820  53 
lemma Transset_iff_Union_subset: "Transset(A) <> \<Union>(A) \<subseteq> A" 
13155  54 
by (unfold Transset_def, blast) 
55 

13356  56 
subsubsection{*Consequences of Downwards Closure*} 
13155  57 

46820  58 
lemma Transset_doubleton_D: 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

59 
"[ Transset(C); {a,b}: C ] ==> a\<in>C & b\<in>C" 
13155  60 
by (unfold Transset_def, blast) 
61 

62 
lemma Transset_Pair_D: 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

63 
"[ Transset(C); <a,b>\<in>C ] ==> a\<in>C & b\<in>C" 
13155  64 
apply (simp add: Pair_def) 
65 
apply (blast dest: Transset_doubleton_D) 

66 
done 

67 

68 
lemma Transset_includes_domain: 

46953  69 
"[ Transset(C); A*B \<subseteq> C; b \<in> B ] ==> A \<subseteq> C" 
13155  70 
by (blast dest: Transset_Pair_D) 
71 

72 
lemma Transset_includes_range: 

46953  73 
"[ Transset(C); A*B \<subseteq> C; a \<in> A ] ==> B \<subseteq> C" 
13155  74 
by (blast dest: Transset_Pair_D) 
75 

13356  76 
subsubsection{*Closure Properties*} 
13155  77 

78 
lemma Transset_0: "Transset(0)" 

79 
by (unfold Transset_def, blast) 

80 

46820  81 
lemma Transset_Un: 
82 
"[ Transset(i); Transset(j) ] ==> Transset(i \<union> j)" 

13155  83 
by (unfold Transset_def, blast) 
84 

46820  85 
lemma Transset_Int: 
86 
"[ Transset(i); Transset(j) ] ==> Transset(i \<inter> j)" 

13155  87 
by (unfold Transset_def, blast) 
88 

89 
lemma Transset_succ: "Transset(i) ==> Transset(succ(i))" 

90 
by (unfold Transset_def, blast) 

91 

92 
lemma Transset_Pow: "Transset(i) ==> Transset(Pow(i))" 

93 
by (unfold Transset_def, blast) 

94 

46820  95 
lemma Transset_Union: "Transset(A) ==> Transset(\<Union>(A))" 
13155  96 
by (unfold Transset_def, blast) 
97 

46820  98 
lemma Transset_Union_family: 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

99 
"[ !!i. i\<in>A ==> Transset(i) ] ==> Transset(\<Union>(A))" 
13155  100 
by (unfold Transset_def, blast) 
101 

46820  102 
lemma Transset_Inter_family: 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

103 
"[ !!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

104 
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

105 

fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset

106 
lemma Transset_UN: 
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13544
diff
changeset

107 
"(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (\<Union>x\<in>A. B(x))" 
46820  108 
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

109 

fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset

110 
lemma Transset_INT: 
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13544
diff
changeset

111 
"(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (\<Inter>x\<in>A. B(x))" 
46820  112 
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

113 

13155  114 

13356  115 
subsection{*Lemmas for Ordinals*} 
13155  116 

117 
lemma OrdI: 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

118 
"[ Transset(i); !!x. x\<in>i ==> Transset(x) ] ==> Ord(i)" 
46820  119 
by (simp add: Ord_def) 
13155  120 

121 
lemma Ord_is_Transset: "Ord(i) ==> Transset(i)" 

46820  122 
by (simp add: Ord_def) 
13155  123 

46820  124 
lemma Ord_contains_Transset: 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

125 
"[ Ord(i); j\<in>i ] ==> Transset(j) " 
13155  126 
by (unfold Ord_def, blast) 
127 

128 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

129 
lemma Ord_in_Ord: "[ Ord(i); j\<in>i ] ==> Ord(j)" 
13155  130 
by (unfold Ord_def Transset_def, blast) 
131 

13243  132 
(*suitable for rewriting PROVIDED i has been fixed*) 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

133 
lemma Ord_in_Ord': "[ j\<in>i; Ord(i) ] ==> Ord(j)" 
13243  134 
by (blast intro: Ord_in_Ord) 
135 

13155  136 
(* Ord(succ(j)) ==> Ord(j) *) 
137 
lemmas Ord_succD = Ord_in_Ord [OF _ succI1] 

138 

139 
lemma Ord_subset_Ord: "[ Ord(i); Transset(j); j<=i ] ==> Ord(j)" 

140 
by (simp add: Ord_def Transset_def, blast) 

141 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

142 
lemma OrdmemD: "[ j\<in>i; Ord(i) ] ==> j<=i" 
13155  143 
by (unfold Ord_def Transset_def, blast) 
144 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

145 
lemma Ord_trans: "[ i\<in>j; j\<in>k; Ord(k) ] ==> i\<in>k" 
13155  146 
by (blast dest: OrdmemD) 
147 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

148 
lemma Ord_succ_subsetI: "[ i\<in>j; Ord(j) ] ==> succ(i) \<subseteq> j" 
13155  149 
by (blast dest: OrdmemD) 
150 

151 

13356  152 
subsection{*The Construction of Ordinals: 0, succ, Union*} 
13155  153 

154 
lemma Ord_0 [iff,TC]: "Ord(0)" 

155 
by (blast intro: OrdI Transset_0) 

156 

157 
lemma Ord_succ [TC]: "Ord(i) ==> Ord(succ(i))" 

158 
by (blast intro: OrdI Transset_succ Ord_is_Transset Ord_contains_Transset) 

159 

160 
lemmas Ord_1 = Ord_0 [THEN Ord_succ] 

161 

162 
lemma Ord_succ_iff [iff]: "Ord(succ(i)) <> Ord(i)" 

163 
by (blast intro: Ord_succ dest!: Ord_succD) 

164 

46820  165 
lemma Ord_Un [intro,simp,TC]: "[ Ord(i); Ord(j) ] ==> Ord(i \<union> j)" 
13155  166 
apply (unfold Ord_def) 
167 
apply (blast intro!: Transset_Un) 

168 
done 

169 

46820  170 
lemma Ord_Int [TC]: "[ Ord(i); Ord(j) ] ==> Ord(i \<inter> j)" 
13155  171 
apply (unfold Ord_def) 
172 
apply (blast intro!: Transset_Int) 

173 
done 

174 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

175 
text{*There is no set of all ordinals, for then it would contain itself*} 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

176 
lemma ON_class: "~ (\<forall>i. i\<in>X <> Ord(i))" 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

177 
proof (rule notI) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

178 
assume X: "\<forall>i. i \<in> X \<longleftrightarrow> Ord(i)" 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

179 
have "\<forall>x y. x\<in>X \<longrightarrow> y\<in>x \<longrightarrow> y\<in>X" 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

180 
by (simp add: X, blast intro: Ord_in_Ord) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

181 
hence "Transset(X)" 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

182 
by (auto simp add: Transset_def) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

183 
moreover have "\<And>x. x \<in> X \<Longrightarrow> Transset(x)" 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

184 
by (simp add: X Ord_def) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

185 
ultimately have "Ord(X)" by (rule OrdI) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

186 
hence "X \<in> X" by (simp add: X) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

187 
thus "False" by (rule mem_irrefl) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

188 
qed 
13155  189 

13356  190 
subsection{*< is 'less Than' for Ordinals*} 
13155  191 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

192 
lemma ltI: "[ i\<in>j; Ord(j) ] ==> i<j" 
13155  193 
by (unfold lt_def, blast) 
194 

195 
lemma ltE: 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

196 
"[ i<j; [ i\<in>j; Ord(i); Ord(j) ] ==> P ] ==> P" 
13155  197 
apply (unfold lt_def) 
198 
apply (blast intro: Ord_in_Ord) 

199 
done 

200 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

201 
lemma ltD: "i<j ==> i\<in>j" 
13155  202 
by (erule ltE, assumption) 
203 

204 
lemma not_lt0 [simp]: "~ i<0" 

205 
by (unfold lt_def, blast) 

206 

207 
lemma lt_Ord: "j<i ==> Ord(j)" 

208 
by (erule ltE, assumption) 

209 

210 
lemma lt_Ord2: "j<i ==> Ord(i)" 

211 
by (erule ltE, assumption) 

212 

46820  213 
(* @{term"ja \<le> j ==> Ord(j)"} *) 
13155  214 
lemmas le_Ord2 = lt_Ord2 [THEN Ord_succD] 
215 

216 
(* i<0 ==> R *) 

217 
lemmas lt0E = not_lt0 [THEN notE, elim!] 

218 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

219 
lemma lt_trans [trans]: "[ i<j; j<k ] ==> i<k" 
13155  220 
by (blast intro!: ltI elim!: ltE intro: Ord_trans) 
221 

222 
lemma lt_not_sym: "i<j ==> ~ (j<i)" 

223 
apply (unfold lt_def) 

224 
apply (blast elim: mem_asym) 

225 
done 

226 

227 
(* [ i<j; ~P ==> j<i ] ==> P *) 

228 
lemmas lt_asym = lt_not_sym [THEN swap] 

229 

230 
lemma lt_irrefl [elim!]: "i<i ==> P" 

231 
by (blast intro: lt_asym) 

232 

233 
lemma lt_not_refl: "~ i<i" 

234 
apply (rule notI) 

235 
apply (erule lt_irrefl) 

236 
done 

237 

238 

46935  239 
text{* Recall that @{term"i \<le> j"} abbreviates @{term"i<succ(j)"} !! *} 
13155  240 

46820  241 
lemma le_iff: "i \<le> j <> i<j  (i=j & Ord(j))" 
13155  242 
by (unfold lt_def, blast) 
243 

244 
(*Equivalently, i<j ==> i < succ(j)*) 

46820  245 
lemma leI: "i<j ==> i \<le> j" 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

246 
by (simp add: le_iff) 
13155  247 

46820  248 
lemma le_eqI: "[ i=j; Ord(j) ] ==> i \<le> j" 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

249 
by (simp add: le_iff) 
13155  250 

251 
lemmas le_refl = refl [THEN le_eqI] 

252 

46820  253 
lemma le_refl_iff [iff]: "i \<le> i <> Ord(i)" 
13155  254 
by (simp (no_asm_simp) add: lt_not_refl le_iff) 
255 

46820  256 
lemma leCI: "(~ (i=j & Ord(j)) ==> i<j) ==> i \<le> j" 
13155  257 
by (simp add: le_iff, blast) 
258 

259 
lemma leE: 

46820  260 
"[ i \<le> j; i<j ==> P; [ i=j; Ord(j) ] ==> P ] ==> P" 
13155  261 
by (simp add: le_iff, blast) 
262 

46820  263 
lemma le_anti_sym: "[ i \<le> j; j \<le> i ] ==> i=j" 
13155  264 
apply (simp add: le_iff) 
265 
apply (blast elim: lt_asym) 

266 
done 

267 

46820  268 
lemma le0_iff [simp]: "i \<le> 0 <> i=0" 
13155  269 
by (blast elim!: leE) 
270 

271 
lemmas le0D = le0_iff [THEN iffD1, dest!] 

272 

13356  273 
subsection{*Natural Deduction Rules for Memrel*} 
13155  274 

275 
(*The lemmas MemrelI/E give better speed than [iff] here*) 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

276 
lemma Memrel_iff [simp]: "<a,b> \<in> Memrel(A) <> a\<in>b & a\<in>A & b\<in>A" 
13155  277 
by (unfold Memrel_def, blast) 
278 

46953  279 
lemma MemrelI [intro!]: "[ a \<in> b; a \<in> A; b \<in> A ] ==> <a,b> \<in> Memrel(A)" 
13155  280 
by auto 
281 

282 
lemma MemrelE [elim!]: 

46820  283 
"[ <a,b> \<in> Memrel(A); 
46953  284 
[ a \<in> A; b \<in> A; a\<in>b ] ==> P ] 
13155  285 
==> P" 
286 
by auto 

287 

46820  288 
lemma Memrel_type: "Memrel(A) \<subseteq> A*A" 
13155  289 
by (unfold Memrel_def, blast) 
290 

46820  291 
lemma Memrel_mono: "A<=B ==> Memrel(A) \<subseteq> Memrel(B)" 
13155  292 
by (unfold Memrel_def, blast) 
293 

294 
lemma Memrel_0 [simp]: "Memrel(0) = 0" 

295 
by (unfold Memrel_def, blast) 

296 

297 
lemma Memrel_1 [simp]: "Memrel(1) = 0" 

298 
by (unfold Memrel_def, blast) 

299 

13269  300 
lemma relation_Memrel: "relation(Memrel(A))" 
14864  301 
by (simp add: relation_def Memrel_def) 
13269  302 

13155  303 
(*The membership relation (as a set) is wellfounded. 
304 
Proof idea: show A<=B by applying the foundation axiom to AB *) 

305 
lemma wf_Memrel: "wf(Memrel(A))" 

306 
apply (unfold wf_def) 

46820  307 
apply (rule foundation [THEN disjE, THEN allI], erule disjI1, blast) 
13155  308 
done 
309 

13396  310 
text{*The premise @{term "Ord(i)"} does not suffice.*} 
46820  311 
lemma trans_Memrel: 
13155  312 
"Ord(i) ==> trans(Memrel(i))" 
313 
by (unfold Ord_def Transset_def trans_def, blast) 

314 

13396  315 
text{*However, the following premise is strong enough.*} 
46820  316 
lemma Transset_trans_Memrel: 
13396  317 
"\<forall>j\<in>i. Transset(j) ==> trans(Memrel(i))" 
318 
by (unfold Transset_def trans_def, blast) 

319 

13155  320 
(*If Transset(A) then Memrel(A) internalizes the membership relation below A*) 
46820  321 
lemma Transset_Memrel_iff: 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

322 
"Transset(A) ==> <a,b> \<in> Memrel(A) <> a\<in>b & b\<in>A" 
13155  323 
by (unfold Transset_def, blast) 
324 

325 

13356  326 
subsection{*Transfinite Induction*} 
13155  327 

328 
(*Epsilon induction over a transitive set*) 

46820  329 
lemma Transset_induct: 
46953  330 
"[ i \<in> k; Transset(k); 
331 
!!x.[ x \<in> k; \<forall>y\<in>x. P(y) ] ==> P(x) ] 

13155  332 
==> P(i)" 
46820  333 
apply (simp add: Transset_def) 
13269  334 
apply (erule wf_Memrel [THEN wf_induct2], blast+) 
13155  335 
done 
336 

337 
(*Induction over an ordinal*) 

46935  338 
lemmas Ord_induct [consumes 2] = Transset_induct [rule_format, OF _ Ord_is_Transset] 
13155  339 

340 
(*Induction over the class of ordinals  a useful corollary of Ord_induct*) 

341 

46935  342 
lemma trans_induct [rule_format, consumes 1, case_names step]: 
46820  343 
"[ Ord(i); 
344 
!!x.[ Ord(x); \<forall>y\<in>x. P(y) ] ==> P(x) ] 

13155  345 
==> P(i)" 
346 
apply (rule Ord_succ [THEN succI1 [THEN Ord_induct]], assumption) 

46820  347 
apply (blast intro: Ord_succ [THEN Ord_in_Ord]) 
13155  348 
done 
349 

13534  350 

46935  351 
section{*Fundamental properties of the epsilon ordering (< on ordinals)*} 
13155  352 

353 

13356  354 
subsubsection{*Proving That < is a Linear Ordering on the Ordinals*} 
13155  355 

46993  356 
lemma Ord_linear: 
357 
"Ord(i) \<Longrightarrow> Ord(j) \<Longrightarrow> i\<in>j  i=j  j\<in>i" 

358 
proof (induct i arbitrary: j rule: trans_induct) 

359 
case (step i) 

360 
note step_i = step 

361 
show ?case using `Ord(j)` 

362 
proof (induct j rule: trans_induct) 

363 
case (step j) 

364 
thus ?case using step_i 

365 
by (blast dest: Ord_trans) 

366 
qed 

367 
qed 

13155  368 

46935  369 
text{*The trichotomy law for ordinals*} 
13155  370 
lemma Ord_linear_lt: 
46935  371 
assumes o: "Ord(i)" "Ord(j)" 
46953  372 
obtains (lt) "i<j"  (eq) "i=j"  (gt) "j<i" 
46820  373 
apply (simp add: lt_def) 
46935  374 
apply (rule_tac i1=i and j1=j in Ord_linear [THEN disjE]) 
375 
apply (blast intro: o)+ 

13155  376 
done 
377 

378 
lemma Ord_linear2: 

46935  379 
assumes o: "Ord(i)" "Ord(j)" 
46953  380 
obtains (lt) "i<j"  (ge) "j \<le> i" 
13784  381 
apply (rule_tac i = i and j = j in Ord_linear_lt) 
46935  382 
apply (blast intro: leI le_eqI sym o) + 
13155  383 
done 
384 

385 
lemma Ord_linear_le: 

46935  386 
assumes o: "Ord(i)" "Ord(j)" 
46953  387 
obtains (le) "i \<le> j"  (ge) "j \<le> i" 
13784  388 
apply (rule_tac i = i and j = j in Ord_linear_lt) 
46935  389 
apply (blast intro: leI le_eqI o) + 
13155  390 
done 
391 

46820  392 
lemma le_imp_not_lt: "j \<le> i ==> ~ i<j" 
13155  393 
by (blast elim!: leE elim: lt_asym) 
394 

46820  395 
lemma not_lt_imp_le: "[ ~ i<j; Ord(i); Ord(j) ] ==> j \<le> i" 
13784  396 
by (rule_tac i = i and j = j in Ord_linear2, auto) 
13155  397 

13356  398 
subsubsection{*Some Rewrite Rules for <, le*} 
13155  399 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

400 
lemma Ord_mem_iff_lt: "Ord(j) ==> i\<in>j <> i<j" 
13155  401 
by (unfold lt_def, blast) 
402 

46820  403 
lemma not_lt_iff_le: "[ Ord(i); Ord(j) ] ==> ~ i<j <> j \<le> i" 
13155  404 
by (blast dest: le_imp_not_lt not_lt_imp_le) 
2540  405 

46820  406 
lemma not_le_iff_lt: "[ Ord(i); Ord(j) ] ==> ~ i \<le> j <> j<i" 
13155  407 
by (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym]) 
408 

409 
(*This is identical to 0<succ(i) *) 

46820  410 
lemma Ord_0_le: "Ord(i) ==> 0 \<le> i" 
13155  411 
by (erule not_lt_iff_le [THEN iffD1], auto) 
412 

46820  413 
lemma Ord_0_lt: "[ Ord(i); i\<noteq>0 ] ==> 0<i" 
13155  414 
apply (erule not_le_iff_lt [THEN iffD1]) 
415 
apply (rule Ord_0, blast) 

416 
done 

417 

46820  418 
lemma Ord_0_lt_iff: "Ord(i) ==> i\<noteq>0 <> 0<i" 
13155  419 
by (blast intro: Ord_0_lt) 
420 

421 

13356  422 
subsection{*Results about LessThan or Equals*} 
13155  423 

46820  424 
(** For ordinals, @{term"j\<subseteq>i"} implies @{term"j \<le> i"} (lessthan or equals) **) 
13155  425 

46820  426 
lemma zero_le_succ_iff [iff]: "0 \<le> succ(x) <> Ord(x)" 
13155  427 
by (blast intro: Ord_0_le elim: ltE) 
428 

46820  429 
lemma subset_imp_le: "[ j<=i; Ord(i); Ord(j) ] ==> j \<le> i" 
13269  430 
apply (rule not_lt_iff_le [THEN iffD1], assumption+) 
13155  431 
apply (blast elim: ltE mem_irrefl) 
432 
done 

433 

46820  434 
lemma le_imp_subset: "i \<le> j ==> i<=j" 
13155  435 
by (blast dest: OrdmemD elim: ltE leE) 
436 

46820  437 
lemma le_subset_iff: "j \<le> i <> j<=i & Ord(i) & Ord(j)" 
13155  438 
by (blast dest: subset_imp_le le_imp_subset elim: ltE) 
439 

46820  440 
lemma le_succ_iff: "i \<le> succ(j) <> i \<le> j  i=succ(j) & Ord(i)" 
13155  441 
apply (simp (no_asm) add: le_iff) 
442 
apply blast 

443 
done 

444 

445 
(*Just a variant of subset_imp_le*) 

46820  446 
lemma all_lt_imp_le: "[ Ord(i); Ord(j); !!x. x<j ==> x<i ] ==> j \<le> i" 
13155  447 
by (blast intro: not_lt_imp_le dest: lt_irrefl) 
448 

13356  449 
subsubsection{*Transitivity Laws*} 
13155  450 

46820  451 
lemma lt_trans1: "[ i \<le> j; j<k ] ==> i<k" 
13155  452 
by (blast elim!: leE intro: lt_trans) 
453 

46820  454 
lemma lt_trans2: "[ i<j; j \<le> k ] ==> i<k" 
13155  455 
by (blast elim!: leE intro: lt_trans) 
456 

46820  457 
lemma le_trans: "[ i \<le> j; j \<le> k ] ==> i \<le> k" 
13155  458 
by (blast intro: lt_trans1) 
459 

46820  460 
lemma succ_leI: "i<j ==> succ(i) \<le> j" 
461 
apply (rule not_lt_iff_le [THEN iffD1]) 

13155  462 
apply (blast elim: ltE leE lt_asym)+ 
463 
done 

464 

465 
(*Identical to succ(i) < succ(j) ==> i<j *) 

46820  466 
lemma succ_leE: "succ(i) \<le> j ==> i<j" 
13155  467 
apply (rule not_le_iff_lt [THEN iffD1]) 
468 
apply (blast elim: ltE leE lt_asym)+ 

469 
done 

470 

46820  471 
lemma succ_le_iff [iff]: "succ(i) \<le> j <> i<j" 
13155  472 
by (blast intro: succ_leI succ_leE) 
473 

46820  474 
lemma succ_le_imp_le: "succ(i) \<le> succ(j) ==> i \<le> j" 
13155  475 
by (blast dest!: succ_leE) 
476 

46820  477 
lemma lt_subset_trans: "[ i \<subseteq> j; j<k; Ord(i) ] ==> i<k" 
478 
apply (rule subset_imp_le [THEN lt_trans1]) 

13155  479 
apply (blast intro: elim: ltE) + 
480 
done 

481 

13172  482 
lemma lt_imp_0_lt: "j<i ==> 0<i" 
46820  483 
by (blast intro: lt_trans1 Ord_0_le [OF lt_Ord]) 
13172  484 

13243  485 
lemma succ_lt_iff: "succ(i) < j <> i<j & succ(i) \<noteq> j" 
46820  486 
apply auto 
487 
apply (blast intro: lt_trans le_refl dest: lt_Ord) 

488 
apply (frule lt_Ord) 

489 
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

490 
apply (blast intro: lt_Ord2) 
46820  491 
apply blast 
492 
apply (simp add: lt_Ord lt_Ord2 le_iff) 

493 
apply (blast dest: lt_asym) 

13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset

494 
done 
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset

495 

13243  496 
lemma Ord_succ_mem_iff: "Ord(j) ==> succ(i) \<in> succ(j) <> i\<in>j" 
46820  497 
apply (insert succ_le_iff [of i j]) 
498 
apply (simp add: lt_def) 

13243  499 
done 
500 

13356  501 
subsubsection{*Union and Intersection*} 
13155  502 

46820  503 
lemma Un_upper1_le: "[ Ord(i); Ord(j) ] ==> i \<le> i \<union> j" 
13155  504 
by (rule Un_upper1 [THEN subset_imp_le], auto) 
505 

46820  506 
lemma Un_upper2_le: "[ Ord(i); Ord(j) ] ==> j \<le> i \<union> j" 
13155  507 
by (rule Un_upper2 [THEN subset_imp_le], auto) 
508 

509 
(*Replacing k by succ(k') yields the similar rule for le!*) 

46820  510 
lemma Un_least_lt: "[ i<k; j<k ] ==> i \<union> j < k" 
13784  511 
apply (rule_tac i = i and j = j in Ord_linear_le) 
46820  512 
apply (auto simp add: Un_commute le_subset_iff subset_Un_iff lt_Ord) 
13155  513 
done 
514 

46820  515 
lemma Un_least_lt_iff: "[ Ord(i); Ord(j) ] ==> i \<union> j < k <> i<k & j<k" 
13155  516 
apply (safe intro!: Un_least_lt) 
517 
apply (rule_tac [2] Un_upper2_le [THEN lt_trans1]) 

46820  518 
apply (rule Un_upper1_le [THEN lt_trans1], auto) 
13155  519 
done 
520 

521 
lemma Un_least_mem_iff: 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

522 
"[ Ord(i); Ord(j); Ord(k) ] ==> i \<union> j \<in> k <> i\<in>k & j\<in>k" 
46820  523 
apply (insert Un_least_lt_iff [of i j k]) 
13155  524 
apply (simp add: lt_def) 
525 
done 

526 

527 
(*Replacing k by succ(k') yields the similar rule for le!*) 

46820  528 
lemma Int_greatest_lt: "[ i<k; j<k ] ==> i \<inter> j < k" 
13784  529 
apply (rule_tac i = i and j = j in Ord_linear_le) 
46820  530 
apply (auto simp add: Int_commute le_subset_iff subset_Int_iff lt_Ord) 
13155  531 
done 
532 

13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset

533 
lemma Ord_Un_if: 
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset

534 
"[ 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

535 
by (simp add: not_lt_iff_le le_imp_subset leI 
46820  536 
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

537 

660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset

538 
lemma succ_Un_distrib: 
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset

539 
"[ Ord(i); Ord(j) ] ==> succ(i \<union> j) = succ(i) \<union> succ(j)" 
46820  540 
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

541 

660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset

542 
lemma lt_Un_iff: 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

543 
"[ Ord(i); Ord(j) ] ==> k < i \<union> j <> k < i  k < j" 
46820  544 
apply (simp add: Ord_Un_if not_lt_iff_le) 
545 
apply (blast intro: leI lt_trans2)+ 

13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset

546 
done 
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset

547 

660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset

548 
lemma le_Un_iff: 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

549 
"[ Ord(i); Ord(j) ] ==> k \<le> i \<union> j <> k \<le> i  k \<le> j" 
46820  550 
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

551 

46820  552 
lemma Un_upper1_lt: "[k < i; Ord(j)] ==> k < i \<union> j" 
553 
by (simp add: lt_Un_iff lt_Ord2) 

13172  554 

46820  555 
lemma Un_upper2_lt: "[k < j; Ord(i)] ==> k < i \<union> j" 
556 
by (simp add: lt_Un_iff lt_Ord2) 

13172  557 

558 
(*See also Transset_iff_Union_succ*) 

559 
lemma Ord_Union_succ_eq: "Ord(i) ==> \<Union>(succ(i)) = i" 

560 
by (blast intro: Ord_trans) 

561 

13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset

562 

13356  563 
subsection{*Results about Limits*} 
13155  564 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

565 
lemma Ord_Union [intro,simp,TC]: "[ !!i. i\<in>A ==> Ord(i) ] ==> Ord(\<Union>(A))" 
13155  566 
apply (rule Ord_is_Transset [THEN Transset_Union_family, THEN OrdI]) 
567 
apply (blast intro: Ord_contains_Transset)+ 

568 
done 

569 

13172  570 
lemma Ord_UN [intro,simp,TC]: 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

571 
"[ !!x. x\<in>A ==> Ord(B(x)) ] ==> Ord(\<Union>x\<in>A. B(x))" 
13155  572 
by (rule Ord_Union, blast) 
573 

13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset

574 
lemma Ord_Inter [intro,simp,TC]: 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

575 
"[ !!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

576 
apply (rule Transset_Inter_family [THEN OrdI]) 
46820  577 
apply (blast intro: Ord_is_Transset) 
578 
apply (simp add: Inter_def) 

579 
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

580 
done 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset

581 

fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset

582 
lemma Ord_INT [intro,simp,TC]: 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

583 
"[ !!x. x\<in>A ==> Ord(B(x)) ] ==> Ord(\<Inter>x\<in>A. B(x))" 
46820  584 
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

585 

fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset

586 

46820  587 
(* No < version of this theorem: consider that @{term"(\<Union>i\<in>nat.i)=nat"}! *) 
13155  588 
lemma UN_least_le: 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

589 
"[ Ord(i); !!x. x\<in>A ==> b(x) \<le> i ] ==> (\<Union>x\<in>A. b(x)) \<le> i" 
13155  590 
apply (rule le_imp_subset [THEN UN_least, THEN subset_imp_le]) 
591 
apply (blast intro: Ord_UN elim: ltE)+ 

592 
done 

593 

594 
lemma UN_succ_least_lt: 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

595 
"[ j<i; !!x. x\<in>A ==> b(x)<j ] ==> (\<Union>x\<in>A. succ(b(x))) < i" 
13155  596 
apply (rule ltE, assumption) 
597 
apply (rule UN_least_le [THEN lt_trans2]) 

598 
apply (blast intro: succ_leI)+ 

599 
done 

600 

13172  601 
lemma UN_upper_lt: 
602 
"[ a\<in>A; i < b(a); Ord(\<Union>x\<in>A. b(x)) ] ==> i < (\<Union>x\<in>A. b(x))" 

46820  603 
by (unfold lt_def, blast) 
13172  604 

13155  605 
lemma UN_upper_le: 
46953  606 
"[ a \<in> A; i \<le> b(a); Ord(\<Union>x\<in>A. b(x)) ] ==> i \<le> (\<Union>x\<in>A. b(x))" 
13155  607 
apply (frule ltD) 
608 
apply (rule le_imp_subset [THEN subset_trans, THEN subset_imp_le]) 

609 
apply (blast intro: lt_Ord UN_upper)+ 

610 
done 

611 

13172  612 
lemma lt_Union_iff: "\<forall>i\<in>A. Ord(i) ==> (j < \<Union>(A)) <> (\<exists>i\<in>A. j<i)" 
613 
by (auto simp: lt_def Ord_Union) 

614 

615 
lemma Union_upper_le: 

46953  616 
"[ j \<in> J; i\<le>j; Ord(\<Union>(J)) ] ==> i \<le> \<Union>J" 
46820  617 
apply (subst Union_eq_UN) 
13172  618 
apply (rule UN_upper_le, auto) 
619 
done 

620 

13155  621 
lemma le_implies_UN_le_UN: 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

622 
"[ !!x. x\<in>A ==> c(x) \<le> d(x) ] ==> (\<Union>x\<in>A. c(x)) \<le> (\<Union>x\<in>A. d(x))" 
13155  623 
apply (rule UN_least_le) 
624 
apply (rule_tac [2] UN_upper_le) 

46820  625 
apply (blast intro: Ord_UN le_Ord2)+ 
13155  626 
done 
627 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13544
diff
changeset

628 
lemma Ord_equality: "Ord(i) ==> (\<Union>y\<in>i. succ(y)) = i" 
13155  629 
by (blast intro: Ord_trans) 
630 

631 
(*Holds for all transitive sets, not just ordinals*) 

46820  632 
lemma Ord_Union_subset: "Ord(i) ==> \<Union>(i) \<subseteq> i" 
13155  633 
by (blast intro: Ord_trans) 
634 

635 

13356  636 
subsection{*Limit Ordinals  General Properties*} 
13155  637 

46820  638 
lemma Limit_Union_eq: "Limit(i) ==> \<Union>(i) = i" 
13155  639 
apply (unfold Limit_def) 
640 
apply (fast intro!: ltI elim!: ltE elim: Ord_trans) 

641 
done 

642 

643 
lemma Limit_is_Ord: "Limit(i) ==> Ord(i)" 

644 
apply (unfold Limit_def) 

645 
apply (erule conjunct1) 

646 
done 

647 

648 
lemma Limit_has_0: "Limit(i) ==> 0 < i" 

649 
apply (unfold Limit_def) 

650 
apply (erule conjunct2 [THEN conjunct1]) 

651 
done 

652 

46820  653 
lemma Limit_nonzero: "Limit(i) ==> i \<noteq> 0" 
13544  654 
by (drule Limit_has_0, blast) 
655 

13155  656 
lemma Limit_has_succ: "[ Limit(i); j<i ] ==> succ(j) < i" 
657 
by (unfold Limit_def, blast) 

658 

13544  659 
lemma Limit_succ_lt_iff [simp]: "Limit(i) ==> succ(j) < i <> (j<i)" 
660 
apply (safe intro!: Limit_has_succ) 

661 
apply (frule lt_Ord) 

46820  662 
apply (blast intro: lt_trans) 
13544  663 
done 
664 

13172  665 
lemma zero_not_Limit [iff]: "~ Limit(0)" 
666 
by (simp add: Limit_def) 

667 

668 
lemma Limit_has_1: "Limit(i) ==> 1 < i" 

669 
by (blast intro: Limit_has_0 Limit_has_succ) 

670 

671 
lemma increasing_LimitI: "[ 0<l; \<forall>x\<in>l. \<exists>y\<in>l. x<y ] ==> Limit(l)" 

13544  672 
apply (unfold Limit_def, simp add: lt_Ord2, clarify) 
46820  673 
apply (drule_tac i=y in ltD) 
13172  674 
apply (blast intro: lt_trans1 [OF _ ltI] lt_Ord2) 
675 
done 

676 

46820  677 
lemma non_succ_LimitI: 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

678 
assumes i: "0<i" and nsucc: "\<And>y. succ(y) \<noteq> i" 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

679 
shows "Limit(i)" 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

680 
proof  
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

681 
have Oi: "Ord(i)" using i by (simp add: lt_def) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

682 
{ fix y 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

683 
assume yi: "y<i" 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

684 
hence Osy: "Ord(succ(y))" by (simp add: lt_Ord Ord_succ) 
46953  685 
have "~ i \<le> y" using yi by (blast dest: le_imp_not_lt) 
686 
hence "succ(y) < i" using nsucc [of y] 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

687 
by (blast intro: Ord_linear_lt [OF Osy Oi]) } 
46953  688 
thus ?thesis using i Oi by (auto simp add: Limit_def) 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

689 
qed 
13155  690 

691 
lemma succ_LimitE [elim!]: "Limit(succ(i)) ==> P" 

692 
apply (rule lt_irrefl) 

693 
apply (rule Limit_has_succ, assumption) 

694 
apply (erule Limit_is_Ord [THEN Ord_succD, THEN le_refl]) 

695 
done 

696 

697 
lemma not_succ_Limit [simp]: "~ Limit(succ(i))" 

698 
by blast 

699 

46820  700 
lemma Limit_le_succD: "[ Limit(i); i \<le> succ(j) ] ==> i \<le> j" 
13155  701 
by (blast elim!: leE) 
702 

13172  703 

13356  704 
subsubsection{*Traditional 3Way Case Analysis on Ordinals*} 
13155  705 

46820  706 
lemma Ord_cases_disj: "Ord(i) ==> i=0  (\<exists>j. Ord(j) & i=succ(j))  Limit(i)" 
13155  707 
by (blast intro!: non_succ_LimitI Ord_0_lt) 
708 

709 
lemma Ord_cases: 

46935  710 
assumes i: "Ord(i)" 
46954  711 
obtains ("0") "i=0"  (succ) j where "Ord(j)" "i=succ(j)"  (limit) "Limit(i)" 
46935  712 
by (insert Ord_cases_disj [OF i], auto) 
13155  713 

46927  714 
lemma trans_induct3_raw: 
46820  715 
"[ Ord(i); 
716 
P(0); 

717 
!!x. [ Ord(x); P(x) ] ==> P(succ(x)); 

718 
!!x. [ Limit(x); \<forall>y\<in>x. P(y) ] ==> P(x) 

13155  719 
] ==> P(i)" 
720 
apply (erule trans_induct) 

721 
apply (erule Ord_cases, blast+) 

722 
done 

723 

46927  724 
lemmas trans_induct3 = trans_induct3_raw [rule_format, case_names 0 succ limit, consumes 1] 
13534  725 

13172  726 
text{*A set of ordinals is either empty, contains its own union, or its 
727 
union is a limit ordinal.*} 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

728 

49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

729 
lemma Union_le: "[ !!x. x\<in>I ==> x\<le>j; Ord(j) ] ==> \<Union>(I) \<le> j" 
46953  730 
by (auto simp add: le_subset_iff Union_least) 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

731 

13172  732 
lemma Ord_set_cases: 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

733 
assumes I: "\<forall>i\<in>I. Ord(i)" 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

734 
shows "I=0 \<or> \<Union>(I) \<in> I \<or> (\<Union>(I) \<notin> I \<and> Limit(\<Union>(I)))" 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

735 
proof (cases "\<Union>(I)" rule: Ord_cases) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

736 
show "Ord(\<Union>I)" using I by (blast intro: Ord_Union) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

737 
next 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

738 
assume "\<Union>I = 0" thus ?thesis by (simp, blast intro: subst_elem) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

739 
next 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

740 
fix j 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

741 
assume j: "Ord(j)" and UIj:"\<Union>(I) = succ(j)" 
46953  742 
{ assume "\<forall>i\<in>I. i\<le>j" 
743 
hence "\<Union>(I) \<le> j" 

744 
by (simp add: Union_le j) 

745 
hence False 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

746 
by (simp add: UIj lt_not_refl) } 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

747 
then obtain i where i: "i \<in> I" "succ(j) \<le> i" using I j 
46953  748 
by (atomize, auto simp add: not_le_iff_lt) 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

749 
have "\<Union>(I) \<le> succ(j)" using UIj j by auto 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

750 
hence "i \<le> succ(j)" using i 
46953  751 
by (simp add: le_subset_iff Union_subset_iff) 
752 
hence "succ(j) = i" using i 

753 
by (blast intro: le_anti_sym) 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

754 
hence "succ(j) \<in> I" by (simp add: i) 
46953  755 
thus ?thesis by (simp add: UIj) 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

756 
next 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

757 
assume "Limit(\<Union>I)" thus ?thesis by auto 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

758 
qed 
13172  759 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

760 
text{*If the union of a set of ordinals is a successor, then it is an element of that set.*} 
13172  761 
lemma Ord_Union_eq_succD: "[\<forall>x\<in>X. Ord(x); \<Union>X = succ(j)] ==> succ(j) \<in> X" 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46820
diff
changeset

762 
by (drule Ord_set_cases, auto) 
13172  763 

764 
lemma Limit_Union [rule_format]: "[ I \<noteq> 0; \<forall>i\<in>I. Limit(i) ] ==> Limit(\<Union>I)" 

765 
apply (simp add: Limit_def lt_def) 

766 
apply (blast intro!: equalityI) 

767 
done 

768 

435  769 
end 