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.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.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:
```