src/ZF/Sum.thy
changeset 46820 c656222c4dc1
parent 45602 2a858377c3d2
child 46821 ff6b0c1087f2
     1.1 --- a/src/ZF/Sum.thy	Sun Mar 04 23:20:43 2012 +0100
     1.2 +++ b/src/ZF/Sum.thy	Tue Mar 06 15:15:49 2012 +0000
     1.3 @@ -10,7 +10,7 @@
     1.4  text{*And the "Part" primitive for simultaneous recursive type definitions*}
     1.5  
     1.6  definition sum :: "[i,i]=>i" (infixr "+" 65) where
     1.7 -     "A+B == {0}*A Un {1}*B"
     1.8 +     "A+B == {0}*A \<union> {1}*B"
     1.9  
    1.10  definition Inl :: "i=>i" where
    1.11       "Inl(a) == <0,a>"
    1.12 @@ -23,29 +23,29 @@
    1.13  
    1.14    (*operator for selecting out the various summands*)
    1.15  definition Part :: "[i,i=>i] => i" where
    1.16 -     "Part(A,h) == {x: A. EX z. x = h(z)}"
    1.17 +     "Part(A,h) == {x: A. \<exists>z. x = h(z)}"
    1.18  
    1.19  subsection{*Rules for the @{term Part} Primitive*}
    1.20  
    1.21  lemma Part_iff: 
    1.22 -    "a : Part(A,h) <-> a:A & (EX y. a=h(y))"
    1.23 +    "a \<in> Part(A,h) <-> a:A & (\<exists>y. a=h(y))"
    1.24  apply (unfold Part_def)
    1.25  apply (rule separation)
    1.26  done
    1.27  
    1.28  lemma Part_eqI [intro]: 
    1.29 -    "[| a : A;  a=h(b) |] ==> a : Part(A,h)"
    1.30 +    "[| a \<in> A;  a=h(b) |] ==> a \<in> Part(A,h)"
    1.31  by (unfold Part_def, blast)
    1.32  
    1.33  lemmas PartI = refl [THEN [2] Part_eqI]
    1.34  
    1.35  lemma PartE [elim!]: 
    1.36 -    "[| a : Part(A,h);  !!z. [| a : A;  a=h(z) |] ==> P   
    1.37 +    "[| a \<in> Part(A,h);  !!z. [| a \<in> A;  a=h(z) |] ==> P   
    1.38       |] ==> P"
    1.39  apply (unfold Part_def, blast)
    1.40  done
    1.41  
    1.42 -lemma Part_subset: "Part(A,h) <= A"
    1.43 +lemma Part_subset: "Part(A,h) \<subseteq> A"
    1.44  apply (unfold Part_def)
    1.45  apply (rule Collect_subset)
    1.46  done
    1.47 @@ -60,10 +60,10 @@
    1.48  
    1.49  (** Introduction rules for the injections **)
    1.50  
    1.51 -lemma InlI [intro!,simp,TC]: "a : A ==> Inl(a) : A+B"
    1.52 +lemma InlI [intro!,simp,TC]: "a \<in> A ==> Inl(a) \<in> A+B"
    1.53  by (unfold sum_defs, blast)
    1.54  
    1.55 -lemma InrI [intro!,simp,TC]: "b : B ==> Inr(b) : A+B"
    1.56 +lemma InrI [intro!,simp,TC]: "b \<in> B ==> Inr(b) \<in> A+B"
    1.57  by (unfold sum_defs, blast)
    1.58  
    1.59  (** Elimination rules **)
    1.60 @@ -106,7 +106,7 @@
    1.61  lemma InrD: "Inr(b): A+B ==> b: B"
    1.62  by blast
    1.63  
    1.64 -lemma sum_iff: "u: A+B <-> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))"
    1.65 +lemma sum_iff: "u: A+B <-> (\<exists>x. x:A & u=Inl(x)) | (\<exists>y. y:B & u=Inr(y))"
    1.66  by blast
    1.67  
    1.68  lemma Inl_in_sum_iff [simp]: "(Inl(x) \<in> A+B) <-> (x \<in> A)";
    1.69 @@ -115,7 +115,7 @@
    1.70  lemma Inr_in_sum_iff [simp]: "(Inr(y) \<in> A+B) <-> (y \<in> B)";
    1.71  by auto
    1.72  
    1.73 -lemma sum_subset_iff: "A+B <= C+D <-> A<=C & B<=D"
    1.74 +lemma sum_subset_iff: "A+B \<subseteq> C+D <-> A<=C & B<=D"
    1.75  by blast
    1.76  
    1.77  lemma sum_equal_iff: "A+B = C+D <-> A=C & B=D"
    1.78 @@ -137,13 +137,13 @@
    1.79      "[| u: A+B;  
    1.80          !!x. x: A ==> c(x): C(Inl(x));    
    1.81          !!y. y: B ==> d(y): C(Inr(y))  
    1.82 -     |] ==> case(c,d,u) : C(u)"
    1.83 +     |] ==> case(c,d,u) \<in> C(u)"
    1.84  by auto
    1.85  
    1.86  lemma expand_case: "u: A+B ==>    
    1.87          R(case(c,d,u)) <->  
    1.88 -        ((ALL x:A. u = Inl(x) --> R(c(x))) &  
    1.89 -        (ALL y:B. u = Inr(y) --> R(d(y))))"
    1.90 +        ((\<forall>x\<in>A. u = Inl(x) \<longrightarrow> R(c(x))) &  
    1.91 +        (\<forall>y\<in>B. u = Inr(y) \<longrightarrow> R(d(y))))"
    1.92  by auto
    1.93  
    1.94  lemma case_cong:
    1.95 @@ -176,7 +176,7 @@
    1.96  lemma Part_Inr: "Part(A+B,Inr) = {Inr(y). y: B}"
    1.97  by blast
    1.98  
    1.99 -lemma PartD1: "a : Part(A,h) ==> a : A"
   1.100 +lemma PartD1: "a \<in> Part(A,h) ==> a \<in> A"
   1.101  by (simp add: Part_def)
   1.102  
   1.103  lemma Part_id: "Part(A,%x. x) = A"
   1.104 @@ -185,7 +185,7 @@
   1.105  lemma Part_Inr2: "Part(A+B, %x. Inr(h(x))) = {Inr(y). y: Part(B,h)}"
   1.106  by blast
   1.107  
   1.108 -lemma Part_sum_equality: "C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C"
   1.109 +lemma Part_sum_equality: "C \<subseteq> A+B ==> Part(C,Inl) \<union> Part(C,Inr) = C"
   1.110  by blast
   1.111  
   1.112  end