src/ZF/Ordinal.thy
changeset 13615 449a70d88b38
parent 13544 895994073bdf
child 13784 b9f6154427a4
     1.1 --- a/src/ZF/Ordinal.thy	Tue Oct 01 11:17:25 2002 +0200
     1.2 +++ b/src/ZF/Ordinal.thy	Tue Oct 01 13:26:10 2002 +0200
     1.3 @@ -102,11 +102,11 @@
     1.4  by (unfold Inter_def Transset_def, blast)
     1.5  
     1.6  lemma Transset_UN:
     1.7 -     "(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (UN x:A. B(x))"
     1.8 +     "(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (\<Union>x\<in>A. B(x))"
     1.9  by (rule Transset_Union_family, auto) 
    1.10  
    1.11  lemma Transset_INT:
    1.12 -     "(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (INT x:A. B(x))"
    1.13 +     "(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (\<Inter>x\<in>A. B(x))"
    1.14  by (rule Transset_Inter_family, auto) 
    1.15  
    1.16  
    1.17 @@ -555,7 +555,7 @@
    1.18  done
    1.19  
    1.20  lemma Ord_UN [intro,simp,TC]:
    1.21 -     "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(UN x:A. B(x))"
    1.22 +     "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(\<Union>x\<in>A. B(x))"
    1.23  by (rule Ord_Union, blast)
    1.24  
    1.25  lemma Ord_Inter [intro,simp,TC]:
    1.26 @@ -567,19 +567,19 @@
    1.27  done
    1.28  
    1.29  lemma Ord_INT [intro,simp,TC]:
    1.30 -    "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(INT x:A. B(x))"
    1.31 +    "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(\<Inter>x\<in>A. B(x))"
    1.32  by (rule Ord_Inter, blast) 
    1.33  
    1.34  
    1.35 -(* No < version; consider (UN i:nat.i)=nat *)
    1.36 +(* No < version; consider (\<Union>i\<in>nat.i)=nat *)
    1.37  lemma UN_least_le:
    1.38 -    "[| Ord(i);  !!x. x:A ==> b(x) le i |] ==> (UN x:A. b(x)) le i"
    1.39 +    "[| Ord(i);  !!x. x:A ==> b(x) le i |] ==> (\<Union>x\<in>A. b(x)) le i"
    1.40  apply (rule le_imp_subset [THEN UN_least, THEN subset_imp_le])
    1.41  apply (blast intro: Ord_UN elim: ltE)+
    1.42  done
    1.43  
    1.44  lemma UN_succ_least_lt:
    1.45 -    "[| j<i;  !!x. x:A ==> b(x)<j |] ==> (UN x:A. succ(b(x))) < i"
    1.46 +    "[| j<i;  !!x. x:A ==> b(x)<j |] ==> (\<Union>x\<in>A. succ(b(x))) < i"
    1.47  apply (rule ltE, assumption)
    1.48  apply (rule UN_least_le [THEN lt_trans2])
    1.49  apply (blast intro: succ_leI)+
    1.50 @@ -590,7 +590,7 @@
    1.51  by (unfold lt_def, blast) 
    1.52  
    1.53  lemma UN_upper_le:
    1.54 -     "[| a: A;  i le b(a);  Ord(UN x:A. b(x)) |] ==> i le (UN x:A. b(x))"
    1.55 +     "[| a: A;  i le b(a);  Ord(\<Union>x\<in>A. b(x)) |] ==> i le (\<Union>x\<in>A. b(x))"
    1.56  apply (frule ltD)
    1.57  apply (rule le_imp_subset [THEN subset_trans, THEN subset_imp_le])
    1.58  apply (blast intro: lt_Ord UN_upper)+
    1.59 @@ -606,13 +606,13 @@
    1.60  done
    1.61  
    1.62  lemma le_implies_UN_le_UN:
    1.63 -    "[| !!x. x:A ==> c(x) le d(x) |] ==> (UN x:A. c(x)) le (UN x:A. d(x))"
    1.64 +    "[| !!x. x:A ==> c(x) le d(x) |] ==> (\<Union>x\<in>A. c(x)) le (\<Union>x\<in>A. d(x))"
    1.65  apply (rule UN_least_le)
    1.66  apply (rule_tac [2] UN_upper_le)
    1.67  apply (blast intro: Ord_UN le_Ord2)+ 
    1.68  done
    1.69  
    1.70 -lemma Ord_equality: "Ord(i) ==> (UN y:i. succ(y)) = i"
    1.71 +lemma Ord_equality: "Ord(i) ==> (\<Union>y\<in>i. succ(y)) = i"
    1.72  by (blast intro: Ord_trans)
    1.73  
    1.74  (*Holds for all transitive sets, not just ordinals*)