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.68  by (simp add: sum_defs)
    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"