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"