--- a/src/ZF/Arith.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Arith.thy Tue Mar 06 16:06:52 2012 +0000
@@ -311,7 +311,7 @@
lemma add_lt_elim1: "[| k#+m < k#+n; m \<in> nat; n \<in> nat |] ==> m < n"
by (drule add_lt_elim1_natify, auto)
-lemma zero_less_add: "[| n \<in> nat; m \<in> nat |] ==> 0 < m #+ n <-> (0<m | 0<n)"
+lemma zero_less_add: "[| n \<in> nat; m \<in> nat |] ==> 0 < m #+ n \<longleftrightarrow> (0<m | 0<n)"
by (induct_tac "n", auto)
@@ -441,13 +441,13 @@
(** Lemmas for the CancelNumerals simproc **)
-lemma eq_add_iff: "(u #+ m = u #+ n) <-> (0 #+ m = natify(n))"
+lemma eq_add_iff: "(u #+ m = u #+ n) \<longleftrightarrow> (0 #+ m = natify(n))"
apply auto
apply (blast dest: add_left_cancel_natify)
apply (simp add: add_def)
done
-lemma less_add_iff: "(u #+ m < u #+ n) <-> (0 #+ m < natify(n))"
+lemma less_add_iff: "(u #+ m < u #+ n) \<longleftrightarrow> (0 #+ m < natify(n))"
apply (auto simp add: add_lt_elim1_natify)
apply (drule add_lt_mono1)
apply (auto simp add: add_commute [of u])
@@ -460,7 +460,7 @@
lemma eq_cong2: "u = u' ==> (t==u) == (t==u')"
by auto
-lemma iff_cong2: "u <-> u' ==> (t==u) == (t==u')"
+lemma iff_cong2: "u \<longleftrightarrow> u' ==> (t==u) == (t==u')"
by auto
@@ -543,11 +543,11 @@
lemma lt_succ_eq_0_disj:
"[| m\<in>nat; n\<in>nat |]
- ==> (m < succ(n)) <-> (m = 0 | (\<exists>j\<in>nat. m = succ(j) & j < n))"
+ ==> (m < succ(n)) \<longleftrightarrow> (m = 0 | (\<exists>j\<in>nat. m = succ(j) & j < n))"
by (induct_tac "m", auto)
lemma less_diff_conv [rule_format]:
- "[| j\<in>nat; k\<in>nat |] ==> \<forall>i\<in>nat. (i < j #- k) <-> (i #+ k < j)"
+ "[| j\<in>nat; k\<in>nat |] ==> \<forall>i\<in>nat. (i < j #- k) \<longleftrightarrow> (i #+ k < j)"
by (erule_tac m = k in diff_induct, auto)
lemmas nat_typechecks = rec_type nat_0I nat_1I nat_succI Ord_nat
--- a/src/ZF/ArithSimp.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/ArithSimp.thy Tue Mar 06 16:06:52 2012 +0000
@@ -43,7 +43,7 @@
done
lemma zero_less_diff [simp]:
- "[| m: nat; n: nat |] ==> 0 < (n #- m) <-> m<n"
+ "[| m: nat; n: nat |] ==> 0 < (n #- m) \<longleftrightarrow> m<n"
apply (rule_tac m = m and n = n in diff_induct)
apply (simp_all (no_asm_simp))
done
@@ -301,37 +301,37 @@
apply (simp (no_asm_simp) add: mult_lt_mono2 mult_commute [of _ k])
done
-lemma add_eq_0_iff [iff]: "m#+n = 0 <-> natify(m)=0 & natify(n)=0"
-apply (subgoal_tac "natify (m) #+ natify (n) = 0 <-> natify (m) =0 & natify (n) =0")
+lemma add_eq_0_iff [iff]: "m#+n = 0 \<longleftrightarrow> natify(m)=0 & natify(n)=0"
+apply (subgoal_tac "natify (m) #+ natify (n) = 0 \<longleftrightarrow> natify (m) =0 & natify (n) =0")
apply (rule_tac [2] n = "natify (m) " in natE)
apply (rule_tac [4] n = "natify (n) " in natE)
apply auto
done
-lemma zero_lt_mult_iff [iff]: "0 < m#*n <-> 0 < natify(m) & 0 < natify(n)"
-apply (subgoal_tac "0 < natify (m) #*natify (n) <-> 0 < natify (m) & 0 < natify (n) ")
+lemma zero_lt_mult_iff [iff]: "0 < m#*n \<longleftrightarrow> 0 < natify(m) & 0 < natify(n)"
+apply (subgoal_tac "0 < natify (m) #*natify (n) \<longleftrightarrow> 0 < natify (m) & 0 < natify (n) ")
apply (rule_tac [2] n = "natify (m) " in natE)
apply (rule_tac [4] n = "natify (n) " in natE)
apply (rule_tac [3] n = "natify (n) " in natE)
apply auto
done
-lemma mult_eq_1_iff [iff]: "m#*n = 1 <-> natify(m)=1 & natify(n)=1"
-apply (subgoal_tac "natify (m) #* natify (n) = 1 <-> natify (m) =1 & natify (n) =1")
+lemma mult_eq_1_iff [iff]: "m#*n = 1 \<longleftrightarrow> natify(m)=1 & natify(n)=1"
+apply (subgoal_tac "natify (m) #* natify (n) = 1 \<longleftrightarrow> natify (m) =1 & natify (n) =1")
apply (rule_tac [2] n = "natify (m) " in natE)
apply (rule_tac [4] n = "natify (n) " in natE)
apply auto
done
-lemma mult_is_zero: "[|m: nat; n: nat|] ==> (m #* n = 0) <-> (m = 0 | n = 0)"
+lemma mult_is_zero: "[|m: nat; n: nat|] ==> (m #* n = 0) \<longleftrightarrow> (m = 0 | n = 0)"
apply auto
apply (erule natE)
apply (erule_tac [2] natE, auto)
done
lemma mult_is_zero_natify [iff]:
- "(m #* n = 0) <-> (natify(m) = 0 | natify(n) = 0)"
+ "(m #* n = 0) \<longleftrightarrow> (natify(m) = 0 | natify(n) = 0)"
apply (cut_tac m = "natify (m) " and n = "natify (n) " in mult_is_zero)
apply auto
done
@@ -340,7 +340,7 @@
subsection{*Cancellation Laws for Common Factors in Comparisons*}
lemma mult_less_cancel_lemma:
- "[| k: nat; m: nat; n: nat |] ==> (m#*k < n#*k) <-> (0<k & m<n)"
+ "[| k: nat; m: nat; n: nat |] ==> (m#*k < n#*k) \<longleftrightarrow> (0<k & m<n)"
apply (safe intro!: mult_lt_mono1)
apply (erule natE, auto)
apply (rule not_le_iff_lt [THEN iffD1])
@@ -349,22 +349,22 @@
done
lemma mult_less_cancel2 [simp]:
- "(m#*k < n#*k) <-> (0 < natify(k) & natify(m) < natify(n))"
+ "(m#*k < n#*k) \<longleftrightarrow> (0 < natify(k) & natify(m) < natify(n))"
apply (rule iff_trans)
apply (rule_tac [2] mult_less_cancel_lemma, auto)
done
lemma mult_less_cancel1 [simp]:
- "(k#*m < k#*n) <-> (0 < natify(k) & natify(m) < natify(n))"
+ "(k#*m < k#*n) \<longleftrightarrow> (0 < natify(k) & natify(m) < natify(n))"
apply (simp (no_asm) add: mult_less_cancel2 mult_commute [of k])
done
-lemma mult_le_cancel2 [simp]: "(m#*k \<le> n#*k) <-> (0 < natify(k) \<longrightarrow> natify(m) \<le> natify(n))"
+lemma mult_le_cancel2 [simp]: "(m#*k \<le> n#*k) \<longleftrightarrow> (0 < natify(k) \<longrightarrow> natify(m) \<le> natify(n))"
apply (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym])
apply auto
done
-lemma mult_le_cancel1 [simp]: "(k#*m \<le> k#*n) <-> (0 < natify(k) \<longrightarrow> natify(m) \<le> natify(n))"
+lemma mult_le_cancel1 [simp]: "(k#*m \<le> k#*n) \<longleftrightarrow> (0 < natify(k) \<longrightarrow> natify(m) \<le> natify(n))"
apply (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym])
apply auto
done
@@ -372,23 +372,23 @@
lemma mult_le_cancel_le1: "k \<in> nat ==> k #* m \<le> k \<longleftrightarrow> (0 < k \<longrightarrow> natify(m) \<le> 1)"
by (cut_tac k = k and m = m and n = 1 in mult_le_cancel1, auto)
-lemma Ord_eq_iff_le: "[| Ord(m); Ord(n) |] ==> m=n <-> (m \<le> n & n \<le> m)"
+lemma Ord_eq_iff_le: "[| Ord(m); Ord(n) |] ==> m=n \<longleftrightarrow> (m \<le> n & n \<le> m)"
by (blast intro: le_anti_sym)
lemma mult_cancel2_lemma:
- "[| k: nat; m: nat; n: nat |] ==> (m#*k = n#*k) <-> (m=n | k=0)"
+ "[| k: nat; m: nat; n: nat |] ==> (m#*k = n#*k) \<longleftrightarrow> (m=n | k=0)"
apply (simp (no_asm_simp) add: Ord_eq_iff_le [of "m#*k"] Ord_eq_iff_le [of m])
apply (auto simp add: Ord_0_lt_iff)
done
lemma mult_cancel2 [simp]:
- "(m#*k = n#*k) <-> (natify(m) = natify(n) | natify(k) = 0)"
+ "(m#*k = n#*k) \<longleftrightarrow> (natify(m) = natify(n) | natify(k) = 0)"
apply (rule iff_trans)
apply (rule_tac [2] mult_cancel2_lemma, auto)
done
lemma mult_cancel1 [simp]:
- "(k#*m = k#*n) <-> (natify(m) = natify(n) | natify(k) = 0)"
+ "(k#*m = k#*n) \<longleftrightarrow> (natify(m) = natify(n) | natify(k) = 0)"
apply (simp (no_asm) add: mult_cancel2 mult_commute [of k])
done
@@ -493,7 +493,7 @@
done
lemma less_iff_succ_add:
- "[| m: nat; n: nat |] ==> (m<n) <-> (\<exists>k\<in>nat. n = succ(m#+k))"
+ "[| m: nat; n: nat |] ==> (m<n) \<longleftrightarrow> (\<exists>k\<in>nat. n = succ(m#+k))"
by (auto intro: less_imp_succ_add)
lemma add_lt_elim2:
@@ -508,11 +508,11 @@
subsubsection{*More Lemmas About Difference*}
lemma diff_is_0_lemma:
- "[| m: nat; n: nat |] ==> m #- n = 0 <-> m \<le> n"
+ "[| m: nat; n: nat |] ==> m #- n = 0 \<longleftrightarrow> m \<le> n"
apply (rule_tac m = m and n = n in diff_induct, simp_all)
done
-lemma diff_is_0_iff: "m #- n = 0 <-> natify(m) \<le> natify(n)"
+lemma diff_is_0_iff: "m #- n = 0 \<longleftrightarrow> natify(m) \<le> natify(n)"
by (simp add: diff_is_0_lemma [symmetric])
lemma nat_lt_imp_diff_eq_0:
@@ -521,7 +521,7 @@
lemma raw_nat_diff_split:
"[| a:nat; b:nat |] ==>
- (P(a #- b)) <-> ((a < b \<longrightarrow>P(0)) & (\<forall>d\<in>nat. a = b #+ d \<longrightarrow> P(d)))"
+ (P(a #- b)) \<longleftrightarrow> ((a < b \<longrightarrow>P(0)) & (\<forall>d\<in>nat. a = b #+ d \<longrightarrow> P(d)))"
apply (case_tac "a < b")
apply (force simp add: nat_lt_imp_diff_eq_0)
apply (rule iffI, force, simp)
@@ -530,7 +530,7 @@
done
lemma nat_diff_split:
- "(P(a #- b)) <->
+ "(P(a #- b)) \<longleftrightarrow>
(natify(a) < natify(b) \<longrightarrow>P(0)) & (\<forall>d\<in>nat. natify(a) = b #+ d \<longrightarrow> P(d))"
apply (cut_tac P=P and a="natify(a)" and b="natify(b)" in raw_nat_diff_split)
apply simp_all
@@ -559,7 +559,7 @@
done
-lemma diff_lt_iff_lt: "[|i\<le>k; j\<in>nat; k\<in>nat|] ==> (k#-i) < (k#-j) <-> j<i"
+lemma diff_lt_iff_lt: "[|i\<le>k; j\<in>nat; k\<in>nat|] ==> (k#-i) < (k#-j) \<longleftrightarrow> j<i"
apply (frule le_in_nat, assumption)
apply (blast intro: lt_imp_diff_lt diff_lt_imp_lt)
done
--- a/src/ZF/Bin.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Bin.thy Tue Mar 06 16:06:52 2012 +0000
@@ -346,7 +346,7 @@
lemma eq_integ_of_eq:
"[| v: bin; w: bin |]
- ==> ((integ_of(v)) = integ_of(w)) <->
+ ==> ((integ_of(v)) = integ_of(w)) \<longleftrightarrow>
iszero (integ_of (bin_add (v, bin_minus(w))))"
apply (unfold iszero_def)
apply (simp add: zcompare_rls integ_of_add integ_of_minus)
@@ -363,7 +363,7 @@
lemma iszero_integ_of_BIT:
"[| w: bin; x: bool |]
- ==> iszero (integ_of (w BIT x)) <-> (x=0 & iszero (integ_of(w)))"
+ ==> iszero (integ_of (w BIT x)) \<longleftrightarrow> (x=0 & iszero (integ_of(w)))"
apply (unfold iszero_def, simp)
apply (subgoal_tac "integ_of (w) \<in> int")
apply typecheck
@@ -374,7 +374,7 @@
done
lemma iszero_integ_of_0:
- "w: bin ==> iszero (integ_of (w BIT 0)) <-> iszero (integ_of(w))"
+ "w: bin ==> iszero (integ_of (w BIT 0)) \<longleftrightarrow> iszero (integ_of(w))"
by (simp only: iszero_integ_of_BIT, blast)
lemma iszero_integ_of_1: "w: bin ==> ~ iszero (integ_of (w BIT 1))"
@@ -387,7 +387,7 @@
lemma less_integ_of_eq_neg:
"[| v: bin; w: bin |]
==> integ_of(v) $< integ_of(w)
- <-> znegative (integ_of (bin_add (v, bin_minus(w))))"
+ \<longleftrightarrow> znegative (integ_of (bin_add (v, bin_minus(w))))"
apply (unfold zless_def zdiff_def)
apply (simp add: integ_of_minus integ_of_add)
done
@@ -400,7 +400,7 @@
lemma neg_integ_of_BIT:
"[| w: bin; x: bool |]
- ==> znegative (integ_of (w BIT x)) <-> znegative (integ_of(w))"
+ ==> znegative (integ_of (w BIT x)) \<longleftrightarrow> znegative (integ_of(w))"
apply simp
apply (subgoal_tac "integ_of (w) \<in> int")
apply typecheck
@@ -416,7 +416,7 @@
(** Less-than-or-equals (<=) **)
lemma le_integ_of_eq_not_less:
- "(integ_of(x) $<= (integ_of(w))) <-> ~ (integ_of(w) $< (integ_of(x)))"
+ "(integ_of(x) $<= (integ_of(w))) \<longleftrightarrow> ~ (integ_of(w) $< (integ_of(x)))"
by (simp add: not_zless_iff_zle [THEN iff_sym])
@@ -509,7 +509,7 @@
lemma zdiff_self [simp]: "x $- x = #0"
by (simp add: zdiff_def)
-lemma znegative_iff_zless_0: "k: int ==> znegative(k) <-> k $< #0"
+lemma znegative_iff_zless_0: "k: int ==> znegative(k) \<longleftrightarrow> k $< #0"
by (simp add: zless_def)
lemma zero_zless_imp_znegative_zminus: "[|#0 $< k; k: int|] ==> znegative($-k)"
@@ -545,7 +545,7 @@
lemma int_of_nat_of_if: "$# nat_of(z) = (if #0 $<= z then intify(z) else #0)"
by (simp add: int_of_nat_of znegative_iff_zless_0 not_zle_iff_zless)
-lemma zless_nat_iff_int_zless: "[| m: nat; z: int |] ==> (m < nat_of(z)) <-> ($#m $< z)"
+lemma zless_nat_iff_int_zless: "[| m: nat; z: int |] ==> (m < nat_of(z)) \<longleftrightarrow> ($#m $< z)"
apply (case_tac "znegative (z) ")
apply (erule_tac [2] not_zneg_nat_of [THEN subst])
apply (auto dest: zless_trans dest!: zero_zle_int_of [THEN zle_zless_trans]
@@ -556,7 +556,7 @@
(** nat_of and zless **)
(*An alternative condition is @{term"$#0 \<subseteq> w"} *)
-lemma zless_nat_conj_lemma: "$#0 $< z ==> (nat_of(w) < nat_of(z)) <-> (w $< z)"
+lemma zless_nat_conj_lemma: "$#0 $< z ==> (nat_of(w) < nat_of(z)) \<longleftrightarrow> (w $< z)"
apply (rule iff_trans)
apply (rule zless_int_of [THEN iff_sym])
apply (auto simp add: int_of_nat_of_if simp del: zless_int_of)
@@ -564,7 +564,7 @@
apply (blast intro: zless_zle_trans)
done
-lemma zless_nat_conj: "(nat_of(w) < nat_of(z)) <-> ($#0 $< z & w $< z)"
+lemma zless_nat_conj: "(nat_of(w) < nat_of(z)) \<longleftrightarrow> ($#0 $< z & w $< z)"
apply (case_tac "$#0 $< z")
apply (auto simp add: zless_nat_conj_lemma nat_le_int0 not_zless_iff_zle)
done
@@ -575,24 +575,24 @@
Conditional rewrite rules are tried after unconditional ones, so a rule
like eq_nat_number_of will be tried first to eliminate #mm=#nn.]
lemma integ_of_reorient [simp]:
- "True ==> (integ_of(w) = x) <-> (x = integ_of(w))"
+ "True ==> (integ_of(w) = x) \<longleftrightarrow> (x = integ_of(w))"
by auto
*)
lemma integ_of_minus_reorient [simp]:
- "(integ_of(w) = $- x) <-> ($- x = integ_of(w))"
+ "(integ_of(w) = $- x) \<longleftrightarrow> ($- x = integ_of(w))"
by auto
lemma integ_of_add_reorient [simp]:
- "(integ_of(w) = x $+ y) <-> (x $+ y = integ_of(w))"
+ "(integ_of(w) = x $+ y) \<longleftrightarrow> (x $+ y = integ_of(w))"
by auto
lemma integ_of_diff_reorient [simp]:
- "(integ_of(w) = x $- y) <-> (x $- y = integ_of(w))"
+ "(integ_of(w) = x $- y) \<longleftrightarrow> (x $- y = integ_of(w))"
by auto
lemma integ_of_mult_reorient [simp]:
- "(integ_of(w) = x $* y) <-> (x $* y = integ_of(w))"
+ "(integ_of(w) = x $* y) \<longleftrightarrow> (x $* y = integ_of(w))"
by auto
end
--- a/src/ZF/Bool.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Bool.thy Tue Mar 06 16:06:52 2012 +0000
@@ -164,10 +164,10 @@
lemma [simp,TC]: "bool_of_o(P) \<in> bool"
by (simp add: bool_of_o_def)
-lemma [simp]: "(bool_of_o(P) = 1) <-> P"
+lemma [simp]: "(bool_of_o(P) = 1) \<longleftrightarrow> P"
by (simp add: bool_of_o_def)
-lemma [simp]: "(bool_of_o(P) = 0) <-> ~P"
+lemma [simp]: "(bool_of_o(P) = 0) \<longleftrightarrow> ~P"
by (simp add: bool_of_o_def)
end
--- a/src/ZF/Cardinal.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Cardinal.thy Tue Mar 06 16:06:52 2012 +0000
@@ -138,7 +138,7 @@
"[| X \<approx> Y; [| X \<lesssim> Y; Y \<lesssim> X |] ==> P |] ==> P"
by (blast intro: eqpoll_imp_lepoll eqpoll_sym)
-lemma eqpoll_iff: "X \<approx> Y <-> X \<lesssim> Y & Y \<lesssim> X"
+lemma eqpoll_iff: "X \<approx> Y \<longleftrightarrow> X \<lesssim> Y & Y \<lesssim> X"
by (blast intro: eqpollI elim!: eqpollE)
lemma lepoll_0_is_0: "A \<lesssim> 0 ==> A = 0"
@@ -149,7 +149,7 @@
(*@{term"0 \<lesssim> Y"}*)
lemmas empty_lepollI = empty_subsetI [THEN subset_imp_lepoll]
-lemma lepoll_0_iff: "A \<lesssim> 0 <-> A=0"
+lemma lepoll_0_iff: "A \<lesssim> 0 \<longleftrightarrow> A=0"
by (blast intro: lepoll_0_is_0 lepoll_refl)
lemma Un_lepoll_Un:
@@ -161,7 +161,7 @@
(*A eqpoll 0 ==> A=0*)
lemmas eqpoll_0_is_0 = eqpoll_imp_lepoll [THEN lepoll_0_is_0]
-lemma eqpoll_0_iff: "A \<approx> 0 <-> A=0"
+lemma eqpoll_0_iff: "A \<approx> 0 \<longleftrightarrow> A=0"
by (blast intro: eqpoll_0_is_0 eqpoll_refl)
lemma eqpoll_disjoint_Un:
@@ -188,7 +188,7 @@
apply (blast intro: well_ord_rvimage)
done
-lemma lepoll_iff_leqpoll: "A \<lesssim> B <-> A \<prec> B | A \<approx> B"
+lemma lepoll_iff_leqpoll: "A \<lesssim> B \<longleftrightarrow> A \<prec> B | A \<approx> B"
apply (unfold lesspoll_def)
apply (blast intro!: eqpollI elim!: eqpollE)
done
@@ -288,7 +288,7 @@
(*Not needed for simplification, but helpful below*)
lemma Least_cong:
- "(!!y. P(y) <-> Q(y)) ==> (LEAST x. P(x)) = (LEAST x. Q(x))"
+ "(!!y. P(y) \<longleftrightarrow> Q(y)) ==> (LEAST x. P(x)) = (LEAST x. Q(x))"
by simp
(*Need AC to get @{term"X \<lesssim> Y ==> |X| \<le> |Y|"}; see well_ord_lepoll_imp_Card_le
@@ -319,7 +319,7 @@
done
lemma well_ord_cardinal_eqpoll_iff:
- "[| well_ord(X,r); well_ord(Y,s) |] ==> |X| = |Y| <-> X \<approx> Y"
+ "[| well_ord(X,r); well_ord(Y,s) |] ==> |X| = |Y| \<longleftrightarrow> X \<approx> Y"
by (blast intro: cardinal_cong well_ord_cardinal_eqE)
@@ -358,7 +358,7 @@
done
(*The cardinals are the initial ordinals*)
-lemma Card_iff_initial: "Card(K) <-> Ord(K) & (\<forall>j. j<K \<longrightarrow> ~ j \<approx> K)"
+lemma Card_iff_initial: "Card(K) \<longleftrightarrow> Ord(K) & (\<forall>j. j<K \<longrightarrow> ~ j \<approx> K)"
apply (safe intro!: CardI Card_is_Ord)
prefer 2 apply blast
apply (unfold Card_def cardinal_def)
@@ -430,10 +430,10 @@
apply (simp (no_asm_simp) add: cardinal_lt_imp_lt Card_is_Ord Card_cardinal_eq)
done
-lemma Card_lt_iff: "[| Ord(i); Card(K) |] ==> (|i| < K) <-> (i < K)"
+lemma Card_lt_iff: "[| Ord(i); Card(K) |] ==> (|i| < K) \<longleftrightarrow> (i < K)"
by (blast intro: Card_lt_imp_lt Ord_cardinal_le [THEN lt_trans1])
-lemma Card_le_iff: "[| Ord(i); Card(K) |] ==> (K \<le> |i|) <-> (K \<le> i)"
+lemma Card_le_iff: "[| Ord(i); Card(K) |] ==> (K \<le> |i|) \<longleftrightarrow> (K \<le> i)"
by (simp add: Card_lt_iff Card_is_Ord Ord_cardinal not_lt_iff_le [THEN iff_sym])
(*Can use AC or finiteness to discharge first premise*)
@@ -510,7 +510,7 @@
apply (blast intro!: succ_leI dest!: succ_lepoll_succD)
done
-lemma nat_eqpoll_iff: "[| m:nat; n: nat |] ==> m \<approx> n <-> m = n"
+lemma nat_eqpoll_iff: "[| m:nat; n: nat |] ==> m \<approx> n \<longleftrightarrow> m = n"
apply (rule iffI)
apply (blast intro: nat_lepoll_imp_le le_anti_sym elim!: eqpollE)
apply (simp add: eqpoll_refl)
@@ -573,7 +573,7 @@
apply (blast intro!: inj_not_surj_succ)
done
-lemma lesspoll_succ_iff: "m:nat ==> A \<prec> succ(m) <-> A \<lesssim> m"
+lemma lesspoll_succ_iff: "m:nat ==> A \<prec> succ(m) \<longleftrightarrow> A \<lesssim> m"
by (blast intro!: lepoll_imp_lesspoll_succ lesspoll_succ_imp_lepoll)
lemma lepoll_succ_disj: "[| A \<lesssim> succ(m); m:nat |] ==> A \<lesssim> m | A \<approx> succ(m)"
@@ -602,7 +602,7 @@
apply (rule Ord_succ_subsetI [THEN subset_imp_lepoll], assumption+)
done
-lemma Ord_nat_eqpoll_iff: "[| Ord(i); n:nat |] ==> i \<approx> n <-> i=n"
+lemma Ord_nat_eqpoll_iff: "[| Ord(i); n:nat |] ==> i \<approx> n \<longleftrightarrow> i=n"
apply (rule iffI)
prefer 2 apply (simp add: eqpoll_refl)
apply (rule Ord_linear_lt [of i n])
@@ -647,11 +647,11 @@
by (simp add: eqpoll_iff cons_lepoll_cong)
lemma cons_lepoll_cons_iff:
- "[| a \<notin> A; b \<notin> B |] ==> cons(a,A) \<lesssim> cons(b,B) <-> A \<lesssim> B"
+ "[| a \<notin> A; b \<notin> B |] ==> cons(a,A) \<lesssim> cons(b,B) \<longleftrightarrow> A \<lesssim> B"
by (blast intro: cons_lepoll_cong cons_lepoll_consD)
lemma cons_eqpoll_cons_iff:
- "[| a \<notin> A; b \<notin> B |] ==> cons(a,A) \<approx> cons(b,B) <-> A \<approx> B"
+ "[| a \<notin> A; b \<notin> B |] ==> cons(a,A) \<approx> cons(b,B) \<longleftrightarrow> A \<approx> B"
by (blast intro: cons_eqpoll_cong cons_eqpoll_consD)
lemma singleton_eqpoll_1: "{a} \<approx> 1"
@@ -813,10 +813,10 @@
apply (erule Finite_cons)
done
-lemma Finite_cons_iff [iff]: "Finite(cons(y,x)) <-> Finite(x)"
+lemma Finite_cons_iff [iff]: "Finite(cons(y,x)) \<longleftrightarrow> Finite(x)"
by (blast intro: Finite_cons subset_Finite)
-lemma Finite_succ_iff [iff]: "Finite(succ(x)) <-> Finite(x)"
+lemma Finite_succ_iff [iff]: "Finite(succ(x)) \<longleftrightarrow> Finite(x)"
by (simp add: succ_def)
lemma nat_le_infinite_Ord:
@@ -859,7 +859,7 @@
lemma Finite_Fin: "[| Finite(A); A \<subseteq> X |] ==> A \<in> Fin(X)"
by (unfold Finite_def, blast intro: Finite_Fin_lemma)
-lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) <-> Finite(B)"
+lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) \<longleftrightarrow> Finite(B)"
apply (unfold Finite_def)
apply (blast intro: eqpoll_trans eqpoll_sym)
done
@@ -888,7 +888,7 @@
lemma Fin_into_Finite: "A \<in> Fin(U) ==> Finite(A)"
by (fast intro!: Finite_0 Finite_cons elim: Fin_induct)
-lemma Finite_Fin_iff: "Finite(A) <-> A \<in> Fin(A)"
+lemma Finite_Fin_iff: "Finite(A) \<longleftrightarrow> A \<in> Fin(A)"
by (blast intro: Finite_into_Fin Fin_into_Finite)
lemma Finite_Un: "[| Finite(A); Finite(B) |] ==> Finite(A \<union> B)"
@@ -897,7 +897,7 @@
intro: Un_upper1 [THEN Fin_mono, THEN subsetD]
Un_upper2 [THEN Fin_mono, THEN subsetD])
-lemma Finite_Un_iff [simp]: "Finite(A \<union> B) <-> (Finite(A) & Finite(B))"
+lemma Finite_Un_iff [simp]: "Finite(A \<union> B) \<longleftrightarrow> (Finite(A) & Finite(B))"
by (blast intro: subset_Finite Finite_Un)
text{*The converse must hold too.*}
@@ -961,7 +961,7 @@
text{*I don't know why, but if the premise is expressed using meta-connectives
then the simplifier cannot prove it automatically in conditional rewriting.*}
lemma Finite_RepFun_iff:
- "(\<forall>x y. f(x)=f(y) \<longrightarrow> x=y) ==> Finite(RepFun(A,f)) <-> Finite(A)"
+ "(\<forall>x y. f(x)=f(y) \<longrightarrow> x=y) ==> Finite(RepFun(A,f)) \<longleftrightarrow> Finite(A)"
by (blast intro: Finite_RepFun Finite_RepFun_iff_lemma [of _ f])
lemma Finite_Pow: "Finite(A) ==> Finite(Pow(A))"
@@ -975,7 +975,7 @@
apply (blast intro: subset_Finite)
done
-lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) <-> Finite(A)"
+lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) \<longleftrightarrow> Finite(A)"
by (blast intro: Finite_Pow Finite_Pow_imp_Finite)
--- a/src/ZF/CardinalArith.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/CardinalArith.thy Tue Mar 06 16:06:52 2012 +0000
@@ -39,11 +39,11 @@
of @{term K}*}
"csucc(K) == LEAST L. Card(L) & K<L"
-notation (xsymbols output)
+notation (xsymbols)
cadd (infixl "\<oplus>" 65) and
cmult (infixl "\<otimes>" 70)
-notation (HTML output)
+notation (HTML)
cadd (infixl "\<oplus>" 65) and
cmult (infixl "\<otimes>" 70)
@@ -109,7 +109,7 @@
apply auto
done
-lemma cadd_commute: "i |+| j = j |+| i"
+lemma cadd_commute: "i \<oplus> j = j \<oplus> i"
apply (unfold cadd_def)
apply (rule sum_commute_eqpoll [THEN cardinal_cong])
done
@@ -125,7 +125,7 @@
(*Unconditional version requires AC*)
lemma well_ord_cadd_assoc:
"[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]
- ==> (i |+| j) |+| k = i |+| (j |+| k)"
+ ==> (i \<oplus> j) \<oplus> k = i \<oplus> (j \<oplus> k)"
apply (unfold cadd_def)
apply (rule cardinal_cong)
apply (rule eqpoll_trans)
@@ -145,7 +145,7 @@
apply (rule bij_0_sum)
done
-lemma cadd_0 [simp]: "Card(K) ==> 0 |+| K = K"
+lemma cadd_0 [simp]: "Card(K) ==> 0 \<oplus> K = K"
apply (unfold cadd_def)
apply (simp add: sum_0_eqpoll [THEN cardinal_cong] Card_cardinal_eq)
done
@@ -161,7 +161,7 @@
(*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
lemma cadd_le_self:
- "[| Card(K); Ord(L) |] ==> K \<le> (K |+| L)"
+ "[| Card(K); Ord(L) |] ==> K \<le> (K \<oplus> L)"
apply (unfold cadd_def)
apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le],
assumption)
@@ -182,7 +182,7 @@
done
lemma cadd_le_mono:
- "[| K' \<le> K; L' \<le> L |] ==> (K' |+| L') \<le> (K |+| L)"
+ "[| K' \<le> K; L' \<le> L |] ==> (K' \<oplus> L') \<le> (K \<oplus> L)"
apply (unfold cadd_def)
apply (safe dest!: le_subset_iff [THEN iffD1])
apply (rule well_ord_lepoll_imp_Card_le)
@@ -204,7 +204,7 @@
(*Pulling the succ(...) outside the |...| requires m, n: nat *)
(*Unconditional version requires AC*)
lemma cadd_succ_lemma:
- "[| Ord(m); Ord(n) |] ==> succ(m) |+| n = |succ(m |+| n)|"
+ "[| Ord(m); Ord(n) |] ==> succ(m) \<oplus> n = |succ(m \<oplus> n)|"
apply (unfold cadd_def)
apply (rule sum_succ_eqpoll [THEN cardinal_cong, THEN trans])
apply (rule succ_eqpoll_cong [THEN cardinal_cong])
@@ -212,7 +212,7 @@
apply (blast intro: well_ord_radd well_ord_Memrel)
done
-lemma nat_cadd_eq_add: "[| m: nat; n: nat |] ==> m |+| n = m#+n"
+lemma nat_cadd_eq_add: "[| m: nat; n: nat |] ==> m \<oplus> n = m#+n"
apply (induct_tac m)
apply (simp add: nat_into_Card [THEN cadd_0])
apply (simp add: cadd_succ_lemma nat_into_Card [THEN Card_cardinal_eq])
@@ -231,7 +231,7 @@
auto)
done
-lemma cmult_commute: "i |*| j = j |*| i"
+lemma cmult_commute: "i \<otimes> j = j \<otimes> i"
apply (unfold cmult_def)
apply (rule prod_commute_eqpoll [THEN cardinal_cong])
done
@@ -247,7 +247,7 @@
(*Unconditional version requires AC*)
lemma well_ord_cmult_assoc:
"[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]
- ==> (i |*| j) |*| k = i |*| (j |*| k)"
+ ==> (i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
apply (unfold cmult_def)
apply (rule cardinal_cong)
apply (rule eqpoll_trans)
@@ -269,7 +269,7 @@
lemma well_ord_cadd_cmult_distrib:
"[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]
- ==> (i |+| j) |*| k = (i |*| k) |+| (j |*| k)"
+ ==> (i \<oplus> j) \<otimes> k = (i \<otimes> k) \<oplus> (j \<otimes> k)"
apply (unfold cadd_def cmult_def)
apply (rule cardinal_cong)
apply (rule eqpoll_trans)
@@ -290,7 +290,7 @@
apply (rule lam_bijective, safe)
done
-lemma cmult_0 [simp]: "0 |*| i = 0"
+lemma cmult_0 [simp]: "0 \<otimes> i = 0"
by (simp add: cmult_def prod_0_eqpoll [THEN cardinal_cong])
subsubsection{*1 is the identity for multiplication*}
@@ -301,7 +301,7 @@
apply (rule singleton_prod_bij [THEN bij_converse_bij])
done
-lemma cmult_1 [simp]: "Card(K) ==> 1 |*| K = K"
+lemma cmult_1 [simp]: "Card(K) ==> 1 \<otimes> K = K"
apply (unfold cmult_def succ_def)
apply (simp add: prod_singleton_eqpoll [THEN cardinal_cong] Card_cardinal_eq)
done
@@ -314,7 +314,7 @@
done
(*Could probably weaken the premise to well_ord(K,r), or remove using AC*)
-lemma cmult_square_le: "Card(K) ==> K \<le> K |*| K"
+lemma cmult_square_le: "Card(K) ==> K \<le> K \<otimes> K"
apply (unfold cmult_def)
apply (rule le_trans)
apply (rule_tac [2] well_ord_lepoll_imp_Card_le)
@@ -332,7 +332,7 @@
(*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
lemma cmult_le_self:
- "[| Card(K); Ord(L); 0<L |] ==> K \<le> (K |*| L)"
+ "[| Card(K); Ord(L); 0<L |] ==> K \<le> (K \<otimes> L)"
apply (unfold cmult_def)
apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le])
apply assumption
@@ -353,7 +353,7 @@
done
lemma cmult_le_mono:
- "[| K' \<le> K; L' \<le> L |] ==> (K' |*| L') \<le> (K |*| L)"
+ "[| K' \<le> K; L' \<le> L |] ==> (K' \<otimes> L') \<le> (K \<otimes> L)"
apply (unfold cmult_def)
apply (safe dest!: le_subset_iff [THEN iffD1])
apply (rule well_ord_lepoll_imp_Card_le)
@@ -374,7 +374,7 @@
(*Unconditional version requires AC*)
lemma cmult_succ_lemma:
- "[| Ord(m); Ord(n) |] ==> succ(m) |*| n = n |+| (m |*| n)"
+ "[| Ord(m); Ord(n) |] ==> succ(m) \<otimes> n = n \<oplus> (m \<otimes> n)"
apply (unfold cmult_def cadd_def)
apply (rule prod_succ_eqpoll [THEN cardinal_cong, THEN trans])
apply (rule cardinal_cong [symmetric])
@@ -382,12 +382,12 @@
apply (blast intro: well_ord_rmult well_ord_Memrel)
done
-lemma nat_cmult_eq_mult: "[| m: nat; n: nat |] ==> m |*| n = m#*n"
+lemma nat_cmult_eq_mult: "[| m: nat; n: nat |] ==> m \<otimes> n = m#*n"
apply (induct_tac m)
apply (simp_all add: cmult_succ_lemma nat_cadd_eq_add)
done
-lemma cmult_2: "Card(n) ==> 2 |*| n = n |+| n"
+lemma cmult_2: "Card(n) ==> 2 \<otimes> n = n \<oplus> n"
by (simp add: cmult_succ_lemma Card_is_Ord cadd_commute [of _ 0])
lemma sum_lepoll_prod: "2 \<lesssim> C ==> B+B \<lesssim> C*B"
@@ -555,7 +555,7 @@
(*Kunen: "each <x,y>: K*K has no more than z*z predecessors..." (page 29) *)
lemma ordermap_csquare_le:
"[| Limit(K); x<K; y<K; z=succ(x \<union> y) |]
- ==> | ordermap(K*K, csquare_rel(K)) ` <x,y> | \<le> |succ(z)| |*| |succ(z)|"
+ ==> | ordermap(K*K, csquare_rel(K)) ` <x,y> | \<le> |succ(z)| \<otimes> |succ(z)|"
apply (unfold cmult_def)
apply (rule well_ord_rmult [THEN well_ord_lepoll_imp_Card_le])
apply (rule Ord_cardinal [THEN well_ord_Memrel])+
@@ -575,7 +575,7 @@
(*Kunen: "... so the order type is @{text"\<le>"} K" *)
lemma ordertype_csquare_le:
- "[| InfCard(K); \<forall>y\<in>K. InfCard(y) \<longrightarrow> y |*| y = y |]
+ "[| InfCard(K); \<forall>y\<in>K. InfCard(y) \<longrightarrow> y \<otimes> y = y |]
==> ordertype(K*K, csquare_rel(K)) \<le> K"
apply (frule InfCard_is_Card [THEN Card_is_Ord])
apply (rule all_lt_imp_le, assumption)
@@ -604,7 +604,7 @@
done
(*Main result: Kunen's Theorem 10.12*)
-lemma InfCard_csquare_eq: "InfCard(K) ==> K |*| K = K"
+lemma InfCard_csquare_eq: "InfCard(K) ==> K \<otimes> K = K"
apply (frule InfCard_is_Card [THEN Card_is_Ord])
apply (erule rev_mp)
apply (erule_tac i=K in trans_induct)
@@ -639,7 +639,7 @@
subsubsection{*Toward's Kunen's Corollary 10.13 (1)*}
-lemma InfCard_le_cmult_eq: "[| InfCard(K); L \<le> K; 0<L |] ==> K |*| L = K"
+lemma InfCard_le_cmult_eq: "[| InfCard(K); L \<le> K; 0<L |] ==> K \<otimes> L = K"
apply (rule le_anti_sym)
prefer 2
apply (erule ltE, blast intro: cmult_le_self InfCard_is_Card)
@@ -649,7 +649,7 @@
done
(*Corollary 10.13 (1), for cardinal multiplication*)
-lemma InfCard_cmult_eq: "[| InfCard(K); InfCard(L) |] ==> K |*| L = K \<union> L"
+lemma InfCard_cmult_eq: "[| InfCard(K); InfCard(L) |] ==> K \<otimes> L = K \<union> L"
apply (rule_tac i = K and j = L in Ord_linear_le)
apply (typecheck add: InfCard_is_Card Card_is_Ord)
apply (rule cmult_commute [THEN ssubst])
@@ -658,13 +658,13 @@
subset_Un_iff2 [THEN iffD1] le_imp_subset)
done
-lemma InfCard_cdouble_eq: "InfCard(K) ==> K |+| K = K"
+lemma InfCard_cdouble_eq: "InfCard(K) ==> K \<oplus> K = K"
apply (simp add: cmult_2 [symmetric] InfCard_is_Card cmult_commute)
apply (simp add: InfCard_le_cmult_eq InfCard_is_Limit Limit_has_0 Limit_has_succ)
done
(*Corollary 10.13 (1), for cardinal addition*)
-lemma InfCard_le_cadd_eq: "[| InfCard(K); L \<le> K |] ==> K |+| L = K"
+lemma InfCard_le_cadd_eq: "[| InfCard(K); L \<le> K |] ==> K \<oplus> L = K"
apply (rule le_anti_sym)
prefer 2
apply (erule ltE, blast intro: cadd_le_self InfCard_is_Card)
@@ -673,7 +673,7 @@
apply (simp add: InfCard_cdouble_eq)
done
-lemma InfCard_cadd_eq: "[| InfCard(K); InfCard(L) |] ==> K |+| L = K \<union> L"
+lemma InfCard_cadd_eq: "[| InfCard(K); InfCard(L) |] ==> K \<oplus> L = K \<union> L"
apply (rule_tac i = K and j = L in Ord_linear_le)
apply (typecheck add: InfCard_is_Card Card_is_Ord)
apply (rule cadd_commute [THEN ssubst])
@@ -704,7 +704,7 @@
(*Allows selective unfolding. Less work than deriving intro/elim rules*)
lemma jump_cardinal_iff:
- "i \<in> jump_cardinal(K) <->
+ "i \<in> jump_cardinal(K) \<longleftrightarrow>
(\<exists>r X. r \<subseteq> K*K & X \<subseteq> K & well_ord(X,r) & i = ordertype(X,r))"
apply (unfold jump_cardinal_def)
apply (blast del: subsetI)
@@ -766,7 +766,7 @@
apply (blast intro: Card_is_Ord)+
done
-lemma lt_csucc_iff: "[| Ord(i); Card(K) |] ==> i < csucc(K) <-> |i| \<le> K"
+lemma lt_csucc_iff: "[| Ord(i); Card(K) |] ==> i < csucc(K) \<longleftrightarrow> |i| \<le> K"
apply (rule iffI)
apply (rule_tac [2] Card_lt_imp_lt)
apply (erule_tac [2] lt_trans1)
@@ -778,7 +778,7 @@
done
lemma Card_lt_csucc_iff:
- "[| Card(K'); Card(K) |] ==> K' < csucc(K) <-> K' \<le> K"
+ "[| Card(K'); Card(K) |] ==> K' < csucc(K) \<longleftrightarrow> K' \<le> K"
by (simp add: lt_csucc_iff Card_cardinal_eq Card_is_Ord)
lemma InfCard_csucc: "InfCard(K) ==> InfCard(csucc(K))"
--- a/src/ZF/Cardinal_AC.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Cardinal_AC.thy Tue Mar 06 16:06:52 2012 +0000
@@ -25,7 +25,7 @@
apply (rule well_ord_cardinal_eqE, assumption+)
done
-lemma cardinal_eqpoll_iff: "|X| = |Y| <-> X eqpoll Y"
+lemma cardinal_eqpoll_iff: "|X| = |Y| \<longleftrightarrow> X eqpoll Y"
by (blast intro: cardinal_cong cardinal_eqE)
lemma cardinal_disjoint_Un:
@@ -38,21 +38,21 @@
apply (erule well_ord_lepoll_imp_Card_le, assumption)
done
-lemma cadd_assoc: "(i |+| j) |+| k = i |+| (j |+| k)"
+lemma cadd_assoc: "(i \<oplus> j) \<oplus> k = i \<oplus> (j \<oplus> k)"
apply (rule AC_well_ord [THEN exE])
apply (rule AC_well_ord [THEN exE])
apply (rule AC_well_ord [THEN exE])
apply (rule well_ord_cadd_assoc, assumption+)
done
-lemma cmult_assoc: "(i |*| j) |*| k = i |*| (j |*| k)"
+lemma cmult_assoc: "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
apply (rule AC_well_ord [THEN exE])
apply (rule AC_well_ord [THEN exE])
apply (rule AC_well_ord [THEN exE])
apply (rule well_ord_cmult_assoc, assumption+)
done
-lemma cadd_cmult_distrib: "(i |+| j) |*| k = (i |*| k) |+| (j |*| k)"
+lemma cadd_cmult_distrib: "(i \<oplus> j) \<otimes> k = (i \<otimes> k) \<oplus> (j \<otimes> k)"
apply (rule AC_well_ord [THEN exE])
apply (rule AC_well_ord [THEN exE])
apply (rule AC_well_ord [THEN exE])
@@ -74,19 +74,19 @@
apply (rule cardinal_eqpoll [THEN eqpoll_imp_lepoll])
done
-lemma le_Card_iff: "Card(K) ==> |A| \<le> K <-> A lepoll K"
+lemma le_Card_iff: "Card(K) ==> |A| \<le> K \<longleftrightarrow> A lepoll K"
apply (erule Card_cardinal_eq [THEN subst], rule iffI,
erule Card_le_imp_lepoll)
apply (erule lepoll_imp_Card_le)
done
-lemma cardinal_0_iff_0 [simp]: "|A| = 0 <-> A = 0";
+lemma cardinal_0_iff_0 [simp]: "|A| = 0 \<longleftrightarrow> A = 0";
apply auto
apply (drule cardinal_0 [THEN ssubst])
apply (blast intro: eqpoll_0_iff [THEN iffD1] cardinal_eqpoll_iff [THEN iffD1])
done
-lemma cardinal_lt_iff_lesspoll: "Ord(i) ==> i < |A| <-> i lesspoll A"
+lemma cardinal_lt_iff_lesspoll: "Ord(i) ==> i < |A| \<longleftrightarrow> i lesspoll A"
apply (cut_tac A = "A" in cardinal_eqpoll)
apply (auto simp add: eqpoll_iff)
apply (blast intro: lesspoll_trans2 lt_Card_imp_lesspoll Card_cardinal)
--- a/src/ZF/EquivClass.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/EquivClass.thy Tue Mar 06 16:06:52 2012 +0000
@@ -92,11 +92,11 @@
by (unfold equiv_def, blast)
lemma equiv_class_eq_iff:
- "equiv(A,r) ==> <x,y>: r <-> r``{x} = r``{y} & x:A & y:A"
+ "equiv(A,r) ==> <x,y>: r \<longleftrightarrow> r``{x} = r``{y} & x:A & y:A"
by (blast intro: eq_equiv_class equiv_class_eq dest: equiv_type)
lemma eq_equiv_class_iff:
- "[| equiv(A,r); x: A; y: A |] ==> r``{x} = r``{y} <-> <x,y>: r"
+ "[| equiv(A,r); x: A; y: A |] ==> r``{x} = r``{y} \<longleftrightarrow> <x,y>: r"
by (blast intro: eq_equiv_class equiv_class_eq dest: equiv_type)
(*** Quotients ***)
--- a/src/ZF/Finite.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Finite.thy Tue Mar 06 16:06:52 2012 +0000
@@ -183,7 +183,7 @@
lemma FiniteFun_Collect_iff:
"f \<in> FiniteFun(A, {y:B. P(y)})
- <-> f \<in> FiniteFun(A,B) & (\<forall>x\<in>domain(f). P(f`x))"
+ \<longleftrightarrow> f \<in> FiniteFun(A,B) & (\<forall>x\<in>domain(f). P(f`x))"
apply auto
apply (blast intro: FiniteFun_mono [THEN [2] rev_subsetD])
apply (blast dest: Pair_mem_PiD FiniteFun_is_fun)
--- a/src/ZF/Inductive_ZF.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Inductive_ZF.thy Tue Mar 06 16:06:52 2012 +0000
@@ -22,7 +22,7 @@
("Tools/primrec_package.ML")
begin
-lemma def_swap_iff: "a == b ==> a = c <-> c = b"
+lemma def_swap_iff: "a == b ==> a = c \<longleftrightarrow> c = b"
by blast
lemma def_trans: "f == g ==> g(a) = b ==> f(a) = b"
--- a/src/ZF/IntArith.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/IntArith.thy Tue Mar 06 16:06:52 2012 +0000
@@ -31,13 +31,13 @@
(** Combining of literal coefficients in sums of products **)
-lemma zless_iff_zdiff_zless_0: "(x $< y) <-> (x$-y $< #0)"
+lemma zless_iff_zdiff_zless_0: "(x $< y) \<longleftrightarrow> (x$-y $< #0)"
by (simp add: zcompare_rls)
-lemma eq_iff_zdiff_eq_0: "[| x: int; y: int |] ==> (x = y) <-> (x$-y = #0)"
+lemma eq_iff_zdiff_eq_0: "[| x: int; y: int |] ==> (x = y) \<longleftrightarrow> (x$-y = #0)"
by (simp add: zcompare_rls)
-lemma zle_iff_zdiff_zle_0: "(x $<= y) <-> (x$-y $<= #0)"
+lemma zle_iff_zdiff_zle_0: "(x $<= y) \<longleftrightarrow> (x$-y $<= #0)"
by (simp add: zcompare_rls)
@@ -58,33 +58,33 @@
zle_iff_zdiff_zle_0 [where y = n]
for u v (* FIXME n (!?) *)
-lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) <-> ((i$-j)$*u $+ m = intify(n))"
+lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m = intify(n))"
apply (simp add: zdiff_def zadd_zmult_distrib)
apply (simp add: zcompare_rls)
apply (simp add: zadd_ac)
done
-lemma eq_add_iff2: "(i$*u $+ m = j$*u $+ n) <-> (intify(m) = (j$-i)$*u $+ n)"
+lemma eq_add_iff2: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> (intify(m) = (j$-i)$*u $+ n)"
apply (simp add: zdiff_def zadd_zmult_distrib)
apply (simp add: zcompare_rls)
apply (simp add: zadd_ac)
done
-lemma less_add_iff1: "(i$*u $+ m $< j$*u $+ n) <-> ((i$-j)$*u $+ m $< n)"
+lemma less_add_iff1: "(i$*u $+ m $< j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $< n)"
apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
done
-lemma less_add_iff2: "(i$*u $+ m $< j$*u $+ n) <-> (m $< (j$-i)$*u $+ n)"
+lemma less_add_iff2: "(i$*u $+ m $< j$*u $+ n) \<longleftrightarrow> (m $< (j$-i)$*u $+ n)"
apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
done
-lemma le_add_iff1: "(i$*u $+ m $<= j$*u $+ n) <-> ((i$-j)$*u $+ m $<= n)"
+lemma le_add_iff1: "(i$*u $+ m $<= j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $<= n)"
apply (simp add: zdiff_def zadd_zmult_distrib)
apply (simp add: zcompare_rls)
apply (simp add: zadd_ac)
done
-lemma le_add_iff2: "(i$*u $+ m $<= j$*u $+ n) <-> (m $<= (j$-i)$*u $+ n)"
+lemma le_add_iff2: "(i$*u $+ m $<= j$*u $+ n) \<longleftrightarrow> (m $<= (j$-i)$*u $+ n)"
apply (simp add: zdiff_def zadd_zmult_distrib)
apply (simp add: zcompare_rls)
apply (simp add: zadd_ac)
--- a/src/ZF/IntDiv_ZF.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/IntDiv_ZF.thy Tue Mar 06 16:06:52 2012 +0000
@@ -136,7 +136,7 @@
(*** Inequality lemmas involving $#succ(m) ***)
lemma zless_add_succ_iff:
- "(w $< z $+ $# succ(m)) <-> (w $< z $+ $#m | intify(w) = z $+ $#m)"
+ "(w $< z $+ $# succ(m)) \<longleftrightarrow> (w $< z $+ $#m | intify(w) = z $+ $#m)"
apply (auto simp add: zless_iff_succ_zadd zadd_assoc int_of_add [symmetric])
apply (rule_tac [3] x = "0" in bexI)
apply (cut_tac m = "m" in int_succ_int_1)
@@ -149,32 +149,32 @@
done
lemma zadd_succ_lemma:
- "z \<in> int ==> (w $+ $# succ(m) $<= z) <-> (w $+ $#m $< z)"
+ "z \<in> int ==> (w $+ $# succ(m) $<= z) \<longleftrightarrow> (w $+ $#m $< z)"
apply (simp only: not_zless_iff_zle [THEN iff_sym] zless_add_succ_iff)
apply (auto intro: zle_anti_sym elim: zless_asym
simp add: zless_imp_zle not_zless_iff_zle)
done
-lemma zadd_succ_zle_iff: "(w $+ $# succ(m) $<= z) <-> (w $+ $#m $< z)"
+lemma zadd_succ_zle_iff: "(w $+ $# succ(m) $<= z) \<longleftrightarrow> (w $+ $#m $< z)"
apply (cut_tac z = "intify (z)" in zadd_succ_lemma)
apply auto
done
(** Inequality reasoning **)
-lemma zless_add1_iff_zle: "(w $< z $+ #1) <-> (w$<=z)"
+lemma zless_add1_iff_zle: "(w $< z $+ #1) \<longleftrightarrow> (w$<=z)"
apply (subgoal_tac "#1 = $# 1")
apply (simp only: zless_add_succ_iff zle_def)
apply auto
done
-lemma add1_zle_iff: "(w $+ #1 $<= z) <-> (w $< z)"
+lemma add1_zle_iff: "(w $+ #1 $<= z) \<longleftrightarrow> (w $< z)"
apply (subgoal_tac "#1 = $# 1")
apply (simp only: zadd_succ_zle_iff)
apply auto
done
-lemma add1_left_zle_iff: "(#1 $+ w $<= z) <-> (w $< z)"
+lemma add1_left_zle_iff: "(#1 $+ w $<= z) \<longleftrightarrow> (w $< z)"
apply (subst zadd_commute)
apply (rule add1_zle_iff)
done
@@ -280,13 +280,13 @@
(** Products of zeroes **)
lemma zmult_eq_lemma:
- "[| m \<in> int; n \<in> int |] ==> (m = #0 | n = #0) <-> (m$*n = #0)"
+ "[| m \<in> int; n \<in> int |] ==> (m = #0 | n = #0) \<longleftrightarrow> (m$*n = #0)"
apply (case_tac "m $< #0")
apply (auto simp add: not_zless_iff_zle zle_def neq_iff_zless)
apply (force dest: zmult_zless_mono1_neg zmult_zless_mono1)+
done
-lemma zmult_eq_0_iff [iff]: "(m$*n = #0) <-> (intify(m) = #0 | intify(n) = #0)"
+lemma zmult_eq_0_iff [iff]: "(m$*n = #0) \<longleftrightarrow> (intify(m) = #0 | intify(n) = #0)"
apply (simp add: zmult_eq_lemma)
done
@@ -296,7 +296,7 @@
lemma zmult_zless_lemma:
"[| k \<in> int; m \<in> int; n \<in> int |]
- ==> (m$*k $< n$*k) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
+ ==> (m$*k $< n$*k) \<longleftrightarrow> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
apply (case_tac "k = #0")
apply (auto simp add: neq_iff_zless zmult_zless_mono1 zmult_zless_mono1_neg)
apply (auto simp add: not_zless_iff_zle
@@ -307,43 +307,43 @@
done
lemma zmult_zless_cancel2:
- "(m$*k $< n$*k) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
+ "(m$*k $< n$*k) \<longleftrightarrow> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
apply (cut_tac k = "intify (k)" and m = "intify (m)" and n = "intify (n)"
in zmult_zless_lemma)
apply auto
done
lemma zmult_zless_cancel1:
- "(k$*m $< k$*n) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
+ "(k$*m $< k$*n) \<longleftrightarrow> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
by (simp add: zmult_commute [of k] zmult_zless_cancel2)
lemma zmult_zle_cancel2:
- "(m$*k $<= n$*k) <-> ((#0 $< k \<longrightarrow> m$<=n) & (k $< #0 \<longrightarrow> n$<=m))"
+ "(m$*k $<= n$*k) \<longleftrightarrow> ((#0 $< k \<longrightarrow> m$<=n) & (k $< #0 \<longrightarrow> n$<=m))"
by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel2)
lemma zmult_zle_cancel1:
- "(k$*m $<= k$*n) <-> ((#0 $< k \<longrightarrow> m$<=n) & (k $< #0 \<longrightarrow> n$<=m))"
+ "(k$*m $<= k$*n) \<longleftrightarrow> ((#0 $< k \<longrightarrow> m$<=n) & (k $< #0 \<longrightarrow> n$<=m))"
by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel1)
-lemma int_eq_iff_zle: "[| m \<in> int; n \<in> int |] ==> m=n <-> (m $<= n & n $<= m)"
+lemma int_eq_iff_zle: "[| m \<in> int; n \<in> int |] ==> m=n \<longleftrightarrow> (m $<= n & n $<= m)"
apply (blast intro: zle_refl zle_anti_sym)
done
lemma zmult_cancel2_lemma:
- "[| k \<in> int; m \<in> int; n \<in> int |] ==> (m$*k = n$*k) <-> (k=#0 | m=n)"
+ "[| k \<in> int; m \<in> int; n \<in> int |] ==> (m$*k = n$*k) \<longleftrightarrow> (k=#0 | m=n)"
apply (simp add: int_eq_iff_zle [of "m$*k"] int_eq_iff_zle [of m])
apply (auto simp add: zmult_zle_cancel2 neq_iff_zless)
done
lemma zmult_cancel2 [simp]:
- "(m$*k = n$*k) <-> (intify(k) = #0 | intify(m) = intify(n))"
+ "(m$*k = n$*k) \<longleftrightarrow> (intify(k) = #0 | intify(m) = intify(n))"
apply (rule iff_trans)
apply (rule_tac [2] zmult_cancel2_lemma)
apply auto
done
lemma zmult_cancel1 [simp]:
- "(k$*m = k$*n) <-> (intify(k) = #0 | intify(m) = intify(n))"
+ "(k$*m = k$*n) \<longleftrightarrow> (intify(k) = #0 | intify(m) = intify(n))"
by (simp add: zmult_commute [of k] zmult_cancel2)
@@ -458,7 +458,7 @@
(*FIXME: use intify in integ_of so that we always have @{term"integ_of w \<in> int"}.
then this rewrite can work for all constants!!*)
-lemma intify_eq_0_iff_zle: "intify(m) = #0 <-> (m $<= #0 & #0 $<= m)"
+lemma intify_eq_0_iff_zle: "intify(m) = #0 \<longleftrightarrow> (m $<= #0 & #0 $<= m)"
apply (simp (no_asm) add: int_eq_iff_zle)
done
@@ -484,7 +484,7 @@
lemma int_0_less_lemma:
"[| x \<in> int; y \<in> int |]
- ==> (#0 $< x $* y) <-> (#0 $< x & #0 $< y | x $< #0 & y $< #0)"
+ ==> (#0 $< x $* y) \<longleftrightarrow> (#0 $< x & #0 $< y | x $< #0 & y $< #0)"
apply (auto simp add: zle_def not_zless_iff_zle zmult_pos zmult_neg)
apply (rule ccontr)
apply (rule_tac [2] ccontr)
@@ -498,30 +498,30 @@
done
lemma int_0_less_mult_iff:
- "(#0 $< x $* y) <-> (#0 $< x & #0 $< y | x $< #0 & y $< #0)"
+ "(#0 $< x $* y) \<longleftrightarrow> (#0 $< x & #0 $< y | x $< #0 & y $< #0)"
apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_less_lemma)
apply auto
done
lemma int_0_le_lemma:
"[| x \<in> int; y \<in> int |]
- ==> (#0 $<= x $* y) <-> (#0 $<= x & #0 $<= y | x $<= #0 & y $<= #0)"
+ ==> (#0 $<= x $* y) \<longleftrightarrow> (#0 $<= x & #0 $<= y | x $<= #0 & y $<= #0)"
by (auto simp add: zle_def not_zless_iff_zle int_0_less_mult_iff)
lemma int_0_le_mult_iff:
- "(#0 $<= x $* y) <-> ((#0 $<= x & #0 $<= y) | (x $<= #0 & y $<= #0))"
+ "(#0 $<= x $* y) \<longleftrightarrow> ((#0 $<= x & #0 $<= y) | (x $<= #0 & y $<= #0))"
apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_le_lemma)
apply auto
done
lemma zmult_less_0_iff:
- "(x $* y $< #0) <-> (#0 $< x & y $< #0 | x $< #0 & #0 $< y)"
+ "(x $* y $< #0) \<longleftrightarrow> (#0 $< x & y $< #0 | x $< #0 & #0 $< y)"
apply (auto simp add: int_0_le_mult_iff not_zle_iff_zless [THEN iff_sym])
apply (auto dest: zless_not_sym simp add: not_zle_iff_zless)
done
lemma zmult_le_0_iff:
- "(x $* y $<= #0) <-> (#0 $<= x & y $<= #0 | x $<= #0 & #0 $<= y)"
+ "(x $* y $<= #0) \<longleftrightarrow> (#0 $<= x & y $<= #0 | x $<= #0 & #0 $<= y)"
by (auto dest: zless_not_sym
simp add: int_0_less_mult_iff not_zless_iff_zle [THEN iff_sym])
@@ -1656,7 +1656,7 @@
apply auto
done
-lemma pos_imp_zdiv_nonneg_iff: "#0 $< b ==> (#0 $<= a zdiv b) <-> (#0 $<= a)"
+lemma pos_imp_zdiv_nonneg_iff: "#0 $< b ==> (#0 $<= a zdiv b) \<longleftrightarrow> (#0 $<= a)"
apply auto
apply (drule_tac [2] zdiv_mono1)
apply (auto simp add: neq_iff_zless)
@@ -1664,7 +1664,7 @@
apply (blast intro: zdiv_neg_pos_less0)
done
-lemma neg_imp_zdiv_nonneg_iff: "b $< #0 ==> (#0 $<= a zdiv b) <-> (a $<= #0)"
+lemma neg_imp_zdiv_nonneg_iff: "b $< #0 ==> (#0 $<= a zdiv b) \<longleftrightarrow> (a $<= #0)"
apply (subst zdiv_zminus_zminus [symmetric])
apply (rule iff_trans)
apply (rule pos_imp_zdiv_nonneg_iff)
@@ -1672,13 +1672,13 @@
done
(*But not (a zdiv b $<= 0 iff a$<=0); consider a=1, b=2 when a zdiv b = 0.*)
-lemma pos_imp_zdiv_neg_iff: "#0 $< b ==> (a zdiv b $< #0) <-> (a $< #0)"
+lemma pos_imp_zdiv_neg_iff: "#0 $< b ==> (a zdiv b $< #0) \<longleftrightarrow> (a $< #0)"
apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym])
apply (erule pos_imp_zdiv_nonneg_iff)
done
(*Again the law fails for $<=: consider a = -1, b = -2 when a zdiv b = 0*)
-lemma neg_imp_zdiv_neg_iff: "b $< #0 ==> (a zdiv b $< #0) <-> (#0 $< a)"
+lemma neg_imp_zdiv_neg_iff: "b $< #0 ==> (a zdiv b $< #0) \<longleftrightarrow> (#0 $< a)"
apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym])
apply (erule neg_imp_zdiv_nonneg_iff)
done
@@ -1710,8 +1710,8 @@
done
- lemma neg_zdiv_mult_2: "a $<= #0 ==> (#1 $+ #2$*b) zdiv (#2$*a) <-> (b$+#1) zdiv a"
- apply (subgoal_tac " (#1 $+ #2$* ($-b-#1)) zdiv (#2 $* ($-a)) <-> ($-b-#1) zdiv ($-a)")
+ lemma neg_zdiv_mult_2: "a $<= #0 ==> (#1 $+ #2$*b) zdiv (#2$*a) \<longleftrightarrow> (b$+#1) zdiv a"
+ apply (subgoal_tac " (#1 $+ #2$* ($-b-#1)) zdiv (#2 $* ($-a)) \<longleftrightarrow> ($-b-#1) zdiv ($-a)")
apply (rule_tac [2] pos_zdiv_mult_2)
apply (auto simp add: zmult_zminus_right)
apply (subgoal_tac " (#-1 - (#2 $* b)) = - (#1 $+ (#2 $* b))")
--- a/src/ZF/Int_ZF.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Int_ZF.thy Tue Mar 06 16:06:52 2012 +0000
@@ -107,7 +107,7 @@
(** Natural deduction for intrel **)
lemma intrel_iff [simp]:
- "<<x1,y1>,<x2,y2>>: intrel <->
+ "<<x1,y1>,<x2,y2>>: intrel \<longleftrightarrow>
x1\<in>nat & y1\<in>nat & x2\<in>nat & y2\<in>nat & x1#+y2 = x2#+y1"
by (simp add: intrel_def)
@@ -148,7 +148,7 @@
lemma int_of_type [simp,TC]: "$#m \<in> int"
by (simp add: int_def quotient_def int_of_def, auto)
-lemma int_of_eq [iff]: "($# m = $# n) <-> natify(m)=natify(n)"
+lemma int_of_eq [iff]: "($# m = $# n) \<longleftrightarrow> natify(m)=natify(n)"
by (simp add: int_of_def)
lemma int_of_inject: "[| $#m = $#n; m\<in>nat; n\<in>nat |] ==> m=n"
@@ -202,16 +202,16 @@
(** Orderings **)
-lemma zless_intify1 [simp]:"intify(x) $< y <-> x $< y"
+lemma zless_intify1 [simp]:"intify(x) $< y \<longleftrightarrow> x $< y"
by (simp add: zless_def)
-lemma zless_intify2 [simp]:"x $< intify(y) <-> x $< y"
+lemma zless_intify2 [simp]:"x $< intify(y) \<longleftrightarrow> x $< y"
by (simp add: zless_def)
-lemma zle_intify1 [simp]:"intify(x) $<= y <-> x $<= y"
+lemma zle_intify1 [simp]:"intify(x) $<= y \<longleftrightarrow> x $<= y"
by (simp add: zle_def)
-lemma zle_intify2 [simp]:"x $<= intify(y) <-> x $<= y"
+lemma zle_intify2 [simp]:"x $<= intify(y) \<longleftrightarrow> x $<= y"
by (simp add: zle_def)
@@ -268,7 +268,7 @@
subsection{*@{term znegative}: the test for negative integers*}
-lemma znegative: "[| x\<in>nat; y\<in>nat |] ==> znegative(intrel``{<x,y>}) <-> x<y"
+lemma znegative: "[| x\<in>nat; y\<in>nat |] ==> znegative(intrel``{<x,y>}) \<longleftrightarrow> x<y"
apply (cases "x<y")
apply (auto simp add: znegative_def not_lt_iff_le)
apply (subgoal_tac "y #+ x2 < x #+ y2", force)
@@ -644,7 +644,7 @@
lemma zless_not_refl [iff]: "~ (z$<z)"
by (auto simp add: zless_def znegative_def int_of_def zdiff_def)
-lemma neq_iff_zless: "[| x: int; y: int |] ==> (x \<noteq> y) <-> (x $< y | y $< x)"
+lemma neq_iff_zless: "[| x: int; y: int |] ==> (x \<noteq> y) \<longleftrightarrow> (x $< y | y $< x)"
by (cut_tac z = x and w = y in zless_linear, auto)
lemma zless_imp_intify_neq: "w $< z ==> intify(w) \<noteq> intify(z)"
@@ -682,14 +682,14 @@
by (cut_tac intify_in_int [THEN zless_succ_zadd_lemma], auto)
lemma zless_iff_succ_zadd:
- "w $< z <-> (\<exists>n\<in>nat. w $+ $#(succ(n)) = intify(z))"
+ "w $< z \<longleftrightarrow> (\<exists>n\<in>nat. w $+ $#(succ(n)) = intify(z))"
apply (rule iffI)
apply (erule zless_imp_succ_zadd, auto)
apply (rename_tac "n")
apply (cut_tac w = w and n = n in zless_succ_zadd, auto)
done
-lemma zless_int_of [simp]: "[| m\<in>nat; n\<in>nat |] ==> ($#m $< $#n) <-> (m<n)"
+lemma zless_int_of [simp]: "[| m\<in>nat; n\<in>nat |] ==> ($#m $< $#n) \<longleftrightarrow> (m<n)"
apply (simp add: less_iff_succ_add zless_iff_succ_zadd int_of_add [symmetric])
apply (blast intro: sym)
done
@@ -768,13 +768,13 @@
apply (simp add: zless_def zdiff_def zminus_def)
done
-lemma not_zless_iff_zle: "~ (z $< w) <-> (w $<= z)"
+lemma not_zless_iff_zle: "~ (z $< w) \<longleftrightarrow> (w $<= z)"
apply (cut_tac z = z and w = w in zless_linear)
apply (auto dest: zless_trans simp add: zle_def)
apply (auto dest!: zless_imp_intify_neq)
done
-lemma not_zle_iff_zless: "~ (z $<= w) <-> (w $< z)"
+lemma not_zle_iff_zless: "~ (z $<= w) \<longleftrightarrow> (w $< z)"
by (simp add: not_zless_iff_zle [THEN iff_sym])
@@ -786,32 +786,32 @@
lemma zdiff_zdiff_eq2: "x $- (y $- z) = (x $+ z) $- y"
by (simp add: zdiff_def zadd_ac)
-lemma zdiff_zless_iff: "(x$-y $< z) <-> (x $< z $+ y)"
+lemma zdiff_zless_iff: "(x$-y $< z) \<longleftrightarrow> (x $< z $+ y)"
by (simp add: zless_def zdiff_def zadd_ac)
-lemma zless_zdiff_iff: "(x $< z$-y) <-> (x $+ y $< z)"
+lemma zless_zdiff_iff: "(x $< z$-y) \<longleftrightarrow> (x $+ y $< z)"
by (simp add: zless_def zdiff_def zadd_ac)
-lemma zdiff_eq_iff: "[| x: int; z: int |] ==> (x$-y = z) <-> (x = z $+ y)"
+lemma zdiff_eq_iff: "[| x: int; z: int |] ==> (x$-y = z) \<longleftrightarrow> (x = z $+ y)"
by (auto simp add: zdiff_def zadd_assoc)
-lemma eq_zdiff_iff: "[| x: int; z: int |] ==> (x = z$-y) <-> (x $+ y = z)"
+lemma eq_zdiff_iff: "[| x: int; z: int |] ==> (x = z$-y) \<longleftrightarrow> (x $+ y = z)"
by (auto simp add: zdiff_def zadd_assoc)
lemma zdiff_zle_iff_lemma:
- "[| x: int; z: int |] ==> (x$-y $<= z) <-> (x $<= z $+ y)"
+ "[| x: int; z: int |] ==> (x$-y $<= z) \<longleftrightarrow> (x $<= z $+ y)"
by (auto simp add: zle_def zdiff_eq_iff zdiff_zless_iff)
-lemma zdiff_zle_iff: "(x$-y $<= z) <-> (x $<= z $+ y)"
+lemma zdiff_zle_iff: "(x$-y $<= z) \<longleftrightarrow> (x $<= z $+ y)"
by (cut_tac zdiff_zle_iff_lemma [OF intify_in_int intify_in_int], simp)
lemma zle_zdiff_iff_lemma:
- "[| x: int; z: int |] ==>(x $<= z$-y) <-> (x $+ y $<= z)"
+ "[| x: int; z: int |] ==>(x $<= z$-y) \<longleftrightarrow> (x $+ y $<= z)"
apply (auto simp add: zle_def zdiff_eq_iff zless_zdiff_iff)
apply (auto simp add: zdiff_def zadd_assoc)
done
-lemma zle_zdiff_iff: "(x $<= z$-y) <-> (x $+ y $<= z)"
+lemma zle_zdiff_iff: "(x $<= z$-y) \<longleftrightarrow> (x $+ y $<= z)"
by (cut_tac zle_zdiff_iff_lemma [ OF intify_in_int intify_in_int], simp)
text{*This list of rewrites simplifies (in)equalities by bringing subtractions
@@ -828,41 +828,41 @@
of the CancelNumerals Simprocs*}
lemma zadd_left_cancel:
- "[| w: int; w': int |] ==> (z $+ w' = z $+ w) <-> (w' = w)"
+ "[| w: int; w': int |] ==> (z $+ w' = z $+ w) \<longleftrightarrow> (w' = w)"
apply safe
apply (drule_tac t = "%x. x $+ ($-z) " in subst_context)
apply (simp add: zadd_ac)
done
lemma zadd_left_cancel_intify [simp]:
- "(z $+ w' = z $+ w) <-> intify(w') = intify(w)"
+ "(z $+ w' = z $+ w) \<longleftrightarrow> intify(w') = intify(w)"
apply (rule iff_trans)
apply (rule_tac [2] zadd_left_cancel, auto)
done
lemma zadd_right_cancel:
- "[| w: int; w': int |] ==> (w' $+ z = w $+ z) <-> (w' = w)"
+ "[| w: int; w': int |] ==> (w' $+ z = w $+ z) \<longleftrightarrow> (w' = w)"
apply safe
apply (drule_tac t = "%x. x $+ ($-z) " in subst_context)
apply (simp add: zadd_ac)
done
lemma zadd_right_cancel_intify [simp]:
- "(w' $+ z = w $+ z) <-> intify(w') = intify(w)"
+ "(w' $+ z = w $+ z) \<longleftrightarrow> intify(w') = intify(w)"
apply (rule iff_trans)
apply (rule_tac [2] zadd_right_cancel, auto)
done
-lemma zadd_right_cancel_zless [simp]: "(w' $+ z $< w $+ z) <-> (w' $< w)"
+lemma zadd_right_cancel_zless [simp]: "(w' $+ z $< w $+ z) \<longleftrightarrow> (w' $< w)"
by (simp add: zdiff_zless_iff [THEN iff_sym] zdiff_def zadd_assoc)
-lemma zadd_left_cancel_zless [simp]: "(z $+ w' $< z $+ w) <-> (w' $< w)"
+lemma zadd_left_cancel_zless [simp]: "(z $+ w' $< z $+ w) \<longleftrightarrow> (w' $< w)"
by (simp add: zadd_commute [of z] zadd_right_cancel_zless)
-lemma zadd_right_cancel_zle [simp]: "(w' $+ z $<= w $+ z) <-> w' $<= w"
+lemma zadd_right_cancel_zle [simp]: "(w' $+ z $<= w $+ z) \<longleftrightarrow> w' $<= w"
by (simp add: zle_def)
-lemma zadd_left_cancel_zle [simp]: "(z $+ w' $<= z $+ w) <-> w' $<= w"
+lemma zadd_left_cancel_zle [simp]: "(z $+ w' $<= z $+ w) \<longleftrightarrow> w' $<= w"
by (simp add: zadd_commute [of z] zadd_right_cancel_zle)
@@ -887,26 +887,26 @@
subsection{*Comparison laws*}
-lemma zminus_zless_zminus [simp]: "($- x $< $- y) <-> (y $< x)"
+lemma zminus_zless_zminus [simp]: "($- x $< $- y) \<longleftrightarrow> (y $< x)"
by (simp add: zless_def zdiff_def zadd_ac)
-lemma zminus_zle_zminus [simp]: "($- x $<= $- y) <-> (y $<= x)"
+lemma zminus_zle_zminus [simp]: "($- x $<= $- y) \<longleftrightarrow> (y $<= x)"
by (simp add: not_zless_iff_zle [THEN iff_sym])
subsubsection{*More inequality lemmas*}
-lemma equation_zminus: "[| x: int; y: int |] ==> (x = $- y) <-> (y = $- x)"
+lemma equation_zminus: "[| x: int; y: int |] ==> (x = $- y) \<longleftrightarrow> (y = $- x)"
by auto
-lemma zminus_equation: "[| x: int; y: int |] ==> ($- x = y) <-> ($- y = x)"
+lemma zminus_equation: "[| x: int; y: int |] ==> ($- x = y) \<longleftrightarrow> ($- y = x)"
by auto
-lemma equation_zminus_intify: "(intify(x) = $- y) <-> (intify(y) = $- x)"
+lemma equation_zminus_intify: "(intify(x) = $- y) \<longleftrightarrow> (intify(y) = $- x)"
apply (cut_tac x = "intify (x) " and y = "intify (y) " in equation_zminus)
apply auto
done
-lemma zminus_equation_intify: "($- x = intify(y)) <-> ($- y = intify(x))"
+lemma zminus_equation_intify: "($- x = intify(y)) \<longleftrightarrow> ($- y = intify(x))"
apply (cut_tac x = "intify (x) " and y = "intify (y) " in zminus_equation)
apply auto
done
@@ -914,16 +914,16 @@
subsubsection{*The next several equations are permutative: watch out!*}
-lemma zless_zminus: "(x $< $- y) <-> (y $< $- x)"
+lemma zless_zminus: "(x $< $- y) \<longleftrightarrow> (y $< $- x)"
by (simp add: zless_def zdiff_def zadd_ac)
-lemma zminus_zless: "($- x $< y) <-> ($- y $< x)"
+lemma zminus_zless: "($- x $< y) \<longleftrightarrow> ($- y $< x)"
by (simp add: zless_def zdiff_def zadd_ac)
-lemma zle_zminus: "(x $<= $- y) <-> (y $<= $- x)"
+lemma zle_zminus: "(x $<= $- y) \<longleftrightarrow> (y $<= $- x)"
by (simp add: not_zless_iff_zle [THEN iff_sym] zminus_zless)
-lemma zminus_zle: "($- x $<= y) <-> ($- y $<= x)"
+lemma zminus_zle: "($- x $<= y) \<longleftrightarrow> ($- y $<= x)"
by (simp add: not_zless_iff_zle [THEN iff_sym] zless_zminus)
end
--- a/src/ZF/List_ZF.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/List_ZF.thy Tue Mar 06 16:06:52 2012 +0000
@@ -136,11 +136,11 @@
(*An elimination rule, for type-checking*)
inductive_cases ConsE: "Cons(a,l) \<in> list(A)"
-lemma Cons_type_iff [simp]: "Cons(a,l) \<in> list(A) <-> a \<in> A & l \<in> list(A)"
+lemma Cons_type_iff [simp]: "Cons(a,l) \<in> list(A) \<longleftrightarrow> a \<in> A & l \<in> list(A)"
by (blast elim: ConsE)
(*Proving freeness results*)
-lemma Cons_iff: "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'"
+lemma Cons_iff: "Cons(a,l)=Cons(a',l') \<longleftrightarrow> a=a' & l=l'"
by auto
lemma Nil_Cons_iff: "~ Nil=Cons(a,l)"
@@ -480,7 +480,7 @@
apply (auto dest: not_lt_imp_le)
done
-lemma lt_min_iff: "[| i:nat; j:nat; k:nat |] ==> i<min(j,k) <-> i<j & i<k"
+lemma lt_min_iff: "[| i:nat; j:nat; k:nat |] ==> i<min(j,k) \<longleftrightarrow> i<j & i<k"
apply (unfold min_def)
apply (auto dest!: not_lt_imp_le intro: lt_trans2 lt_trans)
done
@@ -518,43 +518,43 @@
(** length **)
-lemma length_is_0_iff [simp]: "xs:list(A) ==> length(xs)=0 <-> xs=Nil"
+lemma length_is_0_iff [simp]: "xs:list(A) ==> length(xs)=0 \<longleftrightarrow> xs=Nil"
by (erule list.induct, auto)
-lemma length_is_0_iff2 [simp]: "xs:list(A) ==> 0 = length(xs) <-> xs=Nil"
+lemma length_is_0_iff2 [simp]: "xs:list(A) ==> 0 = length(xs) \<longleftrightarrow> xs=Nil"
by (erule list.induct, auto)
lemma length_tl [simp]: "xs:list(A) ==> length(tl(xs)) = length(xs) #- 1"
by (erule list.induct, auto)
-lemma length_greater_0_iff: "xs:list(A) ==> 0<length(xs) <-> xs \<noteq> Nil"
+lemma length_greater_0_iff: "xs:list(A) ==> 0<length(xs) \<longleftrightarrow> xs \<noteq> Nil"
by (erule list.induct, auto)
-lemma length_succ_iff: "xs:list(A) ==> length(xs)=succ(n) <-> (\<exists>y ys. xs=Cons(y, ys) & length(ys)=n)"
+lemma length_succ_iff: "xs:list(A) ==> length(xs)=succ(n) \<longleftrightarrow> (\<exists>y ys. xs=Cons(y, ys) & length(ys)=n)"
by (erule list.induct, auto)
(** more theorems about append **)
lemma append_is_Nil_iff [simp]:
- "xs:list(A) ==> (xs@ys = Nil) <-> (xs=Nil & ys = Nil)"
+ "xs:list(A) ==> (xs@ys = Nil) \<longleftrightarrow> (xs=Nil & ys = Nil)"
by (erule list.induct, auto)
lemma append_is_Nil_iff2 [simp]:
- "xs:list(A) ==> (Nil = xs@ys) <-> (xs=Nil & ys = Nil)"
+ "xs:list(A) ==> (Nil = xs@ys) \<longleftrightarrow> (xs=Nil & ys = Nil)"
by (erule list.induct, auto)
lemma append_left_is_self_iff [simp]:
- "xs:list(A) ==> (xs@ys = xs) <-> (ys = Nil)"
+ "xs:list(A) ==> (xs@ys = xs) \<longleftrightarrow> (ys = Nil)"
by (erule list.induct, auto)
lemma append_left_is_self_iff2 [simp]:
- "xs:list(A) ==> (xs = xs@ys) <-> (ys = Nil)"
+ "xs:list(A) ==> (xs = xs@ys) \<longleftrightarrow> (ys = Nil)"
by (erule list.induct, auto)
(*TOO SLOW as a default simprule!*)
lemma append_left_is_Nil_iff [rule_format]:
"[| xs:list(A); ys:list(A); zs:list(A) |] ==>
- length(ys)=length(zs) \<longrightarrow> (xs@ys=zs <-> (xs=Nil & ys=zs))"
+ length(ys)=length(zs) \<longrightarrow> (xs@ys=zs \<longleftrightarrow> (xs=Nil & ys=zs))"
apply (erule list.induct)
apply (auto simp add: length_app)
done
@@ -562,14 +562,14 @@
(*TOO SLOW as a default simprule!*)
lemma append_left_is_Nil_iff2 [rule_format]:
"[| xs:list(A); ys:list(A); zs:list(A) |] ==>
- length(ys)=length(zs) \<longrightarrow> (zs=ys@xs <-> (xs=Nil & ys=zs))"
+ length(ys)=length(zs) \<longrightarrow> (zs=ys@xs \<longleftrightarrow> (xs=Nil & ys=zs))"
apply (erule list.induct)
apply (auto simp add: length_app)
done
lemma append_eq_append_iff [rule_format,simp]:
"xs:list(A) ==> \<forall>ys \<in> list(A).
- length(xs)=length(ys) \<longrightarrow> (xs@us = ys@vs) <-> (xs=ys & us=vs)"
+ length(xs)=length(ys) \<longrightarrow> (xs@us = ys@vs) \<longleftrightarrow> (xs=ys & us=vs)"
apply (erule list.induct)
apply (simp (no_asm_simp))
apply clarify
@@ -589,23 +589,23 @@
lemma append_eq_append_iff2 [simp]:
"[| xs:list(A); ys:list(A); us:list(A); vs:list(A); length(us)=length(vs) |]
- ==> xs@us = ys@vs <-> (xs=ys & us=vs)"
+ ==> xs@us = ys@vs \<longleftrightarrow> (xs=ys & us=vs)"
apply (rule iffI)
apply (rule append_eq_append, auto)
done
lemma append_self_iff [simp]:
- "[| xs:list(A); ys:list(A); zs:list(A) |] ==> xs@ys=xs@zs <-> ys=zs"
+ "[| xs:list(A); ys:list(A); zs:list(A) |] ==> xs@ys=xs@zs \<longleftrightarrow> ys=zs"
by simp
lemma append_self_iff2 [simp]:
- "[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs <-> ys=zs"
+ "[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs \<longleftrightarrow> ys=zs"
by simp
(* Can also be proved from append_eq_append_iff2,
but the proof requires two more hypotheses: x:A and y:A *)
lemma append1_eq_iff [rule_format,simp]:
- "xs:list(A) ==> \<forall>ys \<in> list(A). xs@[x] = ys@[y] <-> (xs = ys & x=y)"
+ "xs:list(A) ==> \<forall>ys \<in> list(A). xs@[x] = ys@[y] \<longleftrightarrow> (xs = ys & x=y)"
apply (erule list.induct)
apply clarify
apply (erule list.cases)
@@ -617,11 +617,11 @@
lemma append_right_is_self_iff [simp]:
- "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) <-> (xs=Nil)"
+ "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) \<longleftrightarrow> (xs=Nil)"
by (simp (no_asm_simp) add: append_left_is_Nil_iff)
lemma append_right_is_self_iff2 [simp]:
- "[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) <-> (xs=Nil)"
+ "[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) \<longleftrightarrow> (xs=Nil)"
apply (rule iffI)
apply (drule sym, auto)
done
@@ -635,14 +635,14 @@
by (induct_tac "xs", auto)
(** rev **)
-lemma rev_is_Nil_iff [simp]: "xs:list(A) ==> (rev(xs) = Nil <-> xs = Nil)"
+lemma rev_is_Nil_iff [simp]: "xs:list(A) ==> (rev(xs) = Nil \<longleftrightarrow> xs = Nil)"
by (erule list.induct, auto)
-lemma Nil_is_rev_iff [simp]: "xs:list(A) ==> (Nil = rev(xs) <-> xs = Nil)"
+lemma Nil_is_rev_iff [simp]: "xs:list(A) ==> (Nil = rev(xs) \<longleftrightarrow> xs = Nil)"
by (erule list.induct, auto)
lemma rev_is_rev_iff [rule_format,simp]:
- "xs:list(A) ==> \<forall>ys \<in> list(A). rev(xs)=rev(ys) <-> xs=ys"
+ "xs:list(A) ==> \<forall>ys \<in> list(A). rev(xs)=rev(ys) \<longleftrightarrow> xs=ys"
apply (erule list.induct, force, clarify)
apply (erule_tac a = ys in list.cases, auto)
done
@@ -1027,7 +1027,7 @@
lemma list_update_same_conv [rule_format]:
"xs:list(A) ==>
\<forall>i \<in> nat. i < length(xs) \<longrightarrow>
- (list_update(xs, i, x) = xs) <-> (nth(i, xs) = x)"
+ (list_update(xs, i, x) = xs) \<longleftrightarrow> (nth(i, xs) = x)"
apply (induct_tac "xs")
apply (simp (no_asm))
apply clarify
--- a/src/ZF/Nat_ZF.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Nat_ZF.thy Tue Mar 06 16:06:52 2012 +0000
@@ -123,7 +123,7 @@
lemma succ_natD: "succ(i): nat ==> i: nat"
by (rule Ord_trans [OF succI1], auto)
-lemma nat_succ_iff [iff]: "succ(n): nat <-> n: nat"
+lemma nat_succ_iff [iff]: "succ(n): nat \<longleftrightarrow> n: nat"
by (blast dest!: succ_natD)
lemma nat_le_Limit: "Limit(i) ==> nat \<le> i"
@@ -246,7 +246,7 @@
by (erule nat_induct, auto)
lemma split_nat_case:
- "P(nat_case(a,b,k)) <->
+ "P(nat_case(a,b,k)) \<longleftrightarrow>
((k=0 \<longrightarrow> P(a)) & (\<forall>x. k=succ(x) \<longrightarrow> P(b(x))) & (~ quasinat(k) \<longrightarrow> P(0)))"
apply (rule nat_cases [of k])
apply (auto simp add: non_nat_case)
@@ -294,7 +294,7 @@
apply (blast intro: lt_trans)
done
-lemma Le_iff [iff]: "<x,y> \<in> Le <-> x \<le> y & x \<in> nat & y \<in> nat"
+lemma Le_iff [iff]: "<x,y> \<in> Le \<longleftrightarrow> x \<le> y & x \<in> nat & y \<in> nat"
by (force simp add: Le_def)
end
--- a/src/ZF/Order.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Order.thy Tue Mar 06 16:06:52 2012 +0000
@@ -51,7 +51,7 @@
definition
ord_iso :: "[i,i,i,i]=>i" (*Order isomorphisms*) where
"ord_iso(A,r,B,s) ==
- {f: bij(A,B). \<forall>x\<in>A. \<forall>y\<in>A. <x,y>:r <-> <f`x,f`y>:s}"
+ {f: bij(A,B). \<forall>x\<in>A. \<forall>y\<in>A. <x,y>:r \<longleftrightarrow> <f`x,f`y>:s}"
definition
pred :: "[i,i,i]=>i" (*Set of predecessors*) where
@@ -107,7 +107,7 @@
(** Derived rules for pred(A,x,r) **)
-lemma pred_iff: "y \<in> pred(A,x,r) <-> <y,x>:r & y:A"
+lemma pred_iff: "y \<in> pred(A,x,r) \<longleftrightarrow> <y,x>:r & y:A"
by (unfold pred_def, blast)
lemmas predI = conjI [THEN pred_iff [THEN iffD2]]
@@ -160,30 +160,30 @@
(** Relations restricted to a smaller domain, by Krzysztof Grabczewski **)
-lemma irrefl_Int_iff: "irrefl(A,r \<inter> A*A) <-> irrefl(A,r)"
+lemma irrefl_Int_iff: "irrefl(A,r \<inter> A*A) \<longleftrightarrow> irrefl(A,r)"
by (unfold irrefl_def, blast)
-lemma trans_on_Int_iff: "trans[A](r \<inter> A*A) <-> trans[A](r)"
+lemma trans_on_Int_iff: "trans[A](r \<inter> A*A) \<longleftrightarrow> trans[A](r)"
by (unfold trans_on_def, blast)
-lemma part_ord_Int_iff: "part_ord(A,r \<inter> A*A) <-> part_ord(A,r)"
+lemma part_ord_Int_iff: "part_ord(A,r \<inter> A*A) \<longleftrightarrow> part_ord(A,r)"
apply (unfold part_ord_def)
apply (simp add: irrefl_Int_iff trans_on_Int_iff)
done
-lemma linear_Int_iff: "linear(A,r \<inter> A*A) <-> linear(A,r)"
+lemma linear_Int_iff: "linear(A,r \<inter> A*A) \<longleftrightarrow> linear(A,r)"
by (unfold linear_def, blast)
-lemma tot_ord_Int_iff: "tot_ord(A,r \<inter> A*A) <-> tot_ord(A,r)"
+lemma tot_ord_Int_iff: "tot_ord(A,r \<inter> A*A) \<longleftrightarrow> tot_ord(A,r)"
apply (unfold tot_ord_def)
apply (simp add: part_ord_Int_iff linear_Int_iff)
done
-lemma wf_on_Int_iff: "wf[A](r \<inter> A*A) <-> wf[A](r)"
+lemma wf_on_Int_iff: "wf[A](r \<inter> A*A) \<longleftrightarrow> wf[A](r)"
apply (unfold wf_on_def wf_def, fast) (*10 times faster than blast!*)
done
-lemma well_ord_Int_iff: "well_ord(A,r \<inter> A*A) <-> well_ord(A,r)"
+lemma well_ord_Int_iff: "well_ord(A,r \<inter> A*A) \<longleftrightarrow> well_ord(A,r)"
apply (unfold well_ord_def)
apply (simp add: tot_ord_Int_iff wf_on_Int_iff)
done
@@ -256,7 +256,7 @@
lemma ord_isoI:
"[| f: bij(A, B);
- !!x y. [| x:A; y:A |] ==> <x, y> \<in> r <-> <f`x, f`y> \<in> s |]
+ !!x y. [| x:A; y:A |] ==> <x, y> \<in> r \<longleftrightarrow> <f`x, f`y> \<in> s |]
==> f: ord_iso(A,r,B,s)"
by (simp add: ord_iso_def)
@@ -666,7 +666,7 @@
lemma subset_vimage_vimage_iff:
"[| Preorder(r); A \<subseteq> field(r); B \<subseteq> field(r) |] ==>
- r -`` A \<subseteq> r -`` B <-> (\<forall>a\<in>A. \<exists>b\<in>B. <a, b> \<in> r)"
+ r -`` A \<subseteq> r -`` B \<longleftrightarrow> (\<forall>a\<in>A. \<exists>b\<in>B. <a, b> \<in> r)"
apply (auto simp: subset_def preorder_on_def refl_def vimage_def image_def)
apply blast
unfolding trans_on_def
@@ -679,12 +679,12 @@
lemma subset_vimage1_vimage1_iff:
"[| Preorder(r); a \<in> field(r); b \<in> field(r) |] ==>
- r -`` {a} \<subseteq> r -`` {b} <-> <a, b> \<in> r"
+ r -`` {a} \<subseteq> r -`` {b} \<longleftrightarrow> <a, b> \<in> r"
by (simp add: subset_vimage_vimage_iff)
lemma Refl_antisym_eq_Image1_Image1_iff:
"[| refl(field(r), r); antisym(r); a \<in> field(r); b \<in> field(r) |] ==>
- r `` {a} = r `` {b} <-> a = b"
+ r `` {a} = r `` {b} \<longleftrightarrow> a = b"
apply rule
apply (frule equality_iffD)
apply (drule equality_iffD)
@@ -695,13 +695,13 @@
lemma Partial_order_eq_Image1_Image1_iff:
"[| Partial_order(r); a \<in> field(r); b \<in> field(r) |] ==>
- r `` {a} = r `` {b} <-> a = b"
+ r `` {a} = r `` {b} \<longleftrightarrow> a = b"
by (simp add: partial_order_on_def preorder_on_def
Refl_antisym_eq_Image1_Image1_iff)
lemma Refl_antisym_eq_vimage1_vimage1_iff:
"[| refl(field(r), r); antisym(r); a \<in> field(r); b \<in> field(r) |] ==>
- r -`` {a} = r -`` {b} <-> a = b"
+ r -`` {a} = r -`` {b} \<longleftrightarrow> a = b"
apply rule
apply (frule equality_iffD)
apply (drule equality_iffD)
@@ -712,7 +712,7 @@
lemma Partial_order_eq_vimage1_vimage1_iff:
"[| Partial_order(r); a \<in> field(r); b \<in> field(r) |] ==>
- r -`` {a} = r -`` {b} <-> a = b"
+ r -`` {a} = r -`` {b} \<longleftrightarrow> a = b"
by (simp add: partial_order_on_def preorder_on_def
Refl_antisym_eq_vimage1_vimage1_iff)
--- a/src/ZF/OrderArith.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/OrderArith.thy Tue Mar 06 16:06:52 2012 +0000
@@ -39,19 +39,19 @@
subsubsection{*Rewrite rules. Can be used to obtain introduction rules*}
lemma radd_Inl_Inr_iff [iff]:
- "<Inl(a), Inr(b)> \<in> radd(A,r,B,s) <-> a:A & b:B"
+ "<Inl(a), Inr(b)> \<in> radd(A,r,B,s) \<longleftrightarrow> a:A & b:B"
by (unfold radd_def, blast)
lemma radd_Inl_iff [iff]:
- "<Inl(a'), Inl(a)> \<in> radd(A,r,B,s) <-> a':A & a:A & <a',a>:r"
+ "<Inl(a'), Inl(a)> \<in> radd(A,r,B,s) \<longleftrightarrow> a':A & a:A & <a',a>:r"
by (unfold radd_def, blast)
lemma radd_Inr_iff [iff]:
- "<Inr(b'), Inr(b)> \<in> radd(A,r,B,s) <-> b':B & b:B & <b',b>:s"
+ "<Inr(b'), Inr(b)> \<in> radd(A,r,B,s) \<longleftrightarrow> b':B & b:B & <b',b>:s"
by (unfold radd_def, blast)
lemma radd_Inr_Inl_iff [simp]:
- "<Inr(b), Inl(a)> \<in> radd(A,r,B,s) <-> False"
+ "<Inr(b), Inl(a)> \<in> radd(A,r,B,s) \<longleftrightarrow> False"
by (unfold radd_def, blast)
declare radd_Inr_Inl_iff [THEN iffD1, dest!]
@@ -163,7 +163,7 @@
subsubsection{*Rewrite rule. Can be used to obtain introduction rules*}
lemma rmult_iff [iff]:
- "<<a',b'>, <a,b>> \<in> rmult(A,r,B,s) <->
+ "<<a',b'>, <a,b>> \<in> rmult(A,r,B,s) \<longleftrightarrow>
(<a',a>: r & a':A & a:A & b': B & b: B) |
(<b',b>: s & a'=a & a:A & b': B & b: B)"
@@ -307,7 +307,7 @@
subsubsection{*Rewrite rule*}
-lemma rvimage_iff: "<a,b> \<in> rvimage(A,f,r) <-> <f`a,f`b>: r & a:A & b:A"
+lemma rvimage_iff: "<a,b> \<in> rvimage(A,f,r) \<longleftrightarrow> <f`a,f`b>: r & a:A & b:A"
by (unfold rvimage_def, blast)
subsubsection{*Type checking*}
@@ -450,7 +450,7 @@
done
theorem wf_iff_subset_rvimage:
- "relation(r) ==> wf(r) <-> (\<exists>i f A. Ord(i) & r \<subseteq> rvimage(A, f, Memrel(i)))"
+ "relation(r) ==> wf(r) \<longleftrightarrow> (\<exists>i f A. Ord(i) & r \<subseteq> rvimage(A, f, Memrel(i)))"
by (blast dest!: relation_field_times_field wf_imp_subset_rvimage
intro: wf_rvimage_Ord [THEN wf_subset])
@@ -496,7 +496,7 @@
lemma wf_measure [iff]: "wf(measure(A,f))"
by (simp (no_asm) add: measure_eq_rvimage_Memrel wf_Memrel wf_rvimage)
-lemma measure_iff [iff]: "<x,y> \<in> measure(A,f) <-> x:A & y:A & f(x)<f(y)"
+lemma measure_iff [iff]: "<x,y> \<in> measure(A,f) \<longleftrightarrow> x:A & y:A & f(x)<f(y)"
by (simp (no_asm) add: measure_def)
lemma linear_measure:
--- a/src/ZF/OrderType.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/OrderType.thy Tue Mar 06 16:06:52 2012 +0000
@@ -533,7 +533,7 @@
apply (blast dest: oadd_lt_mono2 elim: lt_irrefl lt_asym)+
done
-lemma oadd_lt_iff2: "Ord(j) ==> i++j < i++k <-> j<k"
+lemma oadd_lt_iff2: "Ord(j) ==> i++j < i++k \<longleftrightarrow> j<k"
by (blast intro!: oadd_lt_mono2 dest!: oadd_lt_cancel2)
lemma oadd_inject: "[| i++j = i++k; Ord(j); Ord(k) |] ==> j=k"
@@ -607,13 +607,13 @@
Union_eq_UN [symmetric] Limit_Union_eq)
done
-lemma oadd_eq_0_iff: "[| Ord(i); Ord(j) |] ==> (i ++ j) = 0 <-> i=0 & j=0"
+lemma oadd_eq_0_iff: "[| Ord(i); Ord(j) |] ==> (i ++ j) = 0 \<longleftrightarrow> i=0 & j=0"
apply (erule trans_induct3 [of j])
apply (simp_all add: oadd_Limit)
apply (simp add: Union_empty_iff Limit_def lt_def, blast)
done
-lemma oadd_eq_lt_iff: "[| Ord(i); Ord(j) |] ==> 0 < (i ++ j) <-> 0<i | 0<j"
+lemma oadd_eq_lt_iff: "[| Ord(i); Ord(j) |] ==> 0 < (i ++ j) \<longleftrightarrow> 0<i | 0<j"
by (simp add: Ord_0_lt_iff [symmetric] oadd_eq_0_iff)
lemma oadd_LimitI: "[| Ord(i); Limit(j) |] ==> Limit(i ++ j)"
@@ -661,7 +661,7 @@
lemma oadd_le_mono: "[| i' \<le> i; j' \<le> j |] ==> i'++j' \<le> i++j"
by (simp del: oadd_succ add: oadd_succ [symmetric] le_Ord2 oadd_lt_mono)
-lemma oadd_le_iff2: "[| Ord(j); Ord(k) |] ==> i++j \<le> i++k <-> j \<le> k"
+lemma oadd_le_iff2: "[| Ord(j); Ord(k) |] ==> i++j \<le> i++k \<longleftrightarrow> j \<le> k"
by (simp del: oadd_succ add: oadd_lt_iff2 oadd_succ [symmetric] Ord_succ)
lemma oadd_lt_self: "[| Ord(i); 0<j |] ==> i < i++j"
--- a/src/ZF/Perm.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Perm.thy Tue Mar 06 16:06:52 2012 +0000
@@ -15,7 +15,7 @@
definition
(*composition of relations and functions; NOT Suppes's relative product*)
comp :: "[i,i]=>i" (infixr "O" 60) where
- "r O s == {xz \<in> domain(s)*range(r) .
+ "r O s == {xz \<in> domain(s)*range(r) .
\<exists>x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
definition
@@ -58,17 +58,17 @@
text{* A function with a right inverse is a surjection *}
-lemma f_imp_surjective:
+lemma f_imp_surjective:
"[| f: A->B; !!y. y:B ==> d(y): A; !!y. y:B ==> f`d(y) = y |]
==> f: surj(A,B)"
by (simp add: surj_def, blast)
-lemma lam_surjective:
- "[| !!x. x:A ==> c(x): B;
- !!y. y:B ==> d(y): A;
- !!y. y:B ==> c(d(y)) = y
+lemma lam_surjective:
+ "[| !!x. x:A ==> c(x): B;
+ !!y. y:B ==> d(y): A;
+ !!y. y:B ==> c(d(y)) = y
|] ==> (\<lambda>x\<in>A. c(x)) \<in> surj(A,B)"
-apply (rule_tac d = d in f_imp_surjective)
+apply (rule_tac d = d in f_imp_surjective)
apply (simp_all add: lam_type)
done
@@ -76,7 +76,7 @@
lemma cantor_surj: "f \<notin> surj(A,Pow(A))"
apply (unfold surj_def, safe)
apply (cut_tac cantor)
-apply (best del: subsetI)
+apply (best del: subsetI)
done
@@ -88,7 +88,7 @@
done
text{*Good for dealing with sets of pairs, but a bit ugly in use [used in AC]*}
-lemma inj_equality:
+lemma inj_equality:
"[| <a,b>:f; <c,b>:f; f: inj(A,B) |] ==> a=c"
apply (unfold inj_def)
apply (blast dest: Pair_mem_PiD)
@@ -104,8 +104,8 @@
apply (blast intro: subst_context [THEN box_equals])
done
-lemma lam_injective:
- "[| !!x. x:A ==> c(x): B;
+lemma lam_injective:
+ "[| !!x. x:A ==> c(x): B;
!!x. x:A ==> d(c(x)) = x |]
==> (\<lambda>x\<in>A. c(x)) \<in> inj(A,B)"
apply (rule_tac d = d in f_imp_injective)
@@ -127,17 +127,17 @@
text{* f: bij(A,B) ==> f: A->B *}
lemmas bij_is_fun = bij_is_inj [THEN inj_is_fun]
-lemma lam_bijective:
- "[| !!x. x:A ==> c(x): B;
- !!y. y:B ==> d(y): A;
- !!x. x:A ==> d(c(x)) = x;
- !!y. y:B ==> c(d(y)) = y
+lemma lam_bijective:
+ "[| !!x. x:A ==> c(x): B;
+ !!y. y:B ==> d(y): A;
+ !!x. x:A ==> d(c(x)) = x;
+ !!y. y:B ==> c(d(y)) = y
|] ==> (\<lambda>x\<in>A. c(x)) \<in> bij(A,B)"
apply (unfold bij_def)
apply (blast intro!: lam_injective lam_surjective)
done
-lemma RepFun_bijective: "(\<forall>y\<in>x. EX! y'. f(y') = f(y))
+lemma RepFun_bijective: "(\<forall>y\<in>x. EX! y'. f(y') = f(y))
==> (\<lambda>z\<in>{f(y). y:x}. THE y. f(y) = z) \<in> bij({f(y). y:x}, x)"
apply (rule_tac d = f in lam_bijective)
apply (auto simp add: the_equality2)
@@ -171,7 +171,7 @@
lemma id_subset_inj: "A<=B ==> id(A): inj(A,B)"
apply (simp add: inj_def id_def)
-apply (blast intro: lam_type)
+apply (blast intro: lam_type)
done
lemmas id_inj = subset_refl [THEN id_subset_inj]
@@ -186,13 +186,13 @@
apply (blast intro: id_inj id_surj)
done
-lemma subset_iff_id: "A \<subseteq> B <-> id(A) \<in> A->B"
+lemma subset_iff_id: "A \<subseteq> B \<longleftrightarrow> id(A) \<in> A->B"
apply (unfold id_def)
apply (force intro!: lam_type dest: apply_type)
done
text{*@{term id} as the identity relation*}
-lemma id_iff [simp]: "<x,y> \<in> id(A) <-> x=y & y \<in> A"
+lemma id_iff [simp]: "<x,y> \<in> id(A) \<longleftrightarrow> x=y & y \<in> A"
by auto
@@ -224,7 +224,7 @@
lemma right_inverse_lemma:
"[| f: A->B; converse(f): C->A; b: C |] ==> f`(converse(f)`b) = b"
-by (rule apply_Pair [THEN converseD [THEN apply_equality]], auto)
+by (rule apply_Pair [THEN converseD [THEN apply_equality]], auto)
(*Should the premises be f:surj(A,B), b:B for symmetry with left_inverse?
No: they would not imply that converse(f) was a function! *)
@@ -239,14 +239,14 @@
lemma inj_converse_inj: "f: inj(A,B) ==> converse(f): inj(range(f), A)"
apply (rule f_imp_injective)
-apply (erule inj_converse_fun, clarify)
+apply (erule inj_converse_fun, clarify)
apply (rule right_inverse)
apply assumption
-apply blast
+apply blast
done
lemma inj_converse_surj: "f: inj(A,B) ==> converse(f): surj(range(f), A)"
-by (blast intro: f_imp_surjective inj_converse_fun left_inverse inj_is_fun
+by (blast intro: f_imp_surjective inj_converse_fun left_inverse inj_is_fun
range_of_fun [THEN apply_type])
text{*Adding this as an intro! rule seems to cause looping*}
@@ -264,17 +264,17 @@
lemma compI [intro]: "[| <a,b>:s; <b,c>:r |] ==> <a,c> \<in> r O s"
by (unfold comp_def, blast)
-lemma compE [elim!]:
- "[| xz \<in> r O s;
+lemma compE [elim!]:
+ "[| xz \<in> r O s;
!!x y z. [| xz=<x,z>; <x,y>:s; <y,z>:r |] ==> P |]
==> P"
by (unfold comp_def, blast)
-lemma compEpair:
- "[| <a,c> \<in> r O s;
+lemma compEpair:
+ "[| <a,c> \<in> r O s;
!!y. [| <a,y>:s; <y,c>:r |] ==> P |]
==> P"
-by (erule compE, simp)
+by (erule compE, simp)
lemma converse_comp: "converse(R O S) = converse(S) O converse(R)"
by blast
@@ -302,7 +302,7 @@
by (auto simp add: inj_def Pi_iff function_def)
lemma inj_bij_range: "f: inj(A,B) ==> f \<in> bij(A,range(f))"
- by (auto simp add: bij_def intro: inj_inj_range inj_is_fun fun_is_surj)
+ by (auto simp add: bij_def intro: inj_inj_range inj_is_fun fun_is_surj)
subsection{*Other Results*}
@@ -319,7 +319,7 @@
by blast
(*left identity of composition; provable inclusions are
- id(A) O r \<subseteq> r
+ id(A) O r \<subseteq> r
and [| r<=A*B; B<=C |] ==> r \<subseteq> id(C) O r *)
lemma left_comp_id: "r<=A*B ==> id(B) O r = r"
by blast
@@ -339,44 +339,44 @@
text{*Don't think the premises can be weakened much*}
lemma comp_fun: "[| g: A->B; f: B->C |] ==> (f O g) \<in> A->C"
apply (auto simp add: Pi_def comp_function Pow_iff comp_rel)
-apply (subst range_rel_subset [THEN domain_comp_eq], auto)
+apply (subst range_rel_subset [THEN domain_comp_eq], auto)
done
(*Thanks to the new definition of "apply", the premise f: B->C is gone!*)
lemma comp_fun_apply [simp]:
"[| g: A->B; a:A |] ==> (f O g)`a = f`(g`a)"
-apply (frule apply_Pair, assumption)
+apply (frule apply_Pair, assumption)
apply (simp add: apply_def image_comp)
-apply (blast dest: apply_equality)
+apply (blast dest: apply_equality)
done
text{*Simplifies compositions of lambda-abstractions*}
-lemma comp_lam:
+lemma comp_lam:
"[| !!x. x:A ==> b(x): B |]
==> (\<lambda>y\<in>B. c(y)) O (\<lambda>x\<in>A. b(x)) = (\<lambda>x\<in>A. c(b(x)))"
-apply (subgoal_tac "(\<lambda>x\<in>A. b(x)) \<in> A -> B")
+apply (subgoal_tac "(\<lambda>x\<in>A. b(x)) \<in> A -> B")
apply (rule fun_extension)
apply (blast intro: comp_fun lam_funtype)
apply (rule lam_funtype)
- apply simp
-apply (simp add: lam_type)
+ apply simp
+apply (simp add: lam_type)
done
lemma comp_inj:
"[| g: inj(A,B); f: inj(B,C) |] ==> (f O g) \<in> inj(A,C)"
-apply (frule inj_is_fun [of g])
-apply (frule inj_is_fun [of f])
+apply (frule inj_is_fun [of g])
+apply (frule inj_is_fun [of f])
apply (rule_tac d = "%y. converse (g) ` (converse (f) ` y)" in f_imp_injective)
- apply (blast intro: comp_fun, simp)
+ apply (blast intro: comp_fun, simp)
done
-lemma comp_surj:
+lemma comp_surj:
"[| g: surj(A,B); f: surj(B,C) |] ==> (f O g) \<in> surj(A,C)"
apply (unfold surj_def)
apply (blast intro!: comp_fun comp_fun_apply)
done
-lemma comp_bij:
+lemma comp_bij:
"[| g: bij(A,B); f: bij(B,C) |] ==> (f O g) \<in> bij(A,C)"
apply (unfold bij_def)
apply (blast intro: comp_inj comp_surj)
@@ -386,14 +386,14 @@
subsection{*Dual Properties of @{term inj} and @{term surj}*}
text{*Useful for proofs from
- D Pastre. Automatic theorem proving in set theory.
+ D Pastre. Automatic theorem proving in set theory.
Artificial Intelligence, 10:1--27, 1978.*}
-lemma comp_mem_injD1:
+lemma comp_mem_injD1:
"[| (f O g): inj(A,C); g: A->B; f: B->C |] ==> g: inj(A,B)"
-by (unfold inj_def, force)
+by (unfold inj_def, force)
-lemma comp_mem_injD2:
+lemma comp_mem_injD2:
"[| (f O g): inj(A,C); g: surj(A,B); f: B->C |] ==> f: inj(B,C)"
apply (unfold inj_def surj_def, safe)
apply (rule_tac x1 = x in bspec [THEN bexE])
@@ -403,17 +403,17 @@
apply (simp (no_asm_simp))
done
-lemma comp_mem_surjD1:
+lemma comp_mem_surjD1:
"[| (f O g): surj(A,C); g: A->B; f: B->C |] ==> f: surj(B,C)"
apply (unfold surj_def)
apply (blast intro!: comp_fun_apply [symmetric] apply_funtype)
done
-lemma comp_mem_surjD2:
+lemma comp_mem_surjD2:
"[| (f O g): surj(A,C); g: A->B; f: inj(B,C) |] ==> g: surj(A,B)"
apply (unfold inj_def surj_def, safe)
-apply (drule_tac x = "f`y" in bspec, auto)
+apply (drule_tac x = "f`y" in bspec, auto)
apply (blast intro: apply_funtype)
done
@@ -422,16 +422,16 @@
text{*left inverse of composition; one inclusion is
@{term "f: A->B ==> id(A) \<subseteq> converse(f) O f"} *}
lemma left_comp_inverse: "f: inj(A,B) ==> converse(f) O f = id(A)"
-apply (unfold inj_def, clarify)
-apply (rule equalityI)
- apply (auto simp add: apply_iff, blast)
+apply (unfold inj_def, clarify)
+apply (rule equalityI)
+ apply (auto simp add: apply_iff, blast)
done
text{*right inverse of composition; one inclusion is
@{term "f: A->B ==> f O converse(f) \<subseteq> id(B)"} *}
-lemma right_comp_inverse:
+lemma right_comp_inverse:
"f: surj(A,B) ==> f O converse(f) = id(B)"
-apply (simp add: surj_def, clarify)
+apply (simp add: surj_def, clarify)
apply (rule equalityI)
apply (best elim: domain_type range_type dest: apply_equality2)
apply (blast intro: apply_Pair)
@@ -440,8 +440,8 @@
subsubsection{*Proving that a Function is a Bijection*}
-lemma comp_eq_id_iff:
- "[| f: A->B; g: B->A |] ==> f O g = id(B) <-> (\<forall>y\<in>B. f`(g`y)=y)"
+lemma comp_eq_id_iff:
+ "[| f: A->B; g: B->A |] ==> f O g = id(B) \<longleftrightarrow> (\<forall>y\<in>B. f`(g`y)=y)"
apply (unfold id_def, safe)
apply (drule_tac t = "%h. h`y " in subst_context)
apply simp
@@ -450,7 +450,7 @@
apply auto
done
-lemma fg_imp_bijective:
+lemma fg_imp_bijective:
"[| f: A->B; g: B->A; f O g = id(B); g O f = id(A) |] ==> f \<in> bij(A,B)"
apply (unfold bij_def)
apply (simp add: comp_eq_id_iff)
@@ -462,7 +462,7 @@
lemma invertible_imp_bijective:
"[| converse(f): B->A; f: A->B |] ==> f \<in> bij(A,B)"
-by (simp add: fg_imp_bijective comp_eq_id_iff
+by (simp add: fg_imp_bijective comp_eq_id_iff
left_inverse_lemma right_inverse_lemma)
subsubsection{*Unions of Functions*}
@@ -471,25 +471,25 @@
text{*Theorem by KG, proof by LCP*}
lemma inj_disjoint_Un:
- "[| f: inj(A,B); g: inj(C,D); B \<inter> D = 0 |]
+ "[| f: inj(A,B); g: inj(C,D); B \<inter> D = 0 |]
==> (\<lambda>a\<in>A \<union> C. if a:A then f`a else g`a) \<in> inj(A \<union> C, B \<union> D)"
-apply (rule_tac d = "%z. if z:B then converse (f) `z else converse (g) `z"
+apply (rule_tac d = "%z. if z:B then converse (f) `z else converse (g) `z"
in lam_injective)
apply (auto simp add: inj_is_fun [THEN apply_type])
done
-lemma surj_disjoint_Un:
- "[| f: surj(A,B); g: surj(C,D); A \<inter> C = 0 |]
+lemma surj_disjoint_Un:
+ "[| f: surj(A,B); g: surj(C,D); A \<inter> C = 0 |]
==> (f \<union> g) \<in> surj(A \<union> C, B \<union> D)"
-apply (simp add: surj_def fun_disjoint_Un)
-apply (blast dest!: domain_of_fun
+apply (simp add: surj_def fun_disjoint_Un)
+apply (blast dest!: domain_of_fun
intro!: fun_disjoint_apply1 fun_disjoint_apply2)
done
text{*A simple, high-level proof; the version for injections follows from it,
- using @term{f:inj(A,B) <-> f:bij(A,range(f))} *}
+ using @{term "f:inj(A,B) \<longleftrightarrow> f:bij(A,range(f))"} *}
lemma bij_disjoint_Un:
- "[| f: bij(A,B); g: bij(C,D); A \<inter> C = 0; B \<inter> D = 0 |]
+ "[| f: bij(A,B); g: bij(C,D); A \<inter> C = 0; B \<inter> D = 0 |]
==> (f \<union> g) \<in> bij(A \<union> C, B \<union> D)"
apply (rule invertible_imp_bijective)
apply (subst converse_Un)
@@ -501,25 +501,25 @@
lemma surj_image:
"f: Pi(A,B) ==> f: surj(A, f``A)"
-apply (simp add: surj_def)
-apply (blast intro: apply_equality apply_Pair Pi_type)
+apply (simp add: surj_def)
+apply (blast intro: apply_equality apply_Pair Pi_type)
done
lemma restrict_image [simp]: "restrict(f,A) `` B = f `` (A \<inter> B)"
by (auto simp add: restrict_def)
-lemma restrict_inj:
+lemma restrict_inj:
"[| f: inj(A,B); C<=A |] ==> restrict(f,C): inj(C,B)"
apply (unfold inj_def)
-apply (safe elim!: restrict_type2, auto)
+apply (safe elim!: restrict_type2, auto)
done
lemma restrict_surj: "[| f: Pi(A,B); C<=A |] ==> restrict(f,C): surj(C, f``C)"
apply (insert restrict_type2 [THEN surj_image])
-apply (simp add: restrict_image)
+apply (simp add: restrict_image)
done
-lemma restrict_bij:
+lemma restrict_bij:
"[| f: inj(A,B); C<=A |] ==> restrict(f,C): bij(C, f``C)"
apply (simp add: inj_def bij_def)
apply (blast intro: restrict_surj surj_is_fun)
@@ -541,8 +541,8 @@
done
-lemma inj_extend:
- "[| f: inj(A,B); a\<notin>A; b\<notin>B |]
+lemma inj_extend:
+ "[| f: inj(A,B); a\<notin>A; b\<notin>B |]
==> cons(<a,b>,f) \<in> inj(cons(a,A), cons(b,B))"
apply (unfold inj_def)
apply (force intro: apply_type simp add: fun_extend)
--- a/src/ZF/QPair.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/QPair.thy Tue Mar 06 16:06:52 2012 +0000
@@ -77,7 +77,7 @@
lemma QPair_empty [simp]: "<0;0> = 0"
by (simp add: QPair_def)
-lemma QPair_iff [simp]: "<a;b> = <c;d> <-> a=c & b=d"
+lemma QPair_iff [simp]: "<a;b> = <c;d> \<longleftrightarrow> a=c & b=d"
apply (simp add: QPair_def)
apply (rule sum_equal_iff)
done
@@ -160,7 +160,7 @@
by auto
lemma expand_qsplit:
- "u: A<*>B ==> R(qsplit(c,u)) <-> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x;y> \<longrightarrow> R(c(x,y)))"
+ "u: A<*>B ==> R(qsplit(c,u)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x;y> \<longrightarrow> R(c(x,y)))"
apply (simp add: qsplit_def, auto)
done
@@ -232,16 +232,16 @@
(** Injection and freeness equivalences, for rewriting **)
-lemma QInl_iff [iff]: "QInl(a)=QInl(b) <-> a=b"
+lemma QInl_iff [iff]: "QInl(a)=QInl(b) \<longleftrightarrow> a=b"
by (simp add: qsum_defs )
-lemma QInr_iff [iff]: "QInr(a)=QInr(b) <-> a=b"
+lemma QInr_iff [iff]: "QInr(a)=QInr(b) \<longleftrightarrow> a=b"
by (simp add: qsum_defs )
-lemma QInl_QInr_iff [simp]: "QInl(a)=QInr(b) <-> False"
+lemma QInl_QInr_iff [simp]: "QInl(a)=QInr(b) \<longleftrightarrow> False"
by (simp add: qsum_defs )
-lemma QInr_QInl_iff [simp]: "QInr(b)=QInl(a) <-> False"
+lemma QInr_QInl_iff [simp]: "QInr(b)=QInl(a) \<longleftrightarrow> False"
by (simp add: qsum_defs )
lemma qsum_empty [simp]: "0<+>0 = 0"
@@ -263,13 +263,13 @@
(** <+> is itself injective... who cares?? **)
lemma qsum_iff:
- "u: A <+> B <-> (\<exists>x. x:A & u=QInl(x)) | (\<exists>y. y:B & u=QInr(y))"
+ "u: A <+> B \<longleftrightarrow> (\<exists>x. x:A & u=QInl(x)) | (\<exists>y. y:B & u=QInr(y))"
by blast
-lemma qsum_subset_iff: "A <+> B \<subseteq> C <+> D <-> A<=C & B<=D"
+lemma qsum_subset_iff: "A <+> B \<subseteq> C <+> D \<longleftrightarrow> A<=C & B<=D"
by blast
-lemma qsum_equal_iff: "A <+> B = C <+> D <-> A=C & B=D"
+lemma qsum_equal_iff: "A <+> B = C <+> D \<longleftrightarrow> A=C & B=D"
apply (simp (no_asm) add: extension qsum_subset_iff)
apply blast
done
--- a/src/ZF/QUniv.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/QUniv.thy Tue Mar 06 16:06:52 2012 +0000
@@ -130,7 +130,7 @@
lemmas quniv_QPair_E = quniv_QPair_D [THEN conjE]
-lemma quniv_QPair_iff: "<a;b> \<in> quniv(A) <-> a: quniv(A) & b: quniv(A)"
+lemma quniv_QPair_iff: "<a;b> \<in> quniv(A) \<longleftrightarrow> a: quniv(A) & b: quniv(A)"
by (blast intro: QPair_in_quniv dest: quniv_QPair_D)
--- a/src/ZF/Sum.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Sum.thy Tue Mar 06 16:06:52 2012 +0000
@@ -28,7 +28,7 @@
subsection{*Rules for the @{term Part} Primitive*}
lemma Part_iff:
- "a \<in> Part(A,h) <-> a:A & (\<exists>y. a=h(y))"
+ "a \<in> Part(A,h) \<longleftrightarrow> a:A & (\<exists>y. a=h(y))"
apply (unfold Part_def)
apply (rule separation)
done
@@ -77,16 +77,16 @@
(** Injection and freeness equivalences, for rewriting **)
-lemma Inl_iff [iff]: "Inl(a)=Inl(b) <-> a=b"
+lemma Inl_iff [iff]: "Inl(a)=Inl(b) \<longleftrightarrow> a=b"
by (simp add: sum_defs)
-lemma Inr_iff [iff]: "Inr(a)=Inr(b) <-> a=b"
+lemma Inr_iff [iff]: "Inr(a)=Inr(b) \<longleftrightarrow> a=b"
by (simp add: sum_defs)
-lemma Inl_Inr_iff [simp]: "Inl(a)=Inr(b) <-> False"
+lemma Inl_Inr_iff [simp]: "Inl(a)=Inr(b) \<longleftrightarrow> False"
by (simp add: sum_defs)
-lemma Inr_Inl_iff [simp]: "Inr(b)=Inl(a) <-> False"
+lemma Inr_Inl_iff [simp]: "Inr(b)=Inl(a) \<longleftrightarrow> False"
by (simp add: sum_defs)
lemma sum_empty [simp]: "0+0 = 0"
@@ -106,19 +106,19 @@
lemma InrD: "Inr(b): A+B ==> b: B"
by blast
-lemma sum_iff: "u: A+B <-> (\<exists>x. x:A & u=Inl(x)) | (\<exists>y. y:B & u=Inr(y))"
+lemma sum_iff: "u: A+B \<longleftrightarrow> (\<exists>x. x:A & u=Inl(x)) | (\<exists>y. y:B & u=Inr(y))"
by blast
-lemma Inl_in_sum_iff [simp]: "(Inl(x) \<in> A+B) <-> (x \<in> A)";
+lemma Inl_in_sum_iff [simp]: "(Inl(x) \<in> A+B) \<longleftrightarrow> (x \<in> A)";
by auto
-lemma Inr_in_sum_iff [simp]: "(Inr(y) \<in> A+B) <-> (y \<in> B)";
+lemma Inr_in_sum_iff [simp]: "(Inr(y) \<in> A+B) \<longleftrightarrow> (y \<in> B)";
by auto
-lemma sum_subset_iff: "A+B \<subseteq> C+D <-> A<=C & B<=D"
+lemma sum_subset_iff: "A+B \<subseteq> C+D \<longleftrightarrow> A<=C & B<=D"
by blast
-lemma sum_equal_iff: "A+B = C+D <-> A=C & B=D"
+lemma sum_equal_iff: "A+B = C+D \<longleftrightarrow> A=C & B=D"
by (simp add: extension sum_subset_iff, blast)
lemma sum_eq_2_times: "A+A = 2*A"
@@ -141,7 +141,7 @@
by auto
lemma expand_case: "u: A+B ==>
- R(case(c,d,u)) <->
+ R(case(c,d,u)) \<longleftrightarrow>
((\<forall>x\<in>A. u = Inl(x) \<longrightarrow> R(c(x))) &
(\<forall>y\<in>B. u = Inr(y) \<longrightarrow> R(d(y))))"
by auto
--- a/src/ZF/Univ.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Univ.thy Tue Mar 06 16:06:52 2012 +0000
@@ -433,10 +433,10 @@
by (blast intro: VsetI_lemma elim: ltE)
text{*Merely a lemma for the next result*}
-lemma Vset_Ord_rank_iff: "Ord(i) ==> b \<in> Vset(i) <-> rank(b) < i"
+lemma Vset_Ord_rank_iff: "Ord(i) ==> b \<in> Vset(i) \<longleftrightarrow> rank(b) < i"
by (blast intro: VsetD VsetI)
-lemma Vset_rank_iff [simp]: "b \<in> Vset(a) <-> rank(b) < rank(a)"
+lemma Vset_rank_iff [simp]: "b \<in> Vset(a) \<longleftrightarrow> rank(b) < rank(a)"
apply (rule Vfrom_rank_eq [THEN subst])
apply (rule Ord_rank [THEN Vset_Ord_rank_iff])
done
@@ -766,10 +766,10 @@
text{*This weaker version says a, b exist at the same level*}
lemmas Vfrom_doubleton_D = Transset_Vfrom [THEN Transset_doubleton_D]
-(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i)
- implies a, b : Vfrom(X,i), which is useless for induction.
- Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i)))
- implies a, b : Vfrom(X,i), leaving the succ(i) case untreated.
+(** Using only the weaker theorem would prove <a,b> \<in> Vfrom(X,i)
+ implies a, b \<in> Vfrom(X,i), which is useless for induction.
+ Using only the stronger theorem would prove <a,b> \<in> Vfrom(X,succ(succ(i)))
+ implies a, b \<in> Vfrom(X,i), leaving the succ(i) case untreated.
The combination gives a reduction by precisely one level, which is
most convenient for proofs.
**)
--- a/src/ZF/WF.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/WF.thy Tue Mar 06 16:06:52 2012 +0000
@@ -63,7 +63,7 @@
lemma wf_on_field_imp_wf: "wf[field(r)](r) ==> wf(r)"
by (unfold wf_def wf_on_def, fast)
-lemma wf_iff_wf_on_field: "wf(r) <-> wf[field(r)](r)"
+lemma wf_iff_wf_on_field: "wf(r) \<longleftrightarrow> wf[field(r)](r)"
by (blast intro: wf_imp_wf_on wf_on_field_imp_wf)
lemma wf_on_subset_A: "[| wf[A](r); B<=A |] ==> wf[B](r)"
@@ -245,7 +245,7 @@
apply (elim ssubst)
apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def)
apply (rule_tac t = "%z. H (?x,z) " in subst_context)
-apply (subgoal_tac "\<forall>y\<in>r-``{x}. \<forall>z. <y,z>:f <-> <y,z>:g")
+apply (subgoal_tac "\<forall>y\<in>r-``{x}. \<forall>z. <y,z>:f \<longleftrightarrow> <y,z>:g")
apply (blast dest: transD)
apply (simp add: apply_iff)
apply (blast dest: transD intro: sym)
@@ -364,7 +364,7 @@
text{*Minimal-element characterization of well-foundedness*}
lemma wf_eq_minimal:
- "wf(r) <-> (\<forall>Q x. x:Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. <y,z>:r \<longrightarrow> y\<notin>Q))"
+ "wf(r) \<longleftrightarrow> (\<forall>Q x. x:Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. <y,z>:r \<longrightarrow> y\<notin>Q))"
by (unfold wf_def, blast)
end
--- a/src/ZF/equalities.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/equalities.thy Tue Mar 06 16:06:52 2012 +0000
@@ -22,21 +22,21 @@
The following are not added to the default simpset because
(a) they duplicate the body and (b) there are no similar rules for @{text Int}.*}
-lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) <-> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))";
+lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))";
by blast
-lemma bex_Un: "(\<exists>x \<in> A\<union>B. P(x)) <-> (\<exists>x \<in> A. P(x)) | (\<exists>x \<in> B. P(x))";
+lemma bex_Un: "(\<exists>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<exists>x \<in> A. P(x)) | (\<exists>x \<in> B. P(x))";
by blast
-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))"
+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))"
by blast
-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))"
+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))"
by blast
subsection{*Converse of a Relation*}
-lemma converse_iff [simp]: "<a,b>\<in> converse(r) <-> <b,a>\<in>r"
+lemma converse_iff [simp]: "<a,b>\<in> converse(r) \<longleftrightarrow> <b,a>\<in>r"
by (unfold converse_def, blast)
lemma converseI [intro!]: "<a,b>\<in>r ==> <b,a>\<in>converse(r)"
@@ -64,7 +64,7 @@
by blast
lemma converse_subset_iff:
- "A \<subseteq> Sigma(X,Y) ==> converse(A) \<subseteq> converse(B) <-> A \<subseteq> B"
+ "A \<subseteq> Sigma(X,Y) ==> converse(A) \<subseteq> converse(B) \<longleftrightarrow> A \<subseteq> B"
by blast
@@ -76,17 +76,17 @@
lemma subset_consI: "B \<subseteq> cons(a,B)"
by blast
-lemma cons_subset_iff [iff]: "cons(a,B)\<subseteq>C <-> a\<in>C & B\<subseteq>C"
+lemma cons_subset_iff [iff]: "cons(a,B)\<subseteq>C \<longleftrightarrow> a\<in>C & B\<subseteq>C"
by blast
(*A safe special case of subset elimination, adding no new variables
[| cons(a,B) \<subseteq> C; [| a \<in> C; B \<subseteq> C |] ==> R |] ==> R *)
lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE]
-lemma subset_empty_iff: "A\<subseteq>0 <-> A=0"
+lemma subset_empty_iff: "A\<subseteq>0 \<longleftrightarrow> A=0"
by blast
-lemma subset_cons_iff: "C\<subseteq>cons(a,B) <-> C\<subseteq>B | (a\<in>C & C-{a} \<subseteq> B)"
+lemma subset_cons_iff: "C\<subseteq>cons(a,B) \<longleftrightarrow> C\<subseteq>B | (a\<in>C & C-{a} \<subseteq> B)"
by blast
(* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)
@@ -134,7 +134,7 @@
"[| succ(i) \<subseteq> j; [| i\<in>j; i\<subseteq>j |] ==> P |] ==> P"
by (unfold succ_def, blast)
-lemma succ_subset_iff: "succ(a) \<subseteq> B <-> (a \<subseteq> B & a \<in> B)"
+lemma succ_subset_iff: "succ(a) \<subseteq> B \<longleftrightarrow> (a \<subseteq> B & a \<in> B)"
by (unfold succ_def, blast)
@@ -142,7 +142,7 @@
(** Intersection is the greatest lower bound of two sets **)
-lemma Int_subset_iff: "C \<subseteq> A \<inter> B <-> C \<subseteq> A & C \<subseteq> B"
+lemma Int_subset_iff: "C \<subseteq> A \<inter> B \<longleftrightarrow> C \<subseteq> A & C \<subseteq> B"
by blast
lemma Int_lower1: "A \<inter> B \<subseteq> A"
@@ -187,10 +187,10 @@
lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
by blast
-lemma subset_Int_iff: "A\<subseteq>B <-> A \<inter> B = A"
+lemma subset_Int_iff: "A\<subseteq>B \<longleftrightarrow> A \<inter> B = A"
by (blast elim!: equalityE)
-lemma subset_Int_iff2: "A\<subseteq>B <-> B \<inter> A = A"
+lemma subset_Int_iff2: "A\<subseteq>B \<longleftrightarrow> B \<inter> A = A"
by (blast elim!: equalityE)
lemma Int_Diff_eq: "C\<subseteq>A ==> (A-B) \<inter> C = C-B"
@@ -211,7 +211,7 @@
(** Union is the least upper bound of two sets *)
-lemma Un_subset_iff: "A \<union> B \<subseteq> C <-> A \<subseteq> C & B \<subseteq> C"
+lemma Un_subset_iff: "A \<union> B \<subseteq> C \<longleftrightarrow> A \<subseteq> C & B \<subseteq> C"
by blast
lemma Un_upper1: "A \<subseteq> A \<union> B"
@@ -253,13 +253,13 @@
lemma Un_Int_distrib: "(A \<inter> B) \<union> C = (A \<union> C) \<inter> (B \<union> C)"
by blast
-lemma subset_Un_iff: "A\<subseteq>B <-> A \<union> B = B"
+lemma subset_Un_iff: "A\<subseteq>B \<longleftrightarrow> A \<union> B = B"
by (blast elim!: equalityE)
-lemma subset_Un_iff2: "A\<subseteq>B <-> B \<union> A = B"
+lemma subset_Un_iff2: "A\<subseteq>B \<longleftrightarrow> B \<union> A = B"
by (blast elim!: equalityE)
-lemma Un_empty [iff]: "(A \<union> B = 0) <-> (A = 0 & B = 0)"
+lemma Un_empty [iff]: "(A \<union> B = 0) \<longleftrightarrow> (A = 0 & B = 0)"
by blast
lemma Un_eq_Union: "A \<union> B = \<Union>({A, B})"
@@ -273,7 +273,7 @@
lemma Diff_contains: "[| C\<subseteq>A; C \<inter> B = 0 |] ==> C \<subseteq> A-B"
by blast
-lemma subset_Diff_cons_iff: "B \<subseteq> A - cons(c,C) <-> B\<subseteq>A-C & c \<notin> B"
+lemma subset_Diff_cons_iff: "B \<subseteq> A - cons(c,C) \<longleftrightarrow> B\<subseteq>A-C & c \<notin> B"
by blast
lemma Diff_cancel: "A - A = 0"
@@ -288,7 +288,7 @@
lemma Diff_0 [simp]: "A - 0 = A"
by blast
-lemma Diff_eq_0_iff: "A - B = 0 <-> A \<subseteq> B"
+lemma Diff_eq_0_iff: "A - B = 0 \<longleftrightarrow> A \<subseteq> B"
by (blast elim: equalityE)
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
@@ -338,7 +338,7 @@
by blast
(*Halmos, Naive Set Theory, page 16.*)
-lemma Un_Int_assoc_iff: "(A \<inter> B) \<union> C = A \<inter> (B \<union> C) <-> C\<subseteq>A"
+lemma Un_Int_assoc_iff: "(A \<inter> B) \<union> C = A \<inter> (B \<union> C) \<longleftrightarrow> C\<subseteq>A"
by (blast elim!: equalityE)
@@ -346,7 +346,7 @@
(** Big Union is the least upper bound of a set **)
-lemma Union_subset_iff: "\<Union>(A) \<subseteq> C <-> (\<forall>x\<in>A. x \<subseteq> C)"
+lemma Union_subset_iff: "\<Union>(A) \<subseteq> C \<longleftrightarrow> (\<forall>x\<in>A. x \<subseteq> C)"
by blast
lemma Union_upper: "B\<in>A ==> B \<subseteq> \<Union>(A)"
@@ -364,10 +364,10 @@
lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>(A) \<inter> \<Union>(B)"
by blast
-lemma Union_disjoint: "\<Union>(C) \<inter> A = 0 <-> (\<forall>B\<in>C. B \<inter> A = 0)"
+lemma Union_disjoint: "\<Union>(C) \<inter> A = 0 \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = 0)"
by (blast elim!: equalityE)
-lemma Union_empty_iff: "\<Union>(A) = 0 <-> (\<forall>B\<in>A. B=0)"
+lemma Union_empty_iff: "\<Union>(A) = 0 \<longleftrightarrow> (\<forall>B\<in>A. B=0)"
by blast
lemma Int_Union2: "\<Union>(B) \<inter> A = (\<Union>C\<in>B. C \<inter> A)"
@@ -375,7 +375,7 @@
(** Big Intersection is the greatest lower bound of a nonempty set **)
-lemma Inter_subset_iff: "A\<noteq>0 ==> C \<subseteq> \<Inter>(A) <-> (\<forall>x\<in>A. C \<subseteq> x)"
+lemma Inter_subset_iff: "A\<noteq>0 ==> C \<subseteq> \<Inter>(A) \<longleftrightarrow> (\<forall>x\<in>A. C \<subseteq> x)"
by blast
lemma Inter_lower: "B\<in>A ==> \<Inter>(A) \<subseteq> B"
@@ -416,10 +416,10 @@
subsection{*Unions and Intersections of Families*}
-lemma subset_UN_iff_eq: "A \<subseteq> (\<Union>i\<in>I. B(i)) <-> A = (\<Union>i\<in>I. A \<inter> B(i))"
+lemma subset_UN_iff_eq: "A \<subseteq> (\<Union>i\<in>I. B(i)) \<longleftrightarrow> A = (\<Union>i\<in>I. A \<inter> B(i))"
by (blast elim!: equalityE)
-lemma UN_subset_iff: "(\<Union>x\<in>A. B(x)) \<subseteq> C <-> (\<forall>x\<in>A. B(x) \<subseteq> C)"
+lemma UN_subset_iff: "(\<Union>x\<in>A. B(x)) \<subseteq> C \<longleftrightarrow> (\<forall>x\<in>A. B(x) \<subseteq> C)"
by blast
lemma UN_upper: "x\<in>A ==> B(x) \<subseteq> (\<Union>x\<in>A. B(x))"
@@ -571,7 +571,7 @@
by blast
lemma times_subset_iff:
- "(A'*B' \<subseteq> A*B) <-> (A' = 0 | B' = 0 | (A'\<subseteq>A) & (B'\<subseteq>B))"
+ "(A'*B' \<subseteq> A*B) \<longleftrightarrow> (A' = 0 | B' = 0 | (A'\<subseteq>A) & (B'\<subseteq>B))"
by blast
lemma Int_Sigma_eq:
@@ -580,7 +580,7 @@
(** Domain **)
-lemma domain_iff: "a: domain(r) <-> (\<exists>y. <a,y>\<in> r)"
+lemma domain_iff: "a: domain(r) \<longleftrightarrow> (\<exists>y. <a,y>\<in> r)"
by (unfold domain_def, blast)
lemma domainI [intro]: "<a,b>\<in> r ==> a: domain(r)"
@@ -739,10 +739,10 @@
subsection{*Image of a Set under a Function or Relation*}
-lemma image_iff: "b \<in> r``A <-> (\<exists>x\<in>A. <x,b>\<in>r)"
+lemma image_iff: "b \<in> r``A \<longleftrightarrow> (\<exists>x\<in>A. <x,b>\<in>r)"
by (unfold image_def, blast)
-lemma image_singleton_iff: "b \<in> r``{a} <-> <a,b>\<in>r"
+lemma image_singleton_iff: "b \<in> r``{a} \<longleftrightarrow> <a,b>\<in>r"
by (rule image_iff [THEN iff_trans], blast)
lemma imageI [intro]: "[| <a,b>\<in> r; a\<in>A |] ==> b \<in> r``A"
@@ -792,10 +792,10 @@
subsection{*Inverse Image of a Set under a Function or Relation*}
lemma vimage_iff:
- "a \<in> r-``B <-> (\<exists>y\<in>B. <a,y>\<in>r)"
+ "a \<in> r-``B \<longleftrightarrow> (\<exists>y\<in>B. <a,y>\<in>r)"
by (unfold vimage_def image_def converse_def, blast)
-lemma vimage_singleton_iff: "a \<in> r-``{b} <-> <a,b>\<in>r"
+lemma vimage_singleton_iff: "a \<in> r-``{b} \<longleftrightarrow> <a,b>\<in>r"
by (rule vimage_iff [THEN iff_trans], blast)
lemma vimageI [intro]: "[| <a,b>\<in> r; b\<in>B |] ==> a \<in> r-``B"
@@ -897,7 +897,7 @@
lemma Union_Pow_eq [simp]: "\<Union>(Pow(A)) = A"
by blast
-lemma Union_Pow_iff: "\<Union>(A) \<in> Pow(B) <-> A \<in> Pow(Pow(B))"
+lemma Union_Pow_iff: "\<Union>(A) \<in> Pow(B) \<longleftrightarrow> A \<in> Pow(Pow(B))"
by blast
lemma Pow_Int_eq [simp]: "Pow(A \<inter> B) = Pow(A) \<inter> Pow(B)"
@@ -912,7 +912,7 @@
lemma RepFun_subset: "[| !!x. x\<in>A ==> f(x) \<in> B |] ==> {f(x). x\<in>A} \<subseteq> B"
by blast
-lemma RepFun_eq_0_iff [simp]: "{f(x).x\<in>A}=0 <-> A=0"
+lemma RepFun_eq_0_iff [simp]: "{f(x).x\<in>A}=0 \<longleftrightarrow> A=0"
by blast
lemma RepFun_constant [simp]: "{c. x\<in>A} = (if A=0 then 0 else {c})"
--- a/src/ZF/ex/Ring.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/ex/Ring.thy Tue Mar 06 16:06:52 2012 +0000
@@ -6,6 +6,10 @@
theory Ring imports Group begin
+no_notation
+ cadd (infixl "\<oplus>" 65) and
+ cmult (infixl "\<otimes>" 70)
+
(*First, we must simulate a record declaration:
record ring = monoid +
add :: "[i, i] => i" (infixl "\<oplus>\<index>" 65)
@@ -46,7 +50,7 @@
"\<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)"
locale abelian_monoid = fixes G (structure)
- assumes a_comm_monoid:
+ assumes a_comm_monoid:
"comm_monoid (<carrier(G), add_field(G), zero(G), 0>)"
text {*
@@ -54,7 +58,7 @@
*}
locale abelian_group = abelian_monoid +
- assumes a_comm_group:
+ assumes a_comm_group:
"comm_group (<carrier(G), add_field(G), zero(G), 0>)"
locale ring = abelian_group R + monoid R for R (structure) +
@@ -75,21 +79,21 @@
lemma (in abelian_monoid) a_monoid:
"monoid (<carrier(G), add_field(G), zero(G), 0>)"
-apply (insert a_comm_monoid)
-apply (simp add: comm_monoid_def)
+apply (insert a_comm_monoid)
+apply (simp add: comm_monoid_def)
done
lemma (in abelian_group) a_group:
"group (<carrier(G), add_field(G), zero(G), 0>)"
-apply (insert a_comm_group)
-apply (simp add: comm_group_def group_def)
+apply (insert a_comm_group)
+apply (simp add: comm_group_def group_def)
done
lemma (in abelian_monoid) l_zero [simp]:
"x \<in> carrier(G) \<Longrightarrow> \<zero> \<oplus> x = x"
apply (insert monoid.l_one [OF a_monoid])
-apply (simp add: ring_add_def)
+apply (simp add: ring_add_def)
done
lemma (in abelian_monoid) zero_closed [intro, simp]:
@@ -102,7 +106,7 @@
lemma (in abelian_monoid) a_closed [intro, simp]:
"[| x \<in> carrier(G); y \<in> carrier(G) |] ==> x \<oplus> y \<in> carrier(G)"
-by (rule monoid.m_closed [OF a_monoid,
+by (rule monoid.m_closed [OF a_monoid,
simplified, simplified ring_add_def [symmetric]])
lemma (in abelian_group) minus_closed [intro, simp]:
@@ -110,18 +114,18 @@
by (simp add: minus_def)
lemma (in abelian_group) a_l_cancel [simp]:
- "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
+ "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
\<Longrightarrow> (x \<oplus> y = x \<oplus> z) <-> (y = z)"
-by (rule group.l_cancel [OF a_group,
+by (rule group.l_cancel [OF a_group,
simplified, simplified ring_add_def [symmetric]])
lemma (in abelian_group) a_r_cancel [simp]:
- "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
+ "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
\<Longrightarrow> (y \<oplus> x = z \<oplus> x) <-> (y = z)"
by (rule group.r_cancel [OF a_group, simplified, simplified ring_add_def [symmetric]])
lemma (in abelian_monoid) a_assoc:
- "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
+ "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
\<Longrightarrow> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
by (rule monoid.m_assoc [OF a_monoid, simplified, simplified ring_add_def [symmetric]])
@@ -136,7 +140,7 @@
simplified, simplified ring_add_def [symmetric]])
lemma (in abelian_monoid) a_lcomm:
- "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
+ "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
\<Longrightarrow> x \<oplus> (y \<oplus> z) = y \<oplus> (x \<oplus> z)"
by (rule comm_monoid.m_lcomm [OF a_comm_monoid,
simplified, simplified ring_add_def [symmetric]])
@@ -168,7 +172,7 @@
lemmas (in abelian_monoid) a_ac = a_assoc a_comm a_lcomm
-text {*
+text {*
The following proofs are from Jacobson, Basic Algebra I, pp.~88--89
*}
@@ -179,7 +183,7 @@
proof -
assume R: "x \<in> carrier(R)"
then have "\<zero> \<cdot> x \<oplus> \<zero> \<cdot> x = (\<zero> \<oplus> \<zero>) \<cdot> x"
- by (blast intro: l_distr [THEN sym])
+ by (blast intro: l_distr [THEN sym])
also from R have "... = \<zero> \<cdot> x \<oplus> \<zero>" by simp
finally have "\<zero> \<cdot> x \<oplus> \<zero> \<cdot> x = \<zero> \<cdot> x \<oplus> \<zero>" .
with R show ?thesis by (simp del: r_zero)
@@ -250,12 +254,12 @@
by (auto simp add: ring_hom_def)
lemma ring_hom_mult:
- "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R); y \<in> carrier(R)\<rbrakk>
+ "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R); y \<in> carrier(R)\<rbrakk>
\<Longrightarrow> h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y)"
by (simp add: ring_hom_def)
lemma ring_hom_add:
- "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R); y \<in> carrier(R)\<rbrakk>
+ "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R); y \<in> carrier(R)\<rbrakk>
\<Longrightarrow> h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)"
by (simp add: ring_hom_def)
@@ -288,8 +292,8 @@
qed
lemma (in ring) id_ring_hom [simp]: "id(carrier(R)) \<in> ring_hom(R,R)"
-apply (rule ring_hom_memI)
-apply (auto simp add: id_type)
+apply (rule ring_hom_memI)
+apply (auto simp add: id_type)
done
end
--- a/src/ZF/func.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/func.thy Tue Mar 06 16:06:52 2012 +0000
@@ -20,12 +20,12 @@
by (simp add: restrict_def relation_def, blast)
lemma Pi_iff:
- "f: Pi(A,B) <-> function(f) & f<=Sigma(A,B) & A<=domain(f)"
+ "f: Pi(A,B) \<longleftrightarrow> function(f) & f<=Sigma(A,B) & A<=domain(f)"
by (unfold Pi_def, blast)
(*For upward compatibility with the former definition*)
lemma Pi_iff_old:
- "f: Pi(A,B) <-> f<=Sigma(A,B) & (\<forall>x\<in>A. EX! y. <x,y>: f)"
+ "f: Pi(A,B) \<longleftrightarrow> f<=Sigma(A,B) & (\<forall>x\<in>A. EX! y. <x,y>: f)"
by (unfold Pi_def function_def, blast)
lemma fun_is_function: "f: Pi(A,B) ==> function(f)"
@@ -96,7 +96,7 @@
lemma apply_funtype: "[| f: A->B; a:A |] ==> f`a \<in> B"
by (blast dest: apply_type)
-lemma apply_iff: "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b"
+lemma apply_iff: "f: Pi(A,B) ==> <a,b>: f \<longleftrightarrow> a:A & f`a = b"
apply (frule fun_is_rel)
apply (blast intro!: apply_Pair apply_equality)
done
@@ -110,7 +110,7 @@
(*Such functions arise in non-standard datatypes, ZF/ex/Ntree for instance*)
lemma Pi_Collect_iff:
"(f \<in> Pi(A, %x. {y:B(x). P(x,y)}))
- <-> f \<in> Pi(A,B) & (\<forall>x\<in>A. P(x, f`x))"
+ \<longleftrightarrow> f \<in> Pi(A,B) & (\<forall>x\<in>A. P(x, f`x))"
by (blast intro: Pi_type dest: apply_type)
lemma Pi_weaken_type:
@@ -222,11 +222,11 @@
done
lemma fun_extension_iff:
- "[| f:Pi(A,B); g:Pi(A,C) |] ==> (\<forall>a\<in>A. f`a = g`a) <-> f=g"
+ "[| f:Pi(A,B); g:Pi(A,C) |] ==> (\<forall>a\<in>A. f`a = g`a) \<longleftrightarrow> f=g"
by (blast intro: fun_extension)
(*thm by Mark Staples, proof by lcp*)
-lemma fun_subset_eq: "[| f:Pi(A,B); g:Pi(A,C) |] ==> f \<subseteq> g <-> (f = g)"
+lemma fun_subset_eq: "[| f:Pi(A,B); g:Pi(A,C) |] ==> f \<subseteq> g \<longleftrightarrow> (f = g)"
by (blast dest: apply_Pair
intro: fun_extension apply_equality [symmetric])
@@ -592,7 +592,7 @@
(* Useful with simp; contributed by Clemens Ballarin. *)
lemma bex_image_simp:
- "[| f \<in> Pi(X, Y); A \<subseteq> X |] ==> (\<exists>x\<in>f``A. P(x)) <-> (\<exists>x\<in>A. P(f`x))"
+ "[| f \<in> Pi(X, Y); A \<subseteq> X |] ==> (\<exists>x\<in>f``A. P(x)) \<longleftrightarrow> (\<exists>x\<in>A. P(f`x))"
apply safe
apply rule
prefer 2 apply assumption
@@ -601,7 +601,7 @@
done
lemma ball_image_simp:
- "[| f \<in> Pi(X, Y); A \<subseteq> X |] ==> (\<forall>x\<in>f``A. P(x)) <-> (\<forall>x\<in>A. P(f`x))"
+ "[| f \<in> Pi(X, Y); A \<subseteq> X |] ==> (\<forall>x\<in>f``A. P(x)) \<longleftrightarrow> (\<forall>x\<in>A. P(f`x))"
apply safe
apply (blast intro: apply_Pair)
apply (drule bspec) apply assumption
--- a/src/ZF/pair.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/pair.thy Tue Mar 06 16:06:52 2012 +0000
@@ -34,13 +34,13 @@
(** Lemmas for showing that <a,b> uniquely determines a and b **)
-lemma singleton_eq_iff [iff]: "{a} = {b} <-> a=b"
+lemma singleton_eq_iff [iff]: "{a} = {b} \<longleftrightarrow> a=b"
by (rule extension [THEN iff_trans], blast)
-lemma doubleton_eq_iff: "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)"
+lemma doubleton_eq_iff: "{a,b} = {c,d} \<longleftrightarrow> (a=c & b=d) | (a=d & b=c)"
by (rule extension [THEN iff_trans], blast)
-lemma Pair_iff [simp]: "<a,b> = <c,d> <-> a=c & b=d"
+lemma Pair_iff [simp]: "<a,b> = <c,d> \<longleftrightarrow> a=c & b=d"
by (simp add: Pair_def doubleton_eq_iff, blast)
lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, elim!]
@@ -76,7 +76,7 @@
text{*Generalizes Cartesian product*}
-lemma Sigma_iff [simp]: "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
+lemma Sigma_iff [simp]: "<a,b>: Sigma(A,B) \<longleftrightarrow> a:A & b:B(a)"
by (simp add: Sigma_def)
lemma SigmaI [TC,intro!]: "[| a:A; b:B(a) |] ==> <a,b> \<in> Sigma(A,B)"
@@ -113,7 +113,7 @@
lemma Sigma_empty2 [simp]: "A*0 = 0"
by blast
-lemma Sigma_empty_iff: "A*B=0 <-> A=0 | B=0"
+lemma Sigma_empty_iff: "A*B=0 \<longleftrightarrow> A=0 | B=0"
by blast
@@ -150,7 +150,7 @@
lemma expand_split:
"u: A*B ==>
- R(split(c,u)) <-> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x,y> \<longrightarrow> R(c(x,y)))"
+ R(split(c,u)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x,y> \<longrightarrow> R(c(x,y)))"
apply (simp add: split_def)
apply auto
done
@@ -177,11 +177,11 @@
*}
lemma split_paired_Bex_Sigma [simp]:
- "(\<exists>z \<in> Sigma(A,B). P(z)) <-> (\<exists>x \<in> A. \<exists>y \<in> B(x). P(<x,y>))"
+ "(\<exists>z \<in> Sigma(A,B). P(z)) \<longleftrightarrow> (\<exists>x \<in> A. \<exists>y \<in> B(x). P(<x,y>))"
by blast
lemma split_paired_Ball_Sigma [simp]:
- "(\<forall>z \<in> Sigma(A,B). P(z)) <-> (\<forall>x \<in> A. \<forall>y \<in> B(x). P(<x,y>))"
+ "(\<forall>z \<in> Sigma(A,B). P(z)) \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> B(x). P(<x,y>))"
by blast
end
--- a/src/ZF/upair.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/upair.thy Tue Mar 06 16:06:52 2012 +0000
@@ -23,7 +23,7 @@
subsection{*Unordered Pairs: constant @{term Upair}*}
-lemma Upair_iff [simp]: "c \<in> Upair(a,b) <-> (c=a | c=b)"
+lemma Upair_iff [simp]: "c \<in> Upair(a,b) \<longleftrightarrow> (c=a | c=b)"
by (unfold Upair_def, blast)
lemma UpairI1: "a \<in> Upair(a,b)"
@@ -37,7 +37,7 @@
subsection{*Rules for Binary Union, Defined via @{term Upair}*}
-lemma Un_iff [simp]: "c \<in> A \<union> B <-> (c:A | c:B)"
+lemma Un_iff [simp]: "c \<in> A \<union> B \<longleftrightarrow> (c:A | c:B)"
apply (simp add: Un_def)
apply (blast intro: UpairI1 UpairI2 elim: UpairE)
done
@@ -63,7 +63,7 @@
subsection{*Rules for Binary Intersection, Defined via @{term Upair}*}
-lemma Int_iff [simp]: "c \<in> A \<inter> B <-> (c:A & c:B)"
+lemma Int_iff [simp]: "c \<in> A \<inter> B \<longleftrightarrow> (c:A & c:B)"
apply (unfold Int_def)
apply (blast intro: UpairI1 UpairI2 elim: UpairE)
done
@@ -83,7 +83,7 @@
subsection{*Rules for Set Difference, Defined via @{term Upair}*}
-lemma Diff_iff [simp]: "c \<in> A-B <-> (c:A & c\<notin>B)"
+lemma Diff_iff [simp]: "c \<in> A-B \<longleftrightarrow> (c:A & c\<notin>B)"
by (unfold Diff_def, blast)
lemma DiffI [intro!]: "[| c \<in> A; c \<notin> B |] ==> c \<in> A - B"
@@ -101,7 +101,7 @@
subsection{*Rules for @{term cons}*}
-lemma cons_iff [simp]: "a \<in> cons(b,A) <-> (a=b | a:A)"
+lemma cons_iff [simp]: "a \<in> cons(b,A) \<longleftrightarrow> (a=b | a:A)"
apply (unfold cons_def)
apply (blast intro: UpairI1 UpairI2 elim: UpairE)
done
@@ -137,7 +137,7 @@
subsection{*Singletons*}
-lemma singleton_iff: "a \<in> {b} <-> a=b"
+lemma singleton_iff: "a \<in> {b} \<longleftrightarrow> a=b"
by simp
lemma singletonI [intro!]: "a \<in> {a}"
@@ -164,7 +164,7 @@
apply (blast+)
done
-(*No congruence rule is necessary: if @{term"\<forall>y.P(y)<->Q(y)"} then
+(*No congruence rule is necessary: if @{term"\<forall>y.P(y)\<longleftrightarrow>Q(y)"} then
@{term "THE x.P(x)"} rewrites to @{term "THE x.Q(x)"} *)
(*If it's "undefined", it's zero!*)
@@ -203,13 +203,13 @@
(*Never use with case splitting, or if P is known to be true or false*)
lemma if_cong:
- "[| P<->Q; Q ==> a=c; ~Q ==> b=d |]
+ "[| P\<longleftrightarrow>Q; Q ==> a=c; ~Q ==> b=d |]
==> (if P then a else b) = (if Q then c else d)"
by (simp add: if_def cong add: conj_cong)
(*Prevents simplification of x and y: faster and allows the execution
of functional programs. NOW THE DEFAULT.*)
-lemma if_weak_cong: "P<->Q ==> (if P then x else y) = (if Q then x else y)"
+lemma if_weak_cong: "P\<longleftrightarrow>Q ==> (if P then x else y) = (if Q then x else y)"
by simp
(*Not needed for rewriting, since P would rewrite to True anyway*)
@@ -221,7 +221,7 @@
by (unfold if_def, blast)
lemma split_if [split]:
- "P(if Q then x else y) <-> ((Q \<longrightarrow> P(x)) & (~Q \<longrightarrow> P(y)))"
+ "P(if Q then x else y) \<longleftrightarrow> ((Q \<longrightarrow> P(x)) & (~Q \<longrightarrow> P(y)))"
by (case_tac Q, simp_all)
(** Rewrite rules for boolean case-splitting: faster than split_if [split]
@@ -236,7 +236,7 @@
lemmas split_ifs = split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
(*Logically equivalent to split_if_mem2*)
-lemma if_iff: "a: (if P then x else y) <-> P & a:x | ~P & a:y"
+lemma if_iff: "a: (if P then x else y) \<longleftrightarrow> P & a:x | ~P & a:y"
by simp
lemma if_type [TC]:
@@ -245,7 +245,7 @@
(** Splitting IFs in the assumptions **)
-lemma split_if_asm: "P(if Q then x else y) <-> (~((Q & ~P(x)) | (~Q & ~P(y))))"
+lemma split_if_asm: "P(if Q then x else y) \<longleftrightarrow> (~((Q & ~P(x)) | (~Q & ~P(y))))"
by simp
lemmas if_splits = split_if split_if_asm
@@ -281,7 +281,7 @@
subsection{*Rules for Successor*}
-lemma succ_iff: "i \<in> succ(j) <-> i=j | i:j"
+lemma succ_iff: "i \<in> succ(j) \<longleftrightarrow> i=j | i:j"
by (unfold succ_def, blast)
lemma succI1 [simp]: "i \<in> succ(i)"
@@ -313,7 +313,7 @@
(* @{term"succ(b) \<noteq> b"} *)
lemmas succ_neq_self = succI1 [THEN mem_imp_not_eq, THEN not_sym]
-lemma succ_inject_iff [simp]: "succ(m) = succ(n) <-> m=n"
+lemma succ_inject_iff [simp]: "succ(m) = succ(n) \<longleftrightarrow> m=n"
by (blast elim: mem_asym elim!: equalityE)
lemmas succ_inject = succ_inject_iff [THEN iffD1, dest!]
@@ -322,83 +322,83 @@
subsection{*Miniscoping of the Bounded Universal Quantifier*}
lemma ball_simps1:
- "(\<forall>x\<in>A. P(x) & Q) <-> (\<forall>x\<in>A. P(x)) & (A=0 | Q)"
- "(\<forall>x\<in>A. P(x) | Q) <-> ((\<forall>x\<in>A. P(x)) | Q)"
- "(\<forall>x\<in>A. P(x) \<longrightarrow> Q) <-> ((\<exists>x\<in>A. P(x)) \<longrightarrow> Q)"
- "(~(\<forall>x\<in>A. P(x))) <-> (\<exists>x\<in>A. ~P(x))"
- "(\<forall>x\<in>0.P(x)) <-> True"
- "(\<forall>x\<in>succ(i).P(x)) <-> P(i) & (\<forall>x\<in>i. P(x))"
- "(\<forall>x\<in>cons(a,B).P(x)) <-> P(a) & (\<forall>x\<in>B. P(x))"
- "(\<forall>x\<in>RepFun(A,f). P(x)) <-> (\<forall>y\<in>A. P(f(y)))"
- "(\<forall>x\<in>\<Union>(A).P(x)) <-> (\<forall>y\<in>A. \<forall>x\<in>y. P(x))"
+ "(\<forall>x\<in>A. P(x) & Q) \<longleftrightarrow> (\<forall>x\<in>A. P(x)) & (A=0 | Q)"
+ "(\<forall>x\<in>A. P(x) | Q) \<longleftrightarrow> ((\<forall>x\<in>A. P(x)) | Q)"
+ "(\<forall>x\<in>A. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P(x)) \<longrightarrow> Q)"
+ "(~(\<forall>x\<in>A. P(x))) \<longleftrightarrow> (\<exists>x\<in>A. ~P(x))"
+ "(\<forall>x\<in>0.P(x)) \<longleftrightarrow> True"
+ "(\<forall>x\<in>succ(i).P(x)) \<longleftrightarrow> P(i) & (\<forall>x\<in>i. P(x))"
+ "(\<forall>x\<in>cons(a,B).P(x)) \<longleftrightarrow> P(a) & (\<forall>x\<in>B. P(x))"
+ "(\<forall>x\<in>RepFun(A,f). P(x)) \<longleftrightarrow> (\<forall>y\<in>A. P(f(y)))"
+ "(\<forall>x\<in>\<Union>(A).P(x)) \<longleftrightarrow> (\<forall>y\<in>A. \<forall>x\<in>y. P(x))"
by blast+
lemma ball_simps2:
- "(\<forall>x\<in>A. P & Q(x)) <-> (A=0 | P) & (\<forall>x\<in>A. Q(x))"
- "(\<forall>x\<in>A. P | Q(x)) <-> (P | (\<forall>x\<in>A. Q(x)))"
- "(\<forall>x\<in>A. P \<longrightarrow> Q(x)) <-> (P \<longrightarrow> (\<forall>x\<in>A. Q(x)))"
+ "(\<forall>x\<in>A. P & Q(x)) \<longleftrightarrow> (A=0 | P) & (\<forall>x\<in>A. Q(x))"
+ "(\<forall>x\<in>A. P | Q(x)) \<longleftrightarrow> (P | (\<forall>x\<in>A. Q(x)))"
+ "(\<forall>x\<in>A. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x\<in>A. Q(x)))"
by blast+
lemma ball_simps3:
- "(\<forall>x\<in>Collect(A,Q).P(x)) <-> (\<forall>x\<in>A. Q(x) \<longrightarrow> P(x))"
+ "(\<forall>x\<in>Collect(A,Q).P(x)) \<longleftrightarrow> (\<forall>x\<in>A. Q(x) \<longrightarrow> P(x))"
by blast+
lemmas ball_simps [simp] = ball_simps1 ball_simps2 ball_simps3
lemma ball_conj_distrib:
- "(\<forall>x\<in>A. P(x) & Q(x)) <-> ((\<forall>x\<in>A. P(x)) & (\<forall>x\<in>A. Q(x)))"
+ "(\<forall>x\<in>A. P(x) & Q(x)) \<longleftrightarrow> ((\<forall>x\<in>A. P(x)) & (\<forall>x\<in>A. Q(x)))"
by blast
subsection{*Miniscoping of the Bounded Existential Quantifier*}
lemma bex_simps1:
- "(\<exists>x\<in>A. P(x) & Q) <-> ((\<exists>x\<in>A. P(x)) & Q)"
- "(\<exists>x\<in>A. P(x) | Q) <-> (\<exists>x\<in>A. P(x)) | (A\<noteq>0 & Q)"
- "(\<exists>x\<in>A. P(x) \<longrightarrow> Q) <-> ((\<forall>x\<in>A. P(x)) \<longrightarrow> (A\<noteq>0 & Q))"
- "(\<exists>x\<in>0.P(x)) <-> False"
- "(\<exists>x\<in>succ(i).P(x)) <-> P(i) | (\<exists>x\<in>i. P(x))"
- "(\<exists>x\<in>cons(a,B).P(x)) <-> P(a) | (\<exists>x\<in>B. P(x))"
- "(\<exists>x\<in>RepFun(A,f). P(x)) <-> (\<exists>y\<in>A. P(f(y)))"
- "(\<exists>x\<in>\<Union>(A).P(x)) <-> (\<exists>y\<in>A. \<exists>x\<in>y. P(x))"
- "(~(\<exists>x\<in>A. P(x))) <-> (\<forall>x\<in>A. ~P(x))"
+ "(\<exists>x\<in>A. P(x) & Q) \<longleftrightarrow> ((\<exists>x\<in>A. P(x)) & Q)"
+ "(\<exists>x\<in>A. P(x) | Q) \<longleftrightarrow> (\<exists>x\<in>A. P(x)) | (A\<noteq>0 & Q)"
+ "(\<exists>x\<in>A. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<forall>x\<in>A. P(x)) \<longrightarrow> (A\<noteq>0 & Q))"
+ "(\<exists>x\<in>0.P(x)) \<longleftrightarrow> False"
+ "(\<exists>x\<in>succ(i).P(x)) \<longleftrightarrow> P(i) | (\<exists>x\<in>i. P(x))"
+ "(\<exists>x\<in>cons(a,B).P(x)) \<longleftrightarrow> P(a) | (\<exists>x\<in>B. P(x))"
+ "(\<exists>x\<in>RepFun(A,f). P(x)) \<longleftrightarrow> (\<exists>y\<in>A. P(f(y)))"
+ "(\<exists>x\<in>\<Union>(A).P(x)) \<longleftrightarrow> (\<exists>y\<in>A. \<exists>x\<in>y. P(x))"
+ "(~(\<exists>x\<in>A. P(x))) \<longleftrightarrow> (\<forall>x\<in>A. ~P(x))"
by blast+
lemma bex_simps2:
- "(\<exists>x\<in>A. P & Q(x)) <-> (P & (\<exists>x\<in>A. Q(x)))"
- "(\<exists>x\<in>A. P | Q(x)) <-> (A\<noteq>0 & P) | (\<exists>x\<in>A. Q(x))"
- "(\<exists>x\<in>A. P \<longrightarrow> Q(x)) <-> ((A=0 | P) \<longrightarrow> (\<exists>x\<in>A. Q(x)))"
+ "(\<exists>x\<in>A. P & Q(x)) \<longleftrightarrow> (P & (\<exists>x\<in>A. Q(x)))"
+ "(\<exists>x\<in>A. P | Q(x)) \<longleftrightarrow> (A\<noteq>0 & P) | (\<exists>x\<in>A. Q(x))"
+ "(\<exists>x\<in>A. P \<longrightarrow> Q(x)) \<longleftrightarrow> ((A=0 | P) \<longrightarrow> (\<exists>x\<in>A. Q(x)))"
by blast+
lemma bex_simps3:
- "(\<exists>x\<in>Collect(A,Q).P(x)) <-> (\<exists>x\<in>A. Q(x) & P(x))"
+ "(\<exists>x\<in>Collect(A,Q).P(x)) \<longleftrightarrow> (\<exists>x\<in>A. Q(x) & P(x))"
by blast
lemmas bex_simps [simp] = bex_simps1 bex_simps2 bex_simps3
lemma bex_disj_distrib:
- "(\<exists>x\<in>A. P(x) | Q(x)) <-> ((\<exists>x\<in>A. P(x)) | (\<exists>x\<in>A. Q(x)))"
+ "(\<exists>x\<in>A. P(x) | Q(x)) \<longleftrightarrow> ((\<exists>x\<in>A. P(x)) | (\<exists>x\<in>A. Q(x)))"
by blast
(** One-point rule for bounded quantifiers: see HOL/Set.ML **)
-lemma bex_triv_one_point1 [simp]: "(\<exists>x\<in>A. x=a) <-> (a:A)"
+lemma bex_triv_one_point1 [simp]: "(\<exists>x\<in>A. x=a) \<longleftrightarrow> (a:A)"
by blast
-lemma bex_triv_one_point2 [simp]: "(\<exists>x\<in>A. a=x) <-> (a:A)"
+lemma bex_triv_one_point2 [simp]: "(\<exists>x\<in>A. a=x) \<longleftrightarrow> (a:A)"
by blast
-lemma bex_one_point1 [simp]: "(\<exists>x\<in>A. x=a & P(x)) <-> (a:A & P(a))"
+lemma bex_one_point1 [simp]: "(\<exists>x\<in>A. x=a & P(x)) \<longleftrightarrow> (a:A & P(a))"
by blast
-lemma bex_one_point2 [simp]: "(\<exists>x\<in>A. a=x & P(x)) <-> (a:A & P(a))"
+lemma bex_one_point2 [simp]: "(\<exists>x\<in>A. a=x & P(x)) \<longleftrightarrow> (a:A & P(a))"
by blast
-lemma ball_one_point1 [simp]: "(\<forall>x\<in>A. x=a \<longrightarrow> P(x)) <-> (a:A \<longrightarrow> P(a))"
+lemma ball_one_point1 [simp]: "(\<forall>x\<in>A. x=a \<longrightarrow> P(x)) \<longleftrightarrow> (a:A \<longrightarrow> P(a))"
by blast
-lemma ball_one_point2 [simp]: "(\<forall>x\<in>A. a=x \<longrightarrow> P(x)) <-> (a:A \<longrightarrow> P(a))"
+lemma ball_one_point2 [simp]: "(\<forall>x\<in>A. a=x \<longrightarrow> P(x)) \<longleftrightarrow> (a:A \<longrightarrow> P(a))"
by blast