--- a/src/ZF/AC/AC15_WO6.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/AC15_WO6.thy Tue Mar 06 16:46:27 2012 +0000
@@ -42,11 +42,11 @@
"0\<notin>A ==> \<forall>B \<in> {cons(0,x*nat). x \<in> A}. ~Finite(B)"
apply clarify
apply (rule nat_not_Finite [THEN notE] )
-apply (subgoal_tac "x ~= 0")
+apply (subgoal_tac "x \<noteq> 0")
apply (blast intro: lepoll_Sigma [THEN lepoll_Finite])+
done
-lemma lemma1: "[| Union(C)=A; a \<in> A |] ==> \<exists>B \<in> C. a \<in> B & B \<subseteq> A"
+lemma lemma1: "[| \<Union>(C)=A; a \<in> A |] ==> \<exists>B \<in> C. a \<in> B & B \<subseteq> A"
by fast
lemma lemma2:
@@ -55,7 +55,7 @@
lemma lemma3:
"\<forall>B \<in> {cons(0, x*nat). x \<in> A}. pairwise_disjoint(f`B) &
- sets_of_size_between(f`B, 2, n) & Union(f`B)=B
+ sets_of_size_between(f`B, 2, n) & \<Union>(f`B)=B
==> \<forall>B \<in> A. \<exists>! u. u \<in> f`cons(0, B*nat) & u \<subseteq> cons(0, B*nat) &
0 \<in> u & 2 \<lesssim> u & u \<lesssim> n"
apply (unfold sets_of_size_between_def)
@@ -104,7 +104,7 @@
lemma ex_fun_AC13_AC15:
"[| \<forall>B \<in> {cons(0, x*nat). x \<in> A}.
pairwise_disjoint(f`B) &
- sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B;
+ sets_of_size_between(f`B, 2, succ(n)) & \<Union>(f`B)=B;
n \<in> nat |]
==> \<exists>f. \<forall>B \<in> A. f`B \<noteq> 0 & f`B \<subseteq> B & f`B \<lesssim> n"
by (fast del: subsetI notI
--- a/src/ZF/AC/AC16_WO4.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/AC16_WO4.thy Tue Mar 06 16:46:27 2012 +0000
@@ -47,8 +47,8 @@
lemmas lepoll_paired = paired_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll];
-lemma lemma2: "\<exists>y R. well_ord(y,R) & x Int y = 0 & ~y \<lesssim> z & ~Finite(y)"
-apply (rule_tac x = "{{a,x}. a \<in> nat Un Hartog (z) }" in exI)
+lemma lemma2: "\<exists>y R. well_ord(y,R) & x \<inter> y = 0 & ~y \<lesssim> z & ~Finite(y)"
+apply (rule_tac x = "{{a,x}. a \<in> nat \<union> Hartog (z) }" in exI)
apply (rule well_ord_Un [OF Ord_nat [THEN well_ord_Memrel]
Ord_Hartog [THEN well_ord_Memrel], THEN exE])
apply (blast intro!: Ord_Hartog well_ord_Memrel well_ord_paired
@@ -60,11 +60,11 @@
lepoll_paired [THEN lepoll_Finite])
done
-lemma infinite_Un: "~Finite(B) ==> ~Finite(A Un B)"
+lemma infinite_Un: "~Finite(B) ==> ~Finite(A \<union> B)"
by (blast intro: subset_Finite)
(* ********************************************************************** *)
-(* There is a v \<in> s(u) such that k \<lesssim> x Int y (in our case succ(k)) *)
+(* There is a v \<in> s(u) such that k \<lesssim> x \<inter> y (in our case succ(k)) *)
(* The idea of the proof is the following \<in> *)
(* Suppose not, i.e. every element of s(u) has exactly k-1 elements of y *)
(* Thence y is less than or equipollent to {v \<in> Pow(x). v \<approx> n#-k} *)
@@ -100,11 +100,11 @@
ordermap_bij [THEN exI [THEN eqpoll_def [THEN def_imp_iff, THEN iffD2]]]
lemma cons_cons_subset:
- "[| a \<subseteq> y; b \<in> y-a; u \<in> x |] ==> cons(b, cons(u, a)) \<in> Pow(x Un y)"
+ "[| a \<subseteq> y; b \<in> y-a; u \<in> x |] ==> cons(b, cons(u, a)) \<in> Pow(x \<union> y)"
by fast
lemma cons_cons_eqpoll:
- "[| a \<approx> k; a \<subseteq> y; b \<in> y-a; u \<in> x; x Int y = 0 |]
+ "[| a \<approx> k; a \<subseteq> y; b \<in> y-a; u \<in> x; x \<inter> y = 0 |]
==> cons(b, cons(u, a)) \<approx> succ(succ(k))"
by (fast intro!: cons_eqpoll_succ)
@@ -124,7 +124,7 @@
lemma cons_eqE: "[| cons(x,a) = cons(y,a); x \<notin> a |] ==> x = y "
by (fast elim!: equalityE)
-lemma eq_imp_Int_eq: "A = B ==> A Int C = B Int C"
+lemma eq_imp_Int_eq: "A = B ==> A \<inter> C = B \<inter> C"
by blast
(* ********************************************************************** *)
@@ -133,7 +133,7 @@
lemma eqpoll_sum_imp_Diff_lepoll_lemma [rule_format]:
"[| k \<in> nat; m \<in> nat |]
- ==> \<forall>A B. A \<approx> k #+ m & k \<lesssim> B & B \<subseteq> A --> A-B \<lesssim> m"
+ ==> \<forall>A B. A \<approx> k #+ m & k \<lesssim> B & B \<subseteq> A \<longrightarrow> A-B \<lesssim> m"
apply (induct_tac "k")
apply (simp add: add_0)
apply (blast intro: eqpoll_imp_lepoll lepoll_trans
@@ -162,7 +162,7 @@
lemma eqpoll_sum_imp_Diff_eqpoll_lemma [rule_format]:
"[| k \<in> nat; m \<in> nat |]
- ==> \<forall>A B. A \<approx> k #+ m & k \<approx> B & B \<subseteq> A --> A-B \<approx> m"
+ ==> \<forall>A B. A \<approx> k #+ m & k \<approx> B & B \<subseteq> A \<longrightarrow> A-B \<approx> m"
apply (induct_tac "k")
apply (force dest!: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_0_is_0])
apply (intro allI impI)
@@ -193,27 +193,27 @@
lemma subsets_lepoll_succ:
"n \<in> nat ==> {z \<in> Pow(y). z \<lesssim> succ(n)} =
- {z \<in> Pow(y). z \<lesssim> n} Un {z \<in> Pow(y). z \<approx> succ(n)}"
+ {z \<in> Pow(y). z \<lesssim> n} \<union> {z \<in> Pow(y). z \<approx> succ(n)}"
by (blast intro: leI le_imp_lepoll nat_into_Ord
lepoll_trans eqpoll_imp_lepoll
dest!: lepoll_succ_disj)
lemma Int_empty:
- "n \<in> nat ==> {z \<in> Pow(y). z \<lesssim> n} Int {z \<in> Pow(y). z \<approx> succ(n)} = 0"
+ "n \<in> nat ==> {z \<in> Pow(y). z \<lesssim> n} \<inter> {z \<in> Pow(y). z \<approx> succ(n)} = 0"
by (blast intro: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans]
succ_lepoll_natE)
locale AC16 =
fixes x and y and k and l and m and t_n and R and MM and LL and GG and s
defines k_def: "k == succ(l)"
- and MM_def: "MM == {v \<in> t_n. succ(k) \<lesssim> v Int y}"
- and LL_def: "LL == {v Int y. v \<in> MM}"
+ and MM_def: "MM == {v \<in> t_n. succ(k) \<lesssim> v \<inter> y}"
+ and LL_def: "LL == {v \<inter> y. v \<in> MM}"
and GG_def: "GG == \<lambda>v \<in> LL. (THE w. w \<in> MM & v \<subseteq> w) - v"
- and s_def: "s(u) == {v \<in> t_n. u \<in> v & k \<lesssim> v Int y}"
- assumes all_ex: "\<forall>z \<in> {z \<in> Pow(x Un y) . z \<approx> succ(k)}.
+ and s_def: "s(u) == {v \<in> t_n. u \<in> v & k \<lesssim> v \<inter> y}"
+ assumes all_ex: "\<forall>z \<in> {z \<in> Pow(x \<union> y) . z \<approx> succ(k)}.
\<exists>! w. w \<in> t_n & z \<subseteq> w "
- and disjoint[iff]: "x Int y = 0"
- and "includes": "t_n \<subseteq> {v \<in> Pow(x Un y). v \<approx> succ(k #+ m)}"
+ and disjoint[iff]: "x \<inter> y = 0"
+ and "includes": "t_n \<subseteq> {v \<in> Pow(x \<union> y). v \<approx> succ(k #+ m)}"
and WO_R[iff]: "well_ord(y,R)"
and lnat[iff]: "l \<in> nat"
and mnat[iff]: "m \<in> nat"
@@ -274,16 +274,16 @@
done
lemma (in AC16) the_eq_cons:
- "[| \<forall>v \<in> s(u). succ(l) \<approx> v Int y;
+ "[| \<forall>v \<in> s(u). succ(l) \<approx> v \<inter> y;
l \<approx> a; a \<subseteq> y; b \<in> y - a; u \<in> x |]
- ==> (THE c. c \<in> s(u) & a \<subseteq> c & b \<in> c) Int y = cons(b, a)"
+ ==> (THE c. c \<in> s(u) & a \<subseteq> c & b \<in> c) \<inter> y = cons(b, a)"
apply (frule ex1_superset_a [THEN theI], assumption+)
apply (rule set_eq_cons)
apply (fast+)
done
lemma (in AC16) y_lepoll_subset_s:
- "[| \<forall>v \<in> s(u). succ(l) \<approx> v Int y;
+ "[| \<forall>v \<in> s(u). succ(l) \<approx> v \<inter> y;
l \<approx> a; a \<subseteq> y; u \<in> x |]
==> y \<lesssim> {v \<in> s(u). a \<subseteq> v}"
apply (rule Diff_Finite_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll,
@@ -310,14 +310,14 @@
by (blast dest: disjoint [THEN equalityD1, THEN subsetD, OF IntI])
lemma (in AC16) w_Int_eq_w_Diff:
- "w \<subseteq> x Un y ==> w Int (x - {u}) = w - cons(u, w Int y)"
+ "w \<subseteq> x \<union> y ==> w \<inter> (x - {u}) = w - cons(u, w \<inter> y)"
by blast
lemma (in AC16) w_Int_eqpoll_m:
"[| w \<in> {v \<in> s(u). a \<subseteq> v};
l \<approx> a; u \<in> x;
- \<forall>v \<in> s(u). succ(l) \<approx> v Int y |]
- ==> w Int (x - {u}) \<approx> m"
+ \<forall>v \<in> s(u). succ(l) \<approx> v \<inter> y |]
+ ==> w \<inter> (x - {u}) \<approx> m"
apply (erule CollectE)
apply (subst w_Int_eq_w_Diff)
apply (fast dest!: s_subset [THEN subsetD]
@@ -341,7 +341,7 @@
done
lemma (in AC16) cons_cons_in:
- "[| z \<in> xa Int (x - {u}); l \<approx> a; a \<subseteq> y; u \<in> x |]
+ "[| z \<in> xa \<inter> (x - {u}); l \<approx> a; a \<subseteq> y; u \<in> x |]
==> \<exists>! w. w \<in> t_n & cons(z, cons(u, a)) \<subseteq> w"
apply (rule all_ex [THEN bspec])
apply (unfold k_def)
@@ -349,9 +349,9 @@
done
lemma (in AC16) subset_s_lepoll_w:
- "[| \<forall>v \<in> s(u). succ(l) \<approx> v Int y; a \<subseteq> y; l \<approx> a; u \<in> x |]
+ "[| \<forall>v \<in> s(u). succ(l) \<approx> v \<inter> y; a \<subseteq> y; l \<approx> a; u \<in> x |]
==> {v \<in> s(u). a \<subseteq> v} \<lesssim> {v \<in> Pow(x). v \<approx> m}"
-apply (rule_tac f3 = "\<lambda>w \<in> {v \<in> s (u) . a \<subseteq> v}. w Int (x - {u})"
+apply (rule_tac f3 = "\<lambda>w \<in> {v \<in> s (u) . a \<subseteq> v}. w \<inter> (x - {u})"
in exI [THEN lepoll_def [THEN def_imp_iff, THEN iffD2]])
apply (simp add: inj_def)
apply (intro conjI lam_type CollectI)
@@ -425,11 +425,11 @@
(* The union of appropriate values is the whole x *)
(* ********************************************************************** *)
-lemma (in AC16) Int_in_LL: "w \<in> MM ==> w Int y \<in> LL"
+lemma (in AC16) Int_in_LL: "w \<in> MM ==> w \<inter> y \<in> LL"
by (unfold LL_def, fast)
lemma (in AC16) in_LL_eq_Int:
- "v \<in> LL ==> v = (THE x. x \<in> MM & v \<subseteq> x) Int y"
+ "v \<in> LL ==> v = (THE x. x \<in> MM & v \<subseteq> x) \<inter> y"
apply (unfold LL_def, clarify)
apply (subst unique_superset_in_MM [THEN the_equality2])
apply (auto simp add: Int_in_LL)
@@ -439,7 +439,7 @@
by (erule unique_superset_in_MM [THEN theI, THEN conjunct1])
lemma (in AC16) the_in_MM_subset:
- "v \<in> LL ==> (THE x. x \<in> MM & v \<subseteq> x) \<subseteq> x Un y"
+ "v \<in> LL ==> (THE x. x \<in> MM & v \<subseteq> x) \<subseteq> x \<union> y"
apply (drule unique_superset1)
apply (unfold MM_def)
apply (fast dest!: unique_superset1 "includes" [THEN subsetD])
@@ -468,9 +468,9 @@
done
-lemma (in AC16) exists_proper_in_s: "u \<in> x ==> \<exists>v \<in> s(u). succ(k) \<lesssim> v Int y"
+lemma (in AC16) exists_proper_in_s: "u \<in> x ==> \<exists>v \<in> s(u). succ(k) \<lesssim> v \<inter> y"
apply (rule ccontr)
-apply (subgoal_tac "\<forall>v \<in> s (u) . k \<approx> v Int y")
+apply (subgoal_tac "\<forall>v \<in> s (u) . k \<approx> v \<inter> y")
prefer 2 apply (simp add: s_def, blast intro: succ_not_lepoll_imp_eqpoll)
apply (unfold k_def)
apply (insert all_ex "includes" lnat)
@@ -568,7 +568,7 @@
apply (rule lemma1, assumption+)
apply (cut_tac lemma2)
apply (elim exE conjE)
-apply (erule_tac x = "A Un y" in allE)
+apply (erule_tac x = "A \<union> y" in allE)
apply (frule infinite_Un, drule mp, assumption)
apply (erule zero_lt_natE, assumption, clarify)
apply (blast intro: AC16.conclusion [OF AC16.intro])
--- a/src/ZF/AC/AC16_lemmas.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/AC16_lemmas.thy Tue Mar 06 16:46:27 2012 +0000
@@ -11,7 +11,7 @@
lemma cons_Diff_eq: "a\<notin>A ==> cons(a,A)-{a}=A"
by fast
-lemma nat_1_lepoll_iff: "1\<lesssim>X <-> (\<exists>x. x \<in> X)"
+lemma nat_1_lepoll_iff: "1\<lesssim>X \<longleftrightarrow> (\<exists>x. x \<in> X)"
apply (unfold lepoll_def)
apply (rule iffI)
apply (fast intro: inj_is_fun [THEN apply_type])
@@ -20,7 +20,7 @@
apply (fast intro!: lam_injective)
done
-lemma eqpoll_1_iff_singleton: "X\<approx>1 <-> (\<exists>x. X={x})"
+lemma eqpoll_1_iff_singleton: "X\<approx>1 \<longleftrightarrow> (\<exists>x. X={x})"
apply (rule iffI)
apply (erule eqpollE)
apply (drule nat_1_lepoll_iff [THEN iffD1])
@@ -79,7 +79,7 @@
apply (simp, blast intro: InfCard_Least_in)
done
-lemma set_of_Ord_succ_Union: "(\<forall>y \<in> z. Ord(y)) ==> z \<subseteq> succ(Union(z))"
+lemma set_of_Ord_succ_Union: "(\<forall>y \<in> z. Ord(y)) ==> z \<subseteq> succ(\<Union>(z))"
apply (rule subsetI)
apply (case_tac "\<forall>y \<in> z. y \<subseteq> x", blast )
apply (simp, erule bexE)
@@ -91,22 +91,22 @@
by (fast elim!: mem_irrefl)
lemma succ_Union_not_mem:
- "(!!y. y \<in> z ==> Ord(y)) ==> succ(Union(z)) \<notin> z"
+ "(!!y. y \<in> z ==> Ord(y)) ==> succ(\<Union>(z)) \<notin> z"
apply (rule set_of_Ord_succ_Union [THEN subset_not_mem], blast)
done
lemma Union_cons_eq_succ_Union:
- "Union(cons(succ(Union(z)),z)) = succ(Union(z))"
+ "\<Union>(cons(succ(\<Union>(z)),z)) = succ(\<Union>(z))"
by fast
-lemma Un_Ord_disj: "[| Ord(i); Ord(j) |] ==> i Un j = i | i Un j = j"
+lemma Un_Ord_disj: "[| Ord(i); Ord(j) |] ==> i \<union> j = i | i \<union> j = j"
by (fast dest!: le_imp_subset elim: Ord_linear_le)
-lemma Union_eq_Un: "x \<in> X ==> Union(X) = x Un Union(X-{x})"
+lemma Union_eq_Un: "x \<in> X ==> \<Union>(X) = x \<union> \<Union>(X-{x})"
by fast
lemma Union_in_lemma [rule_format]:
- "n \<in> nat ==> \<forall>z. (\<forall>y \<in> z. Ord(y)) & z\<approx>n & z\<noteq>0 --> Union(z) \<in> z"
+ "n \<in> nat ==> \<forall>z. (\<forall>y \<in> z. Ord(y)) & z\<approx>n & z\<noteq>0 \<longrightarrow> \<Union>(z) \<in> z"
apply (induct_tac "n")
apply (fast dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0])
apply (intro allI impI)
@@ -126,11 +126,11 @@
apply (drule Un_Ord_disj, assumption, auto)
done
-lemma Union_in: "[| \<forall>x \<in> z. Ord(x); z\<approx>n; z\<noteq>0; n \<in> nat |] ==> Union(z) \<in> z"
+lemma Union_in: "[| \<forall>x \<in> z. Ord(x); z\<approx>n; z\<noteq>0; n \<in> nat |] ==> \<Union>(z) \<in> z"
by (blast intro: Union_in_lemma)
lemma succ_Union_in_x:
- "[| InfCard(x); z \<in> Pow(x); z\<approx>n; n \<in> nat |] ==> succ(Union(z)) \<in> x"
+ "[| InfCard(x); z \<in> Pow(x); z\<approx>n; n \<in> nat |] ==> succ(\<Union>(z)) \<in> x"
apply (rule Limit_has_succ [THEN ltE])
prefer 3 apply assumption
apply (erule InfCard_is_Limit)
@@ -145,9 +145,9 @@
"[| InfCard(x); n \<in> nat |]
==> {y \<in> Pow(x). y\<approx>succ(n)} \<lesssim> {y \<in> Pow(x). y\<approx>succ(succ(n))}"
apply (unfold lepoll_def)
-apply (rule_tac x = "\<lambda>z \<in> {y\<in>Pow(x). y\<approx>succ(n)}. cons(succ(Union(z)), z)"
+apply (rule_tac x = "\<lambda>z \<in> {y\<in>Pow(x). y\<approx>succ(n)}. cons(succ(\<Union>(z)), z)"
in exI)
-apply (rule_tac d = "%z. z-{Union (z) }" in lam_injective)
+apply (rule_tac d = "%z. z-{\<Union>(z) }" in lam_injective)
apply (blast intro!: succ_Union_in_x succ_Union_not_mem
intro: cons_eqpoll_succ Ord_in_Ord
dest!: InfCard_is_Card [THEN Card_is_Ord])
--- a/src/ZF/AC/AC17_AC1.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/AC17_AC1.thy Tue Mar 06 16:46:27 2012 +0000
@@ -75,7 +75,7 @@
apply (erule swap)
apply (rule allI)
apply (erule swap)
-apply (rule_tac x = "Union (A)" in exI)
+apply (rule_tac x = "\<Union>(A)" in exI)
apply (blast intro: lam_type)
done
@@ -136,7 +136,7 @@
AC1 ==> AC2 ==> AC1
AC1 ==> AC4 ==> AC3 ==> AC1
AC4 ==> AC5 ==> AC4
- AC1 <-> AC6
+ AC1 \<longleftrightarrow> AC6
************************************************************************* *)
(* ********************************************************************** *)
@@ -144,7 +144,7 @@
(* ********************************************************************** *)
lemma AC1_AC2_aux1:
- "[| f:(\<Pi> X \<in> A. X); B \<in> A; 0\<notin>A |] ==> {f`B} \<subseteq> B Int {f`C. C \<in> A}"
+ "[| f:(\<Pi> X \<in> A. X); B \<in> A; 0\<notin>A |] ==> {f`B} \<subseteq> B \<inter> {f`C. C \<in> A}"
by (fast elim!: apply_type)
lemma AC1_AC2_aux2:
@@ -169,16 +169,16 @@
lemma AC2_AC1_aux1: "0\<notin>A ==> 0 \<notin> {B*{B}. B \<in> A}"
by (fast dest!: sym [THEN Sigma_empty_iff [THEN iffD1]])
-lemma AC2_AC1_aux2: "[| X*{X} Int C = {y}; X \<in> A |]
- ==> (THE y. X*{X} Int C = {y}): X*A"
+lemma AC2_AC1_aux2: "[| X*{X} \<inter> C = {y}; X \<in> A |]
+ ==> (THE y. X*{X} \<inter> C = {y}): X*A"
apply (rule subst_elem [of y])
apply (blast elim!: equalityE)
apply (auto simp add: singleton_eq_iff)
done
lemma AC2_AC1_aux3:
- "\<forall>D \<in> {E*{E}. E \<in> A}. \<exists>y. D Int C = {y}
- ==> (\<lambda>x \<in> A. fst(THE z. (x*{x} Int C = {z}))) \<in> (\<Pi> X \<in> A. X)"
+ "\<forall>D \<in> {E*{E}. E \<in> A}. \<exists>y. D \<inter> C = {y}
+ ==> (\<lambda>x \<in> A. fst(THE z. (x*{x} \<inter> C = {z}))) \<in> (\<Pi> X \<in> A. X)"
apply (rule lam_type)
apply (drule bspec, blast)
apply (blast intro: AC2_AC1_aux2 fst_type)
@@ -212,7 +212,7 @@
(* AC4 ==> AC3 *)
(* ********************************************************************** *)
-lemma AC4_AC3_aux1: "f \<in> A->B ==> (\<Union>z \<in> A. {z}*f`z) \<subseteq> A*Union(B)"
+lemma AC4_AC3_aux1: "f \<in> A->B ==> (\<Union>z \<in> A. {z}*f`z) \<subseteq> A*\<Union>(B)"
by (fast dest!: apply_type)
lemma AC4_AC3_aux2: "domain(\<Union>z \<in> A. {z}*f(z)) = {a \<in> A. f(a)\<noteq>0}"
@@ -292,10 +292,10 @@
(* ********************************************************************** *)
-(* AC1 <-> AC6 *)
+(* AC1 \<longleftrightarrow> AC6 *)
(* ********************************************************************** *)
-lemma AC1_iff_AC6: "AC1 <-> AC6"
+lemma AC1_iff_AC6: "AC1 \<longleftrightarrow> AC6"
by (unfold AC1_def AC6_def, blast)
end
--- a/src/ZF/AC/AC18_AC19.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/AC18_AC19.thy Tue Mar 06 16:46:27 2012 +0000
@@ -10,7 +10,7 @@
definition
uu :: "i => i" where
- "uu(a) == {c Un {0}. c \<in> a}"
+ "uu(a) == {c \<union> {0}. c \<in> a}"
(* ********************************************************************** *)
@@ -23,7 +23,7 @@
by (rule lam_type, drule apply_type, auto)
lemma lemma_AC18:
- "[| \<forall>A. 0 \<notin> A --> (\<exists>f. f \<in> (\<Pi> X \<in> A. X)); A \<noteq> 0 |]
+ "[| \<forall>A. 0 \<notin> A \<longrightarrow> (\<exists>f. f \<in> (\<Pi> X \<in> A. X)); A \<noteq> 0 |]
==> (\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a, b)) \<subseteq>
(\<Union>f \<in> \<Pi> a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a))"
apply (rule subsetI)
@@ -61,7 +61,7 @@
apply (blast dest!: sym [THEN RepFun_eq_0_iff [THEN iffD1]])
done
-lemma lemma1_1: "[|c \<in> a; x = c Un {0}; x \<notin> a |] ==> x - {0} \<in> a"
+lemma lemma1_1: "[|c \<in> a; x = c \<union> {0}; x \<notin> a |] ==> x - {0} \<in> a"
apply clarify
apply (rule subst_elem, assumption)
apply (fast elim: notE subst_elem)
--- a/src/ZF/AC/AC7_AC9.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/AC7_AC9.thy Tue Mar 06 16:46:27 2012 +0000
@@ -15,13 +15,13 @@
(* - Sigma_fun_space_eqpoll *)
(* ********************************************************************** *)
-lemma Sigma_fun_space_not0: "[| 0\<notin>A; B \<in> A |] ==> (nat->Union(A)) * B \<noteq> 0"
+lemma Sigma_fun_space_not0: "[| 0\<notin>A; B \<in> A |] ==> (nat->\<Union>(A)) * B \<noteq> 0"
by (blast dest!: Sigma_empty_iff [THEN iffD1] Union_empty_iff [THEN iffD1])
lemma inj_lemma:
- "C \<in> A ==> (\<lambda>g \<in> (nat->Union(A))*C.
+ "C \<in> A ==> (\<lambda>g \<in> (nat->\<Union>(A))*C.
(\<lambda>n \<in> nat. if(n=0, snd(g), fst(g)`(n #- 1))))
- \<in> inj((nat->Union(A))*C, (nat->Union(A)) ) "
+ \<in> inj((nat->\<Union>(A))*C, (nat->\<Union>(A)) ) "
apply (unfold inj_def)
apply (rule CollectI)
apply (fast intro!: lam_type if_type apply_type fst_type snd_type, auto)
@@ -31,7 +31,7 @@
done
lemma Sigma_fun_space_eqpoll:
- "[| C \<in> A; 0\<notin>A |] ==> (nat->Union(A)) * C \<approx> (nat->Union(A))"
+ "[| C \<in> A; 0\<notin>A |] ==> (nat->\<Union>(A)) * C \<approx> (nat->\<Union>(A))"
apply (rule eqpollI)
apply (simp add: lepoll_def)
apply (fast intro!: inj_lemma)
@@ -62,10 +62,10 @@
done
lemma AC7_AC6_lemma1:
- "(\<Pi> B \<in> {(nat->Union(A))*C. C \<in> A}. B) \<noteq> 0 ==> (\<Pi> B \<in> A. B) \<noteq> 0"
+ "(\<Pi> B \<in> {(nat->\<Union>(A))*C. C \<in> A}. B) \<noteq> 0 ==> (\<Pi> B \<in> A. B) \<noteq> 0"
by (fast intro!: equals0I lemma1_1 lemma1_2)
-lemma AC7_AC6_lemma2: "0 \<notin> A ==> 0 \<notin> {(nat -> Union(A)) * C. C \<in> A}"
+lemma AC7_AC6_lemma2: "0 \<notin> A ==> 0 \<notin> {(nat -> \<Union>(A)) * C. C \<in> A}"
by (blast dest: Sigma_fun_space_not0)
lemma AC7_AC6: "AC7 ==> AC6"
@@ -125,8 +125,8 @@
(* AC9 ==> AC1 *)
(* The idea of this proof comes from "Equivalents of the Axiom of Choice" *)
(* by Rubin & Rubin. But (x * y) is not necessarily equipollent to *)
-(* (x * y) Un {0} when y is a set of total functions acting from nat to *)
-(* Union(A) -- therefore we have used the set (y * nat) instead of y. *)
+(* (x * y) \<union> {0} when y is a set of total functions acting from nat to *)
+(* \<Union>(A) -- therefore we have used the set (y * nat) instead of y. *)
(* ********************************************************************** *)
lemma snd_lepoll_SigmaI: "b \<in> B \<Longrightarrow> X \<lesssim> B \<times> X"
@@ -134,13 +134,13 @@
prod_commute_eqpoll)
lemma nat_lepoll_lemma:
- "[|0 \<notin> A; B \<in> A|] ==> nat \<lesssim> ((nat \<rightarrow> Union(A)) \<times> B) \<times> nat"
+ "[|0 \<notin> A; B \<in> A|] ==> nat \<lesssim> ((nat \<rightarrow> \<Union>(A)) \<times> B) \<times> nat"
by (blast dest: Sigma_fun_space_not0 intro: snd_lepoll_SigmaI)
lemma AC9_AC1_lemma1:
"[| 0\<notin>A; A\<noteq>0;
- C = {((nat->Union(A))*B)*nat. B \<in> A} Un
- {cons(0,((nat->Union(A))*B)*nat). B \<in> A};
+ C = {((nat->\<Union>(A))*B)*nat. B \<in> A} \<union>
+ {cons(0,((nat->\<Union>(A))*B)*nat). B \<in> A};
B1 \<in> C; B2 \<in> C |]
==> B1 \<approx> B2"
by (blast intro!: nat_lepoll_lemma Sigma_fun_space_eqpoll
@@ -149,8 +149,8 @@
intro: eqpoll_trans eqpoll_sym )
lemma AC9_AC1_lemma2:
- "\<forall>B1 \<in> {(F*B)*N. B \<in> A} Un {cons(0,(F*B)*N). B \<in> A}.
- \<forall>B2 \<in> {(F*B)*N. B \<in> A} Un {cons(0,(F*B)*N). B \<in> A}.
+ "\<forall>B1 \<in> {(F*B)*N. B \<in> A} \<union> {cons(0,(F*B)*N). B \<in> A}.
+ \<forall>B2 \<in> {(F*B)*N. B \<in> A} \<union> {cons(0,(F*B)*N). B \<in> A}.
f`<B1,B2> \<in> bij(B1, B2)
==> (\<lambda>B \<in> A. snd(fst((f`<cons(0,(F*B)*N),(F*B)*N>)`0))) \<in> (\<Pi> X \<in> A. X)"
apply (intro lam_type snd_type fst_type)
@@ -162,7 +162,7 @@
apply (unfold AC1_def AC9_def)
apply (intro allI impI)
apply (erule allE)
-apply (case_tac "A~=0")
+apply (case_tac "A\<noteq>0")
apply (blast dest: AC9_AC1_lemma1 AC9_AC1_lemma2, force)
done
--- a/src/ZF/AC/AC_Equiv.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/AC_Equiv.thy Tue Mar 06 16:46:27 2012 +0000
@@ -38,16 +38,16 @@
& (\<Union>b<a. f`b) = A & (\<forall>b<a. f`b \<lesssim> m))"
definition
- "WO7 == \<forall>A. Finite(A) <-> (\<forall>R. well_ord(A,R) --> well_ord(A,converse(R)))"
+ "WO7 == \<forall>A. Finite(A) \<longleftrightarrow> (\<forall>R. well_ord(A,R) \<longrightarrow> well_ord(A,converse(R)))"
definition
- "WO8 == \<forall>A. (\<exists>f. f \<in> (\<Pi> X \<in> A. X)) --> (\<exists>R. well_ord(A,R))"
+ "WO8 == \<forall>A. (\<exists>f. f \<in> (\<Pi> X \<in> A. X)) \<longrightarrow> (\<exists>R. well_ord(A,R))"
definition
(* Auxiliary concepts needed below *)
pairwise_disjoint :: "i => o" where
- "pairwise_disjoint(A) == \<forall>A1 \<in> A. \<forall>A2 \<in> A. A1 Int A2 \<noteq> 0 --> A1=A2"
+ "pairwise_disjoint(A) == \<forall>A1 \<in> A. \<forall>A2 \<in> A. A1 \<inter> A2 \<noteq> 0 \<longrightarrow> A1=A2"
definition
sets_of_size_between :: "[i, i, i] => o" where
@@ -59,60 +59,60 @@
"AC0 == \<forall>A. \<exists>f. f \<in> (\<Pi> X \<in> Pow(A)-{0}. X)"
definition
- "AC1 == \<forall>A. 0\<notin>A --> (\<exists>f. f \<in> (\<Pi> X \<in> A. X))"
+ "AC1 == \<forall>A. 0\<notin>A \<longrightarrow> (\<exists>f. f \<in> (\<Pi> X \<in> A. X))"
definition
"AC2 == \<forall>A. 0\<notin>A & pairwise_disjoint(A)
- --> (\<exists>C. \<forall>B \<in> A. \<exists>y. B Int C = {y})"
+ \<longrightarrow> (\<exists>C. \<forall>B \<in> A. \<exists>y. B \<inter> C = {y})"
definition
"AC3 == \<forall>A B. \<forall>f \<in> A->B. \<exists>g. g \<in> (\<Pi> x \<in> {a \<in> A. f`a\<noteq>0}. f`x)"
definition
- "AC4 == \<forall>R A B. (R \<subseteq> A*B --> (\<exists>f. f \<in> (\<Pi> x \<in> domain(R). R``{x})))"
+ "AC4 == \<forall>R A B. (R \<subseteq> A*B \<longrightarrow> (\<exists>f. f \<in> (\<Pi> x \<in> domain(R). R``{x})))"
definition
"AC5 == \<forall>A B. \<forall>f \<in> A->B. \<exists>g \<in> range(f)->A. \<forall>x \<in> domain(g). f`(g`x) = x"
definition
- "AC6 == \<forall>A. 0\<notin>A --> (\<Pi> B \<in> A. B)\<noteq>0"
+ "AC6 == \<forall>A. 0\<notin>A \<longrightarrow> (\<Pi> B \<in> A. B)\<noteq>0"
definition
- "AC7 == \<forall>A. 0\<notin>A & (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) --> (\<Pi> B \<in> A. B) \<noteq> 0"
+ "AC7 == \<forall>A. 0\<notin>A & (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) \<longrightarrow> (\<Pi> B \<in> A. B) \<noteq> 0"
definition
"AC8 == \<forall>A. (\<forall>B \<in> A. \<exists>B1 B2. B=<B1,B2> & B1\<approx>B2)
- --> (\<exists>f. \<forall>B \<in> A. f`B \<in> bij(fst(B),snd(B)))"
+ \<longrightarrow> (\<exists>f. \<forall>B \<in> A. f`B \<in> bij(fst(B),snd(B)))"
definition
- "AC9 == \<forall>A. (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) -->
+ "AC9 == \<forall>A. (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) \<longrightarrow>
(\<exists>f. \<forall>B1 \<in> A. \<forall>B2 \<in> A. f`<B1,B2> \<in> bij(B1,B2))"
definition
- "AC10(n) == \<forall>A. (\<forall>B \<in> A. ~Finite(B)) -->
+ "AC10(n) == \<forall>A. (\<forall>B \<in> A. ~Finite(B)) \<longrightarrow>
(\<exists>f. \<forall>B \<in> A. (pairwise_disjoint(f`B) &
- sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B))"
+ sets_of_size_between(f`B, 2, succ(n)) & \<Union>(f`B)=B))"
definition
"AC11 == \<exists>n \<in> nat. 1\<le>n & AC10(n)"
definition
- "AC12 == \<forall>A. (\<forall>B \<in> A. ~Finite(B)) -->
+ "AC12 == \<forall>A. (\<forall>B \<in> A. ~Finite(B)) \<longrightarrow>
(\<exists>n \<in> nat. 1\<le>n & (\<exists>f. \<forall>B \<in> A. (pairwise_disjoint(f`B) &
- sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B)))"
+ sets_of_size_between(f`B, 2, succ(n)) & \<Union>(f`B)=B)))"
definition
- "AC13(m) == \<forall>A. 0\<notin>A --> (\<exists>f. \<forall>B \<in> A. f`B\<noteq>0 & f`B \<subseteq> B & f`B \<lesssim> m)"
+ "AC13(m) == \<forall>A. 0\<notin>A \<longrightarrow> (\<exists>f. \<forall>B \<in> A. f`B\<noteq>0 & f`B \<subseteq> B & f`B \<lesssim> m)"
definition
"AC14 == \<exists>m \<in> nat. 1\<le>m & AC13(m)"
definition
- "AC15 == \<forall>A. 0\<notin>A -->
+ "AC15 == \<forall>A. 0\<notin>A \<longrightarrow>
(\<exists>m \<in> nat. 1\<le>m & (\<exists>f. \<forall>B \<in> A. f`B\<noteq>0 & f`B \<subseteq> B & f`B \<lesssim> m))"
definition
"AC16(n, k) ==
- \<forall>A. ~Finite(A) -->
+ \<forall>A. ~Finite(A) \<longrightarrow>
(\<exists>T. T \<subseteq> {X \<in> Pow(A). X\<approx>succ(n)} &
(\<forall>X \<in> {X \<in> Pow(A). X\<approx>succ(k)}. \<exists>! Y. Y \<in> T & X \<subseteq> Y))"
@@ -121,13 +121,13 @@
\<exists>f \<in> Pow(A)-{0} -> A. f`(g`f) \<in> g`f"
locale AC18 =
- assumes AC18: "A\<noteq>0 & (\<forall>a \<in> A. B(a) \<noteq> 0) -->
+ assumes AC18: "A\<noteq>0 & (\<forall>a \<in> A. B(a) \<noteq> 0) \<longrightarrow>
((\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a,b)) =
(\<Union>f \<in> \<Pi> a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a)))"
--"AC18 cannot be expressed within the object-logic"
definition
- "AC19 == \<forall>A. A\<noteq>0 & 0\<notin>A --> ((\<Inter>a \<in> A. \<Union>b \<in> a. b) =
+ "AC19 == \<forall>A. A\<noteq>0 & 0\<notin>A \<longrightarrow> ((\<Inter>a \<in> A. \<Union>b \<in> a. b) =
(\<Union>f \<in> (\<Pi> B \<in> A. B). \<Inter>a \<in> A. f`a))"
@@ -137,7 +137,7 @@
(* ********************************************************************** *)
(* lemma for ordertype_Int *)
-lemma rvimage_id: "rvimage(A,id(A),r) = r Int A*A"
+lemma rvimage_id: "rvimage(A,id(A),r) = r \<inter> A*A"
apply (unfold rvimage_def)
apply (rule equalityI, safe)
apply (drule_tac P = "%a. <id (A) `xb,a>:r" in id_conv [THEN subst],
@@ -148,7 +148,7 @@
(* used only in Hartog.ML *)
lemma ordertype_Int:
- "well_ord(A,r) ==> ordertype(A, r Int A*A) = ordertype(A,r)"
+ "well_ord(A,r) ==> ordertype(A, r \<inter> A*A) = ordertype(A,r)"
apply (rule_tac P = "%a. ordertype (A,a) =ordertype (A,r) " in rvimage_id [THEN subst])
apply (erule id_bij [THEN bij_ordertype_vimage])
done
@@ -191,11 +191,11 @@
(* ********************************************************************** *)
lemma first_in_B:
- "[| well_ord(Union(A),r); 0\<notin>A; B \<in> A |] ==> (THE b. first(b,B,r)) \<in> B"
+ "[| well_ord(\<Union>(A),r); 0\<notin>A; B \<in> A |] ==> (THE b. first(b,B,r)) \<in> B"
by (blast dest!: well_ord_imp_ex1_first
[THEN theI, THEN first_def [THEN def_imp_iff, THEN iffD1]])
-lemma ex_choice_fun: "[| well_ord(Union(A), R); 0\<notin>A |] ==> \<exists>f. f:(\<Pi> X \<in> A. X)"
+lemma ex_choice_fun: "[| well_ord(\<Union>(A), R); 0\<notin>A |] ==> \<exists>f. f:(\<Pi> X \<in> A. X)"
by (fast elim!: first_in_B intro!: lam_type)
lemma ex_choice_fun_Pow: "well_ord(A, R) ==> \<exists>f. f:(\<Pi> X \<in> Pow(A)-{0}. X)"
--- a/src/ZF/AC/Cardinal_aux.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/Cardinal_aux.thy Tue Mar 06 16:46:27 2012 +0000
@@ -20,13 +20,13 @@
(* j=|A| *)
lemma lepoll_imp_ex_le_eqpoll:
- "[| A \<lesssim> i; Ord(i) |] ==> \<exists>j. j le i & A \<approx> j"
-by (blast intro!: lepoll_cardinal_le well_ord_Memrel
+ "[| A \<lesssim> i; Ord(i) |] ==> \<exists>j. j \<le> i & A \<approx> j"
+by (blast intro!: lepoll_cardinal_le well_ord_Memrel
well_ord_cardinal_eqpoll [THEN eqpoll_sym]
dest: lepoll_well_ord)
(* j=|A| *)
-lemma lesspoll_imp_ex_lt_eqpoll:
+lemma lesspoll_imp_ex_lt_eqpoll:
"[| A \<prec> i; Ord(i) |] ==> \<exists>j. j<i & A \<approx> j"
by (unfold lesspoll_def, blast dest!: lepoll_imp_ex_le_eqpoll elim!: leE)
@@ -34,41 +34,41 @@
apply (unfold InfCard_def)
apply (rule conjI)
apply (rule Card_cardinal)
-apply (rule Card_nat
+apply (rule Card_nat
[THEN Card_def [THEN def_imp_iff, THEN iffD1, THEN ssubst]])
-- "rewriting would loop!"
-apply (rule well_ord_Memrel [THEN well_ord_lepoll_imp_Card_le], assumption)
+apply (rule well_ord_Memrel [THEN well_ord_lepoll_imp_Card_le], assumption)
apply (rule nat_le_infinite_Ord [THEN le_imp_lepoll], assumption+)
done
text{*An alternative and more general proof goes like this: A and B are both
-well-ordered (because they are injected into an ordinal), either A lepoll B
-or B lepoll A. Also both are equipollent to their cardinalities, so
-(if A and B are infinite) then A Un B lepoll |A|+|B| = max(|A|,|B|) lepoll i.
+well-ordered (because they are injected into an ordinal), either @{term"A \<lesssim> B"}
+or @{term"B \<lesssim> A"}. Also both are equipollent to their cardinalities, so
+(if A and B are infinite) then @{term"A \<union> B \<lesssim> |A\<oplus>B| \<longleftrightarrow> max(|A|,|B|) \<lesssim> i"}.
In fact, the correctly strengthened version of this theorem appears below.*}
lemma Un_lepoll_Inf_Ord_weak:
"[|A \<approx> i; B \<approx> i; \<not> Finite(i); Ord(i)|] ==> A \<union> B \<lesssim> i"
apply (rule Un_lepoll_sum [THEN lepoll_trans])
apply (rule lepoll_imp_sum_lepoll_prod [THEN lepoll_trans])
-apply (erule eqpoll_trans [THEN eqpoll_imp_lepoll])
-apply (erule eqpoll_sym)
-apply (rule subset_imp_lepoll [THEN lepoll_trans, THEN lepoll_trans])
-apply (rule nat_2I [THEN OrdmemD], rule Ord_nat)
-apply (rule nat_le_infinite_Ord [THEN le_imp_lepoll], assumption+)
-apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll])
+apply (erule eqpoll_trans [THEN eqpoll_imp_lepoll])
+apply (erule eqpoll_sym)
+apply (rule subset_imp_lepoll [THEN lepoll_trans, THEN lepoll_trans])
+apply (rule nat_2I [THEN OrdmemD], rule Ord_nat)
+apply (rule nat_le_infinite_Ord [THEN le_imp_lepoll], assumption+)
+apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll])
apply (erule prod_eqpoll_cong [THEN eqpoll_imp_lepoll, THEN lepoll_trans],
assumption)
-apply (rule eqpoll_imp_lepoll)
-apply (rule well_ord_Memrel [THEN well_ord_InfCard_square_eq], assumption)
-apply (rule Inf_Ord_imp_InfCard_cardinal, assumption+)
+apply (rule eqpoll_imp_lepoll)
+apply (rule well_ord_Memrel [THEN well_ord_InfCard_square_eq], assumption)
+apply (rule Inf_Ord_imp_InfCard_cardinal, assumption+)
done
lemma Un_eqpoll_Inf_Ord:
- "[| A \<approx> i; B \<approx> i; ~Finite(i); Ord(i) |] ==> A Un B \<approx> i"
+ "[| A \<approx> i; B \<approx> i; ~Finite(i); Ord(i) |] ==> A \<union> B \<approx> i"
apply (rule eqpollI)
-apply (blast intro: Un_lepoll_Inf_Ord_weak)
-apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans])
-apply (rule Un_upper1 [THEN subset_imp_lepoll])
+apply (blast intro: Un_lepoll_Inf_Ord_weak)
+apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans])
+apply (rule Un_upper1 [THEN subset_imp_lepoll])
done
schematic_lemma paired_bij: "?f \<in> bij({{y,z}. y \<in> x}, x)"
@@ -79,19 +79,19 @@
lemma paired_eqpoll: "{{y,z}. y \<in> x} \<approx> x"
by (unfold eqpoll_def, fast intro!: paired_bij)
-lemma ex_eqpoll_disjoint: "\<exists>B. B \<approx> A & B Int C = 0"
+lemma ex_eqpoll_disjoint: "\<exists>B. B \<approx> A & B \<inter> C = 0"
by (fast intro!: paired_eqpoll equals0I elim: mem_asym)
(*Finally we reach this result. Surely there's a simpler proof, as sketched
above?*)
lemma Un_lepoll_Inf_Ord:
- "[| A \<lesssim> i; B \<lesssim> i; ~Finite(i); Ord(i) |] ==> A Un B \<lesssim> i"
+ "[| A \<lesssim> i; B \<lesssim> i; ~Finite(i); Ord(i) |] ==> A \<union> B \<lesssim> i"
apply (rule_tac A1 = i and C1 = i in ex_eqpoll_disjoint [THEN exE])
apply (erule conjE)
-apply (drule lepoll_trans)
+apply (drule lepoll_trans)
apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll])
apply (rule Un_lepoll_Un [THEN lepoll_trans], (assumption+))
-apply (blast intro: eqpoll_refl Un_eqpoll_Inf_Ord eqpoll_imp_lepoll)
+apply (blast intro: eqpoll_refl Un_eqpoll_Inf_Ord eqpoll_imp_lepoll)
done
lemma Least_in_Ord: "[| P(i); i \<in> j; Ord(j) |] ==> (LEAST i. P(i)) \<in> j"
@@ -103,14 +103,14 @@
done
lemma Diff_first_lepoll:
- "[| well_ord(x,r); y \<subseteq> x; y \<lesssim> succ(n); n \<in> nat |]
+ "[| well_ord(x,r); y \<subseteq> x; y \<lesssim> succ(n); n \<in> nat |]
==> y - {THE b. first(b,y,r)} \<lesssim> n"
-apply (case_tac "y=0", simp add: empty_lepollI)
+apply (case_tac "y=0", simp add: empty_lepollI)
apply (fast intro!: Diff_sing_lepoll the_first_in)
done
lemma UN_subset_split:
- "(\<Union>x \<in> X. P(x)) \<subseteq> (\<Union>x \<in> X. P(x)-Q(x)) Un (\<Union>x \<in> X. Q(x))"
+ "(\<Union>x \<in> X. P(x)) \<subseteq> (\<Union>x \<in> X. P(x)-Q(x)) \<union> (\<Union>x \<in> X. Q(x))"
by blast
lemma UN_sing_lepoll: "Ord(a) ==> (\<Union>x \<in> a. {P(x)}) \<lesssim> a"
@@ -122,14 +122,14 @@
done
lemma UN_fun_lepoll_lemma [rule_format]:
- "[| well_ord(T, R); ~Finite(a); Ord(a); n \<in> nat |]
- ==> \<forall>f. (\<forall>b \<in> a. f`b \<lesssim> n & f`b \<subseteq> T) --> (\<Union>b \<in> a. f`b) \<lesssim> a"
+ "[| well_ord(T, R); ~Finite(a); Ord(a); n \<in> nat |]
+ ==> \<forall>f. (\<forall>b \<in> a. f`b \<lesssim> n & f`b \<subseteq> T) \<longrightarrow> (\<Union>b \<in> a. f`b) \<lesssim> a"
apply (induct_tac "n")
apply (rule allI)
apply (rule impI)
apply (rule_tac b = "\<Union>b \<in> a. f`b" in subst)
apply (rule_tac [2] empty_lepollI)
-apply (rule equals0I [symmetric], clarify)
+apply (rule equals0I [symmetric], clarify)
apply (fast dest: lepoll_0_is_0 [THEN subst])
apply (rule allI)
apply (rule impI)
@@ -137,19 +137,19 @@
apply (erule impE, simp)
apply (fast intro!: Diff_first_lepoll, simp)
apply (rule UN_subset_split [THEN subset_imp_lepoll, THEN lepoll_trans])
-apply (fast intro: Un_lepoll_Inf_Ord UN_sing_lepoll)
+apply (fast intro: Un_lepoll_Inf_Ord UN_sing_lepoll)
done
lemma UN_fun_lepoll:
- "[| \<forall>b \<in> a. f`b \<lesssim> n & f`b \<subseteq> T; well_ord(T, R);
+ "[| \<forall>b \<in> a. f`b \<lesssim> n & f`b \<subseteq> T; well_ord(T, R);
~Finite(a); Ord(a); n \<in> nat |] ==> (\<Union>b \<in> a. f`b) \<lesssim> a"
-by (blast intro: UN_fun_lepoll_lemma)
+by (blast intro: UN_fun_lepoll_lemma)
lemma UN_lepoll:
- "[| \<forall>b \<in> a. F(b) \<lesssim> n & F(b) \<subseteq> T; well_ord(T, R);
- ~Finite(a); Ord(a); n \<in> nat |]
+ "[| \<forall>b \<in> a. F(b) \<lesssim> n & F(b) \<subseteq> T; well_ord(T, R);
+ ~Finite(a); Ord(a); n \<in> nat |]
==> (\<Union>b \<in> a. F(b)) \<lesssim> a"
-apply (rule rev_mp)
+apply (rule rev_mp)
apply (rule_tac f="\<lambda>b \<in> a. F (b)" in UN_fun_lepoll)
apply auto
done
@@ -167,11 +167,11 @@
apply (blast intro: Ord_Least ltI)
done
-lemma lepoll_imp_eqpoll_subset:
+lemma lepoll_imp_eqpoll_subset:
"a \<lesssim> X ==> \<exists>Y. Y \<subseteq> X & a \<approx> Y"
-apply (unfold lepoll_def eqpoll_def, clarify)
+apply (unfold lepoll_def eqpoll_def, clarify)
apply (blast intro: restrict_bij
- dest: inj_is_fun [THEN fun_is_rel, THEN image_subset])
+ dest: inj_is_fun [THEN fun_is_rel, THEN image_subset])
done
(* ********************************************************************** *)
@@ -184,27 +184,27 @@
apply (frule_tac j=xa in Un_upper1_le [OF lt_Ord lt_Ord], assumption)
apply (frule_tac j=xa in Un_upper2_le [OF lt_Ord lt_Ord], assumption)
apply (drule Un_least_lt, assumption)
-apply (drule eqpoll_imp_lepoll [THEN lepoll_trans],
+apply (drule eqpoll_imp_lepoll [THEN lepoll_trans],
rule le_imp_lepoll, assumption)+
-apply (case_tac "Finite(x Un xa)")
+apply (case_tac "Finite(x \<union> xa)")
txt{*finite case*}
- apply (drule Finite_Un [OF lepoll_Finite lepoll_Finite], assumption+)
+ apply (drule Finite_Un [OF lepoll_Finite lepoll_Finite], assumption+)
apply (drule subset_Un_Diff [THEN subset_imp_lepoll, THEN lepoll_Finite])
apply (fast dest: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_Finite])
txt{*infinite case*}
apply (drule Un_lepoll_Inf_Ord, (assumption+))
-apply (blast intro: le_Ord2)
-apply (drule lesspoll_trans1
- [OF subset_Un_Diff [THEN subset_imp_lepoll, THEN lepoll_trans]
+apply (blast intro: le_Ord2)
+apply (drule lesspoll_trans1
+ [OF subset_Un_Diff [THEN subset_imp_lepoll, THEN lepoll_trans]
lt_Card_imp_lesspoll], assumption+)
-apply (simp add: lesspoll_def)
+apply (simp add: lesspoll_def)
done
lemma Diff_lesspoll_eqpoll_Card:
"[| A \<approx> a; ~Finite(a); Card(a); B \<prec> a |] ==> A - B \<approx> a"
apply (rule ccontr)
apply (rule Diff_lesspoll_eqpoll_Card_lemma, (assumption+))
-apply (blast intro: lesspoll_def [THEN def_imp_iff, THEN iffD2]
+apply (blast intro: lesspoll_def [THEN def_imp_iff, THEN iffD2]
subset_imp_lepoll eqpoll_imp_lepoll lepoll_trans)
done
--- a/src/ZF/AC/DC.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/DC.thy Tue Mar 06 16:46:27 2012 +0000
@@ -82,13 +82,13 @@
definition
DC :: "i => o" where
"DC(a) == \<forall>X R. R \<subseteq> Pow(X)*X &
- (\<forall>Y \<in> Pow(X). Y \<prec> a --> (\<exists>x \<in> X. <Y,x> \<in> R))
- --> (\<exists>f \<in> a->X. \<forall>b<a. <f``b,f`b> \<in> R)"
+ (\<forall>Y \<in> Pow(X). Y \<prec> a \<longrightarrow> (\<exists>x \<in> X. <Y,x> \<in> R))
+ \<longrightarrow> (\<exists>f \<in> a->X. \<forall>b<a. <f``b,f`b> \<in> R)"
definition
DC0 :: o where
"DC0 == \<forall>A B R. R \<subseteq> A*B & R\<noteq>0 & range(R) \<subseteq> domain(R)
- --> (\<exists>f \<in> nat->domain(R). \<forall>n \<in> nat. <f`n,f`succ(n)>:R)"
+ \<longrightarrow> (\<exists>f \<in> nat->domain(R). \<forall>n \<in> nat. <f`n,f`succ(n)>:R)"
definition
ff :: "[i, i, i, i] => i" where
@@ -99,7 +99,7 @@
locale DC0_imp =
fixes XX and RR and X and R
- assumes all_ex: "\<forall>Y \<in> Pow(X). Y \<prec> nat --> (\<exists>x \<in> X. <Y, x> \<in> R)"
+ assumes all_ex: "\<forall>Y \<in> Pow(X). Y \<prec> nat \<longrightarrow> (\<exists>x \<in> X. <Y, x> \<in> R)"
defines XX_def: "XX == (\<Union>n \<in> nat. {f \<in> n->X. \<forall>k \<in> n. <f``k, f`k> \<in> R})"
and RR_def: "RR == {<z1,z2>:XX*XX. domain(z2)=succ(domain(z1))
@@ -314,7 +314,7 @@
lemma (in imp_DC0) lemma4:
"[| range(R) \<subseteq> domain(R); x \<in> domain(R) |]
==> RR \<subseteq> Pow(XX)*XX &
- (\<forall>Y \<in> Pow(XX). Y \<prec> nat --> (\<exists>x \<in> XX. <Y,x>:RR))"
+ (\<forall>Y \<in> Pow(XX). Y \<prec> nat \<longrightarrow> (\<exists>x \<in> XX. <Y,x>:RR))"
apply (rule conjI)
apply (force dest!: FinD [THEN PowI] simp add: RR_def)
apply (rule impI [THEN ballI])
@@ -331,7 +331,7 @@
lemma (in imp_DC0) UN_image_succ_eq:
"[| f \<in> nat->X; n \<in> nat |]
- ==> (\<Union>x \<in> f``succ(n). P(x)) = P(f`n) Un (\<Union>x \<in> f``n. P(x))"
+ ==> (\<Union>x \<in> f``succ(n). P(x)) = P(f`n) \<union> (\<Union>x \<in> f``n. P(x))"
by (simp add: image_fun OrdmemD)
lemma (in imp_DC0) UN_image_succ_eq_succ:
@@ -475,7 +475,7 @@
done
(* ********************************************************************** *)
-(* \<forall>K. Card(K) --> DC(K) ==> WO3 *)
+(* \<forall>K. Card(K) \<longrightarrow> DC(K) ==> WO3 *)
(* ********************************************************************** *)
lemma fun_Ord_inj:
@@ -492,7 +492,7 @@
lemma value_in_image: "[| f \<in> X->Y; A \<subseteq> X; a \<in> A |] ==> f`a \<in> f``A"
by (fast elim!: image_fun [THEN ssubst])
-theorem DC_WO3: "(\<forall>K. Card(K) --> DC(K)) ==> WO3"
+theorem DC_WO3: "(\<forall>K. Card(K) \<longrightarrow> DC(K)) ==> WO3"
apply (unfold DC_def WO3_def)
apply (rule allI)
apply (case_tac "A \<prec> Hartog (A)")
@@ -516,7 +516,7 @@
done
(* ********************************************************************** *)
-(* WO1 ==> \<forall>K. Card(K) --> DC(K) *)
+(* WO1 ==> \<forall>K. Card(K) \<longrightarrow> DC(K) *)
(* ********************************************************************** *)
lemma images_eq:
@@ -538,7 +538,7 @@
by (fast intro!: lam_type RepFunI)
lemma lemmaX:
- "[| \<forall>Y \<in> Pow(X). Y \<prec> K --> (\<exists>x \<in> X. <Y, x> \<in> R);
+ "[| \<forall>Y \<in> Pow(X). Y \<prec> K \<longrightarrow> (\<exists>x \<in> X. <Y, x> \<in> R);
b \<in> K; Z \<in> Pow(X); Z \<prec> K |]
==> {x \<in> X. <Z,x> \<in> R} \<noteq> 0"
by blast
@@ -546,7 +546,7 @@
lemma WO1_DC_lemma:
"[| Card(K); well_ord(X,Q);
- \<forall>Y \<in> Pow(X). Y \<prec> K --> (\<exists>x \<in> X. <Y, x> \<in> R); b \<in> K |]
+ \<forall>Y \<in> Pow(X). Y \<prec> K \<longrightarrow> (\<exists>x \<in> X. <Y, x> \<in> R); b \<in> K |]
==> ff(b, X, Q, R) \<in> {x \<in> X. <(\<lambda>c \<in> b. ff(c, X, Q, R))``b, x> \<in> R}"
apply (rule_tac P = "b \<in> K" in impE, (erule_tac [2] asm_rl)+)
apply (rule_tac i=b in Card_is_Ord [THEN Ord_in_Ord, THEN trans_induct],
@@ -560,7 +560,7 @@
apply (blast intro: lesspoll_trans1 in_Card_imp_lesspoll RepFun_lepoll)
done
-theorem WO1_DC_Card: "WO1 ==> \<forall>K. Card(K) --> DC(K)"
+theorem WO1_DC_Card: "WO1 ==> \<forall>K. Card(K) \<longrightarrow> DC(K)"
apply (unfold DC_def WO1_def)
apply (rule allI impI)+
apply (erule allE exE conjE)+
--- a/src/ZF/AC/Hartog.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/Hartog.thy Tue Mar 06 16:46:27 2012 +0000
@@ -12,7 +12,7 @@
Hartog :: "i => i" where
"Hartog(X) == LEAST i. ~ i \<lesssim> X"
-lemma Ords_in_set: "\<forall>a. Ord(a) --> a \<in> X ==> P"
+lemma Ords_in_set: "\<forall>a. Ord(a) \<longrightarrow> a \<in> X ==> P"
apply (rule_tac X = "{y \<in> X. Ord (y) }" in ON_class [elim_format])
apply fast
done
@@ -43,15 +43,15 @@
done
lemma Ords_lepoll_set_lemma:
- "(\<forall>a. Ord(a) --> a \<lesssim> X) ==>
- \<forall>a. Ord(a) -->
+ "(\<forall>a. Ord(a) \<longrightarrow> a \<lesssim> X) ==>
+ \<forall>a. Ord(a) \<longrightarrow>
a \<in> {b. Z \<in> Pow(X)*Pow(X*X), \<exists>Y R. Z=<Y,R> & ordertype(Y,R)=b}"
apply (intro allI impI)
apply (elim allE impE, assumption)
apply (blast dest!: Ord_lepoll_imp_eq_ordertype intro: sym)
done
-lemma Ords_lepoll_set: "\<forall>a. Ord(a) --> a \<lesssim> X ==> P"
+lemma Ords_lepoll_set: "\<forall>a. Ord(a) \<longrightarrow> a \<lesssim> X ==> P"
by (erule Ords_lepoll_set_lemma [THEN Ords_in_set])
lemma ex_Ord_not_lepoll: "\<exists>a. Ord(a) & ~a \<lesssim> X"
--- a/src/ZF/AC/WO1_AC.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/WO1_AC.thy Tue Mar 06 16:46:27 2012 +0000
@@ -11,7 +11,7 @@
Assume WO1. Let s be a set of infinite sets.
Suppose x \<in> s. Then x is equipollent to |x| (by WO1), an infinite cardinal
-call it K. Since K = K |+| K = |K+K| (by InfCard_cdouble_eq) there is an
+call it K. Since K = K \<oplus> K = |K+K| (by InfCard_cdouble_eq) there is an
isomorphism h \<in> bij(K+K, x). (Here + means disjoint sum.)
So there is a partition of x into 2-element sets, namely
@@ -41,7 +41,7 @@
lemma lemma1: "[| WO1; \<forall>B \<in> A. \<exists>C \<in> D(B). P(C,B) |] ==> \<exists>f. \<forall>B \<in> A. P(f`B,B)"
apply (unfold WO1_def)
-apply (erule_tac x = "Union ({{C \<in> D (B) . P (C,B) }. B \<in> A}) " in allE)
+apply (erule_tac x = "\<Union>({{C \<in> D (B) . P (C,B) }. B \<in> A}) " in allE)
apply (erule exE, drule ex_choice_fun, fast)
apply (erule exE)
apply (rule_tac x = "\<lambda>x \<in> A. f`{C \<in> D (x) . P (C,x) }" in exI)
@@ -82,7 +82,7 @@
done
lemma lemma2_5:
- "f \<in> bij(D+D, B) ==> Union({{f`Inl(i), f`Inr(i)}. i \<in> D})=B"
+ "f \<in> bij(D+D, B) ==> \<Union>({{f`Inl(i), f`Inr(i)}. i \<in> D})=B"
apply (unfold bij_def surj_def)
apply (fast elim!: inj_is_fun [THEN apply_type])
done
@@ -91,7 +91,7 @@
"[| WO1; ~Finite(B); 1\<le>n |]
==> \<exists>C \<in> Pow(Pow(B)). pairwise_disjoint(C) &
sets_of_size_between(C, 2, succ(n)) &
- Union(C)=B"
+ \<Union>(C)=B"
apply (drule lemma2_1 [THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]],
assumption)
apply (blast intro!: lemma2_2 lemma2_3 lemma2_4 lemma2_5)
--- a/src/ZF/AC/WO1_WO7.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/WO1_WO7.thy Tue Mar 06 16:46:27 2012 +0000
@@ -2,10 +2,10 @@
Author: Lawrence C Paulson, CU Computer Laboratory
Copyright 1998 University of Cambridge
-WO7 <-> LEMMA <-> WO1 (Rubin & Rubin p. 5)
+WO7 \<longleftrightarrow> LEMMA \<longleftrightarrow> WO1 (Rubin & Rubin p. 5)
LEMMA is the sentence denoted by (**)
-Also, WO1 <-> WO8
+Also, WO1 \<longleftrightarrow> WO8
*)
theory WO1_WO7
@@ -14,13 +14,13 @@
definition
"LEMMA ==
- \<forall>X. ~Finite(X) --> (\<exists>R. well_ord(X,R) & ~well_ord(X,converse(R)))"
+ \<forall>X. ~Finite(X) \<longrightarrow> (\<exists>R. well_ord(X,R) & ~well_ord(X,converse(R)))"
(* ********************************************************************** *)
(* It is easy to see that WO7 is equivalent to (**) *)
(* ********************************************************************** *)
-lemma WO7_iff_LEMMA: "WO7 <-> LEMMA"
+lemma WO7_iff_LEMMA: "WO7 \<longleftrightarrow> LEMMA"
apply (unfold WO7_def LEMMA_def)
apply (blast intro: Finite_well_ord_converse)
done
@@ -85,7 +85,7 @@
lepoll_def [THEN def_imp_iff, THEN iffD2] )
done
-lemma WO1_iff_WO7: "WO1 <-> WO7"
+lemma WO1_iff_WO7: "WO1 \<longleftrightarrow> WO7"
apply (simp add: WO7_iff_LEMMA)
apply (blast intro: LEMMA_imp_WO1 WO1_imp_LEMMA)
done
@@ -93,7 +93,7 @@
(* ********************************************************************** *)
-(* The proof of WO8 <-> WO1 (Rubin & Rubin p. 6) *)
+(* The proof of WO8 \<longleftrightarrow> WO1 (Rubin & Rubin p. 6) *)
(* ********************************************************************** *)
lemma WO1_WO8: "WO1 ==> WO8"
--- a/src/ZF/AC/WO2_AC16.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/WO2_AC16.thy Tue Mar 06 16:46:27 2012 +0000
@@ -9,7 +9,7 @@
The first instance is trivial, the third not difficult, but the second
is very complicated requiring many lemmas.
We also need to prove that at any stage gamma the set
-(s - Union(...) - k_gamma) (Rubin & Rubin page 15)
+(s - \<Union>(...) - k_gamma) (Rubin & Rubin page 15)
contains m distinct elements (in fact is equipollent to s)
*)
@@ -22,8 +22,8 @@
"recfunAC16(f,h,i,a) ==
transrec2(i, 0,
%g r. if (\<exists>y \<in> r. h`g \<subseteq> y) then r
- else r Un {f`(LEAST i. h`g \<subseteq> f`i &
- (\<forall>b<a. (h`b \<subseteq> f`i --> (\<forall>t \<in> r. ~ h`b \<subseteq> t))))})"
+ else r \<union> {f`(LEAST i. h`g \<subseteq> f`i &
+ (\<forall>b<a. (h`b \<subseteq> f`i \<longrightarrow> (\<forall>t \<in> r. ~ h`b \<subseteq> t))))})"
(* ********************************************************************** *)
(* Basic properties of recfunAC16 *)
@@ -35,10 +35,10 @@
lemma recfunAC16_succ:
"recfunAC16(f,h,succ(i),a) =
(if (\<exists>y \<in> recfunAC16(f,h,i,a). h ` i \<subseteq> y) then recfunAC16(f,h,i,a)
- else recfunAC16(f,h,i,a) Un
+ else recfunAC16(f,h,i,a) \<union>
{f ` (LEAST j. h ` i \<subseteq> f ` j &
(\<forall>b<a. (h`b \<subseteq> f`j
- --> (\<forall>t \<in> recfunAC16(f,h,i,a). ~ h`b \<subseteq> t))))})"
+ \<longrightarrow> (\<forall>t \<in> recfunAC16(f,h,i,a). ~ h`b \<subseteq> t))))})"
apply (simp add: recfunAC16_def)
done
@@ -52,7 +52,7 @@
lemma transrec2_mono_lemma [rule_format]:
"[| !!g r. r \<subseteq> B(g,r); Ord(i) |]
- ==> j<i --> transrec2(j, 0, B) \<subseteq> transrec2(i, 0, B)"
+ ==> j<i \<longrightarrow> transrec2(j, 0, B) \<subseteq> transrec2(i, 0, B)"
apply (erule trans_induct)
apply (rule Ord_cases, assumption+, fast)
apply (simp (no_asm_simp))
@@ -86,8 +86,8 @@
lemma lemma3_1:
- "[| \<forall>y<x. \<forall>z<a. z<y | (\<exists>Y \<in> F(y). f(z)<=Y) --> (\<exists>! Y. Y \<in> F(y) & f(z)<=Y);
- \<forall>i j. i\<le>j --> F(i) \<subseteq> F(j); j\<le>i; i<x; z<a;
+ "[| \<forall>y<x. \<forall>z<a. z<y | (\<exists>Y \<in> F(y). f(z)<=Y) \<longrightarrow> (\<exists>! Y. Y \<in> F(y) & f(z)<=Y);
+ \<forall>i j. i\<le>j \<longrightarrow> F(i) \<subseteq> F(j); j\<le>i; i<x; z<a;
V \<in> F(i); f(z)<=V; W \<in> F(j); f(z)<=W |]
==> V = W"
apply (erule asm_rl allE impE)+
@@ -96,8 +96,8 @@
lemma lemma3:
- "[| \<forall>y<x. \<forall>z<a. z<y | (\<exists>Y \<in> F(y). f(z)<=Y) --> (\<exists>! Y. Y \<in> F(y) & f(z)<=Y);
- \<forall>i j. i\<le>j --> F(i) \<subseteq> F(j); i<x; j<x; z<a;
+ "[| \<forall>y<x. \<forall>z<a. z<y | (\<exists>Y \<in> F(y). f(z)<=Y) \<longrightarrow> (\<exists>! Y. Y \<in> F(y) & f(z)<=Y);
+ \<forall>i j. i\<le>j \<longrightarrow> F(i) \<subseteq> F(j); i<x; j<x; z<a;
V \<in> F(i); f(z)<=V; W \<in> F(j); f(z)<=W |]
==> V = W"
apply (rule_tac j=j in Ord_linear_le [OF lt_Ord lt_Ord], assumption+)
@@ -107,10 +107,10 @@
lemma lemma4:
"[| \<forall>y<x. F(y) \<subseteq> X &
- (\<forall>x<a. x < y | (\<exists>Y \<in> F(y). h(x) \<subseteq> Y) -->
+ (\<forall>x<a. x < y | (\<exists>Y \<in> F(y). h(x) \<subseteq> Y) \<longrightarrow>
(\<exists>! Y. Y \<in> F(y) & h(x) \<subseteq> Y));
x < a |]
- ==> \<forall>y<x. \<forall>z<a. z < y | (\<exists>Y \<in> F(y). h(z) \<subseteq> Y) -->
+ ==> \<forall>y<x. \<forall>z<a. z < y | (\<exists>Y \<in> F(y). h(z) \<subseteq> Y) \<longrightarrow>
(\<exists>! Y. Y \<in> F(y) & h(z) \<subseteq> Y)"
apply (intro oallI impI)
apply (drule ospec, assumption, clarify)
@@ -119,12 +119,12 @@
lemma lemma5:
"[| \<forall>y<x. F(y) \<subseteq> X &
- (\<forall>x<a. x < y | (\<exists>Y \<in> F(y). h(x) \<subseteq> Y) -->
+ (\<forall>x<a. x < y | (\<exists>Y \<in> F(y). h(x) \<subseteq> Y) \<longrightarrow>
(\<exists>! Y. Y \<in> F(y) & h(x) \<subseteq> Y));
- x < a; Limit(x); \<forall>i j. i\<le>j --> F(i) \<subseteq> F(j) |]
+ x < a; Limit(x); \<forall>i j. i\<le>j \<longrightarrow> F(i) \<subseteq> F(j) |]
==> (\<Union>x<x. F(x)) \<subseteq> X &
(\<forall>xa<a. xa < x | (\<exists>x \<in> \<Union>x<x. F(x). h(xa) \<subseteq> x)
- --> (\<exists>! Y. Y \<in> (\<Union>x<x. F(x)) & h(xa) \<subseteq> Y))"
+ \<longrightarrow> (\<exists>! Y. Y \<in> (\<Union>x<x. F(x)) & h(xa) \<subseteq> Y))"
apply (rule conjI)
apply (rule subsetI)
apply (erule OUN_E)
@@ -147,7 +147,7 @@
(*
First quite complicated proof of the fact used in the recursive construction
of the family T_gamma (WO2 ==> AC16(k #+ m, k)) - the fact that at any stage
- gamma the set (s - Union(...) - k_gamma) is equipollent to s
+ gamma the set (s - \<Union>(...) - k_gamma) is equipollent to s
(Rubin & Rubin page 15).
*)
@@ -179,7 +179,7 @@
lemma Union_lesspoll:
"[| \<forall>x \<in> X. x lepoll n & x \<subseteq> T; well_ord(T, R); X lepoll b;
b<a; ~Finite(a); Card(a); n \<in> nat |]
- ==> Union(X)\<prec>a"
+ ==> \<Union>(X)\<prec>a"
apply (case_tac "Finite (X)")
apply (blast intro: Card_is_Ord Finite_lesspoll_infinite_Ord
lepoll_nat_imp_Finite Finite_Union)
@@ -200,10 +200,10 @@
(* recfunAC16_lepoll_index *)
(* ********************************************************************** *)
-lemma Un_sing_eq_cons: "A Un {a} = cons(a, A)"
+lemma Un_sing_eq_cons: "A \<union> {a} = cons(a, A)"
by fast
-lemma Un_lepoll_succ: "A lepoll B ==> A Un {a} lepoll succ(B)"
+lemma Un_lepoll_succ: "A lepoll B ==> A \<union> {a} lepoll succ(B)"
apply (simp add: Un_sing_eq_cons succ_def)
apply (blast elim!: mem_irrefl intro: cons_lepoll_cong)
done
@@ -211,7 +211,7 @@
lemma Diff_UN_succ_empty: "Ord(a) ==> F(a) - (\<Union>b<succ(a). F(b)) = 0"
by (fast intro!: le_refl)
-lemma Diff_UN_succ_subset: "Ord(a) ==> F(a) Un X - (\<Union>b<succ(a). F(b)) \<subseteq> X"
+lemma Diff_UN_succ_subset: "Ord(a) ==> F(a) \<union> X - (\<Union>b<succ(a). F(b)) \<subseteq> X"
by blast
lemma recfunAC16_Diff_lepoll_1:
@@ -288,7 +288,7 @@
lemma Union_recfunAC16_lesspoll:
"[| recfunAC16(f,g,y,a) \<subseteq> {X \<in> Pow(A). X\<approx>n};
A\<approx>a; y<a; ~Finite(a); Card(a); n \<in> nat |]
- ==> Union(recfunAC16(f,g,y,a))\<prec>a"
+ ==> \<Union>(recfunAC16(f,g,y,a))\<prec>a"
apply (erule eqpoll_def [THEN def_imp_iff, THEN iffD1, THEN exE])
apply (rule_tac T=A in Union_lesspoll, simp_all)
apply (blast intro!: eqpoll_imp_lepoll)
@@ -302,7 +302,7 @@
Card(a); ~ Finite(a); A\<approx>a;
k \<in> nat; y<a;
h \<in> bij(a, {Y \<in> Pow(A). Y\<approx>succ(k)}) |]
- ==> A - Union(recfunAC16(f, h, y, a)) - h`y\<approx>a"
+ ==> A - \<Union>(recfunAC16(f, h, y, a)) - h`y\<approx>a"
apply (rule dbl_Diff_eqpoll_Card, simp_all)
apply (simp add: Union_recfunAC16_lesspoll)
apply (rule Finite_lesspoll_infinite_Ord)
@@ -320,7 +320,7 @@
lemma Un_in_Collect: "[| x \<in> Pow(A - B - h`i); x\<approx>m;
h \<in> bij(a, {x \<in> Pow(A) . x\<approx>k}); i<a; k \<in> nat; m \<in> nat |]
- ==> h ` i Un x \<in> {x \<in> Pow(A) . x\<approx>k #+ m}"
+ ==> h ` i \<union> x \<in> {x \<in> Pow(A) . x\<approx>k #+ m}"
by (blast intro: disj_Un_eqpoll_nat_sum
dest: ltD bij_is_fun [THEN apply_type])
@@ -330,14 +330,14 @@
(* ********************************************************************** *)
lemma lemma6:
- "[| \<forall>y<succ(j). F(y)<=X & (\<forall>x<a. x<y | P(x,y) --> Q(x,y)); succ(j)<a |]
- ==> F(j)<=X & (\<forall>x<a. x<j | P(x,j) --> Q(x,j))"
+ "[| \<forall>y<succ(j). F(y)<=X & (\<forall>x<a. x<y | P(x,y) \<longrightarrow> Q(x,y)); succ(j)<a |]
+ ==> F(j)<=X & (\<forall>x<a. x<j | P(x,j) \<longrightarrow> Q(x,j))"
by (blast intro!: lt_Ord succI1 [THEN ltI, THEN lt_Ord, THEN le_refl])
lemma lemma7:
- "[| \<forall>x<a. x<j | P(x,j) --> Q(x,j); succ(j)<a |]
- ==> P(j,j) --> (\<forall>x<a. x\<le>j | P(x,j) --> Q(x,j))"
+ "[| \<forall>x<a. x<j | P(x,j) \<longrightarrow> Q(x,j); succ(j)<a |]
+ ==> P(j,j) \<longrightarrow> (\<forall>x<a. x\<le>j | P(x,j) \<longrightarrow> Q(x,j))"
by (fast elim!: leE)
(* ********************************************************************** *)
@@ -354,12 +354,12 @@
apply (fast elim!: eqpoll_sym)
done
-lemma subset_Un_disjoint: "[| A \<subseteq> B Un C; A Int C = 0 |] ==> A \<subseteq> B"
+lemma subset_Un_disjoint: "[| A \<subseteq> B \<union> C; A \<inter> C = 0 |] ==> A \<subseteq> B"
by blast
lemma Int_empty:
- "[| X \<in> Pow(A - Union(B) -C); T \<in> B; F \<subseteq> T |] ==> F Int X = 0"
+ "[| X \<in> Pow(A - \<Union>(B) -C); T \<in> B; F \<subseteq> T |] ==> F \<inter> X = 0"
by blast
@@ -369,7 +369,7 @@
lemma subset_imp_eq_lemma:
- "m \<in> nat ==> \<forall>A B. A \<subseteq> B & m lepoll A & B lepoll m --> A=B"
+ "m \<in> nat ==> \<forall>A B. A \<subseteq> B & m lepoll A & B lepoll m \<longrightarrow> A=B"
apply (induct_tac "m")
apply (fast dest!: lepoll_0_is_0)
apply (intro allI impI)
@@ -407,7 +407,7 @@
h \<in> bij(a, {Y \<in> Pow(A). Y\<approx>succ(k)});
~ (\<exists>Y \<in> recfunAC16(f, h, y, a). h`y \<subseteq> Y) |]
==> \<exists>X \<in> {Y \<in> Pow(A). Y\<approx>succ(k #+ m)}. h`y \<subseteq> X &
- (\<forall>b<a. h`b \<subseteq> X -->
+ (\<forall>b<a. h`b \<subseteq> X \<longrightarrow>
(\<forall>T \<in> recfunAC16(f, h, y, a). ~ h`b \<subseteq> T))"
apply (erule_tac m1=m in dbl_Diff_eqpoll [THEN ex_subset_eqpoll, THEN bexE],
assumption+)
@@ -434,7 +434,7 @@
f \<in> bij(a, {Y \<in> Pow(A). Y\<approx>succ(k #+ m)});
~ (\<exists>Y \<in> recfunAC16(f, h, y, a). h`y \<subseteq> Y) |]
==> \<exists>c<a. h`y \<subseteq> f`c &
- (\<forall>b<a. h`b \<subseteq> f`c -->
+ (\<forall>b<a. h`b \<subseteq> f`c \<longrightarrow>
(\<forall>T \<in> recfunAC16(f, h, y, a). ~ h`b \<subseteq> T))"
apply (drule ex_next_set, assumption+)
apply (erule bexE)
@@ -451,11 +451,11 @@
lemma lemma8:
"[| \<forall>x<a. x<j | (\<exists>xa \<in> F(j). P(x, xa))
- --> (\<exists>! Y. Y \<in> F(j) & P(x, Y)); F(j) \<subseteq> X;
- L \<in> X; P(j, L) & (\<forall>x<a. P(x, L) --> (\<forall>xa \<in> F(j). ~P(x, xa))) |]
- ==> F(j) Un {L} \<subseteq> X &
- (\<forall>x<a. x\<le>j | (\<exists>xa \<in> (F(j) Un {L}). P(x, xa)) -->
- (\<exists>! Y. Y \<in> (F(j) Un {L}) & P(x, Y)))"
+ \<longrightarrow> (\<exists>! Y. Y \<in> F(j) & P(x, Y)); F(j) \<subseteq> X;
+ L \<in> X; P(j, L) & (\<forall>x<a. P(x, L) \<longrightarrow> (\<forall>xa \<in> F(j). ~P(x, xa))) |]
+ ==> F(j) \<union> {L} \<subseteq> X &
+ (\<forall>x<a. x\<le>j | (\<exists>xa \<in> (F(j) \<union> {L}). P(x, xa)) \<longrightarrow>
+ (\<exists>! Y. Y \<in> (F(j) \<union> {L}) & P(x, Y)))"
apply (rule conjI)
apply (fast intro!: singleton_subsetI)
apply (rule oallI)
@@ -472,7 +472,7 @@
h \<in> bij(a, {Y \<in> Pow(A) . Y\<approx>succ(k)});
~Finite(a); Card(a); A\<approx>a; k \<in> nat; m \<in> nat |]
==> recfunAC16(f, h, b, a) \<subseteq> {X \<in> Pow(A) . X\<approx>succ(k #+ m)} &
- (\<forall>x<a. x < b | (\<exists>Y \<in> recfunAC16(f, h, b, a). h ` x \<subseteq> Y) -->
+ (\<forall>x<a. x < b | (\<exists>Y \<in> recfunAC16(f, h, b, a). h ` x \<subseteq> Y) \<longrightarrow>
(\<exists>! Y. Y \<in> recfunAC16(f, h, b, a) & h ` x \<subseteq> Y))"
apply (erule lt_induct)
apply (frule lt_Ord)
@@ -507,10 +507,10 @@
(* ********************************************************************** *)
lemma lemma_simp_induct:
- "[| \<forall>b. b<a --> F(b) \<subseteq> S & (\<forall>x<a. (x<b | (\<exists>Y \<in> F(b). f`x \<subseteq> Y))
- --> (\<exists>! Y. Y \<in> F(b) & f`x \<subseteq> Y));
+ "[| \<forall>b. b<a \<longrightarrow> F(b) \<subseteq> S & (\<forall>x<a. (x<b | (\<exists>Y \<in> F(b). f`x \<subseteq> Y))
+ \<longrightarrow> (\<exists>! Y. Y \<in> F(b) & f`x \<subseteq> Y));
f \<in> a->f``(a); Limit(a);
- \<forall>i j. i\<le>j --> F(i) \<subseteq> F(j) |]
+ \<forall>i j. i\<le>j \<longrightarrow> F(i) \<subseteq> F(j) |]
==> (\<Union>j<a. F(j)) \<subseteq> S &
(\<forall>x \<in> f``a. \<exists>! Y. Y \<in> (\<Union>j<a. F(j)) & x \<subseteq> Y)"
apply (rule conjI)
--- a/src/ZF/AC/WO6_WO1.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/WO6_WO1.thy Tue Mar 06 16:46:27 2012 +0000
@@ -22,7 +22,7 @@
definition
uu :: "[i, i, i, i] => i" where
- "uu(f, beta, gamma, delta) == (f`beta * f`gamma) Int f`delta"
+ "uu(f, beta, gamma, delta) == (f`beta * f`gamma) \<inter> f`delta"
(** Definitions for case 1 **)
@@ -171,9 +171,9 @@
(* ********************************************************************** *)
lemma cases:
"\<forall>b<a. \<forall>g<a. \<forall>d<a. u(f,b,g,d) \<lesssim> m
- ==> (\<forall>b<a. f`b \<noteq> 0 -->
+ ==> (\<forall>b<a. f`b \<noteq> 0 \<longrightarrow>
(\<exists>g<a. \<exists>d<a. u(f,b,g,d) \<noteq> 0 & u(f,b,g,d) \<prec> m))
- | (\<exists>b<a. f`b \<noteq> 0 & (\<forall>g<a. \<forall>d<a. u(f,b,g,d) \<noteq> 0 -->
+ | (\<exists>b<a. f`b \<noteq> 0 & (\<forall>g<a. \<forall>d<a. u(f,b,g,d) \<noteq> 0 \<longrightarrow>
u(f,b,g,d) \<approx> m))"
apply (unfold lesspoll_def)
apply (blast del: equalityI)
@@ -182,7 +182,7 @@
(* ********************************************************************** *)
(* Lemmas used in both cases *)
(* ********************************************************************** *)
-lemma UN_oadd: "Ord(a) ==> (\<Union>b<a++a. C(b)) = (\<Union>b<a. C(b) Un C(a++b))"
+lemma UN_oadd: "Ord(a) ==> (\<Union>b<a++a. C(b)) = (\<Union>b<a. C(b) \<union> C(a++b))"
by (blast intro: ltI lt_oadd1 oadd_lt_mono2 dest!: lt_oadd_disj)
@@ -223,7 +223,7 @@
lemma gg1_lepoll_m:
"[| Ord(a); m \<in> nat;
- \<forall>b<a. f`b \<noteq>0 -->
+ \<forall>b<a. f`b \<noteq>0 \<longrightarrow>
(\<exists>g<a. \<exists>d<a. domain(uu(f,b,g,d)) \<noteq> 0 &
domain(uu(f,b,g,d)) \<lesssim> m);
\<forall>b<a. f`b \<lesssim> succ(m); b<a++a |]
@@ -293,7 +293,7 @@
done
lemma uu_Least_is_fun:
- "[| \<forall>g<a. \<forall>d<a. domain(uu(f, b, g, d))\<noteq>0 -->
+ "[| \<forall>g<a. \<forall>d<a. domain(uu(f, b, g, d))\<noteq>0 \<longrightarrow>
domain(uu(f, b, g, d)) \<approx> succ(m);
\<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y;
(\<Union>b<a. f`b)=y; b<a; g<a; d<a;
@@ -312,7 +312,7 @@
done
lemma vv2_subset:
- "[| \<forall>g<a. \<forall>d<a. domain(uu(f, b, g, d))\<noteq>0 -->
+ "[| \<forall>g<a. \<forall>d<a. domain(uu(f, b, g, d))\<noteq>0 \<longrightarrow>
domain(uu(f, b, g, d)) \<approx> succ(m);
\<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y;
(\<Union>b<a. f`b)=y; b<a; g<a; m \<in> nat; s \<in> f`b |]
@@ -325,7 +325,7 @@
(* Case 2: Union of images is the whole "y" *)
(* ********************************************************************** *)
lemma UN_gg2_eq:
- "[| \<forall>g<a. \<forall>d<a. domain(uu(f,b,g,d)) \<noteq> 0 -->
+ "[| \<forall>g<a. \<forall>d<a. domain(uu(f,b,g,d)) \<noteq> 0 \<longrightarrow>
domain(uu(f,b,g,d)) \<approx> succ(m);
\<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y;
(\<Union>b<a. f`b)=y; Ord(a); m \<in> nat; s \<in> f`b; b<a |]
@@ -366,7 +366,7 @@
done
lemma gg2_lepoll_m:
- "[| \<forall>g<a. \<forall>d<a. domain(uu(f,b,g,d)) \<noteq> 0 -->
+ "[| \<forall>g<a. \<forall>d<a. domain(uu(f,b,g,d)) \<noteq> 0 \<longrightarrow>
domain(uu(f,b,g,d)) \<approx> succ(m);
\<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y;
(\<Union>b<a. f`b)=y; b<a; s \<in> f`b; m \<in> nat; m\<noteq> 0; g<a++a |]
@@ -401,7 +401,7 @@
(* ********************************************************************** *)
(* lemma iv - p. 4: *)
-(* For every set x there is a set y such that x Un (y * y) \<subseteq> y *)
+(* For every set x there is a set y such that x \<union> (y * y) \<subseteq> y *)
(* ********************************************************************** *)
@@ -409,29 +409,29 @@
(used only in the following two lemmas) *)
lemma z_n_subset_z_succ_n:
- "\<forall>n \<in> nat. rec(n, x, %k r. r Un r*r) \<subseteq> rec(succ(n), x, %k r. r Un r*r)"
+ "\<forall>n \<in> nat. rec(n, x, %k r. r \<union> r*r) \<subseteq> rec(succ(n), x, %k r. r \<union> r*r)"
by (fast intro: rec_succ [THEN ssubst])
lemma le_subsets:
"[| \<forall>n \<in> nat. f(n)<=f(succ(n)); n\<le>m; n \<in> nat; m \<in> nat |]
==> f(n)<=f(m)"
apply (erule_tac P = "n\<le>m" in rev_mp)
-apply (rule_tac P = "%z. n\<le>z --> f (n) \<subseteq> f (z) " in nat_induct)
+apply (rule_tac P = "%z. n\<le>z \<longrightarrow> f (n) \<subseteq> f (z) " in nat_induct)
apply (auto simp add: le_iff)
done
lemma le_imp_rec_subset:
"[| n\<le>m; m \<in> nat |]
- ==> rec(n, x, %k r. r Un r*r) \<subseteq> rec(m, x, %k r. r Un r*r)"
+ ==> rec(n, x, %k r. r \<union> r*r) \<subseteq> rec(m, x, %k r. r \<union> r*r)"
apply (rule z_n_subset_z_succ_n [THEN le_subsets])
apply (blast intro: lt_nat_in_nat)+
done
-lemma lemma_iv: "\<exists>y. x Un y*y \<subseteq> y"
-apply (rule_tac x = "\<Union>n \<in> nat. rec (n, x, %k r. r Un r*r) " in exI)
+lemma lemma_iv: "\<exists>y. x \<union> y*y \<subseteq> y"
+apply (rule_tac x = "\<Union>n \<in> nat. rec (n, x, %k r. r \<union> r*r) " in exI)
apply safe
apply (rule nat_0I [THEN UN_I], simp)
-apply (rule_tac a = "succ (n Un na) " in UN_I)
+apply (rule_tac a = "succ (n \<union> na) " in UN_I)
apply (erule Un_nat_type [THEN nat_succI], assumption)
apply (auto intro: le_imp_rec_subset [THEN subsetD]
intro!: Un_upper1_le Un_upper2_le Un_nat_type
@@ -494,7 +494,7 @@
lemma rev_induct_lemma [rule_format]:
"[| n \<in> nat; !!m. [| m \<in> nat; m\<noteq>0; P(succ(m)) |] ==> P(m) |]
- ==> n\<noteq>0 --> P(n) --> P(1)"
+ ==> n\<noteq>0 \<longrightarrow> P(n) \<longrightarrow> P(1)"
by (erule nat_induct, blast+)
lemma rev_induct:
--- a/src/ZF/Coind/Dynamic.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Coind/Dynamic.thy Tue Mar 06 16:46:27 2012 +0000
@@ -8,7 +8,7 @@
consts
EvalRel :: i
inductive
- domains "EvalRel" <= "ValEnv * Exp * Val"
+ domains "EvalRel" \<subseteq> "ValEnv * Exp * Val"
intros
eval_constI:
" [| ve \<in> ValEnv; c \<in> Const |] ==>
--- a/src/ZF/Coind/ECR.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Coind/ECR.thy Tue Mar 06 16:46:27 2012 +0000
@@ -10,7 +10,7 @@
consts
HasTyRel :: i
coinductive
- domains "HasTyRel" <= "Val * Ty"
+ domains "HasTyRel" \<subseteq> "Val * Ty"
intros
htr_constI [intro!]:
"[| c \<in> Const; t \<in> Ty; isof(c,t) |] ==> <v_const(c),t> \<in> HasTyRel"
@@ -37,7 +37,7 @@
"[| x \<in> ExVar; e \<in> Exp; t \<in> Ty; ve \<in> ValEnv; te \<in> TyEnv;
<te, e_fn(x, e), t> \<in> ElabRel; ve_dom(ve) = te_dom(te);
{<ve_app(ve,y),te_app(te,y)>.y \<in> ve_dom(ve)} \<in>
- Pow({<v_clos(x,e,ve),t>} Un HasTyRel) |]
+ Pow({<v_clos(x,e,ve),t>} \<union> HasTyRel) |]
==> <v_clos(x, e, ve),t> \<in> HasTyRel"
apply (rule singletonI [THEN HasTyRel.coinduct], auto)
done
@@ -113,10 +113,10 @@
"[| ve \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; c1 \<in> Const; c2 \<in> Const;
<ve,e1,v_const(c1)> \<in> EvalRel;
\<forall>t te.
- hastyenv(ve,te) --> <te,e1,t> \<in> ElabRel --> <v_const(c1),t> \<in> HasTyRel;
+ hastyenv(ve,te) \<longrightarrow> <te,e1,t> \<in> ElabRel \<longrightarrow> <v_const(c1),t> \<in> HasTyRel;
<ve, e2, v_const(c2)> \<in> EvalRel;
\<forall>t te.
- hastyenv(ve,te) --> <te,e2,t> \<in> ElabRel --> <v_const(c2),t> \<in> HasTyRel;
+ hastyenv(ve,te) \<longrightarrow> <te,e2,t> \<in> ElabRel \<longrightarrow> <v_const(c2),t> \<in> HasTyRel;
hastyenv(ve, te);
<te,e_app(e1,e2),t> \<in> ElabRel |]
==> <v_const(c_app(c1, c2)),t> \<in> HasTyRel"
@@ -126,13 +126,13 @@
"[| ve \<in> ValEnv; vem \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; em \<in> Exp; xm \<in> ExVar;
v \<in> Val;
<ve,e1,v_clos(xm,em,vem)> \<in> EvalRel;
- \<forall>t te. hastyenv(ve,te) -->
- <te,e1,t> \<in> ElabRel --> <v_clos(xm,em,vem),t> \<in> HasTyRel;
+ \<forall>t te. hastyenv(ve,te) \<longrightarrow>
+ <te,e1,t> \<in> ElabRel \<longrightarrow> <v_clos(xm,em,vem),t> \<in> HasTyRel;
<ve,e2,v2> \<in> EvalRel;
- \<forall>t te. hastyenv(ve,te) --> <te,e2,t> \<in> ElabRel --> <v2,t> \<in> HasTyRel;
+ \<forall>t te. hastyenv(ve,te) \<longrightarrow> <te,e2,t> \<in> ElabRel \<longrightarrow> <v2,t> \<in> HasTyRel;
<ve_owr(vem,xm,v2),em,v> \<in> EvalRel;
- \<forall>t te. hastyenv(ve_owr(vem,xm,v2),te) -->
- <te,em,t> \<in> ElabRel --> <v,t> \<in> HasTyRel;
+ \<forall>t te. hastyenv(ve_owr(vem,xm,v2),te) \<longrightarrow>
+ <te,em,t> \<in> ElabRel \<longrightarrow> <v,t> \<in> HasTyRel;
hastyenv(ve,te); <te,e_app(e1,e2),t> \<in> ElabRel |]
==> <v,t> \<in> HasTyRel"
apply (erule elab_appE)
@@ -150,7 +150,7 @@
lemma consistency [rule_format]:
"<ve,e,v> \<in> EvalRel
- ==> (\<forall>t te. hastyenv(ve,te) --> <te,e,t> \<in> ElabRel --> <v,t> \<in> HasTyRel)"
+ ==> (\<forall>t te. hastyenv(ve,te) \<longrightarrow> <te,e,t> \<in> ElabRel \<longrightarrow> <v,t> \<in> HasTyRel)"
apply (erule EvalRel.induct)
apply (simp_all add: consistency_const consistency_var consistency_fn
consistency_fix consistency_app1)
--- a/src/ZF/Coind/Map.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Coind/Map.thy Tue Mar 06 16:46:27 2012 +0000
@@ -9,7 +9,7 @@
definition
TMap :: "[i,i] => i" where
- "TMap(A,B) == {m \<in> Pow(A*Union(B)).\<forall>a \<in> A. m``{a} \<in> B}"
+ "TMap(A,B) == {m \<in> Pow(A*\<Union>(B)).\<forall>a \<in> A. m``{a} \<in> B}"
definition
PMap :: "[i,i] => i" where
@@ -23,24 +23,24 @@
definition
map_owr :: "[i,i,i]=>i" where
- "map_owr(m,a,b) == \<Sigma> x \<in> {a} Un domain(m). if x=a then b else m``{x}"
+ "map_owr(m,a,b) == \<Sigma> x \<in> {a} \<union> domain(m). if x=a then b else m``{x}"
definition
map_app :: "[i,i]=>i" where
"map_app(m,a) == m``{a}"
-lemma "{0,1} \<subseteq> {1} Un TMap(I, {0,1})"
+lemma "{0,1} \<subseteq> {1} \<union> TMap(I, {0,1})"
by (unfold TMap_def, blast)
-lemma "{0} Un TMap(I,1) \<subseteq> {1} Un TMap(I, {0} Un TMap(I,1))"
+lemma "{0} \<union> TMap(I,1) \<subseteq> {1} \<union> TMap(I, {0} \<union> TMap(I,1))"
by (unfold TMap_def, blast)
-lemma "{0,1} Un TMap(I,2) \<subseteq> {1} Un TMap(I, {0,1} Un TMap(I,2))"
+lemma "{0,1} \<union> TMap(I,2) \<subseteq> {1} \<union> TMap(I, {0,1} \<union> TMap(I,2))"
by (unfold TMap_def, blast)
(*A bit too slow.
-lemma "{0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2) \<subseteq>
- {1} Un TMap(I, {0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2))"
+lemma "{0,1} \<union> TMap(I,TMap(I,2)) \<union> TMap(I,2) \<subseteq>
+ {1} \<union> TMap(I, {0,1} \<union> TMap(I,TMap(I,2)) \<union> TMap(I,2))"
by (unfold TMap_def, blast)
*)
@@ -68,7 +68,7 @@
(* Lemmas *)
lemma MapQU_lemma:
- "A \<subseteq> univ(X) ==> Pow(A * Union(quniv(X))) \<subseteq> quniv(X)"
+ "A \<subseteq> univ(X) ==> Pow(A * \<Union>(quniv(X))) \<subseteq> quniv(X)"
apply (unfold quniv_def)
apply (rule Pow_mono)
apply (rule subset_trans [OF Sigma_mono product_univ])
@@ -164,7 +164,7 @@
by (unfold map_emp_def, blast)
lemma map_domain_owr:
- "b \<noteq> 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)"
+ "b \<noteq> 0 ==> domain(map_owr(f,a,b)) = {a} \<union> domain(f)"
apply (unfold map_owr_def)
apply (auto simp add: domain_Sigma)
done
--- a/src/ZF/Coind/Static.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Coind/Static.thy Tue Mar 06 16:46:27 2012 +0000
@@ -27,7 +27,7 @@
consts ElabRel :: i
inductive
- domains "ElabRel" <= "TyEnv * Exp * Ty"
+ domains "ElabRel" \<subseteq> "TyEnv * Exp * Ty"
intros
constI [intro!]:
"[| te \<in> TyEnv; c \<in> Const; t \<in> Ty; isof(c,t) |] ==>
--- a/src/ZF/Coind/Types.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Coind/Types.thy Tue Mar 06 16:46:27 2012 +0000
@@ -30,7 +30,7 @@
primrec (*domain of the type environment*)
"te_dom (te_emp) = 0"
- "te_dom (te_owr(te,x,v)) = te_dom(te) Un {x}"
+ "te_dom (te_owr(te,x,v)) = te_dom(te) \<union> {x}"
primrec (*lookup up identifiers in the type environment*)
"te_app (te_emp,x) = 0"
--- a/src/ZF/Coind/Values.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Coind/Values.thy Tue Mar 06 16:46:27 2012 +0000
@@ -80,7 +80,7 @@
(* Equalities for value environments *)
lemma ve_dom_owr [simp]:
- "[| ve \<in> ValEnv; v \<noteq>0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) Un {x}"
+ "[| ve \<in> ValEnv; v \<noteq>0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) \<union> {x}"
apply (erule ValEnvE)
apply (auto simp add: map_domain_owr)
done
--- a/src/ZF/IMP/Equiv.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/IMP/Equiv.thy Tue Mar 06 16:46:27 2012 +0000
@@ -8,7 +8,7 @@
lemma aexp_iff [rule_format]:
"[| a \<in> aexp; sigma: loc -> nat |]
- ==> ALL n. <a,sigma> -a-> n <-> A(a,sigma) = n"
+ ==> \<forall>n. <a,sigma> -a-> n \<longleftrightarrow> A(a,sigma) = n"
apply (erule aexp.induct)
apply (force intro!: evala.intros)+
done
@@ -27,7 +27,7 @@
lemma bexp_iff [rule_format]:
"[| b \<in> bexp; sigma: loc -> nat |]
- ==> ALL w. <b,sigma> -b-> w <-> B(b,sigma) = w"
+ ==> \<forall>w. <b,sigma> -b-> w \<longleftrightarrow> B(b,sigma) = w"
apply (erule bexp.induct)
apply (auto intro!: evalb.intros)
done
--- a/src/ZF/Induct/Acc.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Induct/Acc.thy Tue Mar 06 16:46:27 2012 +0000
@@ -36,7 +36,7 @@
lemma acc_induct [consumes 1, case_names vimage, induct set: acc]:
"[| a \<in> acc(r);
- !!x. [| x \<in> acc(r); \<forall>y. <y,x>:r --> P(y) |] ==> P(x)
+ !!x. [| x \<in> acc(r); \<forall>y. <y,x>:r \<longrightarrow> P(y) |] ==> P(x)
|] ==> P(a)"
by (erule acc.induct) (blast intro: acc.intros)
@@ -55,7 +55,7 @@
apply (blast intro: accI)+
done
-lemma wf_acc_iff: "wf(r) <-> field(r) \<subseteq> acc(r)"
+lemma wf_acc_iff: "wf(r) \<longleftrightarrow> field(r) \<subseteq> acc(r)"
by (rule iffI, erule acc_wfD, erule acc_wfI)
end
--- a/src/ZF/Induct/Binary_Trees.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Induct/Binary_Trees.thy Tue Mar 06 16:46:27 2012 +0000
@@ -20,7 +20,7 @@
lemma Br_neq_left: "l \<in> bt(A) ==> Br(x, l, r) \<noteq> l"
by (induct arbitrary: x r set: bt) auto
-lemma Br_iff: "Br(a, l, r) = Br(a', l', r') <-> a = a' & l = l' & r = r'"
+lemma Br_iff: "Br(a, l, r) = Br(a', l', r') \<longleftrightarrow> a = a' & l = l' & r = r'"
-- "Proving a freeness theorem."
by (fast elim!: bt.free_elims)
--- a/src/ZF/Induct/Comb.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Induct/Comb.thy Tue Mar 06 16:46:27 2012 +0000
@@ -28,7 +28,7 @@
text {*
Inductive definition of contractions, @{text "-1->"} and
- (multi-step) reductions, @{text "--->"}.
+ (multi-step) reductions, @{text "-\<longrightarrow>"}.
*}
consts
@@ -39,8 +39,8 @@
where "p -1-> q == <p,q> \<in> contract"
abbreviation
- contract_multi :: "[i,i] => o" (infixl "--->" 50)
- where "p ---> q == <p,q> \<in> contract^*"
+ contract_multi :: "[i,i] => o" (infixl "-\<longrightarrow>" 50)
+ where "p -\<longrightarrow> q == <p,q> \<in> contract^*"
inductive
domains "contract" \<subseteq> "comb \<times> comb"
@@ -87,14 +87,14 @@
definition
diamond :: "i => o" where
"diamond(r) ==
- \<forall>x y. <x,y>\<in>r --> (\<forall>y'. <x,y'>\<in>r --> (\<exists>z. <y,z>\<in>r & <y',z> \<in> r))"
+ \<forall>x y. <x,y>\<in>r \<longrightarrow> (\<forall>y'. <x,y'>\<in>r \<longrightarrow> (\<exists>z. <y,z>\<in>r & <y',z> \<in> r))"
subsection {* Transitive closure preserves the Church-Rosser property *}
lemma diamond_strip_lemmaD [rule_format]:
"[| diamond(r); <x,y>:r^+ |] ==>
- \<forall>y'. <x,y'>:r --> (\<exists>z. <y',z>: r^+ & <y,z>: r)"
+ \<forall>y'. <x,y'>:r \<longrightarrow> (\<exists>z. <y',z>: r^+ & <y,z>: r)"
apply (unfold diamond_def)
apply (erule trancl_induct)
apply (blast intro: r_into_trancl)
@@ -145,7 +145,7 @@
contract.Ap1 [THEN rtrancl_into_rtrancl2]
contract.Ap2 [THEN rtrancl_into_rtrancl2]
-lemma "p \<in> comb ==> I\<bullet>p ---> p"
+lemma "p \<in> comb ==> I\<bullet>p -\<longrightarrow> p"
-- {* Example only: not used *}
by (unfold I_def) (blast intro: reduction_rls)
@@ -168,7 +168,7 @@
lemma K1_contractD: "K\<bullet>p -1-> r ==> (\<exists>q. r = K\<bullet>q & p -1-> q)"
by auto
-lemma Ap_reduce1: "[| p ---> q; r \<in> comb |] ==> p\<bullet>r ---> q\<bullet>r"
+lemma Ap_reduce1: "[| p -\<longrightarrow> q; r \<in> comb |] ==> p\<bullet>r -\<longrightarrow> q\<bullet>r"
apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
apply (erule rtrancl_induct)
@@ -177,7 +177,7 @@
apply (blast intro: contract_combD2 reduction_rls)
done
-lemma Ap_reduce2: "[| p ---> q; r \<in> comb |] ==> r\<bullet>p ---> r\<bullet>q"
+lemma Ap_reduce2: "[| p -\<longrightarrow> q; r \<in> comb |] ==> r\<bullet>p -\<longrightarrow> r\<bullet>q"
apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
apply (erule rtrancl_induct)
@@ -247,13 +247,13 @@
done
text {*
- \medskip Equivalence of @{prop "p ---> q"} and @{prop "p ===> q"}.
+ \medskip Equivalence of @{prop "p -\<longrightarrow> q"} and @{prop "p ===> q"}.
*}
lemma contract_imp_parcontract: "p-1->q ==> p=1=>q"
by (induct set: contract) auto
-lemma reduce_imp_parreduce: "p--->q ==> p===>q"
+lemma reduce_imp_parreduce: "p-\<longrightarrow>q ==> p===>q"
apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
apply (erule rtrancl_induct)
@@ -262,7 +262,7 @@
trans_trancl [THEN transD])
done
-lemma parcontract_imp_reduce: "p=1=>q ==> p--->q"
+lemma parcontract_imp_reduce: "p=1=>q ==> p-\<longrightarrow>q"
apply (induct set: parcontract)
apply (blast intro: reduction_rls)
apply (blast intro: reduction_rls)
@@ -271,7 +271,7 @@
Ap_reduce1 Ap_reduce2 parcontract_combD1 parcontract_combD2)
done
-lemma parreduce_imp_reduce: "p===>q ==> p--->q"
+lemma parreduce_imp_reduce: "p===>q ==> p-\<longrightarrow>q"
apply (frule trancl_type [THEN subsetD, THEN SigmaD1])
apply (drule field_parcontract_eq [THEN equalityD1, THEN subsetD])
apply (erule trancl_induct, erule parcontract_imp_reduce)
@@ -279,7 +279,7 @@
apply (erule parcontract_imp_reduce)
done
-lemma parreduce_iff_reduce: "p===>q <-> p--->q"
+lemma parreduce_iff_reduce: "p===>q \<longleftrightarrow> p-\<longrightarrow>q"
by (blast intro: parreduce_imp_reduce reduce_imp_parreduce)
end
--- a/src/ZF/Induct/FoldSet.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Induct/FoldSet.thy Tue Mar 06 16:46:27 2012 +0000
@@ -11,10 +11,10 @@
consts fold_set :: "[i, i, [i,i]=>i, i] => i"
inductive
- domains "fold_set(A, B, f,e)" <= "Fin(A)*B"
+ domains "fold_set(A, B, f,e)" \<subseteq> "Fin(A)*B"
intros
emptyI: "e\<in>B ==> <0, e>\<in>fold_set(A, B, f,e)"
- consI: "[| x\<in>A; x \<notin>C; <C,y> : fold_set(A, B,f,e); f(x,y):B |]
+ consI: "[| x\<in>A; x \<notin>C; <C,y> \<in> fold_set(A, B,f,e); f(x,y):B |]
==> <cons(x,C), f(x,y)>\<in>fold_set(A, B, f, e)"
type_intros Fin.intros
@@ -29,12 +29,12 @@
(** foldSet **)
-inductive_cases empty_fold_setE: "<0, x> : fold_set(A, B, f,e)"
-inductive_cases cons_fold_setE: "<cons(x,C), y> : fold_set(A, B, f,e)"
+inductive_cases empty_fold_setE: "<0, x> \<in> fold_set(A, B, f,e)"
+inductive_cases cons_fold_setE: "<cons(x,C), y> \<in> fold_set(A, B, f,e)"
(* add-hoc lemmas *)
-lemma cons_lemma1: "[| x\<notin>C; x\<notin>B |] ==> cons(x,B)=cons(x,C) <-> B = C"
+lemma cons_lemma1: "[| x\<notin>C; x\<notin>B |] ==> cons(x,B)=cons(x,C) \<longleftrightarrow> B = C"
by (auto elim: equalityE)
lemma cons_lemma2: "[| cons(x, B)=cons(y, C); x\<noteq>y; x\<notin>B; y\<notin>C |]
@@ -44,13 +44,13 @@
(* fold_set monotonicity *)
lemma fold_set_mono_lemma:
- "<C, x> : fold_set(A, B, f, e)
- ==> ALL D. A<=D --> <C, x> : fold_set(D, B, f, e)"
+ "<C, x> \<in> fold_set(A, B, f, e)
+ ==> \<forall>D. A<=D \<longrightarrow> <C, x> \<in> fold_set(D, B, f, e)"
apply (erule fold_set.induct)
apply (auto intro: fold_set.intros)
done
-lemma fold_set_mono: " C<=A ==> fold_set(C, B, f, e) <= fold_set(A, B, f, e)"
+lemma fold_set_mono: " C<=A ==> fold_set(C, B, f, e) \<subseteq> fold_set(A, B, f, e)"
apply clarify
apply (frule fold_set.dom_subset [THEN subsetD], clarify)
apply (auto dest: fold_set_mono_lemma)
@@ -64,8 +64,8 @@
(* Proving that fold_set is deterministic *)
lemma Diff1_fold_set:
- "[| <C-{x},y> : fold_set(A, B, f,e); x\<in>C; x\<in>A; f(x, y):B |]
- ==> <C, f(x, y)> : fold_set(A, B, f, e)"
+ "[| <C-{x},y> \<in> fold_set(A, B, f,e); x\<in>C; x\<in>A; f(x, y):B |]
+ ==> <C, f(x, y)> \<in> fold_set(A, B, f, e)"
apply (frule fold_set.dom_subset [THEN subsetD])
apply (erule cons_Diff [THEN subst], rule fold_set.intros, auto)
done
@@ -79,7 +79,7 @@
lemma (in fold_typing) Fin_imp_fold_set:
- "C\<in>Fin(A) ==> (EX x. <C, x> : fold_set(A, B, f,e))"
+ "C\<in>Fin(A) ==> (\<exists>x. <C, x> \<in> fold_set(A, B, f,e))"
apply (erule Fin_induct)
apply (auto dest: fold_set.dom_subset [THEN subsetD]
intro: fold_set.intros etype ftype)
@@ -91,9 +91,9 @@
lemma (in fold_typing) fold_set_determ_lemma [rule_format]:
"n\<in>nat
- ==> ALL C. |C|<n -->
- (ALL x. <C, x> : fold_set(A, B, f,e)-->
- (ALL y. <C, y> : fold_set(A, B, f,e) --> y=x))"
+ ==> \<forall>C. |C|<n \<longrightarrow>
+ (\<forall>x. <C, x> \<in> fold_set(A, B, f,e)\<longrightarrow>
+ (\<forall>y. <C, y> \<in> fold_set(A, B, f,e) \<longrightarrow> y=x))"
apply (erule nat_induct)
apply (auto simp add: le_iff)
apply (erule fold_set.cases)
@@ -110,7 +110,7 @@
apply (drule cons_lemma2, safe)
apply (frule Diff_sing_imp, assumption+)
txt{** LEVEL 17*}
-apply (subgoal_tac "|Ca| le |Cb|")
+apply (subgoal_tac "|Ca| \<le> |Cb|")
prefer 2
apply (rule succ_le_imp_le)
apply (simp add: Fin_into_Finite Finite_imp_succ_cardinal_Diff
@@ -122,7 +122,7 @@
apply (blast dest!: ftype fold_set.dom_subset [THEN subsetD])
apply (subgoal_tac "ya = f(xb,xa) ")
prefer 2 apply (blast del: equalityCE)
-apply (subgoal_tac "<Cb-{x}, xa> : fold_set(A,B,f,e)")
+apply (subgoal_tac "<Cb-{x}, xa> \<in> fold_set(A,B,f,e)")
prefer 2 apply simp
apply (subgoal_tac "yb = f (x, xa) ")
apply (drule_tac [2] C = Cb in Diff1_fold_set, simp_all)
@@ -143,7 +143,7 @@
(** The fold function **)
lemma (in fold_typing) fold_equality:
- "<C,y> : fold_set(A,B,f,e) ==> fold[B](f,e,C) = y"
+ "<C,y> \<in> fold_set(A,B,f,e) ==> fold[B](f,e,C) = y"
apply (unfold fold_def)
apply (frule fold_set.dom_subset [THEN subsetD], clarify)
apply (rule the_equality)
@@ -154,15 +154,15 @@
apply (auto dest: fold_set_lemma intro: ftype etype fcomm)
done
-lemma fold_0 [simp]: "e : B ==> fold[B](f,e,0) = e"
+lemma fold_0 [simp]: "e \<in> B ==> fold[B](f,e,0) = e"
apply (unfold fold_def)
apply (blast elim!: empty_fold_setE intro: fold_set.intros)
done
text{*This result is the right-to-left direction of the subsequent result*}
lemma (in fold_typing) fold_set_imp_cons:
- "[| <C, y> : fold_set(C, B, f, e); C : Fin(A); c : A; c\<notin>C |]
- ==> <cons(c, C), f(c,y)> : fold_set(cons(c, C), B, f, e)"
+ "[| <C, y> \<in> fold_set(C, B, f, e); C \<in> Fin(A); c \<in> A; c\<notin>C |]
+ ==> <cons(c, C), f(c,y)> \<in> fold_set(cons(c, C), B, f, e)"
apply (frule FinD [THEN fold_set_mono, THEN subsetD])
apply assumption
apply (frule fold_set.dom_subset [of A, THEN subsetD])
@@ -170,9 +170,9 @@
done
lemma (in fold_typing) fold_cons_lemma [rule_format]:
-"[| C : Fin(A); c : A; c\<notin>C |]
- ==> <cons(c, C), v> : fold_set(cons(c, C), B, f, e) <->
- (EX y. <C, y> : fold_set(C, B, f, e) & v = f(c, y))"
+"[| C \<in> Fin(A); c \<in> A; c\<notin>C |]
+ ==> <cons(c, C), v> \<in> fold_set(cons(c, C), B, f, e) \<longleftrightarrow>
+ (\<exists>y. <C, y> \<in> fold_set(C, B, f, e) & v = f(c, y))"
apply auto
prefer 2 apply (blast intro: fold_set_imp_cons)
apply (frule_tac Fin.consI [of c, THEN FinD, THEN fold_set_mono, THEN subsetD], assumption+)
@@ -220,7 +220,7 @@
lemma (in fold_typing) fold_nest_Un_Int:
"[| C\<in>Fin(A); D\<in>Fin(A) |]
==> fold[B](f, fold[B](f, e, D), C) =
- fold[B](f, fold[B](f, e, (C Int D)), C Un D)"
+ fold[B](f, fold[B](f, e, (C \<inter> D)), C \<union> D)"
apply (erule Fin_induct, auto)
apply (simp add: Un_cons Int_cons_left fold_type fold_commute
fold_typing.fold_cons [of A _ _ f]
@@ -228,8 +228,8 @@
done
lemma (in fold_typing) fold_nest_Un_disjoint:
- "[| C\<in>Fin(A); D\<in>Fin(A); C Int D = 0 |]
- ==> fold[B](f,e,C Un D) = fold[B](f, fold[B](f,e,D), C)"
+ "[| C\<in>Fin(A); D\<in>Fin(A); C \<inter> D = 0 |]
+ ==> fold[B](f,e,C \<union> D) = fold[B](f, fold[B](f,e,D), C)"
by (simp add: fold_nest_Un_Int)
lemma Finite_cons_lemma: "Finite(C) ==> C\<in>Fin(cons(c, C))"
@@ -245,7 +245,7 @@
lemma setsum_cons [simp]:
"Finite(C) ==>
setsum(g, cons(c,C)) =
- (if c : C then setsum(g,C) else g(c) $+ setsum(g,C))"
+ (if c \<in> C then setsum(g,C) else g(c) $+ setsum(g,C))"
apply (auto simp add: setsum_def Finite_cons cons_absorb)
apply (rule_tac A = "cons (c, C)" in fold_typing.fold_cons)
apply (auto intro: fold_typing.intro Finite_cons_lemma)
@@ -260,7 +260,7 @@
(*The reversed orientation looks more natural, but LOOPS as a simprule!*)
lemma setsum_Un_Int:
"[| Finite(C); Finite(D) |]
- ==> setsum(g, C Un D) $+ setsum(g, C Int D)
+ ==> setsum(g, C \<union> D) $+ setsum(g, C \<inter> D)
= setsum(g, C) $+ setsum(g, D)"
apply (erule Finite_induct)
apply (simp_all add: Int_cons_right cons_absorb Un_cons Int_commute Finite_Un
@@ -274,27 +274,27 @@
done
lemma setsum_Un_disjoint:
- "[| Finite(C); Finite(D); C Int D = 0 |]
- ==> setsum(g, C Un D) = setsum(g, C) $+ setsum(g,D)"
+ "[| Finite(C); Finite(D); C \<inter> D = 0 |]
+ ==> setsum(g, C \<union> D) = setsum(g, C) $+ setsum(g,D)"
apply (subst setsum_Un_Int [symmetric])
-apply (subgoal_tac [3] "Finite (C Un D) ")
+apply (subgoal_tac [3] "Finite (C \<union> D) ")
apply (auto intro: Finite_Un)
done
lemma Finite_RepFun [rule_format (no_asm)]:
- "Finite(I) ==> (\<forall>i\<in>I. Finite(C(i))) --> Finite(RepFun(I, C))"
+ "Finite(I) ==> (\<forall>i\<in>I. Finite(C(i))) \<longrightarrow> Finite(RepFun(I, C))"
apply (erule Finite_induct, auto)
done
lemma setsum_UN_disjoint [rule_format (no_asm)]:
"Finite(I)
- ==> (\<forall>i\<in>I. Finite(C(i))) -->
- (\<forall>i\<in>I. \<forall>j\<in>I. i\<noteq>j --> C(i) Int C(j) = 0) -->
+ ==> (\<forall>i\<in>I. Finite(C(i))) \<longrightarrow>
+ (\<forall>i\<in>I. \<forall>j\<in>I. i\<noteq>j \<longrightarrow> C(i) \<inter> C(j) = 0) \<longrightarrow>
setsum(f, \<Union>i\<in>I. C(i)) = setsum (%i. setsum(f, C(i)), I)"
apply (erule Finite_induct, auto)
apply (subgoal_tac "\<forall>i\<in>B. x \<noteq> i")
prefer 2 apply blast
-apply (subgoal_tac "C (x) Int (\<Union>i\<in>B. C (i)) = 0")
+apply (subgoal_tac "C (x) \<inter> (\<Union>i\<in>B. C (i)) = 0")
prefer 2 apply blast
apply (subgoal_tac "Finite (\<Union>i\<in>B. C (i)) & Finite (C (x)) & Finite (B) ")
apply (simp (no_asm_simp) add: setsum_Un_disjoint)
@@ -332,21 +332,21 @@
lemma setsum_Un:
"[| Finite(A); Finite(B) |]
- ==> setsum(f, A Un B) =
- setsum(f, A) $+ setsum(f, B) $- setsum(f, A Int B)"
+ ==> setsum(f, A \<union> B) =
+ setsum(f, A) $+ setsum(f, B) $- setsum(f, A \<inter> B)"
apply (subst setsum_Un_Int [symmetric], auto)
done
lemma setsum_zneg_or_0 [rule_format (no_asm)]:
- "Finite(A) ==> (\<forall>x\<in>A. g(x) $<= #0) --> setsum(g, A) $<= #0"
+ "Finite(A) ==> (\<forall>x\<in>A. g(x) $<= #0) \<longrightarrow> setsum(g, A) $<= #0"
apply (erule Finite_induct)
apply (auto intro: zneg_or_0_add_zneg_or_0_imp_zneg_or_0)
done
lemma setsum_succD_lemma [rule_format]:
"Finite(A)
- ==> \<forall>n\<in>nat. setsum(f,A) = $# succ(n) --> (\<exists>a\<in>A. #0 $< f(a))"
+ ==> \<forall>n\<in>nat. setsum(f,A) = $# succ(n) \<longrightarrow> (\<exists>a\<in>A. #0 $< f(a))"
apply (erule Finite_induct)
apply (auto simp del: int_of_0 int_of_succ simp add: not_zless_iff_zle int_of_0 [symmetric])
apply (subgoal_tac "setsum (f, B) $<= #0")
@@ -368,7 +368,7 @@
done
lemma g_zpos_imp_setsum_zpos [rule_format]:
- "Finite(A) ==> (\<forall>x\<in>A. #0 $<= g(x)) --> #0 $<= setsum(g, A)"
+ "Finite(A) ==> (\<forall>x\<in>A. #0 $<= g(x)) \<longrightarrow> #0 $<= setsum(g, A)"
apply (erule Finite_induct)
apply (simp (no_asm))
apply (auto intro: zpos_add_zpos_imp_zpos)
@@ -382,13 +382,13 @@
lemma g_zspos_imp_setsum_zspos [rule_format]:
"Finite(A)
- ==> (\<forall>x\<in>A. #0 $< g(x)) --> A \<noteq> 0 --> (#0 $< setsum(g, A))"
+ ==> (\<forall>x\<in>A. #0 $< g(x)) \<longrightarrow> A \<noteq> 0 \<longrightarrow> (#0 $< setsum(g, A))"
apply (erule Finite_induct)
apply (auto intro: zspos_add_zspos_imp_zspos)
done
lemma setsum_Diff [rule_format]:
- "Finite(A) ==> \<forall>a. M(a) = #0 --> setsum(M, A) = setsum(M, A-{a})"
+ "Finite(A) ==> \<forall>a. M(a) = #0 \<longrightarrow> setsum(M, A) = setsum(M, A-{a})"
apply (erule Finite_induct)
apply (simp_all add: Diff_cons_eq Finite_Diff)
done
--- a/src/ZF/Induct/ListN.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Induct/ListN.thy Tue Mar 06 16:46:27 2012 +0000
@@ -24,7 +24,7 @@
lemma list_into_listn: "l \<in> list(A) ==> <length(l),l> \<in> listn(A)"
by (induct set: list) (simp_all add: listn.intros)
-lemma listn_iff: "<n,l> \<in> listn(A) <-> l \<in> list(A) & length(l)=n"
+lemma listn_iff: "<n,l> \<in> listn(A) \<longleftrightarrow> l \<in> list(A) & length(l)=n"
apply (rule iffI)
apply (erule listn.induct)
apply auto
--- a/src/ZF/Induct/Multiset.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Induct/Multiset.thy Tue Mar 06 16:46:27 2012 +0000
@@ -34,8 +34,8 @@
definition
munion :: "[i, i] => i" (infixl "+#" 65) where
- "M +# N == \<lambda>x \<in> mset_of(M) Un mset_of(N).
- if x \<in> mset_of(M) Int mset_of(N) then (M`x) #+ (N`x)
+ "M +# N == \<lambda>x \<in> mset_of(M) \<union> mset_of(N).
+ if x \<in> mset_of(M) \<inter> mset_of(N) then (M`x) #+ (N`x)
else (if x \<in> mset_of(M) then M`x else N`x)"
definition
@@ -74,7 +74,7 @@
"a :# M == a \<in> mset_of(M)"
syntax
- "_MColl" :: "[pttrn, i, o] => i" ("(1{# _ : _./ _#})")
+ "_MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})")
syntax (xsymbols)
"_MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})")
translations
@@ -144,7 +144,7 @@
text{* A useful simplification rule *}
lemma multiset_fun_iff:
- "(f \<in> A -> nat-{0}) <-> f \<in> A->nat&(\<forall>a \<in> A. f`a \<in> nat & 0 < f`a)"
+ "(f \<in> A -> nat-{0}) \<longleftrightarrow> f \<in> A->nat&(\<forall>a \<in> A. f`a \<in> nat & 0 < f`a)"
apply safe
apply (rule_tac [4] B1 = "range (f) " in Pi_mono [THEN subsetD])
apply (auto intro!: Ord_0_lt
@@ -170,10 +170,10 @@
apply (blast intro: Fin_into_Finite)
done
-lemma Mult_iff_multiset: "M \<in> Mult(A) <-> multiset(M) & mset_of(M)\<subseteq>A"
+lemma Mult_iff_multiset: "M \<in> Mult(A) \<longleftrightarrow> multiset(M) & mset_of(M)\<subseteq>A"
by (blast dest: Mult_into_multiset intro: multiset_into_Mult)
-lemma multiset_iff_Mult_mset_of: "multiset(M) <-> M \<in> Mult(mset_of(M))"
+lemma multiset_iff_Mult_mset_of: "multiset(M) \<longleftrightarrow> M \<in> Mult(mset_of(M))"
by (auto simp add: Mult_iff_multiset)
@@ -193,13 +193,13 @@
lemma mset_of_0 [iff]: "mset_of(0) = 0"
by (simp add: mset_of_def)
-lemma mset_is_0_iff: "multiset(M) ==> mset_of(M)=0 <-> M=0"
+lemma mset_is_0_iff: "multiset(M) ==> mset_of(M)=0 \<longleftrightarrow> M=0"
by (auto simp add: multiset_def mset_of_def)
lemma mset_of_single [iff]: "mset_of({#a#}) = {a}"
by (simp add: msingle_def mset_of_def)
-lemma mset_of_union [iff]: "mset_of(M +# N) = mset_of(M) Un mset_of(N)"
+lemma mset_of_union [iff]: "mset_of(M +# N) = mset_of(M) \<union> mset_of(N)"
by (simp add: mset_of_def munion_def)
lemma mset_of_diff [simp]: "mset_of(M)\<subseteq>A ==> mset_of(M -# N) \<subseteq> A"
@@ -210,7 +210,7 @@
lemma msingle_not_0 [iff]: "{#a#} \<noteq> 0 & 0 \<noteq> {#a#}"
by (simp add: msingle_def)
-lemma msingle_eq_iff [iff]: "({#a#} = {#b#}) <-> (a = b)"
+lemma msingle_eq_iff [iff]: "({#a#} = {#b#}) \<longleftrightarrow> (a = b)"
by (simp add: msingle_def)
lemma msingle_multiset [iff,TC]: "multiset({#a#})"
@@ -248,7 +248,7 @@
lemma munion_multiset [simp]: "[| multiset(M); multiset(N) |] ==> multiset(M +# N)"
apply (unfold multiset_def munion_def mset_of_def, auto)
-apply (rule_tac x = "A Un Aa" in exI)
+apply (rule_tac x = "A \<union> Aa" in exI)
apply (auto intro!: lam_type intro: Finite_Un simp add: multiset_fun_iff zero_less_add)
done
@@ -298,7 +298,7 @@
prefer 2 apply (force intro!: lam_type)
apply (subgoal_tac [2] "{x \<in> A \<union> {a} . x \<noteq> a \<and> x \<in> A} = A")
apply (rule fun_extension, auto)
-apply (drule_tac x = "A Un {a}" in spec)
+apply (drule_tac x = "A \<union> {a}" in spec)
apply (simp add: Finite_Un)
apply (force intro!: lam_type)
done
@@ -361,7 +361,7 @@
apply (blast dest!: fun_is_rel)
done
-lemma msize_eq_0_iff: "multiset(M) ==> msize(M)=#0 <-> M=0"
+lemma msize_eq_0_iff: "multiset(M) ==> msize(M)=#0 \<longleftrightarrow> M=0"
apply (simp add: msize_def, auto)
apply (rule_tac P = "setsum (?u,?v) \<noteq> #0" in swap)
apply blast
@@ -378,11 +378,11 @@
done
lemma setsum_mcount_Int:
- "Finite(A) ==> setsum(%a. $# mcount(N, a), A Int mset_of(N))
+ "Finite(A) ==> setsum(%a. $# mcount(N, a), A \<inter> mset_of(N))
= setsum(%a. $# mcount(N, a), A)"
apply (induct rule: Finite_induct)
apply auto
-apply (subgoal_tac "Finite (B Int mset_of (N))")
+apply (subgoal_tac "Finite (B \<inter> mset_of (N))")
prefer 2 apply (blast intro: subset_Finite)
apply (auto simp add: mcount_def Int_cons_left)
done
@@ -412,7 +412,7 @@
done
lemma multiset_equality:
- "[| multiset(M); multiset(N) |]==> M=N<->(\<forall>a. mcount(M, a)=mcount(N, a))"
+ "[| multiset(M); multiset(N) |]==> M=N\<longleftrightarrow>(\<forall>a. mcount(M, a)=mcount(N, a))"
apply auto
apply (subgoal_tac "mset_of (M) = mset_of (N) ")
prefer 2 apply (blast intro: equality_lemma)
@@ -426,28 +426,28 @@
(** More algebraic properties of multisets **)
-lemma munion_eq_0_iff [simp]: "[|multiset(M); multiset(N)|]==>(M +# N =0) <-> (M=0 & N=0)"
+lemma munion_eq_0_iff [simp]: "[|multiset(M); multiset(N)|]==>(M +# N =0) \<longleftrightarrow> (M=0 & N=0)"
by (auto simp add: multiset_equality)
-lemma empty_eq_munion_iff [simp]: "[|multiset(M); multiset(N)|]==>(0=M +# N) <-> (M=0 & N=0)"
+lemma empty_eq_munion_iff [simp]: "[|multiset(M); multiset(N)|]==>(0=M +# N) \<longleftrightarrow> (M=0 & N=0)"
apply (rule iffI, drule sym)
apply (simp_all add: multiset_equality)
done
lemma munion_right_cancel [simp]:
- "[| multiset(M); multiset(N); multiset(K) |]==>(M +# K = N +# K)<->(M=N)"
+ "[| multiset(M); multiset(N); multiset(K) |]==>(M +# K = N +# K)\<longleftrightarrow>(M=N)"
by (auto simp add: multiset_equality)
lemma munion_left_cancel [simp]:
- "[|multiset(K); multiset(M); multiset(N)|] ==>(K +# M = K +# N) <-> (M = N)"
+ "[|multiset(K); multiset(M); multiset(N)|] ==>(K +# M = K +# N) \<longleftrightarrow> (M = N)"
by (auto simp add: multiset_equality)
-lemma nat_add_eq_1_cases: "[| m \<in> nat; n \<in> nat |] ==> (m #+ n = 1) <-> (m=1 & n=0) | (m=0 & n=1)"
+lemma nat_add_eq_1_cases: "[| m \<in> nat; n \<in> nat |] ==> (m #+ n = 1) \<longleftrightarrow> (m=1 & n=0) | (m=0 & n=1)"
by (induct_tac n) auto
lemma munion_is_single:
"[|multiset(M); multiset(N)|]
- ==> (M +# N = {#a#}) <-> (M={#a#} & N=0) | (M = 0 & N = {#a#})"
+ ==> (M +# N = {#a#}) \<longleftrightarrow> (M={#a#} & N=0) | (M = 0 & N = {#a#})"
apply (simp (no_asm_simp) add: multiset_equality)
apply safe
apply simp_all
@@ -467,8 +467,8 @@
done
lemma msingle_is_union: "[| multiset(M); multiset(N) |]
- ==> ({#a#} = M +# N) <-> ({#a#} = M & N=0 | M = 0 & {#a#} = N)"
-apply (subgoal_tac " ({#a#} = M +# N) <-> (M +# N = {#a#}) ")
+ ==> ({#a#} = M +# N) \<longleftrightarrow> ({#a#} = M & N=0 | M = 0 & {#a#} = N)"
+apply (subgoal_tac " ({#a#} = M +# N) \<longleftrightarrow> (M +# N = {#a#}) ")
apply (simp (no_asm_simp) add: munion_is_single)
apply blast
apply (blast dest: sym)
@@ -478,7 +478,7 @@
lemma setsum_decr:
"Finite(A)
- ==> (\<forall>M. multiset(M) -->
+ ==> (\<forall>M. multiset(M) \<longrightarrow>
(\<forall>a \<in> mset_of(M). setsum(%z. $# mcount(M(a:=M`a #- 1), z), A) =
(if a \<in> A then setsum(%z. $# mcount(M, z), A) $- #1
else setsum(%z. $# mcount(M, z), A))))"
@@ -494,7 +494,7 @@
lemma setsum_decr2:
"Finite(A)
- ==> \<forall>M. multiset(M) --> (\<forall>a \<in> mset_of(M).
+ ==> \<forall>M. multiset(M) \<longrightarrow> (\<forall>a \<in> mset_of(M).
setsum(%x. $# mcount(funrestrict(M, mset_of(M)-{a}), x), A) =
(if a \<in> A then setsum(%x. $# mcount(M, x), A) $- $# M`a
else setsum(%x. $# mcount(M, x), A)))"
@@ -514,11 +514,11 @@
apply (simp add: mcount_def mset_of_def)
done
-lemma nat_le_1_cases: "n \<in> nat ==> n le 1 <-> (n=0 | n=1)"
+lemma nat_le_1_cases: "n \<in> nat ==> n \<le> 1 \<longleftrightarrow> (n=0 | n=1)"
by (auto elim: natE)
lemma succ_pred_eq_self: "[| 0<n; n \<in> nat |] ==> succ(n #- 1) = n"
-apply (subgoal_tac "1 le n")
+apply (subgoal_tac "1 \<le> n")
apply (drule add_diff_inverse2, auto)
done
@@ -536,8 +536,8 @@
and prem2: "!!M b. [| multiset(M); b \<in> mset_of(M); P(M) |] ==> P(M(b:= M`b #+ 1))"
shows
"[| n \<in> nat; P(0) |]
- ==> (\<forall>M. multiset(M)-->
- (setsum(%x. $# mcount(M, x), {x \<in> mset_of(M). 0 < M`x}) = $# n) --> P(M))"
+ ==> (\<forall>M. multiset(M)\<longrightarrow>
+ (setsum(%x. $# mcount(M, x), {x \<in> mset_of(M). 0 < M`x}) = $# n) \<longrightarrow> P(M))"
apply (erule nat_induct, clarify)
apply (frule msize_eq_0_iff)
apply (auto simp add: mset_of_def multiset_def multiset_fun_iff msize_def)
@@ -562,9 +562,9 @@
apply (drule mp, drule_tac [2] mp, simp_all)
apply (rule_tac x = A in exI)
apply (auto intro: update_type)
-apply (subgoal_tac "Finite ({x \<in> cons (a, A) . x\<noteq>a-->0<M`x}) ")
+apply (subgoal_tac "Finite ({x \<in> cons (a, A) . x\<noteq>a\<longrightarrow>0<M`x}) ")
prefer 2 apply (blast intro: Collect_subset [THEN subset_Finite] Finite_cons)
-apply (drule_tac A = "{x \<in> cons (a, A) . x\<noteq>a-->0<M`x}" in setsum_decr)
+apply (drule_tac A = "{x \<in> cons (a, A) . x\<noteq>a\<longrightarrow>0<M`x}" in setsum_decr)
apply (drule_tac x = M in spec)
apply (subgoal_tac "multiset (M) ")
prefer 2
@@ -631,7 +631,7 @@
apply (simp add: multiset_def)
apply (auto simp add: munion_def multiset_fun_iff msingle_def)
apply (unfold mset_of_def, simp)
-apply (subgoal_tac "A Un {a} = A")
+apply (subgoal_tac "A \<union> {a} = A")
apply (rule fun_extension)
apply (auto dest: domain_type intro: lam_type update_type)
done
@@ -665,7 +665,7 @@
by (auto simp add: mset_of_def MCollect_def multiset_def funrestrict_def)
lemma MCollect_mem_iff [iff]:
- "x \<in> mset_of({#x \<in> M. P(x)#}) <-> x \<in> mset_of(M) & P(x)"
+ "x \<in> mset_of({#x \<in> M. P(x)#}) \<longleftrightarrow> x \<in> mset_of(M) & P(x)"
by (simp add: MCollect_def mset_of_def)
lemma mcount_MCollect [simp]:
@@ -682,7 +682,7 @@
(* and more algebraic laws on multisets *)
lemma munion_eq_conv_diff: "[| multiset(M); multiset(N) |]
- ==> (M +# {#a#} = N +# {#b#}) <-> (M = N & a = b |
+ ==> (M +# {#a#} = N +# {#b#}) \<longleftrightarrow> (M = N & a = b |
M = N -# {#a#} +# {#b#} & N = M -# {#b#} +# {#a#})"
apply (simp del: mcount_single add: multiset_equality)
apply (rule iffI, erule_tac [2] disjE, erule_tac [3] conjE)
@@ -697,7 +697,7 @@
lemma melem_diff_single:
"multiset(M) ==>
- k \<in> mset_of(M -# {#a#}) <-> (k=a & 1 < mcount(M,a)) | (k\<noteq> a & k \<in> mset_of(M))"
+ k \<in> mset_of(M -# {#a#}) \<longleftrightarrow> (k=a & 1 < mcount(M,a)) | (k\<noteq> a & k \<in> mset_of(M))"
apply (simp add: multiset_def)
apply (simp add: normalize_def mset_of_def msingle_def mdiff_def mcount_def)
apply (auto dest: domain_type intro: zero_less_diff [THEN iffD1]
@@ -709,7 +709,7 @@
lemma munion_eq_conv_exist:
"[| M \<in> Mult(A); N \<in> Mult(A) |]
- ==> (M +# {#a#} = N +# {#b#}) <->
+ ==> (M +# {#a#} = N +# {#b#}) \<longleftrightarrow>
(M=N & a=b | (\<exists>K \<in> Mult(A). M= K +# {#b#} & N=K +# {#a#}))"
by (auto simp add: Mult_iff_multiset melem_diff_single munion_eq_conv_diff)
@@ -728,7 +728,7 @@
by (auto simp add: multirel1_def)
lemma multirel1_iff:
-" <N, M> \<in> multirel1(A, r) <->
+" <N, M> \<in> multirel1(A, r) \<longleftrightarrow>
(\<exists>a. a \<in> A &
(\<exists>M0. M0 \<in> Mult(A) & (\<exists>K. K \<in> Mult(A) &
M=M0 +# {#a#} & N=M0 +# K & (\<forall>b \<in> mset_of(K). <b,a> \<in> r))))"
@@ -789,10 +789,10 @@
lemma acc_0: "acc(0)=0"
by (auto intro!: equalityI dest: acc.dom_subset [THEN subsetD])
-lemma lemma1: "[| \<forall>b \<in> A. <b,a> \<in> r -->
+lemma lemma1: "[| \<forall>b \<in> A. <b,a> \<in> r \<longrightarrow>
(\<forall>M \<in> acc(multirel1(A, r)). M +# {#b#}:acc(multirel1(A, r)));
M0 \<in> acc(multirel1(A, r)); a \<in> A;
- \<forall>M. <M,M0> \<in> multirel1(A, r) --> M +# {#a#} \<in> acc(multirel1(A, r)) |]
+ \<forall>M. <M,M0> \<in> multirel1(A, r) \<longrightarrow> M +# {#a#} \<in> acc(multirel1(A, r)) |]
==> M0 +# {#a#} \<in> acc(multirel1(A, r))"
apply (subgoal_tac "M0 \<in> Mult(A) ")
prefer 2
@@ -822,7 +822,7 @@
done
lemma lemma2: "[| \<forall>b \<in> A. <b,a> \<in> r
- --> (\<forall>M \<in> acc(multirel1(A, r)). M +# {#b#} :acc(multirel1(A, r)));
+ \<longrightarrow> (\<forall>M \<in> acc(multirel1(A, r)). M +# {#b#} :acc(multirel1(A, r)));
M \<in> acc(multirel1(A, r)); a \<in> A|] ==> M +# {#a#} \<in> acc(multirel1(A, r))"
apply (erule acc_induct)
apply (blast intro: lemma1)
@@ -834,8 +834,8 @@
apply (blast intro: lemma2)
done
-lemma lemma4: "multiset(M) ==> mset_of(M)\<subseteq>A -->
- wf[A](r) --> M \<in> field(multirel1(A, r)) --> M \<in> acc(multirel1(A, r))"
+lemma lemma4: "multiset(M) ==> mset_of(M)\<subseteq>A \<longrightarrow>
+ wf[A](r) \<longrightarrow> M \<in> field(multirel1(A, r)) \<longrightarrow> M \<in> acc(multirel1(A, r))"
apply (erule multiset_induct)
(* proving the base case *)
apply clarify
@@ -899,7 +899,7 @@
(* Equivalence of multirel with the usual (closure-free) def *)
-lemma add_diff_eq: "k \<in> nat ==> 0 < k --> n #+ k #- 1 = n #+ (k #- 1)"
+lemma add_diff_eq: "k \<in> nat ==> 0 < k \<longrightarrow> n #+ k #- 1 = n #+ (k #- 1)"
by (erule nat_induct, auto)
lemma mdiff_union_single_conv: "[|a \<in> mset_of(J); multiset(I); multiset(J) |]
@@ -910,14 +910,14 @@
apply (auto dest: domain_type simp add: add_diff_eq)
done
-lemma diff_add_commute: "[| n le m; m \<in> nat; n \<in> nat; k \<in> nat |] ==> m #- n #+ k = m #+ k #- n"
+lemma diff_add_commute: "[| n \<le> m; m \<in> nat; n \<in> nat; k \<in> nat |] ==> m #- n #+ k = m #+ k #- n"
by (auto simp add: le_iff less_iff_succ_add)
(* One direction *)
lemma multirel_implies_one_step:
"<M,N> \<in> multirel(A, r) ==>
- trans[A](r) -->
+ trans[A](r) \<longrightarrow>
(\<exists>I J K.
I \<in> Mult(A) & J \<in> Mult(A) & K \<in> Mult(A) &
N = I +# J & M = I +# K & J \<noteq> 0 &
@@ -986,7 +986,7 @@
(\<forall>I J K.
I \<in> Mult(A) & J \<in> Mult(A) & K \<in> Mult(A) &
(msize(J) = $# n & J \<noteq>0 & (\<forall>k \<in> mset_of(K). \<exists>j \<in> mset_of(J). <k, j> \<in> r))
- --> <I +# K, I +# J> \<in> multirel(A, r))"
+ \<longrightarrow> <I +# K, I +# J> \<in> multirel(A, r))"
apply (simp add: Mult_iff_multiset)
apply (erule nat_induct, clarify)
apply (drule_tac M = J in msize_eq_0_iff, auto)
@@ -1039,7 +1039,7 @@
(*irreflexivity*)
lemma multirel_irrefl_lemma:
- "Finite(A) ==> part_ord(A, r) --> (\<forall>x \<in> A. \<exists>y \<in> A. <x,y> \<in> r) -->A=0"
+ "Finite(A) ==> part_ord(A, r) \<longrightarrow> (\<forall>x \<in> A. \<exists>y \<in> A. <x,y> \<in> r) \<longrightarrow>A=0"
apply (erule Finite_induct)
apply (auto dest: subset_consI [THEN [2] part_ord_subset])
apply (auto simp add: part_ord_def irrefl_def)
@@ -1152,7 +1152,7 @@
lemma munion_omultiset [simp]: "[| omultiset(M); omultiset(N) |] ==> omultiset(M +# N)"
apply (simp add: omultiset_def, clarify)
-apply (rule_tac x = "i Un ia" in exI)
+apply (rule_tac x = "i \<union> ia" in exI)
apply (simp add: Mult_iff_multiset Ord_Un Un_subset_iff)
apply (blast intro: field_Memrel_mono)
done
@@ -1173,7 +1173,7 @@
apply (drule_tac i = x in ltI [THEN lt_irrefl], auto)
done
-lemma trans_iff_trans_on: "trans(r) <-> trans[field(r)](r)"
+lemma trans_iff_trans_on: "trans(r) \<longleftrightarrow> trans[field(r)](r)"
by (simp add: trans_on_def trans_def, auto)
lemma part_ord_Memrel: "Ord(i) ==>part_ord(field(Memrel(i)), Memrel(i))"
@@ -1204,7 +1204,7 @@
(*transitivity*)
lemma mless_trans: "[| K <# M; M <# N |] ==> K <# N"
apply (simp add: mless_def, clarify)
-apply (rule_tac x = "i Un ia" in exI)
+apply (rule_tac x = "i \<union> ia" in exI)
apply (blast dest: multirel_Memrel_mono [OF Un_upper1 Un_upper1, THEN subsetD]
multirel_Memrel_mono [OF Un_upper2 Un_upper2, THEN subsetD]
intro: multirel_trans Ord_Un)
@@ -1236,14 +1236,14 @@
apply (blast intro: mless_trans)
done
-lemma mless_le_iff: "M <# N <-> (M <#= N & M \<noteq> N)"
+lemma mless_le_iff: "M <# N \<longleftrightarrow> (M <#= N & M \<noteq> N)"
by (simp add: mle_def, auto)
(** Monotonicity of mless **)
lemma munion_less_mono2: "[| M <# N; omultiset(K) |] ==> K +# M <# K +# N"
apply (simp add: mless_def omultiset_def, clarify)
-apply (rule_tac x = "i Un ia" in exI)
+apply (rule_tac x = "i \<union> ia" in exI)
apply (simp add: Mult_iff_multiset Ord_Un Un_subset_iff)
apply (rule munion_multirel_mono2)
apply (blast intro: multirel_Memrel_mono [THEN subsetD])
--- a/src/ZF/Induct/Mutil.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Induct/Mutil.thy Tue Mar 06 16:46:27 2012 +0000
@@ -24,10 +24,10 @@
type_intros empty_subsetI cons_subsetI PowI SigmaI nat_succI
inductive
- domains "tiling(A)" \<subseteq> "Pow(Union(A))"
+ domains "tiling(A)" \<subseteq> "Pow(\<Union>(A))"
intros
empty: "0 \<in> tiling(A)"
- Un: "[| a \<in> A; t \<in> tiling(A); a Int t = 0 |] ==> a Un t \<in> tiling(A)"
+ Un: "[| a \<in> A; t \<in> tiling(A); a \<inter> t = 0 |] ==> a \<union> t \<in> tiling(A)"
type_intros empty_subsetI Union_upper Un_least PowI
type_elims PowD [elim_format]
@@ -38,7 +38,7 @@
subsection {* Basic properties of evnodd *}
-lemma evnodd_iff: "<i,j>: evnodd(A,b) <-> <i,j>: A & (i#+j) mod 2 = b"
+lemma evnodd_iff: "<i,j>: evnodd(A,b) \<longleftrightarrow> <i,j>: A & (i#+j) mod 2 = b"
by (unfold evnodd_def) blast
lemma evnodd_subset: "evnodd(A, b) \<subseteq> A"
@@ -47,7 +47,7 @@
lemma Finite_evnodd: "Finite(X) ==> Finite(evnodd(X,b))"
by (rule lepoll_Finite, rule subset_imp_lepoll, rule evnodd_subset)
-lemma evnodd_Un: "evnodd(A Un B, b) = evnodd(A,b) Un evnodd(B,b)"
+lemma evnodd_Un: "evnodd(A \<union> B, b) = evnodd(A,b) \<union> evnodd(B,b)"
by (simp add: evnodd_def Collect_Un)
lemma evnodd_Diff: "evnodd(A - B, b) = evnodd(A,b) - evnodd(B,b)"
@@ -83,7 +83,7 @@
text {* The union of two disjoint tilings is a tiling *}
lemma tiling_UnI:
- "t \<in> tiling(A) ==> u \<in> tiling(A) ==> t Int u = 0 ==> t Un u \<in> tiling(A)"
+ "t \<in> tiling(A) ==> u \<in> tiling(A) ==> t \<inter> u = 0 ==> t \<union> u \<in> tiling(A)"
apply (induct set: tiling)
apply (simp add: tiling.intros)
apply (simp add: Un_assoc subset_empty_iff [THEN iff_sym])
@@ -108,7 +108,7 @@
apply simp
apply assumption
apply safe
- apply (subgoal_tac "\<forall>p b. p \<in> evnodd (a,b) --> p\<notin>evnodd (t,b)")
+ apply (subgoal_tac "\<forall>p b. p \<in> evnodd (a,b) \<longrightarrow> p\<notin>evnodd (t,b)")
apply (simp add: evnodd_Un Un_cons tiling_domino_Finite
evnodd_subset [THEN subset_Finite] Finite_imp_cardinal_cons)
apply (blast dest!: evnodd_subset [THEN subsetD] elim: equalityE)
@@ -123,7 +123,7 @@
prefer 2 apply assumption
apply (rename_tac n')
apply (subgoal_tac (*seems the easiest way of turning one to the other*)
- "{i}*{succ (n'#+n') } Un {i}*{n'#+n'} =
+ "{i}*{succ (n'#+n') } \<union> {i}*{n'#+n'} =
{<i,n'#+n'>, <i,succ (n'#+n') >}")
prefer 2 apply blast
apply (simp add: domino.horiz)
--- a/src/ZF/Induct/PropLog.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Induct/PropLog.thy Tue Mar 06 16:46:27 2012 +0000
@@ -68,13 +68,13 @@
"is_true(p,t) == is_true_fun(p,t) = 1"
-- {* this definition is required since predicates can't be recursive *}
-lemma is_true_Fls [simp]: "is_true(Fls,t) <-> False"
+lemma is_true_Fls [simp]: "is_true(Fls,t) \<longleftrightarrow> False"
by (simp add: is_true_def)
-lemma is_true_Var [simp]: "is_true(#v,t) <-> v \<in> t"
+lemma is_true_Var [simp]: "is_true(#v,t) \<longleftrightarrow> v \<in> t"
by (simp add: is_true_def)
-lemma is_true_Imp [simp]: "is_true(p=>q,t) <-> (is_true(p,t)-->is_true(q,t))"
+lemma is_true_Imp [simp]: "is_true(p=>q,t) \<longleftrightarrow> (is_true(p,t)\<longrightarrow>is_true(q,t))"
by (simp add: is_true_def)
@@ -87,7 +87,7 @@
definition
logcon :: "[i,i] => o" (infixl "|=" 50) where
- "H |= p == \<forall>t. (\<forall>q \<in> H. is_true(q,t)) --> is_true(p,t)"
+ "H |= p == \<forall>t. (\<forall>q \<in> H. is_true(q,t)) \<longrightarrow> is_true(p,t)"
text {*
@@ -335,7 +335,7 @@
apply (blast intro: propn_Is)
done
-theorem thms_iff: "H \<in> Fin(propn) ==> H |- p <-> H |= p \<and> p \<in> propn"
+theorem thms_iff: "H \<in> Fin(propn) ==> H |- p \<longleftrightarrow> H |= p \<and> p \<in> propn"
by (blast intro: soundness completeness thms_in_pl)
end
--- a/src/ZF/ex/CoUnit.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/ex/CoUnit.thy Tue Mar 06 16:46:27 2012 +0000
@@ -27,7 +27,7 @@
inductive_cases ConE: "Con(x) \<in> counit"
-- {* USELESS because folding on @{term "Con(xa) == xa"} fails. *}
-lemma Con_iff: "Con(x) = Con(y) <-> x = y"
+lemma Con_iff: "Con(x) = Con(y) \<longleftrightarrow> x = y"
-- {* Proving freeness results. *}
by (auto elim!: counit.free_elims)
@@ -55,7 +55,7 @@
inductive_cases Con2E: "Con2(x, y) \<in> counit2"
-lemma Con2_iff: "Con2(x, y) = Con2(x', y') <-> x = x' & y = y'"
+lemma Con2_iff: "Con2(x, y) = Con2(x', y') \<longleftrightarrow> x = x' & y = y'"
-- {* Proving freeness results. *}
by (fast elim!: counit2.free_elims)
@@ -73,7 +73,7 @@
done
lemma counit2_Int_Vset_subset [rule_format]:
- "Ord(i) ==> \<forall>x y. x \<in> counit2 --> y \<in> counit2 --> x Int Vset(i) \<subseteq> y"
+ "Ord(i) ==> \<forall>x y. x \<in> counit2 \<longrightarrow> y \<in> counit2 \<longrightarrow> x \<inter> Vset(i) \<subseteq> y"
-- {* Lemma for proving finality. *}
apply (erule trans_induct)
apply (tactic "safe_tac (put_claset subset_cs @{context})")
--- a/src/ZF/ex/Commutation.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/ex/Commutation.thy Tue Mar 06 16:46:27 2012 +0000
@@ -10,7 +10,7 @@
definition
square :: "[i, i, i, i] => o" where
"square(r,s,t,u) ==
- (\<forall>a b. <a,b> \<in> r --> (\<forall>c. <a, c> \<in> s --> (\<exists>x. <b,x> \<in> t & <c,x> \<in> u)))"
+ (\<forall>a b. <a,b> \<in> r \<longrightarrow> (\<forall>c. <a, c> \<in> s \<longrightarrow> (\<exists>x. <b,x> \<in> t & <c,x> \<in> u)))"
definition
commute :: "[i, i] => o" where
@@ -26,7 +26,7 @@
definition
Church_Rosser :: "i => o" where
- "Church_Rosser(r) == (\<forall>x y. <x,y> \<in> (r Un converse(r))^* -->
+ "Church_Rosser(r) == (\<forall>x y. <x,y> \<in> (r \<union> converse(r))^* \<longrightarrow>
(\<exists>z. <x,z> \<in> r^* & <y,z> \<in> r^*))"
definition
@@ -79,11 +79,11 @@
apply (simp_all add: rtrancl_field)
done
-lemma commute_Un: "[| commute(r,t); commute(s,t) |] ==> commute(r Un s, t)"
+lemma commute_Un: "[| commute(r,t); commute(s,t) |] ==> commute(r \<union> s, t)"
unfolding commute_def square_def by blast
lemma diamond_Un:
- "[| diamond(r); diamond(s); commute(r, s) |] ==> diamond(r Un s)"
+ "[| diamond(r); diamond(s); commute(r, s) |] ==> diamond(r \<union> s)"
unfolding diamond_def by (blast intro: commute_Un commute_sym)
lemma diamond_confluent:
@@ -94,7 +94,7 @@
lemma confluent_Un:
"[| confluent(r); confluent(s); commute(r^*, s^*);
- relation(r); relation(s) |] ==> confluent(r Un s)"
+ relation(r); relation(s) |] ==> confluent(r \<union> s)"
apply (unfold confluent_def)
apply (rule rtrancl_Un_rtrancl [THEN subst], auto)
apply (blast dest: diamond_Un intro: diamond_confluent [THEN confluentD])
@@ -136,7 +136,7 @@
done
-lemma Church_Rosser: "Church_Rosser(r) <-> confluent(r)"
+lemma Church_Rosser: "Church_Rosser(r) \<longleftrightarrow> confluent(r)"
by (blast intro: Church_Rosser1 Church_Rosser2)
end
--- a/src/ZF/ex/Group.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/ex/Group.thy Tue Mar 06 16:46:27 2012 +0000
@@ -105,7 +105,7 @@
proof -
have l_cancel [simp]:
"\<And>x y z. \<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> \<Longrightarrow>
- (x \<cdot> y = x \<cdot> z) <-> (y = z)"
+ (x \<cdot> y = x \<cdot> z) \<longleftrightarrow> (y = z)"
proof
fix x y z
assume G: "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)"
@@ -178,7 +178,7 @@
lemma (in group) l_cancel [simp]:
assumes "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)"
- shows "(x \<cdot> y = x \<cdot> z) <-> (y = z)"
+ shows "(x \<cdot> y = x \<cdot> z) \<longleftrightarrow> (y = z)"
proof
assume eq: "x \<cdot> y = x \<cdot> z"
hence "(inv x \<cdot> x) \<cdot> y = (inv x \<cdot> x) \<cdot> z"
@@ -191,7 +191,7 @@
lemma (in group) r_cancel [simp]:
assumes "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)"
- shows "(y \<cdot> x = z \<cdot> x) <-> (y = z)"
+ shows "(y \<cdot> x = z \<cdot> x) \<longleftrightarrow> (y = z)"
proof
assume eq: "y \<cdot> x = z \<cdot> x"
then have "y \<cdot> (x \<cdot> inv x) = z \<cdot> (x \<cdot> inv x)"
@@ -679,9 +679,9 @@
text{*Alternative characterization of normal subgroups*}
lemma (in group) normal_inv_iff:
- "(N \<lhd> G) <->
+ "(N \<lhd> G) \<longleftrightarrow>
(subgroup(N,G) & (\<forall>x \<in> carrier(G). \<forall>h \<in> N. x \<cdot> h \<cdot> (inv x) \<in> N))"
- (is "_ <-> ?rhs")
+ (is "_ \<longleftrightarrow> ?rhs")
proof
assume N: "N \<lhd> G"
show ?rhs
--- a/src/ZF/ex/LList.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/ex/LList.thy Tue Mar 06 16:46:27 2012 +0000
@@ -30,7 +30,7 @@
standard pairs work just as well. To use variant pairs, must change prefix
a q/Q to the Sigma, Pair and converse rules.*)
coinductive
- domains "lleq(A)" <= "llist(A) * llist(A)"
+ domains "lleq(A)" \<subseteq> "llist(A) * llist(A)"
intros
LNil: "<LNil, LNil> \<in> lleq(A)"
LCons: "[| a \<in> A; <l,l'> \<in> lleq(A) |]
@@ -74,7 +74,7 @@
inductive_cases LConsE: "LCons(a,l) \<in> llist(A)"
(*Proving freeness results*)
-lemma LCons_iff: "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'"
+lemma LCons_iff: "LCons(a,l)=LCons(a',l') \<longleftrightarrow> a=a' & l=l'"
by auto
lemma LNil_LCons_iff: "~ LNil=LCons(a,l)"
@@ -107,7 +107,7 @@
declare Ord_in_Ord [elim!]
lemma llist_quniv_lemma [rule_format]:
- "Ord(i) ==> \<forall>l \<in> llist(quniv(A)). l Int Vset(i) \<subseteq> univ(eclose(A))"
+ "Ord(i) ==> \<forall>l \<in> llist(quniv(A)). l \<inter> Vset(i) \<subseteq> univ(eclose(A))"
apply (erule trans_induct)
apply (rule ballI)
apply (erule llist.cases)
@@ -135,7 +135,7 @@
(*Lemma for proving finality. Unfold the lazy list; use induction hypothesis*)
lemma lleq_Int_Vset_subset [rule_format]:
- "Ord(i) ==> \<forall>l l'. <l,l'> \<in> lleq(A) --> l Int Vset(i) \<subseteq> l'"
+ "Ord(i) ==> \<forall>l l'. <l,l'> \<in> lleq(A) \<longrightarrow> l \<inter> Vset(i) \<subseteq> l'"
apply (erule trans_induct)
apply (intro allI impI)
apply (erule lleq.cases)
@@ -200,7 +200,7 @@
flip_LCons [simp]
not_type [simp]
-lemma bool_Int_subset_univ: "b \<in> bool ==> b Int X \<subseteq> univ(eclose(A))"
+lemma bool_Int_subset_univ: "b \<in> bool ==> b \<inter> X \<subseteq> univ(eclose(A))"
by (fast intro: Int_lower1 [THEN subset_trans] elim!: boolE)
declare not_type [intro!]
@@ -209,7 +209,7 @@
(*Reasoning borrowed from lleq.ML; a similar proof works for all
"productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
lemma flip_llist_quniv_lemma [rule_format]:
- "Ord(i) ==> \<forall>l \<in> llist(bool). flip(l) Int Vset(i) \<subseteq> univ(eclose(bool))"
+ "Ord(i) ==> \<forall>l \<in> llist(bool). flip(l) \<inter> Vset(i) \<subseteq> univ(eclose(bool))"
apply (erule trans_induct)
apply (rule ballI)
apply (erule llist.cases, simp_all)
--- a/src/ZF/ex/Limit.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/ex/Limit.thy Tue Mar 06 16:46:27 2012 +0000
@@ -7,13 +7,13 @@
The following paper comments on the formalization:
"A Comparison of HOL-ST and Isabelle/ZF" by Sten Agerholm
-In Proceedings of the First Isabelle Users Workshop, Technical
+In Proceedings of the First Isabelle Users Workshop, Technical
Report No. 379, University of Cambridge Computer Laboratory, 1995.
This is a condensed version of:
"A Comparison of HOL-ST and Isabelle/ZF" by Sten Agerholm
-Technical Report No. 369, University of Cambridge Computer
+Technical Report No. 369, University of Cambridge Computer
Laboratory, 1995.
*)
@@ -32,8 +32,8 @@
"po(D) ==
(\<forall>x \<in> set(D). rel(D,x,x)) &
(\<forall>x \<in> set(D). \<forall>y \<in> set(D). \<forall>z \<in> set(D).
- rel(D,x,y) --> rel(D,y,z) --> rel(D,x,z)) &
- (\<forall>x \<in> set(D). \<forall>y \<in> set(D). rel(D,x,y) --> rel(D,y,x) --> x = y)"
+ rel(D,x,y) \<longrightarrow> rel(D,y,z) \<longrightarrow> rel(D,x,z)) &
+ (\<forall>x \<in> set(D). \<forall>y \<in> set(D). rel(D,x,y) \<longrightarrow> rel(D,y,x) \<longrightarrow> x = y)"
definition
chain :: "[i,i]=>o" where
@@ -46,7 +46,7 @@
definition
islub :: "[i,i,i]=>o" where
- "islub(D,X,x) == isub(D,X,x) & (\<forall>y. isub(D,X,y) --> rel(D,x,y))"
+ "islub(D,X,x) == isub(D,X,x) & (\<forall>y. isub(D,X,y) \<longrightarrow> rel(D,x,y))"
definition
lub :: "[i,i]=>i" where
@@ -54,7 +54,7 @@
definition
cpo :: "i=>o" where
- "cpo(D) == po(D) & (\<forall>X. chain(D,X) --> (\<exists>x. islub(D,X,x)))"
+ "cpo(D) == po(D) & (\<forall>X. chain(D,X) \<longrightarrow> (\<exists>x. islub(D,X,x)))"
definition
pcpo :: "i=>o" where
@@ -68,13 +68,13 @@
mono :: "[i,i]=>i" where
"mono(D,E) ==
{f \<in> set(D)->set(E).
- \<forall>x \<in> set(D). \<forall>y \<in> set(D). rel(D,x,y) --> rel(E,f`x,f`y)}"
+ \<forall>x \<in> set(D). \<forall>y \<in> set(D). rel(D,x,y) \<longrightarrow> rel(E,f`x,f`y)}"
definition
cont :: "[i,i]=>i" where
"cont(D,E) ==
{f \<in> mono(D,E).
- \<forall>X. chain(D,X) --> f`(lub(D,X)) = lub(E,\<lambda>n \<in> nat. f`(X`n))}"
+ \<forall>X. chain(D,X) \<longrightarrow> f`(lub(D,X)) = lub(E,\<lambda>n \<in> nat. f`(X`n))}"
definition
cf :: "[i,i]=>i" where
@@ -134,8 +134,8 @@
subcpo :: "[i,i]=>o" where
"subcpo(D,E) ==
set(D) \<subseteq> set(E) &
- (\<forall>x \<in> set(D). \<forall>y \<in> set(D). rel(D,x,y) <-> rel(E,x,y)) &
- (\<forall>X. chain(D,X) --> lub(E,X):set(D))"
+ (\<forall>x \<in> set(D). \<forall>y \<in> set(D). rel(D,x,y) \<longleftrightarrow> rel(E,x,y)) &
+ (\<forall>X. chain(D,X) \<longrightarrow> lub(E,X):set(D))"
definition
subpcpo :: "[i,i]=>o" where
@@ -154,13 +154,13 @@
definition
e_less :: "[i,i,i,i]=>i" where
- (* Valid for m le n only. *)
+ (* Valid for m \<le> n only. *)
"e_less(DD,ee,m,n) == rec(n#-m,id(set(DD`m)),%x y. ee`(m#+x) O y)"
definition
e_gr :: "[i,i,i,i]=>i" where
- (* Valid for n le m only. *)
+ (* Valid for n \<le> m only. *)
"e_gr(DD,ee,m,n) ==
rec(m#-n,id(set(DD`n)),
%x y. y O Rp(DD`(n#+x),DD`(succ(n#+x)),ee`(n#+x)))"
@@ -168,7 +168,7 @@
definition
eps :: "[i,i,i,i]=>i" where
- "eps(DD,ee,m,n) == if(m le n,e_less(DD,ee,m,n),e_gr(DD,ee,m,n))"
+ "eps(DD,ee,m,n) == if(m \<le> n,e_less(DD,ee,m,n),e_gr(DD,ee,m,n))"
definition
rho_emb :: "[i,i,i]=>i" where
@@ -182,7 +182,7 @@
commute :: "[i,i,i,i=>i]=>o" where
"commute(DD,ee,E,r) ==
(\<forall>n \<in> nat. emb(DD`n,E,r(n))) &
- (\<forall>m \<in> nat. \<forall>n \<in> nat. m le n --> r(n) O eps(DD,ee,m,n) = r(m))"
+ (\<forall>m \<in> nat. \<forall>n \<in> nat. m \<le> n \<longrightarrow> r(n) O eps(DD,ee,m,n) = r(m))"
definition
mediating :: "[i,i,i=>i,i=>i,i]=>o" where
@@ -224,7 +224,7 @@
"[| !!x. x \<in> set(D) ==> rel(D,x,x);
!!x y z. [| rel(D,x,y); rel(D,y,z); x \<in> set(D); y \<in> set(D); z \<in> set(D)|]
==> rel(D,x,z);
- !!x y. [| rel(D,x,y); rel(D,y,x); x \<in> set(D); y \<in> set(D)|] ==> x=y |]
+ !!x y. [| rel(D,x,y); rel(D,y,x); x \<in> set(D); y \<in> set(D)|] ==> x=y |]
==> po(D)"
by (unfold po_def, blast)
@@ -323,7 +323,7 @@
done
lemma chain_rel_gen:
- "[|n le m; chain(D,X); cpo(D); m \<in> nat|] ==> rel(D,X`n,X`m)"
+ "[|n \<le> m; chain(D,X); cpo(D); m \<in> nat|] ==> rel(D,X`n,X`m)"
apply (frule lt_nat_in_nat, erule nat_succI)
apply (erule rev_mp) (*prepare the induction*)
apply (induct_tac m)
@@ -382,14 +382,14 @@
(*----------------------------------------------------------------------*)
lemma isub_suffix:
- "[| chain(D,X); cpo(D) |] ==> isub(D,suffix(X,n),x) <-> isub(D,X,x)"
+ "[| chain(D,X); cpo(D) |] ==> isub(D,suffix(X,n),x) \<longleftrightarrow> isub(D,X,x)"
apply (simp add: isub_def suffix_def, safe)
apply (drule_tac x = na in bspec)
apply (auto intro: cpo_trans chain_rel_gen_add)
done
lemma islub_suffix:
- "[|chain(D,X); cpo(D)|] ==> islub(D,suffix(X,n),x) <-> islub(D,X,x)"
+ "[|chain(D,X); cpo(D)|] ==> islub(D,suffix(X,n),x) \<longleftrightarrow> islub(D,X,x)"
by (simp add: islub_def isub_suffix)
lemma lub_suffix:
@@ -401,7 +401,7 @@
(*----------------------------------------------------------------------*)
lemma dominateI:
- "[| !!m. m \<in> nat ==> n(m):nat; !!m. m \<in> nat ==> rel(D,X`m,Y`n(m))|]
+ "[| !!m. m \<in> nat ==> n(m):nat; !!m. m \<in> nat ==> rel(D,X`m,Y`n(m))|]
==> dominate(D,X,Y)"
by (simp add: dominate_def, blast)
@@ -426,7 +426,7 @@
lemma dominate_islub_eq:
"[|dominate(D,X,Y); subchain(Y,X); islub(D,X,x); islub(D,Y,y); cpo(D);
X \<in> nat->set(D); Y \<in> nat->set(D)|] ==> x = y"
-by (blast intro: cpo_antisym dominate_islub islub_least subchain_isub
+by (blast intro: cpo_antisym dominate_islub islub_least subchain_isub
islub_isub islub_in)
@@ -488,19 +488,19 @@
shows "matrix(D,M)"
proof -
{
- fix n m assume "n : nat" "m : nat"
+ fix n m assume "n \<in> nat" "m \<in> nat"
with chain_rel [OF yprem]
have "rel(D, M ` n ` m, M ` succ(n) ` m)" by simp
} note rel_succ = this
show "matrix(D,M)"
proof (simp add: matrix_def Mfun rel_succ, intro conjI ballI)
- fix n m assume n: "n : nat" and m: "m : nat"
+ fix n m assume n: "n \<in> nat" and m: "m \<in> nat"
thus "rel(D, M ` n ` m, M ` n ` succ(m))"
by (simp add: chain_rel xprem)
next
- fix n m assume n: "n : nat" and m: "m : nat"
+ fix n m assume n: "n \<in> nat" and m: "m \<in> nat"
thus "rel(D, M ` n ` m, M ` succ(n) ` succ(m))"
- by (rule cpo_trans [OF cpoD rel_succ],
+ by (rule cpo_trans [OF cpoD rel_succ],
simp_all add: chain_fun [THEN apply_type] xprem)
qed
qed
@@ -511,31 +511,31 @@
by simp
lemma isub_lemma:
- "[|isub(D, \<lambda>n \<in> nat. M`n`n, y); matrix(D,M); cpo(D)|]
+ "[|isub(D, \<lambda>n \<in> nat. M`n`n, y); matrix(D,M); cpo(D)|]
==> isub(D, \<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m), y)"
proof (simp add: isub_def, safe)
fix n
- assume DM: "matrix(D, M)" and D: "cpo(D)" and n: "n \<in> nat" and y: "y \<in> set(D)"
+ assume DM: "matrix(D, M)" and D: "cpo(D)" and n: "n \<in> nat" and y: "y \<in> set(D)"
and rel: "\<forall>n\<in>nat. rel(D, M ` n ` n, y)"
have "rel(D, lub(D, M ` n), y)"
proof (rule matrix_chain_left [THEN cpo_lub, THEN islub_least], simp_all add: n D DM)
- show "isub(D, M ` n, y)"
+ show "isub(D, M ` n, y)"
proof (unfold isub_def, intro conjI ballI y)
fix k assume k: "k \<in> nat"
show "rel(D, M ` n ` k, y)"
- proof (cases "n le k")
- case True
- hence yy: "rel(D, M`n`k, M`k`k)"
- by (blast intro: lemma2 n k y DM D chain_rel_gen matrix_chain_right)
+ proof (cases "n \<le> k")
+ case True
+ hence yy: "rel(D, M`n`k, M`k`k)"
+ by (blast intro: lemma2 n k y DM D chain_rel_gen matrix_chain_right)
show "?thesis"
- by (rule cpo_trans [OF D yy],
+ by (rule cpo_trans [OF D yy],
simp_all add: k rel n y DM matrix_in)
next
case False
- hence le: "k le n"
- by (blast intro: not_le_iff_lt [THEN iffD1, THEN leI] nat_into_Ord n k)
+ hence le: "k \<le> n"
+ by (blast intro: not_le_iff_lt [THEN iffD1, THEN leI] nat_into_Ord n k)
show "?thesis"
- by (rule cpo_trans [OF D chain_rel_gen [OF le]],
+ by (rule cpo_trans [OF D chain_rel_gen [OF le]],
simp_all add: n y k rel DM D matrix_chain_left)
qed
qed
@@ -550,7 +550,7 @@
proof (simp add: chain_def, intro conjI ballI)
assume "matrix(D, M)" "cpo(D)"
thus "(\<lambda>x\<in>nat. lub(D, Lambda(nat, op `(M ` x)))) \<in> nat \<rightarrow> set(D)"
- by (force intro: islub_in cpo_lub chainI lam_type matrix_in matrix_rel_0_1)
+ by (force intro: islub_in cpo_lub chainI lam_type matrix_in matrix_rel_0_1)
next
fix n
assume DD: "matrix(D, M)" "cpo(D)" "n \<in> nat"
@@ -558,24 +558,24 @@
by (force simp add: dominate_def intro: matrix_rel_1_0)
with DD show "rel(D, lub(D, Lambda(nat, op `(M ` n))),
lub(D, Lambda(nat, op `(M ` succ(n)))))"
- by (simp add: matrix_chain_left [THEN chain_fun, THEN eta]
+ by (simp add: matrix_chain_left [THEN chain_fun, THEN eta]
dominate_islub cpo_lub matrix_chain_left chain_fun)
qed
lemma isub_eq:
assumes DM: "matrix(D, M)" and D: "cpo(D)"
- shows "isub(D,(\<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m)),y) <-> isub(D,(\<lambda>n \<in> nat. M`n`n),y)"
+ shows "isub(D,(\<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m)),y) \<longleftrightarrow> isub(D,(\<lambda>n \<in> nat. M`n`n),y)"
proof
assume isub: "isub(D, \<lambda>n\<in>nat. lub(D, Lambda(nat, op `(M ` n))), y)"
- hence dom: "dominate(D, \<lambda>n\<in>nat. M ` n ` n, \<lambda>n\<in>nat. lub(D, Lambda(nat, op `(M ` n))))"
+ hence dom: "dominate(D, \<lambda>n\<in>nat. M ` n ` n, \<lambda>n\<in>nat. lub(D, Lambda(nat, op `(M ` n))))"
using DM D
by (simp add: dominate_def, intro ballI bexI,
simp_all add: matrix_chain_left [THEN chain_fun, THEN eta] islub_ub cpo_lub matrix_chain_left)
thus "isub(D, \<lambda>n\<in>nat. M ` n ` n, y)" using DM D
- by - (rule dominate_isub [OF dom isub],
+ by - (rule dominate_isub [OF dom isub],
simp_all add: matrix_chain_diag chain_fun matrix_chain_lub)
next
- assume isub: "isub(D, \<lambda>n\<in>nat. M ` n ` n, y)"
+ assume isub: "isub(D, \<lambda>n\<in>nat. M ` n ` n, y)"
thus "isub(D, \<lambda>n\<in>nat. lub(D, Lambda(nat, op `(M ` n))), y)" using DM D
by (simp add: isub_lemma)
qed
@@ -591,7 +591,7 @@
by (simp add: lub_def)
lemma lub_matrix_diag:
- "[|matrix(D,M); cpo(D)|]
+ "[|matrix(D,M); cpo(D)|]
==> lub(D,(\<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m))) =
lub(D,(\<lambda>n \<in> nat. M`n`n))"
apply (simp (no_asm) add: lub_matrix_diag_aux1 lub_matrix_diag_aux2)
@@ -599,7 +599,7 @@
done
lemma lub_matrix_diag_sym:
- "[|matrix(D,M); cpo(D)|]
+ "[|matrix(D,M); cpo(D)|]
==> lub(D,(\<lambda>m \<in> nat. lub(D,\<lambda>n \<in> nat. M`n`m))) =
lub(D,(\<lambda>n \<in> nat. M`n`n))"
by (drule matrix_sym_axis [THEN lub_matrix_diag], auto)
@@ -610,7 +610,7 @@
lemma monoI:
"[|f \<in> set(D)->set(E);
- !!x y. [|rel(D,x,y); x \<in> set(D); y \<in> set(D)|] ==> rel(E,f`x,f`y)|]
+ !!x y. [|rel(D,x,y); x \<in> set(D); y \<in> set(D)|] ==> rel(E,f`x,f`y)|]
==> f \<in> mono(D,E)"
by (simp add: mono_def)
@@ -627,14 +627,14 @@
lemma contI:
"[|f \<in> set(D)->set(E);
!!x y. [|rel(D,x,y); x \<in> set(D); y \<in> set(D)|] ==> rel(E,f`x,f`y);
- !!X. chain(D,X) ==> f`lub(D,X) = lub(E,\<lambda>n \<in> nat. f`(X`n))|]
+ !!X. chain(D,X) ==> f`lub(D,X) = lub(E,\<lambda>n \<in> nat. f`(X`n))|]
==> f \<in> cont(D,E)"
by (simp add: cont_def mono_def)
lemma cont2mono: "f \<in> cont(D,E) ==> f \<in> mono(D,E)"
by (simp add: cont_def)
-lemma cont_fun [TC] : "f \<in> cont(D,E) ==> f \<in> set(D)->set(E)"
+lemma cont_fun [TC]: "f \<in> cont(D,E) ==> f \<in> set(D)->set(E)"
apply (simp add: cont_def)
apply (rule mono_fun, blast)
done
@@ -684,7 +684,7 @@
(* rel_cf originally an equality. Now stated as two rules. Seemed easiest. *)
lemma rel_cfI:
- "[|!!x. x \<in> set(D) ==> rel(E,f`x,g`x); f \<in> cont(D,E); g \<in> cont(D,E)|]
+ "[|!!x. x \<in> set(D) ==> rel(E,f`x,g`x); f \<in> cont(D,E); g \<in> cont(D,E)|]
==> rel(cf(D,E),f,g)"
by (simp add: rel_I cf_def)
@@ -703,7 +703,7 @@
done
lemma matrix_lemma:
- "[|chain(cf(D,E),X); chain(D,Xa); cpo(D); cpo(E) |]
+ "[|chain(cf(D,E),X); chain(D,Xa); cpo(D); cpo(E) |]
==> matrix(E,\<lambda>x \<in> nat. \<lambda>xa \<in> nat. X`x`(Xa`xa))"
apply (rule matrix_chainI, auto)
apply (force intro: chainI lam_type apply_funtype cont_fun cf_cont cont_mono)
@@ -716,13 +716,13 @@
shows "(\<lambda>x \<in> set(D). lub(E, \<lambda>n \<in> nat. X ` n ` x)) \<in> cont(D, E)"
proof (rule contI)
show "(\<lambda>x\<in>set(D). lub(E, \<lambda>n\<in>nat. X ` n ` x)) \<in> set(D) \<rightarrow> set(E)"
- by (blast intro: lam_type chain_cf [THEN cpo_lub, THEN islub_in] ch E)
+ by (blast intro: lam_type chain_cf [THEN cpo_lub, THEN islub_in] ch E)
next
fix x y
assume xy: "rel(D, x, y)" "x \<in> set(D)" "y \<in> set(D)"
hence dom: "dominate(E, \<lambda>n\<in>nat. X ` n ` x, \<lambda>n\<in>nat. X ` n ` y)"
by (force intro: dominateI chain_in [OF ch, THEN cf_cont, THEN cont_mono])
- note chE = chain_cf [OF ch]
+ note chE = chain_cf [OF ch]
from xy show "rel(E, (\<lambda>x\<in>set(D). lub(E, \<lambda>n\<in>nat. X ` n ` x)) ` x,
(\<lambda>x\<in>set(D). lub(E, \<lambda>n\<in>nat. X ` n ` x)) ` y)"
by (simp add: dominate_islub [OF dom] cpo_lub [OF chE] E chain_fun [OF chE])
@@ -735,7 +735,7 @@
by (simp add: D E)
also have "... = lub(E, \<lambda>x\<in>nat. lub(E, \<lambda>n\<in>nat. X ` n ` (Y ` x)))"
using matrix_lemma [THEN lub_matrix_diag_sym, OF ch chDY]
- by (simp add: D E)
+ by (simp add: D E)
finally have "lub(E, \<lambda>x\<in>nat. lub(E, \<lambda>n\<in>nat. X ` x ` (Y ` n))) =
lub(E, \<lambda>x\<in>nat. lub(E, \<lambda>n\<in>nat. X ` n ` (Y ` x)))" .
thus "(\<lambda>x\<in>set(D). lub(E, \<lambda>n\<in>nat. X ` n ` x)) ` lub(D, Y) =
@@ -745,7 +745,7 @@
qed
lemma islub_cf:
- "[| chain(cf(D,E),X); cpo(D); cpo(E)|]
+ "[| chain(cf(D,E),X); cpo(D); cpo(E)|]
==> islub(cf(D,E), X, \<lambda>x \<in> set(D). lub(E,\<lambda>n \<in> nat. X`n`x))"
apply (rule islubI)
apply (rule isubI)
@@ -774,13 +774,13 @@
apply (assumption | rule cf_cont [THEN cont_fun, THEN apply_type] cf_cont)+
apply (rule fun_extension)
apply (assumption | rule cf_cont [THEN cont_fun])+
-apply (blast intro: cpo_antisym rel_cf
+apply (blast intro: cpo_antisym rel_cf
cf_cont [THEN cont_fun, THEN apply_type])
apply (fast intro: islub_cf)
done
lemma lub_cf:
- "[| chain(cf(D,E),X); cpo(D); cpo(E)|]
+ "[| chain(cf(D,E),X); cpo(D); cpo(E)|]
==> lub(cf(D,E), X) = (\<lambda>x \<in> set(D). lub(E,\<lambda>n \<in> nat. X`n`x))"
by (blast intro: islub_unique cpo_lub islub_cf cpo_cf)
@@ -801,13 +801,13 @@
lemma pcpo_cf:
"[|cpo(D); pcpo(E)|] ==> pcpo(cf(D,E))"
apply (rule pcpoI)
-apply (assumption |
+apply (assumption |
rule cf_least bot_in const_cont [THEN cont_cf] cf_cont cpo_cf pcpo_cpo)+
done
lemma bot_cf:
"[|cpo(D); pcpo(E)|] ==> bot(cf(D,E)) = (\<lambda>x \<in> set(D).bot(E))"
-by (blast intro: bot_unique [symmetric] pcpo_cf cf_least
+by (blast intro: bot_unique [symmetric] pcpo_cf cf_least
bot_in [THEN const_cont, THEN cont_cf] cf_cont pcpo_cpo)
(*----------------------------------------------------------------------*)
@@ -838,9 +838,9 @@
lemma comp_mono:
"[| f \<in> cont(D',E); g \<in> cont(D,D'); f':cont(D',E); g':cont(D,D');
- rel(cf(D',E),f,f'); rel(cf(D,D'),g,g'); cpo(D); cpo(E) |]
+ rel(cf(D',E),f,f'); rel(cf(D,D'),g,g'); cpo(D); cpo(E) |]
==> rel(cf(D,E),f O g,f' O g')"
-apply (rule rel_cfI)
+apply (rule rel_cfI)
apply (subst comp_cont_apply)
apply (rule_tac [3] comp_cont_apply [THEN ssubst])
apply (rule_tac [5] cpo_trans)
@@ -848,7 +848,7 @@
done
lemma chain_cf_comp:
- "[| chain(cf(D',E),X); chain(cf(D,D'),Y); cpo(D); cpo(E)|]
+ "[| chain(cf(D',E),X); chain(cf(D,D'),Y); cpo(D); cpo(E)|]
==> chain(cf(D,E),\<lambda>n \<in> nat. X`n O Y`n)"
apply (rule chainI)
defer 1
@@ -858,23 +858,23 @@
apply (rule_tac [3] comp_cont_apply [THEN ssubst])
apply (rule_tac [5] cpo_trans)
apply (rule_tac [6] rel_cf)
-apply (rule_tac [8] cont_mono)
-apply (blast intro: lam_type comp_pres_cont cont_cf chain_in [THEN cf_cont]
+apply (rule_tac [8] cont_mono)
+apply (blast intro: lam_type comp_pres_cont cont_cf chain_in [THEN cf_cont]
cont_map chain_rel rel_cf)+
done
lemma comp_lubs:
- "[| chain(cf(D',E),X); chain(cf(D,D'),Y); cpo(D); cpo(D'); cpo(E)|]
+ "[| chain(cf(D',E),X); chain(cf(D,D'),Y); cpo(D); cpo(D'); cpo(E)|]
==> lub(cf(D',E),X) O lub(cf(D,D'),Y) = lub(cf(D,E),\<lambda>n \<in> nat. X`n O Y`n)"
apply (rule fun_extension)
apply (rule_tac [3] lub_cf [THEN ssubst])
-apply (assumption |
- rule comp_fun cf_cont [THEN cont_fun] cpo_lub [THEN islub_in]
+apply (assumption |
+ rule comp_fun cf_cont [THEN cont_fun] cpo_lub [THEN islub_in]
cpo_cf chain_cf_comp)+
apply (simp add: chain_in [THEN cf_cont, THEN comp_cont_apply])
apply (subst comp_cont_apply)
apply (assumption | rule cpo_lub [THEN islub_in, THEN cf_cont] cpo_cf)+
-apply (simp add: lub_cf chain_cf chain_in [THEN cf_cont, THEN cont_lub]
+apply (simp add: lub_cf chain_cf chain_in [THEN cf_cont, THEN cont_lub]
chain_cf [THEN cpo_lub, THEN islub_in])
apply (cut_tac M = "\<lambda>xa \<in> nat. \<lambda>xb \<in> nat. X`xa` (Y`xb`x)" in lub_matrix_diag)
prefer 3 apply simp
@@ -968,8 +968,8 @@
lemma projpair_unique:
- "[|cpo(D); cpo(E); projpair(D,E,e,p); projpair(D,E,e',p')|]
- ==> (e=e')<->(p=p')"
+ "[|cpo(D); cpo(E); projpair(D,E,e,p); projpair(D,E,e',p')|]
+ ==> (e=e')\<longleftrightarrow>(p=p')"
by (blast intro: cpo_antisym projpair_unique_aux1 projpair_unique_aux2 cpo_cf cont_cf
dest: projpair_ep_cont)
@@ -1036,7 +1036,7 @@
(* Proof in Isa/ZF: 23 lines (compared to 56: 60% reduction). *)
lemma comp_lemma:
- "[|emb(D,D',e); emb(D',E,e'); cpo(D); cpo(D'); cpo(E)|]
+ "[|emb(D,D',e); emb(D',E,e'); cpo(D); cpo(D'); cpo(E)|]
==> projpair(D,E,e' O e,(Rp(D,D',e)) O (Rp(D',E,e')))"
apply (simp add: projpair_def, safe)
apply (assumption | rule comp_pres_cont Rp_cont emb_cont)+
@@ -1090,7 +1090,7 @@
by (simp add: iprod_def rel_def)
lemma chain_iprod:
- "[|chain(iprod(DD),X); !!n. n \<in> nat ==> cpo(DD`n); n \<in> nat|]
+ "[|chain(iprod(DD),X); !!n. n \<in> nat ==> cpo(DD`n); n \<in> nat|]
==> chain(DD`n,\<lambda>m \<in> nat. X`m`n)"
apply (unfold chain_def, safe)
apply (rule lam_type)
@@ -1101,7 +1101,7 @@
done
lemma islub_iprod:
- "[|chain(iprod(DD),X); !!n. n \<in> nat ==> cpo(DD`n)|]
+ "[|chain(iprod(DD),X); !!n. n \<in> nat ==> cpo(DD`n)|]
==> islub(iprod(DD),X,\<lambda>n \<in> nat. lub(DD`n,\<lambda>m \<in> nat. X`m`n))"
apply (simp add: islub_def isub_def, safe)
apply (rule iprodI)
@@ -1151,7 +1151,7 @@
lemma subcpoI:
"[|set(D)<=set(E);
- !!x y. [|x \<in> set(D); y \<in> set(D)|] ==> rel(D,x,y)<->rel(E,x,y);
+ !!x y. [|x \<in> set(D); y \<in> set(D)|] ==> rel(D,x,y)\<longleftrightarrow>rel(E,x,y);
!!X. chain(D,X) ==> lub(E,X) \<in> set(D)|] ==> subcpo(D,E)"
by (simp add: subcpo_def)
@@ -1159,7 +1159,7 @@
by (simp add: subcpo_def)
lemma subcpo_rel_eq:
- "[|subcpo(D,E); x \<in> set(D); y \<in> set(D)|] ==> rel(D,x,y)<->rel(E,x,y)"
+ "[|subcpo(D,E); x \<in> set(D); y \<in> set(D)|] ==> rel(D,x,y)\<longleftrightarrow>rel(E,x,y)"
by (simp add: subcpo_def)
lemmas subcpo_relD1 = subcpo_rel_eq [THEN iffD1]
@@ -1213,7 +1213,7 @@
by (simp add: rel_def mkcpo_def)
lemma rel_mkcpo:
- "[|x \<in> set(D); y \<in> set(D)|] ==> rel(mkcpo(D,P),x,y) <-> rel(D,x,y)"
+ "[|x \<in> set(D); y \<in> set(D)|] ==> rel(mkcpo(D,P),x,y) \<longleftrightarrow> rel(D,x,y)"
by (simp add: mkcpo_def rel_def set_def)
lemma chain_mkcpo:
@@ -1273,7 +1273,7 @@
lemma rel_DinfI:
"[|!!n. n \<in> nat ==> rel(DD`n,x`n,y`n);
- x:(\<Pi> n \<in> nat. set(DD`n)); y:(\<Pi> n \<in> nat. set(DD`n))|]
+ x:(\<Pi> n \<in> nat. set(DD`n)); y:(\<Pi> n \<in> nat. set(DD`n))|]
==> rel(Dinf(DD,ee),x,y)"
apply (simp add: Dinf_def)
apply (blast intro: rel_mkcpo [THEN iffD2] rel_iprodI iprodI)
@@ -1299,7 +1299,7 @@
apply (assumption | rule chain_Dinf emb_chain_cpo)+
apply simp
apply (subst Rp_cont [THEN cont_lub])
-apply (assumption |
+apply (assumption |
rule emb_chain_cpo emb_chain_emb nat_succI chain_iprod chain_Dinf)+
(* Useful simplification, ugly in HOL. *)
apply (simp add: Dinf_eq chain_in)
@@ -1341,11 +1341,11 @@
by (simp add: e_less_def)
lemma le_exists:
- "[| m le n; !!x. [|n=m#+x; x \<in> nat|] ==> Q; n \<in> nat |] ==> Q"
+ "[| m \<le> n; !!x. [|n=m#+x; x \<in> nat|] ==> Q; n \<in> nat |] ==> Q"
apply (drule less_imp_succ_add, auto)
done
-lemma e_less_le: "[| m le n; n \<in> nat |]
+lemma e_less_le: "[| m \<le> n; n \<in> nat |]
==> e_less(DD,ee,m,succ(n)) = ee`n O e_less(DD,ee,m,n)"
apply (rule le_exists, assumption)
apply (simp add: e_less_add, assumption)
@@ -1358,7 +1358,7 @@
by (simp add: e_less_le e_less_eq)
lemma e_less_succ_emb:
- "[|!!n. n \<in> nat ==> emb(DD`n,DD`succ(n),ee`n); m \<in> nat|]
+ "[|!!n. n \<in> nat ==> emb(DD`n,DD`succ(n),ee`n); m \<in> nat|]
==> e_less(DD,ee,m,succ(m)) = ee`m"
apply (simp add: e_less_succ)
apply (blast intro: emb_cont cont_fun comp_id)
@@ -1370,7 +1370,7 @@
lemma emb_e_less_add:
"[| emb_chain(DD,ee); m \<in> nat |]
==> emb(DD`m, DD`(m#+k), e_less(DD,ee,m,m#+k))"
-apply (subgoal_tac "emb (DD`m, DD` (m#+natify (k)),
+apply (subgoal_tac "emb (DD`m, DD` (m#+natify (k)),
e_less (DD,ee,m,m#+natify (k))) ")
apply (rule_tac [2] n = "natify (k) " in nat_induct)
apply (simp_all add: e_less_eq)
@@ -1380,7 +1380,7 @@
done
lemma emb_e_less:
- "[| m le n; emb_chain(DD,ee); n \<in> nat |]
+ "[| m \<le> n; emb_chain(DD,ee); n \<in> nat |]
==> emb(DD`m, DD`n, e_less(DD,ee,m,n))"
apply (frule lt_nat_in_nat)
apply (erule nat_succI)
@@ -1397,8 +1397,8 @@
Therefore this theorem is only a lemma. *)
lemma e_less_split_add_lemma [rule_format]:
- "[| emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
- ==> n le k -->
+ "[| emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
+ ==> n \<le> k \<longrightarrow>
e_less(DD,ee,m,m#+k) = e_less(DD,ee,m#+n,m#+k) O e_less(DD,ee,m,m#+n)"
apply (induct_tac k)
apply (simp add: e_less_eq id_type [THEN id_comp])
@@ -1419,7 +1419,7 @@
done
lemma e_less_split_add:
- "[| n le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
+ "[| n \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
==> e_less(DD,ee,m,m#+k) = e_less(DD,ee,m#+n,m#+k) O e_less(DD,ee,m,m#+n)"
by (blast intro: e_less_split_add_lemma)
@@ -1428,13 +1428,13 @@
by (simp add: e_gr_def)
lemma e_gr_add:
- "[|n \<in> nat; k \<in> nat|]
+ "[|n \<in> nat; k \<in> nat|]
==> e_gr(DD,ee,succ(n#+k),n) =
e_gr(DD,ee,n#+k,n) O Rp(DD`(n#+k),DD`succ(n#+k),ee`(n#+k))"
by (simp add: e_gr_def)
lemma e_gr_le:
- "[|n le m; m \<in> nat; n \<in> nat|]
+ "[|n \<le> m; m \<in> nat; n \<in> nat|]
==> e_gr(DD,ee,succ(m),n) = e_gr(DD,ee,m,n) O Rp(DD`m,DD`succ(m),ee`m)"
apply (erule le_exists)
apply (simp add: e_gr_add, assumption+)
@@ -1445,14 +1445,14 @@
by (simp add: e_gr_le e_gr_eq)
(* Cpo asm's due to THE uniqueness. *)
-lemma e_gr_succ_emb: "[|emb_chain(DD,ee); m \<in> nat|]
+lemma e_gr_succ_emb: "[|emb_chain(DD,ee); m \<in> nat|]
==> e_gr(DD,ee,succ(m),m) = Rp(DD`m,DD`succ(m),ee`m)"
apply (simp add: e_gr_succ)
apply (blast intro: id_comp Rp_cont cont_fun emb_chain_cpo emb_chain_emb)
done
lemma e_gr_fun_add:
- "[|emb_chain(DD,ee); n \<in> nat; k \<in> nat|]
+ "[|emb_chain(DD,ee); n \<in> nat; k \<in> nat|]
==> e_gr(DD,ee,n#+k,n): set(DD`(n#+k))->set(DD`n)"
apply (induct_tac k)
apply (simp add: e_gr_eq id_type)
@@ -1461,15 +1461,15 @@
done
lemma e_gr_fun:
- "[|n le m; emb_chain(DD,ee); m \<in> nat; n \<in> nat|]
+ "[|n \<le> m; emb_chain(DD,ee); m \<in> nat; n \<in> nat|]
==> e_gr(DD,ee,m,n): set(DD`m)->set(DD`n)"
apply (rule le_exists, assumption)
apply (simp add: e_gr_fun_add, assumption+)
done
lemma e_gr_split_add_lemma:
- "[| emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
- ==> m le k -->
+ "[| emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
+ ==> m \<le> k \<longrightarrow>
e_gr(DD,ee,n#+k,n) = e_gr(DD,ee,n#+m,n) O e_gr(DD,ee,n#+k,n#+m)"
apply (induct_tac k)
apply (rule impI)
@@ -1491,19 +1491,19 @@
done
lemma e_gr_split_add:
- "[| m le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
+ "[| m \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
==> e_gr(DD,ee,n#+k,n) = e_gr(DD,ee,n#+m,n) O e_gr(DD,ee,n#+k,n#+m)"
apply (blast intro: e_gr_split_add_lemma [THEN mp])
done
lemma e_less_cont:
- "[|m le n; emb_chain(DD,ee); m \<in> nat; n \<in> nat|]
+ "[|m \<le> n; emb_chain(DD,ee); m \<in> nat; n \<in> nat|]
==> e_less(DD,ee,m,n):cont(DD`m,DD`n)"
apply (blast intro: emb_cont emb_e_less)
done
lemma e_gr_cont:
- "[|n le m; emb_chain(DD,ee); m \<in> nat; n \<in> nat|]
+ "[|n \<le> m; emb_chain(DD,ee); m \<in> nat; n \<in> nat|]
==> e_gr(DD,ee,m,n):cont(DD`m,DD`n)"
apply (erule rev_mp)
apply (induct_tac m)
@@ -1520,7 +1520,7 @@
(* Considerably shorter.... 57 against 26 *)
lemma e_less_e_gr_split_add:
- "[|n le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
+ "[|n \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
==> e_less(DD,ee,m,m#+n) = e_gr(DD,ee,m#+k,m#+n) O e_less(DD,ee,m,m#+k)"
(* Use mp to prepare for induction. *)
apply (erule rev_mp)
@@ -1547,7 +1547,7 @@
(* Again considerably shorter, and easy to obtain from the previous thm. *)
lemma e_gr_e_less_split_add:
- "[|m le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
+ "[|m \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
==> e_gr(DD,ee,n#+m,n) = e_gr(DD,ee,n#+k,n) O e_less(DD,ee,n#+m,n#+k)"
(* Use mp to prepare for induction. *)
apply (erule rev_mp)
@@ -1572,7 +1572,7 @@
lemma emb_eps:
- "[|m le n; emb_chain(DD,ee); m \<in> nat; n \<in> nat|]
+ "[|m \<le> n; emb_chain(DD,ee); m \<in> nat; n \<in> nat|]
==> emb(DD`m,DD`n,eps(DD,ee,m,n))"
apply (simp add: eps_def)
apply (blast intro: emb_e_less)
@@ -1595,7 +1595,7 @@
by (simp add: eps_def add_le_self)
lemma eps_e_less:
- "[|m le n; m \<in> nat; n \<in> nat|] ==> eps(DD,ee,m,n) = e_less(DD,ee,m,n)"
+ "[|m \<le> n; m \<in> nat; n \<in> nat|] ==> eps(DD,ee,m,n) = e_less(DD,ee,m,n)"
by (simp add: eps_def)
lemma eps_e_gr_add:
@@ -1603,7 +1603,7 @@
by (simp add: eps_def e_less_eq e_gr_eq)
lemma eps_e_gr:
- "[|n le m; m \<in> nat; n \<in> nat|] ==> eps(DD,ee,m,n) = e_gr(DD,ee,m,n)"
+ "[|n \<le> m; m \<in> nat; n \<in> nat|] ==> eps(DD,ee,m,n) = e_gr(DD,ee,m,n)"
apply (erule le_exists)
apply (simp_all add: eps_e_gr_add)
done
@@ -1627,28 +1627,28 @@
(* Theorems about splitting. *)
lemma eps_split_add_left:
- "[|n le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
+ "[|n \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
==> eps(DD,ee,m,m#+k) = eps(DD,ee,m#+n,m#+k) O eps(DD,ee,m,m#+n)"
apply (simp add: eps_e_less add_le_self add_le_mono)
apply (auto intro: e_less_split_add)
done
lemma eps_split_add_left_rev:
- "[|n le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
+ "[|n \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
==> eps(DD,ee,m,m#+n) = eps(DD,ee,m#+k,m#+n) O eps(DD,ee,m,m#+k)"
apply (simp add: eps_e_less_add eps_e_gr add_le_self add_le_mono)
apply (auto intro: e_less_e_gr_split_add)
done
lemma eps_split_add_right:
- "[|m le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
+ "[|m \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
==> eps(DD,ee,n#+k,n) = eps(DD,ee,n#+m,n) O eps(DD,ee,n#+k,n#+m)"
apply (simp add: eps_e_gr add_le_self add_le_mono)
apply (auto intro: e_gr_split_add)
done
lemma eps_split_add_right_rev:
- "[|m le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
+ "[|m \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
==> eps(DD,ee,n#+m,n) = eps(DD,ee,n#+k,n) O eps(DD,ee,n#+m,n#+k)"
apply (simp add: eps_e_gr_add eps_e_less add_le_self add_le_mono)
apply (auto intro: e_gr_e_less_split_add)
@@ -1657,8 +1657,8 @@
(* Arithmetic *)
lemma le_exists_lemma:
- "[| n le k; k le m;
- !!p q. [|p le q; k=n#+p; m=n#+q; p \<in> nat; q \<in> nat|] ==> R;
+ "[| n \<le> k; k \<le> m;
+ !!p q. [|p \<le> q; k=n#+p; m=n#+q; p \<in> nat; q \<in> nat|] ==> R;
m \<in> nat |]==>R"
apply (rule le_exists, assumption)
prefer 2 apply (simp add: lt_nat_in_nat)
@@ -1666,28 +1666,28 @@
done
lemma eps_split_left_le:
- "[|m le k; k le n; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
+ "[|m \<le> k; k \<le> n; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
==> eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)"
apply (rule le_exists_lemma, assumption+)
apply (auto intro: eps_split_add_left)
done
lemma eps_split_left_le_rev:
- "[|m le n; n le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
+ "[|m \<le> n; n \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
==> eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)"
apply (rule le_exists_lemma, assumption+)
apply (auto intro: eps_split_add_left_rev)
done
lemma eps_split_right_le:
- "[|n le k; k le m; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
+ "[|n \<le> k; k \<le> m; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
==> eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)"
apply (rule le_exists_lemma, assumption+)
apply (auto intro: eps_split_add_right)
done
lemma eps_split_right_le_rev:
- "[|n le m; m le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
+ "[|n \<le> m; m \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
==> eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)"
apply (rule le_exists_lemma, assumption+)
apply (auto intro: eps_split_add_right_rev)
@@ -1696,7 +1696,7 @@
(* The desired two theorems about `splitting'. *)
lemma eps_split_left:
- "[|m le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
+ "[|m \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
==> eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)"
apply (rule nat_linear_le)
apply (rule_tac [4] eps_split_right_le_rev)
@@ -1708,7 +1708,7 @@
done
lemma eps_split_right:
- "[|n le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
+ "[|n \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
==> eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)"
apply (rule nat_linear_le)
apply (rule_tac [3] eps_split_left_le_rev)
@@ -1726,7 +1726,7 @@
(* Considerably shorter. *)
lemma rho_emb_fun:
- "[|emb_chain(DD,ee); n \<in> nat|]
+ "[|emb_chain(DD,ee); n \<in> nat|]
==> rho_emb(DD,ee,n): set(DD`n) -> set(Dinf(DD,ee))"
apply (simp add: rho_emb_def)
apply (assumption |
@@ -1742,8 +1742,8 @@
apply (assumption | rule add_le_self nat_0I nat_succI)+
apply (simp add: eps_succ_Rp)
apply (subst comp_fun_apply)
- apply (assumption |
- rule eps_fun nat_succI Rp_cont [THEN cont_fun]
+ apply (assumption |
+ rule eps_fun nat_succI Rp_cont [THEN cont_fun]
emb_chain_emb emb_chain_cpo refl)+
(* Now the second part of the proof. Slightly different than HOL. *)
apply (simp add: eps_e_less nat_succI)
@@ -1752,7 +1752,7 @@
apply (subst comp_fun_apply)
apply (assumption | rule e_less_cont cont_fun emb_chain_emb emb_cont)+
apply (subst embRp_eq_thm)
-apply (assumption |
+apply (assumption |
rule emb_chain_emb e_less_cont [THEN cont_fun, THEN apply_type]
emb_chain_cpo nat_succI)+
apply (simp add: eps_e_less)
@@ -1773,13 +1773,13 @@
(* Shorter proof, 23 against 62. *)
lemma rho_emb_cont:
- "[|emb_chain(DD,ee); n \<in> nat|]
+ "[|emb_chain(DD,ee); n \<in> nat|]
==> rho_emb(DD,ee,n): cont(DD`n,Dinf(DD,ee))"
apply (rule contI)
apply (assumption | rule rho_emb_fun)+
apply (rule rel_DinfI)
apply (simp add: rho_emb_def)
-apply (assumption |
+apply (assumption |
rule eps_cont [THEN cont_mono] Dinf_prod apply_type rho_emb_fun)+
(* Continuity, different order, slightly different proofs. *)
apply (subst lub_Dinf)
@@ -1788,16 +1788,16 @@
apply simp
apply (rule rel_DinfI)
apply (simp add: rho_emb_apply2 chain_in)
-apply (assumption |
- rule eps_cont [THEN cont_mono] chain_rel Dinf_prod
+apply (assumption |
+ rule eps_cont [THEN cont_mono] chain_rel Dinf_prod
rho_emb_fun [THEN apply_type] chain_in nat_succI)+
(* Now, back to the result of applying lub_Dinf *)
apply (simp add: rho_emb_apply2 chain_in)
apply (subst rho_emb_apply1)
apply (assumption | rule cpo_lub [THEN islub_in] emb_chain_cpo)+
apply (rule fun_extension)
-apply (assumption |
- rule lam_type eps_cont [THEN cont_fun, THEN apply_type]
+apply (assumption |
+ rule lam_type eps_cont [THEN cont_fun, THEN apply_type]
cpo_lub [THEN islub_in] emb_chain_cpo)+
apply (assumption | rule cont_chain eps_cont emb_chain_cpo)+
apply simp
@@ -1807,7 +1807,7 @@
(* 32 vs 61, using safe_tac with imp in asm would be unfortunate (5steps) *)
lemma eps1_aux1:
- "[|m le n; emb_chain(DD,ee); x \<in> set(Dinf(DD,ee)); m \<in> nat; n \<in> nat|]
+ "[|m \<le> n; emb_chain(DD,ee); x \<in> set(Dinf(DD,ee)); m \<in> nat; n \<in> nat|]
==> rel(DD`n,e_less(DD,ee,m,n)`(x`m),x`n)"
apply (erule rev_mp) (* For induction proof *)
apply (induct_tac n)
@@ -1823,16 +1823,16 @@
apply (rule_tac [2] e_less_le [THEN ssubst])
apply (assumption | rule emb_chain_cpo nat_succI)+
apply (subst comp_fun_apply)
-apply (assumption |
- rule emb_chain_emb [THEN emb_cont] e_less_cont cont_fun apply_type
+apply (assumption |
+ rule emb_chain_emb [THEN emb_cont] e_less_cont cont_fun apply_type
Dinf_prod)+
apply (rule_tac y = "x`xa" in emb_chain_emb [THEN emb_cont, THEN cont_mono])
apply (assumption | rule e_less_cont [THEN cont_fun] apply_type Dinf_prod)+
apply (rule_tac x1 = x and n1 = xa in Dinf_eq [THEN subst])
apply (rule_tac [3] comp_fun_apply [THEN subst])
apply (rename_tac [5] y)
-apply (rule_tac [5] P =
- "%z. rel(DD`succ(y),
+apply (rule_tac [5] P =
+ "%z. rel(DD`succ(y),
(ee`y O Rp(?DD(y)`y,?DD(y)`succ(y),?ee(y)`y)) ` (x`succ(y)),
z)"
in id_conv [THEN subst])
@@ -1851,7 +1851,7 @@
(* 18 vs 40 *)
lemma eps1_aux2:
- "[|n le m; emb_chain(DD,ee); x \<in> set(Dinf(DD,ee)); m \<in> nat; n \<in> nat|]
+ "[|n \<le> m; emb_chain(DD,ee); x \<in> set(Dinf(DD,ee)); m \<in> nat; n \<in> nat|]
==> rel(DD`n,e_gr(DD,ee,m,n)`(x`m),x`n)"
apply (erule rev_mp) (* For induction proof *)
apply (induct_tac m)
@@ -1866,8 +1866,8 @@
apply (subst e_gr_le)
apply (rule_tac [4] comp_fun_apply [THEN ssubst])
apply (rule_tac [6] Dinf_eq [THEN ssubst])
-apply (assumption |
- rule emb_chain_emb emb_chain_cpo Rp_cont e_gr_cont cont_fun emb_cont
+apply (assumption |
+ rule emb_chain_emb emb_chain_cpo Rp_cont e_gr_cont cont_fun emb_cont
apply_type Dinf_prod nat_succI)+
apply (simp add: e_gr_eq)
apply (subst id_conv)
@@ -1875,7 +1875,7 @@
done
lemma eps1:
- "[|emb_chain(DD,ee); x \<in> set(Dinf(DD,ee)); m \<in> nat; n \<in> nat|]
+ "[|emb_chain(DD,ee); x \<in> set(Dinf(DD,ee)); m \<in> nat; n \<in> nat|]
==> rel(DD`n,eps(DD,ee,m,n)`(x`m),x`n)"
apply (simp add: eps_def)
apply (blast intro: eps1_aux1 not_le_iff_lt [THEN iffD1, THEN leI, THEN eps1_aux2]
@@ -1887,7 +1887,7 @@
Look for occurences of rel_cfI, rel_DinfI, etc to evaluate the problem. *)
lemma lam_Dinf_cont:
- "[| emb_chain(DD,ee); n \<in> nat |]
+ "[| emb_chain(DD,ee); n \<in> nat |]
==> (\<lambda>x \<in> set(Dinf(DD,ee)). x`n) \<in> cont(Dinf(DD,ee),DD`n)"
apply (rule contI)
apply (assumption | rule lam_type apply_type Dinf_prod)+
@@ -1899,7 +1899,7 @@
done
lemma rho_projpair:
- "[| emb_chain(DD,ee); n \<in> nat |]
+ "[| emb_chain(DD,ee); n \<in> nat |]
==> projpair(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n),rho_proj(DD,ee,n))"
apply (simp add: rho_proj_def)
apply (rule projpairI)
@@ -1913,23 +1913,23 @@
apply (rule_tac [4] comp_fun_apply [THEN ssubst])
apply (rule_tac [6] beta [THEN ssubst])
apply (rule_tac [7] rho_emb_id [THEN ssubst])
-apply (assumption |
+apply (assumption |
rule comp_fun id_type lam_type rho_emb_fun Dinf_prod [THEN apply_type]
apply_type refl)+
(*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
-apply (rule rel_cfI) (* ------------------>>>Yields type cond, not in HOL *)
+apply (rule rel_cfI) (* ----------------\<longrightarrow>>>Yields type cond, not in HOL *)
apply (subst id_conv)
apply (rule_tac [2] comp_fun_apply [THEN ssubst])
apply (rule_tac [4] beta [THEN ssubst])
apply (rule_tac [5] rho_emb_apply1 [THEN ssubst])
-apply (rule_tac [6] rel_DinfI)
+apply (rule_tac [6] rel_DinfI)
apply (rule_tac [6] beta [THEN ssubst])
(* Dinf_prod bad with lam_type *)
apply (assumption |
rule eps1 lam_type rho_emb_fun eps_fun
Dinf_prod [THEN apply_type] refl)+
-apply (assumption |
- rule apply_type eps_fun Dinf_prod comp_pres_cont rho_emb_cont
+apply (assumption |
+ rule apply_type eps_fun Dinf_prod comp_pres_cont rho_emb_cont
lam_Dinf_cont id_cont cpo_Dinf emb_chain_cpo)+
done
@@ -1937,7 +1937,7 @@
"[| emb_chain(DD,ee); n \<in> nat |] ==> emb(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n))"
by (auto simp add: emb_def intro: exI rho_projpair)
-lemma rho_proj_cont: "[| emb_chain(DD,ee); n \<in> nat |]
+lemma rho_proj_cont: "[| emb_chain(DD,ee); n \<in> nat |]
==> rho_proj(DD,ee,n) \<in> cont(Dinf(DD,ee),DD`n)"
by (auto intro: rho_projpair projpair_p_cont)
@@ -1947,7 +1947,7 @@
lemma commuteI:
"[| !!n. n \<in> nat ==> emb(DD`n,E,r(n));
- !!m n. [|m le n; m \<in> nat; n \<in> nat|] ==> r(n) O eps(DD,ee,m,n) = r(m) |]
+ !!m n. [|m \<le> n; m \<in> nat; n \<in> nat|] ==> r(n) O eps(DD,ee,m,n) = r(m) |]
==> commute(DD,ee,E,r)"
by (simp add: commute_def)
@@ -1956,7 +1956,7 @@
by (simp add: commute_def)
lemma commute_eq:
- "[| commute(DD,ee,E,r); m le n; m \<in> nat; n \<in> nat |]
+ "[| commute(DD,ee,E,r); m \<le> n; m \<in> nat; n \<in> nat |]
==> r(n) O eps(DD,ee,m,n) = r(m) "
by (simp add: commute_def)
@@ -1976,17 +1976,17 @@
apply (auto intro: eps_fun)
done
-lemma le_succ: "n \<in> nat ==> n le succ(n)"
+lemma le_succ: "n \<in> nat ==> n \<le> succ(n)"
by (simp add: le_succ_iff)
(* Shorter proof: 21 vs 83 (106 - 23, due to OAssoc complication) *)
lemma commute_chain:
- "[| commute(DD,ee,E,r); emb_chain(DD,ee); cpo(E) |]
+ "[| commute(DD,ee,E,r); emb_chain(DD,ee); cpo(E) |]
==> chain(cf(E,E),\<lambda>n \<in> nat. r(n) O Rp(DD`n,E,r(n)))"
apply (rule chainI)
-apply (blast intro: lam_type cont_cf comp_pres_cont commute_emb Rp_cont
- emb_cont emb_chain_cpo,
+apply (blast intro: lam_type cont_cf comp_pres_cont commute_emb Rp_cont
+ emb_cont emb_chain_cpo,
simp)
apply (rule_tac r1 = r and m1 = n in commute_eq [THEN subst])
apply (assumption | rule le_succ nat_succI)+
@@ -1995,14 +1995,14 @@
apply (rule comp_assoc [THEN subst]) (* comp_assoc is simpler in Isa *)
apply (rule_tac r1 = "r (succ (n))" in comp_assoc [THEN ssubst])
apply (rule comp_mono)
-apply (blast intro: comp_pres_cont eps_cont emb_eps commute_emb Rp_cont
+apply (blast intro: comp_pres_cont eps_cont emb_eps commute_emb Rp_cont
emb_cont emb_chain_cpo le_succ)+
apply (rule_tac b="r(succ(n))" in comp_id [THEN subst]) (* 1 subst too much *)
apply (rule_tac [2] comp_mono)
-apply (blast intro: comp_pres_cont eps_cont emb_eps emb_id commute_emb
+apply (blast intro: comp_pres_cont eps_cont emb_eps emb_id commute_emb
Rp_cont emb_cont cont_fun emb_chain_cpo le_succ)+
apply (subst comp_id) (* Undoes "1 subst too much", typing next anyway *)
-apply (blast intro: cont_fun Rp_cont emb_cont commute_emb cont_cf cpo_cf
+apply (blast intro: cont_fun Rp_cont emb_cont commute_emb cont_cf cpo_cf
emb_chain_cpo embRp_rel emb_eps le_succ)+
done
@@ -2013,14 +2013,14 @@
by (auto intro: commute_chain rho_emb_commute cpo_Dinf)
lemma rho_emb_chain_apply1:
- "[| emb_chain(DD,ee); x \<in> set(Dinf(DD,ee)) |]
+ "[| emb_chain(DD,ee); x \<in> set(Dinf(DD,ee)) |]
==> chain(Dinf(DD,ee),
\<lambda>n \<in> nat.
(rho_emb(DD,ee,n) O Rp(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n)))`x)"
by (drule rho_emb_chain [THEN chain_cf], assumption, simp)
lemma chain_iprod_emb_chain:
- "[| chain(iprod(DD),X); emb_chain(DD,ee); n \<in> nat |]
+ "[| chain(iprod(DD),X); emb_chain(DD,ee); n \<in> nat |]
==> chain(DD`n,\<lambda>m \<in> nat. X `m `n)"
by (auto intro: chain_iprod emb_chain_cpo)
@@ -2031,7 +2031,7 @@
\<lambda>xa \<in> nat.
(rho_emb(DD, ee, xa) O Rp(DD ` xa, Dinf(DD, ee),rho_emb(DD, ee, xa))) `
x ` n)"
-by (frule rho_emb_chain_apply1 [THEN chain_Dinf, THEN chain_iprod_emb_chain],
+by (frule rho_emb_chain_apply1 [THEN chain_Dinf, THEN chain_iprod_emb_chain],
auto)
(* Shorter proof: 32 vs 72 (roughly), Isabelle proof has lemmas. *)
@@ -2045,7 +2045,7 @@
apply (rule cpo_cf) (*Instantiate variable, continued below (loops otherwise)*)
apply (assumption | rule cpo_Dinf)+
apply (rule islub_least)
-apply (assumption |
+apply (assumption |
rule cpo_lub rho_emb_chain cpo_cf cpo_Dinf isubI cont_cf id_cont)+
apply simp
apply (assumption | rule embRp_rel emb_rho_emb emb_chain_cpo cpo_Dinf)+
@@ -2055,7 +2055,7 @@
apply (subst lub_Dinf)
apply (assumption | rule rho_emb_chain_apply1)+
defer 1
-apply (assumption |
+apply (assumption |
rule Dinf_prod cpo_lub [THEN islub_in] id_cont cpo_Dinf cpo_cf cf_cont
rho_emb_chain rho_emb_chain_apply1 id_cont [THEN cont_cf])+
apply simp
@@ -2064,11 +2064,11 @@
apply (rule_tac [6] x1 = "x`n" in chain_const [THEN chain_fun])
defer 1
apply (assumption |
- rule rho_emb_chain_apply2 emb_chain_cpo islub_const apply_type
+ rule rho_emb_chain_apply2 emb_chain_cpo islub_const apply_type
Dinf_prod emb_chain_cpo chain_fun rho_emb_chain_apply2)+
apply (rule dominateI, assumption, simp)
apply (subst comp_fun_apply)
-apply (assumption |
+apply (assumption |
rule cont_fun Rp_cont emb_cont emb_rho_emb cpo_Dinf emb_chain_cpo)+
apply (subst rho_projpair [THEN Rp_unique])
prefer 5
@@ -2079,28 +2079,28 @@
lemma theta_chain: (* almost same proof as commute_chain *)
"[| commute(DD,ee,E,r); commute(DD,ee,G,f);
- emb_chain(DD,ee); cpo(E); cpo(G) |]
+ emb_chain(DD,ee); cpo(E); cpo(G) |]
==> chain(cf(E,G),\<lambda>n \<in> nat. f(n) O Rp(DD`n,E,r(n)))"
apply (rule chainI)
-apply (blast intro: lam_type cont_cf comp_pres_cont commute_emb Rp_cont
- emb_cont emb_chain_cpo,
+apply (blast intro: lam_type cont_cf comp_pres_cont commute_emb Rp_cont
+ emb_cont emb_chain_cpo,
simp)
apply (rule_tac r1 = r and m1 = n in commute_eq [THEN subst])
apply (rule_tac [5] r1 = f and m1 = n in commute_eq [THEN subst])
apply (assumption | rule le_succ nat_succI)+
apply (subst Rp_comp)
apply (assumption | rule emb_eps commute_emb emb_chain_cpo le_succ nat_succI)+
-apply (rule comp_assoc [THEN subst])
+apply (rule comp_assoc [THEN subst])
apply (rule_tac r1 = "f (succ (n))" in comp_assoc [THEN ssubst])
apply (rule comp_mono)
apply (blast intro: comp_pres_cont eps_cont emb_eps commute_emb Rp_cont
emb_cont emb_chain_cpo le_succ)+
apply (rule_tac b="f(succ(n))" in comp_id [THEN subst]) (* 1 subst too much *)
apply (rule_tac [2] comp_mono)
-apply (blast intro: comp_pres_cont eps_cont emb_eps emb_id commute_emb
+apply (blast intro: comp_pres_cont eps_cont emb_eps emb_id commute_emb
Rp_cont emb_cont cont_fun emb_chain_cpo le_succ)+
apply (subst comp_id) (* Undoes "1 subst too much", typing next anyway *)
-apply (blast intro: cont_fun Rp_cont emb_cont commute_emb cont_cf cpo_cf
+apply (blast intro: cont_fun Rp_cont emb_cont commute_emb cont_cf cpo_cf
emb_chain_cpo embRp_rel emb_eps le_succ)+
done
@@ -2109,7 +2109,7 @@
emb_chain(DD,ee); cpo(E); cpo(G) |]
==> chain(cf(G,E),\<lambda>n \<in> nat. r(n) O Rp(DD`n,G,f(n)))"
apply (rule chainI)
-apply (blast intro: lam_type cont_cf comp_pres_cont commute_emb Rp_cont
+apply (blast intro: lam_type cont_cf comp_pres_cont commute_emb Rp_cont
emb_cont emb_chain_cpo, simp)
apply (rule_tac r1 = r and m1 = n in commute_eq [THEN subst])
apply (rule_tac [5] r1 = f and m1 = n in commute_eq [THEN subst])
@@ -2119,14 +2119,14 @@
apply (rule comp_assoc [THEN subst]) (* comp_assoc is simpler in Isa *)
apply (rule_tac r1 = "r (succ (n))" in comp_assoc [THEN ssubst])
apply (rule comp_mono)
-apply (blast intro: comp_pres_cont eps_cont emb_eps commute_emb Rp_cont
+apply (blast intro: comp_pres_cont eps_cont emb_eps commute_emb Rp_cont
emb_cont emb_chain_cpo le_succ)+
apply (rule_tac b="r(succ(n))" in comp_id [THEN subst]) (* 1 subst too much *)
apply (rule_tac [2] comp_mono)
-apply (blast intro: comp_pres_cont eps_cont emb_eps emb_id commute_emb
+apply (blast intro: comp_pres_cont eps_cont emb_eps emb_id commute_emb
Rp_cont emb_cont cont_fun emb_chain_cpo le_succ)+
apply (subst comp_id) (* Undoes "1 subst too much", typing next anyway *)
-apply (blast intro: cont_fun Rp_cont emb_cont commute_emb cont_cf cpo_cf
+apply (blast intro: cont_fun Rp_cont emb_cont commute_emb cont_cf cpo_cf
emb_chain_cpo embRp_rel emb_eps le_succ)+
done
@@ -2139,7 +2139,7 @@
lemma commute_O_lemma:
"[| commute(DD,ee,E,r); commute(DD,ee,G,f);
- emb_chain(DD,ee); cpo(E); cpo(G); x \<in> nat |]
+ emb_chain(DD,ee); cpo(E); cpo(G); x \<in> nat |]
==> r(x) O Rp(DD ` x, G, f(x)) O f(x) O Rp(DD ` x, E, r(x)) =
r(x) O Rp(DD ` x, E, r(x))"
apply (rule_tac s1 = "f (x) " in comp_assoc [THEN subst])
@@ -2162,12 +2162,12 @@
apply (simp add: projpair_def rho_proj_def, safe)
apply (rule_tac [3] comp_lubs [THEN ssubst])
(* The following one line is 15 lines in HOL, and includes existentials. *)
-apply (assumption |
+apply (assumption |
rule cf_cont islub_in cpo_lub cpo_cf theta_chain theta_proj_chain)+
apply (simp (no_asm) add: comp_assoc)
apply (simp add: commute_O_lemma)
apply (subst comp_lubs)
-apply (assumption |
+apply (assumption |
rule cf_cont islub_in cpo_lub cpo_cf theta_chain theta_proj_chain)+
apply (simp (no_asm) add: comp_assoc)
apply (simp add: commute_O_lemma)
@@ -2184,14 +2184,14 @@
lemma emb_theta:
"[| lub(cf(E,E), \<lambda>n \<in> nat. r(n) O Rp(DD`n,E,r(n))) = id(set(E));
commute(DD,ee,E,r); commute(DD,ee,G,f);
- emb_chain(DD,ee); cpo(E); cpo(G) |]
+ emb_chain(DD,ee); cpo(E); cpo(G) |]
==> emb(E,G,lub(cf(E,G), \<lambda>n \<in> nat. f(n) O Rp(DD`n,E,r(n))))"
apply (simp add: emb_def)
apply (blast intro: theta_projpair)
done
lemma mono_lemma:
- "[| g \<in> cont(D,D'); cpo(D); cpo(D'); cpo(E) |]
+ "[| g \<in> cont(D,D'); cpo(D); cpo(D'); cpo(E) |]
==> (\<lambda>f \<in> cont(D',E). f O g) \<in> mono(cf(D',E),cf(D,E))"
apply (rule monoI)
apply (simp add: set_def cf_def)
@@ -2207,31 +2207,31 @@
((\<lambda>n \<in> nat. f(n) O Rp(DD ` n, E, r(n))) ` na)) =
(\<lambda>na \<in> nat. (f(na) O Rp(DD ` na, E, r(na))) O r(n))"
apply (rule fun_extension)
-(*something wrong here*)
+(*something wrong here*)
apply (auto simp del: beta_if simp add: beta intro: lam_type)
done
lemma chain_lemma:
"[| commute(DD,ee,E,r); commute(DD,ee,G,f);
- emb_chain(DD,ee); cpo(E); cpo(G); n \<in> nat |]
+ emb_chain(DD,ee); cpo(E); cpo(G); n \<in> nat |]
==> chain(cf(DD`n,G),\<lambda>x \<in> nat. (f(x) O Rp(DD ` x, E, r(x))) O r(n))"
apply (rule commute_lam_lemma [THEN subst])
-apply (blast intro: theta_chain emb_chain_cpo
+apply (blast intro: theta_chain emb_chain_cpo
commute_emb [THEN emb_cont, THEN mono_lemma, THEN mono_chain])+
done
lemma suffix_lemma:
"[| commute(DD,ee,E,r); commute(DD,ee,G,f);
- emb_chain(DD,ee); cpo(E); cpo(G); cpo(DD`x); x \<in> nat |]
- ==> suffix(\<lambda>n \<in> nat. (f(n) O Rp(DD`n,E,r(n))) O r(x),x) =
+ emb_chain(DD,ee); cpo(E); cpo(G); cpo(DD`x); x \<in> nat |]
+ ==> suffix(\<lambda>n \<in> nat. (f(n) O Rp(DD`n,E,r(n))) O r(x),x) =
(\<lambda>n \<in> nat. f(x))"
apply (simp add: suffix_def)
apply (rule lam_type [THEN fun_extension])
-apply (blast intro: lam_type comp_fun cont_fun Rp_cont emb_cont
+apply (blast intro: lam_type comp_fun cont_fun Rp_cont emb_cont
commute_emb emb_chain_cpo)+
apply simp
apply (rename_tac y)
-apply (subgoal_tac
+apply (subgoal_tac
"f(x#+y) O (Rp(DD`(x#+y), E, r(x#+y)) O r (x#+y)) O eps(DD, ee, x, x#+y)
= f(x)")
apply (simp add: comp_assoc commute_eq add_le_self)
@@ -2258,12 +2258,12 @@
apply (assumption | rule mediatingI emb_theta)+
apply (rule_tac b = "r (n) " in lub_const [THEN subst])
apply (rule_tac [3] comp_lubs [THEN ssubst])
-apply (blast intro: cont_cf emb_cont commute_emb cpo_cf theta_chain
+apply (blast intro: cont_cf emb_cont commute_emb cpo_cf theta_chain
chain_const emb_chain_cpo)+
apply (simp (no_asm))
apply (rule_tac n1 = n in lub_suffix [THEN subst])
apply (assumption | rule chain_lemma cpo_cf emb_chain_cpo)+
-apply (simp add: suffix_lemma lub_const cont_cf emb_cont commute_emb cpo_cf
+apply (simp add: suffix_lemma lub_const cont_cf emb_cont commute_emb cpo_cf
emb_chain_cpo)
done
@@ -2271,7 +2271,7 @@
"[| mediating(E,G,r,f,t);
lub(cf(E,E), \<lambda>n \<in> nat. r(n) O Rp(DD`n,E,r(n))) = id(set(E));
commute(DD,ee,E,r); commute(DD,ee,G,f);
- emb_chain(DD,ee); cpo(E); cpo(G) |]
+ emb_chain(DD,ee); cpo(E); cpo(G) |]
==> t = lub(cf(E,G), \<lambda>n \<in> nat. f(n) O Rp(DD`n,E,r(n)))"
apply (rule_tac b = t in comp_id [THEN subst])
apply (erule_tac [2] subst)
@@ -2294,11 +2294,11 @@
(Dinf(DD,ee),G,rho_emb(DD,ee),f,
lub(cf(Dinf(DD,ee),G),
\<lambda>n \<in> nat. f(n) O Rp(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n)))) &
- (\<forall>t. mediating(Dinf(DD,ee),G,rho_emb(DD,ee),f,t) -->
+ (\<forall>t. mediating(Dinf(DD,ee),G,rho_emb(DD,ee),f,t) \<longrightarrow>
t = lub(cf(Dinf(DD,ee),G),
\<lambda>n \<in> nat. f(n) O Rp(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n))))"
apply safe
-apply (assumption |
+apply (assumption |
rule lub_universal_mediating rho_emb_commute rho_emb_lub cpo_Dinf)+
apply (auto intro: lub_universal_unique rho_emb_commute rho_emb_lub cpo_Dinf)
done
--- a/src/ZF/ex/Primes.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/ex/Primes.thy Tue Mar 06 16:46:27 2012 +0000
@@ -14,7 +14,7 @@
definition
is_gcd :: "[i,i,i]=>o" --{*definition of great common divisor*} where
"is_gcd(p,m,n) == ((p dvd m) & (p dvd n)) &
- (\<forall>d\<in>nat. (d dvd m) & (d dvd n) --> d dvd p)"
+ (\<forall>d\<in>nat. (d dvd m) & (d dvd n) \<longrightarrow> d dvd p)"
definition
gcd :: "[i,i]=>i" --{*Euclid's algorithm for the gcd*} where
@@ -28,7 +28,7 @@
definition
prime :: i --{*the set of prime numbers*} where
- "prime == {p \<in> nat. 1<p & (\<forall>m \<in> nat. m dvd p --> m=1 | m=p)}"
+ "prime == {p \<in> nat. 1<p & (\<forall>m \<in> nat. m dvd p \<longrightarrow> m=1 | m=p)}"
subsection{*The Divides Relation*}
@@ -143,7 +143,7 @@
(*Imitating TFL*)
lemma gcd_induct_lemma [rule_format (no_asm)]: "[| n \<in> nat;
\<forall>m \<in> nat. P(m,0);
- \<forall>m \<in> nat. \<forall>n \<in> nat. 0<n --> P(n, m mod n) --> P(m,n) |]
+ \<forall>m \<in> nat. \<forall>n \<in> nat. 0<n \<longrightarrow> P(n, m mod n) \<longrightarrow> P(m,n) |]
==> \<forall>m \<in> nat. P (m,n)"
apply (erule_tac i = n in complete_induct)
apply (case_tac "x=0")
@@ -206,7 +206,7 @@
lemma gcd_greatest_raw [rule_format]:
"[| m \<in> nat; n \<in> nat; f \<in> nat |]
- ==> (f dvd m) --> (f dvd n) --> f dvd gcd(m,n)"
+ ==> (f dvd m) \<longrightarrow> (f dvd n) \<longrightarrow> f dvd gcd(m,n)"
apply (rule_tac m = m and n = n in gcd_induct)
apply (simp_all add: gcd_non_0 dvd_mod)
done
@@ -217,7 +217,7 @@
done
lemma gcd_greatest_iff [simp]: "[| k \<in> nat; m \<in> nat; n \<in> nat |]
- ==> (k dvd gcd (m, n)) <-> (k dvd m & k dvd n)"
+ ==> (k dvd gcd (m, n)) \<longleftrightarrow> (k dvd m & k dvd n)"
by (blast intro!: gcd_greatest gcd_dvd1 gcd_dvd2 intro: dvd_trans)
@@ -235,7 +235,7 @@
apply (blast intro: dvd_anti_sym)
done
-lemma is_gcd_commute: "is_gcd(k,m,n) <-> is_gcd(k,n,m)"
+lemma is_gcd_commute: "is_gcd(k,m,n) \<longleftrightarrow> is_gcd(k,n,m)"
by (simp add: is_gcd_def, blast)
lemma gcd_commute_raw: "[| m \<in> nat; n \<in> nat |] ==> gcd(m,n) = gcd(n,m)"
@@ -331,7 +331,7 @@
done
lemma relprime_dvd_mult_iff:
- "[| gcd (k,n) = 1; m \<in> nat |] ==> k dvd (m #* n) <-> k dvd m"
+ "[| gcd (k,n) = 1; m \<in> nat |] ==> k dvd (m #* n) \<longleftrightarrow> k dvd m"
by (blast intro: dvdI2 relprime_dvd_mult dvd_trans)
lemma prime_imp_relprime:
--- a/src/ZF/ex/Ramsey.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/ex/Ramsey.thy Tue Mar 06 16:46:27 2012 +0000
@@ -28,7 +28,7 @@
definition
Symmetric :: "i=>o" where
- "Symmetric(E) == (\<forall>x y. <x,y>:E --> <y,x>:E)"
+ "Symmetric(E) == (\<forall>x y. <x,y>:E \<longrightarrow> <y,x>:E)"
definition
Atleast :: "[i,i]=>o" where -- "not really necessary: ZF defines cardinality"
@@ -36,15 +36,15 @@
definition
Clique :: "[i,i,i]=>o" where
- "Clique(C,V,E) == (C \<subseteq> V) & (\<forall>x \<in> C. \<forall>y \<in> C. x\<noteq>y --> <x,y> \<in> E)"
+ "Clique(C,V,E) == (C \<subseteq> V) & (\<forall>x \<in> C. \<forall>y \<in> C. x\<noteq>y \<longrightarrow> <x,y> \<in> E)"
definition
Indept :: "[i,i,i]=>o" where
- "Indept(I,V,E) == (I \<subseteq> V) & (\<forall>x \<in> I. \<forall>y \<in> I. x\<noteq>y --> <x,y> \<notin> E)"
+ "Indept(I,V,E) == (I \<subseteq> V) & (\<forall>x \<in> I. \<forall>y \<in> I. x\<noteq>y \<longrightarrow> <x,y> \<notin> E)"
definition
Ramsey :: "[i,i,i]=>o" where
- "Ramsey(n,i,j) == \<forall>V E. Symmetric(E) & Atleast(n,V) -->
+ "Ramsey(n,i,j) == \<forall>V E. Symmetric(E) & Atleast(n,V) \<longrightarrow>
(\<exists>C. Clique(C,V,E) & Atleast(i,C)) |
(\<exists>I. Indept(I,V,E) & Atleast(j,I))"
@@ -93,7 +93,7 @@
the same proof could be used!!*)
lemma pigeon2 [rule_format]:
"m \<in> nat ==>
- \<forall>n \<in> nat. \<forall>A B. Atleast((m#+n) #- succ(0), A Un B) -->
+ \<forall>n \<in> nat. \<forall>A B. Atleast((m#+n) #- succ(0), A \<union> B) \<longrightarrow>
Atleast(m,A) | Atleast(n,B)"
apply (induct_tac "m")
apply (blast intro!: Atleast0, simp)
--- a/src/ZF/ex/Ring.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/ex/Ring.thy Tue Mar 06 16:46:27 2012 +0000
@@ -115,13 +115,13 @@
lemma (in abelian_group) a_l_cancel [simp]:
"\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
- \<Longrightarrow> (x \<oplus> y = x \<oplus> z) <-> (y = z)"
+ \<Longrightarrow> (x \<oplus> y = x \<oplus> z) \<longleftrightarrow> (y = z)"
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>
- \<Longrightarrow> (y \<oplus> x = z \<oplus> x) <-> (y = z)"
+ \<Longrightarrow> (y \<oplus> x = z \<oplus> x) \<longleftrightarrow> (y = z)"
by (rule group.r_cancel [OF a_group, simplified, simplified ring_add_def [symmetric]])
lemma (in abelian_monoid) a_assoc:
@@ -234,7 +234,7 @@
ring_hom :: "[i,i] => i" where
"ring_hom(R,S) ==
{h \<in> carrier(R) -> carrier(S).
- (\<forall>x y. x \<in> carrier(R) & y \<in> carrier(R) -->
+ (\<forall>x y. x \<in> carrier(R) & y \<in> carrier(R) \<longrightarrow>
h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y) &
h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)) &
h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>}"
--- a/src/ZF/ex/misc.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/ex/misc.thy Tue Mar 06 16:46:27 2012 +0000
@@ -31,16 +31,16 @@
text{*A weird property of ordered pairs.*}
-lemma "b\<noteq>c ==> <a,b> Int <a,c> = <a,a>"
+lemma "b\<noteq>c ==> <a,b> \<inter> <a,c> = <a,a>"
by (simp add: Pair_def Int_cons_left Int_cons_right doubleton_eq_iff, blast)
text{*These two are cited in Benzmueller and Kohlhase's system description of
LEO, CADE-15, 1998 (page 139-143) as theorems LEO could not prove.*}
-lemma "(X = Y Un Z) <-> (Y \<subseteq> X & Z \<subseteq> X & (\<forall>V. Y \<subseteq> V & Z \<subseteq> V --> X \<subseteq> V))"
+lemma "(X = Y \<union> Z) \<longleftrightarrow> (Y \<subseteq> X & Z \<subseteq> X & (\<forall>V. Y \<subseteq> V & Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
by (blast intro!: equalityI)
text{*the dual of the previous one*}
-lemma "(X = Y Int Z) <-> (X \<subseteq> Y & X \<subseteq> Z & (\<forall>V. V \<subseteq> Y & V \<subseteq> Z --> V \<subseteq> X))"
+lemma "(X = Y \<inter> Z) \<longleftrightarrow> (X \<subseteq> Y & X \<subseteq> Z & (\<forall>V. V \<subseteq> Y & V \<subseteq> Z \<longrightarrow> V \<subseteq> X))"
by (blast intro!: equalityI)
text{*trivial example of term synthesis: apparently hard for some provers!*}
@@ -52,18 +52,18 @@
by blast
text{*variant of the benchmark above*}
-lemma "\<forall>x \<in> S. Union(S) \<subseteq> x ==> \<exists>z. S \<subseteq> {z}"
+lemma "\<forall>x \<in> S. \<Union>(S) \<subseteq> x ==> \<exists>z. S \<subseteq> {z}"
by blast
(*Example 12 (credited to Peter Andrews) from
W. Bledsoe. A Maximal Method for Set Variables in Automatic Theorem-proving.
In: J. Hayes and D. Michie and L. Mikulich, eds. Machine Intelligence 9.
Ellis Horwood, 53-100 (1979). *)
-lemma "(\<forall>F. {x} \<in> F --> {y} \<in> F) --> (\<forall>A. x \<in> A --> y \<in> A)"
+lemma "(\<forall>F. {x} \<in> F \<longrightarrow> {y} \<in> F) \<longrightarrow> (\<forall>A. x \<in> A \<longrightarrow> y \<in> A)"
by best
text{*A characterization of functions suggested by Tobias Nipkow*}
-lemma "r \<in> domain(r)->B <-> r \<subseteq> domain(r)*B & (\<forall>X. r `` (r -`` X) \<subseteq> X)"
+lemma "r \<in> domain(r)->B \<longleftrightarrow> r \<subseteq> domain(r)*B & (\<forall>X. r `` (r -`` X) \<subseteq> X)"
by (unfold Pi_def function_def, best)
@@ -81,8 +81,8 @@
rewriting does not instantiate Vars.*)
lemma "(\<forall>A f B g. hom(A,f,B,g) =
{H \<in> A->B. f \<in> A*A->A & g \<in> B*B->B &
- (\<forall>x \<in> A. \<forall>y \<in> A. H`(f`<x,y>) = g`<H`x,H`y>)}) -->
- J \<in> hom(A,f,B,g) & K \<in> hom(B,g,C,h) -->
+ (\<forall>x \<in> A. \<forall>y \<in> A. H`(f`<x,y>) = g`<H`x,H`y>)}) \<longrightarrow>
+ J \<in> hom(A,f,B,g) & K \<in> hom(B,g,C,h) \<longrightarrow>
(K O J) \<in> hom(A,f,C,h)"
by force
@@ -90,7 +90,7 @@
lemma "(!! A f B g. hom(A,f,B,g) ==
{H \<in> A->B. f \<in> A*A->A & g \<in> B*B->B &
(\<forall>x \<in> A. \<forall>y \<in> A. H`(f`<x,y>) = g`<H`x,H`y>)})
- ==> J \<in> hom(A,f,B,g) & K \<in> hom(B,g,C,h) --> (K O J) \<in> hom(A,f,C,h)"
+ ==> J \<in> hom(A,f,B,g) & K \<in> hom(B,g,C,h) \<longrightarrow> (K O J) \<in> hom(A,f,C,h)"
by force