src/ZF/Ordinal.thy
 author wenzelm Thu Apr 26 14:24:08 2007 +0200 (2007-04-26) changeset 22808 a7daa74e2980 parent 16417 9bc16273c2d4 child 24893 b8ef7afe3a6b permissions -rw-r--r--
eliminated unnamed infixes, tuned syntax;
 clasohm@1478 ` 1` ```(* Title: ZF/Ordinal.thy ``` lcp@435 ` 2` ``` ID: \$Id\$ ``` clasohm@1478 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` lcp@435 ` 4` ``` Copyright 1994 University of Cambridge ``` lcp@435 ` 5` lcp@435 ` 6` ```*) ``` lcp@435 ` 7` paulson@13356 ` 8` ```header{*Transitive Sets and Ordinals*} ``` paulson@13356 ` 9` haftmann@16417 ` 10` ```theory Ordinal imports WF Bool equalities begin ``` paulson@13155 ` 11` paulson@13155 ` 12` ```constdefs ``` paulson@13155 ` 13` paulson@13155 ` 14` ``` Memrel :: "i=>i" ``` paulson@13155 ` 15` ``` "Memrel(A) == {z: A*A . EX x y. z= & x:y }" ``` paulson@13155 ` 16` paulson@13155 ` 17` ``` Transset :: "i=>o" ``` paulson@13155 ` 18` ``` "Transset(i) == ALL x:i. x<=i" ``` paulson@13155 ` 19` paulson@13155 ` 20` ``` Ord :: "i=>o" ``` paulson@13155 ` 21` ``` "Ord(i) == Transset(i) & (ALL x:i. Transset(x))" ``` paulson@13155 ` 22` paulson@13155 ` 23` ``` lt :: "[i,i] => o" (infixl "<" 50) (*less-than on ordinals*) ``` paulson@13155 ` 24` ``` "io" ``` paulson@13155 ` 27` ``` "Limit(i) == Ord(i) & 0 succ(y)" 50) ``` lcp@435 ` 35` wenzelm@22808 ` 36` ```notation (HTML output) ``` wenzelm@22808 ` 37` ``` le (infixl "\" 50) ``` paulson@13155 ` 38` paulson@13155 ` 39` paulson@13356 ` 40` ```subsection{*Rules for Transset*} ``` paulson@13155 ` 41` paulson@13356 ` 42` ```subsubsection{*Three Neat Characterisations of Transset*} ``` paulson@13155 ` 43` paulson@13155 ` 44` ```lemma Transset_iff_Pow: "Transset(A) <-> A<=Pow(A)" ``` paulson@13155 ` 45` ```by (unfold Transset_def, blast) ``` paulson@13155 ` 46` paulson@13155 ` 47` ```lemma Transset_iff_Union_succ: "Transset(A) <-> Union(succ(A)) = A" ``` paulson@13155 ` 48` ```apply (unfold Transset_def) ``` paulson@13155 ` 49` ```apply (blast elim!: equalityE) ``` paulson@13155 ` 50` ```done ``` paulson@13155 ` 51` paulson@13155 ` 52` ```lemma Transset_iff_Union_subset: "Transset(A) <-> Union(A) <= A" ``` paulson@13155 ` 53` ```by (unfold Transset_def, blast) ``` paulson@13155 ` 54` paulson@13356 ` 55` ```subsubsection{*Consequences of Downwards Closure*} ``` paulson@13155 ` 56` paulson@13155 ` 57` ```lemma Transset_doubleton_D: ``` paulson@13155 ` 58` ``` "[| Transset(C); {a,b}: C |] ==> a:C & b: C" ``` paulson@13155 ` 59` ```by (unfold Transset_def, blast) ``` paulson@13155 ` 60` paulson@13155 ` 61` ```lemma Transset_Pair_D: ``` paulson@13155 ` 62` ``` "[| Transset(C); : C |] ==> a:C & b: C" ``` paulson@13155 ` 63` ```apply (simp add: Pair_def) ``` paulson@13155 ` 64` ```apply (blast dest: Transset_doubleton_D) ``` paulson@13155 ` 65` ```done ``` paulson@13155 ` 66` paulson@13155 ` 67` ```lemma Transset_includes_domain: ``` paulson@13155 ` 68` ``` "[| Transset(C); A*B <= C; b: B |] ==> A <= C" ``` paulson@13155 ` 69` ```by (blast dest: Transset_Pair_D) ``` paulson@13155 ` 70` paulson@13155 ` 71` ```lemma Transset_includes_range: ``` paulson@13155 ` 72` ``` "[| Transset(C); A*B <= C; a: A |] ==> B <= C" ``` paulson@13155 ` 73` ```by (blast dest: Transset_Pair_D) ``` paulson@13155 ` 74` paulson@13356 ` 75` ```subsubsection{*Closure Properties*} ``` paulson@13155 ` 76` paulson@13155 ` 77` ```lemma Transset_0: "Transset(0)" ``` paulson@13155 ` 78` ```by (unfold Transset_def, blast) ``` paulson@13155 ` 79` paulson@13155 ` 80` ```lemma Transset_Un: ``` paulson@13155 ` 81` ``` "[| Transset(i); Transset(j) |] ==> Transset(i Un j)" ``` paulson@13155 ` 82` ```by (unfold Transset_def, blast) ``` paulson@13155 ` 83` paulson@13155 ` 84` ```lemma Transset_Int: ``` paulson@13155 ` 85` ``` "[| Transset(i); Transset(j) |] ==> Transset(i Int j)" ``` paulson@13155 ` 86` ```by (unfold Transset_def, blast) ``` paulson@13155 ` 87` paulson@13155 ` 88` ```lemma Transset_succ: "Transset(i) ==> Transset(succ(i))" ``` paulson@13155 ` 89` ```by (unfold Transset_def, blast) ``` paulson@13155 ` 90` paulson@13155 ` 91` ```lemma Transset_Pow: "Transset(i) ==> Transset(Pow(i))" ``` paulson@13155 ` 92` ```by (unfold Transset_def, blast) ``` paulson@13155 ` 93` paulson@13155 ` 94` ```lemma Transset_Union: "Transset(A) ==> Transset(Union(A))" ``` paulson@13155 ` 95` ```by (unfold Transset_def, blast) ``` paulson@13155 ` 96` paulson@13155 ` 97` ```lemma Transset_Union_family: ``` paulson@13155 ` 98` ``` "[| !!i. i:A ==> Transset(i) |] ==> Transset(Union(A))" ``` paulson@13155 ` 99` ```by (unfold Transset_def, blast) ``` paulson@13155 ` 100` paulson@13155 ` 101` ```lemma Transset_Inter_family: ``` paulson@13203 ` 102` ``` "[| !!i. i:A ==> Transset(i) |] ==> Transset(Inter(A))" ``` paulson@13203 ` 103` ```by (unfold Inter_def Transset_def, blast) ``` paulson@13203 ` 104` paulson@13203 ` 105` ```lemma Transset_UN: ``` paulson@13615 ` 106` ``` "(!!x. x \ A ==> Transset(B(x))) ==> Transset (\x\A. B(x))" ``` paulson@13203 ` 107` ```by (rule Transset_Union_family, auto) ``` paulson@13203 ` 108` paulson@13203 ` 109` ```lemma Transset_INT: ``` paulson@13615 ` 110` ``` "(!!x. x \ A ==> Transset(B(x))) ==> Transset (\x\A. B(x))" ``` paulson@13203 ` 111` ```by (rule Transset_Inter_family, auto) ``` paulson@13203 ` 112` paulson@13155 ` 113` paulson@13356 ` 114` ```subsection{*Lemmas for Ordinals*} ``` paulson@13155 ` 115` paulson@13155 ` 116` ```lemma OrdI: ``` paulson@13155 ` 117` ``` "[| Transset(i); !!x. x:i ==> Transset(x) |] ==> Ord(i)" ``` paulson@13155 ` 118` ```by (simp add: Ord_def) ``` paulson@13155 ` 119` paulson@13155 ` 120` ```lemma Ord_is_Transset: "Ord(i) ==> Transset(i)" ``` paulson@13155 ` 121` ```by (simp add: Ord_def) ``` paulson@13155 ` 122` paulson@13155 ` 123` ```lemma Ord_contains_Transset: ``` paulson@13155 ` 124` ``` "[| Ord(i); j:i |] ==> Transset(j) " ``` paulson@13155 ` 125` ```by (unfold Ord_def, blast) ``` paulson@13155 ` 126` paulson@13155 ` 127` paulson@13155 ` 128` ```lemma Ord_in_Ord: "[| Ord(i); j:i |] ==> Ord(j)" ``` paulson@13155 ` 129` ```by (unfold Ord_def Transset_def, blast) ``` paulson@13155 ` 130` paulson@13243 ` 131` ```(*suitable for rewriting PROVIDED i has been fixed*) ``` paulson@13243 ` 132` ```lemma Ord_in_Ord': "[| j:i; Ord(i) |] ==> Ord(j)" ``` paulson@13243 ` 133` ```by (blast intro: Ord_in_Ord) ``` paulson@13243 ` 134` paulson@13155 ` 135` ```(* Ord(succ(j)) ==> Ord(j) *) ``` paulson@13155 ` 136` ```lemmas Ord_succD = Ord_in_Ord [OF _ succI1] ``` paulson@13155 ` 137` paulson@13155 ` 138` ```lemma Ord_subset_Ord: "[| Ord(i); Transset(j); j<=i |] ==> Ord(j)" ``` paulson@13155 ` 139` ```by (simp add: Ord_def Transset_def, blast) ``` paulson@13155 ` 140` paulson@13155 ` 141` ```lemma OrdmemD: "[| j:i; Ord(i) |] ==> j<=i" ``` paulson@13155 ` 142` ```by (unfold Ord_def Transset_def, blast) ``` paulson@13155 ` 143` paulson@13155 ` 144` ```lemma Ord_trans: "[| i:j; j:k; Ord(k) |] ==> i:k" ``` paulson@13155 ` 145` ```by (blast dest: OrdmemD) ``` paulson@13155 ` 146` paulson@13155 ` 147` ```lemma Ord_succ_subsetI: "[| i:j; Ord(j) |] ==> succ(i) <= j" ``` paulson@13155 ` 148` ```by (blast dest: OrdmemD) ``` paulson@13155 ` 149` paulson@13155 ` 150` paulson@13356 ` 151` ```subsection{*The Construction of Ordinals: 0, succ, Union*} ``` paulson@13155 ` 152` paulson@13155 ` 153` ```lemma Ord_0 [iff,TC]: "Ord(0)" ``` paulson@13155 ` 154` ```by (blast intro: OrdI Transset_0) ``` paulson@13155 ` 155` paulson@13155 ` 156` ```lemma Ord_succ [TC]: "Ord(i) ==> Ord(succ(i))" ``` paulson@13155 ` 157` ```by (blast intro: OrdI Transset_succ Ord_is_Transset Ord_contains_Transset) ``` paulson@13155 ` 158` paulson@13155 ` 159` ```lemmas Ord_1 = Ord_0 [THEN Ord_succ] ``` paulson@13155 ` 160` paulson@13155 ` 161` ```lemma Ord_succ_iff [iff]: "Ord(succ(i)) <-> Ord(i)" ``` paulson@13155 ` 162` ```by (blast intro: Ord_succ dest!: Ord_succD) ``` paulson@13155 ` 163` paulson@13172 ` 164` ```lemma Ord_Un [intro,simp,TC]: "[| Ord(i); Ord(j) |] ==> Ord(i Un j)" ``` paulson@13155 ` 165` ```apply (unfold Ord_def) ``` paulson@13155 ` 166` ```apply (blast intro!: Transset_Un) ``` paulson@13155 ` 167` ```done ``` paulson@13155 ` 168` paulson@13155 ` 169` ```lemma Ord_Int [TC]: "[| Ord(i); Ord(j) |] ==> Ord(i Int j)" ``` paulson@13155 ` 170` ```apply (unfold Ord_def) ``` paulson@13155 ` 171` ```apply (blast intro!: Transset_Int) ``` paulson@13155 ` 172` ```done ``` paulson@13155 ` 173` paulson@13155 ` 174` ```(*There is no set of all ordinals, for then it would contain itself*) ``` paulson@13155 ` 175` ```lemma ON_class: "~ (ALL i. i:X <-> Ord(i))" ``` paulson@13155 ` 176` ```apply (rule notI) ``` paulson@13784 ` 177` ```apply (frule_tac x = X in spec) ``` paulson@13155 ` 178` ```apply (safe elim!: mem_irrefl) ``` paulson@13155 ` 179` ```apply (erule swap, rule OrdI [OF _ Ord_is_Transset]) ``` paulson@13155 ` 180` ```apply (simp add: Transset_def) ``` paulson@13155 ` 181` ```apply (blast intro: Ord_in_Ord)+ ``` paulson@13155 ` 182` ```done ``` paulson@13155 ` 183` paulson@13356 ` 184` ```subsection{*< is 'less Than' for Ordinals*} ``` paulson@13155 ` 185` paulson@13155 ` 186` ```lemma ltI: "[| i:j; Ord(j) |] ==> i P |] ==> P" ``` paulson@13155 ` 191` ```apply (unfold lt_def) ``` paulson@13155 ` 192` ```apply (blast intro: Ord_in_Ord) ``` paulson@13155 ` 193` ```done ``` paulson@13155 ` 194` paulson@13155 ` 195` ```lemma ltD: "i i:j" ``` paulson@13155 ` 196` ```by (erule ltE, assumption) ``` paulson@13155 ` 197` paulson@13155 ` 198` ```lemma not_lt0 [simp]: "~ i<0" ``` paulson@13155 ` 199` ```by (unfold lt_def, blast) ``` paulson@13155 ` 200` paulson@13155 ` 201` ```lemma lt_Ord: "j Ord(j)" ``` paulson@13155 ` 202` ```by (erule ltE, assumption) ``` paulson@13155 ` 203` paulson@13155 ` 204` ```lemma lt_Ord2: "j Ord(i)" ``` paulson@13155 ` 205` ```by (erule ltE, assumption) ``` paulson@13155 ` 206` paulson@13155 ` 207` ```(* "ja le j ==> Ord(j)" *) ``` paulson@13155 ` 208` ```lemmas le_Ord2 = lt_Ord2 [THEN Ord_succD] ``` paulson@13155 ` 209` paulson@13155 ` 210` ```(* i<0 ==> R *) ``` paulson@13155 ` 211` ```lemmas lt0E = not_lt0 [THEN notE, elim!] ``` paulson@13155 ` 212` paulson@13155 ` 213` ```lemma lt_trans: "[| i i ~ (j j P *) ``` paulson@13155 ` 222` ```lemmas lt_asym = lt_not_sym [THEN swap] ``` paulson@13155 ` 223` paulson@13155 ` 224` ```lemma lt_irrefl [elim!]: "i P" ``` paulson@13155 ` 225` ```by (blast intro: lt_asym) ``` paulson@13155 ` 226` paulson@13155 ` 227` ```lemma lt_not_refl: "~ i i i < succ(j)*) ``` paulson@13155 ` 239` ```lemma leI: "i i le j" ``` paulson@13155 ` 240` ```by (simp (no_asm_simp) add: le_iff) ``` paulson@13155 ` 241` paulson@13155 ` 242` ```lemma le_eqI: "[| i=j; Ord(j) |] ==> i le j" ``` paulson@13155 ` 243` ```by (simp (no_asm_simp) add: le_iff) ``` paulson@13155 ` 244` paulson@13155 ` 245` ```lemmas le_refl = refl [THEN le_eqI] ``` paulson@13155 ` 246` paulson@13155 ` 247` ```lemma le_refl_iff [iff]: "i le i <-> Ord(i)" ``` paulson@13155 ` 248` ```by (simp (no_asm_simp) add: lt_not_refl le_iff) ``` paulson@13155 ` 249` paulson@13155 ` 250` ```lemma leCI: "(~ (i=j & Ord(j)) ==> i i le j" ``` paulson@13155 ` 251` ```by (simp add: le_iff, blast) ``` paulson@13155 ` 252` paulson@13155 ` 253` ```lemma leE: ``` paulson@13155 ` 254` ``` "[| i le j; i P; [| i=j; Ord(j) |] ==> P |] ==> P" ``` paulson@13155 ` 255` ```by (simp add: le_iff, blast) ``` paulson@13155 ` 256` paulson@13155 ` 257` ```lemma le_anti_sym: "[| i le j; j le i |] ==> i=j" ``` paulson@13155 ` 258` ```apply (simp add: le_iff) ``` paulson@13155 ` 259` ```apply (blast elim: lt_asym) ``` paulson@13155 ` 260` ```done ``` paulson@13155 ` 261` paulson@13155 ` 262` ```lemma le0_iff [simp]: "i le 0 <-> i=0" ``` paulson@13155 ` 263` ```by (blast elim!: leE) ``` paulson@13155 ` 264` paulson@13155 ` 265` ```lemmas le0D = le0_iff [THEN iffD1, dest!] ``` paulson@13155 ` 266` paulson@13356 ` 267` ```subsection{*Natural Deduction Rules for Memrel*} ``` paulson@13155 ` 268` paulson@13155 ` 269` ```(*The lemmas MemrelI/E give better speed than [iff] here*) ``` paulson@13155 ` 270` ```lemma Memrel_iff [simp]: " : Memrel(A) <-> a:b & a:A & b:A" ``` paulson@13155 ` 271` ```by (unfold Memrel_def, blast) ``` paulson@13155 ` 272` paulson@13155 ` 273` ```lemma MemrelI [intro!]: "[| a: b; a: A; b: A |] ==> : Memrel(A)" ``` paulson@13155 ` 274` ```by auto ``` paulson@13155 ` 275` paulson@13155 ` 276` ```lemma MemrelE [elim!]: ``` paulson@13155 ` 277` ``` "[| : Memrel(A); ``` paulson@13155 ` 278` ``` [| a: A; b: A; a:b |] ==> P |] ``` paulson@13155 ` 279` ``` ==> P" ``` paulson@13155 ` 280` ```by auto ``` paulson@13155 ` 281` paulson@13155 ` 282` ```lemma Memrel_type: "Memrel(A) <= A*A" ``` paulson@13155 ` 283` ```by (unfold Memrel_def, blast) ``` paulson@13155 ` 284` paulson@13155 ` 285` ```lemma Memrel_mono: "A<=B ==> Memrel(A) <= Memrel(B)" ``` paulson@13155 ` 286` ```by (unfold Memrel_def, blast) ``` paulson@13155 ` 287` paulson@13155 ` 288` ```lemma Memrel_0 [simp]: "Memrel(0) = 0" ``` paulson@13155 ` 289` ```by (unfold Memrel_def, blast) ``` paulson@13155 ` 290` paulson@13155 ` 291` ```lemma Memrel_1 [simp]: "Memrel(1) = 0" ``` paulson@13155 ` 292` ```by (unfold Memrel_def, blast) ``` paulson@13155 ` 293` paulson@13269 ` 294` ```lemma relation_Memrel: "relation(Memrel(A))" ``` paulson@14864 ` 295` ```by (simp add: relation_def Memrel_def) ``` paulson@13269 ` 296` paulson@13155 ` 297` ```(*The membership relation (as a set) is well-founded. ``` paulson@13155 ` 298` ``` Proof idea: show A<=B by applying the foundation axiom to A-B *) ``` paulson@13155 ` 299` ```lemma wf_Memrel: "wf(Memrel(A))" ``` paulson@13155 ` 300` ```apply (unfold wf_def) ``` paulson@13155 ` 301` ```apply (rule foundation [THEN disjE, THEN allI], erule disjI1, blast) ``` paulson@13155 ` 302` ```done ``` paulson@13155 ` 303` paulson@13396 ` 304` ```text{*The premise @{term "Ord(i)"} does not suffice.*} ``` paulson@13155 ` 305` ```lemma trans_Memrel: ``` paulson@13155 ` 306` ``` "Ord(i) ==> trans(Memrel(i))" ``` paulson@13155 ` 307` ```by (unfold Ord_def Transset_def trans_def, blast) ``` paulson@13155 ` 308` paulson@13396 ` 309` ```text{*However, the following premise is strong enough.*} ``` paulson@13396 ` 310` ```lemma Transset_trans_Memrel: ``` paulson@13396 ` 311` ``` "\j\i. Transset(j) ==> trans(Memrel(i))" ``` paulson@13396 ` 312` ```by (unfold Transset_def trans_def, blast) ``` paulson@13396 ` 313` paulson@13155 ` 314` ```(*If Transset(A) then Memrel(A) internalizes the membership relation below A*) ``` paulson@13155 ` 315` ```lemma Transset_Memrel_iff: ``` paulson@13155 ` 316` ``` "Transset(A) ==> : Memrel(A) <-> a:b & b:A" ``` paulson@13155 ` 317` ```by (unfold Transset_def, blast) ``` paulson@13155 ` 318` paulson@13155 ` 319` paulson@13356 ` 320` ```subsection{*Transfinite Induction*} ``` paulson@13155 ` 321` paulson@13155 ` 322` ```(*Epsilon induction over a transitive set*) ``` paulson@13155 ` 323` ```lemma Transset_induct: ``` paulson@13155 ` 324` ``` "[| i: k; Transset(k); ``` paulson@13155 ` 325` ``` !!x.[| x: k; ALL y:x. P(y) |] ==> P(x) |] ``` paulson@13155 ` 326` ``` ==> P(i)" ``` paulson@13155 ` 327` ```apply (simp add: Transset_def) ``` paulson@13269 ` 328` ```apply (erule wf_Memrel [THEN wf_induct2], blast+) ``` paulson@13155 ` 329` ```done ``` paulson@13155 ` 330` paulson@13155 ` 331` ```(*Induction over an ordinal*) ``` wenzelm@13534 ` 332` ```lemmas Ord_induct [consumes 2] = Transset_induct [OF _ Ord_is_Transset] ``` wenzelm@13534 ` 333` ```lemmas Ord_induct_rule = Ord_induct [rule_format, consumes 2] ``` paulson@13155 ` 334` paulson@13155 ` 335` ```(*Induction over the class of ordinals -- a useful corollary of Ord_induct*) ``` paulson@13155 ` 336` wenzelm@13534 ` 337` ```lemma trans_induct [consumes 1]: ``` paulson@13155 ` 338` ``` "[| Ord(i); ``` paulson@13155 ` 339` ``` !!x.[| Ord(x); ALL y:x. P(y) |] ==> P(x) |] ``` paulson@13155 ` 340` ``` ==> P(i)" ``` paulson@13155 ` 341` ```apply (rule Ord_succ [THEN succI1 [THEN Ord_induct]], assumption) ``` paulson@13155 ` 342` ```apply (blast intro: Ord_succ [THEN Ord_in_Ord]) ``` paulson@13155 ` 343` ```done ``` paulson@13155 ` 344` wenzelm@13534 ` 345` ```lemmas trans_induct_rule = trans_induct [rule_format, consumes 1] ``` wenzelm@13534 ` 346` paulson@13155 ` 347` paulson@13155 ` 348` ```(*** Fundamental properties of the epsilon ordering (< on ordinals) ***) ``` paulson@13155 ` 349` paulson@13155 ` 350` paulson@13356 ` 351` ```subsubsection{*Proving That < is a Linear Ordering on the Ordinals*} ``` paulson@13155 ` 352` paulson@13155 ` 353` ```lemma Ord_linear [rule_format]: ``` paulson@13155 ` 354` ``` "Ord(i) ==> (ALL j. Ord(j) --> i:j | i=j | j:i)" ``` paulson@13155 ` 355` ```apply (erule trans_induct) ``` paulson@13155 ` 356` ```apply (rule impI [THEN allI]) ``` paulson@13155 ` 357` ```apply (erule_tac i=j in trans_induct) ``` paulson@13155 ` 358` ```apply (blast dest: Ord_trans) ``` paulson@13155 ` 359` ```done ``` paulson@13155 ` 360` paulson@13155 ` 361` ```(*The trichotomy law for ordinals!*) ``` paulson@13155 ` 362` ```lemma Ord_linear_lt: ``` paulson@13155 ` 363` ``` "[| Ord(i); Ord(j); i P; i=j ==> P; j P |] ==> P" ``` paulson@13155 ` 364` ```apply (simp add: lt_def) ``` paulson@13155 ` 365` ```apply (rule_tac i1=i and j1=j in Ord_linear [THEN disjE], blast+) ``` paulson@13155 ` 366` ```done ``` paulson@13155 ` 367` paulson@13155 ` 368` ```lemma Ord_linear2: ``` paulson@13155 ` 369` ``` "[| Ord(i); Ord(j); i P; j le i ==> P |] ==> P" ``` paulson@13784 ` 370` ```apply (rule_tac i = i and j = j in Ord_linear_lt) ``` paulson@13155 ` 371` ```apply (blast intro: leI le_eqI sym ) + ``` paulson@13155 ` 372` ```done ``` paulson@13155 ` 373` paulson@13155 ` 374` ```lemma Ord_linear_le: ``` paulson@13155 ` 375` ``` "[| Ord(i); Ord(j); i le j ==> P; j le i ==> P |] ==> P" ``` paulson@13784 ` 376` ```apply (rule_tac i = i and j = j in Ord_linear_lt) ``` paulson@13155 ` 377` ```apply (blast intro: leI le_eqI ) + ``` paulson@13155 ` 378` ```done ``` paulson@13155 ` 379` paulson@13155 ` 380` ```lemma le_imp_not_lt: "j le i ==> ~ i j le i" ``` paulson@13784 ` 384` ```by (rule_tac i = i and j = j in Ord_linear2, auto) ``` paulson@13155 ` 385` paulson@13356 ` 386` ```subsubsection{*Some Rewrite Rules for <, le*} ``` paulson@13155 ` 387` paulson@13155 ` 388` ```lemma Ord_mem_iff_lt: "Ord(j) ==> i:j <-> i ~ i j le i" ``` paulson@13155 ` 392` ```by (blast dest: le_imp_not_lt not_lt_imp_le) ``` wenzelm@2540 ` 393` paulson@13155 ` 394` ```lemma not_le_iff_lt: "[| Ord(i); Ord(j) |] ==> ~ i le j <-> j 0 le i" ``` paulson@13155 ` 399` ```by (erule not_lt_iff_le [THEN iffD1], auto) ``` paulson@13155 ` 400` paulson@13155 ` 401` ```lemma Ord_0_lt: "[| Ord(i); i~=0 |] ==> 0 i~=0 <-> 0 Ord(x)" ``` paulson@13155 ` 415` ```by (blast intro: Ord_0_le elim: ltE) ``` paulson@13155 ` 416` paulson@13155 ` 417` ```lemma subset_imp_le: "[| j<=i; Ord(i); Ord(j) |] ==> j le i" ``` paulson@13269 ` 418` ```apply (rule not_lt_iff_le [THEN iffD1], assumption+) ``` paulson@13155 ` 419` ```apply (blast elim: ltE mem_irrefl) ``` paulson@13155 ` 420` ```done ``` paulson@13155 ` 421` paulson@13155 ` 422` ```lemma le_imp_subset: "i le j ==> i<=j" ``` paulson@13155 ` 423` ```by (blast dest: OrdmemD elim: ltE leE) ``` paulson@13155 ` 424` paulson@13155 ` 425` ```lemma le_subset_iff: "j le i <-> j<=i & Ord(i) & Ord(j)" ``` paulson@13155 ` 426` ```by (blast dest: subset_imp_le le_imp_subset elim: ltE) ``` paulson@13155 ` 427` paulson@13155 ` 428` ```lemma le_succ_iff: "i le succ(j) <-> i le j | i=succ(j) & Ord(i)" ``` paulson@13155 ` 429` ```apply (simp (no_asm) add: le_iff) ``` paulson@13155 ` 430` ```apply blast ``` paulson@13155 ` 431` ```done ``` paulson@13155 ` 432` paulson@13155 ` 433` ```(*Just a variant of subset_imp_le*) ``` paulson@13155 ` 434` ```lemma all_lt_imp_le: "[| Ord(i); Ord(j); !!x. x x j le i" ``` paulson@13155 ` 435` ```by (blast intro: not_lt_imp_le dest: lt_irrefl) ``` paulson@13155 ` 436` paulson@13356 ` 437` ```subsubsection{*Transitivity Laws*} ``` paulson@13155 ` 438` paulson@13155 ` 439` ```lemma lt_trans1: "[| i le j; j i i i le k" ``` paulson@13155 ` 446` ```by (blast intro: lt_trans1) ``` paulson@13155 ` 447` paulson@13155 ` 448` ```lemma succ_leI: "i succ(i) le j" ``` paulson@13155 ` 449` ```apply (rule not_lt_iff_le [THEN iffD1]) ``` paulson@13155 ` 450` ```apply (blast elim: ltE leE lt_asym)+ ``` paulson@13155 ` 451` ```done ``` paulson@13155 ` 452` paulson@13155 ` 453` ```(*Identical to succ(i) < succ(j) ==> i i i i le j" ``` paulson@13155 ` 463` ```by (blast dest!: succ_leE) ``` paulson@13155 ` 464` paulson@13155 ` 465` ```lemma lt_subset_trans: "[| i <= j; j i 0 i j" ``` paulson@13162 ` 474` ```apply auto ``` paulson@13162 ` 475` ```apply (blast intro: lt_trans le_refl dest: lt_Ord) ``` paulson@13162 ` 476` ```apply (frule lt_Ord) ``` paulson@13162 ` 477` ```apply (rule not_le_iff_lt [THEN iffD1]) ``` paulson@13162 ` 478` ``` apply (blast intro: lt_Ord2) ``` paulson@13162 ` 479` ``` apply blast ``` paulson@13162 ` 480` ```apply (simp add: lt_Ord lt_Ord2 le_iff) ``` paulson@13162 ` 481` ```apply (blast dest: lt_asym) ``` paulson@13162 ` 482` ```done ``` paulson@13162 ` 483` paulson@13243 ` 484` ```lemma Ord_succ_mem_iff: "Ord(j) ==> succ(i) \ succ(j) <-> i\j" ``` paulson@13243 ` 485` ```apply (insert succ_le_iff [of i j]) ``` paulson@13243 ` 486` ```apply (simp add: lt_def) ``` paulson@13243 ` 487` ```done ``` paulson@13243 ` 488` paulson@13356 ` 489` ```subsubsection{*Union and Intersection*} ``` paulson@13155 ` 490` paulson@13155 ` 491` ```lemma Un_upper1_le: "[| Ord(i); Ord(j) |] ==> i le i Un j" ``` paulson@13155 ` 492` ```by (rule Un_upper1 [THEN subset_imp_le], auto) ``` paulson@13155 ` 493` paulson@13155 ` 494` ```lemma Un_upper2_le: "[| Ord(i); Ord(j) |] ==> j le i Un j" ``` paulson@13155 ` 495` ```by (rule Un_upper2 [THEN subset_imp_le], auto) ``` paulson@13155 ` 496` paulson@13155 ` 497` ```(*Replacing k by succ(k') yields the similar rule for le!*) ``` paulson@13155 ` 498` ```lemma Un_least_lt: "[| i i Un j < k" ``` paulson@13784 ` 499` ```apply (rule_tac i = i and j = j in Ord_linear_le) ``` paulson@13155 ` 500` ```apply (auto simp add: Un_commute le_subset_iff subset_Un_iff lt_Ord) ``` paulson@13155 ` 501` ```done ``` paulson@13155 ` 502` paulson@13155 ` 503` ```lemma Un_least_lt_iff: "[| Ord(i); Ord(j) |] ==> i Un j < k <-> i i Un j : k <-> i:k & j:k" ``` paulson@13155 ` 511` ```apply (insert Un_least_lt_iff [of i j k]) ``` paulson@13155 ` 512` ```apply (simp add: lt_def) ``` paulson@13155 ` 513` ```done ``` paulson@13155 ` 514` paulson@13155 ` 515` ```(*Replacing k by succ(k') yields the similar rule for le!*) ``` paulson@13155 ` 516` ```lemma Int_greatest_lt: "[| i i Int j < k" ``` paulson@13784 ` 517` ```apply (rule_tac i = i and j = j in Ord_linear_le) ``` paulson@13155 ` 518` ```apply (auto simp add: Int_commute le_subset_iff subset_Int_iff lt_Ord) ``` paulson@13155 ` 519` ```done ``` paulson@13155 ` 520` paulson@13162 ` 521` ```lemma Ord_Un_if: ``` paulson@13162 ` 522` ``` "[| Ord(i); Ord(j) |] ==> i \ j = (if j succ(i \ j) = succ(i) \ succ(j)" ``` paulson@13162 ` 528` ```by (simp add: Ord_Un_if lt_Ord le_Ord2) ``` paulson@13162 ` 529` paulson@13162 ` 530` ```lemma lt_Un_iff: ``` paulson@13162 ` 531` ``` "[| Ord(i); Ord(j) |] ==> k < i \ j <-> k < i | k < j"; ``` paulson@13162 ` 532` ```apply (simp add: Ord_Un_if not_lt_iff_le) ``` paulson@13162 ` 533` ```apply (blast intro: leI lt_trans2)+ ``` paulson@13162 ` 534` ```done ``` paulson@13162 ` 535` paulson@13162 ` 536` ```lemma le_Un_iff: ``` paulson@13162 ` 537` ``` "[| Ord(i); Ord(j) |] ==> k \ i \ j <-> k \ i | k \ j"; ``` paulson@13162 ` 538` ```by (simp add: succ_Un_distrib lt_Un_iff [symmetric]) ``` paulson@13162 ` 539` paulson@13172 ` 540` ```lemma Un_upper1_lt: "[|k < i; Ord(j)|] ==> k < i Un j" ``` paulson@13172 ` 541` ```by (simp add: lt_Un_iff lt_Ord2) ``` paulson@13172 ` 542` paulson@13172 ` 543` ```lemma Un_upper2_lt: "[|k < j; Ord(i)|] ==> k < i Un j" ``` paulson@13172 ` 544` ```by (simp add: lt_Un_iff lt_Ord2) ``` paulson@13172 ` 545` paulson@13172 ` 546` ```(*See also Transset_iff_Union_succ*) ``` paulson@13172 ` 547` ```lemma Ord_Union_succ_eq: "Ord(i) ==> \(succ(i)) = i" ``` paulson@13172 ` 548` ```by (blast intro: Ord_trans) ``` paulson@13172 ` 549` paulson@13162 ` 550` paulson@13356 ` 551` ```subsection{*Results about Limits*} ``` paulson@13155 ` 552` paulson@13172 ` 553` ```lemma Ord_Union [intro,simp,TC]: "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))" ``` paulson@13155 ` 554` ```apply (rule Ord_is_Transset [THEN Transset_Union_family, THEN OrdI]) ``` paulson@13155 ` 555` ```apply (blast intro: Ord_contains_Transset)+ ``` paulson@13155 ` 556` ```done ``` paulson@13155 ` 557` paulson@13172 ` 558` ```lemma Ord_UN [intro,simp,TC]: ``` paulson@13615 ` 559` ``` "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(\x\A. B(x))" ``` paulson@13155 ` 560` ```by (rule Ord_Union, blast) ``` paulson@13155 ` 561` paulson@13203 ` 562` ```lemma Ord_Inter [intro,simp,TC]: ``` paulson@13203 ` 563` ``` "[| !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))" ``` paulson@13203 ` 564` ```apply (rule Transset_Inter_family [THEN OrdI]) ``` paulson@13203 ` 565` ```apply (blast intro: Ord_is_Transset) ``` paulson@13203 ` 566` ```apply (simp add: Inter_def) ``` paulson@13203 ` 567` ```apply (blast intro: Ord_contains_Transset) ``` paulson@13203 ` 568` ```done ``` paulson@13203 ` 569` paulson@13203 ` 570` ```lemma Ord_INT [intro,simp,TC]: ``` paulson@13615 ` 571` ``` "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(\x\A. B(x))" ``` paulson@13203 ` 572` ```by (rule Ord_Inter, blast) ``` paulson@13203 ` 573` paulson@13203 ` 574` paulson@13615 ` 575` ```(* No < version; consider (\i\nat.i)=nat *) ``` paulson@13155 ` 576` ```lemma UN_least_le: ``` paulson@13615 ` 577` ``` "[| Ord(i); !!x. x:A ==> b(x) le i |] ==> (\x\A. b(x)) le i" ``` paulson@13155 ` 578` ```apply (rule le_imp_subset [THEN UN_least, THEN subset_imp_le]) ``` paulson@13155 ` 579` ```apply (blast intro: Ord_UN elim: ltE)+ ``` paulson@13155 ` 580` ```done ``` paulson@13155 ` 581` paulson@13155 ` 582` ```lemma UN_succ_least_lt: ``` paulson@13615 ` 583` ``` "[| j b(x) (\x\A. succ(b(x))) < i" ``` paulson@13155 ` 584` ```apply (rule ltE, assumption) ``` paulson@13155 ` 585` ```apply (rule UN_least_le [THEN lt_trans2]) ``` paulson@13155 ` 586` ```apply (blast intro: succ_leI)+ ``` paulson@13155 ` 587` ```done ``` paulson@13155 ` 588` paulson@13172 ` 589` ```lemma UN_upper_lt: ``` paulson@13172 ` 590` ``` "[| a\A; i < b(a); Ord(\x\A. b(x)) |] ==> i < (\x\A. b(x))" ``` paulson@13172 ` 591` ```by (unfold lt_def, blast) ``` paulson@13172 ` 592` paulson@13155 ` 593` ```lemma UN_upper_le: ``` paulson@13615 ` 594` ``` "[| a: A; i le b(a); Ord(\x\A. b(x)) |] ==> i le (\x\A. b(x))" ``` paulson@13155 ` 595` ```apply (frule ltD) ``` paulson@13155 ` 596` ```apply (rule le_imp_subset [THEN subset_trans, THEN subset_imp_le]) ``` paulson@13155 ` 597` ```apply (blast intro: lt_Ord UN_upper)+ ``` paulson@13155 ` 598` ```done ``` paulson@13155 ` 599` paulson@13172 ` 600` ```lemma lt_Union_iff: "\i\A. Ord(i) ==> (j < \(A)) <-> (\i\A. jj; Ord(\(J)) |] ==> i \ \J" ``` paulson@13172 ` 605` ```apply (subst Union_eq_UN) ``` paulson@13172 ` 606` ```apply (rule UN_upper_le, auto) ``` paulson@13172 ` 607` ```done ``` paulson@13172 ` 608` paulson@13155 ` 609` ```lemma le_implies_UN_le_UN: ``` paulson@13615 ` 610` ``` "[| !!x. x:A ==> c(x) le d(x) |] ==> (\x\A. c(x)) le (\x\A. d(x))" ``` paulson@13155 ` 611` ```apply (rule UN_least_le) ``` paulson@13155 ` 612` ```apply (rule_tac [2] UN_upper_le) ``` paulson@13155 ` 613` ```apply (blast intro: Ord_UN le_Ord2)+ ``` paulson@13155 ` 614` ```done ``` paulson@13155 ` 615` paulson@13615 ` 616` ```lemma Ord_equality: "Ord(i) ==> (\y\i. succ(y)) = i" ``` paulson@13155 ` 617` ```by (blast intro: Ord_trans) ``` paulson@13155 ` 618` paulson@13155 ` 619` ```(*Holds for all transitive sets, not just ordinals*) ``` paulson@13155 ` 620` ```lemma Ord_Union_subset: "Ord(i) ==> Union(i) <= i" ``` paulson@13155 ` 621` ```by (blast intro: Ord_trans) ``` paulson@13155 ` 622` paulson@13155 ` 623` paulson@13356 ` 624` ```subsection{*Limit Ordinals -- General Properties*} ``` paulson@13155 ` 625` paulson@13155 ` 626` ```lemma Limit_Union_eq: "Limit(i) ==> Union(i) = i" ``` paulson@13155 ` 627` ```apply (unfold Limit_def) ``` paulson@13155 ` 628` ```apply (fast intro!: ltI elim!: ltE elim: Ord_trans) ``` paulson@13155 ` 629` ```done ``` paulson@13155 ` 630` paulson@13155 ` 631` ```lemma Limit_is_Ord: "Limit(i) ==> Ord(i)" ``` paulson@13155 ` 632` ```apply (unfold Limit_def) ``` paulson@13155 ` 633` ```apply (erule conjunct1) ``` paulson@13155 ` 634` ```done ``` paulson@13155 ` 635` paulson@13155 ` 636` ```lemma Limit_has_0: "Limit(i) ==> 0 < i" ``` paulson@13155 ` 637` ```apply (unfold Limit_def) ``` paulson@13155 ` 638` ```apply (erule conjunct2 [THEN conjunct1]) ``` paulson@13155 ` 639` ```done ``` paulson@13155 ` 640` paulson@13544 ` 641` ```lemma Limit_nonzero: "Limit(i) ==> i ~= 0" ``` paulson@13544 ` 642` ```by (drule Limit_has_0, blast) ``` paulson@13544 ` 643` paulson@13155 ` 644` ```lemma Limit_has_succ: "[| Limit(i); j succ(j) < i" ``` paulson@13155 ` 645` ```by (unfold Limit_def, blast) ``` paulson@13155 ` 646` paulson@13544 ` 647` ```lemma Limit_succ_lt_iff [simp]: "Limit(i) ==> succ(j) < i <-> (j 1 < i" ``` paulson@13172 ` 657` ```by (blast intro: Limit_has_0 Limit_has_succ) ``` paulson@13172 ` 658` paulson@13172 ` 659` ```lemma increasing_LimitI: "[| 0x\l. \y\l. x Limit(l)" ``` paulson@13544 ` 660` ```apply (unfold Limit_def, simp add: lt_Ord2, clarify) ``` paulson@13172 ` 661` ```apply (drule_tac i=y in ltD) ``` paulson@13172 ` 662` ```apply (blast intro: lt_trans1 [OF _ ltI] lt_Ord2) ``` paulson@13172 ` 663` ```done ``` paulson@13172 ` 664` paulson@13155 ` 665` ```lemma non_succ_LimitI: ``` paulson@13155 ` 666` ``` "[| 0 Limit(i)" ``` paulson@13155 ` 667` ```apply (unfold Limit_def) ``` paulson@13155 ` 668` ```apply (safe del: subsetI) ``` paulson@13155 ` 669` ```apply (rule_tac [2] not_le_iff_lt [THEN iffD1]) ``` paulson@13155 ` 670` ```apply (simp_all add: lt_Ord lt_Ord2) ``` paulson@13155 ` 671` ```apply (blast elim: leE lt_asym) ``` paulson@13155 ` 672` ```done ``` paulson@13155 ` 673` paulson@13155 ` 674` ```lemma succ_LimitE [elim!]: "Limit(succ(i)) ==> P" ``` paulson@13155 ` 675` ```apply (rule lt_irrefl) ``` paulson@13155 ` 676` ```apply (rule Limit_has_succ, assumption) ``` paulson@13155 ` 677` ```apply (erule Limit_is_Ord [THEN Ord_succD, THEN le_refl]) ``` paulson@13155 ` 678` ```done ``` paulson@13155 ` 679` paulson@13155 ` 680` ```lemma not_succ_Limit [simp]: "~ Limit(succ(i))" ``` paulson@13155 ` 681` ```by blast ``` paulson@13155 ` 682` paulson@13155 ` 683` ```lemma Limit_le_succD: "[| Limit(i); i le succ(j) |] ==> i le j" ``` paulson@13155 ` 684` ```by (blast elim!: leE) ``` paulson@13155 ` 685` paulson@13172 ` 686` paulson@13356 ` 687` ```subsubsection{*Traditional 3-Way Case Analysis on Ordinals*} ``` paulson@13155 ` 688` paulson@13155 ` 689` ```lemma Ord_cases_disj: "Ord(i) ==> i=0 | (EX j. Ord(j) & i=succ(j)) | Limit(i)" ``` paulson@13155 ` 690` ```by (blast intro!: non_succ_LimitI Ord_0_lt) ``` paulson@13155 ` 691` paulson@13155 ` 692` ```lemma Ord_cases: ``` paulson@13155 ` 693` ``` "[| Ord(i); ``` paulson@13155 ` 694` ``` i=0 ==> P; ``` paulson@13155 ` 695` ``` !!j. [| Ord(j); i=succ(j) |] ==> P; ``` paulson@13155 ` 696` ``` Limit(i) ==> P ``` paulson@13155 ` 697` ``` |] ==> P" ``` paulson@13155 ` 698` ```by (drule Ord_cases_disj, blast) ``` paulson@13155 ` 699` wenzelm@13534 ` 700` ```lemma trans_induct3 [case_names 0 succ limit, consumes 1]: ``` paulson@13155 ` 701` ``` "[| Ord(i); ``` paulson@13155 ` 702` ``` P(0); ``` paulson@13155 ` 703` ``` !!x. [| Ord(x); P(x) |] ==> P(succ(x)); ``` paulson@13155 ` 704` ``` !!x. [| Limit(x); ALL y:x. P(y) |] ==> P(x) ``` paulson@13155 ` 705` ``` |] ==> P(i)" ``` paulson@13155 ` 706` ```apply (erule trans_induct) ``` paulson@13155 ` 707` ```apply (erule Ord_cases, blast+) ``` paulson@13155 ` 708` ```done ``` paulson@13155 ` 709` wenzelm@13534 ` 710` ```lemmas trans_induct3_rule = trans_induct3 [rule_format, case_names 0 succ limit, consumes 1] ``` wenzelm@13534 ` 711` paulson@13172 ` 712` ```text{*A set of ordinals is either empty, contains its own union, or its ``` paulson@13172 ` 713` ```union is a limit ordinal.*} ``` paulson@13172 ` 714` ```lemma Ord_set_cases: ``` paulson@13172 ` 715` ``` "\i\I. Ord(i) ==> I=0 \ \(I) \ I \ (\(I) \ I \ Limit(\(I)))" ``` paulson@13172 ` 716` ```apply (clarify elim!: not_emptyE) ``` paulson@13172 ` 717` ```apply (cases "\(I)" rule: Ord_cases) ``` paulson@13172 ` 718` ``` apply (blast intro: Ord_Union) ``` paulson@13172 ` 719` ``` apply (blast intro: subst_elem) ``` paulson@13172 ` 720` ``` apply auto ``` paulson@13172 ` 721` ```apply (clarify elim!: equalityE succ_subsetE) ``` paulson@13172 ` 722` ```apply (simp add: Union_subset_iff) ``` paulson@13172 ` 723` ```apply (subgoal_tac "B = succ(j)", blast) ``` paulson@13172 ` 724` ```apply (rule le_anti_sym) ``` paulson@13172 ` 725` ``` apply (simp add: le_subset_iff) ``` paulson@13172 ` 726` ```apply (simp add: ltI) ``` paulson@13172 ` 727` ```done ``` paulson@13172 ` 728` paulson@13172 ` 729` ```text{*If the union of a set of ordinals is a successor, then it is ``` paulson@13172 ` 730` ```an element of that set.*} ``` paulson@13172 ` 731` ```lemma Ord_Union_eq_succD: "[|\x\X. Ord(x); \X = succ(j)|] ==> succ(j) \ X" ``` paulson@13172 ` 732` ```by (drule Ord_set_cases, auto) ``` paulson@13172 ` 733` paulson@13172 ` 734` ```lemma Limit_Union [rule_format]: "[| I \ 0; \i\I. Limit(i) |] ==> Limit(\I)" ``` paulson@13172 ` 735` ```apply (simp add: Limit_def lt_def) ``` paulson@13172 ` 736` ```apply (blast intro!: equalityI) ``` paulson@13172 ` 737` ```done ``` paulson@13172 ` 738` paulson@13155 ` 739` ```ML ``` paulson@13155 ` 740` ```{* ``` paulson@13155 ` 741` ```val Memrel_def = thm "Memrel_def"; ``` paulson@13155 ` 742` ```val Transset_def = thm "Transset_def"; ``` paulson@13155 ` 743` ```val Ord_def = thm "Ord_def"; ``` paulson@13155 ` 744` ```val lt_def = thm "lt_def"; ``` paulson@13155 ` 745` ```val Limit_def = thm "Limit_def"; ``` paulson@13155 ` 746` paulson@13155 ` 747` ```val Transset_iff_Pow = thm "Transset_iff_Pow"; ``` paulson@13155 ` 748` ```val Transset_iff_Union_succ = thm "Transset_iff_Union_succ"; ``` paulson@13155 ` 749` ```val Transset_iff_Union_subset = thm "Transset_iff_Union_subset"; ``` paulson@13155 ` 750` ```val Transset_doubleton_D = thm "Transset_doubleton_D"; ``` paulson@13155 ` 751` ```val Transset_Pair_D = thm "Transset_Pair_D"; ``` paulson@13155 ` 752` ```val Transset_includes_domain = thm "Transset_includes_domain"; ``` paulson@13155 ` 753` ```val Transset_includes_range = thm "Transset_includes_range"; ``` paulson@13155 ` 754` ```val Transset_0 = thm "Transset_0"; ``` paulson@13155 ` 755` ```val Transset_Un = thm "Transset_Un"; ``` paulson@13155 ` 756` ```val Transset_Int = thm "Transset_Int"; ``` paulson@13155 ` 757` ```val Transset_succ = thm "Transset_succ"; ``` paulson@13155 ` 758` ```val Transset_Pow = thm "Transset_Pow"; ``` paulson@13155 ` 759` ```val Transset_Union = thm "Transset_Union"; ``` paulson@13155 ` 760` ```val Transset_Union_family = thm "Transset_Union_family"; ``` paulson@13155 ` 761` ```val Transset_Inter_family = thm "Transset_Inter_family"; ``` paulson@13155 ` 762` ```val OrdI = thm "OrdI"; ``` paulson@13155 ` 763` ```val Ord_is_Transset = thm "Ord_is_Transset"; ``` paulson@13155 ` 764` ```val Ord_contains_Transset = thm "Ord_contains_Transset"; ``` paulson@13155 ` 765` ```val Ord_in_Ord = thm "Ord_in_Ord"; ``` paulson@13155 ` 766` ```val Ord_succD = thm "Ord_succD"; ``` paulson@13155 ` 767` ```val Ord_subset_Ord = thm "Ord_subset_Ord"; ``` paulson@13155 ` 768` ```val OrdmemD = thm "OrdmemD"; ``` paulson@13155 ` 769` ```val Ord_trans = thm "Ord_trans"; ``` paulson@13155 ` 770` ```val Ord_succ_subsetI = thm "Ord_succ_subsetI"; ``` paulson@13155 ` 771` ```val Ord_0 = thm "Ord_0"; ``` paulson@13155 ` 772` ```val Ord_succ = thm "Ord_succ"; ``` paulson@13155 ` 773` ```val Ord_1 = thm "Ord_1"; ``` paulson@13155 ` 774` ```val Ord_succ_iff = thm "Ord_succ_iff"; ``` paulson@13155 ` 775` ```val Ord_Un = thm "Ord_Un"; ``` paulson@13155 ` 776` ```val Ord_Int = thm "Ord_Int"; ``` paulson@13155 ` 777` ```val Ord_Inter = thm "Ord_Inter"; ``` paulson@13155 ` 778` ```val Ord_INT = thm "Ord_INT"; ``` paulson@13155 ` 779` ```val ON_class = thm "ON_class"; ``` paulson@13155 ` 780` ```val ltI = thm "ltI"; ``` paulson@13155 ` 781` ```val ltE = thm "ltE"; ``` paulson@13155 ` 782` ```val ltD = thm "ltD"; ``` paulson@13155 ` 783` ```val not_lt0 = thm "not_lt0"; ``` paulson@13155 ` 784` ```val lt_Ord = thm "lt_Ord"; ``` paulson@13155 ` 785` ```val lt_Ord2 = thm "lt_Ord2"; ``` paulson@13155 ` 786` ```val le_Ord2 = thm "le_Ord2"; ``` paulson@13155 ` 787` ```val lt0E = thm "lt0E"; ``` paulson@13155 ` 788` ```val lt_trans = thm "lt_trans"; ``` paulson@13155 ` 789` ```val lt_not_sym = thm "lt_not_sym"; ``` paulson@13155 ` 790` ```val lt_asym = thm "lt_asym"; ``` paulson@13155 ` 791` ```val lt_irrefl = thm "lt_irrefl"; ``` paulson@13155 ` 792` ```val lt_not_refl = thm "lt_not_refl"; ``` paulson@13155 ` 793` ```val le_iff = thm "le_iff"; ``` paulson@13155 ` 794` ```val leI = thm "leI"; ``` paulson@13155 ` 795` ```val le_eqI = thm "le_eqI"; ``` paulson@13155 ` 796` ```val le_refl = thm "le_refl"; ``` paulson@13155 ` 797` ```val le_refl_iff = thm "le_refl_iff"; ``` paulson@13155 ` 798` ```val leCI = thm "leCI"; ``` paulson@13155 ` 799` ```val leE = thm "leE"; ``` paulson@13155 ` 800` ```val le_anti_sym = thm "le_anti_sym"; ``` paulson@13155 ` 801` ```val le0_iff = thm "le0_iff"; ``` paulson@13155 ` 802` ```val le0D = thm "le0D"; ``` paulson@13155 ` 803` ```val Memrel_iff = thm "Memrel_iff"; ``` paulson@13155 ` 804` ```val MemrelI = thm "MemrelI"; ``` paulson@13155 ` 805` ```val MemrelE = thm "MemrelE"; ``` paulson@13155 ` 806` ```val Memrel_type = thm "Memrel_type"; ``` paulson@13155 ` 807` ```val Memrel_mono = thm "Memrel_mono"; ``` paulson@13155 ` 808` ```val Memrel_0 = thm "Memrel_0"; ``` paulson@13155 ` 809` ```val Memrel_1 = thm "Memrel_1"; ``` paulson@13155 ` 810` ```val wf_Memrel = thm "wf_Memrel"; ``` paulson@13155 ` 811` ```val trans_Memrel = thm "trans_Memrel"; ``` paulson@13155 ` 812` ```val Transset_Memrel_iff = thm "Transset_Memrel_iff"; ``` paulson@13155 ` 813` ```val Transset_induct = thm "Transset_induct"; ``` paulson@13155 ` 814` ```val Ord_induct = thm "Ord_induct"; ``` paulson@13155 ` 815` ```val trans_induct = thm "trans_induct"; ``` paulson@13155 ` 816` ```val Ord_linear = thm "Ord_linear"; ``` paulson@13155 ` 817` ```val Ord_linear_lt = thm "Ord_linear_lt"; ``` paulson@13155 ` 818` ```val Ord_linear2 = thm "Ord_linear2"; ``` paulson@13155 ` 819` ```val Ord_linear_le = thm "Ord_linear_le"; ``` paulson@13155 ` 820` ```val le_imp_not_lt = thm "le_imp_not_lt"; ``` paulson@13155 ` 821` ```val not_lt_imp_le = thm "not_lt_imp_le"; ``` paulson@13155 ` 822` ```val Ord_mem_iff_lt = thm "Ord_mem_iff_lt"; ``` paulson@13155 ` 823` ```val not_lt_iff_le = thm "not_lt_iff_le"; ``` paulson@13155 ` 824` ```val not_le_iff_lt = thm "not_le_iff_lt"; ``` paulson@13155 ` 825` ```val Ord_0_le = thm "Ord_0_le"; ``` paulson@13155 ` 826` ```val Ord_0_lt = thm "Ord_0_lt"; ``` paulson@13155 ` 827` ```val Ord_0_lt_iff = thm "Ord_0_lt_iff"; ``` paulson@13155 ` 828` ```val zero_le_succ_iff = thm "zero_le_succ_iff"; ``` paulson@13155 ` 829` ```val subset_imp_le = thm "subset_imp_le"; ``` paulson@13155 ` 830` ```val le_imp_subset = thm "le_imp_subset"; ``` paulson@13155 ` 831` ```val le_subset_iff = thm "le_subset_iff"; ``` paulson@13155 ` 832` ```val le_succ_iff = thm "le_succ_iff"; ``` paulson@13155 ` 833` ```val all_lt_imp_le = thm "all_lt_imp_le"; ``` paulson@13155 ` 834` ```val lt_trans1 = thm "lt_trans1"; ``` paulson@13155 ` 835` ```val lt_trans2 = thm "lt_trans2"; ``` paulson@13155 ` 836` ```val le_trans = thm "le_trans"; ``` paulson@13155 ` 837` ```val succ_leI = thm "succ_leI"; ``` paulson@13155 ` 838` ```val succ_leE = thm "succ_leE"; ``` paulson@13155 ` 839` ```val succ_le_iff = thm "succ_le_iff"; ``` paulson@13155 ` 840` ```val succ_le_imp_le = thm "succ_le_imp_le"; ``` paulson@13155 ` 841` ```val lt_subset_trans = thm "lt_subset_trans"; ``` paulson@13155 ` 842` ```val Un_upper1_le = thm "Un_upper1_le"; ``` paulson@13155 ` 843` ```val Un_upper2_le = thm "Un_upper2_le"; ``` paulson@13155 ` 844` ```val Un_least_lt = thm "Un_least_lt"; ``` paulson@13155 ` 845` ```val Un_least_lt_iff = thm "Un_least_lt_iff"; ``` paulson@13155 ` 846` ```val Un_least_mem_iff = thm "Un_least_mem_iff"; ``` paulson@13155 ` 847` ```val Int_greatest_lt = thm "Int_greatest_lt"; ``` paulson@13155 ` 848` ```val Ord_Union = thm "Ord_Union"; ``` paulson@13155 ` 849` ```val Ord_UN = thm "Ord_UN"; ``` paulson@13155 ` 850` ```val UN_least_le = thm "UN_least_le"; ``` paulson@13155 ` 851` ```val UN_succ_least_lt = thm "UN_succ_least_lt"; ``` paulson@13155 ` 852` ```val UN_upper_le = thm "UN_upper_le"; ``` paulson@13155 ` 853` ```val le_implies_UN_le_UN = thm "le_implies_UN_le_UN"; ``` paulson@13155 ` 854` ```val Ord_equality = thm "Ord_equality"; ``` paulson@13155 ` 855` ```val Ord_Union_subset = thm "Ord_Union_subset"; ``` paulson@13155 ` 856` ```val Limit_Union_eq = thm "Limit_Union_eq"; ``` paulson@13155 ` 857` ```val Limit_is_Ord = thm "Limit_is_Ord"; ``` paulson@13155 ` 858` ```val Limit_has_0 = thm "Limit_has_0"; ``` paulson@13155 ` 859` ```val Limit_has_succ = thm "Limit_has_succ"; ``` paulson@13155 ` 860` ```val non_succ_LimitI = thm "non_succ_LimitI"; ``` paulson@13155 ` 861` ```val succ_LimitE = thm "succ_LimitE"; ``` paulson@13155 ` 862` ```val not_succ_Limit = thm "not_succ_Limit"; ``` paulson@13155 ` 863` ```val Limit_le_succD = thm "Limit_le_succD"; ``` paulson@13155 ` 864` ```val Ord_cases_disj = thm "Ord_cases_disj"; ``` paulson@13155 ` 865` ```val Ord_cases = thm "Ord_cases"; ``` paulson@13155 ` 866` ```val trans_induct3 = thm "trans_induct3"; ``` paulson@13155 ` 867` ```*} ``` lcp@435 ` 868` lcp@435 ` 869` ```end ```