src/ZF/Ordinal.thy
changeset 13203 fac77a839aa2
parent 13172 03a5afa7b888
child 13243 ba53d07d32d5
     1.1 --- a/src/ZF/Ordinal.thy	Wed Jun 05 12:24:14 2002 +0200
     1.2 +++ b/src/ZF/Ordinal.thy	Wed Jun 05 15:34:55 2002 +0200
     1.3 @@ -97,8 +97,17 @@
     1.4  by (unfold Transset_def, blast)
     1.5  
     1.6  lemma Transset_Inter_family: 
     1.7 -    "[| j:A;  !!i. i:A ==> Transset(i) |] ==> Transset(Inter(A))"
     1.8 -by (unfold Transset_def, blast)
     1.9 +    "[| !!i. i:A ==> Transset(i) |] ==> Transset(Inter(A))"
    1.10 +by (unfold Inter_def Transset_def, blast)
    1.11 +
    1.12 +lemma Transset_UN:
    1.13 +     "(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (UN x:A. B(x))"
    1.14 +by (rule Transset_Union_family, auto) 
    1.15 +
    1.16 +lemma Transset_INT:
    1.17 +     "(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (INT x:A. B(x))"
    1.18 +by (rule Transset_Inter_family, auto) 
    1.19 +
    1.20  
    1.21  (*** Natural Deduction rules for Ord ***)
    1.22  
    1.23 @@ -157,18 +166,6 @@
    1.24  apply (blast intro!: Transset_Int)
    1.25  done
    1.26  
    1.27 -
    1.28 -lemma Ord_Inter:
    1.29 -    "[| j:A;  !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))"
    1.30 -apply (rule Transset_Inter_family [THEN OrdI], assumption)
    1.31 -apply (blast intro: Ord_is_Transset) 
    1.32 -apply (blast intro: Ord_contains_Transset) 
    1.33 -done
    1.34 -
    1.35 -lemma Ord_INT:
    1.36 -    "[| j:A;  !!x. x:A ==> Ord(B(x)) |] ==> Ord(INT x:A. B(x))"
    1.37 -by (rule RepFunI [THEN Ord_Inter], assumption, blast) 
    1.38 -
    1.39  (*There is no set of all ordinals, for then it would contain itself*)
    1.40  lemma ON_class: "~ (ALL i. i:X <-> Ord(i))"
    1.41  apply (rule notI)
    1.42 @@ -532,8 +529,6 @@
    1.43  by (blast intro: Ord_trans)
    1.44  
    1.45  
    1.46 -(*FIXME: the Intersection duals are missing!*)
    1.47 -
    1.48  (*** Results about limits ***)
    1.49  
    1.50  lemma Ord_Union [intro,simp,TC]: "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))"
    1.51 @@ -545,6 +540,19 @@
    1.52       "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(UN x:A. B(x))"
    1.53  by (rule Ord_Union, blast)
    1.54  
    1.55 +lemma Ord_Inter [intro,simp,TC]:
    1.56 +    "[| !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))" 
    1.57 +apply (rule Transset_Inter_family [THEN OrdI])
    1.58 +apply (blast intro: Ord_is_Transset) 
    1.59 +apply (simp add: Inter_def) 
    1.60 +apply (blast intro: Ord_contains_Transset) 
    1.61 +done
    1.62 +
    1.63 +lemma Ord_INT [intro,simp,TC]:
    1.64 +    "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(INT x:A. B(x))"
    1.65 +by (rule Ord_Inter, blast) 
    1.66 +
    1.67 +
    1.68  (* No < version; consider (UN i:nat.i)=nat *)
    1.69  lemma UN_least_le:
    1.70      "[| Ord(i);  !!x. x:A ==> b(x) le i |] ==> (UN x:A. b(x)) le i"