--- a/src/ZF/Cardinal_AC.thy Thu Mar 15 23:06:22 2012 +0100
+++ b/src/ZF/Cardinal_AC.thy Fri Mar 16 16:29:28 2012 +0000
@@ -134,29 +134,38 @@
(*Kunen's Lemma 10.21*)
lemma cardinal_UN_le:
- "[| InfCard(K); \<forall>i\<in>K. |X(i)| \<le> K |] ==> |\<Union>i\<in>K. X(i)| \<le> K"
-apply (simp add: InfCard_is_Card le_Card_iff)
-apply (rule lepoll_trans)
- prefer 2
- apply (rule InfCard_square_eq [THEN eqpoll_imp_lepoll])
- apply (simp add: InfCard_is_Card Card_cardinal_eq)
-apply (unfold lepoll_def)
-apply (frule InfCard_is_Card [THEN Card_is_Ord])
-apply (erule AC_ball_Pi [THEN exE])
-apply (rule exI)
-(*Lemma needed in both subgoals, for a fixed z*)
-apply (subgoal_tac "\<forall>z\<in>(\<Union>i\<in>K. X (i)). z: X (LEAST i. z:X (i)) &
- (LEAST i. z:X (i)) \<in> K")
- prefer 2
- apply (fast intro!: Least_le [THEN lt_trans1, THEN ltD] ltI
- elim!: LeastI Ord_in_Ord)
-apply (rule_tac c = "%z. <LEAST i. z:X (i), f ` (LEAST i. z:X (i)) ` z>"
- and d = "%<i,j>. converse (f`i) ` j" in lam_injective)
-(*Instantiate the lemma proved above*)
-by (blast intro: inj_is_fun [THEN apply_type] dest: apply_type, force)
+ assumes K: "InfCard(K)"
+ shows "(!!i. i\<in>K ==> |X(i)| \<le> K) ==> |\<Union>i\<in>K. X(i)| \<le> K"
+proof (simp add: K InfCard_is_Card le_Card_iff)
+ have [intro]: "Ord(K)" by (blast intro: InfCard_is_Card Card_is_Ord K)
+ assume "!!i. i\<in>K ==> X(i) \<lesssim> K"
+ hence "!!i. i\<in>K ==> \<exists>f. f \<in> inj(X(i), K)" by (simp add: lepoll_def)
+ with AC_Pi obtain f where f: "f \<in> (\<Pi> i\<in>K. inj(X(i), K))"
+ apply - apply atomize apply auto done
+ { fix z
+ assume z: "z \<in> (\<Union>i\<in>K. X(i))"
+ then obtain i where i: "i \<in> K" "Ord(i)" "z \<in> X(i)"
+ by (blast intro: Ord_in_Ord [of K])
+ hence "(LEAST i. z \<in> X(i)) \<le> i" by (fast intro: Least_le)
+ hence "(LEAST i. z \<in> X(i)) < K" by (best intro: lt_trans1 ltI i)
+ hence "(LEAST i. z \<in> X(i)) \<in> K" and "z \<in> X(LEAST i. z \<in> X(i))"
+ by (auto intro: LeastI ltD i)
+ } note mems = this
+ have "(\<Union>i\<in>K. X(i)) \<lesssim> K \<times> K"
+ proof (unfold lepoll_def)
+ show "\<exists>f. f \<in> inj(\<Union>RepFun(K, X), K \<times> K)"
+ apply (rule exI)
+ apply (rule_tac c = "%z. \<langle>LEAST i. z \<in> X(i), f ` (LEAST i. z \<in> X(i)) ` z\<rangle>"
+ and d = "%\<langle>i,j\<rangle>. converse (f`i) ` j" in lam_injective)
+ apply (force intro: f inj_is_fun mems apply_type Perm.left_inverse)+
+ done
+ qed
+ also have "... \<approx> K"
+ by (simp add: K InfCard_square_eq InfCard_is_Card Card_cardinal_eq)
+ finally show "(\<Union>i\<in>K. X(i)) \<lesssim> K" .
+qed
-
-(*The same again, using csucc*)
+text{*The same again, using @{term csucc}*}
lemma cardinal_UN_lt_csucc:
"[| InfCard(K); \<forall>i\<in>K. |X(i)| < csucc(K) |]
==> |\<Union>i\<in>K. X(i)| < csucc(K)"
--- a/src/ZF/Constructible/Normal.thy Thu Mar 15 23:06:22 2012 +0100
+++ b/src/ZF/Constructible/Normal.thy Fri Mar 16 16:29:28 2012 +0000
@@ -226,7 +226,7 @@
by (simp add: Normal_def mono_Ord_def cont_Ord_def)
lemma mono_Ord_imp_Ord: "[| Ord(i); mono_Ord(F) |] ==> Ord(F(i))"
-apply (simp add: mono_Ord_def)
+apply (auto simp add: mono_Ord_def)
apply (blast intro: lt_Ord)
done
@@ -242,16 +242,29 @@
lemma Normal_imp_mono: "[| i<j; Normal(F) |] ==> F(i) < F(j)"
by (simp add: Normal_def mono_Ord_def)
-lemma Normal_increasing: "[| Ord(i); Normal(F) |] ==> i\<le>F(i)"
-apply (induct i rule: trans_induct3)
- apply (simp add: subset_imp_le)
- apply (subgoal_tac "F(x) < F(succ(x))")
- apply (force intro: lt_trans1)
- apply (simp add: Normal_def mono_Ord_def)
-apply (subgoal_tac "(\<Union>y<x. y) \<le> (\<Union>y<x. F(y))")
- apply (simp add: Normal_imp_cont Limit_OUN_eq)
-apply (blast intro: ltD le_implies_OUN_le_OUN)
-done
+lemma Normal_increasing:
+ assumes i: "Ord(i)" and F: "Normal(F)" shows"i \<le> F(i)"
+using i
+proof (induct i rule: trans_induct3)
+ case 0 thus ?case by (simp add: subset_imp_le F)
+next
+ case (succ i)
+ hence "F(i) < F(succ(i))" using F
+ by (simp add: Normal_def mono_Ord_def)
+ thus ?case using succ.hyps
+ by (blast intro: lt_trans1)
+next
+ case (limit l)
+ hence "l = (\<Union>y<l. y)"
+ by (simp add: Limit_OUN_eq)
+ also have "... \<le> (\<Union>y<l. F(y))" using limit
+ by (blast intro: ltD le_implies_OUN_le_OUN)
+ finally have "l \<le> (\<Union>y<l. F(y))" .
+ moreover have "(\<Union>y<l. F(y)) \<le> F(l)" using limit F
+ by (simp add: Normal_imp_cont lt_Ord)
+ ultimately show ?case
+ by (blast intro: le_trans)
+qed
subsubsection{*The class of fixedpoints is closed and unbounded*}
@@ -387,24 +400,32 @@
apply (simp_all add: ltD def_transrec2 [OF normalize_def])
done
-lemma normalize_lemma [rule_format]:
- "[| Ord(b); !!x. Ord(x) ==> Ord(F(x)) |]
- ==> \<forall>a. a < b \<longrightarrow> normalize(F, a) < normalize(F, b)"
-apply (erule trans_induct3)
- apply (simp_all add: le_iff def_transrec2 [OF normalize_def])
- apply clarify
-apply (rule Un_upper2_lt)
- apply auto
- apply (drule spec, drule mp, assumption)
- apply (erule leI)
-apply (drule Limit_has_succ, assumption)
-apply (blast intro!: Ord_normalize intro: OUN_upper_lt ltD lt_Ord)
-done
-
lemma normalize_increasing:
- "[| a < b; !!x. Ord(x) ==> Ord(F(x)) |]
- ==> normalize(F, a) < normalize(F, b)"
-by (blast intro!: normalize_lemma intro: lt_Ord2)
+ assumes ab: "a < b" and F: "!!x. Ord(x) ==> Ord(F(x))"
+ shows "normalize(F,a) < normalize(F,b)"
+proof -
+ { fix x
+ have "Ord(b)" using ab by (blast intro: lt_Ord2)
+ hence "x < b \<Longrightarrow> normalize(F,x) < normalize(F,b)"
+ proof (induct b arbitrary: x rule: trans_induct3)
+ case 0 thus ?case by simp
+ next
+ case (succ b)
+ thus ?case
+ by (auto simp add: le_iff def_transrec2 [OF normalize_def] intro: Un_upper2_lt F)
+ next
+ case (limit l)
+ hence sc: "succ(x) < l"
+ by (blast intro: Limit_has_succ)
+ hence "normalize(F,x) < normalize(F,succ(x))"
+ by (blast intro: limit elim: ltE)
+ hence "normalize(F,x) < (\<Union>j<l. normalize(F,j))"
+ by (blast intro: OUN_upper_lt lt_Ord F sc)
+ thus ?case using limit
+ by (simp add: def_transrec2 [OF normalize_def])
+ qed
+ } thus ?thesis using ab .
+qed
theorem Normal_normalize:
"(!!x. Ord(x) ==> Ord(F(x))) ==> Normal(normalize(F))"
@@ -414,14 +435,20 @@
done
theorem le_normalize:
- "[| Ord(a); cont_Ord(F); !!x. Ord(x) ==> Ord(F(x)) |]
- ==> F(a) \<le> normalize(F,a)"
-apply (erule trans_induct3)
-apply (simp_all add: def_transrec2 [OF normalize_def])
-apply (simp add: Un_upper1_le)
-apply (simp add: cont_Ord_def)
-apply (blast intro: ltD le_implies_OUN_le_OUN)
-done
+ assumes a: "Ord(a)" and coF: "cont_Ord(F)" and F: "!!x. Ord(x) ==> Ord(F(x))"
+ shows "F(a) \<le> normalize(F,a)"
+using a
+proof (induct a rule: trans_induct3)
+ case 0 thus ?case by (simp add: F def_transrec2 [OF normalize_def])
+next
+ case (succ a)
+ thus ?case
+ by (simp add: def_transrec2 [OF normalize_def] Un_upper1_le F )
+next
+ case (limit l)
+ thus ?case using F coF [unfolded cont_Ord_def]
+ by (simp add: def_transrec2 [OF normalize_def] le_implies_OUN_le_OUN ltD)
+qed
subsection {*The Alephs*}
@@ -442,18 +469,30 @@
def_transrec2 [OF Aleph_def])
done
-lemma Aleph_lemma [rule_format]:
- "Ord(b) ==> \<forall>a. a < b \<longrightarrow> Aleph(a) < Aleph(b)"
-apply (erule trans_induct3)
-apply (simp_all add: le_iff def_transrec2 [OF Aleph_def])
-apply (blast intro: lt_trans lt_csucc Card_is_Ord, clarify)
-apply (drule Limit_has_succ, assumption)
-apply (blast intro: Card_is_Ord Card_Aleph OUN_upper_lt ltD lt_Ord)
-done
-
lemma Aleph_increasing:
- "a < b ==> Aleph(a) < Aleph(b)"
-by (blast intro!: Aleph_lemma intro: lt_Ord2)
+ assumes ab: "a < b" shows "Aleph(a) < Aleph(b)"
+proof -
+ { fix x
+ have "Ord(b)" using ab by (blast intro: lt_Ord2)
+ hence "x < b \<Longrightarrow> Aleph(x) < Aleph(b)"
+ proof (induct b arbitrary: x rule: trans_induct3)
+ case 0 thus ?case by simp
+ next
+ case (succ b)
+ thus ?case
+ by (force simp add: le_iff def_transrec2 [OF Aleph_def]
+ intro: lt_trans lt_csucc Card_is_Ord)
+ next
+ case (limit l)
+ hence sc: "succ(x) < l"
+ by (blast intro: Limit_has_succ)
+ hence "\<aleph> x < (\<Union>j<l. \<aleph>j)" using limit
+ by (blast intro: OUN_upper_lt Card_is_Ord ltD lt_Ord)
+ thus ?case using limit
+ by (simp add: def_transrec2 [OF Aleph_def])
+ qed
+ } thus ?thesis using ab .
+qed
theorem Normal_Aleph: "Normal(Aleph)"
apply (rule NormalI)