src/ZF/OrdQuant.thy
changeset 13615 449a70d88b38
parent 13462 56610e2ba220
child 13807 a28a8fbc76d4
     1.1 --- a/src/ZF/OrdQuant.thy	Tue Oct 01 11:17:25 2002 +0200
     1.2 +++ b/src/ZF/OrdQuant.thy	Tue Oct 01 13:26:10 2002 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  
     1.5    (* Ordinal Union *)
     1.6    OUnion :: "[i, i => i] => i"
     1.7 -    "OUnion(i,B) == {z: UN x:i. B(x). Ord(i)}"
     1.8 +    "OUnion(i,B) == {z: \<Union>x\<in>i. B(x). Ord(i)}"
     1.9  
    1.10  syntax
    1.11    "@oall"     :: "[idt, i, o] => o"        ("(3ALL _<_./ _)" 10)
    1.12 @@ -77,31 +77,31 @@
    1.13  apply (auto simp add: lt_def)
    1.14  done
    1.15  
    1.16 -lemma Limit_OUN_eq: "Limit(i) ==> (UN x<i. x) = i"
    1.17 +lemma Limit_OUN_eq: "Limit(i) ==> (\<Union>x<i. x) = i"
    1.18  by (simp add: OUnion_def Limit_Union_eq Limit_is_Ord)
    1.19  
    1.20 -(* No < version; consider (UN i:nat.i)=nat *)
    1.21 +(* No < version; consider (\<Union>i\<in>nat.i)=nat *)
    1.22  lemma OUN_least:
    1.23 -     "(!!x. x<A ==> B(x) \<subseteq> C) ==> (UN x<A. B(x)) \<subseteq> C"
    1.24 +     "(!!x. x<A ==> B(x) \<subseteq> C) ==> (\<Union>x<A. B(x)) \<subseteq> C"
    1.25  by (simp add: OUnion_def UN_least ltI)
    1.26  
    1.27 -(* No < version; consider (UN i:nat.i)=nat *)
    1.28 +(* No < version; consider (\<Union>i\<in>nat.i)=nat *)
    1.29  lemma OUN_least_le:
    1.30 -     "[| Ord(i);  !!x. x<A ==> b(x) \<le> i |] ==> (UN x<A. b(x)) \<le> i"
    1.31 +     "[| Ord(i);  !!x. x<A ==> b(x) \<le> i |] ==> (\<Union>x<A. b(x)) \<le> i"
    1.32  by (simp add: OUnion_def UN_least_le ltI Ord_0_le)
    1.33  
    1.34  lemma le_implies_OUN_le_OUN:
    1.35 -     "[| !!x. x<A ==> c(x) \<le> d(x) |] ==> (UN x<A. c(x)) \<le> (UN x<A. d(x))"
    1.36 +     "[| !!x. x<A ==> c(x) \<le> d(x) |] ==> (\<Union>x<A. c(x)) \<le> (\<Union>x<A. d(x))"
    1.37  by (blast intro: OUN_least_le OUN_upper_le le_Ord2 Ord_OUN)
    1.38  
    1.39  lemma OUN_UN_eq:
    1.40       "(!!x. x:A ==> Ord(B(x)))
    1.41 -      ==> (UN z < (UN x:A. B(x)). C(z)) = (UN  x:A. UN z < B(x). C(z))"
    1.42 +      ==> (\<Union>z < (\<Union>x\<in>A. B(x)). C(z)) = (\<Union>x\<in>A. \<Union>z < B(x). C(z))"
    1.43  by (simp add: OUnion_def)
    1.44  
    1.45  lemma OUN_Union_eq:
    1.46       "(!!x. x:X ==> Ord(x))
    1.47 -      ==> (UN z < Union(X). C(z)) = (UN x:X. UN z < x. C(z))"
    1.48 +      ==> (\<Union>z < Union(X). C(z)) = (\<Union>x\<in>X. \<Union>z < x. C(z))"
    1.49  by (simp add: OUnion_def)
    1.50  
    1.51  (*So that rule_format will get rid of ALL x<A...*)
    1.52 @@ -165,19 +165,19 @@
    1.53  
    1.54  subsubsection {*Rules for Ordinal-Indexed Unions*}
    1.55  
    1.56 -lemma OUN_I [intro]: "[| a<i;  b: B(a) |] ==> b: (UN z<i. B(z))"
    1.57 +lemma OUN_I [intro]: "[| a<i;  b: B(a) |] ==> b: (\<Union>z<i. B(z))"
    1.58  by (unfold OUnion_def lt_def, blast)
    1.59  
    1.60  lemma OUN_E [elim!]:
    1.61 -    "[| b : (UN z<i. B(z));  !!a.[| b: B(a);  a<i |] ==> R |] ==> R"
    1.62 +    "[| b : (\<Union>z<i. B(z));  !!a.[| b: B(a);  a<i |] ==> R |] ==> R"
    1.63  apply (unfold OUnion_def lt_def, blast)
    1.64  done
    1.65  
    1.66 -lemma OUN_iff: "b : (UN x<i. B(x)) <-> (EX x<i. b : B(x))"
    1.67 +lemma OUN_iff: "b : (\<Union>x<i. B(x)) <-> (EX x<i. b : B(x))"
    1.68  by (unfold OUnion_def oex_def lt_def, blast)
    1.69  
    1.70  lemma OUN_cong [cong]:
    1.71 -    "[| i=j;  !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))"
    1.72 +    "[| i=j;  !!x. x<j ==> C(x)=D(x) |] ==> (\<Union>x<i. C(x)) = (\<Union>x<j. D(x))"
    1.73  by (simp add: OUnion_def lt_def OUN_iff)
    1.74  
    1.75  lemma lt_induct: