src/ZF/Sum.thy
 changeset 46821 ff6b0c1087f2 parent 46820 c656222c4dc1 child 46953 2b6e55924af3
```     1.1 --- a/src/ZF/Sum.thy	Tue Mar 06 15:15:49 2012 +0000
1.2 +++ b/src/ZF/Sum.thy	Tue Mar 06 16:06:52 2012 +0000
1.3 @@ -28,7 +28,7 @@
1.4  subsection{*Rules for the @{term Part} Primitive*}
1.5
1.6  lemma Part_iff:
1.7 -    "a \<in> Part(A,h) <-> a:A & (\<exists>y. a=h(y))"
1.8 +    "a \<in> Part(A,h) \<longleftrightarrow> a:A & (\<exists>y. a=h(y))"
1.9  apply (unfold Part_def)
1.10  apply (rule separation)
1.11  done
1.12 @@ -77,16 +77,16 @@
1.13
1.14  (** Injection and freeness equivalences, for rewriting **)
1.15
1.16 -lemma Inl_iff [iff]: "Inl(a)=Inl(b) <-> a=b"
1.17 +lemma Inl_iff [iff]: "Inl(a)=Inl(b) \<longleftrightarrow> a=b"
1.19
1.20 -lemma Inr_iff [iff]: "Inr(a)=Inr(b) <-> a=b"
1.21 +lemma Inr_iff [iff]: "Inr(a)=Inr(b) \<longleftrightarrow> a=b"
1.23
1.24 -lemma Inl_Inr_iff [simp]: "Inl(a)=Inr(b) <-> False"
1.25 +lemma Inl_Inr_iff [simp]: "Inl(a)=Inr(b) \<longleftrightarrow> False"
1.27
1.28 -lemma Inr_Inl_iff [simp]: "Inr(b)=Inl(a) <-> False"
1.29 +lemma Inr_Inl_iff [simp]: "Inr(b)=Inl(a) \<longleftrightarrow> False"
1.31
1.32  lemma sum_empty [simp]: "0+0 = 0"
1.33 @@ -106,19 +106,19 @@
1.34  lemma InrD: "Inr(b): A+B ==> b: B"
1.35  by blast
1.36
1.37 -lemma sum_iff: "u: A+B <-> (\<exists>x. x:A & u=Inl(x)) | (\<exists>y. y:B & u=Inr(y))"
1.38 +lemma sum_iff: "u: A+B \<longleftrightarrow> (\<exists>x. x:A & u=Inl(x)) | (\<exists>y. y:B & u=Inr(y))"
1.39  by blast
1.40
1.41 -lemma Inl_in_sum_iff [simp]: "(Inl(x) \<in> A+B) <-> (x \<in> A)";
1.42 +lemma Inl_in_sum_iff [simp]: "(Inl(x) \<in> A+B) \<longleftrightarrow> (x \<in> A)";
1.43  by auto
1.44
1.45 -lemma Inr_in_sum_iff [simp]: "(Inr(y) \<in> A+B) <-> (y \<in> B)";
1.46 +lemma Inr_in_sum_iff [simp]: "(Inr(y) \<in> A+B) \<longleftrightarrow> (y \<in> B)";
1.47  by auto
1.48
1.49 -lemma sum_subset_iff: "A+B \<subseteq> C+D <-> A<=C & B<=D"
1.50 +lemma sum_subset_iff: "A+B \<subseteq> C+D \<longleftrightarrow> A<=C & B<=D"
1.51  by blast
1.52
1.53 -lemma sum_equal_iff: "A+B = C+D <-> A=C & B=D"
1.54 +lemma sum_equal_iff: "A+B = C+D \<longleftrightarrow> A=C & B=D"
1.55  by (simp add: extension sum_subset_iff, blast)
1.56
1.57  lemma sum_eq_2_times: "A+A = 2*A"
1.58 @@ -141,7 +141,7 @@
1.59  by auto
1.60
1.61  lemma expand_case: "u: A+B ==>
1.62 -        R(case(c,d,u)) <->
1.63 +        R(case(c,d,u)) \<longleftrightarrow>
1.64          ((\<forall>x\<in>A. u = Inl(x) \<longrightarrow> R(c(x))) &
1.65          (\<forall>y\<in>B. u = Inr(y) \<longrightarrow> R(d(y))))"
1.66  by auto
```