src/ZF/equalities.thy
changeset 46821 ff6b0c1087f2
parent 46820 c656222c4dc1
child 58860 fee7cfa69c50
     1.1 --- a/src/ZF/equalities.thy	Tue Mar 06 15:15:49 2012 +0000
     1.2 +++ b/src/ZF/equalities.thy	Tue Mar 06 16:06:52 2012 +0000
     1.3 @@ -22,21 +22,21 @@
     1.4    The following are not added to the default simpset because
     1.5    (a) they duplicate the body and (b) there are no similar rules for @{text Int}.*}
     1.6  
     1.7 -lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) <-> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))";
     1.8 +lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))";
     1.9    by blast
    1.10  
    1.11 -lemma bex_Un: "(\<exists>x \<in> A\<union>B. P(x)) <-> (\<exists>x \<in> A. P(x)) | (\<exists>x \<in> B. P(x))";
    1.12 +lemma bex_Un: "(\<exists>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<exists>x \<in> A. P(x)) | (\<exists>x \<in> B. P(x))";
    1.13    by blast
    1.14  
    1.15 -lemma ball_UN: "(\<forall>z \<in> (\<Union>x\<in>A. B(x)). P(z)) <-> (\<forall>x\<in>A. \<forall>z \<in> B(x). P(z))"
    1.16 +lemma ball_UN: "(\<forall>z \<in> (\<Union>x\<in>A. B(x)). P(z)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>z \<in> B(x). P(z))"
    1.17    by blast
    1.18  
    1.19 -lemma bex_UN: "(\<exists>z \<in> (\<Union>x\<in>A. B(x)). P(z)) <-> (\<exists>x\<in>A. \<exists>z\<in>B(x). P(z))"
    1.20 +lemma bex_UN: "(\<exists>z \<in> (\<Union>x\<in>A. B(x)). P(z)) \<longleftrightarrow> (\<exists>x\<in>A. \<exists>z\<in>B(x). P(z))"
    1.21    by blast
    1.22  
    1.23  subsection{*Converse of a Relation*}
    1.24  
    1.25 -lemma converse_iff [simp]: "<a,b>\<in> converse(r) <-> <b,a>\<in>r"
    1.26 +lemma converse_iff [simp]: "<a,b>\<in> converse(r) \<longleftrightarrow> <b,a>\<in>r"
    1.27  by (unfold converse_def, blast)
    1.28  
    1.29  lemma converseI [intro!]: "<a,b>\<in>r ==> <b,a>\<in>converse(r)"
    1.30 @@ -64,7 +64,7 @@
    1.31  by blast
    1.32  
    1.33  lemma converse_subset_iff:
    1.34 -     "A \<subseteq> Sigma(X,Y) ==> converse(A) \<subseteq> converse(B) <-> A \<subseteq> B"
    1.35 +     "A \<subseteq> Sigma(X,Y) ==> converse(A) \<subseteq> converse(B) \<longleftrightarrow> A \<subseteq> B"
    1.36  by blast
    1.37  
    1.38  
    1.39 @@ -76,17 +76,17 @@
    1.40  lemma subset_consI: "B \<subseteq> cons(a,B)"
    1.41  by blast
    1.42  
    1.43 -lemma cons_subset_iff [iff]: "cons(a,B)\<subseteq>C <-> a\<in>C & B\<subseteq>C"
    1.44 +lemma cons_subset_iff [iff]: "cons(a,B)\<subseteq>C \<longleftrightarrow> a\<in>C & B\<subseteq>C"
    1.45  by blast
    1.46  
    1.47  (*A safe special case of subset elimination, adding no new variables
    1.48    [| cons(a,B) \<subseteq> C; [| a \<in> C; B \<subseteq> C |] ==> R |] ==> R *)
    1.49  lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE]
    1.50  
    1.51 -lemma subset_empty_iff: "A\<subseteq>0 <-> A=0"
    1.52 +lemma subset_empty_iff: "A\<subseteq>0 \<longleftrightarrow> A=0"
    1.53  by blast
    1.54  
    1.55 -lemma subset_cons_iff: "C\<subseteq>cons(a,B) <-> C\<subseteq>B | (a\<in>C & C-{a} \<subseteq> B)"
    1.56 +lemma subset_cons_iff: "C\<subseteq>cons(a,B) \<longleftrightarrow> C\<subseteq>B | (a\<in>C & C-{a} \<subseteq> B)"
    1.57  by blast
    1.58  
    1.59  (* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)
    1.60 @@ -134,7 +134,7 @@
    1.61      "[| succ(i) \<subseteq> j;  [| i\<in>j;  i\<subseteq>j |] ==> P |] ==> P"
    1.62  by (unfold succ_def, blast)
    1.63  
    1.64 -lemma succ_subset_iff: "succ(a) \<subseteq> B <-> (a \<subseteq> B & a \<in> B)"
    1.65 +lemma succ_subset_iff: "succ(a) \<subseteq> B \<longleftrightarrow> (a \<subseteq> B & a \<in> B)"
    1.66  by (unfold succ_def, blast)
    1.67  
    1.68  
    1.69 @@ -142,7 +142,7 @@
    1.70  
    1.71  (** Intersection is the greatest lower bound of two sets **)
    1.72  
    1.73 -lemma Int_subset_iff: "C \<subseteq> A \<inter> B <-> C \<subseteq> A & C \<subseteq> B"
    1.74 +lemma Int_subset_iff: "C \<subseteq> A \<inter> B \<longleftrightarrow> C \<subseteq> A & C \<subseteq> B"
    1.75  by blast
    1.76  
    1.77  lemma Int_lower1: "A \<inter> B \<subseteq> A"
    1.78 @@ -187,10 +187,10 @@
    1.79  lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
    1.80  by blast
    1.81  
    1.82 -lemma subset_Int_iff: "A\<subseteq>B <-> A \<inter> B = A"
    1.83 +lemma subset_Int_iff: "A\<subseteq>B \<longleftrightarrow> A \<inter> B = A"
    1.84  by (blast elim!: equalityE)
    1.85  
    1.86 -lemma subset_Int_iff2: "A\<subseteq>B <-> B \<inter> A = A"
    1.87 +lemma subset_Int_iff2: "A\<subseteq>B \<longleftrightarrow> B \<inter> A = A"
    1.88  by (blast elim!: equalityE)
    1.89  
    1.90  lemma Int_Diff_eq: "C\<subseteq>A ==> (A-B) \<inter> C = C-B"
    1.91 @@ -211,7 +211,7 @@
    1.92  
    1.93  (** Union is the least upper bound of two sets *)
    1.94  
    1.95 -lemma Un_subset_iff: "A \<union> B \<subseteq> C <-> A \<subseteq> C & B \<subseteq> C"
    1.96 +lemma Un_subset_iff: "A \<union> B \<subseteq> C \<longleftrightarrow> A \<subseteq> C & B \<subseteq> C"
    1.97  by blast
    1.98  
    1.99  lemma Un_upper1: "A \<subseteq> A \<union> B"
   1.100 @@ -253,13 +253,13 @@
   1.101  lemma Un_Int_distrib: "(A \<inter> B) \<union> C  =  (A \<union> C) \<inter> (B \<union> C)"
   1.102  by blast
   1.103  
   1.104 -lemma subset_Un_iff: "A\<subseteq>B <-> A \<union> B = B"
   1.105 +lemma subset_Un_iff: "A\<subseteq>B \<longleftrightarrow> A \<union> B = B"
   1.106  by (blast elim!: equalityE)
   1.107  
   1.108 -lemma subset_Un_iff2: "A\<subseteq>B <-> B \<union> A = B"
   1.109 +lemma subset_Un_iff2: "A\<subseteq>B \<longleftrightarrow> B \<union> A = B"
   1.110  by (blast elim!: equalityE)
   1.111  
   1.112 -lemma Un_empty [iff]: "(A \<union> B = 0) <-> (A = 0 & B = 0)"
   1.113 +lemma Un_empty [iff]: "(A \<union> B = 0) \<longleftrightarrow> (A = 0 & B = 0)"
   1.114  by blast
   1.115  
   1.116  lemma Un_eq_Union: "A \<union> B = \<Union>({A, B})"
   1.117 @@ -273,7 +273,7 @@
   1.118  lemma Diff_contains: "[| C\<subseteq>A;  C \<inter> B = 0 |] ==> C \<subseteq> A-B"
   1.119  by blast
   1.120  
   1.121 -lemma subset_Diff_cons_iff: "B \<subseteq> A - cons(c,C)  <->  B\<subseteq>A-C & c \<notin> B"
   1.122 +lemma subset_Diff_cons_iff: "B \<subseteq> A - cons(c,C)  \<longleftrightarrow>  B\<subseteq>A-C & c \<notin> B"
   1.123  by blast
   1.124  
   1.125  lemma Diff_cancel: "A - A = 0"
   1.126 @@ -288,7 +288,7 @@
   1.127  lemma Diff_0 [simp]: "A - 0 = A"
   1.128  by blast
   1.129  
   1.130 -lemma Diff_eq_0_iff: "A - B = 0 <-> A \<subseteq> B"
   1.131 +lemma Diff_eq_0_iff: "A - B = 0 \<longleftrightarrow> A \<subseteq> B"
   1.132  by (blast elim: equalityE)
   1.133  
   1.134  (*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
   1.135 @@ -338,7 +338,7 @@
   1.136  by blast
   1.137  
   1.138  (*Halmos, Naive Set Theory, page 16.*)
   1.139 -lemma Un_Int_assoc_iff: "(A \<inter> B) \<union> C = A \<inter> (B \<union> C)  <->  C\<subseteq>A"
   1.140 +lemma Un_Int_assoc_iff: "(A \<inter> B) \<union> C = A \<inter> (B \<union> C)  \<longleftrightarrow>  C\<subseteq>A"
   1.141  by (blast elim!: equalityE)
   1.142  
   1.143  
   1.144 @@ -346,7 +346,7 @@
   1.145  
   1.146  (** Big Union is the least upper bound of a set  **)
   1.147  
   1.148 -lemma Union_subset_iff: "\<Union>(A) \<subseteq> C <-> (\<forall>x\<in>A. x \<subseteq> C)"
   1.149 +lemma Union_subset_iff: "\<Union>(A) \<subseteq> C \<longleftrightarrow> (\<forall>x\<in>A. x \<subseteq> C)"
   1.150  by blast
   1.151  
   1.152  lemma Union_upper: "B\<in>A ==> B \<subseteq> \<Union>(A)"
   1.153 @@ -364,10 +364,10 @@
   1.154  lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>(A) \<inter> \<Union>(B)"
   1.155  by blast
   1.156  
   1.157 -lemma Union_disjoint: "\<Union>(C) \<inter> A = 0 <-> (\<forall>B\<in>C. B \<inter> A = 0)"
   1.158 +lemma Union_disjoint: "\<Union>(C) \<inter> A = 0 \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = 0)"
   1.159  by (blast elim!: equalityE)
   1.160  
   1.161 -lemma Union_empty_iff: "\<Union>(A) = 0 <-> (\<forall>B\<in>A. B=0)"
   1.162 +lemma Union_empty_iff: "\<Union>(A) = 0 \<longleftrightarrow> (\<forall>B\<in>A. B=0)"
   1.163  by blast
   1.164  
   1.165  lemma Int_Union2: "\<Union>(B) \<inter> A = (\<Union>C\<in>B. C \<inter> A)"
   1.166 @@ -375,7 +375,7 @@
   1.167  
   1.168  (** Big Intersection is the greatest lower bound of a nonempty set **)
   1.169  
   1.170 -lemma Inter_subset_iff: "A\<noteq>0  ==>  C \<subseteq> \<Inter>(A) <-> (\<forall>x\<in>A. C \<subseteq> x)"
   1.171 +lemma Inter_subset_iff: "A\<noteq>0  ==>  C \<subseteq> \<Inter>(A) \<longleftrightarrow> (\<forall>x\<in>A. C \<subseteq> x)"
   1.172  by blast
   1.173  
   1.174  lemma Inter_lower: "B\<in>A ==> \<Inter>(A) \<subseteq> B"
   1.175 @@ -416,10 +416,10 @@
   1.176  
   1.177  subsection{*Unions and Intersections of Families*}
   1.178  
   1.179 -lemma subset_UN_iff_eq: "A \<subseteq> (\<Union>i\<in>I. B(i)) <-> A = (\<Union>i\<in>I. A \<inter> B(i))"
   1.180 +lemma subset_UN_iff_eq: "A \<subseteq> (\<Union>i\<in>I. B(i)) \<longleftrightarrow> A = (\<Union>i\<in>I. A \<inter> B(i))"
   1.181  by (blast elim!: equalityE)
   1.182  
   1.183 -lemma UN_subset_iff: "(\<Union>x\<in>A. B(x)) \<subseteq> C <-> (\<forall>x\<in>A. B(x) \<subseteq> C)"
   1.184 +lemma UN_subset_iff: "(\<Union>x\<in>A. B(x)) \<subseteq> C \<longleftrightarrow> (\<forall>x\<in>A. B(x) \<subseteq> C)"
   1.185  by blast
   1.186  
   1.187  lemma UN_upper: "x\<in>A ==> B(x) \<subseteq> (\<Union>x\<in>A. B(x))"
   1.188 @@ -571,7 +571,7 @@
   1.189  by blast
   1.190  
   1.191  lemma times_subset_iff:
   1.192 -     "(A'*B' \<subseteq> A*B) <-> (A' = 0 | B' = 0 | (A'\<subseteq>A) & (B'\<subseteq>B))"
   1.193 +     "(A'*B' \<subseteq> A*B) \<longleftrightarrow> (A' = 0 | B' = 0 | (A'\<subseteq>A) & (B'\<subseteq>B))"
   1.194  by blast
   1.195  
   1.196  lemma Int_Sigma_eq:
   1.197 @@ -580,7 +580,7 @@
   1.198  
   1.199  (** Domain **)
   1.200  
   1.201 -lemma domain_iff: "a: domain(r) <-> (\<exists>y. <a,y>\<in> r)"
   1.202 +lemma domain_iff: "a: domain(r) \<longleftrightarrow> (\<exists>y. <a,y>\<in> r)"
   1.203  by (unfold domain_def, blast)
   1.204  
   1.205  lemma domainI [intro]: "<a,b>\<in> r ==> a: domain(r)"
   1.206 @@ -739,10 +739,10 @@
   1.207  
   1.208  subsection{*Image of a Set under a Function or Relation*}
   1.209  
   1.210 -lemma image_iff: "b \<in> r``A <-> (\<exists>x\<in>A. <x,b>\<in>r)"
   1.211 +lemma image_iff: "b \<in> r``A \<longleftrightarrow> (\<exists>x\<in>A. <x,b>\<in>r)"
   1.212  by (unfold image_def, blast)
   1.213  
   1.214 -lemma image_singleton_iff: "b \<in> r``{a} <-> <a,b>\<in>r"
   1.215 +lemma image_singleton_iff: "b \<in> r``{a} \<longleftrightarrow> <a,b>\<in>r"
   1.216  by (rule image_iff [THEN iff_trans], blast)
   1.217  
   1.218  lemma imageI [intro]: "[| <a,b>\<in> r;  a\<in>A |] ==> b \<in> r``A"
   1.219 @@ -792,10 +792,10 @@
   1.220  subsection{*Inverse Image of a Set under a Function or Relation*}
   1.221  
   1.222  lemma vimage_iff:
   1.223 -    "a \<in> r-``B <-> (\<exists>y\<in>B. <a,y>\<in>r)"
   1.224 +    "a \<in> r-``B \<longleftrightarrow> (\<exists>y\<in>B. <a,y>\<in>r)"
   1.225  by (unfold vimage_def image_def converse_def, blast)
   1.226  
   1.227 -lemma vimage_singleton_iff: "a \<in> r-``{b} <-> <a,b>\<in>r"
   1.228 +lemma vimage_singleton_iff: "a \<in> r-``{b} \<longleftrightarrow> <a,b>\<in>r"
   1.229  by (rule vimage_iff [THEN iff_trans], blast)
   1.230  
   1.231  lemma vimageI [intro]: "[| <a,b>\<in> r;  b\<in>B |] ==> a \<in> r-``B"
   1.232 @@ -897,7 +897,7 @@
   1.233  lemma Union_Pow_eq [simp]: "\<Union>(Pow(A)) = A"
   1.234  by blast
   1.235  
   1.236 -lemma Union_Pow_iff: "\<Union>(A) \<in> Pow(B) <-> A \<in> Pow(Pow(B))"
   1.237 +lemma Union_Pow_iff: "\<Union>(A) \<in> Pow(B) \<longleftrightarrow> A \<in> Pow(Pow(B))"
   1.238  by blast
   1.239  
   1.240  lemma Pow_Int_eq [simp]: "Pow(A \<inter> B) = Pow(A) \<inter> Pow(B)"
   1.241 @@ -912,7 +912,7 @@
   1.242  lemma RepFun_subset: "[| !!x. x\<in>A ==> f(x) \<in> B |] ==> {f(x). x\<in>A} \<subseteq> B"
   1.243  by blast
   1.244  
   1.245 -lemma RepFun_eq_0_iff [simp]: "{f(x).x\<in>A}=0 <-> A=0"
   1.246 +lemma RepFun_eq_0_iff [simp]: "{f(x).x\<in>A}=0 \<longleftrightarrow> A=0"
   1.247  by blast
   1.248  
   1.249  lemma RepFun_constant [simp]: "{c. x\<in>A} = (if A=0 then 0 else {c})"