src/ZF/Sum.thy
 changeset 46953 2b6e55924af3 parent 46821 ff6b0c1087f2 child 58860 fee7cfa69c50
```     1.1 --- a/src/ZF/Sum.thy	Thu Mar 15 15:54:22 2012 +0000
1.2 +++ b/src/ZF/Sum.thy	Thu Mar 15 16:35:02 2012 +0000
1.3 @@ -23,24 +23,24 @@
1.4
1.5    (*operator for selecting out the various summands*)
1.6  definition Part :: "[i,i=>i] => i" where
1.7 -     "Part(A,h) == {x: A. \<exists>z. x = h(z)}"
1.8 +     "Part(A,h) == {x \<in> A. \<exists>z. x = h(z)}"
1.9
1.10  subsection{*Rules for the @{term Part} Primitive*}
1.11
1.12 -lemma Part_iff:
1.13 -    "a \<in> Part(A,h) \<longleftrightarrow> a:A & (\<exists>y. a=h(y))"
1.14 +lemma Part_iff:
1.15 +    "a \<in> Part(A,h) \<longleftrightarrow> a \<in> A & (\<exists>y. a=h(y))"
1.16  apply (unfold Part_def)
1.17  apply (rule separation)
1.18  done
1.19
1.20 -lemma Part_eqI [intro]:
1.21 +lemma Part_eqI [intro]:
1.22      "[| a \<in> A;  a=h(b) |] ==> a \<in> Part(A,h)"
1.23  by (unfold Part_def, blast)
1.24
1.25  lemmas PartI = refl [THEN [2] Part_eqI]
1.26
1.27 -lemma PartE [elim!]:
1.28 -    "[| a \<in> Part(A,h);  !!z. [| a \<in> A;  a=h(z) |] ==> P
1.29 +lemma PartE [elim!]:
1.30 +    "[| a \<in> Part(A,h);  !!z. [| a \<in> A;  a=h(z) |] ==> P
1.31       |] ==> P"
1.32  apply (unfold Part_def, blast)
1.33  done
1.34 @@ -69,11 +69,11 @@
1.35  (** Elimination rules **)
1.36
1.37  lemma sumE [elim!]:
1.38 -    "[| u: A+B;
1.39 -        !!x. [| x:A;  u=Inl(x) |] ==> P;
1.40 -        !!y. [| y:B;  u=Inr(y) |] ==> P
1.41 +    "[| u \<in> A+B;
1.42 +        !!x. [| x \<in> A;  u=Inl(x) |] ==> P;
1.43 +        !!y. [| y \<in> B;  u=Inr(y) |] ==> P
1.44       |] ==> P"
1.45 -by (unfold sum_defs, blast)
1.46 +by (unfold sum_defs, blast)
1.47
1.48  (** Injection and freeness equivalences, for rewriting **)
1.49
1.50 @@ -100,13 +100,13 @@
1.51  lemmas Inr_neq_Inl = Inr_Inl_iff [THEN iffD1, THEN FalseE, elim!]
1.52
1.53
1.54 -lemma InlD: "Inl(a): A+B ==> a: A"
1.55 +lemma InlD: "Inl(a): A+B ==> a \<in> A"
1.56  by blast
1.57
1.58 -lemma InrD: "Inr(b): A+B ==> b: B"
1.59 +lemma InrD: "Inr(b): A+B ==> b \<in> B"
1.60  by blast
1.61
1.62 -lemma sum_iff: "u: A+B \<longleftrightarrow> (\<exists>x. x:A & u=Inl(x)) | (\<exists>y. y:B & u=Inr(y))"
1.63 +lemma sum_iff: "u \<in> A+B \<longleftrightarrow> (\<exists>x. x \<in> A & u=Inl(x)) | (\<exists>y. y \<in> B & u=Inr(y))"
1.64  by blast
1.65
1.66  lemma Inl_in_sum_iff [simp]: "(Inl(x) \<in> A+B) \<longleftrightarrow> (x \<in> A)";
1.67 @@ -134,27 +134,27 @@
1.69
1.70  lemma case_type [TC]:
1.71 -    "[| u: A+B;
1.72 -        !!x. x: A ==> c(x): C(Inl(x));
1.73 -        !!y. y: B ==> d(y): C(Inr(y))
1.74 +    "[| u \<in> A+B;
1.75 +        !!x. x \<in> A ==> c(x): C(Inl(x));
1.76 +        !!y. y \<in> B ==> d(y): C(Inr(y))
1.77       |] ==> case(c,d,u) \<in> C(u)"
1.78  by auto
1.79
1.80 -lemma expand_case: "u: A+B ==>
1.81 -        R(case(c,d,u)) \<longleftrightarrow>
1.82 -        ((\<forall>x\<in>A. u = Inl(x) \<longrightarrow> R(c(x))) &
1.83 +lemma expand_case: "u \<in> A+B ==>
1.84 +        R(case(c,d,u)) \<longleftrightarrow>
1.85 +        ((\<forall>x\<in>A. u = Inl(x) \<longrightarrow> R(c(x))) &
1.86          (\<forall>y\<in>B. u = Inr(y) \<longrightarrow> R(d(y))))"
1.87  by auto
1.88
1.89  lemma case_cong:
1.90 -  "[| z: A+B;
1.91 -      !!x. x:A ==> c(x)=c'(x);
1.92 -      !!y. y:B ==> d(y)=d'(y)
1.93 +  "[| z \<in> A+B;
1.94 +      !!x. x \<in> A ==> c(x)=c'(x);
1.95 +      !!y. y \<in> B ==> d(y)=d'(y)
1.96     |] ==> case(c,d,z) = case(c',d',z)"
1.97 -by auto
1.98 +by auto
1.99
1.100 -lemma case_case: "z: A+B ==>
1.101 -        case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) =
1.102 +lemma case_case: "z \<in> A+B ==>
1.103 +        case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) =
1.104          case(%x. c(c'(x)), %y. d(d'(y)), z)"
1.105  by auto
1.106
1.107 @@ -170,10 +170,10 @@
1.108  lemmas Part_CollectE =
1.109       Part_Collect [THEN equalityD1, THEN subsetD, THEN CollectE]
1.110
1.111 -lemma Part_Inl: "Part(A+B,Inl) = {Inl(x). x: A}"
1.112 +lemma Part_Inl: "Part(A+B,Inl) = {Inl(x). x \<in> A}"
1.113  by blast
1.114
1.115 -lemma Part_Inr: "Part(A+B,Inr) = {Inr(y). y: B}"
1.116 +lemma Part_Inr: "Part(A+B,Inr) = {Inr(y). y \<in> B}"
1.117  by blast
1.118
1.119  lemma PartD1: "a \<in> Part(A,h) ==> a \<in> A"
1.120 @@ -182,7 +182,7 @@
1.121  lemma Part_id: "Part(A,%x. x) = A"
1.122  by blast
1.123
1.124 -lemma Part_Inr2: "Part(A+B, %x. Inr(h(x))) = {Inr(y). y: Part(B,h)}"
1.125 +lemma Part_Inr2: "Part(A+B, %x. Inr(h(x))) = {Inr(y). y \<in> Part(B,h)}"
1.126  by blast
1.127
1.128  lemma Part_sum_equality: "C \<subseteq> A+B ==> Part(C,Inl) \<union> Part(C,Inr) = C"
```