--- a/src/ZF/AC/HH.thy Thu Mar 15 16:35:02 2012 +0000
+++ b/src/ZF/AC/HH.thy Thu Mar 15 17:38:05 2012 +0000
@@ -98,7 +98,7 @@
done
lemma HH_subset_x_imp_lepoll:
- "[| HH(f, x, i) \<in> Pow(x)-{0}; Ord(i) |] ==> i lepoll Pow(x)-{0}"
+ "[| HH(f, x, i) \<in> Pow(x)-{0}; Ord(i) |] ==> i \<lesssim> Pow(x)-{0}"
apply (unfold lepoll_def inj_def)
apply (rule_tac x = "\<lambda>j \<in> i. HH (f, x, j) " in exI)
apply (simp (no_asm_simp))
--- a/src/ZF/AC/WO2_AC16.thy Thu Mar 15 16:35:02 2012 +0000
+++ b/src/ZF/AC/WO2_AC16.thy Thu Mar 15 17:38:05 2012 +0000
@@ -177,7 +177,7 @@
done
lemma Union_lesspoll:
- "[| \<forall>x \<in> X. x lepoll n & x \<subseteq> T; well_ord(T, R); X lepoll b;
+ "[| \<forall>x \<in> X. x \<lesssim> n & x \<subseteq> T; well_ord(T, R); X \<lesssim> b;
b<a; ~Finite(a); Card(a); n \<in> nat |]
==> \<Union>(X)\<prec>a"
apply (case_tac "Finite (X)")
@@ -203,7 +203,7 @@
lemma Un_sing_eq_cons: "A \<union> {a} = cons(a, A)"
by fast
-lemma Un_lepoll_succ: "A lepoll B ==> A \<union> {a} lepoll succ(B)"
+lemma Un_lepoll_succ: "A \<lesssim> B ==> A \<union> {a} \<lesssim> succ(B)"
apply (simp add: Un_sing_eq_cons succ_def)
apply (blast elim!: mem_irrefl intro: cons_lepoll_cong)
done
@@ -216,7 +216,7 @@
lemma recfunAC16_Diff_lepoll_1:
"Ord(x)
- ==> recfunAC16(f, g, x, a) - (\<Union>i<x. recfunAC16(f, g, i, a)) lepoll 1"
+ ==> recfunAC16(f, g, x, a) - (\<Union>i<x. recfunAC16(f, g, i, a)) \<lesssim> 1"
apply (erule Ord_cases)
apply (simp add: recfunAC16_0 empty_subsetI [THEN subset_imp_lepoll])
(*Limit case*)
@@ -247,13 +247,13 @@
done
-lemma two_in_lepoll_1: "[| A lepoll 1; a \<in> A; b \<in> A |] ==> a=b"
+lemma two_in_lepoll_1: "[| A \<lesssim> 1; a \<in> A; b \<in> A |] ==> a=b"
by (fast dest!: lepoll_1_is_sing)
lemma UN_lepoll_index:
- "[| \<forall>i<a. F(i)-(\<Union>j<i. F(j)) lepoll 1; Limit(a) |]
- ==> (\<Union>x<a. F(x)) lepoll a"
+ "[| \<forall>i<a. F(i)-(\<Union>j<i. F(j)) \<lesssim> 1; Limit(a) |]
+ ==> (\<Union>x<a. F(x)) \<lesssim> a"
apply (rule lepoll_def [THEN def_imp_iff [THEN iffD2]])
apply (rule_tac x = "\<lambda>z \<in> (\<Union>x<a. F (x)). LEAST i. z \<in> F (i) " in exI)
apply (unfold inj_def)
@@ -271,7 +271,7 @@
done
-lemma recfunAC16_lepoll_index: "Ord(y) ==> recfunAC16(f, h, y, a) lepoll y"
+lemma recfunAC16_lepoll_index: "Ord(y) ==> recfunAC16(f, h, y, a) \<lesssim> y"
apply (erule trans_induct3)
(*0 case*)
apply (simp (no_asm_simp) add: recfunAC16_0 lepoll_refl)
@@ -369,7 +369,7 @@
lemma subset_imp_eq_lemma:
- "m \<in> nat ==> \<forall>A B. A \<subseteq> B & m lepoll A & B lepoll m \<longrightarrow> A=B"
+ "m \<in> nat ==> \<forall>A B. A \<subseteq> B & m \<lesssim> A & B \<lesssim> m \<longrightarrow> A=B"
apply (induct_tac "m")
apply (fast dest!: lepoll_0_is_0)
apply (intro allI impI)
@@ -385,7 +385,7 @@
done
-lemma subset_imp_eq: "[| A \<subseteq> B; m lepoll A; B lepoll m; m \<in> nat |] ==> A=B"
+lemma subset_imp_eq: "[| A \<subseteq> B; m \<lesssim> A; B \<lesssim> m; m \<in> nat |] ==> A=B"
by (blast dest!: subset_imp_eq_lemma)
--- a/src/ZF/Cardinal_AC.thy Thu Mar 15 16:35:02 2012 +0000
+++ b/src/ZF/Cardinal_AC.thy Thu Mar 15 17:38:05 2012 +0000
@@ -11,7 +11,7 @@
subsection{*Strengthened Forms of Existing Theorems on Cardinals*}
-lemma cardinal_eqpoll: "|A| eqpoll A"
+lemma cardinal_eqpoll: "|A| \<approx> A"
apply (rule AC_well_ord [THEN exE])
apply (erule well_ord_cardinal_eqpoll)
done
@@ -19,13 +19,13 @@
text{*The theorem @{term "||A|| = |A|"} *}
lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, simp]
-lemma cardinal_eqE: "|X| = |Y| ==> X eqpoll Y"
+lemma cardinal_eqE: "|X| = |Y| ==> X \<approx> Y"
apply (rule AC_well_ord [THEN exE])
apply (rule AC_well_ord [THEN exE])
apply (rule well_ord_cardinal_eqE, assumption+)
done
-lemma cardinal_eqpoll_iff: "|X| = |Y| \<longleftrightarrow> X eqpoll Y"
+lemma cardinal_eqpoll_iff: "|X| = |Y| \<longleftrightarrow> X \<approx> Y"
by (blast intro: cardinal_cong cardinal_eqE)
lemma cardinal_disjoint_Un:
@@ -33,7 +33,7 @@
==> |A \<union> C| = |B \<union> D|"
by (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un)
-lemma lepoll_imp_Card_le: "A lepoll B ==> |A| \<le> |B|"
+lemma lepoll_imp_Card_le: "A \<lesssim> B ==> |A| \<le> |B|"
apply (rule AC_well_ord [THEN exE])
apply (erule well_ord_lepoll_imp_Card_le, assumption)
done
@@ -59,7 +59,7 @@
apply (rule well_ord_cadd_cmult_distrib, assumption+)
done
-lemma InfCard_square_eq: "InfCard(|A|) ==> A*A eqpoll A"
+lemma InfCard_square_eq: "InfCard(|A|) ==> A*A \<approx> A"
apply (rule AC_well_ord [THEN exE])
apply (erule well_ord_InfCard_square_eq, assumption)
done
@@ -67,36 +67,50 @@
subsection {*The relationship between cardinality and le-pollence*}
-lemma Card_le_imp_lepoll: "|A| \<le> |B| ==> A lepoll B"
-apply (rule cardinal_eqpoll
- [THEN eqpoll_sym, THEN eqpoll_imp_lepoll, THEN lepoll_trans])
-apply (erule le_imp_subset [THEN subset_imp_lepoll, THEN lepoll_trans])
-apply (rule cardinal_eqpoll [THEN eqpoll_imp_lepoll])
-done
+lemma Card_le_imp_lepoll:
+ assumes "|A| \<le> |B|" shows "A \<lesssim> B"
+proof -
+ have "A \<approx> |A|"
+ by (rule cardinal_eqpoll [THEN eqpoll_sym])
+ also have "... \<lesssim> |B|"
+ by (rule le_imp_subset [THEN subset_imp_lepoll]) (rule assms)
+ also have "... \<approx> B"
+ by (rule cardinal_eqpoll)
+ finally show ?thesis .
+qed
-lemma le_Card_iff: "Card(K) ==> |A| \<le> K \<longleftrightarrow> A lepoll K"
+lemma le_Card_iff: "Card(K) ==> |A| \<le> K \<longleftrightarrow> A \<lesssim> K"
apply (erule Card_cardinal_eq [THEN subst], rule iffI,
erule Card_le_imp_lepoll)
apply (erule lepoll_imp_Card_le)
done
-lemma cardinal_0_iff_0 [simp]: "|A| = 0 \<longleftrightarrow> A = 0";
+lemma cardinal_0_iff_0 [simp]: "|A| = 0 \<longleftrightarrow> A = 0"
apply auto
apply (drule cardinal_0 [THEN ssubst])
apply (blast intro: eqpoll_0_iff [THEN iffD1] cardinal_eqpoll_iff [THEN iffD1])
done
-lemma cardinal_lt_iff_lesspoll: "Ord(i) ==> i < |A| \<longleftrightarrow> i lesspoll A"
-apply (cut_tac A = "A" in cardinal_eqpoll)
-apply (auto simp add: eqpoll_iff)
-apply (blast intro: lesspoll_trans2 lt_Card_imp_lesspoll Card_cardinal)
-apply (force intro: cardinal_lt_imp_lt lesspoll_cardinal_lt lesspoll_trans2
- simp add: cardinal_idem)
-done
+lemma cardinal_lt_iff_lesspoll:
+ assumes i: "Ord(i)" shows "i < |A| \<longleftrightarrow> i \<prec> A"
+proof
+ assume "i < |A|"
+ hence "i \<prec> |A|"
+ by (blast intro: lt_Card_imp_lesspoll Card_cardinal)
+ also have "... \<approx> A"
+ by (rule cardinal_eqpoll)
+ finally show "i \<prec> A" .
+next
+ assume "i \<prec> A"
+ also have "... \<approx> |A|"
+ by (blast intro: cardinal_eqpoll eqpoll_sym)
+ finally have "i \<prec> |A|" .
+ thus "i < |A|" using i
+ by (force intro: cardinal_lt_imp_lt lesspoll_cardinal_lt)
+qed
lemma cardinal_le_imp_lepoll: " i \<le> |A| ==> i \<lesssim> A"
-apply (blast intro: lt_Ord Card_le_imp_lepoll Ord_cardinal_le le_trans)
-done
+ by (blast intro: lt_Ord Card_le_imp_lepoll Ord_cardinal_le le_trans)
subsection{*Other Applications of AC*}
@@ -164,15 +178,21 @@
set need not be a cardinal. Surprisingly complicated proof!
**)
-(*Work backwards along the injection from W into K, given that @{term"W\<noteq>0"}.*)
+text{*Work backwards along the injection from @{term W} into @{term K}, given that @{term"W\<noteq>0"}.*}
+
lemma inj_UN_subset:
- "[| f: inj(A,B); a:A |] ==>
- (\<Union>x\<in>A. C(x)) \<subseteq> (\<Union>y\<in>B. C(if y: range(f) then converse(f)`y else a))"
-apply (rule UN_least)
-apply (rule_tac x1= "f`x" in subset_trans [OF _ UN_upper])
- apply (simp add: inj_is_fun [THEN apply_rangeI])
-apply (blast intro: inj_is_fun [THEN apply_type])
-done
+ assumes f: "f \<in> inj(A,B)" and a: "a \<in> A"
+ shows "(\<Union>x\<in>A. C(x)) \<subseteq> (\<Union>y\<in>B. C(if y \<in> range(f) then converse(f)`y else a))"
+proof (rule UN_least)
+ fix x
+ assume x: "x \<in> A"
+ hence fx: "f ` x \<in> B" by (blast intro: f inj_is_fun [THEN apply_type])
+ have "C(x) \<subseteq> C(if f ` x \<in> range(f) then converse(f) ` (f ` x) else a)"
+ using f x by (simp add: inj_is_fun [THEN apply_rangeI])
+ also have "... \<subseteq> (\<Union>y\<in>B. C(if y \<in> range(f) then converse(f) ` y else a))"
+ by (rule UN_upper [OF fx])
+ finally show "C(x) \<subseteq> (\<Union>y\<in>B. C(if y \<in> range(f) then converse(f)`y else a))" .
+qed
(*Simpler to require |W|=K; we'd have a bijection; but the theorem would
be weaker.*)
--- a/src/ZF/Nat_ZF.thy Thu Mar 15 16:35:02 2012 +0000
+++ b/src/ZF/Nat_ZF.thy Thu Mar 15 17:38:05 2012 +0000
@@ -92,7 +92,7 @@
lemma natE:
assumes "n \<in> nat"
- obtains (0) "n=0" | (succ) x where "x \<in> nat" "n=succ(x)"
+ obtains ("0") "n=0" | (succ) x where "x \<in> nat" "n=succ(x)"
using assms
by (rule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE]) auto
--- a/src/ZF/Ordinal.thy Thu Mar 15 16:35:02 2012 +0000
+++ b/src/ZF/Ordinal.thy Thu Mar 15 17:38:05 2012 +0000
@@ -703,7 +703,7 @@
lemma Ord_cases:
assumes i: "Ord(i)"
- obtains (0) "i=0" | (succ) j where "Ord(j)" "i=succ(j)" | (limit) "Limit(i)"
+ obtains ("0") "i=0" | (succ) j where "Ord(j)" "i=succ(j)" | (limit) "Limit(i)"
by (insert Ord_cases_disj [OF i], auto)
lemma trans_induct3_raw:
--- a/src/ZF/UNITY/AllocBase.thy Thu Mar 15 16:35:02 2012 +0000
+++ b/src/ZF/UNITY/AllocBase.thy Thu Mar 15 17:38:05 2012 +0000
@@ -342,7 +342,7 @@
apply (simp add: length_nat_list_inj)
done
-lemma nat_lepoll_var: "nat lepoll var"
+lemma nat_lepoll_var: "nat \<lesssim> var"
apply (unfold lepoll_def)
apply (rule_tac x = " (\<lambda>x\<in>nat. nat_var_inj (x))" in exI)
apply (rule var_infinite_lemma)