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.18  by (simp add: sum_defs)
    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.22  by (simp add: sum_defs)
    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.26  by (simp add: sum_defs)
    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.30  by (simp add: sum_defs)
    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