--- 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