Using mathematical notation for <-> and cardinal arithmetic
authorpaulson
Tue Mar 06 16:06:52 2012 +0000 (2012-03-06 ago)
changeset 46821ff6b0c1087f2
parent 46820 c656222c4dc1
child 46822 95f1e700b712
Using mathematical notation for <-> and cardinal arithmetic
src/ZF/Arith.thy
src/ZF/ArithSimp.thy
src/ZF/Bin.thy
src/ZF/Bool.thy
src/ZF/Cardinal.thy
src/ZF/CardinalArith.thy
src/ZF/Cardinal_AC.thy
src/ZF/EquivClass.thy
src/ZF/Finite.thy
src/ZF/Inductive_ZF.thy
src/ZF/IntArith.thy
src/ZF/IntDiv_ZF.thy
src/ZF/Int_ZF.thy
src/ZF/List_ZF.thy
src/ZF/Nat_ZF.thy
src/ZF/Order.thy
src/ZF/OrderArith.thy
src/ZF/OrderType.thy
src/ZF/Perm.thy
src/ZF/QPair.thy
src/ZF/QUniv.thy
src/ZF/Sum.thy
src/ZF/Univ.thy
src/ZF/WF.thy
src/ZF/equalities.thy
src/ZF/ex/Ring.thy
src/ZF/func.thy
src/ZF/pair.thy
src/ZF/upair.thy
     1.1 --- a/src/ZF/Arith.thy	Tue Mar 06 15:15:49 2012 +0000
     1.2 +++ b/src/ZF/Arith.thy	Tue Mar 06 16:06:52 2012 +0000
     1.3 @@ -311,7 +311,7 @@
     1.4  lemma add_lt_elim1: "[| k#+m < k#+n; m \<in> nat; n \<in> nat |] ==> m < n"
     1.5  by (drule add_lt_elim1_natify, auto)
     1.6  
     1.7 -lemma zero_less_add: "[| n \<in> nat; m \<in> nat |] ==> 0 < m #+ n <-> (0<m | 0<n)"
     1.8 +lemma zero_less_add: "[| n \<in> nat; m \<in> nat |] ==> 0 < m #+ n \<longleftrightarrow> (0<m | 0<n)"
     1.9  by (induct_tac "n", auto)
    1.10  
    1.11  
    1.12 @@ -441,13 +441,13 @@
    1.13  
    1.14  (** Lemmas for the CancelNumerals simproc **)
    1.15  
    1.16 -lemma eq_add_iff: "(u #+ m = u #+ n) <-> (0 #+ m = natify(n))"
    1.17 +lemma eq_add_iff: "(u #+ m = u #+ n) \<longleftrightarrow> (0 #+ m = natify(n))"
    1.18  apply auto
    1.19  apply (blast dest: add_left_cancel_natify)
    1.20  apply (simp add: add_def)
    1.21  done
    1.22  
    1.23 -lemma less_add_iff: "(u #+ m < u #+ n) <-> (0 #+ m < natify(n))"
    1.24 +lemma less_add_iff: "(u #+ m < u #+ n) \<longleftrightarrow> (0 #+ m < natify(n))"
    1.25  apply (auto simp add: add_lt_elim1_natify)
    1.26  apply (drule add_lt_mono1)
    1.27  apply (auto simp add: add_commute [of u])
    1.28 @@ -460,7 +460,7 @@
    1.29  lemma eq_cong2: "u = u' ==> (t==u) == (t==u')"
    1.30  by auto
    1.31  
    1.32 -lemma iff_cong2: "u <-> u' ==> (t==u) == (t==u')"
    1.33 +lemma iff_cong2: "u \<longleftrightarrow> u' ==> (t==u) == (t==u')"
    1.34  by auto
    1.35  
    1.36  
    1.37 @@ -543,11 +543,11 @@
    1.38  
    1.39  lemma lt_succ_eq_0_disj:
    1.40       "[| m\<in>nat; n\<in>nat |]
    1.41 -      ==> (m < succ(n)) <-> (m = 0 | (\<exists>j\<in>nat. m = succ(j) & j < n))"
    1.42 +      ==> (m < succ(n)) \<longleftrightarrow> (m = 0 | (\<exists>j\<in>nat. m = succ(j) & j < n))"
    1.43  by (induct_tac "m", auto)
    1.44  
    1.45  lemma less_diff_conv [rule_format]:
    1.46 -     "[| j\<in>nat; k\<in>nat |] ==> \<forall>i\<in>nat. (i < j #- k) <-> (i #+ k < j)"
    1.47 +     "[| j\<in>nat; k\<in>nat |] ==> \<forall>i\<in>nat. (i < j #- k) \<longleftrightarrow> (i #+ k < j)"
    1.48  by (erule_tac m = k in diff_induct, auto)
    1.49  
    1.50  lemmas nat_typechecks = rec_type nat_0I nat_1I nat_succI Ord_nat
     2.1 --- a/src/ZF/ArithSimp.thy	Tue Mar 06 15:15:49 2012 +0000
     2.2 +++ b/src/ZF/ArithSimp.thy	Tue Mar 06 16:06:52 2012 +0000
     2.3 @@ -43,7 +43,7 @@
     2.4  done
     2.5  
     2.6  lemma zero_less_diff [simp]:
     2.7 -     "[| m: nat; n: nat |] ==> 0 < (n #- m)   <->   m<n"
     2.8 +     "[| m: nat; n: nat |] ==> 0 < (n #- m)   \<longleftrightarrow>   m<n"
     2.9  apply (rule_tac m = m and n = n in diff_induct)
    2.10  apply (simp_all (no_asm_simp))
    2.11  done
    2.12 @@ -301,37 +301,37 @@
    2.13  apply (simp (no_asm_simp) add: mult_lt_mono2 mult_commute [of _ k])
    2.14  done
    2.15  
    2.16 -lemma add_eq_0_iff [iff]: "m#+n = 0 <-> natify(m)=0 & natify(n)=0"
    2.17 -apply (subgoal_tac "natify (m) #+ natify (n) = 0 <-> natify (m) =0 & natify (n) =0")
    2.18 +lemma add_eq_0_iff [iff]: "m#+n = 0 \<longleftrightarrow> natify(m)=0 & natify(n)=0"
    2.19 +apply (subgoal_tac "natify (m) #+ natify (n) = 0 \<longleftrightarrow> natify (m) =0 & natify (n) =0")
    2.20  apply (rule_tac [2] n = "natify (m) " in natE)
    2.21   apply (rule_tac [4] n = "natify (n) " in natE)
    2.22  apply auto
    2.23  done
    2.24  
    2.25 -lemma zero_lt_mult_iff [iff]: "0 < m#*n <-> 0 < natify(m) & 0 < natify(n)"
    2.26 -apply (subgoal_tac "0 < natify (m) #*natify (n) <-> 0 < natify (m) & 0 < natify (n) ")
    2.27 +lemma zero_lt_mult_iff [iff]: "0 < m#*n \<longleftrightarrow> 0 < natify(m) & 0 < natify(n)"
    2.28 +apply (subgoal_tac "0 < natify (m) #*natify (n) \<longleftrightarrow> 0 < natify (m) & 0 < natify (n) ")
    2.29  apply (rule_tac [2] n = "natify (m) " in natE)
    2.30   apply (rule_tac [4] n = "natify (n) " in natE)
    2.31    apply (rule_tac [3] n = "natify (n) " in natE)
    2.32  apply auto
    2.33  done
    2.34  
    2.35 -lemma mult_eq_1_iff [iff]: "m#*n = 1 <-> natify(m)=1 & natify(n)=1"
    2.36 -apply (subgoal_tac "natify (m) #* natify (n) = 1 <-> natify (m) =1 & natify (n) =1")
    2.37 +lemma mult_eq_1_iff [iff]: "m#*n = 1 \<longleftrightarrow> natify(m)=1 & natify(n)=1"
    2.38 +apply (subgoal_tac "natify (m) #* natify (n) = 1 \<longleftrightarrow> natify (m) =1 & natify (n) =1")
    2.39  apply (rule_tac [2] n = "natify (m) " in natE)
    2.40   apply (rule_tac [4] n = "natify (n) " in natE)
    2.41  apply auto
    2.42  done
    2.43  
    2.44  
    2.45 -lemma mult_is_zero: "[|m: nat; n: nat|] ==> (m #* n = 0) <-> (m = 0 | n = 0)"
    2.46 +lemma mult_is_zero: "[|m: nat; n: nat|] ==> (m #* n = 0) \<longleftrightarrow> (m = 0 | n = 0)"
    2.47  apply auto
    2.48  apply (erule natE)
    2.49  apply (erule_tac [2] natE, auto)
    2.50  done
    2.51  
    2.52  lemma mult_is_zero_natify [iff]:
    2.53 -     "(m #* n = 0) <-> (natify(m) = 0 | natify(n) = 0)"
    2.54 +     "(m #* n = 0) \<longleftrightarrow> (natify(m) = 0 | natify(n) = 0)"
    2.55  apply (cut_tac m = "natify (m) " and n = "natify (n) " in mult_is_zero)
    2.56  apply auto
    2.57  done
    2.58 @@ -340,7 +340,7 @@
    2.59  subsection{*Cancellation Laws for Common Factors in Comparisons*}
    2.60  
    2.61  lemma mult_less_cancel_lemma:
    2.62 -     "[| k: nat; m: nat; n: nat |] ==> (m#*k < n#*k) <-> (0<k & m<n)"
    2.63 +     "[| k: nat; m: nat; n: nat |] ==> (m#*k < n#*k) \<longleftrightarrow> (0<k & m<n)"
    2.64  apply (safe intro!: mult_lt_mono1)
    2.65  apply (erule natE, auto)
    2.66  apply (rule not_le_iff_lt [THEN iffD1])
    2.67 @@ -349,22 +349,22 @@
    2.68  done
    2.69  
    2.70  lemma mult_less_cancel2 [simp]:
    2.71 -     "(m#*k < n#*k) <-> (0 < natify(k) & natify(m) < natify(n))"
    2.72 +     "(m#*k < n#*k) \<longleftrightarrow> (0 < natify(k) & natify(m) < natify(n))"
    2.73  apply (rule iff_trans)
    2.74  apply (rule_tac [2] mult_less_cancel_lemma, auto)
    2.75  done
    2.76  
    2.77  lemma mult_less_cancel1 [simp]:
    2.78 -     "(k#*m < k#*n) <-> (0 < natify(k) & natify(m) < natify(n))"
    2.79 +     "(k#*m < k#*n) \<longleftrightarrow> (0 < natify(k) & natify(m) < natify(n))"
    2.80  apply (simp (no_asm) add: mult_less_cancel2 mult_commute [of k])
    2.81  done
    2.82  
    2.83 -lemma mult_le_cancel2 [simp]: "(m#*k \<le> n#*k) <-> (0 < natify(k) \<longrightarrow> natify(m) \<le> natify(n))"
    2.84 +lemma mult_le_cancel2 [simp]: "(m#*k \<le> n#*k) \<longleftrightarrow> (0 < natify(k) \<longrightarrow> natify(m) \<le> natify(n))"
    2.85  apply (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym])
    2.86  apply auto
    2.87  done
    2.88  
    2.89 -lemma mult_le_cancel1 [simp]: "(k#*m \<le> k#*n) <-> (0 < natify(k) \<longrightarrow> natify(m) \<le> natify(n))"
    2.90 +lemma mult_le_cancel1 [simp]: "(k#*m \<le> k#*n) \<longleftrightarrow> (0 < natify(k) \<longrightarrow> natify(m) \<le> natify(n))"
    2.91  apply (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym])
    2.92  apply auto
    2.93  done
    2.94 @@ -372,23 +372,23 @@
    2.95  lemma mult_le_cancel_le1: "k \<in> nat ==> k #* m \<le> k \<longleftrightarrow> (0 < k \<longrightarrow> natify(m) \<le> 1)"
    2.96  by (cut_tac k = k and m = m and n = 1 in mult_le_cancel1, auto)
    2.97  
    2.98 -lemma Ord_eq_iff_le: "[| Ord(m); Ord(n) |] ==> m=n <-> (m \<le> n & n \<le> m)"
    2.99 +lemma Ord_eq_iff_le: "[| Ord(m); Ord(n) |] ==> m=n \<longleftrightarrow> (m \<le> n & n \<le> m)"
   2.100  by (blast intro: le_anti_sym)
   2.101  
   2.102  lemma mult_cancel2_lemma:
   2.103 -     "[| k: nat; m: nat; n: nat |] ==> (m#*k = n#*k) <-> (m=n | k=0)"
   2.104 +     "[| k: nat; m: nat; n: nat |] ==> (m#*k = n#*k) \<longleftrightarrow> (m=n | k=0)"
   2.105  apply (simp (no_asm_simp) add: Ord_eq_iff_le [of "m#*k"] Ord_eq_iff_le [of m])
   2.106  apply (auto simp add: Ord_0_lt_iff)
   2.107  done
   2.108  
   2.109  lemma mult_cancel2 [simp]:
   2.110 -     "(m#*k = n#*k) <-> (natify(m) = natify(n) | natify(k) = 0)"
   2.111 +     "(m#*k = n#*k) \<longleftrightarrow> (natify(m) = natify(n) | natify(k) = 0)"
   2.112  apply (rule iff_trans)
   2.113  apply (rule_tac [2] mult_cancel2_lemma, auto)
   2.114  done
   2.115  
   2.116  lemma mult_cancel1 [simp]:
   2.117 -     "(k#*m = k#*n) <-> (natify(m) = natify(n) | natify(k) = 0)"
   2.118 +     "(k#*m = k#*n) \<longleftrightarrow> (natify(m) = natify(n) | natify(k) = 0)"
   2.119  apply (simp (no_asm) add: mult_cancel2 mult_commute [of k])
   2.120  done
   2.121  
   2.122 @@ -493,7 +493,7 @@
   2.123  done
   2.124  
   2.125  lemma less_iff_succ_add:
   2.126 -     "[| m: nat; n: nat |] ==> (m<n) <-> (\<exists>k\<in>nat. n = succ(m#+k))"
   2.127 +     "[| m: nat; n: nat |] ==> (m<n) \<longleftrightarrow> (\<exists>k\<in>nat. n = succ(m#+k))"
   2.128  by (auto intro: less_imp_succ_add)
   2.129  
   2.130  lemma add_lt_elim2:
   2.131 @@ -508,11 +508,11 @@
   2.132  subsubsection{*More Lemmas About Difference*}
   2.133  
   2.134  lemma diff_is_0_lemma:
   2.135 -     "[| m: nat; n: nat |] ==> m #- n = 0 <-> m \<le> n"
   2.136 +     "[| m: nat; n: nat |] ==> m #- n = 0 \<longleftrightarrow> m \<le> n"
   2.137  apply (rule_tac m = m and n = n in diff_induct, simp_all)
   2.138  done
   2.139  
   2.140 -lemma diff_is_0_iff: "m #- n = 0 <-> natify(m) \<le> natify(n)"
   2.141 +lemma diff_is_0_iff: "m #- n = 0 \<longleftrightarrow> natify(m) \<le> natify(n)"
   2.142  by (simp add: diff_is_0_lemma [symmetric])
   2.143  
   2.144  lemma nat_lt_imp_diff_eq_0:
   2.145 @@ -521,7 +521,7 @@
   2.146  
   2.147  lemma raw_nat_diff_split:
   2.148       "[| a:nat; b:nat |] ==>
   2.149 -      (P(a #- b)) <-> ((a < b \<longrightarrow>P(0)) & (\<forall>d\<in>nat. a = b #+ d \<longrightarrow> P(d)))"
   2.150 +      (P(a #- b)) \<longleftrightarrow> ((a < b \<longrightarrow>P(0)) & (\<forall>d\<in>nat. a = b #+ d \<longrightarrow> P(d)))"
   2.151  apply (case_tac "a < b")
   2.152   apply (force simp add: nat_lt_imp_diff_eq_0)
   2.153  apply (rule iffI, force, simp)
   2.154 @@ -530,7 +530,7 @@
   2.155  done
   2.156  
   2.157  lemma nat_diff_split:
   2.158 -   "(P(a #- b)) <->
   2.159 +   "(P(a #- b)) \<longleftrightarrow>
   2.160      (natify(a) < natify(b) \<longrightarrow>P(0)) & (\<forall>d\<in>nat. natify(a) = b #+ d \<longrightarrow> P(d))"
   2.161  apply (cut_tac P=P and a="natify(a)" and b="natify(b)" in raw_nat_diff_split)
   2.162  apply simp_all
   2.163 @@ -559,7 +559,7 @@
   2.164  done
   2.165  
   2.166  
   2.167 -lemma diff_lt_iff_lt: "[|i\<le>k; j\<in>nat; k\<in>nat|] ==> (k#-i) < (k#-j) <-> j<i"
   2.168 +lemma diff_lt_iff_lt: "[|i\<le>k; j\<in>nat; k\<in>nat|] ==> (k#-i) < (k#-j) \<longleftrightarrow> j<i"
   2.169  apply (frule le_in_nat, assumption)
   2.170  apply (blast intro: lt_imp_diff_lt diff_lt_imp_lt)
   2.171  done
     3.1 --- a/src/ZF/Bin.thy	Tue Mar 06 15:15:49 2012 +0000
     3.2 +++ b/src/ZF/Bin.thy	Tue Mar 06 16:06:52 2012 +0000
     3.3 @@ -346,7 +346,7 @@
     3.4  
     3.5  lemma eq_integ_of_eq:
     3.6       "[| v: bin;  w: bin |]
     3.7 -      ==> ((integ_of(v)) = integ_of(w)) <->
     3.8 +      ==> ((integ_of(v)) = integ_of(w)) \<longleftrightarrow>
     3.9            iszero (integ_of (bin_add (v, bin_minus(w))))"
    3.10  apply (unfold iszero_def)
    3.11  apply (simp add: zcompare_rls integ_of_add integ_of_minus)
    3.12 @@ -363,7 +363,7 @@
    3.13  
    3.14  lemma iszero_integ_of_BIT:
    3.15       "[| w: bin; x: bool |]
    3.16 -      ==> iszero (integ_of (w BIT x)) <-> (x=0 & iszero (integ_of(w)))"
    3.17 +      ==> iszero (integ_of (w BIT x)) \<longleftrightarrow> (x=0 & iszero (integ_of(w)))"
    3.18  apply (unfold iszero_def, simp)
    3.19  apply (subgoal_tac "integ_of (w) \<in> int")
    3.20  apply typecheck
    3.21 @@ -374,7 +374,7 @@
    3.22  done
    3.23  
    3.24  lemma iszero_integ_of_0:
    3.25 -     "w: bin ==> iszero (integ_of (w BIT 0)) <-> iszero (integ_of(w))"
    3.26 +     "w: bin ==> iszero (integ_of (w BIT 0)) \<longleftrightarrow> iszero (integ_of(w))"
    3.27  by (simp only: iszero_integ_of_BIT, blast)
    3.28  
    3.29  lemma iszero_integ_of_1: "w: bin ==> ~ iszero (integ_of (w BIT 1))"
    3.30 @@ -387,7 +387,7 @@
    3.31  lemma less_integ_of_eq_neg:
    3.32       "[| v: bin;  w: bin |]
    3.33        ==> integ_of(v) $< integ_of(w)
    3.34 -          <-> znegative (integ_of (bin_add (v, bin_minus(w))))"
    3.35 +          \<longleftrightarrow> znegative (integ_of (bin_add (v, bin_minus(w))))"
    3.36  apply (unfold zless_def zdiff_def)
    3.37  apply (simp add: integ_of_minus integ_of_add)
    3.38  done
    3.39 @@ -400,7 +400,7 @@
    3.40  
    3.41  lemma neg_integ_of_BIT:
    3.42       "[| w: bin; x: bool |]
    3.43 -      ==> znegative (integ_of (w BIT x)) <-> znegative (integ_of(w))"
    3.44 +      ==> znegative (integ_of (w BIT x)) \<longleftrightarrow> znegative (integ_of(w))"
    3.45  apply simp
    3.46  apply (subgoal_tac "integ_of (w) \<in> int")
    3.47  apply typecheck
    3.48 @@ -416,7 +416,7 @@
    3.49  (** Less-than-or-equals (<=) **)
    3.50  
    3.51  lemma le_integ_of_eq_not_less:
    3.52 -     "(integ_of(x) $<= (integ_of(w))) <-> ~ (integ_of(w) $< (integ_of(x)))"
    3.53 +     "(integ_of(x) $<= (integ_of(w))) \<longleftrightarrow> ~ (integ_of(w) $< (integ_of(x)))"
    3.54  by (simp add: not_zless_iff_zle [THEN iff_sym])
    3.55  
    3.56  
    3.57 @@ -509,7 +509,7 @@
    3.58  lemma zdiff_self [simp]: "x $- x = #0"
    3.59  by (simp add: zdiff_def)
    3.60  
    3.61 -lemma znegative_iff_zless_0: "k: int ==> znegative(k) <-> k $< #0"
    3.62 +lemma znegative_iff_zless_0: "k: int ==> znegative(k) \<longleftrightarrow> k $< #0"
    3.63  by (simp add: zless_def)
    3.64  
    3.65  lemma zero_zless_imp_znegative_zminus: "[|#0 $< k; k: int|] ==> znegative($-k)"
    3.66 @@ -545,7 +545,7 @@
    3.67  lemma int_of_nat_of_if: "$# nat_of(z) = (if #0 $<= z then intify(z) else #0)"
    3.68  by (simp add: int_of_nat_of znegative_iff_zless_0 not_zle_iff_zless)
    3.69  
    3.70 -lemma zless_nat_iff_int_zless: "[| m: nat; z: int |] ==> (m < nat_of(z)) <-> ($#m $< z)"
    3.71 +lemma zless_nat_iff_int_zless: "[| m: nat; z: int |] ==> (m < nat_of(z)) \<longleftrightarrow> ($#m $< z)"
    3.72  apply (case_tac "znegative (z) ")
    3.73  apply (erule_tac [2] not_zneg_nat_of [THEN subst])
    3.74  apply (auto dest: zless_trans dest!: zero_zle_int_of [THEN zle_zless_trans]
    3.75 @@ -556,7 +556,7 @@
    3.76  (** nat_of and zless **)
    3.77  
    3.78  (*An alternative condition is  @{term"$#0 \<subseteq> w"}  *)
    3.79 -lemma zless_nat_conj_lemma: "$#0 $< z ==> (nat_of(w) < nat_of(z)) <-> (w $< z)"
    3.80 +lemma zless_nat_conj_lemma: "$#0 $< z ==> (nat_of(w) < nat_of(z)) \<longleftrightarrow> (w $< z)"
    3.81  apply (rule iff_trans)
    3.82  apply (rule zless_int_of [THEN iff_sym])
    3.83  apply (auto simp add: int_of_nat_of_if simp del: zless_int_of)
    3.84 @@ -564,7 +564,7 @@
    3.85  apply (blast intro: zless_zle_trans)
    3.86  done
    3.87  
    3.88 -lemma zless_nat_conj: "(nat_of(w) < nat_of(z)) <-> ($#0 $< z & w $< z)"
    3.89 +lemma zless_nat_conj: "(nat_of(w) < nat_of(z)) \<longleftrightarrow> ($#0 $< z & w $< z)"
    3.90  apply (case_tac "$#0 $< z")
    3.91  apply (auto simp add: zless_nat_conj_lemma nat_le_int0 not_zless_iff_zle)
    3.92  done
    3.93 @@ -575,24 +575,24 @@
    3.94      Conditional rewrite rules are tried after unconditional ones, so a rule
    3.95      like eq_nat_number_of will be tried first to eliminate #mm=#nn.]
    3.96    lemma integ_of_reorient [simp]:
    3.97 -       "True ==> (integ_of(w) = x) <-> (x = integ_of(w))"
    3.98 +       "True ==> (integ_of(w) = x) \<longleftrightarrow> (x = integ_of(w))"
    3.99    by auto
   3.100  *)
   3.101  
   3.102  lemma integ_of_minus_reorient [simp]:
   3.103 -     "(integ_of(w) = $- x) <-> ($- x = integ_of(w))"
   3.104 +     "(integ_of(w) = $- x) \<longleftrightarrow> ($- x = integ_of(w))"
   3.105  by auto
   3.106  
   3.107  lemma integ_of_add_reorient [simp]:
   3.108 -     "(integ_of(w) = x $+ y) <-> (x $+ y = integ_of(w))"
   3.109 +     "(integ_of(w) = x $+ y) \<longleftrightarrow> (x $+ y = integ_of(w))"
   3.110  by auto
   3.111  
   3.112  lemma integ_of_diff_reorient [simp]:
   3.113 -     "(integ_of(w) = x $- y) <-> (x $- y = integ_of(w))"
   3.114 +     "(integ_of(w) = x $- y) \<longleftrightarrow> (x $- y = integ_of(w))"
   3.115  by auto
   3.116  
   3.117  lemma integ_of_mult_reorient [simp]:
   3.118 -     "(integ_of(w) = x $* y) <-> (x $* y = integ_of(w))"
   3.119 +     "(integ_of(w) = x $* y) \<longleftrightarrow> (x $* y = integ_of(w))"
   3.120  by auto
   3.121  
   3.122  end
     4.1 --- a/src/ZF/Bool.thy	Tue Mar 06 15:15:49 2012 +0000
     4.2 +++ b/src/ZF/Bool.thy	Tue Mar 06 16:06:52 2012 +0000
     4.3 @@ -164,10 +164,10 @@
     4.4  lemma [simp,TC]: "bool_of_o(P) \<in> bool"
     4.5  by (simp add: bool_of_o_def)
     4.6  
     4.7 -lemma [simp]: "(bool_of_o(P) = 1) <-> P"
     4.8 +lemma [simp]: "(bool_of_o(P) = 1) \<longleftrightarrow> P"
     4.9  by (simp add: bool_of_o_def)
    4.10  
    4.11 -lemma [simp]: "(bool_of_o(P) = 0) <-> ~P"
    4.12 +lemma [simp]: "(bool_of_o(P) = 0) \<longleftrightarrow> ~P"
    4.13  by (simp add: bool_of_o_def)
    4.14  
    4.15  end
     5.1 --- a/src/ZF/Cardinal.thy	Tue Mar 06 15:15:49 2012 +0000
     5.2 +++ b/src/ZF/Cardinal.thy	Tue Mar 06 16:06:52 2012 +0000
     5.3 @@ -138,7 +138,7 @@
     5.4      "[| X \<approx> Y; [| X \<lesssim> Y; Y \<lesssim> X |] ==> P |] ==> P"
     5.5  by (blast intro: eqpoll_imp_lepoll eqpoll_sym)
     5.6  
     5.7 -lemma eqpoll_iff: "X \<approx> Y <-> X \<lesssim> Y & Y \<lesssim> X"
     5.8 +lemma eqpoll_iff: "X \<approx> Y \<longleftrightarrow> X \<lesssim> Y & Y \<lesssim> X"
     5.9  by (blast intro: eqpollI elim!: eqpollE)
    5.10  
    5.11  lemma lepoll_0_is_0: "A \<lesssim> 0 ==> A = 0"
    5.12 @@ -149,7 +149,7 @@
    5.13  (*@{term"0 \<lesssim> Y"}*)
    5.14  lemmas empty_lepollI = empty_subsetI [THEN subset_imp_lepoll]
    5.15  
    5.16 -lemma lepoll_0_iff: "A \<lesssim> 0 <-> A=0"
    5.17 +lemma lepoll_0_iff: "A \<lesssim> 0 \<longleftrightarrow> A=0"
    5.18  by (blast intro: lepoll_0_is_0 lepoll_refl)
    5.19  
    5.20  lemma Un_lepoll_Un:
    5.21 @@ -161,7 +161,7 @@
    5.22  (*A eqpoll 0 ==> A=0*)
    5.23  lemmas eqpoll_0_is_0 = eqpoll_imp_lepoll [THEN lepoll_0_is_0]
    5.24  
    5.25 -lemma eqpoll_0_iff: "A \<approx> 0 <-> A=0"
    5.26 +lemma eqpoll_0_iff: "A \<approx> 0 \<longleftrightarrow> A=0"
    5.27  by (blast intro: eqpoll_0_is_0 eqpoll_refl)
    5.28  
    5.29  lemma eqpoll_disjoint_Un:
    5.30 @@ -188,7 +188,7 @@
    5.31  apply (blast intro: well_ord_rvimage)
    5.32  done
    5.33  
    5.34 -lemma lepoll_iff_leqpoll: "A \<lesssim> B <-> A \<prec> B | A \<approx> B"
    5.35 +lemma lepoll_iff_leqpoll: "A \<lesssim> B \<longleftrightarrow> A \<prec> B | A \<approx> B"
    5.36  apply (unfold lesspoll_def)
    5.37  apply (blast intro!: eqpollI elim!: eqpollE)
    5.38  done
    5.39 @@ -288,7 +288,7 @@
    5.40  
    5.41  (*Not needed for simplification, but helpful below*)
    5.42  lemma Least_cong:
    5.43 -     "(!!y. P(y) <-> Q(y)) ==> (LEAST x. P(x)) = (LEAST x. Q(x))"
    5.44 +     "(!!y. P(y) \<longleftrightarrow> Q(y)) ==> (LEAST x. P(x)) = (LEAST x. Q(x))"
    5.45  by simp
    5.46  
    5.47  (*Need AC to get @{term"X \<lesssim> Y ==> |X| \<le> |Y|"};  see well_ord_lepoll_imp_Card_le
    5.48 @@ -319,7 +319,7 @@
    5.49  done
    5.50  
    5.51  lemma well_ord_cardinal_eqpoll_iff:
    5.52 -     "[| well_ord(X,r);  well_ord(Y,s) |] ==> |X| = |Y| <-> X \<approx> Y"
    5.53 +     "[| well_ord(X,r);  well_ord(Y,s) |] ==> |X| = |Y| \<longleftrightarrow> X \<approx> Y"
    5.54  by (blast intro: cardinal_cong well_ord_cardinal_eqE)
    5.55  
    5.56  
    5.57 @@ -358,7 +358,7 @@
    5.58  done
    5.59  
    5.60  (*The cardinals are the initial ordinals*)
    5.61 -lemma Card_iff_initial: "Card(K) <-> Ord(K) & (\<forall>j. j<K \<longrightarrow> ~ j \<approx> K)"
    5.62 +lemma Card_iff_initial: "Card(K) \<longleftrightarrow> Ord(K) & (\<forall>j. j<K \<longrightarrow> ~ j \<approx> K)"
    5.63  apply (safe intro!: CardI Card_is_Ord)
    5.64   prefer 2 apply blast
    5.65  apply (unfold Card_def cardinal_def)
    5.66 @@ -430,10 +430,10 @@
    5.67  apply (simp (no_asm_simp) add: cardinal_lt_imp_lt Card_is_Ord Card_cardinal_eq)
    5.68  done
    5.69  
    5.70 -lemma Card_lt_iff: "[| Ord(i);  Card(K) |] ==> (|i| < K) <-> (i < K)"
    5.71 +lemma Card_lt_iff: "[| Ord(i);  Card(K) |] ==> (|i| < K) \<longleftrightarrow> (i < K)"
    5.72  by (blast intro: Card_lt_imp_lt Ord_cardinal_le [THEN lt_trans1])
    5.73  
    5.74 -lemma Card_le_iff: "[| Ord(i);  Card(K) |] ==> (K \<le> |i|) <-> (K \<le> i)"
    5.75 +lemma Card_le_iff: "[| Ord(i);  Card(K) |] ==> (K \<le> |i|) \<longleftrightarrow> (K \<le> i)"
    5.76  by (simp add: Card_lt_iff Card_is_Ord Ord_cardinal not_lt_iff_le [THEN iff_sym])
    5.77  
    5.78  (*Can use AC or finiteness to discharge first premise*)
    5.79 @@ -510,7 +510,7 @@
    5.80  apply (blast intro!: succ_leI dest!: succ_lepoll_succD)
    5.81  done
    5.82  
    5.83 -lemma nat_eqpoll_iff: "[| m:nat; n: nat |] ==> m \<approx> n <-> m = n"
    5.84 +lemma nat_eqpoll_iff: "[| m:nat; n: nat |] ==> m \<approx> n \<longleftrightarrow> m = n"
    5.85  apply (rule iffI)
    5.86  apply (blast intro: nat_lepoll_imp_le le_anti_sym elim!: eqpollE)
    5.87  apply (simp add: eqpoll_refl)
    5.88 @@ -573,7 +573,7 @@
    5.89  apply (blast intro!: inj_not_surj_succ)
    5.90  done
    5.91  
    5.92 -lemma lesspoll_succ_iff: "m:nat ==> A \<prec> succ(m) <-> A \<lesssim> m"
    5.93 +lemma lesspoll_succ_iff: "m:nat ==> A \<prec> succ(m) \<longleftrightarrow> A \<lesssim> m"
    5.94  by (blast intro!: lepoll_imp_lesspoll_succ lesspoll_succ_imp_lepoll)
    5.95  
    5.96  lemma lepoll_succ_disj: "[| A \<lesssim> succ(m);  m:nat |] ==> A \<lesssim> m | A \<approx> succ(m)"
    5.97 @@ -602,7 +602,7 @@
    5.98  apply (rule Ord_succ_subsetI [THEN subset_imp_lepoll], assumption+)
    5.99  done
   5.100  
   5.101 -lemma Ord_nat_eqpoll_iff: "[| Ord(i);  n:nat |] ==> i \<approx> n <-> i=n"
   5.102 +lemma Ord_nat_eqpoll_iff: "[| Ord(i);  n:nat |] ==> i \<approx> n \<longleftrightarrow> i=n"
   5.103  apply (rule iffI)
   5.104   prefer 2 apply (simp add: eqpoll_refl)
   5.105  apply (rule Ord_linear_lt [of i n])
   5.106 @@ -647,11 +647,11 @@
   5.107  by (simp add: eqpoll_iff cons_lepoll_cong)
   5.108  
   5.109  lemma cons_lepoll_cons_iff:
   5.110 -     "[| a \<notin> A;  b \<notin> B |] ==> cons(a,A) \<lesssim> cons(b,B)  <->  A \<lesssim> B"
   5.111 +     "[| a \<notin> A;  b \<notin> B |] ==> cons(a,A) \<lesssim> cons(b,B)  \<longleftrightarrow>  A \<lesssim> B"
   5.112  by (blast intro: cons_lepoll_cong cons_lepoll_consD)
   5.113  
   5.114  lemma cons_eqpoll_cons_iff:
   5.115 -     "[| a \<notin> A;  b \<notin> B |] ==> cons(a,A) \<approx> cons(b,B)  <->  A \<approx> B"
   5.116 +     "[| a \<notin> A;  b \<notin> B |] ==> cons(a,A) \<approx> cons(b,B)  \<longleftrightarrow>  A \<approx> B"
   5.117  by (blast intro: cons_eqpoll_cong cons_eqpoll_consD)
   5.118  
   5.119  lemma singleton_eqpoll_1: "{a} \<approx> 1"
   5.120 @@ -813,10 +813,10 @@
   5.121  apply (erule Finite_cons)
   5.122  done
   5.123  
   5.124 -lemma Finite_cons_iff [iff]: "Finite(cons(y,x)) <-> Finite(x)"
   5.125 +lemma Finite_cons_iff [iff]: "Finite(cons(y,x)) \<longleftrightarrow> Finite(x)"
   5.126  by (blast intro: Finite_cons subset_Finite)
   5.127  
   5.128 -lemma Finite_succ_iff [iff]: "Finite(succ(x)) <-> Finite(x)"
   5.129 +lemma Finite_succ_iff [iff]: "Finite(succ(x)) \<longleftrightarrow> Finite(x)"
   5.130  by (simp add: succ_def)
   5.131  
   5.132  lemma nat_le_infinite_Ord:
   5.133 @@ -859,7 +859,7 @@
   5.134  lemma Finite_Fin: "[| Finite(A); A \<subseteq> X |] ==> A \<in> Fin(X)"
   5.135  by (unfold Finite_def, blast intro: Finite_Fin_lemma)
   5.136  
   5.137 -lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) <-> Finite(B)"
   5.138 +lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) \<longleftrightarrow> Finite(B)"
   5.139  apply (unfold Finite_def)
   5.140  apply (blast intro: eqpoll_trans eqpoll_sym)
   5.141  done
   5.142 @@ -888,7 +888,7 @@
   5.143  lemma Fin_into_Finite: "A \<in> Fin(U) ==> Finite(A)"
   5.144  by (fast intro!: Finite_0 Finite_cons elim: Fin_induct)
   5.145  
   5.146 -lemma Finite_Fin_iff: "Finite(A) <-> A \<in> Fin(A)"
   5.147 +lemma Finite_Fin_iff: "Finite(A) \<longleftrightarrow> A \<in> Fin(A)"
   5.148  by (blast intro: Finite_into_Fin Fin_into_Finite)
   5.149  
   5.150  lemma Finite_Un: "[| Finite(A); Finite(B) |] ==> Finite(A \<union> B)"
   5.151 @@ -897,7 +897,7 @@
   5.152            intro: Un_upper1 [THEN Fin_mono, THEN subsetD]
   5.153                   Un_upper2 [THEN Fin_mono, THEN subsetD])
   5.154  
   5.155 -lemma Finite_Un_iff [simp]: "Finite(A \<union> B) <-> (Finite(A) & Finite(B))"
   5.156 +lemma Finite_Un_iff [simp]: "Finite(A \<union> B) \<longleftrightarrow> (Finite(A) & Finite(B))"
   5.157  by (blast intro: subset_Finite Finite_Un)
   5.158  
   5.159  text{*The converse must hold too.*}
   5.160 @@ -961,7 +961,7 @@
   5.161  text{*I don't know why, but if the premise is expressed using meta-connectives
   5.162  then  the simplifier cannot prove it automatically in conditional rewriting.*}
   5.163  lemma Finite_RepFun_iff:
   5.164 -     "(\<forall>x y. f(x)=f(y) \<longrightarrow> x=y) ==> Finite(RepFun(A,f)) <-> Finite(A)"
   5.165 +     "(\<forall>x y. f(x)=f(y) \<longrightarrow> x=y) ==> Finite(RepFun(A,f)) \<longleftrightarrow> Finite(A)"
   5.166  by (blast intro: Finite_RepFun Finite_RepFun_iff_lemma [of _ f])
   5.167  
   5.168  lemma Finite_Pow: "Finite(A) ==> Finite(Pow(A))"
   5.169 @@ -975,7 +975,7 @@
   5.170  apply (blast intro: subset_Finite)
   5.171  done
   5.172  
   5.173 -lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) <-> Finite(A)"
   5.174 +lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) \<longleftrightarrow> Finite(A)"
   5.175  by (blast intro: Finite_Pow Finite_Pow_imp_Finite)
   5.176  
   5.177  
     6.1 --- a/src/ZF/CardinalArith.thy	Tue Mar 06 15:15:49 2012 +0000
     6.2 +++ b/src/ZF/CardinalArith.thy	Tue Mar 06 16:06:52 2012 +0000
     6.3 @@ -39,11 +39,11 @@
     6.4          of @{term K}*}
     6.5      "csucc(K) == LEAST L. Card(L) & K<L"
     6.6  
     6.7 -notation (xsymbols output)
     6.8 +notation (xsymbols)
     6.9    cadd  (infixl "\<oplus>" 65) and
    6.10    cmult  (infixl "\<otimes>" 70)
    6.11  
    6.12 -notation (HTML output)
    6.13 +notation (HTML)
    6.14    cadd  (infixl "\<oplus>" 65) and
    6.15    cmult  (infixl "\<otimes>" 70)
    6.16  
    6.17 @@ -109,7 +109,7 @@
    6.18  apply auto
    6.19  done
    6.20  
    6.21 -lemma cadd_commute: "i |+| j = j |+| i"
    6.22 +lemma cadd_commute: "i \<oplus> j = j \<oplus> i"
    6.23  apply (unfold cadd_def)
    6.24  apply (rule sum_commute_eqpoll [THEN cardinal_cong])
    6.25  done
    6.26 @@ -125,7 +125,7 @@
    6.27  (*Unconditional version requires AC*)
    6.28  lemma well_ord_cadd_assoc:
    6.29      "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]
    6.30 -     ==> (i |+| j) |+| k = i |+| (j |+| k)"
    6.31 +     ==> (i \<oplus> j) \<oplus> k = i \<oplus> (j \<oplus> k)"
    6.32  apply (unfold cadd_def)
    6.33  apply (rule cardinal_cong)
    6.34  apply (rule eqpoll_trans)
    6.35 @@ -145,7 +145,7 @@
    6.36  apply (rule bij_0_sum)
    6.37  done
    6.38  
    6.39 -lemma cadd_0 [simp]: "Card(K) ==> 0 |+| K = K"
    6.40 +lemma cadd_0 [simp]: "Card(K) ==> 0 \<oplus> K = K"
    6.41  apply (unfold cadd_def)
    6.42  apply (simp add: sum_0_eqpoll [THEN cardinal_cong] Card_cardinal_eq)
    6.43  done
    6.44 @@ -161,7 +161,7 @@
    6.45  (*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
    6.46  
    6.47  lemma cadd_le_self:
    6.48 -    "[| Card(K);  Ord(L) |] ==> K \<le> (K |+| L)"
    6.49 +    "[| Card(K);  Ord(L) |] ==> K \<le> (K \<oplus> L)"
    6.50  apply (unfold cadd_def)
    6.51  apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le],
    6.52         assumption)
    6.53 @@ -182,7 +182,7 @@
    6.54  done
    6.55  
    6.56  lemma cadd_le_mono:
    6.57 -    "[| K' \<le> K;  L' \<le> L |] ==> (K' |+| L') \<le> (K |+| L)"
    6.58 +    "[| K' \<le> K;  L' \<le> L |] ==> (K' \<oplus> L') \<le> (K \<oplus> L)"
    6.59  apply (unfold cadd_def)
    6.60  apply (safe dest!: le_subset_iff [THEN iffD1])
    6.61  apply (rule well_ord_lepoll_imp_Card_le)
    6.62 @@ -204,7 +204,7 @@
    6.63  (*Pulling the  succ(...)  outside the |...| requires m, n: nat  *)
    6.64  (*Unconditional version requires AC*)
    6.65  lemma cadd_succ_lemma:
    6.66 -    "[| Ord(m);  Ord(n) |] ==> succ(m) |+| n = |succ(m |+| n)|"
    6.67 +    "[| Ord(m);  Ord(n) |] ==> succ(m) \<oplus> n = |succ(m \<oplus> n)|"
    6.68  apply (unfold cadd_def)
    6.69  apply (rule sum_succ_eqpoll [THEN cardinal_cong, THEN trans])
    6.70  apply (rule succ_eqpoll_cong [THEN cardinal_cong])
    6.71 @@ -212,7 +212,7 @@
    6.72  apply (blast intro: well_ord_radd well_ord_Memrel)
    6.73  done
    6.74  
    6.75 -lemma nat_cadd_eq_add: "[| m: nat;  n: nat |] ==> m |+| n = m#+n"
    6.76 +lemma nat_cadd_eq_add: "[| m: nat;  n: nat |] ==> m \<oplus> n = m#+n"
    6.77  apply (induct_tac m)
    6.78  apply (simp add: nat_into_Card [THEN cadd_0])
    6.79  apply (simp add: cadd_succ_lemma nat_into_Card [THEN Card_cardinal_eq])
    6.80 @@ -231,7 +231,7 @@
    6.81         auto)
    6.82  done
    6.83  
    6.84 -lemma cmult_commute: "i |*| j = j |*| i"
    6.85 +lemma cmult_commute: "i \<otimes> j = j \<otimes> i"
    6.86  apply (unfold cmult_def)
    6.87  apply (rule prod_commute_eqpoll [THEN cardinal_cong])
    6.88  done
    6.89 @@ -247,7 +247,7 @@
    6.90  (*Unconditional version requires AC*)
    6.91  lemma well_ord_cmult_assoc:
    6.92      "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]
    6.93 -     ==> (i |*| j) |*| k = i |*| (j |*| k)"
    6.94 +     ==> (i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
    6.95  apply (unfold cmult_def)
    6.96  apply (rule cardinal_cong)
    6.97  apply (rule eqpoll_trans)
    6.98 @@ -269,7 +269,7 @@
    6.99  
   6.100  lemma well_ord_cadd_cmult_distrib:
   6.101      "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]
   6.102 -     ==> (i |+| j) |*| k = (i |*| k) |+| (j |*| k)"
   6.103 +     ==> (i \<oplus> j) \<otimes> k = (i \<otimes> k) \<oplus> (j \<otimes> k)"
   6.104  apply (unfold cadd_def cmult_def)
   6.105  apply (rule cardinal_cong)
   6.106  apply (rule eqpoll_trans)
   6.107 @@ -290,7 +290,7 @@
   6.108  apply (rule lam_bijective, safe)
   6.109  done
   6.110  
   6.111 -lemma cmult_0 [simp]: "0 |*| i = 0"
   6.112 +lemma cmult_0 [simp]: "0 \<otimes> i = 0"
   6.113  by (simp add: cmult_def prod_0_eqpoll [THEN cardinal_cong])
   6.114  
   6.115  subsubsection{*1 is the identity for multiplication*}
   6.116 @@ -301,7 +301,7 @@
   6.117  apply (rule singleton_prod_bij [THEN bij_converse_bij])
   6.118  done
   6.119  
   6.120 -lemma cmult_1 [simp]: "Card(K) ==> 1 |*| K = K"
   6.121 +lemma cmult_1 [simp]: "Card(K) ==> 1 \<otimes> K = K"
   6.122  apply (unfold cmult_def succ_def)
   6.123  apply (simp add: prod_singleton_eqpoll [THEN cardinal_cong] Card_cardinal_eq)
   6.124  done
   6.125 @@ -314,7 +314,7 @@
   6.126  done
   6.127  
   6.128  (*Could probably weaken the premise to well_ord(K,r), or remove using AC*)
   6.129 -lemma cmult_square_le: "Card(K) ==> K \<le> K |*| K"
   6.130 +lemma cmult_square_le: "Card(K) ==> K \<le> K \<otimes> K"
   6.131  apply (unfold cmult_def)
   6.132  apply (rule le_trans)
   6.133  apply (rule_tac [2] well_ord_lepoll_imp_Card_le)
   6.134 @@ -332,7 +332,7 @@
   6.135  
   6.136  (*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
   6.137  lemma cmult_le_self:
   6.138 -    "[| Card(K);  Ord(L);  0<L |] ==> K \<le> (K |*| L)"
   6.139 +    "[| Card(K);  Ord(L);  0<L |] ==> K \<le> (K \<otimes> L)"
   6.140  apply (unfold cmult_def)
   6.141  apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le])
   6.142    apply assumption
   6.143 @@ -353,7 +353,7 @@
   6.144  done
   6.145  
   6.146  lemma cmult_le_mono:
   6.147 -    "[| K' \<le> K;  L' \<le> L |] ==> (K' |*| L') \<le> (K |*| L)"
   6.148 +    "[| K' \<le> K;  L' \<le> L |] ==> (K' \<otimes> L') \<le> (K \<otimes> L)"
   6.149  apply (unfold cmult_def)
   6.150  apply (safe dest!: le_subset_iff [THEN iffD1])
   6.151  apply (rule well_ord_lepoll_imp_Card_le)
   6.152 @@ -374,7 +374,7 @@
   6.153  
   6.154  (*Unconditional version requires AC*)
   6.155  lemma cmult_succ_lemma:
   6.156 -    "[| Ord(m);  Ord(n) |] ==> succ(m) |*| n = n |+| (m |*| n)"
   6.157 +    "[| Ord(m);  Ord(n) |] ==> succ(m) \<otimes> n = n \<oplus> (m \<otimes> n)"
   6.158  apply (unfold cmult_def cadd_def)
   6.159  apply (rule prod_succ_eqpoll [THEN cardinal_cong, THEN trans])
   6.160  apply (rule cardinal_cong [symmetric])
   6.161 @@ -382,12 +382,12 @@
   6.162  apply (blast intro: well_ord_rmult well_ord_Memrel)
   6.163  done
   6.164  
   6.165 -lemma nat_cmult_eq_mult: "[| m: nat;  n: nat |] ==> m |*| n = m#*n"
   6.166 +lemma nat_cmult_eq_mult: "[| m: nat;  n: nat |] ==> m \<otimes> n = m#*n"
   6.167  apply (induct_tac m)
   6.168  apply (simp_all add: cmult_succ_lemma nat_cadd_eq_add)
   6.169  done
   6.170  
   6.171 -lemma cmult_2: "Card(n) ==> 2 |*| n = n |+| n"
   6.172 +lemma cmult_2: "Card(n) ==> 2 \<otimes> n = n \<oplus> n"
   6.173  by (simp add: cmult_succ_lemma Card_is_Ord cadd_commute [of _ 0])
   6.174  
   6.175  lemma sum_lepoll_prod: "2 \<lesssim> C ==> B+B \<lesssim> C*B"
   6.176 @@ -555,7 +555,7 @@
   6.177  (*Kunen: "each <x,y>: K*K has no more than z*z predecessors..." (page 29) *)
   6.178  lemma ordermap_csquare_le:
   6.179    "[| Limit(K);  x<K;  y<K;  z=succ(x \<union> y) |]
   6.180 -   ==> | ordermap(K*K, csquare_rel(K)) ` <x,y> | \<le> |succ(z)| |*| |succ(z)|"
   6.181 +   ==> | ordermap(K*K, csquare_rel(K)) ` <x,y> | \<le> |succ(z)| \<otimes> |succ(z)|"
   6.182  apply (unfold cmult_def)
   6.183  apply (rule well_ord_rmult [THEN well_ord_lepoll_imp_Card_le])
   6.184  apply (rule Ord_cardinal [THEN well_ord_Memrel])+
   6.185 @@ -575,7 +575,7 @@
   6.186  
   6.187  (*Kunen: "... so the order type is @{text"\<le>"} K" *)
   6.188  lemma ordertype_csquare_le:
   6.189 -     "[| InfCard(K);  \<forall>y\<in>K. InfCard(y) \<longrightarrow> y |*| y = y |]
   6.190 +     "[| InfCard(K);  \<forall>y\<in>K. InfCard(y) \<longrightarrow> y \<otimes> y = y |]
   6.191        ==> ordertype(K*K, csquare_rel(K)) \<le> K"
   6.192  apply (frule InfCard_is_Card [THEN Card_is_Ord])
   6.193  apply (rule all_lt_imp_le, assumption)
   6.194 @@ -604,7 +604,7 @@
   6.195  done
   6.196  
   6.197  (*Main result: Kunen's Theorem 10.12*)
   6.198 -lemma InfCard_csquare_eq: "InfCard(K) ==> K |*| K = K"
   6.199 +lemma InfCard_csquare_eq: "InfCard(K) ==> K \<otimes> K = K"
   6.200  apply (frule InfCard_is_Card [THEN Card_is_Ord])
   6.201  apply (erule rev_mp)
   6.202  apply (erule_tac i=K in trans_induct)
   6.203 @@ -639,7 +639,7 @@
   6.204  
   6.205  subsubsection{*Toward's Kunen's Corollary 10.13 (1)*}
   6.206  
   6.207 -lemma InfCard_le_cmult_eq: "[| InfCard(K);  L \<le> K;  0<L |] ==> K |*| L = K"
   6.208 +lemma InfCard_le_cmult_eq: "[| InfCard(K);  L \<le> K;  0<L |] ==> K \<otimes> L = K"
   6.209  apply (rule le_anti_sym)
   6.210   prefer 2
   6.211   apply (erule ltE, blast intro: cmult_le_self InfCard_is_Card)
   6.212 @@ -649,7 +649,7 @@
   6.213  done
   6.214  
   6.215  (*Corollary 10.13 (1), for cardinal multiplication*)
   6.216 -lemma InfCard_cmult_eq: "[| InfCard(K);  InfCard(L) |] ==> K |*| L = K \<union> L"
   6.217 +lemma InfCard_cmult_eq: "[| InfCard(K);  InfCard(L) |] ==> K \<otimes> L = K \<union> L"
   6.218  apply (rule_tac i = K and j = L in Ord_linear_le)
   6.219  apply (typecheck add: InfCard_is_Card Card_is_Ord)
   6.220  apply (rule cmult_commute [THEN ssubst])
   6.221 @@ -658,13 +658,13 @@
   6.222                       subset_Un_iff2 [THEN iffD1] le_imp_subset)
   6.223  done
   6.224  
   6.225 -lemma InfCard_cdouble_eq: "InfCard(K) ==> K |+| K = K"
   6.226 +lemma InfCard_cdouble_eq: "InfCard(K) ==> K \<oplus> K = K"
   6.227  apply (simp add: cmult_2 [symmetric] InfCard_is_Card cmult_commute)
   6.228  apply (simp add: InfCard_le_cmult_eq InfCard_is_Limit Limit_has_0 Limit_has_succ)
   6.229  done
   6.230  
   6.231  (*Corollary 10.13 (1), for cardinal addition*)
   6.232 -lemma InfCard_le_cadd_eq: "[| InfCard(K);  L \<le> K |] ==> K |+| L = K"
   6.233 +lemma InfCard_le_cadd_eq: "[| InfCard(K);  L \<le> K |] ==> K \<oplus> L = K"
   6.234  apply (rule le_anti_sym)
   6.235   prefer 2
   6.236   apply (erule ltE, blast intro: cadd_le_self InfCard_is_Card)
   6.237 @@ -673,7 +673,7 @@
   6.238  apply (simp add: InfCard_cdouble_eq)
   6.239  done
   6.240  
   6.241 -lemma InfCard_cadd_eq: "[| InfCard(K);  InfCard(L) |] ==> K |+| L = K \<union> L"
   6.242 +lemma InfCard_cadd_eq: "[| InfCard(K);  InfCard(L) |] ==> K \<oplus> L = K \<union> L"
   6.243  apply (rule_tac i = K and j = L in Ord_linear_le)
   6.244  apply (typecheck add: InfCard_is_Card Card_is_Ord)
   6.245  apply (rule cadd_commute [THEN ssubst])
   6.246 @@ -704,7 +704,7 @@
   6.247  
   6.248  (*Allows selective unfolding.  Less work than deriving intro/elim rules*)
   6.249  lemma jump_cardinal_iff:
   6.250 -     "i \<in> jump_cardinal(K) <->
   6.251 +     "i \<in> jump_cardinal(K) \<longleftrightarrow>
   6.252        (\<exists>r X. r \<subseteq> K*K & X \<subseteq> K & well_ord(X,r) & i = ordertype(X,r))"
   6.253  apply (unfold jump_cardinal_def)
   6.254  apply (blast del: subsetI)
   6.255 @@ -766,7 +766,7 @@
   6.256  apply (blast intro: Card_is_Ord)+
   6.257  done
   6.258  
   6.259 -lemma lt_csucc_iff: "[| Ord(i); Card(K) |] ==> i < csucc(K) <-> |i| \<le> K"
   6.260 +lemma lt_csucc_iff: "[| Ord(i); Card(K) |] ==> i < csucc(K) \<longleftrightarrow> |i| \<le> K"
   6.261  apply (rule iffI)
   6.262  apply (rule_tac [2] Card_lt_imp_lt)
   6.263  apply (erule_tac [2] lt_trans1)
   6.264 @@ -778,7 +778,7 @@
   6.265  done
   6.266  
   6.267  lemma Card_lt_csucc_iff:
   6.268 -     "[| Card(K'); Card(K) |] ==> K' < csucc(K) <-> K' \<le> K"
   6.269 +     "[| Card(K'); Card(K) |] ==> K' < csucc(K) \<longleftrightarrow> K' \<le> K"
   6.270  by (simp add: lt_csucc_iff Card_cardinal_eq Card_is_Ord)
   6.271  
   6.272  lemma InfCard_csucc: "InfCard(K) ==> InfCard(csucc(K))"
     7.1 --- a/src/ZF/Cardinal_AC.thy	Tue Mar 06 15:15:49 2012 +0000
     7.2 +++ b/src/ZF/Cardinal_AC.thy	Tue Mar 06 16:06:52 2012 +0000
     7.3 @@ -25,7 +25,7 @@
     7.4  apply (rule well_ord_cardinal_eqE, assumption+)
     7.5  done
     7.6  
     7.7 -lemma cardinal_eqpoll_iff: "|X| = |Y| <-> X eqpoll Y"
     7.8 +lemma cardinal_eqpoll_iff: "|X| = |Y| \<longleftrightarrow> X eqpoll Y"
     7.9  by (blast intro: cardinal_cong cardinal_eqE)
    7.10  
    7.11  lemma cardinal_disjoint_Un:
    7.12 @@ -38,21 +38,21 @@
    7.13  apply (erule well_ord_lepoll_imp_Card_le, assumption)
    7.14  done
    7.15  
    7.16 -lemma cadd_assoc: "(i |+| j) |+| k = i |+| (j |+| k)"
    7.17 +lemma cadd_assoc: "(i \<oplus> j) \<oplus> k = i \<oplus> (j \<oplus> k)"
    7.18  apply (rule AC_well_ord [THEN exE])
    7.19  apply (rule AC_well_ord [THEN exE])
    7.20  apply (rule AC_well_ord [THEN exE])
    7.21  apply (rule well_ord_cadd_assoc, assumption+)
    7.22  done
    7.23  
    7.24 -lemma cmult_assoc: "(i |*| j) |*| k = i |*| (j |*| k)"
    7.25 +lemma cmult_assoc: "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
    7.26  apply (rule AC_well_ord [THEN exE])
    7.27  apply (rule AC_well_ord [THEN exE])
    7.28  apply (rule AC_well_ord [THEN exE])
    7.29  apply (rule well_ord_cmult_assoc, assumption+)
    7.30  done
    7.31  
    7.32 -lemma cadd_cmult_distrib: "(i |+| j) |*| k = (i |*| k) |+| (j |*| k)"
    7.33 +lemma cadd_cmult_distrib: "(i \<oplus> j) \<otimes> k = (i \<otimes> k) \<oplus> (j \<otimes> k)"
    7.34  apply (rule AC_well_ord [THEN exE])
    7.35  apply (rule AC_well_ord [THEN exE])
    7.36  apply (rule AC_well_ord [THEN exE])
    7.37 @@ -74,19 +74,19 @@
    7.38  apply (rule cardinal_eqpoll [THEN eqpoll_imp_lepoll])
    7.39  done
    7.40  
    7.41 -lemma le_Card_iff: "Card(K) ==> |A| \<le> K <-> A lepoll K"
    7.42 +lemma le_Card_iff: "Card(K) ==> |A| \<le> K \<longleftrightarrow> A lepoll K"
    7.43  apply (erule Card_cardinal_eq [THEN subst], rule iffI,
    7.44         erule Card_le_imp_lepoll)
    7.45  apply (erule lepoll_imp_Card_le)
    7.46  done
    7.47  
    7.48 -lemma cardinal_0_iff_0 [simp]: "|A| = 0 <-> A = 0";
    7.49 +lemma cardinal_0_iff_0 [simp]: "|A| = 0 \<longleftrightarrow> A = 0";
    7.50  apply auto
    7.51  apply (drule cardinal_0 [THEN ssubst])
    7.52  apply (blast intro: eqpoll_0_iff [THEN iffD1] cardinal_eqpoll_iff [THEN iffD1])
    7.53  done
    7.54  
    7.55 -lemma cardinal_lt_iff_lesspoll: "Ord(i) ==> i < |A| <-> i lesspoll A"
    7.56 +lemma cardinal_lt_iff_lesspoll: "Ord(i) ==> i < |A| \<longleftrightarrow> i lesspoll A"
    7.57  apply (cut_tac A = "A" in cardinal_eqpoll)
    7.58  apply (auto simp add: eqpoll_iff)
    7.59  apply (blast intro: lesspoll_trans2 lt_Card_imp_lesspoll Card_cardinal)
     8.1 --- a/src/ZF/EquivClass.thy	Tue Mar 06 15:15:49 2012 +0000
     8.2 +++ b/src/ZF/EquivClass.thy	Tue Mar 06 16:06:52 2012 +0000
     8.3 @@ -92,11 +92,11 @@
     8.4  by (unfold equiv_def, blast)
     8.5  
     8.6  lemma equiv_class_eq_iff:
     8.7 -     "equiv(A,r) ==> <x,y>: r <-> r``{x} = r``{y} & x:A & y:A"
     8.8 +     "equiv(A,r) ==> <x,y>: r \<longleftrightarrow> r``{x} = r``{y} & x:A & y:A"
     8.9  by (blast intro: eq_equiv_class equiv_class_eq dest: equiv_type)
    8.10  
    8.11  lemma eq_equiv_class_iff:
    8.12 -     "[| equiv(A,r);  x: A;  y: A |] ==> r``{x} = r``{y} <-> <x,y>: r"
    8.13 +     "[| equiv(A,r);  x: A;  y: A |] ==> r``{x} = r``{y} \<longleftrightarrow> <x,y>: r"
    8.14  by (blast intro: eq_equiv_class equiv_class_eq dest: equiv_type)
    8.15  
    8.16  (*** Quotients ***)
     9.1 --- a/src/ZF/Finite.thy	Tue Mar 06 15:15:49 2012 +0000
     9.2 +++ b/src/ZF/Finite.thy	Tue Mar 06 16:06:52 2012 +0000
     9.3 @@ -183,7 +183,7 @@
     9.4  
     9.5  lemma FiniteFun_Collect_iff:
     9.6       "f \<in> FiniteFun(A, {y:B. P(y)})
     9.7 -      <-> f \<in> FiniteFun(A,B) & (\<forall>x\<in>domain(f). P(f`x))"
     9.8 +      \<longleftrightarrow> f \<in> FiniteFun(A,B) & (\<forall>x\<in>domain(f). P(f`x))"
     9.9  apply auto
    9.10  apply (blast intro: FiniteFun_mono [THEN [2] rev_subsetD])
    9.11  apply (blast dest: Pair_mem_PiD FiniteFun_is_fun)
    10.1 --- a/src/ZF/Inductive_ZF.thy	Tue Mar 06 15:15:49 2012 +0000
    10.2 +++ b/src/ZF/Inductive_ZF.thy	Tue Mar 06 16:06:52 2012 +0000
    10.3 @@ -22,7 +22,7 @@
    10.4    ("Tools/primrec_package.ML")
    10.5  begin
    10.6  
    10.7 -lemma def_swap_iff: "a == b ==> a = c <-> c = b"
    10.8 +lemma def_swap_iff: "a == b ==> a = c \<longleftrightarrow> c = b"
    10.9    by blast
   10.10  
   10.11  lemma def_trans: "f == g ==> g(a) = b ==> f(a) = b"
    11.1 --- a/src/ZF/IntArith.thy	Tue Mar 06 15:15:49 2012 +0000
    11.2 +++ b/src/ZF/IntArith.thy	Tue Mar 06 16:06:52 2012 +0000
    11.3 @@ -31,13 +31,13 @@
    11.4  
    11.5  (** Combining of literal coefficients in sums of products **)
    11.6  
    11.7 -lemma zless_iff_zdiff_zless_0: "(x $< y) <-> (x$-y $< #0)"
    11.8 +lemma zless_iff_zdiff_zless_0: "(x $< y) \<longleftrightarrow> (x$-y $< #0)"
    11.9    by (simp add: zcompare_rls)
   11.10  
   11.11 -lemma eq_iff_zdiff_eq_0: "[| x: int; y: int |] ==> (x = y) <-> (x$-y = #0)"
   11.12 +lemma eq_iff_zdiff_eq_0: "[| x: int; y: int |] ==> (x = y) \<longleftrightarrow> (x$-y = #0)"
   11.13    by (simp add: zcompare_rls)
   11.14  
   11.15 -lemma zle_iff_zdiff_zle_0: "(x $<= y) <-> (x$-y $<= #0)"
   11.16 +lemma zle_iff_zdiff_zle_0: "(x $<= y) \<longleftrightarrow> (x$-y $<= #0)"
   11.17    by (simp add: zcompare_rls)
   11.18  
   11.19  
   11.20 @@ -58,33 +58,33 @@
   11.21    zle_iff_zdiff_zle_0 [where y = n]
   11.22    for u v (* FIXME n (!?) *)
   11.23  
   11.24 -lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) <-> ((i$-j)$*u $+ m = intify(n))"
   11.25 +lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m = intify(n))"
   11.26    apply (simp add: zdiff_def zadd_zmult_distrib)
   11.27    apply (simp add: zcompare_rls)
   11.28    apply (simp add: zadd_ac)
   11.29    done
   11.30  
   11.31 -lemma eq_add_iff2: "(i$*u $+ m = j$*u $+ n) <-> (intify(m) = (j$-i)$*u $+ n)"
   11.32 +lemma eq_add_iff2: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> (intify(m) = (j$-i)$*u $+ n)"
   11.33    apply (simp add: zdiff_def zadd_zmult_distrib)
   11.34    apply (simp add: zcompare_rls)
   11.35    apply (simp add: zadd_ac)
   11.36    done
   11.37  
   11.38 -lemma less_add_iff1: "(i$*u $+ m $< j$*u $+ n) <-> ((i$-j)$*u $+ m $< n)"
   11.39 +lemma less_add_iff1: "(i$*u $+ m $< j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $< n)"
   11.40    apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
   11.41    done
   11.42  
   11.43 -lemma less_add_iff2: "(i$*u $+ m $< j$*u $+ n) <-> (m $< (j$-i)$*u $+ n)"
   11.44 +lemma less_add_iff2: "(i$*u $+ m $< j$*u $+ n) \<longleftrightarrow> (m $< (j$-i)$*u $+ n)"
   11.45    apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
   11.46    done
   11.47  
   11.48 -lemma le_add_iff1: "(i$*u $+ m $<= j$*u $+ n) <-> ((i$-j)$*u $+ m $<= n)"
   11.49 +lemma le_add_iff1: "(i$*u $+ m $<= j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $<= n)"
   11.50    apply (simp add: zdiff_def zadd_zmult_distrib)
   11.51    apply (simp add: zcompare_rls)
   11.52    apply (simp add: zadd_ac)
   11.53    done
   11.54  
   11.55 -lemma le_add_iff2: "(i$*u $+ m $<= j$*u $+ n) <-> (m $<= (j$-i)$*u $+ n)"
   11.56 +lemma le_add_iff2: "(i$*u $+ m $<= j$*u $+ n) \<longleftrightarrow> (m $<= (j$-i)$*u $+ n)"
   11.57    apply (simp add: zdiff_def zadd_zmult_distrib)
   11.58    apply (simp add: zcompare_rls)
   11.59    apply (simp add: zadd_ac)
    12.1 --- a/src/ZF/IntDiv_ZF.thy	Tue Mar 06 15:15:49 2012 +0000
    12.2 +++ b/src/ZF/IntDiv_ZF.thy	Tue Mar 06 16:06:52 2012 +0000
    12.3 @@ -136,7 +136,7 @@
    12.4  (*** Inequality lemmas involving $#succ(m) ***)
    12.5  
    12.6  lemma zless_add_succ_iff:
    12.7 -     "(w $< z $+ $# succ(m)) <-> (w $< z $+ $#m | intify(w) = z $+ $#m)"
    12.8 +     "(w $< z $+ $# succ(m)) \<longleftrightarrow> (w $< z $+ $#m | intify(w) = z $+ $#m)"
    12.9  apply (auto simp add: zless_iff_succ_zadd zadd_assoc int_of_add [symmetric])
   12.10  apply (rule_tac [3] x = "0" in bexI)
   12.11  apply (cut_tac m = "m" in int_succ_int_1)
   12.12 @@ -149,32 +149,32 @@
   12.13  done
   12.14  
   12.15  lemma zadd_succ_lemma:
   12.16 -     "z \<in> int ==> (w $+ $# succ(m) $<= z) <-> (w $+ $#m $< z)"
   12.17 +     "z \<in> int ==> (w $+ $# succ(m) $<= z) \<longleftrightarrow> (w $+ $#m $< z)"
   12.18  apply (simp only: not_zless_iff_zle [THEN iff_sym] zless_add_succ_iff)
   12.19  apply (auto intro: zle_anti_sym elim: zless_asym
   12.20              simp add: zless_imp_zle not_zless_iff_zle)
   12.21  done
   12.22  
   12.23 -lemma zadd_succ_zle_iff: "(w $+ $# succ(m) $<= z) <-> (w $+ $#m $< z)"
   12.24 +lemma zadd_succ_zle_iff: "(w $+ $# succ(m) $<= z) \<longleftrightarrow> (w $+ $#m $< z)"
   12.25  apply (cut_tac z = "intify (z)" in zadd_succ_lemma)
   12.26  apply auto
   12.27  done
   12.28  
   12.29  (** Inequality reasoning **)
   12.30  
   12.31 -lemma zless_add1_iff_zle: "(w $< z $+ #1) <-> (w$<=z)"
   12.32 +lemma zless_add1_iff_zle: "(w $< z $+ #1) \<longleftrightarrow> (w$<=z)"
   12.33  apply (subgoal_tac "#1 = $# 1")
   12.34  apply (simp only: zless_add_succ_iff zle_def)
   12.35  apply auto
   12.36  done
   12.37  
   12.38 -lemma add1_zle_iff: "(w $+ #1 $<= z) <-> (w $< z)"
   12.39 +lemma add1_zle_iff: "(w $+ #1 $<= z) \<longleftrightarrow> (w $< z)"
   12.40  apply (subgoal_tac "#1 = $# 1")
   12.41  apply (simp only: zadd_succ_zle_iff)
   12.42  apply auto
   12.43  done
   12.44  
   12.45 -lemma add1_left_zle_iff: "(#1 $+ w $<= z) <-> (w $< z)"
   12.46 +lemma add1_left_zle_iff: "(#1 $+ w $<= z) \<longleftrightarrow> (w $< z)"
   12.47  apply (subst zadd_commute)
   12.48  apply (rule add1_zle_iff)
   12.49  done
   12.50 @@ -280,13 +280,13 @@
   12.51  (** Products of zeroes **)
   12.52  
   12.53  lemma zmult_eq_lemma:
   12.54 -     "[| m \<in> int; n \<in> int |] ==> (m = #0 | n = #0) <-> (m$*n = #0)"
   12.55 +     "[| m \<in> int; n \<in> int |] ==> (m = #0 | n = #0) \<longleftrightarrow> (m$*n = #0)"
   12.56  apply (case_tac "m $< #0")
   12.57  apply (auto simp add: not_zless_iff_zle zle_def neq_iff_zless)
   12.58  apply (force dest: zmult_zless_mono1_neg zmult_zless_mono1)+
   12.59  done
   12.60  
   12.61 -lemma zmult_eq_0_iff [iff]: "(m$*n = #0) <-> (intify(m) = #0 | intify(n) = #0)"
   12.62 +lemma zmult_eq_0_iff [iff]: "(m$*n = #0) \<longleftrightarrow> (intify(m) = #0 | intify(n) = #0)"
   12.63  apply (simp add: zmult_eq_lemma)
   12.64  done
   12.65  
   12.66 @@ -296,7 +296,7 @@
   12.67  
   12.68  lemma zmult_zless_lemma:
   12.69       "[| k \<in> int; m \<in> int; n \<in> int |]
   12.70 -      ==> (m$*k $< n$*k) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
   12.71 +      ==> (m$*k $< n$*k) \<longleftrightarrow> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
   12.72  apply (case_tac "k = #0")
   12.73  apply (auto simp add: neq_iff_zless zmult_zless_mono1 zmult_zless_mono1_neg)
   12.74  apply (auto simp add: not_zless_iff_zle
   12.75 @@ -307,43 +307,43 @@
   12.76  done
   12.77  
   12.78  lemma zmult_zless_cancel2:
   12.79 -     "(m$*k $< n$*k) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
   12.80 +     "(m$*k $< n$*k) \<longleftrightarrow> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
   12.81  apply (cut_tac k = "intify (k)" and m = "intify (m)" and n = "intify (n)"
   12.82         in zmult_zless_lemma)
   12.83  apply auto
   12.84  done
   12.85  
   12.86  lemma zmult_zless_cancel1:
   12.87 -     "(k$*m $< k$*n) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
   12.88 +     "(k$*m $< k$*n) \<longleftrightarrow> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
   12.89  by (simp add: zmult_commute [of k] zmult_zless_cancel2)
   12.90  
   12.91  lemma zmult_zle_cancel2:
   12.92 -     "(m$*k $<= n$*k) <-> ((#0 $< k \<longrightarrow> m$<=n) & (k $< #0 \<longrightarrow> n$<=m))"
   12.93 +     "(m$*k $<= n$*k) \<longleftrightarrow> ((#0 $< k \<longrightarrow> m$<=n) & (k $< #0 \<longrightarrow> n$<=m))"
   12.94  by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel2)
   12.95  
   12.96  lemma zmult_zle_cancel1:
   12.97 -     "(k$*m $<= k$*n) <-> ((#0 $< k \<longrightarrow> m$<=n) & (k $< #0 \<longrightarrow> n$<=m))"
   12.98 +     "(k$*m $<= k$*n) \<longleftrightarrow> ((#0 $< k \<longrightarrow> m$<=n) & (k $< #0 \<longrightarrow> n$<=m))"
   12.99  by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel1)
  12.100  
  12.101 -lemma int_eq_iff_zle: "[| m \<in> int; n \<in> int |] ==> m=n <-> (m $<= n & n $<= m)"
  12.102 +lemma int_eq_iff_zle: "[| m \<in> int; n \<in> int |] ==> m=n \<longleftrightarrow> (m $<= n & n $<= m)"
  12.103  apply (blast intro: zle_refl zle_anti_sym)
  12.104  done
  12.105  
  12.106  lemma zmult_cancel2_lemma:
  12.107 -     "[| k \<in> int; m \<in> int; n \<in> int |] ==> (m$*k = n$*k) <-> (k=#0 | m=n)"
  12.108 +     "[| k \<in> int; m \<in> int; n \<in> int |] ==> (m$*k = n$*k) \<longleftrightarrow> (k=#0 | m=n)"
  12.109  apply (simp add: int_eq_iff_zle [of "m$*k"] int_eq_iff_zle [of m])
  12.110  apply (auto simp add: zmult_zle_cancel2 neq_iff_zless)
  12.111  done
  12.112  
  12.113  lemma zmult_cancel2 [simp]:
  12.114 -     "(m$*k = n$*k) <-> (intify(k) = #0 | intify(m) = intify(n))"
  12.115 +     "(m$*k = n$*k) \<longleftrightarrow> (intify(k) = #0 | intify(m) = intify(n))"
  12.116  apply (rule iff_trans)
  12.117  apply (rule_tac [2] zmult_cancel2_lemma)
  12.118  apply auto
  12.119  done
  12.120  
  12.121  lemma zmult_cancel1 [simp]:
  12.122 -     "(k$*m = k$*n) <-> (intify(k) = #0 | intify(m) = intify(n))"
  12.123 +     "(k$*m = k$*n) \<longleftrightarrow> (intify(k) = #0 | intify(m) = intify(n))"
  12.124  by (simp add: zmult_commute [of k] zmult_cancel2)
  12.125  
  12.126  
  12.127 @@ -458,7 +458,7 @@
  12.128  
  12.129  (*FIXME: use intify in integ_of so that we always have @{term"integ_of w \<in> int"}.
  12.130      then this rewrite can work for all constants!!*)
  12.131 -lemma intify_eq_0_iff_zle: "intify(m) = #0 <-> (m $<= #0 & #0 $<= m)"
  12.132 +lemma intify_eq_0_iff_zle: "intify(m) = #0 \<longleftrightarrow> (m $<= #0 & #0 $<= m)"
  12.133  apply (simp (no_asm) add: int_eq_iff_zle)
  12.134  done
  12.135  
  12.136 @@ -484,7 +484,7 @@
  12.137  
  12.138  lemma int_0_less_lemma:
  12.139       "[| x \<in> int; y \<in> int |]
  12.140 -      ==> (#0 $< x $* y) <-> (#0 $< x & #0 $< y | x $< #0 & y $< #0)"
  12.141 +      ==> (#0 $< x $* y) \<longleftrightarrow> (#0 $< x & #0 $< y | x $< #0 & y $< #0)"
  12.142  apply (auto simp add: zle_def not_zless_iff_zle zmult_pos zmult_neg)
  12.143  apply (rule ccontr)
  12.144  apply (rule_tac [2] ccontr)
  12.145 @@ -498,30 +498,30 @@
  12.146  done
  12.147  
  12.148  lemma int_0_less_mult_iff:
  12.149 -     "(#0 $< x $* y) <-> (#0 $< x & #0 $< y | x $< #0 & y $< #0)"
  12.150 +     "(#0 $< x $* y) \<longleftrightarrow> (#0 $< x & #0 $< y | x $< #0 & y $< #0)"
  12.151  apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_less_lemma)
  12.152  apply auto
  12.153  done
  12.154  
  12.155  lemma int_0_le_lemma:
  12.156       "[| x \<in> int; y \<in> int |]
  12.157 -      ==> (#0 $<= x $* y) <-> (#0 $<= x & #0 $<= y | x $<= #0 & y $<= #0)"
  12.158 +      ==> (#0 $<= x $* y) \<longleftrightarrow> (#0 $<= x & #0 $<= y | x $<= #0 & y $<= #0)"
  12.159  by (auto simp add: zle_def not_zless_iff_zle int_0_less_mult_iff)
  12.160  
  12.161  lemma int_0_le_mult_iff:
  12.162 -     "(#0 $<= x $* y) <-> ((#0 $<= x & #0 $<= y) | (x $<= #0 & y $<= #0))"
  12.163 +     "(#0 $<= x $* y) \<longleftrightarrow> ((#0 $<= x & #0 $<= y) | (x $<= #0 & y $<= #0))"
  12.164  apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_le_lemma)
  12.165  apply auto
  12.166  done
  12.167  
  12.168  lemma zmult_less_0_iff:
  12.169 -     "(x $* y $< #0) <-> (#0 $< x & y $< #0 | x $< #0 & #0 $< y)"
  12.170 +     "(x $* y $< #0) \<longleftrightarrow> (#0 $< x & y $< #0 | x $< #0 & #0 $< y)"
  12.171  apply (auto simp add: int_0_le_mult_iff not_zle_iff_zless [THEN iff_sym])
  12.172  apply (auto dest: zless_not_sym simp add: not_zle_iff_zless)
  12.173  done
  12.174  
  12.175  lemma zmult_le_0_iff:
  12.176 -     "(x $* y $<= #0) <-> (#0 $<= x & y $<= #0 | x $<= #0 & #0 $<= y)"
  12.177 +     "(x $* y $<= #0) \<longleftrightarrow> (#0 $<= x & y $<= #0 | x $<= #0 & #0 $<= y)"
  12.178  by (auto dest: zless_not_sym
  12.179           simp add: int_0_less_mult_iff not_zless_iff_zle [THEN iff_sym])
  12.180  
  12.181 @@ -1656,7 +1656,7 @@
  12.182  apply auto
  12.183  done
  12.184  
  12.185 -lemma pos_imp_zdiv_nonneg_iff: "#0 $< b ==> (#0 $<= a zdiv b) <-> (#0 $<= a)"
  12.186 +lemma pos_imp_zdiv_nonneg_iff: "#0 $< b ==> (#0 $<= a zdiv b) \<longleftrightarrow> (#0 $<= a)"
  12.187  apply auto
  12.188  apply (drule_tac [2] zdiv_mono1)
  12.189  apply (auto simp add: neq_iff_zless)
  12.190 @@ -1664,7 +1664,7 @@
  12.191  apply (blast intro: zdiv_neg_pos_less0)
  12.192  done
  12.193  
  12.194 -lemma neg_imp_zdiv_nonneg_iff: "b $< #0 ==> (#0 $<= a zdiv b) <-> (a $<= #0)"
  12.195 +lemma neg_imp_zdiv_nonneg_iff: "b $< #0 ==> (#0 $<= a zdiv b) \<longleftrightarrow> (a $<= #0)"
  12.196  apply (subst zdiv_zminus_zminus [symmetric])
  12.197  apply (rule iff_trans)
  12.198  apply (rule pos_imp_zdiv_nonneg_iff)
  12.199 @@ -1672,13 +1672,13 @@
  12.200  done
  12.201  
  12.202  (*But not (a zdiv b $<= 0 iff a$<=0); consider a=1, b=2 when a zdiv b = 0.*)
  12.203 -lemma pos_imp_zdiv_neg_iff: "#0 $< b ==> (a zdiv b $< #0) <-> (a $< #0)"
  12.204 +lemma pos_imp_zdiv_neg_iff: "#0 $< b ==> (a zdiv b $< #0) \<longleftrightarrow> (a $< #0)"
  12.205  apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym])
  12.206  apply (erule pos_imp_zdiv_nonneg_iff)
  12.207  done
  12.208  
  12.209  (*Again the law fails for $<=: consider a = -1, b = -2 when a zdiv b = 0*)
  12.210 -lemma neg_imp_zdiv_neg_iff: "b $< #0 ==> (a zdiv b $< #0) <-> (#0 $< a)"
  12.211 +lemma neg_imp_zdiv_neg_iff: "b $< #0 ==> (a zdiv b $< #0) \<longleftrightarrow> (#0 $< a)"
  12.212  apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym])
  12.213  apply (erule neg_imp_zdiv_nonneg_iff)
  12.214  done
  12.215 @@ -1710,8 +1710,8 @@
  12.216   done
  12.217  
  12.218  
  12.219 - lemma neg_zdiv_mult_2: "a $<= #0 ==> (#1 $+ #2$*b) zdiv (#2$*a) <-> (b$+#1) zdiv a"
  12.220 - apply (subgoal_tac " (#1 $+ #2$* ($-b-#1)) zdiv (#2 $* ($-a)) <-> ($-b-#1) zdiv ($-a)")
  12.221 + lemma neg_zdiv_mult_2: "a $<= #0 ==> (#1 $+ #2$*b) zdiv (#2$*a) \<longleftrightarrow> (b$+#1) zdiv a"
  12.222 + apply (subgoal_tac " (#1 $+ #2$* ($-b-#1)) zdiv (#2 $* ($-a)) \<longleftrightarrow> ($-b-#1) zdiv ($-a)")
  12.223   apply (rule_tac [2] pos_zdiv_mult_2)
  12.224   apply (auto simp add: zmult_zminus_right)
  12.225   apply (subgoal_tac " (#-1 - (#2 $* b)) = - (#1 $+ (#2 $* b))")
    13.1 --- a/src/ZF/Int_ZF.thy	Tue Mar 06 15:15:49 2012 +0000
    13.2 +++ b/src/ZF/Int_ZF.thy	Tue Mar 06 16:06:52 2012 +0000
    13.3 @@ -107,7 +107,7 @@
    13.4  (** Natural deduction for intrel **)
    13.5  
    13.6  lemma intrel_iff [simp]: 
    13.7 -    "<<x1,y1>,<x2,y2>>: intrel <->  
    13.8 +    "<<x1,y1>,<x2,y2>>: intrel \<longleftrightarrow>  
    13.9       x1\<in>nat & y1\<in>nat & x2\<in>nat & y2\<in>nat & x1#+y2 = x2#+y1"
   13.10  by (simp add: intrel_def)
   13.11  
   13.12 @@ -148,7 +148,7 @@
   13.13  lemma int_of_type [simp,TC]: "$#m \<in> int"
   13.14  by (simp add: int_def quotient_def int_of_def, auto)
   13.15  
   13.16 -lemma int_of_eq [iff]: "($# m = $# n) <-> natify(m)=natify(n)"
   13.17 +lemma int_of_eq [iff]: "($# m = $# n) \<longleftrightarrow> natify(m)=natify(n)"
   13.18  by (simp add: int_of_def)
   13.19  
   13.20  lemma int_of_inject: "[| $#m = $#n;  m\<in>nat;  n\<in>nat |] ==> m=n"
   13.21 @@ -202,16 +202,16 @@
   13.22  
   13.23  (** Orderings **)
   13.24  
   13.25 -lemma zless_intify1 [simp]:"intify(x) $< y <-> x $< y"
   13.26 +lemma zless_intify1 [simp]:"intify(x) $< y \<longleftrightarrow> x $< y"
   13.27  by (simp add: zless_def)
   13.28  
   13.29 -lemma zless_intify2 [simp]:"x $< intify(y) <-> x $< y"
   13.30 +lemma zless_intify2 [simp]:"x $< intify(y) \<longleftrightarrow> x $< y"
   13.31  by (simp add: zless_def)
   13.32  
   13.33 -lemma zle_intify1 [simp]:"intify(x) $<= y <-> x $<= y"
   13.34 +lemma zle_intify1 [simp]:"intify(x) $<= y \<longleftrightarrow> x $<= y"
   13.35  by (simp add: zle_def)
   13.36  
   13.37 -lemma zle_intify2 [simp]:"x $<= intify(y) <-> x $<= y"
   13.38 +lemma zle_intify2 [simp]:"x $<= intify(y) \<longleftrightarrow> x $<= y"
   13.39  by (simp add: zle_def)
   13.40  
   13.41  
   13.42 @@ -268,7 +268,7 @@
   13.43  
   13.44  subsection{*@{term znegative}: the test for negative integers*}
   13.45  
   13.46 -lemma znegative: "[| x\<in>nat; y\<in>nat |] ==> znegative(intrel``{<x,y>}) <-> x<y"
   13.47 +lemma znegative: "[| x\<in>nat; y\<in>nat |] ==> znegative(intrel``{<x,y>}) \<longleftrightarrow> x<y"
   13.48  apply (cases "x<y") 
   13.49  apply (auto simp add: znegative_def not_lt_iff_le)
   13.50  apply (subgoal_tac "y #+ x2 < x #+ y2", force) 
   13.51 @@ -644,7 +644,7 @@
   13.52  lemma zless_not_refl [iff]: "~ (z$<z)"
   13.53  by (auto simp add: zless_def znegative_def int_of_def zdiff_def)
   13.54  
   13.55 -lemma neq_iff_zless: "[| x: int; y: int |] ==> (x \<noteq> y) <-> (x $< y | y $< x)"
   13.56 +lemma neq_iff_zless: "[| x: int; y: int |] ==> (x \<noteq> y) \<longleftrightarrow> (x $< y | y $< x)"
   13.57  by (cut_tac z = x and w = y in zless_linear, auto)
   13.58  
   13.59  lemma zless_imp_intify_neq: "w $< z ==> intify(w) \<noteq> intify(z)"
   13.60 @@ -682,14 +682,14 @@
   13.61  by (cut_tac intify_in_int [THEN zless_succ_zadd_lemma], auto)
   13.62  
   13.63  lemma zless_iff_succ_zadd:
   13.64 -     "w $< z <-> (\<exists>n\<in>nat. w $+ $#(succ(n)) = intify(z))"
   13.65 +     "w $< z \<longleftrightarrow> (\<exists>n\<in>nat. w $+ $#(succ(n)) = intify(z))"
   13.66  apply (rule iffI)
   13.67  apply (erule zless_imp_succ_zadd, auto)
   13.68  apply (rename_tac "n")
   13.69  apply (cut_tac w = w and n = n in zless_succ_zadd, auto)
   13.70  done
   13.71  
   13.72 -lemma zless_int_of [simp]: "[| m\<in>nat; n\<in>nat |] ==> ($#m $< $#n) <-> (m<n)"
   13.73 +lemma zless_int_of [simp]: "[| m\<in>nat; n\<in>nat |] ==> ($#m $< $#n) \<longleftrightarrow> (m<n)"
   13.74  apply (simp add: less_iff_succ_add zless_iff_succ_zadd int_of_add [symmetric])
   13.75  apply (blast intro: sym)
   13.76  done
   13.77 @@ -768,13 +768,13 @@
   13.78  apply (simp add: zless_def zdiff_def zminus_def)
   13.79  done
   13.80  
   13.81 -lemma not_zless_iff_zle: "~ (z $< w) <-> (w $<= z)"
   13.82 +lemma not_zless_iff_zle: "~ (z $< w) \<longleftrightarrow> (w $<= z)"
   13.83  apply (cut_tac z = z and w = w in zless_linear)
   13.84  apply (auto dest: zless_trans simp add: zle_def)
   13.85  apply (auto dest!: zless_imp_intify_neq)
   13.86  done
   13.87  
   13.88 -lemma not_zle_iff_zless: "~ (z $<= w) <-> (w $< z)"
   13.89 +lemma not_zle_iff_zless: "~ (z $<= w) \<longleftrightarrow> (w $< z)"
   13.90  by (simp add: not_zless_iff_zle [THEN iff_sym])
   13.91  
   13.92  
   13.93 @@ -786,32 +786,32 @@
   13.94  lemma zdiff_zdiff_eq2: "x $- (y $- z) = (x $+ z) $- y"
   13.95  by (simp add: zdiff_def zadd_ac)
   13.96  
   13.97 -lemma zdiff_zless_iff: "(x$-y $< z) <-> (x $< z $+ y)"
   13.98 +lemma zdiff_zless_iff: "(x$-y $< z) \<longleftrightarrow> (x $< z $+ y)"
   13.99  by (simp add: zless_def zdiff_def zadd_ac)
  13.100  
  13.101 -lemma zless_zdiff_iff: "(x $< z$-y) <-> (x $+ y $< z)"
  13.102 +lemma zless_zdiff_iff: "(x $< z$-y) \<longleftrightarrow> (x $+ y $< z)"
  13.103  by (simp add: zless_def zdiff_def zadd_ac)
  13.104  
  13.105 -lemma zdiff_eq_iff: "[| x: int; z: int |] ==> (x$-y = z) <-> (x = z $+ y)"
  13.106 +lemma zdiff_eq_iff: "[| x: int; z: int |] ==> (x$-y = z) \<longleftrightarrow> (x = z $+ y)"
  13.107  by (auto simp add: zdiff_def zadd_assoc)
  13.108  
  13.109 -lemma eq_zdiff_iff: "[| x: int; z: int |] ==> (x = z$-y) <-> (x $+ y = z)"
  13.110 +lemma eq_zdiff_iff: "[| x: int; z: int |] ==> (x = z$-y) \<longleftrightarrow> (x $+ y = z)"
  13.111  by (auto simp add: zdiff_def zadd_assoc)
  13.112  
  13.113  lemma zdiff_zle_iff_lemma:
  13.114 -     "[| x: int; z: int |] ==> (x$-y $<= z) <-> (x $<= z $+ y)"
  13.115 +     "[| x: int; z: int |] ==> (x$-y $<= z) \<longleftrightarrow> (x $<= z $+ y)"
  13.116  by (auto simp add: zle_def zdiff_eq_iff zdiff_zless_iff)
  13.117  
  13.118 -lemma zdiff_zle_iff: "(x$-y $<= z) <-> (x $<= z $+ y)"
  13.119 +lemma zdiff_zle_iff: "(x$-y $<= z) \<longleftrightarrow> (x $<= z $+ y)"
  13.120  by (cut_tac zdiff_zle_iff_lemma [OF intify_in_int intify_in_int], simp)
  13.121  
  13.122  lemma zle_zdiff_iff_lemma:
  13.123 -     "[| x: int; z: int |] ==>(x $<= z$-y) <-> (x $+ y $<= z)"
  13.124 +     "[| x: int; z: int |] ==>(x $<= z$-y) \<longleftrightarrow> (x $+ y $<= z)"
  13.125  apply (auto simp add: zle_def zdiff_eq_iff zless_zdiff_iff)
  13.126  apply (auto simp add: zdiff_def zadd_assoc)
  13.127  done
  13.128  
  13.129 -lemma zle_zdiff_iff: "(x $<= z$-y) <-> (x $+ y $<= z)"
  13.130 +lemma zle_zdiff_iff: "(x $<= z$-y) \<longleftrightarrow> (x $+ y $<= z)"
  13.131  by (cut_tac zle_zdiff_iff_lemma [ OF intify_in_int intify_in_int], simp)
  13.132  
  13.133  text{*This list of rewrites simplifies (in)equalities by bringing subtractions
  13.134 @@ -828,41 +828,41 @@
  13.135       of the CancelNumerals Simprocs*}
  13.136  
  13.137  lemma zadd_left_cancel:
  13.138 -     "[| w: int; w': int |] ==> (z $+ w' = z $+ w) <-> (w' = w)"
  13.139 +     "[| w: int; w': int |] ==> (z $+ w' = z $+ w) \<longleftrightarrow> (w' = w)"
  13.140  apply safe
  13.141  apply (drule_tac t = "%x. x $+ ($-z) " in subst_context)
  13.142  apply (simp add: zadd_ac)
  13.143  done
  13.144  
  13.145  lemma zadd_left_cancel_intify [simp]:
  13.146 -     "(z $+ w' = z $+ w) <-> intify(w') = intify(w)"
  13.147 +     "(z $+ w' = z $+ w) \<longleftrightarrow> intify(w') = intify(w)"
  13.148  apply (rule iff_trans)
  13.149  apply (rule_tac [2] zadd_left_cancel, auto)
  13.150  done
  13.151  
  13.152  lemma zadd_right_cancel:
  13.153 -     "[| w: int; w': int |] ==> (w' $+ z = w $+ z) <-> (w' = w)"
  13.154 +     "[| w: int; w': int |] ==> (w' $+ z = w $+ z) \<longleftrightarrow> (w' = w)"
  13.155  apply safe
  13.156  apply (drule_tac t = "%x. x $+ ($-z) " in subst_context)
  13.157  apply (simp add: zadd_ac)
  13.158  done
  13.159  
  13.160  lemma zadd_right_cancel_intify [simp]:
  13.161 -     "(w' $+ z = w $+ z) <-> intify(w') = intify(w)"
  13.162 +     "(w' $+ z = w $+ z) \<longleftrightarrow> intify(w') = intify(w)"
  13.163  apply (rule iff_trans)
  13.164  apply (rule_tac [2] zadd_right_cancel, auto)
  13.165  done
  13.166  
  13.167 -lemma zadd_right_cancel_zless [simp]: "(w' $+ z $< w $+ z) <-> (w' $< w)"
  13.168 +lemma zadd_right_cancel_zless [simp]: "(w' $+ z $< w $+ z) \<longleftrightarrow> (w' $< w)"
  13.169  by (simp add: zdiff_zless_iff [THEN iff_sym] zdiff_def zadd_assoc)
  13.170  
  13.171 -lemma zadd_left_cancel_zless [simp]: "(z $+ w' $< z $+ w) <-> (w' $< w)"
  13.172 +lemma zadd_left_cancel_zless [simp]: "(z $+ w' $< z $+ w) \<longleftrightarrow> (w' $< w)"
  13.173  by (simp add: zadd_commute [of z] zadd_right_cancel_zless)
  13.174  
  13.175 -lemma zadd_right_cancel_zle [simp]: "(w' $+ z $<= w $+ z) <-> w' $<= w"
  13.176 +lemma zadd_right_cancel_zle [simp]: "(w' $+ z $<= w $+ z) \<longleftrightarrow> w' $<= w"
  13.177  by (simp add: zle_def)
  13.178  
  13.179 -lemma zadd_left_cancel_zle [simp]: "(z $+ w' $<= z $+ w) <->  w' $<= w"
  13.180 +lemma zadd_left_cancel_zle [simp]: "(z $+ w' $<= z $+ w) \<longleftrightarrow>  w' $<= w"
  13.181  by (simp add: zadd_commute [of z]  zadd_right_cancel_zle)
  13.182  
  13.183  
  13.184 @@ -887,26 +887,26 @@
  13.185  
  13.186  subsection{*Comparison laws*}
  13.187  
  13.188 -lemma zminus_zless_zminus [simp]: "($- x $< $- y) <-> (y $< x)"
  13.189 +lemma zminus_zless_zminus [simp]: "($- x $< $- y) \<longleftrightarrow> (y $< x)"
  13.190  by (simp add: zless_def zdiff_def zadd_ac)
  13.191  
  13.192 -lemma zminus_zle_zminus [simp]: "($- x $<= $- y) <-> (y $<= x)"
  13.193 +lemma zminus_zle_zminus [simp]: "($- x $<= $- y) \<longleftrightarrow> (y $<= x)"
  13.194  by (simp add: not_zless_iff_zle [THEN iff_sym])
  13.195  
  13.196  subsubsection{*More inequality lemmas*}
  13.197  
  13.198 -lemma equation_zminus: "[| x: int;  y: int |] ==> (x = $- y) <-> (y = $- x)"
  13.199 +lemma equation_zminus: "[| x: int;  y: int |] ==> (x = $- y) \<longleftrightarrow> (y = $- x)"
  13.200  by auto
  13.201  
  13.202 -lemma zminus_equation: "[| x: int;  y: int |] ==> ($- x = y) <-> ($- y = x)"
  13.203 +lemma zminus_equation: "[| x: int;  y: int |] ==> ($- x = y) \<longleftrightarrow> ($- y = x)"
  13.204  by auto
  13.205  
  13.206 -lemma equation_zminus_intify: "(intify(x) = $- y) <-> (intify(y) = $- x)"
  13.207 +lemma equation_zminus_intify: "(intify(x) = $- y) \<longleftrightarrow> (intify(y) = $- x)"
  13.208  apply (cut_tac x = "intify (x) " and y = "intify (y) " in equation_zminus)
  13.209  apply auto
  13.210  done
  13.211  
  13.212 -lemma zminus_equation_intify: "($- x = intify(y)) <-> ($- y = intify(x))"
  13.213 +lemma zminus_equation_intify: "($- x = intify(y)) \<longleftrightarrow> ($- y = intify(x))"
  13.214  apply (cut_tac x = "intify (x) " and y = "intify (y) " in zminus_equation)
  13.215  apply auto
  13.216  done
  13.217 @@ -914,16 +914,16 @@
  13.218  
  13.219  subsubsection{*The next several equations are permutative: watch out!*}
  13.220  
  13.221 -lemma zless_zminus: "(x $< $- y) <-> (y $< $- x)"
  13.222 +lemma zless_zminus: "(x $< $- y) \<longleftrightarrow> (y $< $- x)"
  13.223  by (simp add: zless_def zdiff_def zadd_ac)
  13.224  
  13.225 -lemma zminus_zless: "($- x $< y) <-> ($- y $< x)"
  13.226 +lemma zminus_zless: "($- x $< y) \<longleftrightarrow> ($- y $< x)"
  13.227  by (simp add: zless_def zdiff_def zadd_ac)
  13.228  
  13.229 -lemma zle_zminus: "(x $<= $- y) <-> (y $<= $- x)"
  13.230 +lemma zle_zminus: "(x $<= $- y) \<longleftrightarrow> (y $<= $- x)"
  13.231  by (simp add: not_zless_iff_zle [THEN iff_sym] zminus_zless)
  13.232  
  13.233 -lemma zminus_zle: "($- x $<= y) <-> ($- y $<= x)"
  13.234 +lemma zminus_zle: "($- x $<= y) \<longleftrightarrow> ($- y $<= x)"
  13.235  by (simp add: not_zless_iff_zle [THEN iff_sym] zless_zminus)
  13.236  
  13.237  end
    14.1 --- a/src/ZF/List_ZF.thy	Tue Mar 06 15:15:49 2012 +0000
    14.2 +++ b/src/ZF/List_ZF.thy	Tue Mar 06 16:06:52 2012 +0000
    14.3 @@ -136,11 +136,11 @@
    14.4  (*An elimination rule, for type-checking*)
    14.5  inductive_cases ConsE: "Cons(a,l) \<in> list(A)"
    14.6  
    14.7 -lemma Cons_type_iff [simp]: "Cons(a,l) \<in> list(A) <-> a \<in> A & l \<in> list(A)"
    14.8 +lemma Cons_type_iff [simp]: "Cons(a,l) \<in> list(A) \<longleftrightarrow> a \<in> A & l \<in> list(A)"
    14.9  by (blast elim: ConsE)
   14.10  
   14.11  (*Proving freeness results*)
   14.12 -lemma Cons_iff: "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'"
   14.13 +lemma Cons_iff: "Cons(a,l)=Cons(a',l') \<longleftrightarrow> a=a' & l=l'"
   14.14  by auto
   14.15  
   14.16  lemma Nil_Cons_iff: "~ Nil=Cons(a,l)"
   14.17 @@ -480,7 +480,7 @@
   14.18  apply (auto dest: not_lt_imp_le)
   14.19  done
   14.20  
   14.21 -lemma lt_min_iff: "[| i:nat; j:nat; k:nat |] ==> i<min(j,k) <-> i<j & i<k"
   14.22 +lemma lt_min_iff: "[| i:nat; j:nat; k:nat |] ==> i<min(j,k) \<longleftrightarrow> i<j & i<k"
   14.23  apply (unfold min_def)
   14.24  apply (auto dest!: not_lt_imp_le intro: lt_trans2 lt_trans)
   14.25  done
   14.26 @@ -518,43 +518,43 @@
   14.27  
   14.28  (** length **)
   14.29  
   14.30 -lemma length_is_0_iff [simp]: "xs:list(A) ==> length(xs)=0 <-> xs=Nil"
   14.31 +lemma length_is_0_iff [simp]: "xs:list(A) ==> length(xs)=0 \<longleftrightarrow> xs=Nil"
   14.32  by (erule list.induct, auto)
   14.33  
   14.34 -lemma length_is_0_iff2 [simp]: "xs:list(A) ==> 0 = length(xs) <-> xs=Nil"
   14.35 +lemma length_is_0_iff2 [simp]: "xs:list(A) ==> 0 = length(xs) \<longleftrightarrow> xs=Nil"
   14.36  by (erule list.induct, auto)
   14.37  
   14.38  lemma length_tl [simp]: "xs:list(A) ==> length(tl(xs)) = length(xs) #- 1"
   14.39  by (erule list.induct, auto)
   14.40  
   14.41 -lemma length_greater_0_iff: "xs:list(A) ==> 0<length(xs) <-> xs \<noteq> Nil"
   14.42 +lemma length_greater_0_iff: "xs:list(A) ==> 0<length(xs) \<longleftrightarrow> xs \<noteq> Nil"
   14.43  by (erule list.induct, auto)
   14.44  
   14.45 -lemma length_succ_iff: "xs:list(A) ==> length(xs)=succ(n) <-> (\<exists>y ys. xs=Cons(y, ys) & length(ys)=n)"
   14.46 +lemma length_succ_iff: "xs:list(A) ==> length(xs)=succ(n) \<longleftrightarrow> (\<exists>y ys. xs=Cons(y, ys) & length(ys)=n)"
   14.47  by (erule list.induct, auto)
   14.48  
   14.49  (** more theorems about append **)
   14.50  
   14.51  lemma append_is_Nil_iff [simp]:
   14.52 -     "xs:list(A) ==> (xs@ys = Nil) <-> (xs=Nil & ys = Nil)"
   14.53 +     "xs:list(A) ==> (xs@ys = Nil) \<longleftrightarrow> (xs=Nil & ys = Nil)"
   14.54  by (erule list.induct, auto)
   14.55  
   14.56  lemma append_is_Nil_iff2 [simp]:
   14.57 -     "xs:list(A) ==> (Nil = xs@ys) <-> (xs=Nil & ys = Nil)"
   14.58 +     "xs:list(A) ==> (Nil = xs@ys) \<longleftrightarrow> (xs=Nil & ys = Nil)"
   14.59  by (erule list.induct, auto)
   14.60  
   14.61  lemma append_left_is_self_iff [simp]:
   14.62 -     "xs:list(A) ==> (xs@ys = xs) <-> (ys = Nil)"
   14.63 +     "xs:list(A) ==> (xs@ys = xs) \<longleftrightarrow> (ys = Nil)"
   14.64  by (erule list.induct, auto)
   14.65  
   14.66  lemma append_left_is_self_iff2 [simp]:
   14.67 -     "xs:list(A) ==> (xs = xs@ys) <-> (ys = Nil)"
   14.68 +     "xs:list(A) ==> (xs = xs@ys) \<longleftrightarrow> (ys = Nil)"
   14.69  by (erule list.induct, auto)
   14.70  
   14.71  (*TOO SLOW as a default simprule!*)
   14.72  lemma append_left_is_Nil_iff [rule_format]:
   14.73       "[| xs:list(A); ys:list(A); zs:list(A) |] ==>
   14.74 -   length(ys)=length(zs) \<longrightarrow> (xs@ys=zs <-> (xs=Nil & ys=zs))"
   14.75 +   length(ys)=length(zs) \<longrightarrow> (xs@ys=zs \<longleftrightarrow> (xs=Nil & ys=zs))"
   14.76  apply (erule list.induct)
   14.77  apply (auto simp add: length_app)
   14.78  done
   14.79 @@ -562,14 +562,14 @@
   14.80  (*TOO SLOW as a default simprule!*)
   14.81  lemma append_left_is_Nil_iff2 [rule_format]:
   14.82       "[| xs:list(A); ys:list(A); zs:list(A) |] ==>
   14.83 -   length(ys)=length(zs) \<longrightarrow> (zs=ys@xs <-> (xs=Nil & ys=zs))"
   14.84 +   length(ys)=length(zs) \<longrightarrow> (zs=ys@xs \<longleftrightarrow> (xs=Nil & ys=zs))"
   14.85  apply (erule list.induct)
   14.86  apply (auto simp add: length_app)
   14.87  done
   14.88  
   14.89  lemma append_eq_append_iff [rule_format,simp]:
   14.90       "xs:list(A) ==> \<forall>ys \<in> list(A).
   14.91 -      length(xs)=length(ys) \<longrightarrow> (xs@us = ys@vs) <-> (xs=ys & us=vs)"
   14.92 +      length(xs)=length(ys) \<longrightarrow> (xs@us = ys@vs) \<longleftrightarrow> (xs=ys & us=vs)"
   14.93  apply (erule list.induct)
   14.94  apply (simp (no_asm_simp))
   14.95  apply clarify
   14.96 @@ -589,23 +589,23 @@
   14.97  
   14.98  lemma append_eq_append_iff2 [simp]:
   14.99   "[| xs:list(A); ys:list(A); us:list(A); vs:list(A); length(us)=length(vs) |]
  14.100 -  ==>  xs@us = ys@vs <-> (xs=ys & us=vs)"
  14.101 +  ==>  xs@us = ys@vs \<longleftrightarrow> (xs=ys & us=vs)"
  14.102  apply (rule iffI)
  14.103  apply (rule append_eq_append, auto)
  14.104  done
  14.105  
  14.106  lemma append_self_iff [simp]:
  14.107 -     "[| xs:list(A); ys:list(A); zs:list(A) |] ==> xs@ys=xs@zs <-> ys=zs"
  14.108 +     "[| xs:list(A); ys:list(A); zs:list(A) |] ==> xs@ys=xs@zs \<longleftrightarrow> ys=zs"
  14.109  by simp
  14.110  
  14.111  lemma append_self_iff2 [simp]:
  14.112 -     "[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs <-> ys=zs"
  14.113 +     "[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs \<longleftrightarrow> ys=zs"
  14.114  by simp
  14.115  
  14.116  (* Can also be proved from append_eq_append_iff2,
  14.117  but the proof requires two more hypotheses: x:A and y:A *)
  14.118  lemma append1_eq_iff [rule_format,simp]:
  14.119 -     "xs:list(A) ==> \<forall>ys \<in> list(A). xs@[x] = ys@[y] <-> (xs = ys & x=y)"
  14.120 +     "xs:list(A) ==> \<forall>ys \<in> list(A). xs@[x] = ys@[y] \<longleftrightarrow> (xs = ys & x=y)"
  14.121  apply (erule list.induct)
  14.122   apply clarify
  14.123   apply (erule list.cases)
  14.124 @@ -617,11 +617,11 @@
  14.125  
  14.126  
  14.127  lemma append_right_is_self_iff [simp]:
  14.128 -     "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) <-> (xs=Nil)"
  14.129 +     "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) \<longleftrightarrow> (xs=Nil)"
  14.130  by (simp (no_asm_simp) add: append_left_is_Nil_iff)
  14.131  
  14.132  lemma append_right_is_self_iff2 [simp]:
  14.133 -     "[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) <-> (xs=Nil)"
  14.134 +     "[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) \<longleftrightarrow> (xs=Nil)"
  14.135  apply (rule iffI)
  14.136  apply (drule sym, auto)
  14.137  done
  14.138 @@ -635,14 +635,14 @@
  14.139  by (induct_tac "xs", auto)
  14.140  
  14.141  (** rev **)
  14.142 -lemma rev_is_Nil_iff [simp]: "xs:list(A) ==> (rev(xs) = Nil <-> xs = Nil)"
  14.143 +lemma rev_is_Nil_iff [simp]: "xs:list(A) ==> (rev(xs) = Nil \<longleftrightarrow> xs = Nil)"
  14.144  by (erule list.induct, auto)
  14.145  
  14.146 -lemma Nil_is_rev_iff [simp]: "xs:list(A) ==> (Nil = rev(xs) <-> xs = Nil)"
  14.147 +lemma Nil_is_rev_iff [simp]: "xs:list(A) ==> (Nil = rev(xs) \<longleftrightarrow> xs = Nil)"
  14.148  by (erule list.induct, auto)
  14.149  
  14.150  lemma rev_is_rev_iff [rule_format,simp]:
  14.151 -     "xs:list(A) ==> \<forall>ys \<in> list(A). rev(xs)=rev(ys) <-> xs=ys"
  14.152 +     "xs:list(A) ==> \<forall>ys \<in> list(A). rev(xs)=rev(ys) \<longleftrightarrow> xs=ys"
  14.153  apply (erule list.induct, force, clarify)
  14.154  apply (erule_tac a = ys in list.cases, auto)
  14.155  done
  14.156 @@ -1027,7 +1027,7 @@
  14.157  lemma list_update_same_conv [rule_format]:
  14.158       "xs:list(A) ==>
  14.159        \<forall>i \<in> nat. i < length(xs) \<longrightarrow>
  14.160 -                 (list_update(xs, i, x) = xs) <-> (nth(i, xs) = x)"
  14.161 +                 (list_update(xs, i, x) = xs) \<longleftrightarrow> (nth(i, xs) = x)"
  14.162  apply (induct_tac "xs")
  14.163   apply (simp (no_asm))
  14.164  apply clarify
    15.1 --- a/src/ZF/Nat_ZF.thy	Tue Mar 06 15:15:49 2012 +0000
    15.2 +++ b/src/ZF/Nat_ZF.thy	Tue Mar 06 16:06:52 2012 +0000
    15.3 @@ -123,7 +123,7 @@
    15.4  lemma succ_natD: "succ(i): nat ==> i: nat"
    15.5  by (rule Ord_trans [OF succI1], auto)
    15.6  
    15.7 -lemma nat_succ_iff [iff]: "succ(n): nat <-> n: nat"
    15.8 +lemma nat_succ_iff [iff]: "succ(n): nat \<longleftrightarrow> n: nat"
    15.9  by (blast dest!: succ_natD)
   15.10  
   15.11  lemma nat_le_Limit: "Limit(i) ==> nat \<le> i"
   15.12 @@ -246,7 +246,7 @@
   15.13  by (erule nat_induct, auto)
   15.14  
   15.15  lemma split_nat_case:
   15.16 -  "P(nat_case(a,b,k)) <->
   15.17 +  "P(nat_case(a,b,k)) \<longleftrightarrow>
   15.18     ((k=0 \<longrightarrow> P(a)) & (\<forall>x. k=succ(x) \<longrightarrow> P(b(x))) & (~ quasinat(k) \<longrightarrow> P(0)))"
   15.19  apply (rule nat_cases [of k])
   15.20  apply (auto simp add: non_nat_case)
   15.21 @@ -294,7 +294,7 @@
   15.22  apply (blast intro: lt_trans)
   15.23  done
   15.24  
   15.25 -lemma Le_iff [iff]: "<x,y> \<in> Le <-> x \<le> y & x \<in> nat & y \<in> nat"
   15.26 +lemma Le_iff [iff]: "<x,y> \<in> Le \<longleftrightarrow> x \<le> y & x \<in> nat & y \<in> nat"
   15.27  by (force simp add: Le_def)
   15.28  
   15.29  end
    16.1 --- a/src/ZF/Order.thy	Tue Mar 06 15:15:49 2012 +0000
    16.2 +++ b/src/ZF/Order.thy	Tue Mar 06 16:06:52 2012 +0000
    16.3 @@ -51,7 +51,7 @@
    16.4  definition
    16.5    ord_iso  :: "[i,i,i,i]=>i"            (*Order isomorphisms*)  where
    16.6     "ord_iso(A,r,B,s) ==
    16.7 -              {f: bij(A,B). \<forall>x\<in>A. \<forall>y\<in>A. <x,y>:r <-> <f`x,f`y>:s}"
    16.8 +              {f: bij(A,B). \<forall>x\<in>A. \<forall>y\<in>A. <x,y>:r \<longleftrightarrow> <f`x,f`y>:s}"
    16.9  
   16.10  definition
   16.11    pred     :: "[i,i,i]=>i"              (*Set of predecessors*)  where
   16.12 @@ -107,7 +107,7 @@
   16.13  
   16.14  (** Derived rules for pred(A,x,r) **)
   16.15  
   16.16 -lemma pred_iff: "y \<in> pred(A,x,r) <-> <y,x>:r & y:A"
   16.17 +lemma pred_iff: "y \<in> pred(A,x,r) \<longleftrightarrow> <y,x>:r & y:A"
   16.18  by (unfold pred_def, blast)
   16.19  
   16.20  lemmas predI = conjI [THEN pred_iff [THEN iffD2]]
   16.21 @@ -160,30 +160,30 @@
   16.22  
   16.23  (** Relations restricted to a smaller domain, by Krzysztof Grabczewski **)
   16.24  
   16.25 -lemma irrefl_Int_iff: "irrefl(A,r \<inter> A*A) <-> irrefl(A,r)"
   16.26 +lemma irrefl_Int_iff: "irrefl(A,r \<inter> A*A) \<longleftrightarrow> irrefl(A,r)"
   16.27  by (unfold irrefl_def, blast)
   16.28  
   16.29 -lemma trans_on_Int_iff: "trans[A](r \<inter> A*A) <-> trans[A](r)"
   16.30 +lemma trans_on_Int_iff: "trans[A](r \<inter> A*A) \<longleftrightarrow> trans[A](r)"
   16.31  by (unfold trans_on_def, blast)
   16.32  
   16.33 -lemma part_ord_Int_iff: "part_ord(A,r \<inter> A*A) <-> part_ord(A,r)"
   16.34 +lemma part_ord_Int_iff: "part_ord(A,r \<inter> A*A) \<longleftrightarrow> part_ord(A,r)"
   16.35  apply (unfold part_ord_def)
   16.36  apply (simp add: irrefl_Int_iff trans_on_Int_iff)
   16.37  done
   16.38  
   16.39 -lemma linear_Int_iff: "linear(A,r \<inter> A*A) <-> linear(A,r)"
   16.40 +lemma linear_Int_iff: "linear(A,r \<inter> A*A) \<longleftrightarrow> linear(A,r)"
   16.41  by (unfold linear_def, blast)
   16.42  
   16.43 -lemma tot_ord_Int_iff: "tot_ord(A,r \<inter> A*A) <-> tot_ord(A,r)"
   16.44 +lemma tot_ord_Int_iff: "tot_ord(A,r \<inter> A*A) \<longleftrightarrow> tot_ord(A,r)"
   16.45  apply (unfold tot_ord_def)
   16.46  apply (simp add: part_ord_Int_iff linear_Int_iff)
   16.47  done
   16.48  
   16.49 -lemma wf_on_Int_iff: "wf[A](r \<inter> A*A) <-> wf[A](r)"
   16.50 +lemma wf_on_Int_iff: "wf[A](r \<inter> A*A) \<longleftrightarrow> wf[A](r)"
   16.51  apply (unfold wf_on_def wf_def, fast) (*10 times faster than blast!*)
   16.52  done
   16.53  
   16.54 -lemma well_ord_Int_iff: "well_ord(A,r \<inter> A*A) <-> well_ord(A,r)"
   16.55 +lemma well_ord_Int_iff: "well_ord(A,r \<inter> A*A) \<longleftrightarrow> well_ord(A,r)"
   16.56  apply (unfold well_ord_def)
   16.57  apply (simp add: tot_ord_Int_iff wf_on_Int_iff)
   16.58  done
   16.59 @@ -256,7 +256,7 @@
   16.60  
   16.61  lemma ord_isoI:
   16.62      "[| f: bij(A, B);
   16.63 -        !!x y. [| x:A; y:A |] ==> <x, y> \<in> r <-> <f`x, f`y> \<in> s |]
   16.64 +        !!x y. [| x:A; y:A |] ==> <x, y> \<in> r \<longleftrightarrow> <f`x, f`y> \<in> s |]
   16.65       ==> f: ord_iso(A,r,B,s)"
   16.66  by (simp add: ord_iso_def)
   16.67  
   16.68 @@ -666,7 +666,7 @@
   16.69  
   16.70  lemma subset_vimage_vimage_iff:
   16.71    "[| Preorder(r); A \<subseteq> field(r); B \<subseteq> field(r) |] ==>
   16.72 -  r -`` A \<subseteq> r -`` B <-> (\<forall>a\<in>A. \<exists>b\<in>B. <a, b> \<in> r)"
   16.73 +  r -`` A \<subseteq> r -`` B \<longleftrightarrow> (\<forall>a\<in>A. \<exists>b\<in>B. <a, b> \<in> r)"
   16.74    apply (auto simp: subset_def preorder_on_def refl_def vimage_def image_def)
   16.75     apply blast
   16.76    unfolding trans_on_def
   16.77 @@ -679,12 +679,12 @@
   16.78  
   16.79  lemma subset_vimage1_vimage1_iff:
   16.80    "[| Preorder(r); a \<in> field(r); b \<in> field(r) |] ==>
   16.81 -  r -`` {a} \<subseteq> r -`` {b} <-> <a, b> \<in> r"
   16.82 +  r -`` {a} \<subseteq> r -`` {b} \<longleftrightarrow> <a, b> \<in> r"
   16.83    by (simp add: subset_vimage_vimage_iff)
   16.84  
   16.85  lemma Refl_antisym_eq_Image1_Image1_iff:
   16.86    "[| refl(field(r), r); antisym(r); a \<in> field(r); b \<in> field(r) |] ==>
   16.87 -  r `` {a} = r `` {b} <-> a = b"
   16.88 +  r `` {a} = r `` {b} \<longleftrightarrow> a = b"
   16.89    apply rule
   16.90     apply (frule equality_iffD)
   16.91     apply (drule equality_iffD)
   16.92 @@ -695,13 +695,13 @@
   16.93  
   16.94  lemma Partial_order_eq_Image1_Image1_iff:
   16.95    "[| Partial_order(r); a \<in> field(r); b \<in> field(r) |] ==>
   16.96 -  r `` {a} = r `` {b} <-> a = b"
   16.97 +  r `` {a} = r `` {b} \<longleftrightarrow> a = b"
   16.98    by (simp add: partial_order_on_def preorder_on_def
   16.99      Refl_antisym_eq_Image1_Image1_iff)
  16.100  
  16.101  lemma Refl_antisym_eq_vimage1_vimage1_iff:
  16.102    "[| refl(field(r), r); antisym(r); a \<in> field(r); b \<in> field(r) |] ==>
  16.103 -  r -`` {a} = r -`` {b} <-> a = b"
  16.104 +  r -`` {a} = r -`` {b} \<longleftrightarrow> a = b"
  16.105    apply rule
  16.106     apply (frule equality_iffD)
  16.107     apply (drule equality_iffD)
  16.108 @@ -712,7 +712,7 @@
  16.109  
  16.110  lemma Partial_order_eq_vimage1_vimage1_iff:
  16.111    "[| Partial_order(r); a \<in> field(r); b \<in> field(r) |] ==>
  16.112 -  r -`` {a} = r -`` {b} <-> a = b"
  16.113 +  r -`` {a} = r -`` {b} \<longleftrightarrow> a = b"
  16.114    by (simp add: partial_order_on_def preorder_on_def
  16.115      Refl_antisym_eq_vimage1_vimage1_iff)
  16.116  
    17.1 --- a/src/ZF/OrderArith.thy	Tue Mar 06 15:15:49 2012 +0000
    17.2 +++ b/src/ZF/OrderArith.thy	Tue Mar 06 16:06:52 2012 +0000
    17.3 @@ -39,19 +39,19 @@
    17.4  subsubsection{*Rewrite rules.  Can be used to obtain introduction rules*}
    17.5  
    17.6  lemma radd_Inl_Inr_iff [iff]: 
    17.7 -    "<Inl(a), Inr(b)> \<in> radd(A,r,B,s)  <->  a:A & b:B"
    17.8 +    "<Inl(a), Inr(b)> \<in> radd(A,r,B,s)  \<longleftrightarrow>  a:A & b:B"
    17.9  by (unfold radd_def, blast)
   17.10  
   17.11  lemma radd_Inl_iff [iff]: 
   17.12 -    "<Inl(a'), Inl(a)> \<in> radd(A,r,B,s)  <->  a':A & a:A & <a',a>:r"
   17.13 +    "<Inl(a'), Inl(a)> \<in> radd(A,r,B,s)  \<longleftrightarrow>  a':A & a:A & <a',a>:r"
   17.14  by (unfold radd_def, blast)
   17.15  
   17.16  lemma radd_Inr_iff [iff]: 
   17.17 -    "<Inr(b'), Inr(b)> \<in> radd(A,r,B,s) <->  b':B & b:B & <b',b>:s"
   17.18 +    "<Inr(b'), Inr(b)> \<in> radd(A,r,B,s) \<longleftrightarrow>  b':B & b:B & <b',b>:s"
   17.19  by (unfold radd_def, blast)
   17.20  
   17.21  lemma radd_Inr_Inl_iff [simp]: 
   17.22 -    "<Inr(b), Inl(a)> \<in> radd(A,r,B,s) <-> False"
   17.23 +    "<Inr(b), Inl(a)> \<in> radd(A,r,B,s) \<longleftrightarrow> False"
   17.24  by (unfold radd_def, blast)
   17.25  
   17.26  declare radd_Inr_Inl_iff [THEN iffD1, dest!] 
   17.27 @@ -163,7 +163,7 @@
   17.28  subsubsection{*Rewrite rule.  Can be used to obtain introduction rules*}
   17.29  
   17.30  lemma  rmult_iff [iff]: 
   17.31 -    "<<a',b'>, <a,b>> \<in> rmult(A,r,B,s) <->        
   17.32 +    "<<a',b'>, <a,b>> \<in> rmult(A,r,B,s) \<longleftrightarrow>        
   17.33              (<a',a>: r  & a':A & a:A & b': B & b: B) |   
   17.34              (<b',b>: s  & a'=a & a:A & b': B & b: B)"
   17.35  
   17.36 @@ -307,7 +307,7 @@
   17.37  
   17.38  subsubsection{*Rewrite rule*}
   17.39  
   17.40 -lemma rvimage_iff: "<a,b> \<in> rvimage(A,f,r)  <->  <f`a,f`b>: r & a:A & b:A"
   17.41 +lemma rvimage_iff: "<a,b> \<in> rvimage(A,f,r)  \<longleftrightarrow>  <f`a,f`b>: r & a:A & b:A"
   17.42  by (unfold rvimage_def, blast)
   17.43  
   17.44  subsubsection{*Type checking*}
   17.45 @@ -450,7 +450,7 @@
   17.46  done
   17.47  
   17.48  theorem wf_iff_subset_rvimage:
   17.49 -  "relation(r) ==> wf(r) <-> (\<exists>i f A. Ord(i) & r \<subseteq> rvimage(A, f, Memrel(i)))"
   17.50 +  "relation(r) ==> wf(r) \<longleftrightarrow> (\<exists>i f A. Ord(i) & r \<subseteq> rvimage(A, f, Memrel(i)))"
   17.51  by (blast dest!: relation_field_times_field wf_imp_subset_rvimage
   17.52            intro: wf_rvimage_Ord [THEN wf_subset])
   17.53  
   17.54 @@ -496,7 +496,7 @@
   17.55  lemma wf_measure [iff]: "wf(measure(A,f))"
   17.56  by (simp (no_asm) add: measure_eq_rvimage_Memrel wf_Memrel wf_rvimage)
   17.57  
   17.58 -lemma measure_iff [iff]: "<x,y> \<in> measure(A,f) <-> x:A & y:A & f(x)<f(y)"
   17.59 +lemma measure_iff [iff]: "<x,y> \<in> measure(A,f) \<longleftrightarrow> x:A & y:A & f(x)<f(y)"
   17.60  by (simp (no_asm) add: measure_def)
   17.61  
   17.62  lemma linear_measure: 
    18.1 --- a/src/ZF/OrderType.thy	Tue Mar 06 15:15:49 2012 +0000
    18.2 +++ b/src/ZF/OrderType.thy	Tue Mar 06 16:06:52 2012 +0000
    18.3 @@ -533,7 +533,7 @@
    18.4  apply (blast dest: oadd_lt_mono2 elim: lt_irrefl lt_asym)+
    18.5  done
    18.6  
    18.7 -lemma oadd_lt_iff2: "Ord(j) ==> i++j < i++k <-> j<k"
    18.8 +lemma oadd_lt_iff2: "Ord(j) ==> i++j < i++k \<longleftrightarrow> j<k"
    18.9  by (blast intro!: oadd_lt_mono2 dest!: oadd_lt_cancel2)
   18.10  
   18.11  lemma oadd_inject: "[| i++j = i++k;  Ord(j); Ord(k) |] ==> j=k"
   18.12 @@ -607,13 +607,13 @@
   18.13                   Union_eq_UN [symmetric] Limit_Union_eq)
   18.14  done
   18.15  
   18.16 -lemma oadd_eq_0_iff: "[| Ord(i); Ord(j) |] ==> (i ++ j) = 0 <-> i=0 & j=0"
   18.17 +lemma oadd_eq_0_iff: "[| Ord(i); Ord(j) |] ==> (i ++ j) = 0 \<longleftrightarrow> i=0 & j=0"
   18.18  apply (erule trans_induct3 [of j])
   18.19  apply (simp_all add: oadd_Limit)
   18.20  apply (simp add: Union_empty_iff Limit_def lt_def, blast)
   18.21  done
   18.22  
   18.23 -lemma oadd_eq_lt_iff: "[| Ord(i); Ord(j) |] ==> 0 < (i ++ j) <-> 0<i | 0<j"
   18.24 +lemma oadd_eq_lt_iff: "[| Ord(i); Ord(j) |] ==> 0 < (i ++ j) \<longleftrightarrow> 0<i | 0<j"
   18.25  by (simp add: Ord_0_lt_iff [symmetric] oadd_eq_0_iff)
   18.26  
   18.27  lemma oadd_LimitI: "[| Ord(i); Limit(j) |] ==> Limit(i ++ j)"
   18.28 @@ -661,7 +661,7 @@
   18.29  lemma oadd_le_mono: "[| i' \<le> i;  j' \<le> j |] ==> i'++j' \<le> i++j"
   18.30  by (simp del: oadd_succ add: oadd_succ [symmetric] le_Ord2 oadd_lt_mono)
   18.31  
   18.32 -lemma oadd_le_iff2: "[| Ord(j); Ord(k) |] ==> i++j \<le> i++k <-> j \<le> k"
   18.33 +lemma oadd_le_iff2: "[| Ord(j); Ord(k) |] ==> i++j \<le> i++k \<longleftrightarrow> j \<le> k"
   18.34  by (simp del: oadd_succ add: oadd_lt_iff2 oadd_succ [symmetric] Ord_succ)
   18.35  
   18.36  lemma oadd_lt_self: "[| Ord(i);  0<j |] ==> i < i++j"
    19.1 --- a/src/ZF/Perm.thy	Tue Mar 06 15:15:49 2012 +0000
    19.2 +++ b/src/ZF/Perm.thy	Tue Mar 06 16:06:52 2012 +0000
    19.3 @@ -15,7 +15,7 @@
    19.4  definition
    19.5    (*composition of relations and functions; NOT Suppes's relative product*)
    19.6    comp     :: "[i,i]=>i"      (infixr "O" 60)  where
    19.7 -    "r O s == {xz \<in> domain(s)*range(r) . 
    19.8 +    "r O s == {xz \<in> domain(s)*range(r) .
    19.9                 \<exists>x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
   19.10  
   19.11  definition
   19.12 @@ -58,17 +58,17 @@
   19.13  
   19.14  text{* A function with a right inverse is a surjection *}
   19.15  
   19.16 -lemma f_imp_surjective: 
   19.17 +lemma f_imp_surjective:
   19.18      "[| f: A->B;  !!y. y:B ==> d(y): A;  !!y. y:B ==> f`d(y) = y |]
   19.19       ==> f: surj(A,B)"
   19.20    by (simp add: surj_def, blast)
   19.21  
   19.22 -lemma lam_surjective: 
   19.23 -    "[| !!x. x:A ==> c(x): B;            
   19.24 -        !!y. y:B ==> d(y): A;            
   19.25 -        !!y. y:B ==> c(d(y)) = y         
   19.26 +lemma lam_surjective:
   19.27 +    "[| !!x. x:A ==> c(x): B;
   19.28 +        !!y. y:B ==> d(y): A;
   19.29 +        !!y. y:B ==> c(d(y)) = y
   19.30       |] ==> (\<lambda>x\<in>A. c(x)) \<in> surj(A,B)"
   19.31 -apply (rule_tac d = d in f_imp_surjective) 
   19.32 +apply (rule_tac d = d in f_imp_surjective)
   19.33  apply (simp_all add: lam_type)
   19.34  done
   19.35  
   19.36 @@ -76,7 +76,7 @@
   19.37  lemma cantor_surj: "f \<notin> surj(A,Pow(A))"
   19.38  apply (unfold surj_def, safe)
   19.39  apply (cut_tac cantor)
   19.40 -apply (best del: subsetI) 
   19.41 +apply (best del: subsetI)
   19.42  done
   19.43  
   19.44  
   19.45 @@ -88,7 +88,7 @@
   19.46  done
   19.47  
   19.48  text{*Good for dealing with sets of pairs, but a bit ugly in use [used in AC]*}
   19.49 -lemma inj_equality: 
   19.50 +lemma inj_equality:
   19.51      "[| <a,b>:f;  <c,b>:f;  f: inj(A,B) |] ==> a=c"
   19.52  apply (unfold inj_def)
   19.53  apply (blast dest: Pair_mem_PiD)
   19.54 @@ -104,8 +104,8 @@
   19.55  apply (blast intro: subst_context [THEN box_equals])
   19.56  done
   19.57  
   19.58 -lemma lam_injective: 
   19.59 -    "[| !!x. x:A ==> c(x): B;            
   19.60 +lemma lam_injective:
   19.61 +    "[| !!x. x:A ==> c(x): B;
   19.62          !!x. x:A ==> d(c(x)) = x |]
   19.63       ==> (\<lambda>x\<in>A. c(x)) \<in> inj(A,B)"
   19.64  apply (rule_tac d = d in f_imp_injective)
   19.65 @@ -127,17 +127,17 @@
   19.66  text{* f: bij(A,B) ==> f: A->B *}
   19.67  lemmas bij_is_fun = bij_is_inj [THEN inj_is_fun]
   19.68  
   19.69 -lemma lam_bijective: 
   19.70 -    "[| !!x. x:A ==> c(x): B;            
   19.71 -        !!y. y:B ==> d(y): A;            
   19.72 -        !!x. x:A ==> d(c(x)) = x;        
   19.73 -        !!y. y:B ==> c(d(y)) = y         
   19.74 +lemma lam_bijective:
   19.75 +    "[| !!x. x:A ==> c(x): B;
   19.76 +        !!y. y:B ==> d(y): A;
   19.77 +        !!x. x:A ==> d(c(x)) = x;
   19.78 +        !!y. y:B ==> c(d(y)) = y
   19.79       |] ==> (\<lambda>x\<in>A. c(x)) \<in> bij(A,B)"
   19.80  apply (unfold bij_def)
   19.81  apply (blast intro!: lam_injective lam_surjective)
   19.82  done
   19.83  
   19.84 -lemma RepFun_bijective: "(\<forall>y\<in>x. EX! y'. f(y') = f(y))   
   19.85 +lemma RepFun_bijective: "(\<forall>y\<in>x. EX! y'. f(y') = f(y))
   19.86        ==> (\<lambda>z\<in>{f(y). y:x}. THE y. f(y) = z) \<in> bij({f(y). y:x}, x)"
   19.87  apply (rule_tac d = f in lam_bijective)
   19.88  apply (auto simp add: the_equality2)
   19.89 @@ -171,7 +171,7 @@
   19.90  
   19.91  lemma id_subset_inj: "A<=B ==> id(A): inj(A,B)"
   19.92  apply (simp add: inj_def id_def)
   19.93 -apply (blast intro: lam_type) 
   19.94 +apply (blast intro: lam_type)
   19.95  done
   19.96  
   19.97  lemmas id_inj = subset_refl [THEN id_subset_inj]
   19.98 @@ -186,13 +186,13 @@
   19.99  apply (blast intro: id_inj id_surj)
  19.100  done
  19.101  
  19.102 -lemma subset_iff_id: "A \<subseteq> B <-> id(A) \<in> A->B"
  19.103 +lemma subset_iff_id: "A \<subseteq> B \<longleftrightarrow> id(A) \<in> A->B"
  19.104  apply (unfold id_def)
  19.105  apply (force intro!: lam_type dest: apply_type)
  19.106  done
  19.107  
  19.108  text{*@{term id} as the identity relation*}
  19.109 -lemma id_iff [simp]: "<x,y> \<in> id(A) <-> x=y & y \<in> A"
  19.110 +lemma id_iff [simp]: "<x,y> \<in> id(A) \<longleftrightarrow> x=y & y \<in> A"
  19.111  by auto
  19.112  
  19.113  
  19.114 @@ -224,7 +224,7 @@
  19.115  
  19.116  lemma right_inverse_lemma:
  19.117       "[| f: A->B;  converse(f): C->A;  b: C |] ==> f`(converse(f)`b) = b"
  19.118 -by (rule apply_Pair [THEN converseD [THEN apply_equality]], auto) 
  19.119 +by (rule apply_Pair [THEN converseD [THEN apply_equality]], auto)
  19.120  
  19.121  (*Should the premises be f:surj(A,B), b:B for symmetry with left_inverse?
  19.122    No: they would not imply that converse(f) was a function! *)
  19.123 @@ -239,14 +239,14 @@
  19.124  
  19.125  lemma inj_converse_inj: "f: inj(A,B) ==> converse(f): inj(range(f), A)"
  19.126  apply (rule f_imp_injective)
  19.127 -apply (erule inj_converse_fun, clarify) 
  19.128 +apply (erule inj_converse_fun, clarify)
  19.129  apply (rule right_inverse)
  19.130   apply assumption
  19.131 -apply blast 
  19.132 +apply blast
  19.133  done
  19.134  
  19.135  lemma inj_converse_surj: "f: inj(A,B) ==> converse(f): surj(range(f), A)"
  19.136 -by (blast intro: f_imp_surjective inj_converse_fun left_inverse inj_is_fun 
  19.137 +by (blast intro: f_imp_surjective inj_converse_fun left_inverse inj_is_fun
  19.138                   range_of_fun [THEN apply_type])
  19.139  
  19.140  text{*Adding this as an intro! rule seems to cause looping*}
  19.141 @@ -264,17 +264,17 @@
  19.142  lemma compI [intro]: "[| <a,b>:s; <b,c>:r |] ==> <a,c> \<in> r O s"
  19.143  by (unfold comp_def, blast)
  19.144  
  19.145 -lemma compE [elim!]: 
  19.146 -    "[| xz \<in> r O s;   
  19.147 +lemma compE [elim!]:
  19.148 +    "[| xz \<in> r O s;
  19.149          !!x y z. [| xz=<x,z>;  <x,y>:s;  <y,z>:r |] ==> P |]
  19.150       ==> P"
  19.151  by (unfold comp_def, blast)
  19.152  
  19.153 -lemma compEpair: 
  19.154 -    "[| <a,c> \<in> r O s;   
  19.155 +lemma compEpair:
  19.156 +    "[| <a,c> \<in> r O s;
  19.157          !!y. [| <a,y>:s;  <y,c>:r |] ==> P |]
  19.158       ==> P"
  19.159 -by (erule compE, simp)  
  19.160 +by (erule compE, simp)
  19.161  
  19.162  lemma converse_comp: "converse(R O S) = converse(S) O converse(R)"
  19.163  by blast
  19.164 @@ -302,7 +302,7 @@
  19.165    by (auto simp add: inj_def Pi_iff function_def)
  19.166  
  19.167  lemma inj_bij_range: "f: inj(A,B) ==> f \<in> bij(A,range(f))"
  19.168 -  by (auto simp add: bij_def intro: inj_inj_range inj_is_fun fun_is_surj) 
  19.169 +  by (auto simp add: bij_def intro: inj_inj_range inj_is_fun fun_is_surj)
  19.170  
  19.171  
  19.172  subsection{*Other Results*}
  19.173 @@ -319,7 +319,7 @@
  19.174  by blast
  19.175  
  19.176  (*left identity of composition; provable inclusions are
  19.177 -        id(A) O r \<subseteq> r       
  19.178 +        id(A) O r \<subseteq> r
  19.179    and   [| r<=A*B; B<=C |] ==> r \<subseteq> id(C) O r *)
  19.180  lemma left_comp_id: "r<=A*B ==> id(B) O r = r"
  19.181  by blast
  19.182 @@ -339,44 +339,44 @@
  19.183  text{*Don't think the premises can be weakened much*}
  19.184  lemma comp_fun: "[| g: A->B;  f: B->C |] ==> (f O g) \<in> A->C"
  19.185  apply (auto simp add: Pi_def comp_function Pow_iff comp_rel)
  19.186 -apply (subst range_rel_subset [THEN domain_comp_eq], auto) 
  19.187 +apply (subst range_rel_subset [THEN domain_comp_eq], auto)
  19.188  done
  19.189  
  19.190  (*Thanks to the new definition of "apply", the premise f: B->C is gone!*)
  19.191  lemma comp_fun_apply [simp]:
  19.192       "[| g: A->B;  a:A |] ==> (f O g)`a = f`(g`a)"
  19.193 -apply (frule apply_Pair, assumption) 
  19.194 +apply (frule apply_Pair, assumption)
  19.195  apply (simp add: apply_def image_comp)
  19.196 -apply (blast dest: apply_equality) 
  19.197 +apply (blast dest: apply_equality)
  19.198  done
  19.199  
  19.200  text{*Simplifies compositions of lambda-abstractions*}
  19.201 -lemma comp_lam: 
  19.202 +lemma comp_lam:
  19.203      "[| !!x. x:A ==> b(x): B |]
  19.204       ==> (\<lambda>y\<in>B. c(y)) O (\<lambda>x\<in>A. b(x)) = (\<lambda>x\<in>A. c(b(x)))"
  19.205 -apply (subgoal_tac "(\<lambda>x\<in>A. b(x)) \<in> A -> B") 
  19.206 +apply (subgoal_tac "(\<lambda>x\<in>A. b(x)) \<in> A -> B")
  19.207   apply (rule fun_extension)
  19.208     apply (blast intro: comp_fun lam_funtype)
  19.209    apply (rule lam_funtype)
  19.210 - apply simp 
  19.211 -apply (simp add: lam_type) 
  19.212 + apply simp
  19.213 +apply (simp add: lam_type)
  19.214  done
  19.215  
  19.216  lemma comp_inj:
  19.217       "[| g: inj(A,B);  f: inj(B,C) |] ==> (f O g) \<in> inj(A,C)"
  19.218 -apply (frule inj_is_fun [of g]) 
  19.219 -apply (frule inj_is_fun [of f]) 
  19.220 +apply (frule inj_is_fun [of g])
  19.221 +apply (frule inj_is_fun [of f])
  19.222  apply (rule_tac d = "%y. converse (g) ` (converse (f) ` y)" in f_imp_injective)
  19.223 - apply (blast intro: comp_fun, simp)  
  19.224 + apply (blast intro: comp_fun, simp)
  19.225  done
  19.226  
  19.227 -lemma comp_surj: 
  19.228 +lemma comp_surj:
  19.229      "[| g: surj(A,B);  f: surj(B,C) |] ==> (f O g) \<in> surj(A,C)"
  19.230  apply (unfold surj_def)
  19.231  apply (blast intro!: comp_fun comp_fun_apply)
  19.232  done
  19.233  
  19.234 -lemma comp_bij: 
  19.235 +lemma comp_bij:
  19.236      "[| g: bij(A,B);  f: bij(B,C) |] ==> (f O g) \<in> bij(A,C)"
  19.237  apply (unfold bij_def)
  19.238  apply (blast intro: comp_inj comp_surj)
  19.239 @@ -386,14 +386,14 @@
  19.240  subsection{*Dual Properties of @{term inj} and @{term surj}*}
  19.241  
  19.242  text{*Useful for proofs from
  19.243 -    D Pastre.  Automatic theorem proving in set theory. 
  19.244 +    D Pastre.  Automatic theorem proving in set theory.
  19.245      Artificial Intelligence, 10:1--27, 1978.*}
  19.246  
  19.247 -lemma comp_mem_injD1: 
  19.248 +lemma comp_mem_injD1:
  19.249      "[| (f O g): inj(A,C);  g: A->B;  f: B->C |] ==> g: inj(A,B)"
  19.250 -by (unfold inj_def, force) 
  19.251 +by (unfold inj_def, force)
  19.252  
  19.253 -lemma comp_mem_injD2: 
  19.254 +lemma comp_mem_injD2:
  19.255      "[| (f O g): inj(A,C);  g: surj(A,B);  f: B->C |] ==> f: inj(B,C)"
  19.256  apply (unfold inj_def surj_def, safe)
  19.257  apply (rule_tac x1 = x in bspec [THEN bexE])
  19.258 @@ -403,17 +403,17 @@
  19.259  apply (simp (no_asm_simp))
  19.260  done
  19.261  
  19.262 -lemma comp_mem_surjD1: 
  19.263 +lemma comp_mem_surjD1:
  19.264      "[| (f O g): surj(A,C);  g: A->B;  f: B->C |] ==> f: surj(B,C)"
  19.265  apply (unfold surj_def)
  19.266  apply (blast intro!: comp_fun_apply [symmetric] apply_funtype)
  19.267  done
  19.268  
  19.269  
  19.270 -lemma comp_mem_surjD2: 
  19.271 +lemma comp_mem_surjD2:
  19.272      "[| (f O g): surj(A,C);  g: A->B;  f: inj(B,C) |] ==> g: surj(A,B)"
  19.273  apply (unfold inj_def surj_def, safe)
  19.274 -apply (drule_tac x = "f`y" in bspec, auto)  
  19.275 +apply (drule_tac x = "f`y" in bspec, auto)
  19.276  apply (blast intro: apply_funtype)
  19.277  done
  19.278  
  19.279 @@ -422,16 +422,16 @@
  19.280  text{*left inverse of composition; one inclusion is
  19.281          @{term "f: A->B ==> id(A) \<subseteq> converse(f) O f"} *}
  19.282  lemma left_comp_inverse: "f: inj(A,B) ==> converse(f) O f = id(A)"
  19.283 -apply (unfold inj_def, clarify) 
  19.284 -apply (rule equalityI) 
  19.285 - apply (auto simp add: apply_iff, blast)  
  19.286 +apply (unfold inj_def, clarify)
  19.287 +apply (rule equalityI)
  19.288 + apply (auto simp add: apply_iff, blast)
  19.289  done
  19.290  
  19.291  text{*right inverse of composition; one inclusion is
  19.292                  @{term "f: A->B ==> f O converse(f) \<subseteq> id(B)"} *}
  19.293 -lemma right_comp_inverse: 
  19.294 +lemma right_comp_inverse:
  19.295      "f: surj(A,B) ==> f O converse(f) = id(B)"
  19.296 -apply (simp add: surj_def, clarify) 
  19.297 +apply (simp add: surj_def, clarify)
  19.298  apply (rule equalityI)
  19.299  apply (best elim: domain_type range_type dest: apply_equality2)
  19.300  apply (blast intro: apply_Pair)
  19.301 @@ -440,8 +440,8 @@
  19.302  
  19.303  subsubsection{*Proving that a Function is a Bijection*}
  19.304  
  19.305 -lemma comp_eq_id_iff: 
  19.306 -    "[| f: A->B;  g: B->A |] ==> f O g = id(B) <-> (\<forall>y\<in>B. f`(g`y)=y)"
  19.307 +lemma comp_eq_id_iff:
  19.308 +    "[| f: A->B;  g: B->A |] ==> f O g = id(B) \<longleftrightarrow> (\<forall>y\<in>B. f`(g`y)=y)"
  19.309  apply (unfold id_def, safe)
  19.310   apply (drule_tac t = "%h. h`y " in subst_context)
  19.311   apply simp
  19.312 @@ -450,7 +450,7 @@
  19.313   apply auto
  19.314  done
  19.315  
  19.316 -lemma fg_imp_bijective: 
  19.317 +lemma fg_imp_bijective:
  19.318      "[| f: A->B;  g: B->A;  f O g = id(B);  g O f = id(A) |] ==> f \<in> bij(A,B)"
  19.319  apply (unfold bij_def)
  19.320  apply (simp add: comp_eq_id_iff)
  19.321 @@ -462,7 +462,7 @@
  19.322  
  19.323  lemma invertible_imp_bijective:
  19.324       "[| converse(f): B->A;  f: A->B |] ==> f \<in> bij(A,B)"
  19.325 -by (simp add: fg_imp_bijective comp_eq_id_iff 
  19.326 +by (simp add: fg_imp_bijective comp_eq_id_iff
  19.327                left_inverse_lemma right_inverse_lemma)
  19.328  
  19.329  subsubsection{*Unions of Functions*}
  19.330 @@ -471,25 +471,25 @@
  19.331  
  19.332  text{*Theorem by KG, proof by LCP*}
  19.333  lemma inj_disjoint_Un:
  19.334 -     "[| f: inj(A,B);  g: inj(C,D);  B \<inter> D = 0 |]  
  19.335 +     "[| f: inj(A,B);  g: inj(C,D);  B \<inter> D = 0 |]
  19.336        ==> (\<lambda>a\<in>A \<union> C. if a:A then f`a else g`a) \<in> inj(A \<union> C, B \<union> D)"
  19.337 -apply (rule_tac d = "%z. if z:B then converse (f) `z else converse (g) `z" 
  19.338 +apply (rule_tac d = "%z. if z:B then converse (f) `z else converse (g) `z"
  19.339         in lam_injective)
  19.340  apply (auto simp add: inj_is_fun [THEN apply_type])
  19.341  done
  19.342  
  19.343 -lemma surj_disjoint_Un: 
  19.344 -    "[| f: surj(A,B);  g: surj(C,D);  A \<inter> C = 0 |]   
  19.345 +lemma surj_disjoint_Un:
  19.346 +    "[| f: surj(A,B);  g: surj(C,D);  A \<inter> C = 0 |]
  19.347       ==> (f \<union> g) \<in> surj(A \<union> C, B \<union> D)"
  19.348 -apply (simp add: surj_def fun_disjoint_Un) 
  19.349 -apply (blast dest!: domain_of_fun 
  19.350 +apply (simp add: surj_def fun_disjoint_Un)
  19.351 +apply (blast dest!: domain_of_fun
  19.352               intro!: fun_disjoint_apply1 fun_disjoint_apply2)
  19.353  done
  19.354  
  19.355  text{*A simple, high-level proof; the version for injections follows from it,
  19.356 -  using  @term{f:inj(A,B) <-> f:bij(A,range(f))}  *}
  19.357 +  using  @{term "f:inj(A,B) \<longleftrightarrow> f:bij(A,range(f))"}  *}
  19.358  lemma bij_disjoint_Un:
  19.359 -     "[| f: bij(A,B);  g: bij(C,D);  A \<inter> C = 0;  B \<inter> D = 0 |]  
  19.360 +     "[| f: bij(A,B);  g: bij(C,D);  A \<inter> C = 0;  B \<inter> D = 0 |]
  19.361        ==> (f \<union> g) \<in> bij(A \<union> C, B \<union> D)"
  19.362  apply (rule invertible_imp_bijective)
  19.363  apply (subst converse_Un)
  19.364 @@ -501,25 +501,25 @@
  19.365  
  19.366  lemma surj_image:
  19.367      "f: Pi(A,B) ==> f: surj(A, f``A)"
  19.368 -apply (simp add: surj_def) 
  19.369 -apply (blast intro: apply_equality apply_Pair Pi_type) 
  19.370 +apply (simp add: surj_def)
  19.371 +apply (blast intro: apply_equality apply_Pair Pi_type)
  19.372  done
  19.373  
  19.374  lemma restrict_image [simp]: "restrict(f,A) `` B = f `` (A \<inter> B)"
  19.375  by (auto simp add: restrict_def)
  19.376  
  19.377 -lemma restrict_inj: 
  19.378 +lemma restrict_inj:
  19.379      "[| f: inj(A,B);  C<=A |] ==> restrict(f,C): inj(C,B)"
  19.380  apply (unfold inj_def)
  19.381 -apply (safe elim!: restrict_type2, auto) 
  19.382 +apply (safe elim!: restrict_type2, auto)
  19.383  done
  19.384  
  19.385  lemma restrict_surj: "[| f: Pi(A,B);  C<=A |] ==> restrict(f,C): surj(C, f``C)"
  19.386  apply (insert restrict_type2 [THEN surj_image])
  19.387 -apply (simp add: restrict_image) 
  19.388 +apply (simp add: restrict_image)
  19.389  done
  19.390  
  19.391 -lemma restrict_bij: 
  19.392 +lemma restrict_bij:
  19.393      "[| f: inj(A,B);  C<=A |] ==> restrict(f,C): bij(C, f``C)"
  19.394  apply (simp add: inj_def bij_def)
  19.395  apply (blast intro: restrict_surj surj_is_fun)
  19.396 @@ -541,8 +541,8 @@
  19.397  done
  19.398  
  19.399  
  19.400 -lemma inj_extend: 
  19.401 -    "[| f: inj(A,B);  a\<notin>A;  b\<notin>B |]  
  19.402 +lemma inj_extend:
  19.403 +    "[| f: inj(A,B);  a\<notin>A;  b\<notin>B |]
  19.404       ==> cons(<a,b>,f) \<in> inj(cons(a,A), cons(b,B))"
  19.405  apply (unfold inj_def)
  19.406  apply (force intro: apply_type  simp add: fun_extend)
    20.1 --- a/src/ZF/QPair.thy	Tue Mar 06 15:15:49 2012 +0000
    20.2 +++ b/src/ZF/QPair.thy	Tue Mar 06 16:06:52 2012 +0000
    20.3 @@ -77,7 +77,7 @@
    20.4  lemma QPair_empty [simp]: "<0;0> = 0"
    20.5  by (simp add: QPair_def)
    20.6  
    20.7 -lemma QPair_iff [simp]: "<a;b> = <c;d> <-> a=c & b=d"
    20.8 +lemma QPair_iff [simp]: "<a;b> = <c;d> \<longleftrightarrow> a=c & b=d"
    20.9  apply (simp add: QPair_def)
   20.10  apply (rule sum_equal_iff)
   20.11  done
   20.12 @@ -160,7 +160,7 @@
   20.13  by auto 
   20.14  
   20.15  lemma expand_qsplit: 
   20.16 - "u: A<*>B ==> R(qsplit(c,u)) <-> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x;y> \<longrightarrow> R(c(x,y)))"
   20.17 + "u: A<*>B ==> R(qsplit(c,u)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x;y> \<longrightarrow> R(c(x,y)))"
   20.18  apply (simp add: qsplit_def, auto)
   20.19  done
   20.20  
   20.21 @@ -232,16 +232,16 @@
   20.22  
   20.23  (** Injection and freeness equivalences, for rewriting **)
   20.24  
   20.25 -lemma QInl_iff [iff]: "QInl(a)=QInl(b) <-> a=b"
   20.26 +lemma QInl_iff [iff]: "QInl(a)=QInl(b) \<longleftrightarrow> a=b"
   20.27  by (simp add: qsum_defs )
   20.28  
   20.29 -lemma QInr_iff [iff]: "QInr(a)=QInr(b) <-> a=b"
   20.30 +lemma QInr_iff [iff]: "QInr(a)=QInr(b) \<longleftrightarrow> a=b"
   20.31  by (simp add: qsum_defs )
   20.32  
   20.33 -lemma QInl_QInr_iff [simp]: "QInl(a)=QInr(b) <-> False"
   20.34 +lemma QInl_QInr_iff [simp]: "QInl(a)=QInr(b) \<longleftrightarrow> False"
   20.35  by (simp add: qsum_defs )
   20.36  
   20.37 -lemma QInr_QInl_iff [simp]: "QInr(b)=QInl(a) <-> False"
   20.38 +lemma QInr_QInl_iff [simp]: "QInr(b)=QInl(a) \<longleftrightarrow> False"
   20.39  by (simp add: qsum_defs )
   20.40  
   20.41  lemma qsum_empty [simp]: "0<+>0 = 0"
   20.42 @@ -263,13 +263,13 @@
   20.43  (** <+> is itself injective... who cares?? **)
   20.44  
   20.45  lemma qsum_iff:
   20.46 -     "u: A <+> B <-> (\<exists>x. x:A & u=QInl(x)) | (\<exists>y. y:B & u=QInr(y))"
   20.47 +     "u: A <+> B \<longleftrightarrow> (\<exists>x. x:A & u=QInl(x)) | (\<exists>y. y:B & u=QInr(y))"
   20.48  by blast
   20.49  
   20.50 -lemma qsum_subset_iff: "A <+> B \<subseteq> C <+> D <-> A<=C & B<=D"
   20.51 +lemma qsum_subset_iff: "A <+> B \<subseteq> C <+> D \<longleftrightarrow> A<=C & B<=D"
   20.52  by blast
   20.53  
   20.54 -lemma qsum_equal_iff: "A <+> B = C <+> D <-> A=C & B=D"
   20.55 +lemma qsum_equal_iff: "A <+> B = C <+> D \<longleftrightarrow> A=C & B=D"
   20.56  apply (simp (no_asm) add: extension qsum_subset_iff)
   20.57  apply blast
   20.58  done
    21.1 --- a/src/ZF/QUniv.thy	Tue Mar 06 15:15:49 2012 +0000
    21.2 +++ b/src/ZF/QUniv.thy	Tue Mar 06 16:06:52 2012 +0000
    21.3 @@ -130,7 +130,7 @@
    21.4  
    21.5  lemmas quniv_QPair_E = quniv_QPair_D [THEN conjE]
    21.6  
    21.7 -lemma quniv_QPair_iff: "<a;b> \<in> quniv(A) <-> a: quniv(A) & b: quniv(A)"
    21.8 +lemma quniv_QPair_iff: "<a;b> \<in> quniv(A) \<longleftrightarrow> a: quniv(A) & b: quniv(A)"
    21.9  by (blast intro: QPair_in_quniv dest: quniv_QPair_D)
   21.10  
   21.11  
    22.1 --- a/src/ZF/Sum.thy	Tue Mar 06 15:15:49 2012 +0000
    22.2 +++ b/src/ZF/Sum.thy	Tue Mar 06 16:06:52 2012 +0000
    22.3 @@ -28,7 +28,7 @@
    22.4  subsection{*Rules for the @{term Part} Primitive*}
    22.5  
    22.6  lemma Part_iff: 
    22.7 -    "a \<in> Part(A,h) <-> a:A & (\<exists>y. a=h(y))"
    22.8 +    "a \<in> Part(A,h) \<longleftrightarrow> a:A & (\<exists>y. a=h(y))"
    22.9  apply (unfold Part_def)
   22.10  apply (rule separation)
   22.11  done
   22.12 @@ -77,16 +77,16 @@
   22.13  
   22.14  (** Injection and freeness equivalences, for rewriting **)
   22.15  
   22.16 -lemma Inl_iff [iff]: "Inl(a)=Inl(b) <-> a=b"
   22.17 +lemma Inl_iff [iff]: "Inl(a)=Inl(b) \<longleftrightarrow> a=b"
   22.18  by (simp add: sum_defs)
   22.19  
   22.20 -lemma Inr_iff [iff]: "Inr(a)=Inr(b) <-> a=b"
   22.21 +lemma Inr_iff [iff]: "Inr(a)=Inr(b) \<longleftrightarrow> a=b"
   22.22  by (simp add: sum_defs)
   22.23  
   22.24 -lemma Inl_Inr_iff [simp]: "Inl(a)=Inr(b) <-> False"
   22.25 +lemma Inl_Inr_iff [simp]: "Inl(a)=Inr(b) \<longleftrightarrow> False"
   22.26  by (simp add: sum_defs)
   22.27  
   22.28 -lemma Inr_Inl_iff [simp]: "Inr(b)=Inl(a) <-> False"
   22.29 +lemma Inr_Inl_iff [simp]: "Inr(b)=Inl(a) \<longleftrightarrow> False"
   22.30  by (simp add: sum_defs)
   22.31  
   22.32  lemma sum_empty [simp]: "0+0 = 0"
   22.33 @@ -106,19 +106,19 @@
   22.34  lemma InrD: "Inr(b): A+B ==> b: B"
   22.35  by blast
   22.36  
   22.37 -lemma sum_iff: "u: A+B <-> (\<exists>x. x:A & u=Inl(x)) | (\<exists>y. y:B & u=Inr(y))"
   22.38 +lemma sum_iff: "u: A+B \<longleftrightarrow> (\<exists>x. x:A & u=Inl(x)) | (\<exists>y. y:B & u=Inr(y))"
   22.39  by blast
   22.40  
   22.41 -lemma Inl_in_sum_iff [simp]: "(Inl(x) \<in> A+B) <-> (x \<in> A)";
   22.42 +lemma Inl_in_sum_iff [simp]: "(Inl(x) \<in> A+B) \<longleftrightarrow> (x \<in> A)";
   22.43  by auto
   22.44  
   22.45 -lemma Inr_in_sum_iff [simp]: "(Inr(y) \<in> A+B) <-> (y \<in> B)";
   22.46 +lemma Inr_in_sum_iff [simp]: "(Inr(y) \<in> A+B) \<longleftrightarrow> (y \<in> B)";
   22.47  by auto
   22.48  
   22.49 -lemma sum_subset_iff: "A+B \<subseteq> C+D <-> A<=C & B<=D"
   22.50 +lemma sum_subset_iff: "A+B \<subseteq> C+D \<longleftrightarrow> A<=C & B<=D"
   22.51  by blast
   22.52  
   22.53 -lemma sum_equal_iff: "A+B = C+D <-> A=C & B=D"
   22.54 +lemma sum_equal_iff: "A+B = C+D \<longleftrightarrow> A=C & B=D"
   22.55  by (simp add: extension sum_subset_iff, blast)
   22.56  
   22.57  lemma sum_eq_2_times: "A+A = 2*A"
   22.58 @@ -141,7 +141,7 @@
   22.59  by auto
   22.60  
   22.61  lemma expand_case: "u: A+B ==>    
   22.62 -        R(case(c,d,u)) <->  
   22.63 +        R(case(c,d,u)) \<longleftrightarrow>  
   22.64          ((\<forall>x\<in>A. u = Inl(x) \<longrightarrow> R(c(x))) &  
   22.65          (\<forall>y\<in>B. u = Inr(y) \<longrightarrow> R(d(y))))"
   22.66  by auto
    23.1 --- a/src/ZF/Univ.thy	Tue Mar 06 15:15:49 2012 +0000
    23.2 +++ b/src/ZF/Univ.thy	Tue Mar 06 16:06:52 2012 +0000
    23.3 @@ -433,10 +433,10 @@
    23.4  by (blast intro: VsetI_lemma elim: ltE)
    23.5  
    23.6  text{*Merely a lemma for the next result*}
    23.7 -lemma Vset_Ord_rank_iff: "Ord(i) ==> b \<in> Vset(i) <-> rank(b) < i"
    23.8 +lemma Vset_Ord_rank_iff: "Ord(i) ==> b \<in> Vset(i) \<longleftrightarrow> rank(b) < i"
    23.9  by (blast intro: VsetD VsetI)
   23.10  
   23.11 -lemma Vset_rank_iff [simp]: "b \<in> Vset(a) <-> rank(b) < rank(a)"
   23.12 +lemma Vset_rank_iff [simp]: "b \<in> Vset(a) \<longleftrightarrow> rank(b) < rank(a)"
   23.13  apply (rule Vfrom_rank_eq [THEN subst])
   23.14  apply (rule Ord_rank [THEN Vset_Ord_rank_iff])
   23.15  done
   23.16 @@ -766,10 +766,10 @@
   23.17  text{*This weaker version says a, b exist at the same level*}
   23.18  lemmas Vfrom_doubleton_D = Transset_Vfrom [THEN Transset_doubleton_D]
   23.19  
   23.20 -(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i)
   23.21 -      implies a, b : Vfrom(X,i), which is useless for induction.
   23.22 -    Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i)))
   23.23 -      implies a, b : Vfrom(X,i), leaving the succ(i) case untreated.
   23.24 +(** Using only the weaker theorem would prove <a,b> \<in> Vfrom(X,i)
   23.25 +      implies a, b \<in> Vfrom(X,i), which is useless for induction.
   23.26 +    Using only the stronger theorem would prove <a,b> \<in> Vfrom(X,succ(succ(i)))
   23.27 +      implies a, b \<in> Vfrom(X,i), leaving the succ(i) case untreated.
   23.28      The combination gives a reduction by precisely one level, which is
   23.29        most convenient for proofs.
   23.30  **)
    24.1 --- a/src/ZF/WF.thy	Tue Mar 06 15:15:49 2012 +0000
    24.2 +++ b/src/ZF/WF.thy	Tue Mar 06 16:06:52 2012 +0000
    24.3 @@ -63,7 +63,7 @@
    24.4  lemma wf_on_field_imp_wf: "wf[field(r)](r) ==> wf(r)"
    24.5  by (unfold wf_def wf_on_def, fast)
    24.6  
    24.7 -lemma wf_iff_wf_on_field: "wf(r) <-> wf[field(r)](r)"
    24.8 +lemma wf_iff_wf_on_field: "wf(r) \<longleftrightarrow> wf[field(r)](r)"
    24.9  by (blast intro: wf_imp_wf_on wf_on_field_imp_wf)
   24.10  
   24.11  lemma wf_on_subset_A: "[| wf[A](r);  B<=A |] ==> wf[B](r)"
   24.12 @@ -245,7 +245,7 @@
   24.13  apply (elim ssubst)
   24.14  apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def)
   24.15  apply (rule_tac t = "%z. H (?x,z) " in subst_context)
   24.16 -apply (subgoal_tac "\<forall>y\<in>r-``{x}. \<forall>z. <y,z>:f <-> <y,z>:g")
   24.17 +apply (subgoal_tac "\<forall>y\<in>r-``{x}. \<forall>z. <y,z>:f \<longleftrightarrow> <y,z>:g")
   24.18   apply (blast dest: transD)
   24.19  apply (simp add: apply_iff)
   24.20  apply (blast dest: transD intro: sym)
   24.21 @@ -364,7 +364,7 @@
   24.22  
   24.23  text{*Minimal-element characterization of well-foundedness*}
   24.24  lemma wf_eq_minimal:
   24.25 -     "wf(r) <-> (\<forall>Q x. x:Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. <y,z>:r \<longrightarrow> y\<notin>Q))"
   24.26 +     "wf(r) \<longleftrightarrow> (\<forall>Q x. x:Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. <y,z>:r \<longrightarrow> y\<notin>Q))"
   24.27  by (unfold wf_def, blast)
   24.28  
   24.29  end
    25.1 --- a/src/ZF/equalities.thy	Tue Mar 06 15:15:49 2012 +0000
    25.2 +++ b/src/ZF/equalities.thy	Tue Mar 06 16:06:52 2012 +0000
    25.3 @@ -22,21 +22,21 @@
    25.4    The following are not added to the default simpset because
    25.5    (a) they duplicate the body and (b) there are no similar rules for @{text Int}.*}
    25.6  
    25.7 -lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) <-> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))";
    25.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))";
    25.9    by blast
   25.10  
   25.11 -lemma bex_Un: "(\<exists>x \<in> A\<union>B. P(x)) <-> (\<exists>x \<in> A. P(x)) | (\<exists>x \<in> B. P(x))";
   25.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))";
   25.13    by blast
   25.14  
   25.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))"
   25.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))"
   25.17    by blast
   25.18  
   25.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))"
   25.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))"
   25.21    by blast
   25.22  
   25.23  subsection{*Converse of a Relation*}
   25.24  
   25.25 -lemma converse_iff [simp]: "<a,b>\<in> converse(r) <-> <b,a>\<in>r"
   25.26 +lemma converse_iff [simp]: "<a,b>\<in> converse(r) \<longleftrightarrow> <b,a>\<in>r"
   25.27  by (unfold converse_def, blast)
   25.28  
   25.29  lemma converseI [intro!]: "<a,b>\<in>r ==> <b,a>\<in>converse(r)"
   25.30 @@ -64,7 +64,7 @@
   25.31  by blast
   25.32  
   25.33  lemma converse_subset_iff:
   25.34 -     "A \<subseteq> Sigma(X,Y) ==> converse(A) \<subseteq> converse(B) <-> A \<subseteq> B"
   25.35 +     "A \<subseteq> Sigma(X,Y) ==> converse(A) \<subseteq> converse(B) \<longleftrightarrow> A \<subseteq> B"
   25.36  by blast
   25.37  
   25.38  
   25.39 @@ -76,17 +76,17 @@
   25.40  lemma subset_consI: "B \<subseteq> cons(a,B)"
   25.41  by blast
   25.42  
   25.43 -lemma cons_subset_iff [iff]: "cons(a,B)\<subseteq>C <-> a\<in>C & B\<subseteq>C"
   25.44 +lemma cons_subset_iff [iff]: "cons(a,B)\<subseteq>C \<longleftrightarrow> a\<in>C & B\<subseteq>C"
   25.45  by blast
   25.46  
   25.47  (*A safe special case of subset elimination, adding no new variables
   25.48    [| cons(a,B) \<subseteq> C; [| a \<in> C; B \<subseteq> C |] ==> R |] ==> R *)
   25.49  lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE]
   25.50  
   25.51 -lemma subset_empty_iff: "A\<subseteq>0 <-> A=0"
   25.52 +lemma subset_empty_iff: "A\<subseteq>0 \<longleftrightarrow> A=0"
   25.53  by blast
   25.54  
   25.55 -lemma subset_cons_iff: "C\<subseteq>cons(a,B) <-> C\<subseteq>B | (a\<in>C & C-{a} \<subseteq> B)"
   25.56 +lemma subset_cons_iff: "C\<subseteq>cons(a,B) \<longleftrightarrow> C\<subseteq>B | (a\<in>C & C-{a} \<subseteq> B)"
   25.57  by blast
   25.58  
   25.59  (* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)
   25.60 @@ -134,7 +134,7 @@
   25.61      "[| succ(i) \<subseteq> j;  [| i\<in>j;  i\<subseteq>j |] ==> P |] ==> P"
   25.62  by (unfold succ_def, blast)
   25.63  
   25.64 -lemma succ_subset_iff: "succ(a) \<subseteq> B <-> (a \<subseteq> B & a \<in> B)"
   25.65 +lemma succ_subset_iff: "succ(a) \<subseteq> B \<longleftrightarrow> (a \<subseteq> B & a \<in> B)"
   25.66  by (unfold succ_def, blast)
   25.67  
   25.68  
   25.69 @@ -142,7 +142,7 @@
   25.70  
   25.71  (** Intersection is the greatest lower bound of two sets **)
   25.72  
   25.73 -lemma Int_subset_iff: "C \<subseteq> A \<inter> B <-> C \<subseteq> A & C \<subseteq> B"
   25.74 +lemma Int_subset_iff: "C \<subseteq> A \<inter> B \<longleftrightarrow> C \<subseteq> A & C \<subseteq> B"
   25.75  by blast
   25.76  
   25.77  lemma Int_lower1: "A \<inter> B \<subseteq> A"
   25.78 @@ -187,10 +187,10 @@
   25.79  lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
   25.80  by blast
   25.81  
   25.82 -lemma subset_Int_iff: "A\<subseteq>B <-> A \<inter> B = A"
   25.83 +lemma subset_Int_iff: "A\<subseteq>B \<longleftrightarrow> A \<inter> B = A"
   25.84  by (blast elim!: equalityE)
   25.85  
   25.86 -lemma subset_Int_iff2: "A\<subseteq>B <-> B \<inter> A = A"
   25.87 +lemma subset_Int_iff2: "A\<subseteq>B \<longleftrightarrow> B \<inter> A = A"
   25.88  by (blast elim!: equalityE)
   25.89  
   25.90  lemma Int_Diff_eq: "C\<subseteq>A ==> (A-B) \<inter> C = C-B"
   25.91 @@ -211,7 +211,7 @@
   25.92  
   25.93  (** Union is the least upper bound of two sets *)
   25.94  
   25.95 -lemma Un_subset_iff: "A \<union> B \<subseteq> C <-> A \<subseteq> C & B \<subseteq> C"
   25.96 +lemma Un_subset_iff: "A \<union> B \<subseteq> C \<longleftrightarrow> A \<subseteq> C & B \<subseteq> C"
   25.97  by blast
   25.98  
   25.99  lemma Un_upper1: "A \<subseteq> A \<union> B"
  25.100 @@ -253,13 +253,13 @@
  25.101  lemma Un_Int_distrib: "(A \<inter> B) \<union> C  =  (A \<union> C) \<inter> (B \<union> C)"
  25.102  by blast
  25.103  
  25.104 -lemma subset_Un_iff: "A\<subseteq>B <-> A \<union> B = B"
  25.105 +lemma subset_Un_iff: "A\<subseteq>B \<longleftrightarrow> A \<union> B = B"
  25.106  by (blast elim!: equalityE)
  25.107  
  25.108 -lemma subset_Un_iff2: "A\<subseteq>B <-> B \<union> A = B"
  25.109 +lemma subset_Un_iff2: "A\<subseteq>B \<longleftrightarrow> B \<union> A = B"
  25.110  by (blast elim!: equalityE)
  25.111  
  25.112 -lemma Un_empty [iff]: "(A \<union> B = 0) <-> (A = 0 & B = 0)"
  25.113 +lemma Un_empty [iff]: "(A \<union> B = 0) \<longleftrightarrow> (A = 0 & B = 0)"
  25.114  by blast
  25.115  
  25.116  lemma Un_eq_Union: "A \<union> B = \<Union>({A, B})"
  25.117 @@ -273,7 +273,7 @@
  25.118  lemma Diff_contains: "[| C\<subseteq>A;  C \<inter> B = 0 |] ==> C \<subseteq> A-B"
  25.119  by blast
  25.120  
  25.121 -lemma subset_Diff_cons_iff: "B \<subseteq> A - cons(c,C)  <->  B\<subseteq>A-C & c \<notin> B"
  25.122 +lemma subset_Diff_cons_iff: "B \<subseteq> A - cons(c,C)  \<longleftrightarrow>  B\<subseteq>A-C & c \<notin> B"
  25.123  by blast
  25.124  
  25.125  lemma Diff_cancel: "A - A = 0"
  25.126 @@ -288,7 +288,7 @@
  25.127  lemma Diff_0 [simp]: "A - 0 = A"
  25.128  by blast
  25.129  
  25.130 -lemma Diff_eq_0_iff: "A - B = 0 <-> A \<subseteq> B"
  25.131 +lemma Diff_eq_0_iff: "A - B = 0 \<longleftrightarrow> A \<subseteq> B"
  25.132  by (blast elim: equalityE)
  25.133  
  25.134  (*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
  25.135 @@ -338,7 +338,7 @@
  25.136  by blast
  25.137  
  25.138  (*Halmos, Naive Set Theory, page 16.*)
  25.139 -lemma Un_Int_assoc_iff: "(A \<inter> B) \<union> C = A \<inter> (B \<union> C)  <->  C\<subseteq>A"
  25.140 +lemma Un_Int_assoc_iff: "(A \<inter> B) \<union> C = A \<inter> (B \<union> C)  \<longleftrightarrow>  C\<subseteq>A"
  25.141  by (blast elim!: equalityE)
  25.142  
  25.143  
  25.144 @@ -346,7 +346,7 @@
  25.145  
  25.146  (** Big Union is the least upper bound of a set  **)
  25.147  
  25.148 -lemma Union_subset_iff: "\<Union>(A) \<subseteq> C <-> (\<forall>x\<in>A. x \<subseteq> C)"
  25.149 +lemma Union_subset_iff: "\<Union>(A) \<subseteq> C \<longleftrightarrow> (\<forall>x\<in>A. x \<subseteq> C)"
  25.150  by blast
  25.151  
  25.152  lemma Union_upper: "B\<in>A ==> B \<subseteq> \<Union>(A)"
  25.153 @@ -364,10 +364,10 @@
  25.154  lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>(A) \<inter> \<Union>(B)"
  25.155  by blast
  25.156  
  25.157 -lemma Union_disjoint: "\<Union>(C) \<inter> A = 0 <-> (\<forall>B\<in>C. B \<inter> A = 0)"
  25.158 +lemma Union_disjoint: "\<Union>(C) \<inter> A = 0 \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = 0)"
  25.159  by (blast elim!: equalityE)
  25.160  
  25.161 -lemma Union_empty_iff: "\<Union>(A) = 0 <-> (\<forall>B\<in>A. B=0)"
  25.162 +lemma Union_empty_iff: "\<Union>(A) = 0 \<longleftrightarrow> (\<forall>B\<in>A. B=0)"
  25.163  by blast
  25.164  
  25.165  lemma Int_Union2: "\<Union>(B) \<inter> A = (\<Union>C\<in>B. C \<inter> A)"
  25.166 @@ -375,7 +375,7 @@
  25.167  
  25.168  (** Big Intersection is the greatest lower bound of a nonempty set **)
  25.169  
  25.170 -lemma Inter_subset_iff: "A\<noteq>0  ==>  C \<subseteq> \<Inter>(A) <-> (\<forall>x\<in>A. C \<subseteq> x)"
  25.171 +lemma Inter_subset_iff: "A\<noteq>0  ==>  C \<subseteq> \<Inter>(A) \<longleftrightarrow> (\<forall>x\<in>A. C \<subseteq> x)"
  25.172  by blast
  25.173  
  25.174  lemma Inter_lower: "B\<in>A ==> \<Inter>(A) \<subseteq> B"
  25.175 @@ -416,10 +416,10 @@
  25.176  
  25.177  subsection{*Unions and Intersections of Families*}
  25.178  
  25.179 -lemma subset_UN_iff_eq: "A \<subseteq> (\<Union>i\<in>I. B(i)) <-> A = (\<Union>i\<in>I. A \<inter> B(i))"
  25.180 +lemma subset_UN_iff_eq: "A \<subseteq> (\<Union>i\<in>I. B(i)) \<longleftrightarrow> A = (\<Union>i\<in>I. A \<inter> B(i))"
  25.181  by (blast elim!: equalityE)
  25.182  
  25.183 -lemma UN_subset_iff: "(\<Union>x\<in>A. B(x)) \<subseteq> C <-> (\<forall>x\<in>A. B(x) \<subseteq> C)"
  25.184 +lemma UN_subset_iff: "(\<Union>x\<in>A. B(x)) \<subseteq> C \<longleftrightarrow> (\<forall>x\<in>A. B(x) \<subseteq> C)"
  25.185  by blast
  25.186  
  25.187  lemma UN_upper: "x\<in>A ==> B(x) \<subseteq> (\<Union>x\<in>A. B(x))"
  25.188 @@ -571,7 +571,7 @@
  25.189  by blast
  25.190  
  25.191  lemma times_subset_iff:
  25.192 -     "(A'*B' \<subseteq> A*B) <-> (A' = 0 | B' = 0 | (A'\<subseteq>A) & (B'\<subseteq>B))"
  25.193 +     "(A'*B' \<subseteq> A*B) \<longleftrightarrow> (A' = 0 | B' = 0 | (A'\<subseteq>A) & (B'\<subseteq>B))"
  25.194  by blast
  25.195  
  25.196  lemma Int_Sigma_eq:
  25.197 @@ -580,7 +580,7 @@
  25.198  
  25.199  (** Domain **)
  25.200  
  25.201 -lemma domain_iff: "a: domain(r) <-> (\<exists>y. <a,y>\<in> r)"
  25.202 +lemma domain_iff: "a: domain(r) \<longleftrightarrow> (\<exists>y. <a,y>\<in> r)"
  25.203  by (unfold domain_def, blast)
  25.204  
  25.205  lemma domainI [intro]: "<a,b>\<in> r ==> a: domain(r)"
  25.206 @@ -739,10 +739,10 @@
  25.207  
  25.208  subsection{*Image of a Set under a Function or Relation*}
  25.209  
  25.210 -lemma image_iff: "b \<in> r``A <-> (\<exists>x\<in>A. <x,b>\<in>r)"
  25.211 +lemma image_iff: "b \<in> r``A \<longleftrightarrow> (\<exists>x\<in>A. <x,b>\<in>r)"
  25.212  by (unfold image_def, blast)
  25.213  
  25.214 -lemma image_singleton_iff: "b \<in> r``{a} <-> <a,b>\<in>r"
  25.215 +lemma image_singleton_iff: "b \<in> r``{a} \<longleftrightarrow> <a,b>\<in>r"
  25.216  by (rule image_iff [THEN iff_trans], blast)
  25.217  
  25.218  lemma imageI [intro]: "[| <a,b>\<in> r;  a\<in>A |] ==> b \<in> r``A"
  25.219 @@ -792,10 +792,10 @@
  25.220  subsection{*Inverse Image of a Set under a Function or Relation*}
  25.221  
  25.222  lemma vimage_iff:
  25.223 -    "a \<in> r-``B <-> (\<exists>y\<in>B. <a,y>\<in>r)"
  25.224 +    "a \<in> r-``B \<longleftrightarrow> (\<exists>y\<in>B. <a,y>\<in>r)"
  25.225  by (unfold vimage_def image_def converse_def, blast)
  25.226  
  25.227 -lemma vimage_singleton_iff: "a \<in> r-``{b} <-> <a,b>\<in>r"
  25.228 +lemma vimage_singleton_iff: "a \<in> r-``{b} \<longleftrightarrow> <a,b>\<in>r"
  25.229  by (rule vimage_iff [THEN iff_trans], blast)
  25.230  
  25.231  lemma vimageI [intro]: "[| <a,b>\<in> r;  b\<in>B |] ==> a \<in> r-``B"
  25.232 @@ -897,7 +897,7 @@
  25.233  lemma Union_Pow_eq [simp]: "\<Union>(Pow(A)) = A"
  25.234  by blast
  25.235  
  25.236 -lemma Union_Pow_iff: "\<Union>(A) \<in> Pow(B) <-> A \<in> Pow(Pow(B))"
  25.237 +lemma Union_Pow_iff: "\<Union>(A) \<in> Pow(B) \<longleftrightarrow> A \<in> Pow(Pow(B))"
  25.238  by blast
  25.239  
  25.240  lemma Pow_Int_eq [simp]: "Pow(A \<inter> B) = Pow(A) \<inter> Pow(B)"
  25.241 @@ -912,7 +912,7 @@
  25.242  lemma RepFun_subset: "[| !!x. x\<in>A ==> f(x) \<in> B |] ==> {f(x). x\<in>A} \<subseteq> B"
  25.243  by blast
  25.244  
  25.245 -lemma RepFun_eq_0_iff [simp]: "{f(x).x\<in>A}=0 <-> A=0"
  25.246 +lemma RepFun_eq_0_iff [simp]: "{f(x).x\<in>A}=0 \<longleftrightarrow> A=0"
  25.247  by blast
  25.248  
  25.249  lemma RepFun_constant [simp]: "{c. x\<in>A} = (if A=0 then 0 else {c})"
    26.1 --- a/src/ZF/ex/Ring.thy	Tue Mar 06 15:15:49 2012 +0000
    26.2 +++ b/src/ZF/ex/Ring.thy	Tue Mar 06 16:06:52 2012 +0000
    26.3 @@ -6,6 +6,10 @@
    26.4  
    26.5  theory Ring imports Group begin
    26.6  
    26.7 +no_notation
    26.8 +  cadd  (infixl "\<oplus>" 65) and
    26.9 +  cmult  (infixl "\<otimes>" 70)
   26.10 +
   26.11  (*First, we must simulate a record declaration:
   26.12  record ring = monoid +
   26.13    add :: "[i, i] => i" (infixl "\<oplus>\<index>" 65)
   26.14 @@ -46,7 +50,7 @@
   26.15    "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
   26.16  
   26.17  locale abelian_monoid = fixes G (structure)
   26.18 -  assumes a_comm_monoid: 
   26.19 +  assumes a_comm_monoid:
   26.20      "comm_monoid (<carrier(G), add_field(G), zero(G), 0>)"
   26.21  
   26.22  text {*
   26.23 @@ -54,7 +58,7 @@
   26.24  *}
   26.25  
   26.26  locale abelian_group = abelian_monoid +
   26.27 -  assumes a_comm_group: 
   26.28 +  assumes a_comm_group:
   26.29      "comm_group (<carrier(G), add_field(G), zero(G), 0>)"
   26.30  
   26.31  locale ring = abelian_group R + monoid R for R (structure) +
   26.32 @@ -75,21 +79,21 @@
   26.33  
   26.34  lemma (in abelian_monoid) a_monoid:
   26.35       "monoid (<carrier(G), add_field(G), zero(G), 0>)"
   26.36 -apply (insert a_comm_monoid) 
   26.37 -apply (simp add: comm_monoid_def) 
   26.38 +apply (insert a_comm_monoid)
   26.39 +apply (simp add: comm_monoid_def)
   26.40  done
   26.41  
   26.42  lemma (in abelian_group) a_group:
   26.43       "group (<carrier(G), add_field(G), zero(G), 0>)"
   26.44 -apply (insert a_comm_group) 
   26.45 -apply (simp add: comm_group_def group_def) 
   26.46 +apply (insert a_comm_group)
   26.47 +apply (simp add: comm_group_def group_def)
   26.48  done
   26.49  
   26.50  
   26.51  lemma (in abelian_monoid) l_zero [simp]:
   26.52       "x \<in> carrier(G) \<Longrightarrow> \<zero> \<oplus> x = x"
   26.53  apply (insert monoid.l_one [OF a_monoid])
   26.54 -apply (simp add: ring_add_def) 
   26.55 +apply (simp add: ring_add_def)
   26.56  done
   26.57  
   26.58  lemma (in abelian_monoid) zero_closed [intro, simp]:
   26.59 @@ -102,7 +106,7 @@
   26.60  
   26.61  lemma (in abelian_monoid) a_closed [intro, simp]:
   26.62       "[| x \<in> carrier(G); y \<in> carrier(G) |] ==> x \<oplus> y \<in> carrier(G)"
   26.63 -by (rule monoid.m_closed [OF a_monoid, 
   26.64 +by (rule monoid.m_closed [OF a_monoid,
   26.65                    simplified, simplified ring_add_def [symmetric]])
   26.66  
   26.67  lemma (in abelian_group) minus_closed [intro, simp]:
   26.68 @@ -110,18 +114,18 @@
   26.69  by (simp add: minus_def)
   26.70  
   26.71  lemma (in abelian_group) a_l_cancel [simp]:
   26.72 -     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> 
   26.73 +     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
   26.74        \<Longrightarrow> (x \<oplus> y = x \<oplus> z) <-> (y = z)"
   26.75 -by (rule group.l_cancel [OF a_group, 
   26.76 +by (rule group.l_cancel [OF a_group,
   26.77               simplified, simplified ring_add_def [symmetric]])
   26.78  
   26.79  lemma (in abelian_group) a_r_cancel [simp]:
   26.80 -     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> 
   26.81 +     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
   26.82        \<Longrightarrow> (y \<oplus> x = z \<oplus> x) <-> (y = z)"
   26.83  by (rule group.r_cancel [OF a_group, simplified, simplified ring_add_def [symmetric]])
   26.84  
   26.85  lemma (in abelian_monoid) a_assoc:
   26.86 -  "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> 
   26.87 +  "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
   26.88     \<Longrightarrow> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
   26.89  by (rule monoid.m_assoc [OF a_monoid, simplified, simplified ring_add_def [symmetric]])
   26.90  
   26.91 @@ -136,7 +140,7 @@
   26.92      simplified, simplified ring_add_def [symmetric]])
   26.93  
   26.94  lemma (in abelian_monoid) a_lcomm:
   26.95 -     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> 
   26.96 +     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
   26.97        \<Longrightarrow> x \<oplus> (y \<oplus> z) = y \<oplus> (x \<oplus> z)"
   26.98  by (rule comm_monoid.m_lcomm [OF a_comm_monoid,
   26.99      simplified, simplified ring_add_def [symmetric]])
  26.100 @@ -168,7 +172,7 @@
  26.101  
  26.102  lemmas (in abelian_monoid) a_ac = a_assoc a_comm a_lcomm
  26.103  
  26.104 -text {* 
  26.105 +text {*
  26.106    The following proofs are from Jacobson, Basic Algebra I, pp.~88--89
  26.107  *}
  26.108  
  26.109 @@ -179,7 +183,7 @@
  26.110  proof -
  26.111    assume R: "x \<in> carrier(R)"
  26.112    then have "\<zero> \<cdot> x \<oplus> \<zero> \<cdot> x = (\<zero> \<oplus> \<zero>) \<cdot> x"
  26.113 -    by (blast intro: l_distr [THEN sym]) 
  26.114 +    by (blast intro: l_distr [THEN sym])
  26.115    also from R have "... = \<zero> \<cdot> x \<oplus> \<zero>" by simp
  26.116    finally have "\<zero> \<cdot> x \<oplus> \<zero> \<cdot> x = \<zero> \<cdot> x \<oplus> \<zero>" .
  26.117    with R show ?thesis by (simp del: r_zero)
  26.118 @@ -250,12 +254,12 @@
  26.119  by (auto simp add: ring_hom_def)
  26.120  
  26.121  lemma ring_hom_mult:
  26.122 -     "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> 
  26.123 +     "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R); y \<in> carrier(R)\<rbrakk>
  26.124        \<Longrightarrow> h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y)"
  26.125  by (simp add: ring_hom_def)
  26.126  
  26.127  lemma ring_hom_add:
  26.128 -     "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> 
  26.129 +     "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R); y \<in> carrier(R)\<rbrakk>
  26.130        \<Longrightarrow> h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)"
  26.131  by (simp add: ring_hom_def)
  26.132  
  26.133 @@ -288,8 +292,8 @@
  26.134  qed
  26.135  
  26.136  lemma (in ring) id_ring_hom [simp]: "id(carrier(R)) \<in> ring_hom(R,R)"
  26.137 -apply (rule ring_hom_memI)  
  26.138 -apply (auto simp add: id_type) 
  26.139 +apply (rule ring_hom_memI)
  26.140 +apply (auto simp add: id_type)
  26.141  done
  26.142  
  26.143  end
    27.1 --- a/src/ZF/func.thy	Tue Mar 06 15:15:49 2012 +0000
    27.2 +++ b/src/ZF/func.thy	Tue Mar 06 16:06:52 2012 +0000
    27.3 @@ -20,12 +20,12 @@
    27.4  by (simp add: restrict_def relation_def, blast) 
    27.5  
    27.6  lemma Pi_iff:
    27.7 -    "f: Pi(A,B) <-> function(f) & f<=Sigma(A,B) & A<=domain(f)"
    27.8 +    "f: Pi(A,B) \<longleftrightarrow> function(f) & f<=Sigma(A,B) & A<=domain(f)"
    27.9  by (unfold Pi_def, blast)
   27.10  
   27.11  (*For upward compatibility with the former definition*)
   27.12  lemma Pi_iff_old:
   27.13 -    "f: Pi(A,B) <-> f<=Sigma(A,B) & (\<forall>x\<in>A. EX! y. <x,y>: f)"
   27.14 +    "f: Pi(A,B) \<longleftrightarrow> f<=Sigma(A,B) & (\<forall>x\<in>A. EX! y. <x,y>: f)"
   27.15  by (unfold Pi_def function_def, blast)
   27.16  
   27.17  lemma fun_is_function: "f: Pi(A,B) ==> function(f)"
   27.18 @@ -96,7 +96,7 @@
   27.19  lemma apply_funtype: "[| f: A->B;  a:A |] ==> f`a \<in> B"
   27.20  by (blast dest: apply_type)
   27.21  
   27.22 -lemma apply_iff: "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b"
   27.23 +lemma apply_iff: "f: Pi(A,B) ==> <a,b>: f \<longleftrightarrow> a:A & f`a = b"
   27.24  apply (frule fun_is_rel)
   27.25  apply (blast intro!: apply_Pair apply_equality)
   27.26  done
   27.27 @@ -110,7 +110,7 @@
   27.28  (*Such functions arise in non-standard datatypes, ZF/ex/Ntree for instance*)
   27.29  lemma Pi_Collect_iff:
   27.30       "(f \<in> Pi(A, %x. {y:B(x). P(x,y)}))
   27.31 -      <->  f \<in> Pi(A,B) & (\<forall>x\<in>A. P(x, f`x))"
   27.32 +      \<longleftrightarrow>  f \<in> Pi(A,B) & (\<forall>x\<in>A. P(x, f`x))"
   27.33  by (blast intro: Pi_type dest: apply_type)
   27.34  
   27.35  lemma Pi_weaken_type:
   27.36 @@ -222,11 +222,11 @@
   27.37  done
   27.38  
   27.39  lemma fun_extension_iff:
   27.40 -     "[| f:Pi(A,B); g:Pi(A,C) |] ==> (\<forall>a\<in>A. f`a = g`a) <-> f=g"
   27.41 +     "[| f:Pi(A,B); g:Pi(A,C) |] ==> (\<forall>a\<in>A. f`a = g`a) \<longleftrightarrow> f=g"
   27.42  by (blast intro: fun_extension)
   27.43  
   27.44  (*thm by Mark Staples, proof by lcp*)
   27.45 -lemma fun_subset_eq: "[| f:Pi(A,B); g:Pi(A,C) |] ==> f \<subseteq> g <-> (f = g)"
   27.46 +lemma fun_subset_eq: "[| f:Pi(A,B); g:Pi(A,C) |] ==> f \<subseteq> g \<longleftrightarrow> (f = g)"
   27.47  by (blast dest: apply_Pair
   27.48            intro: fun_extension apply_equality [symmetric])
   27.49  
   27.50 @@ -592,7 +592,7 @@
   27.51  (* Useful with simp; contributed by Clemens Ballarin. *)
   27.52  
   27.53  lemma bex_image_simp:
   27.54 -  "[| f \<in> Pi(X, Y); A \<subseteq> X |]  ==> (\<exists>x\<in>f``A. P(x)) <-> (\<exists>x\<in>A. P(f`x))"
   27.55 +  "[| f \<in> Pi(X, Y); A \<subseteq> X |]  ==> (\<exists>x\<in>f``A. P(x)) \<longleftrightarrow> (\<exists>x\<in>A. P(f`x))"
   27.56    apply safe
   27.57     apply rule
   27.58      prefer 2 apply assumption
   27.59 @@ -601,7 +601,7 @@
   27.60    done
   27.61  
   27.62  lemma ball_image_simp:
   27.63 -  "[| f \<in> Pi(X, Y); A \<subseteq> X |]  ==> (\<forall>x\<in>f``A. P(x)) <-> (\<forall>x\<in>A. P(f`x))"
   27.64 +  "[| f \<in> Pi(X, Y); A \<subseteq> X |]  ==> (\<forall>x\<in>f``A. P(x)) \<longleftrightarrow> (\<forall>x\<in>A. P(f`x))"
   27.65    apply safe
   27.66     apply (blast intro: apply_Pair)
   27.67    apply (drule bspec) apply assumption
    28.1 --- a/src/ZF/pair.thy	Tue Mar 06 15:15:49 2012 +0000
    28.2 +++ b/src/ZF/pair.thy	Tue Mar 06 16:06:52 2012 +0000
    28.3 @@ -34,13 +34,13 @@
    28.4  
    28.5  (** Lemmas for showing that <a,b> uniquely determines a and b **)
    28.6  
    28.7 -lemma singleton_eq_iff [iff]: "{a} = {b} <-> a=b"
    28.8 +lemma singleton_eq_iff [iff]: "{a} = {b} \<longleftrightarrow> a=b"
    28.9  by (rule extension [THEN iff_trans], blast)
   28.10  
   28.11 -lemma doubleton_eq_iff: "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)"
   28.12 +lemma doubleton_eq_iff: "{a,b} = {c,d} \<longleftrightarrow> (a=c & b=d) | (a=d & b=c)"
   28.13  by (rule extension [THEN iff_trans], blast)
   28.14  
   28.15 -lemma Pair_iff [simp]: "<a,b> = <c,d> <-> a=c & b=d"
   28.16 +lemma Pair_iff [simp]: "<a,b> = <c,d> \<longleftrightarrow> a=c & b=d"
   28.17  by (simp add: Pair_def doubleton_eq_iff, blast)
   28.18  
   28.19  lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, elim!]
   28.20 @@ -76,7 +76,7 @@
   28.21  
   28.22  text{*Generalizes Cartesian product*}
   28.23  
   28.24 -lemma Sigma_iff [simp]: "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
   28.25 +lemma Sigma_iff [simp]: "<a,b>: Sigma(A,B) \<longleftrightarrow> a:A & b:B(a)"
   28.26  by (simp add: Sigma_def)
   28.27  
   28.28  lemma SigmaI [TC,intro!]: "[| a:A;  b:B(a) |] ==> <a,b> \<in> Sigma(A,B)"
   28.29 @@ -113,7 +113,7 @@
   28.30  lemma Sigma_empty2 [simp]: "A*0 = 0"
   28.31  by blast
   28.32  
   28.33 -lemma Sigma_empty_iff: "A*B=0 <-> A=0 | B=0"
   28.34 +lemma Sigma_empty_iff: "A*B=0 \<longleftrightarrow> A=0 | B=0"
   28.35  by blast
   28.36  
   28.37  
   28.38 @@ -150,7 +150,7 @@
   28.39  
   28.40  lemma expand_split: 
   28.41    "u: A*B ==>    
   28.42 -        R(split(c,u)) <-> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x,y> \<longrightarrow> R(c(x,y)))"
   28.43 +        R(split(c,u)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x,y> \<longrightarrow> R(c(x,y)))"
   28.44  apply (simp add: split_def)
   28.45  apply auto
   28.46  done
   28.47 @@ -177,11 +177,11 @@
   28.48  *}
   28.49  
   28.50  lemma split_paired_Bex_Sigma [simp]:
   28.51 -     "(\<exists>z \<in> Sigma(A,B). P(z)) <-> (\<exists>x \<in> A. \<exists>y \<in> B(x). P(<x,y>))"
   28.52 +     "(\<exists>z \<in> Sigma(A,B). P(z)) \<longleftrightarrow> (\<exists>x \<in> A. \<exists>y \<in> B(x). P(<x,y>))"
   28.53  by blast
   28.54  
   28.55  lemma split_paired_Ball_Sigma [simp]:
   28.56 -     "(\<forall>z \<in> Sigma(A,B). P(z)) <-> (\<forall>x \<in> A. \<forall>y \<in> B(x). P(<x,y>))"
   28.57 +     "(\<forall>z \<in> Sigma(A,B). P(z)) \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> B(x). P(<x,y>))"
   28.58  by blast
   28.59  
   28.60  end
    29.1 --- a/src/ZF/upair.thy	Tue Mar 06 15:15:49 2012 +0000
    29.2 +++ b/src/ZF/upair.thy	Tue Mar 06 16:06:52 2012 +0000
    29.3 @@ -23,7 +23,7 @@
    29.4  
    29.5  subsection{*Unordered Pairs: constant @{term Upair}*}
    29.6  
    29.7 -lemma Upair_iff [simp]: "c \<in> Upair(a,b) <-> (c=a | c=b)"
    29.8 +lemma Upair_iff [simp]: "c \<in> Upair(a,b) \<longleftrightarrow> (c=a | c=b)"
    29.9  by (unfold Upair_def, blast)
   29.10  
   29.11  lemma UpairI1: "a \<in> Upair(a,b)"
   29.12 @@ -37,7 +37,7 @@
   29.13  
   29.14  subsection{*Rules for Binary Union, Defined via @{term Upair}*}
   29.15  
   29.16 -lemma Un_iff [simp]: "c \<in> A \<union> B <-> (c:A | c:B)"
   29.17 +lemma Un_iff [simp]: "c \<in> A \<union> B \<longleftrightarrow> (c:A | c:B)"
   29.18  apply (simp add: Un_def)
   29.19  apply (blast intro: UpairI1 UpairI2 elim: UpairE)
   29.20  done
   29.21 @@ -63,7 +63,7 @@
   29.22  
   29.23  subsection{*Rules for Binary Intersection, Defined via @{term Upair}*}
   29.24  
   29.25 -lemma Int_iff [simp]: "c \<in> A \<inter> B <-> (c:A & c:B)"
   29.26 +lemma Int_iff [simp]: "c \<in> A \<inter> B \<longleftrightarrow> (c:A & c:B)"
   29.27  apply (unfold Int_def)
   29.28  apply (blast intro: UpairI1 UpairI2 elim: UpairE)
   29.29  done
   29.30 @@ -83,7 +83,7 @@
   29.31  
   29.32  subsection{*Rules for Set Difference, Defined via @{term Upair}*}
   29.33  
   29.34 -lemma Diff_iff [simp]: "c \<in> A-B <-> (c:A & c\<notin>B)"
   29.35 +lemma Diff_iff [simp]: "c \<in> A-B \<longleftrightarrow> (c:A & c\<notin>B)"
   29.36  by (unfold Diff_def, blast)
   29.37  
   29.38  lemma DiffI [intro!]: "[| c \<in> A;  c \<notin> B |] ==> c \<in> A - B"
   29.39 @@ -101,7 +101,7 @@
   29.40  
   29.41  subsection{*Rules for @{term cons}*}
   29.42  
   29.43 -lemma cons_iff [simp]: "a \<in> cons(b,A) <-> (a=b | a:A)"
   29.44 +lemma cons_iff [simp]: "a \<in> cons(b,A) \<longleftrightarrow> (a=b | a:A)"
   29.45  apply (unfold cons_def)
   29.46  apply (blast intro: UpairI1 UpairI2 elim: UpairE)
   29.47  done
   29.48 @@ -137,7 +137,7 @@
   29.49  
   29.50  subsection{*Singletons*}
   29.51  
   29.52 -lemma singleton_iff: "a \<in> {b} <-> a=b"
   29.53 +lemma singleton_iff: "a \<in> {b} \<longleftrightarrow> a=b"
   29.54  by simp
   29.55  
   29.56  lemma singletonI [intro!]: "a \<in> {a}"
   29.57 @@ -164,7 +164,7 @@
   29.58  apply (blast+)
   29.59  done
   29.60  
   29.61 -(*No congruence rule is necessary: if @{term"\<forall>y.P(y)<->Q(y)"} then
   29.62 +(*No congruence rule is necessary: if @{term"\<forall>y.P(y)\<longleftrightarrow>Q(y)"} then
   29.63    @{term "THE x.P(x)"}  rewrites to @{term "THE x.Q(x)"} *)
   29.64  
   29.65  (*If it's "undefined", it's zero!*)
   29.66 @@ -203,13 +203,13 @@
   29.67  
   29.68  (*Never use with case splitting, or if P is known to be true or false*)
   29.69  lemma if_cong:
   29.70 -    "[| P<->Q;  Q ==> a=c;  ~Q ==> b=d |]
   29.71 +    "[| P\<longleftrightarrow>Q;  Q ==> a=c;  ~Q ==> b=d |]
   29.72       ==> (if P then a else b) = (if Q then c else d)"
   29.73  by (simp add: if_def cong add: conj_cong)
   29.74  
   29.75  (*Prevents simplification of x and y: faster and allows the execution
   29.76    of functional programs. NOW THE DEFAULT.*)
   29.77 -lemma if_weak_cong: "P<->Q ==> (if P then x else y) = (if Q then x else y)"
   29.78 +lemma if_weak_cong: "P\<longleftrightarrow>Q ==> (if P then x else y) = (if Q then x else y)"
   29.79  by simp
   29.80  
   29.81  (*Not needed for rewriting, since P would rewrite to True anyway*)
   29.82 @@ -221,7 +221,7 @@
   29.83  by (unfold if_def, blast)
   29.84  
   29.85  lemma split_if [split]:
   29.86 -     "P(if Q then x else y) <-> ((Q \<longrightarrow> P(x)) & (~Q \<longrightarrow> P(y)))"
   29.87 +     "P(if Q then x else y) \<longleftrightarrow> ((Q \<longrightarrow> P(x)) & (~Q \<longrightarrow> P(y)))"
   29.88  by (case_tac Q, simp_all)
   29.89  
   29.90  (** Rewrite rules for boolean case-splitting: faster than split_if [split]
   29.91 @@ -236,7 +236,7 @@
   29.92  lemmas split_ifs = split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
   29.93  
   29.94  (*Logically equivalent to split_if_mem2*)
   29.95 -lemma if_iff: "a: (if P then x else y) <-> P & a:x | ~P & a:y"
   29.96 +lemma if_iff: "a: (if P then x else y) \<longleftrightarrow> P & a:x | ~P & a:y"
   29.97  by simp
   29.98  
   29.99  lemma if_type [TC]:
  29.100 @@ -245,7 +245,7 @@
  29.101  
  29.102  (** Splitting IFs in the assumptions **)
  29.103  
  29.104 -lemma split_if_asm: "P(if Q then x else y) <-> (~((Q & ~P(x)) | (~Q & ~P(y))))"
  29.105 +lemma split_if_asm: "P(if Q then x else y) \<longleftrightarrow> (~((Q & ~P(x)) | (~Q & ~P(y))))"
  29.106  by simp
  29.107  
  29.108  lemmas if_splits = split_if split_if_asm
  29.109 @@ -281,7 +281,7 @@
  29.110  
  29.111  subsection{*Rules for Successor*}
  29.112  
  29.113 -lemma succ_iff: "i \<in> succ(j) <-> i=j | i:j"
  29.114 +lemma succ_iff: "i \<in> succ(j) \<longleftrightarrow> i=j | i:j"
  29.115  by (unfold succ_def, blast)
  29.116  
  29.117  lemma succI1 [simp]: "i \<in> succ(i)"
  29.118 @@ -313,7 +313,7 @@
  29.119  (* @{term"succ(b) \<noteq> b"} *)
  29.120  lemmas succ_neq_self = succI1 [THEN mem_imp_not_eq, THEN not_sym]
  29.121  
  29.122 -lemma succ_inject_iff [simp]: "succ(m) = succ(n) <-> m=n"
  29.123 +lemma succ_inject_iff [simp]: "succ(m) = succ(n) \<longleftrightarrow> m=n"
  29.124  by (blast elim: mem_asym elim!: equalityE)
  29.125  
  29.126  lemmas succ_inject = succ_inject_iff [THEN iffD1, dest!]
  29.127 @@ -322,83 +322,83 @@
  29.128  subsection{*Miniscoping of the Bounded Universal Quantifier*}
  29.129  
  29.130  lemma ball_simps1:
  29.131 -     "(\<forall>x\<in>A. P(x) & Q)   <-> (\<forall>x\<in>A. P(x)) & (A=0 | Q)"
  29.132 -     "(\<forall>x\<in>A. P(x) | Q)   <-> ((\<forall>x\<in>A. P(x)) | Q)"
  29.133 -     "(\<forall>x\<in>A. P(x) \<longrightarrow> Q) <-> ((\<exists>x\<in>A. P(x)) \<longrightarrow> Q)"
  29.134 -     "(~(\<forall>x\<in>A. P(x))) <-> (\<exists>x\<in>A. ~P(x))"
  29.135 -     "(\<forall>x\<in>0.P(x)) <-> True"
  29.136 -     "(\<forall>x\<in>succ(i).P(x)) <-> P(i) & (\<forall>x\<in>i. P(x))"
  29.137 -     "(\<forall>x\<in>cons(a,B).P(x)) <-> P(a) & (\<forall>x\<in>B. P(x))"
  29.138 -     "(\<forall>x\<in>RepFun(A,f). P(x)) <-> (\<forall>y\<in>A. P(f(y)))"
  29.139 -     "(\<forall>x\<in>\<Union>(A).P(x)) <-> (\<forall>y\<in>A. \<forall>x\<in>y. P(x))"
  29.140 +     "(\<forall>x\<in>A. P(x) & Q)   \<longleftrightarrow> (\<forall>x\<in>A. P(x)) & (A=0 | Q)"
  29.141 +     "(\<forall>x\<in>A. P(x) | Q)   \<longleftrightarrow> ((\<forall>x\<in>A. P(x)) | Q)"
  29.142 +     "(\<forall>x\<in>A. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P(x)) \<longrightarrow> Q)"
  29.143 +     "(~(\<forall>x\<in>A. P(x))) \<longleftrightarrow> (\<exists>x\<in>A. ~P(x))"
  29.144 +     "(\<forall>x\<in>0.P(x)) \<longleftrightarrow> True"
  29.145 +     "(\<forall>x\<in>succ(i).P(x)) \<longleftrightarrow> P(i) & (\<forall>x\<in>i. P(x))"
  29.146 +     "(\<forall>x\<in>cons(a,B).P(x)) \<longleftrightarrow> P(a) & (\<forall>x\<in>B. P(x))"
  29.147 +     "(\<forall>x\<in>RepFun(A,f). P(x)) \<longleftrightarrow> (\<forall>y\<in>A. P(f(y)))"
  29.148 +     "(\<forall>x\<in>\<Union>(A).P(x)) \<longleftrightarrow> (\<forall>y\<in>A. \<forall>x\<in>y. P(x))"
  29.149  by blast+
  29.150  
  29.151  lemma ball_simps2:
  29.152 -     "(\<forall>x\<in>A. P & Q(x))   <-> (A=0 | P) & (\<forall>x\<in>A. Q(x))"
  29.153 -     "(\<forall>x\<in>A. P | Q(x))   <-> (P | (\<forall>x\<in>A. Q(x)))"
  29.154 -     "(\<forall>x\<in>A. P \<longrightarrow> Q(x)) <-> (P \<longrightarrow> (\<forall>x\<in>A. Q(x)))"
  29.155 +     "(\<forall>x\<in>A. P & Q(x))   \<longleftrightarrow> (A=0 | P) & (\<forall>x\<in>A. Q(x))"
  29.156 +     "(\<forall>x\<in>A. P | Q(x))   \<longleftrightarrow> (P | (\<forall>x\<in>A. Q(x)))"
  29.157 +     "(\<forall>x\<in>A. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x\<in>A. Q(x)))"
  29.158  by blast+
  29.159  
  29.160  lemma ball_simps3:
  29.161 -     "(\<forall>x\<in>Collect(A,Q).P(x)) <-> (\<forall>x\<in>A. Q(x) \<longrightarrow> P(x))"
  29.162 +     "(\<forall>x\<in>Collect(A,Q).P(x)) \<longleftrightarrow> (\<forall>x\<in>A. Q(x) \<longrightarrow> P(x))"
  29.163  by blast+
  29.164  
  29.165  lemmas ball_simps [simp] = ball_simps1 ball_simps2 ball_simps3
  29.166  
  29.167  lemma ball_conj_distrib:
  29.168 -    "(\<forall>x\<in>A. P(x) & Q(x)) <-> ((\<forall>x\<in>A. P(x)) & (\<forall>x\<in>A. Q(x)))"
  29.169 +    "(\<forall>x\<in>A. P(x) & Q(x)) \<longleftrightarrow> ((\<forall>x\<in>A. P(x)) & (\<forall>x\<in>A. Q(x)))"
  29.170  by blast
  29.171  
  29.172  
  29.173  subsection{*Miniscoping of the Bounded Existential Quantifier*}
  29.174  
  29.175  lemma bex_simps1:
  29.176 -     "(\<exists>x\<in>A. P(x) & Q) <-> ((\<exists>x\<in>A. P(x)) & Q)"
  29.177 -     "(\<exists>x\<in>A. P(x) | Q) <-> (\<exists>x\<in>A. P(x)) | (A\<noteq>0 & Q)"
  29.178 -     "(\<exists>x\<in>A. P(x) \<longrightarrow> Q) <-> ((\<forall>x\<in>A. P(x)) \<longrightarrow> (A\<noteq>0 & Q))"
  29.179 -     "(\<exists>x\<in>0.P(x)) <-> False"
  29.180 -     "(\<exists>x\<in>succ(i).P(x)) <-> P(i) | (\<exists>x\<in>i. P(x))"
  29.181 -     "(\<exists>x\<in>cons(a,B).P(x)) <-> P(a) | (\<exists>x\<in>B. P(x))"
  29.182 -     "(\<exists>x\<in>RepFun(A,f). P(x)) <-> (\<exists>y\<in>A. P(f(y)))"
  29.183 -     "(\<exists>x\<in>\<Union>(A).P(x)) <-> (\<exists>y\<in>A. \<exists>x\<in>y.  P(x))"
  29.184 -     "(~(\<exists>x\<in>A. P(x))) <-> (\<forall>x\<in>A. ~P(x))"
  29.185 +     "(\<exists>x\<in>A. P(x) & Q) \<longleftrightarrow> ((\<exists>x\<in>A. P(x)) & Q)"
  29.186 +     "(\<exists>x\<in>A. P(x) | Q) \<longleftrightarrow> (\<exists>x\<in>A. P(x)) | (A\<noteq>0 & Q)"
  29.187 +     "(\<exists>x\<in>A. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<forall>x\<in>A. P(x)) \<longrightarrow> (A\<noteq>0 & Q))"
  29.188 +     "(\<exists>x\<in>0.P(x)) \<longleftrightarrow> False"
  29.189 +     "(\<exists>x\<in>succ(i).P(x)) \<longleftrightarrow> P(i) | (\<exists>x\<in>i. P(x))"
  29.190 +     "(\<exists>x\<in>cons(a,B).P(x)) \<longleftrightarrow> P(a) | (\<exists>x\<in>B. P(x))"
  29.191 +     "(\<exists>x\<in>RepFun(A,f). P(x)) \<longleftrightarrow> (\<exists>y\<in>A. P(f(y)))"
  29.192 +     "(\<exists>x\<in>\<Union>(A).P(x)) \<longleftrightarrow> (\<exists>y\<in>A. \<exists>x\<in>y.  P(x))"
  29.193 +     "(~(\<exists>x\<in>A. P(x))) \<longleftrightarrow> (\<forall>x\<in>A. ~P(x))"
  29.194  by blast+
  29.195  
  29.196  lemma bex_simps2:
  29.197 -     "(\<exists>x\<in>A. P & Q(x)) <-> (P & (\<exists>x\<in>A. Q(x)))"
  29.198 -     "(\<exists>x\<in>A. P | Q(x)) <-> (A\<noteq>0 & P) | (\<exists>x\<in>A. Q(x))"
  29.199 -     "(\<exists>x\<in>A. P \<longrightarrow> Q(x)) <-> ((A=0 | P) \<longrightarrow> (\<exists>x\<in>A. Q(x)))"
  29.200 +     "(\<exists>x\<in>A. P & Q(x)) \<longleftrightarrow> (P & (\<exists>x\<in>A. Q(x)))"
  29.201 +     "(\<exists>x\<in>A. P | Q(x)) \<longleftrightarrow> (A\<noteq>0 & P) | (\<exists>x\<in>A. Q(x))"
  29.202 +     "(\<exists>x\<in>A. P \<longrightarrow> Q(x)) \<longleftrightarrow> ((A=0 | P) \<longrightarrow> (\<exists>x\<in>A. Q(x)))"
  29.203  by blast+
  29.204  
  29.205  lemma bex_simps3:
  29.206 -     "(\<exists>x\<in>Collect(A,Q).P(x)) <-> (\<exists>x\<in>A. Q(x) & P(x))"
  29.207 +     "(\<exists>x\<in>Collect(A,Q).P(x)) \<longleftrightarrow> (\<exists>x\<in>A. Q(x) & P(x))"
  29.208  by blast
  29.209  
  29.210  lemmas bex_simps [simp] = bex_simps1 bex_simps2 bex_simps3
  29.211  
  29.212  lemma bex_disj_distrib:
  29.213 -    "(\<exists>x\<in>A. P(x) | Q(x)) <-> ((\<exists>x\<in>A. P(x)) | (\<exists>x\<in>A. Q(x)))"
  29.214 +    "(\<exists>x\<in>A. P(x) | Q(x)) \<longleftrightarrow> ((\<exists>x\<in>A. P(x)) | (\<exists>x\<in>A. Q(x)))"
  29.215  by blast
  29.216  
  29.217  
  29.218  (** One-point rule for bounded quantifiers: see HOL/Set.ML **)
  29.219  
  29.220 -lemma bex_triv_one_point1 [simp]: "(\<exists>x\<in>A. x=a) <-> (a:A)"
  29.221 +lemma bex_triv_one_point1 [simp]: "(\<exists>x\<in>A. x=a) \<longleftrightarrow> (a:A)"
  29.222  by blast
  29.223  
  29.224 -lemma bex_triv_one_point2 [simp]: "(\<exists>x\<in>A. a=x) <-> (a:A)"
  29.225 +lemma bex_triv_one_point2 [simp]: "(\<exists>x\<in>A. a=x) \<longleftrightarrow> (a:A)"
  29.226  by blast
  29.227  
  29.228 -lemma bex_one_point1 [simp]: "(\<exists>x\<in>A. x=a & P(x)) <-> (a:A & P(a))"
  29.229 +lemma bex_one_point1 [simp]: "(\<exists>x\<in>A. x=a & P(x)) \<longleftrightarrow> (a:A & P(a))"
  29.230  by blast
  29.231  
  29.232 -lemma bex_one_point2 [simp]: "(\<exists>x\<in>A. a=x & P(x)) <-> (a:A & P(a))"
  29.233 +lemma bex_one_point2 [simp]: "(\<exists>x\<in>A. a=x & P(x)) \<longleftrightarrow> (a:A & P(a))"
  29.234  by blast
  29.235  
  29.236 -lemma ball_one_point1 [simp]: "(\<forall>x\<in>A. x=a \<longrightarrow> P(x)) <-> (a:A \<longrightarrow> P(a))"
  29.237 +lemma ball_one_point1 [simp]: "(\<forall>x\<in>A. x=a \<longrightarrow> P(x)) \<longleftrightarrow> (a:A \<longrightarrow> P(a))"
  29.238  by blast
  29.239  
  29.240 -lemma ball_one_point2 [simp]: "(\<forall>x\<in>A. a=x \<longrightarrow> P(x)) <-> (a:A \<longrightarrow> P(a))"
  29.241 +lemma ball_one_point2 [simp]: "(\<forall>x\<in>A. a=x \<longrightarrow> P(x)) \<longleftrightarrow> (a:A \<longrightarrow> P(a))"
  29.242  by blast
  29.243  
  29.244