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