src/ZF/Ordinal.thy
changeset 13155 dcbf6cb95534
parent 12114 a8e860c86252
child 13162 660a71e712af
     1.1 --- a/src/ZF/Ordinal.thy	Wed May 15 13:50:38 2002 +0200
     1.2 +++ b/src/ZF/Ordinal.thy	Thu May 16 09:16:22 2002 +0200
     1.3 @@ -6,27 +6,728 @@
     1.4  Ordinals in Zermelo-Fraenkel Set Theory 
     1.5  *)
     1.6  
     1.7 -Ordinal = WF + Bool + equalities +
     1.8 -consts
     1.9 -  Memrel        :: i=>i
    1.10 -  Transset,Ord  :: i=>o
    1.11 -  "<"           :: [i,i] => o  (infixl 50) (*less than on ordinals*)
    1.12 -  Limit         :: i=>o
    1.13 +theory Ordinal = WF + Bool + equalities:
    1.14 +
    1.15 +constdefs
    1.16 +
    1.17 +  Memrel        :: "i=>i"
    1.18 +    "Memrel(A)   == {z: A*A . EX x y. z=<x,y> & x:y }"
    1.19 +
    1.20 +  Transset  :: "i=>o"
    1.21 +    "Transset(i) == ALL x:i. x<=i"
    1.22 +
    1.23 +  Ord  :: "i=>o"
    1.24 +    "Ord(i)      == Transset(i) & (ALL x:i. Transset(x))"
    1.25 +
    1.26 +  lt        :: "[i,i] => o"  (infixl "<" 50)   (*less-than on ordinals*)
    1.27 +    "i<j         == i:j & Ord(j)"
    1.28 +
    1.29 +  Limit         :: "i=>o"
    1.30 +    "Limit(i)    == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
    1.31  
    1.32  syntax
    1.33 -  "le"          :: [i,i] => o  (infixl 50) (*less than or equals*)
    1.34 +  "le"          :: "[i,i] => o"  (infixl 50)   (*less-than or equals*)
    1.35  
    1.36  translations
    1.37    "x le y"      == "x < succ(y)"
    1.38  
    1.39  syntax (xsymbols)
    1.40 -  "op le"       :: [i,i] => o  (infixl "\\<le>" 50) (*less than or equals*)
    1.41 +  "op le"       :: "[i,i] => o"  (infixl "\<le>" 50)  (*less-than or equals*)
    1.42 +
    1.43 +
    1.44 +(*** Rules for Transset ***)
    1.45 +
    1.46 +(** Three neat characterisations of Transset **)
    1.47 +
    1.48 +lemma Transset_iff_Pow: "Transset(A) <-> A<=Pow(A)"
    1.49 +by (unfold Transset_def, blast)
    1.50 +
    1.51 +lemma Transset_iff_Union_succ: "Transset(A) <-> Union(succ(A)) = A"
    1.52 +apply (unfold Transset_def)
    1.53 +apply (blast elim!: equalityE)
    1.54 +done
    1.55 +
    1.56 +lemma Transset_iff_Union_subset: "Transset(A) <-> Union(A) <= A"
    1.57 +by (unfold Transset_def, blast)
    1.58 +
    1.59 +(** Consequences of downwards closure **)
    1.60 +
    1.61 +lemma Transset_doubleton_D: 
    1.62 +    "[| Transset(C); {a,b}: C |] ==> a:C & b: C"
    1.63 +by (unfold Transset_def, blast)
    1.64 +
    1.65 +lemma Transset_Pair_D:
    1.66 +    "[| Transset(C); <a,b>: C |] ==> a:C & b: C"
    1.67 +apply (simp add: Pair_def)
    1.68 +apply (blast dest: Transset_doubleton_D)
    1.69 +done
    1.70 +
    1.71 +lemma Transset_includes_domain:
    1.72 +    "[| Transset(C); A*B <= C; b: B |] ==> A <= C"
    1.73 +by (blast dest: Transset_Pair_D)
    1.74 +
    1.75 +lemma Transset_includes_range:
    1.76 +    "[| Transset(C); A*B <= C; a: A |] ==> B <= C"
    1.77 +by (blast dest: Transset_Pair_D)
    1.78 +
    1.79 +(** Closure properties **)
    1.80 +
    1.81 +lemma Transset_0: "Transset(0)"
    1.82 +by (unfold Transset_def, blast)
    1.83 +
    1.84 +lemma Transset_Un: 
    1.85 +    "[| Transset(i);  Transset(j) |] ==> Transset(i Un j)"
    1.86 +by (unfold Transset_def, blast)
    1.87 +
    1.88 +lemma Transset_Int: 
    1.89 +    "[| Transset(i);  Transset(j) |] ==> Transset(i Int j)"
    1.90 +by (unfold Transset_def, blast)
    1.91 +
    1.92 +lemma Transset_succ: "Transset(i) ==> Transset(succ(i))"
    1.93 +by (unfold Transset_def, blast)
    1.94 +
    1.95 +lemma Transset_Pow: "Transset(i) ==> Transset(Pow(i))"
    1.96 +by (unfold Transset_def, blast)
    1.97 +
    1.98 +lemma Transset_Union: "Transset(A) ==> Transset(Union(A))"
    1.99 +by (unfold Transset_def, blast)
   1.100 +
   1.101 +lemma Transset_Union_family: 
   1.102 +    "[| !!i. i:A ==> Transset(i) |] ==> Transset(Union(A))"
   1.103 +by (unfold Transset_def, blast)
   1.104 +
   1.105 +lemma Transset_Inter_family: 
   1.106 +    "[| j:A;  !!i. i:A ==> Transset(i) |] ==> Transset(Inter(A))"
   1.107 +by (unfold Transset_def, blast)
   1.108 +
   1.109 +(*** Natural Deduction rules for Ord ***)
   1.110 +
   1.111 +lemma OrdI:
   1.112 +    "[| Transset(i);  !!x. x:i ==> Transset(x) |]  ==>  Ord(i)"
   1.113 +by (simp add: Ord_def) 
   1.114 +
   1.115 +lemma Ord_is_Transset: "Ord(i) ==> Transset(i)"
   1.116 +by (simp add: Ord_def) 
   1.117 +
   1.118 +lemma Ord_contains_Transset: 
   1.119 +    "[| Ord(i);  j:i |] ==> Transset(j) "
   1.120 +by (unfold Ord_def, blast)
   1.121 +
   1.122 +(*** Lemmas for ordinals ***)
   1.123 +
   1.124 +lemma Ord_in_Ord: "[| Ord(i);  j:i |] ==> Ord(j)"
   1.125 +by (unfold Ord_def Transset_def, blast)
   1.126 +
   1.127 +(* Ord(succ(j)) ==> Ord(j) *)
   1.128 +lemmas Ord_succD = Ord_in_Ord [OF _ succI1]
   1.129 +
   1.130 +lemma Ord_subset_Ord: "[| Ord(i);  Transset(j);  j<=i |] ==> Ord(j)"
   1.131 +by (simp add: Ord_def Transset_def, blast)
   1.132 +
   1.133 +lemma OrdmemD: "[| j:i;  Ord(i) |] ==> j<=i"
   1.134 +by (unfold Ord_def Transset_def, blast)
   1.135 +
   1.136 +lemma Ord_trans: "[| i:j;  j:k;  Ord(k) |] ==> i:k"
   1.137 +by (blast dest: OrdmemD)
   1.138 +
   1.139 +lemma Ord_succ_subsetI: "[| i:j;  Ord(j) |] ==> succ(i) <= j"
   1.140 +by (blast dest: OrdmemD)
   1.141 +
   1.142 +
   1.143 +(*** The construction of ordinals: 0, succ, Union ***)
   1.144 +
   1.145 +lemma Ord_0 [iff,TC]: "Ord(0)"
   1.146 +by (blast intro: OrdI Transset_0)
   1.147 +
   1.148 +lemma Ord_succ [TC]: "Ord(i) ==> Ord(succ(i))"
   1.149 +by (blast intro: OrdI Transset_succ Ord_is_Transset Ord_contains_Transset)
   1.150 +
   1.151 +lemmas Ord_1 = Ord_0 [THEN Ord_succ]
   1.152 +
   1.153 +lemma Ord_succ_iff [iff]: "Ord(succ(i)) <-> Ord(i)"
   1.154 +by (blast intro: Ord_succ dest!: Ord_succD)
   1.155 +
   1.156 +lemma Ord_Un [TC]: "[| Ord(i); Ord(j) |] ==> Ord(i Un j)"
   1.157 +apply (unfold Ord_def)
   1.158 +apply (blast intro!: Transset_Un)
   1.159 +done
   1.160 +
   1.161 +lemma Ord_Int [TC]: "[| Ord(i); Ord(j) |] ==> Ord(i Int j)"
   1.162 +apply (unfold Ord_def)
   1.163 +apply (blast intro!: Transset_Int)
   1.164 +done
   1.165 +
   1.166 +
   1.167 +lemma Ord_Inter:
   1.168 +    "[| j:A;  !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))"
   1.169 +apply (rule Transset_Inter_family [THEN OrdI], assumption)
   1.170 +apply (blast intro: Ord_is_Transset) 
   1.171 +apply (blast intro: Ord_contains_Transset) 
   1.172 +done
   1.173 +
   1.174 +lemma Ord_INT:
   1.175 +    "[| j:A;  !!x. x:A ==> Ord(B(x)) |] ==> Ord(INT x:A. B(x))"
   1.176 +by (rule RepFunI [THEN Ord_Inter], assumption, blast) 
   1.177 +
   1.178 +(*There is no set of all ordinals, for then it would contain itself*)
   1.179 +lemma ON_class: "~ (ALL i. i:X <-> Ord(i))"
   1.180 +apply (rule notI)
   1.181 +apply (frule_tac x = "X" in spec)
   1.182 +apply (safe elim!: mem_irrefl)
   1.183 +apply (erule swap, rule OrdI [OF _ Ord_is_Transset])
   1.184 +apply (simp add: Transset_def)
   1.185 +apply (blast intro: Ord_in_Ord)+
   1.186 +done
   1.187 +
   1.188 +(*** < is 'less than' for ordinals ***)
   1.189 +
   1.190 +lemma ltI: "[| i:j;  Ord(j) |] ==> i<j"
   1.191 +by (unfold lt_def, blast)
   1.192 +
   1.193 +lemma ltE:
   1.194 +    "[| i<j;  [| i:j;  Ord(i);  Ord(j) |] ==> P |] ==> P"
   1.195 +apply (unfold lt_def)
   1.196 +apply (blast intro: Ord_in_Ord)
   1.197 +done
   1.198 +
   1.199 +lemma ltD: "i<j ==> i:j"
   1.200 +by (erule ltE, assumption)
   1.201 +
   1.202 +lemma not_lt0 [simp]: "~ i<0"
   1.203 +by (unfold lt_def, blast)
   1.204 +
   1.205 +lemma lt_Ord: "j<i ==> Ord(j)"
   1.206 +by (erule ltE, assumption)
   1.207 +
   1.208 +lemma lt_Ord2: "j<i ==> Ord(i)"
   1.209 +by (erule ltE, assumption)
   1.210 +
   1.211 +(* "ja le j ==> Ord(j)" *)
   1.212 +lemmas le_Ord2 = lt_Ord2 [THEN Ord_succD]
   1.213 +
   1.214 +(* i<0 ==> R *)
   1.215 +lemmas lt0E = not_lt0 [THEN notE, elim!]
   1.216 +
   1.217 +lemma lt_trans: "[| i<j;  j<k |] ==> i<k"
   1.218 +by (blast intro!: ltI elim!: ltE intro: Ord_trans)
   1.219 +
   1.220 +lemma lt_not_sym: "i<j ==> ~ (j<i)"
   1.221 +apply (unfold lt_def)
   1.222 +apply (blast elim: mem_asym)
   1.223 +done
   1.224 +
   1.225 +(* [| i<j;  ~P ==> j<i |] ==> P *)
   1.226 +lemmas lt_asym = lt_not_sym [THEN swap]
   1.227 +
   1.228 +lemma lt_irrefl [elim!]: "i<i ==> P"
   1.229 +by (blast intro: lt_asym)
   1.230 +
   1.231 +lemma lt_not_refl: "~ i<i"
   1.232 +apply (rule notI)
   1.233 +apply (erule lt_irrefl)
   1.234 +done
   1.235 +
   1.236 +
   1.237 +(** le is less than or equals;  recall  i le j  abbrevs  i<succ(j) !! **)
   1.238 +
   1.239 +lemma le_iff: "i le j <-> i<j | (i=j & Ord(j))"
   1.240 +by (unfold lt_def, blast)
   1.241 +
   1.242 +(*Equivalently, i<j ==> i < succ(j)*)
   1.243 +lemma leI: "i<j ==> i le j"
   1.244 +by (simp (no_asm_simp) add: le_iff)
   1.245 +
   1.246 +lemma le_eqI: "[| i=j;  Ord(j) |] ==> i le j"
   1.247 +by (simp (no_asm_simp) add: le_iff)
   1.248 +
   1.249 +lemmas le_refl = refl [THEN le_eqI]
   1.250 +
   1.251 +lemma le_refl_iff [iff]: "i le i <-> Ord(i)"
   1.252 +by (simp (no_asm_simp) add: lt_not_refl le_iff)
   1.253 +
   1.254 +lemma leCI: "(~ (i=j & Ord(j)) ==> i<j) ==> i le j"
   1.255 +by (simp add: le_iff, blast)
   1.256 +
   1.257 +lemma leE:
   1.258 +    "[| i le j;  i<j ==> P;  [| i=j;  Ord(j) |] ==> P |] ==> P"
   1.259 +by (simp add: le_iff, blast)
   1.260 +
   1.261 +lemma le_anti_sym: "[| i le j;  j le i |] ==> i=j"
   1.262 +apply (simp add: le_iff)
   1.263 +apply (blast elim: lt_asym)
   1.264 +done
   1.265 +
   1.266 +lemma le0_iff [simp]: "i le 0 <-> i=0"
   1.267 +by (blast elim!: leE)
   1.268 +
   1.269 +lemmas le0D = le0_iff [THEN iffD1, dest!]
   1.270 +
   1.271 +(*** Natural Deduction rules for Memrel ***)
   1.272 +
   1.273 +(*The lemmas MemrelI/E give better speed than [iff] here*)
   1.274 +lemma Memrel_iff [simp]: "<a,b> : Memrel(A) <-> a:b & a:A & b:A"
   1.275 +by (unfold Memrel_def, blast)
   1.276 +
   1.277 +lemma MemrelI [intro!]: "[| a: b;  a: A;  b: A |] ==> <a,b> : Memrel(A)"
   1.278 +by auto
   1.279 +
   1.280 +lemma MemrelE [elim!]:
   1.281 +    "[| <a,b> : Memrel(A);   
   1.282 +        [| a: A;  b: A;  a:b |]  ==> P |]  
   1.283 +     ==> P"
   1.284 +by auto
   1.285 +
   1.286 +lemma Memrel_type: "Memrel(A) <= A*A"
   1.287 +by (unfold Memrel_def, blast)
   1.288 +
   1.289 +lemma Memrel_mono: "A<=B ==> Memrel(A) <= Memrel(B)"
   1.290 +by (unfold Memrel_def, blast)
   1.291 +
   1.292 +lemma Memrel_0 [simp]: "Memrel(0) = 0"
   1.293 +by (unfold Memrel_def, blast)
   1.294 +
   1.295 +lemma Memrel_1 [simp]: "Memrel(1) = 0"
   1.296 +by (unfold Memrel_def, blast)
   1.297 +
   1.298 +(*The membership relation (as a set) is well-founded.
   1.299 +  Proof idea: show A<=B by applying the foundation axiom to A-B *)
   1.300 +lemma wf_Memrel: "wf(Memrel(A))"
   1.301 +apply (unfold wf_def)
   1.302 +apply (rule foundation [THEN disjE, THEN allI], erule disjI1, blast) 
   1.303 +done
   1.304 +
   1.305 +(*Transset(i) does not suffice, though ALL j:i.Transset(j) does*)
   1.306 +lemma trans_Memrel: 
   1.307 +    "Ord(i) ==> trans(Memrel(i))"
   1.308 +by (unfold Ord_def Transset_def trans_def, blast)
   1.309 +
   1.310 +(*If Transset(A) then Memrel(A) internalizes the membership relation below A*)
   1.311 +lemma Transset_Memrel_iff: 
   1.312 +    "Transset(A) ==> <a,b> : Memrel(A) <-> a:b & b:A"
   1.313 +by (unfold Transset_def, blast)
   1.314 +
   1.315 +
   1.316 +(*** Transfinite induction ***)
   1.317 +
   1.318 +(*Epsilon induction over a transitive set*)
   1.319 +lemma Transset_induct: 
   1.320 +    "[| i: k;  Transset(k);                           
   1.321 +        !!x.[| x: k;  ALL y:x. P(y) |] ==> P(x) |]
   1.322 +     ==>  P(i)"
   1.323 +apply (simp add: Transset_def) 
   1.324 +apply (erule wf_Memrel [THEN wf_induct2], blast)
   1.325 +apply blast 
   1.326 +done
   1.327 +
   1.328 +(*Induction over an ordinal*)
   1.329 +lemmas Ord_induct = Transset_induct [OF _ Ord_is_Transset]
   1.330 +
   1.331 +(*Induction over the class of ordinals -- a useful corollary of Ord_induct*)
   1.332 +
   1.333 +lemma trans_induct:
   1.334 +    "[| Ord(i);  
   1.335 +        !!x.[| Ord(x);  ALL y:x. P(y) |] ==> P(x) |]
   1.336 +     ==>  P(i)"
   1.337 +apply (rule Ord_succ [THEN succI1 [THEN Ord_induct]], assumption)
   1.338 +apply (blast intro: Ord_succ [THEN Ord_in_Ord]) 
   1.339 +done
   1.340 +
   1.341 +
   1.342 +(*** Fundamental properties of the epsilon ordering (< on ordinals) ***)
   1.343 +
   1.344 +
   1.345 +(** Proving that < is a linear ordering on the ordinals **)
   1.346 +
   1.347 +lemma Ord_linear [rule_format]:
   1.348 +     "Ord(i) ==> (ALL j. Ord(j) --> i:j | i=j | j:i)"
   1.349 +apply (erule trans_induct)
   1.350 +apply (rule impI [THEN allI])
   1.351 +apply (erule_tac i=j in trans_induct) 
   1.352 +apply (blast dest: Ord_trans) 
   1.353 +done
   1.354 +
   1.355 +(*The trichotomy law for ordinals!*)
   1.356 +lemma Ord_linear_lt:
   1.357 +    "[| Ord(i);  Ord(j);  i<j ==> P;  i=j ==> P;  j<i ==> P |] ==> P"
   1.358 +apply (simp add: lt_def) 
   1.359 +apply (rule_tac i1=i and j1=j in Ord_linear [THEN disjE], blast+)
   1.360 +done
   1.361 +
   1.362 +lemma Ord_linear2:
   1.363 +    "[| Ord(i);  Ord(j);  i<j ==> P;  j le i ==> P |]  ==> P"
   1.364 +apply (rule_tac i = "i" and j = "j" in Ord_linear_lt)
   1.365 +apply (blast intro: leI le_eqI sym ) +
   1.366 +done
   1.367 +
   1.368 +lemma Ord_linear_le:
   1.369 +    "[| Ord(i);  Ord(j);  i le j ==> P;  j le i ==> P |]  ==> P"
   1.370 +apply (rule_tac i = "i" and j = "j" in Ord_linear_lt)
   1.371 +apply (blast intro: leI le_eqI ) +
   1.372 +done
   1.373 +
   1.374 +lemma le_imp_not_lt: "j le i ==> ~ i<j"
   1.375 +by (blast elim!: leE elim: lt_asym)
   1.376 +
   1.377 +lemma not_lt_imp_le: "[| ~ i<j;  Ord(i);  Ord(j) |] ==> j le i"
   1.378 +by (rule_tac i = "i" and j = "j" in Ord_linear2, auto)
   1.379 +
   1.380 +(** Some rewrite rules for <, le **)
   1.381 +
   1.382 +lemma Ord_mem_iff_lt: "Ord(j) ==> i:j <-> i<j"
   1.383 +by (unfold lt_def, blast)
   1.384 +
   1.385 +lemma not_lt_iff_le: "[| Ord(i);  Ord(j) |] ==> ~ i<j <-> j le i"
   1.386 +by (blast dest: le_imp_not_lt not_lt_imp_le)
   1.387  
   1.388 -defs
   1.389 -  Memrel_def    "Memrel(A)   == {z: A*A . EX x y. z=<x,y> & x:y }"
   1.390 -  Transset_def  "Transset(i) == ALL x:i. x<=i"
   1.391 -  Ord_def       "Ord(i)      == Transset(i) & (ALL x:i. Transset(x))"
   1.392 -  lt_def        "i<j         == i:j & Ord(j)"
   1.393 -  Limit_def     "Limit(i)    == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
   1.394 +lemma not_le_iff_lt: "[| Ord(i);  Ord(j) |] ==> ~ i le j <-> j<i"
   1.395 +by (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym])
   1.396 +
   1.397 +(*This is identical to 0<succ(i) *)
   1.398 +lemma Ord_0_le: "Ord(i) ==> 0 le i"
   1.399 +by (erule not_lt_iff_le [THEN iffD1], auto)
   1.400 +
   1.401 +lemma Ord_0_lt: "[| Ord(i);  i~=0 |] ==> 0<i"
   1.402 +apply (erule not_le_iff_lt [THEN iffD1])
   1.403 +apply (rule Ord_0, blast)
   1.404 +done
   1.405 +
   1.406 +lemma Ord_0_lt_iff: "Ord(i) ==> i~=0 <-> 0<i"
   1.407 +by (blast intro: Ord_0_lt)
   1.408 +
   1.409 +
   1.410 +(*** Results about less-than or equals ***)
   1.411 +
   1.412 +(** For ordinals, j<=i (subset) implies j le i (less-than or equals) **)
   1.413 +
   1.414 +lemma zero_le_succ_iff [iff]: "0 le succ(x) <-> Ord(x)"
   1.415 +by (blast intro: Ord_0_le elim: ltE)
   1.416 +
   1.417 +lemma subset_imp_le: "[| j<=i;  Ord(i);  Ord(j) |] ==> j le i"
   1.418 +apply (rule not_lt_iff_le [THEN iffD1], assumption)
   1.419 +apply assumption
   1.420 +apply (blast elim: ltE mem_irrefl)
   1.421 +done
   1.422 +
   1.423 +lemma le_imp_subset: "i le j ==> i<=j"
   1.424 +by (blast dest: OrdmemD elim: ltE leE)
   1.425 +
   1.426 +lemma le_subset_iff: "j le i <-> j<=i & Ord(i) & Ord(j)"
   1.427 +by (blast dest: subset_imp_le le_imp_subset elim: ltE)
   1.428 +
   1.429 +lemma le_succ_iff: "i le succ(j) <-> i le j | i=succ(j) & Ord(i)"
   1.430 +apply (simp (no_asm) add: le_iff)
   1.431 +apply blast
   1.432 +done
   1.433 +
   1.434 +(*Just a variant of subset_imp_le*)
   1.435 +lemma all_lt_imp_le: "[| Ord(i);  Ord(j);  !!x. x<j ==> x<i |] ==> j le i"
   1.436 +by (blast intro: not_lt_imp_le dest: lt_irrefl)
   1.437 +
   1.438 +(** Transitive laws **)
   1.439 +
   1.440 +lemma lt_trans1: "[| i le j;  j<k |] ==> i<k"
   1.441 +by (blast elim!: leE intro: lt_trans)
   1.442 +
   1.443 +lemma lt_trans2: "[| i<j;  j le k |] ==> i<k"
   1.444 +by (blast elim!: leE intro: lt_trans)
   1.445 +
   1.446 +lemma le_trans: "[| i le j;  j le k |] ==> i le k"
   1.447 +by (blast intro: lt_trans1)
   1.448 +
   1.449 +lemma succ_leI: "i<j ==> succ(i) le j"
   1.450 +apply (rule not_lt_iff_le [THEN iffD1]) 
   1.451 +apply (blast elim: ltE leE lt_asym)+
   1.452 +done
   1.453 +
   1.454 +(*Identical to  succ(i) < succ(j) ==> i<j  *)
   1.455 +lemma succ_leE: "succ(i) le j ==> i<j"
   1.456 +apply (rule not_le_iff_lt [THEN iffD1])
   1.457 +apply (blast elim: ltE leE lt_asym)+
   1.458 +done
   1.459 +
   1.460 +lemma succ_le_iff [iff]: "succ(i) le j <-> i<j"
   1.461 +by (blast intro: succ_leI succ_leE)
   1.462 +
   1.463 +lemma succ_le_imp_le: "succ(i) le succ(j) ==> i le j"
   1.464 +by (blast dest!: succ_leE)
   1.465 +
   1.466 +lemma lt_subset_trans: "[| i <= j;  j<k;  Ord(i) |] ==> i<k"
   1.467 +apply (rule subset_imp_le [THEN lt_trans1]) 
   1.468 +apply (blast intro: elim: ltE) +
   1.469 +done
   1.470 +
   1.471 +(** Union and Intersection **)
   1.472 +
   1.473 +lemma Un_upper1_le: "[| Ord(i); Ord(j) |] ==> i le i Un j"
   1.474 +by (rule Un_upper1 [THEN subset_imp_le], auto)
   1.475 +
   1.476 +lemma Un_upper2_le: "[| Ord(i); Ord(j) |] ==> j le i Un j"
   1.477 +by (rule Un_upper2 [THEN subset_imp_le], auto)
   1.478 +
   1.479 +(*Replacing k by succ(k') yields the similar rule for le!*)
   1.480 +lemma Un_least_lt: "[| i<k;  j<k |] ==> i Un j < k"
   1.481 +apply (rule_tac i = "i" and j = "j" in Ord_linear_le)
   1.482 +apply (auto simp add: Un_commute le_subset_iff subset_Un_iff lt_Ord) 
   1.483 +done
   1.484 +
   1.485 +lemma Un_least_lt_iff: "[| Ord(i); Ord(j) |] ==> i Un j < k  <->  i<k & j<k"
   1.486 +apply (safe intro!: Un_least_lt)
   1.487 +apply (rule_tac [2] Un_upper2_le [THEN lt_trans1])
   1.488 +apply (rule Un_upper1_le [THEN lt_trans1], auto) 
   1.489 +done
   1.490 +
   1.491 +lemma Un_least_mem_iff:
   1.492 +    "[| Ord(i); Ord(j); Ord(k) |] ==> i Un j : k  <->  i:k & j:k"
   1.493 +apply (insert Un_least_lt_iff [of i j k]) 
   1.494 +apply (simp add: lt_def)
   1.495 +done
   1.496 +
   1.497 +(*Replacing k by succ(k') yields the similar rule for le!*)
   1.498 +lemma Int_greatest_lt: "[| i<k;  j<k |] ==> i Int j < k"
   1.499 +apply (rule_tac i = "i" and j = "j" in Ord_linear_le)
   1.500 +apply (auto simp add: Int_commute le_subset_iff subset_Int_iff lt_Ord) 
   1.501 +done
   1.502 +
   1.503 +(*FIXME: the Intersection duals are missing!*)
   1.504 +
   1.505 +(*** Results about limits ***)
   1.506 +
   1.507 +lemma Ord_Union: "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))"
   1.508 +apply (rule Ord_is_Transset [THEN Transset_Union_family, THEN OrdI])
   1.509 +apply (blast intro: Ord_contains_Transset)+
   1.510 +done
   1.511 +
   1.512 +lemma Ord_UN: "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(UN x:A. B(x))"
   1.513 +by (rule Ord_Union, blast)
   1.514 +
   1.515 +(* No < version; consider (UN i:nat.i)=nat *)
   1.516 +lemma UN_least_le:
   1.517 +    "[| Ord(i);  !!x. x:A ==> b(x) le i |] ==> (UN x:A. b(x)) le i"
   1.518 +apply (rule le_imp_subset [THEN UN_least, THEN subset_imp_le])
   1.519 +apply (blast intro: Ord_UN elim: ltE)+
   1.520 +done
   1.521 +
   1.522 +lemma UN_succ_least_lt:
   1.523 +    "[| j<i;  !!x. x:A ==> b(x)<j |] ==> (UN x:A. succ(b(x))) < i"
   1.524 +apply (rule ltE, assumption)
   1.525 +apply (rule UN_least_le [THEN lt_trans2])
   1.526 +apply (blast intro: succ_leI)+
   1.527 +done
   1.528 +
   1.529 +lemma UN_upper_le:
   1.530 +     "[| a: A;  i le b(a);  Ord(UN x:A. b(x)) |] ==> i le (UN x:A. b(x))"
   1.531 +apply (frule ltD)
   1.532 +apply (rule le_imp_subset [THEN subset_trans, THEN subset_imp_le])
   1.533 +apply (blast intro: lt_Ord UN_upper)+
   1.534 +done
   1.535 +
   1.536 +lemma le_implies_UN_le_UN:
   1.537 +    "[| !!x. x:A ==> c(x) le d(x) |] ==> (UN x:A. c(x)) le (UN x:A. d(x))"
   1.538 +apply (rule UN_least_le)
   1.539 +apply (rule_tac [2] UN_upper_le)
   1.540 +apply (blast intro: Ord_UN le_Ord2)+ 
   1.541 +done
   1.542 +
   1.543 +lemma Ord_equality: "Ord(i) ==> (UN y:i. succ(y)) = i"
   1.544 +by (blast intro: Ord_trans)
   1.545 +
   1.546 +(*Holds for all transitive sets, not just ordinals*)
   1.547 +lemma Ord_Union_subset: "Ord(i) ==> Union(i) <= i"
   1.548 +by (blast intro: Ord_trans)
   1.549 +
   1.550 +
   1.551 +(*** Limit ordinals -- general properties ***)
   1.552 +
   1.553 +lemma Limit_Union_eq: "Limit(i) ==> Union(i) = i"
   1.554 +apply (unfold Limit_def)
   1.555 +apply (fast intro!: ltI elim!: ltE elim: Ord_trans)
   1.556 +done
   1.557 +
   1.558 +lemma Limit_is_Ord: "Limit(i) ==> Ord(i)"
   1.559 +apply (unfold Limit_def)
   1.560 +apply (erule conjunct1)
   1.561 +done
   1.562 +
   1.563 +lemma Limit_has_0: "Limit(i) ==> 0 < i"
   1.564 +apply (unfold Limit_def)
   1.565 +apply (erule conjunct2 [THEN conjunct1])
   1.566 +done
   1.567 +
   1.568 +lemma Limit_has_succ: "[| Limit(i);  j<i |] ==> succ(j) < i"
   1.569 +by (unfold Limit_def, blast)
   1.570 +
   1.571 +lemma non_succ_LimitI: 
   1.572 +    "[| 0<i;  ALL y. succ(y) ~= i |] ==> Limit(i)"
   1.573 +apply (unfold Limit_def)
   1.574 +apply (safe del: subsetI)
   1.575 +apply (rule_tac [2] not_le_iff_lt [THEN iffD1])
   1.576 +apply (simp_all add: lt_Ord lt_Ord2) 
   1.577 +apply (blast elim: leE lt_asym)
   1.578 +done
   1.579 +
   1.580 +lemma succ_LimitE [elim!]: "Limit(succ(i)) ==> P"
   1.581 +apply (rule lt_irrefl)
   1.582 +apply (rule Limit_has_succ, assumption)
   1.583 +apply (erule Limit_is_Ord [THEN Ord_succD, THEN le_refl])
   1.584 +done
   1.585 +
   1.586 +lemma not_succ_Limit [simp]: "~ Limit(succ(i))"
   1.587 +by blast
   1.588 +
   1.589 +lemma Limit_le_succD: "[| Limit(i);  i le succ(j) |] ==> i le j"
   1.590 +by (blast elim!: leE)
   1.591 +
   1.592 +(** Traditional 3-way case analysis on ordinals **)
   1.593 +
   1.594 +lemma Ord_cases_disj: "Ord(i) ==> i=0 | (EX j. Ord(j) & i=succ(j)) | Limit(i)"
   1.595 +by (blast intro!: non_succ_LimitI Ord_0_lt)
   1.596 +
   1.597 +lemma Ord_cases:
   1.598 +    "[| Ord(i);                  
   1.599 +        i=0                          ==> P;      
   1.600 +        !!j. [| Ord(j); i=succ(j) |] ==> P;      
   1.601 +        Limit(i)                     ==> P       
   1.602 +     |] ==> P"
   1.603 +by (drule Ord_cases_disj, blast)  
   1.604 +
   1.605 +lemma trans_induct3:
   1.606 +     "[| Ord(i);                 
   1.607 +         P(0);                   
   1.608 +         !!x. [| Ord(x);  P(x) |] ==> P(succ(x));        
   1.609 +         !!x. [| Limit(x);  ALL y:x. P(y) |] ==> P(x)    
   1.610 +      |] ==> P(i)"
   1.611 +apply (erule trans_induct)
   1.612 +apply (erule Ord_cases, blast+)
   1.613 +done
   1.614 +
   1.615 +ML 
   1.616 +{*
   1.617 +val Memrel_def = thm "Memrel_def";
   1.618 +val Transset_def = thm "Transset_def";
   1.619 +val Ord_def = thm "Ord_def";
   1.620 +val lt_def = thm "lt_def";
   1.621 +val Limit_def = thm "Limit_def";
   1.622 +
   1.623 +val Transset_iff_Pow = thm "Transset_iff_Pow";
   1.624 +val Transset_iff_Union_succ = thm "Transset_iff_Union_succ";
   1.625 +val Transset_iff_Union_subset = thm "Transset_iff_Union_subset";
   1.626 +val Transset_doubleton_D = thm "Transset_doubleton_D";
   1.627 +val Transset_Pair_D = thm "Transset_Pair_D";
   1.628 +val Transset_includes_domain = thm "Transset_includes_domain";
   1.629 +val Transset_includes_range = thm "Transset_includes_range";
   1.630 +val Transset_0 = thm "Transset_0";
   1.631 +val Transset_Un = thm "Transset_Un";
   1.632 +val Transset_Int = thm "Transset_Int";
   1.633 +val Transset_succ = thm "Transset_succ";
   1.634 +val Transset_Pow = thm "Transset_Pow";
   1.635 +val Transset_Union = thm "Transset_Union";
   1.636 +val Transset_Union_family = thm "Transset_Union_family";
   1.637 +val Transset_Inter_family = thm "Transset_Inter_family";
   1.638 +val OrdI = thm "OrdI";
   1.639 +val Ord_is_Transset = thm "Ord_is_Transset";
   1.640 +val Ord_contains_Transset = thm "Ord_contains_Transset";
   1.641 +val Ord_in_Ord = thm "Ord_in_Ord";
   1.642 +val Ord_succD = thm "Ord_succD";
   1.643 +val Ord_subset_Ord = thm "Ord_subset_Ord";
   1.644 +val OrdmemD = thm "OrdmemD";
   1.645 +val Ord_trans = thm "Ord_trans";
   1.646 +val Ord_succ_subsetI = thm "Ord_succ_subsetI";
   1.647 +val Ord_0 = thm "Ord_0";
   1.648 +val Ord_succ = thm "Ord_succ";
   1.649 +val Ord_1 = thm "Ord_1";
   1.650 +val Ord_succ_iff = thm "Ord_succ_iff";
   1.651 +val Ord_Un = thm "Ord_Un";
   1.652 +val Ord_Int = thm "Ord_Int";
   1.653 +val Ord_Inter = thm "Ord_Inter";
   1.654 +val Ord_INT = thm "Ord_INT";
   1.655 +val ON_class = thm "ON_class";
   1.656 +val ltI = thm "ltI";
   1.657 +val ltE = thm "ltE";
   1.658 +val ltD = thm "ltD";
   1.659 +val not_lt0 = thm "not_lt0";
   1.660 +val lt_Ord = thm "lt_Ord";
   1.661 +val lt_Ord2 = thm "lt_Ord2";
   1.662 +val le_Ord2 = thm "le_Ord2";
   1.663 +val lt0E = thm "lt0E";
   1.664 +val lt_trans = thm "lt_trans";
   1.665 +val lt_not_sym = thm "lt_not_sym";
   1.666 +val lt_asym = thm "lt_asym";
   1.667 +val lt_irrefl = thm "lt_irrefl";
   1.668 +val lt_not_refl = thm "lt_not_refl";
   1.669 +val le_iff = thm "le_iff";
   1.670 +val leI = thm "leI";
   1.671 +val le_eqI = thm "le_eqI";
   1.672 +val le_refl = thm "le_refl";
   1.673 +val le_refl_iff = thm "le_refl_iff";
   1.674 +val leCI = thm "leCI";
   1.675 +val leE = thm "leE";
   1.676 +val le_anti_sym = thm "le_anti_sym";
   1.677 +val le0_iff = thm "le0_iff";
   1.678 +val le0D = thm "le0D";
   1.679 +val Memrel_iff = thm "Memrel_iff";
   1.680 +val MemrelI = thm "MemrelI";
   1.681 +val MemrelE = thm "MemrelE";
   1.682 +val Memrel_type = thm "Memrel_type";
   1.683 +val Memrel_mono = thm "Memrel_mono";
   1.684 +val Memrel_0 = thm "Memrel_0";
   1.685 +val Memrel_1 = thm "Memrel_1";
   1.686 +val wf_Memrel = thm "wf_Memrel";
   1.687 +val trans_Memrel = thm "trans_Memrel";
   1.688 +val Transset_Memrel_iff = thm "Transset_Memrel_iff";
   1.689 +val Transset_induct = thm "Transset_induct";
   1.690 +val Ord_induct = thm "Ord_induct";
   1.691 +val trans_induct = thm "trans_induct";
   1.692 +val Ord_linear = thm "Ord_linear";
   1.693 +val Ord_linear_lt = thm "Ord_linear_lt";
   1.694 +val Ord_linear2 = thm "Ord_linear2";
   1.695 +val Ord_linear_le = thm "Ord_linear_le";
   1.696 +val le_imp_not_lt = thm "le_imp_not_lt";
   1.697 +val not_lt_imp_le = thm "not_lt_imp_le";
   1.698 +val Ord_mem_iff_lt = thm "Ord_mem_iff_lt";
   1.699 +val not_lt_iff_le = thm "not_lt_iff_le";
   1.700 +val not_le_iff_lt = thm "not_le_iff_lt";
   1.701 +val Ord_0_le = thm "Ord_0_le";
   1.702 +val Ord_0_lt = thm "Ord_0_lt";
   1.703 +val Ord_0_lt_iff = thm "Ord_0_lt_iff";
   1.704 +val zero_le_succ_iff = thm "zero_le_succ_iff";
   1.705 +val subset_imp_le = thm "subset_imp_le";
   1.706 +val le_imp_subset = thm "le_imp_subset";
   1.707 +val le_subset_iff = thm "le_subset_iff";
   1.708 +val le_succ_iff = thm "le_succ_iff";
   1.709 +val all_lt_imp_le = thm "all_lt_imp_le";
   1.710 +val lt_trans1 = thm "lt_trans1";
   1.711 +val lt_trans2 = thm "lt_trans2";
   1.712 +val le_trans = thm "le_trans";
   1.713 +val succ_leI = thm "succ_leI";
   1.714 +val succ_leE = thm "succ_leE";
   1.715 +val succ_le_iff = thm "succ_le_iff";
   1.716 +val succ_le_imp_le = thm "succ_le_imp_le";
   1.717 +val lt_subset_trans = thm "lt_subset_trans";
   1.718 +val Un_upper1_le = thm "Un_upper1_le";
   1.719 +val Un_upper2_le = thm "Un_upper2_le";
   1.720 +val Un_least_lt = thm "Un_least_lt";
   1.721 +val Un_least_lt_iff = thm "Un_least_lt_iff";
   1.722 +val Un_least_mem_iff = thm "Un_least_mem_iff";
   1.723 +val Int_greatest_lt = thm "Int_greatest_lt";
   1.724 +val Ord_Union = thm "Ord_Union";
   1.725 +val Ord_UN = thm "Ord_UN";
   1.726 +val UN_least_le = thm "UN_least_le";
   1.727 +val UN_succ_least_lt = thm "UN_succ_least_lt";
   1.728 +val UN_upper_le = thm "UN_upper_le";
   1.729 +val le_implies_UN_le_UN = thm "le_implies_UN_le_UN";
   1.730 +val Ord_equality = thm "Ord_equality";
   1.731 +val Ord_Union_subset = thm "Ord_Union_subset";
   1.732 +val Limit_Union_eq = thm "Limit_Union_eq";
   1.733 +val Limit_is_Ord = thm "Limit_is_Ord";
   1.734 +val Limit_has_0 = thm "Limit_has_0";
   1.735 +val Limit_has_succ = thm "Limit_has_succ";
   1.736 +val non_succ_LimitI = thm "non_succ_LimitI";
   1.737 +val succ_LimitE = thm "succ_LimitE";
   1.738 +val not_succ_Limit = thm "not_succ_Limit";
   1.739 +val Limit_le_succD = thm "Limit_le_succD";
   1.740 +val Ord_cases_disj = thm "Ord_cases_disj";
   1.741 +val Ord_cases = thm "Ord_cases";
   1.742 +val trans_induct3 = thm "trans_induct3";
   1.743 +*}
   1.744  
   1.745  end