1.1 --- a/src/ZF/Cardinal_AC.thy Fri Mar 16 15:51:53 2012 +0100
1.2 +++ b/src/ZF/Cardinal_AC.thy Fri Mar 16 16:29:51 2012 +0000
1.3 @@ -134,29 +134,38 @@
1.4
1.5 (*Kunen's Lemma 10.21*)
1.6 lemma cardinal_UN_le:
1.7 - "[| InfCard(K); \<forall>i\<in>K. |X(i)| \<le> K |] ==> |\<Union>i\<in>K. X(i)| \<le> K"
1.8 -apply (simp add: InfCard_is_Card le_Card_iff)
1.9 -apply (rule lepoll_trans)
1.10 - prefer 2
1.11 - apply (rule InfCard_square_eq [THEN eqpoll_imp_lepoll])
1.12 - apply (simp add: InfCard_is_Card Card_cardinal_eq)
1.13 -apply (unfold lepoll_def)
1.14 -apply (frule InfCard_is_Card [THEN Card_is_Ord])
1.15 -apply (erule AC_ball_Pi [THEN exE])
1.16 -apply (rule exI)
1.17 -(*Lemma needed in both subgoals, for a fixed z*)
1.18 -apply (subgoal_tac "\<forall>z\<in>(\<Union>i\<in>K. X (i)). z: X (LEAST i. z:X (i)) &
1.19 - (LEAST i. z:X (i)) \<in> K")
1.20 - prefer 2
1.21 - apply (fast intro!: Least_le [THEN lt_trans1, THEN ltD] ltI
1.22 - elim!: LeastI Ord_in_Ord)
1.23 -apply (rule_tac c = "%z. <LEAST i. z:X (i), f ` (LEAST i. z:X (i)) ` z>"
1.24 - and d = "%<i,j>. converse (f`i) ` j" in lam_injective)
1.25 -(*Instantiate the lemma proved above*)
1.26 -by (blast intro: inj_is_fun [THEN apply_type] dest: apply_type, force)
1.27 + assumes K: "InfCard(K)"
1.28 + shows "(!!i. i\<in>K ==> |X(i)| \<le> K) ==> |\<Union>i\<in>K. X(i)| \<le> K"
1.29 +proof (simp add: K InfCard_is_Card le_Card_iff)
1.30 + have [intro]: "Ord(K)" by (blast intro: InfCard_is_Card Card_is_Ord K)
1.31 + assume "!!i. i\<in>K ==> X(i) \<lesssim> K"
1.32 + hence "!!i. i\<in>K ==> \<exists>f. f \<in> inj(X(i), K)" by (simp add: lepoll_def)
1.33 + with AC_Pi obtain f where f: "f \<in> (\<Pi> i\<in>K. inj(X(i), K))"
1.34 + apply - apply atomize apply auto done
1.35 + { fix z
1.36 + assume z: "z \<in> (\<Union>i\<in>K. X(i))"
1.37 + then obtain i where i: "i \<in> K" "Ord(i)" "z \<in> X(i)"
1.38 + by (blast intro: Ord_in_Ord [of K])
1.39 + hence "(LEAST i. z \<in> X(i)) \<le> i" by (fast intro: Least_le)
1.40 + hence "(LEAST i. z \<in> X(i)) < K" by (best intro: lt_trans1 ltI i)
1.41 + hence "(LEAST i. z \<in> X(i)) \<in> K" and "z \<in> X(LEAST i. z \<in> X(i))"
1.42 + by (auto intro: LeastI ltD i)
1.43 + } note mems = this
1.44 + have "(\<Union>i\<in>K. X(i)) \<lesssim> K \<times> K"
1.45 + proof (unfold lepoll_def)
1.46 + show "\<exists>f. f \<in> inj(\<Union>RepFun(K, X), K \<times> K)"
1.47 + apply (rule exI)
1.48 + apply (rule_tac c = "%z. \<langle>LEAST i. z \<in> X(i), f ` (LEAST i. z \<in> X(i)) ` z\<rangle>"
1.49 + and d = "%\<langle>i,j\<rangle>. converse (f`i) ` j" in lam_injective)
1.50 + apply (force intro: f inj_is_fun mems apply_type Perm.left_inverse)+
1.51 + done
1.52 + qed
1.53 + also have "... \<approx> K"
1.54 + by (simp add: K InfCard_square_eq InfCard_is_Card Card_cardinal_eq)
1.55 + finally show "(\<Union>i\<in>K. X(i)) \<lesssim> K" .
1.56 +qed
1.57
1.58 -
1.59 -(*The same again, using csucc*)
1.60 +text{*The same again, using @{term csucc}*}
1.61 lemma cardinal_UN_lt_csucc:
1.62 "[| InfCard(K); \<forall>i\<in>K. |X(i)| < csucc(K) |]
1.63 ==> |\<Union>i\<in>K. X(i)| < csucc(K)"
2.1 --- a/src/ZF/Constructible/Normal.thy Fri Mar 16 15:51:53 2012 +0100
2.2 +++ b/src/ZF/Constructible/Normal.thy Fri Mar 16 16:29:51 2012 +0000
2.3 @@ -226,7 +226,7 @@
2.4 by (simp add: Normal_def mono_Ord_def cont_Ord_def)
2.5
2.6 lemma mono_Ord_imp_Ord: "[| Ord(i); mono_Ord(F) |] ==> Ord(F(i))"
2.7 -apply (simp add: mono_Ord_def)
2.8 +apply (auto simp add: mono_Ord_def)
2.9 apply (blast intro: lt_Ord)
2.10 done
2.11
2.12 @@ -242,16 +242,29 @@
2.13 lemma Normal_imp_mono: "[| i<j; Normal(F) |] ==> F(i) < F(j)"
2.14 by (simp add: Normal_def mono_Ord_def)
2.15
2.16 -lemma Normal_increasing: "[| Ord(i); Normal(F) |] ==> i\<le>F(i)"
2.17 -apply (induct i rule: trans_induct3)
2.18 - apply (simp add: subset_imp_le)
2.19 - apply (subgoal_tac "F(x) < F(succ(x))")
2.20 - apply (force intro: lt_trans1)
2.21 - apply (simp add: Normal_def mono_Ord_def)
2.22 -apply (subgoal_tac "(\<Union>y<x. y) \<le> (\<Union>y<x. F(y))")
2.23 - apply (simp add: Normal_imp_cont Limit_OUN_eq)
2.24 -apply (blast intro: ltD le_implies_OUN_le_OUN)
2.25 -done
2.26 +lemma Normal_increasing:
2.27 + assumes i: "Ord(i)" and F: "Normal(F)" shows"i \<le> F(i)"
2.28 +using i
2.29 +proof (induct i rule: trans_induct3)
2.30 + case 0 thus ?case by (simp add: subset_imp_le F)
2.31 +next
2.32 + case (succ i)
2.33 + hence "F(i) < F(succ(i))" using F
2.34 + by (simp add: Normal_def mono_Ord_def)
2.35 + thus ?case using succ.hyps
2.36 + by (blast intro: lt_trans1)
2.37 +next
2.38 + case (limit l)
2.39 + hence "l = (\<Union>y<l. y)"
2.40 + by (simp add: Limit_OUN_eq)
2.41 + also have "... \<le> (\<Union>y<l. F(y))" using limit
2.42 + by (blast intro: ltD le_implies_OUN_le_OUN)
2.43 + finally have "l \<le> (\<Union>y<l. F(y))" .
2.44 + moreover have "(\<Union>y<l. F(y)) \<le> F(l)" using limit F
2.45 + by (simp add: Normal_imp_cont lt_Ord)
2.46 + ultimately show ?case
2.47 + by (blast intro: le_trans)
2.48 +qed
2.49
2.50
2.51 subsubsection{*The class of fixedpoints is closed and unbounded*}
2.52 @@ -387,24 +400,32 @@
2.53 apply (simp_all add: ltD def_transrec2 [OF normalize_def])
2.54 done
2.55
2.56 -lemma normalize_lemma [rule_format]:
2.57 - "[| Ord(b); !!x. Ord(x) ==> Ord(F(x)) |]
2.58 - ==> \<forall>a. a < b \<longrightarrow> normalize(F, a) < normalize(F, b)"
2.59 -apply (erule trans_induct3)
2.60 - apply (simp_all add: le_iff def_transrec2 [OF normalize_def])
2.61 - apply clarify
2.62 -apply (rule Un_upper2_lt)
2.63 - apply auto
2.64 - apply (drule spec, drule mp, assumption)
2.65 - apply (erule leI)
2.66 -apply (drule Limit_has_succ, assumption)
2.67 -apply (blast intro!: Ord_normalize intro: OUN_upper_lt ltD lt_Ord)
2.68 -done
2.69 -
2.70 lemma normalize_increasing:
2.71 - "[| a < b; !!x. Ord(x) ==> Ord(F(x)) |]
2.72 - ==> normalize(F, a) < normalize(F, b)"
2.73 -by (blast intro!: normalize_lemma intro: lt_Ord2)
2.74 + assumes ab: "a < b" and F: "!!x. Ord(x) ==> Ord(F(x))"
2.75 + shows "normalize(F,a) < normalize(F,b)"
2.76 +proof -
2.77 + { fix x
2.78 + have "Ord(b)" using ab by (blast intro: lt_Ord2)
2.79 + hence "x < b \<Longrightarrow> normalize(F,x) < normalize(F,b)"
2.80 + proof (induct b arbitrary: x rule: trans_induct3)
2.81 + case 0 thus ?case by simp
2.82 + next
2.83 + case (succ b)
2.84 + thus ?case
2.85 + by (auto simp add: le_iff def_transrec2 [OF normalize_def] intro: Un_upper2_lt F)
2.86 + next
2.87 + case (limit l)
2.88 + hence sc: "succ(x) < l"
2.89 + by (blast intro: Limit_has_succ)
2.90 + hence "normalize(F,x) < normalize(F,succ(x))"
2.91 + by (blast intro: limit elim: ltE)
2.92 + hence "normalize(F,x) < (\<Union>j<l. normalize(F,j))"
2.93 + by (blast intro: OUN_upper_lt lt_Ord F sc)
2.94 + thus ?case using limit
2.95 + by (simp add: def_transrec2 [OF normalize_def])
2.96 + qed
2.97 + } thus ?thesis using ab .
2.98 +qed
2.99
2.100 theorem Normal_normalize:
2.101 "(!!x. Ord(x) ==> Ord(F(x))) ==> Normal(normalize(F))"
2.102 @@ -414,14 +435,20 @@
2.103 done
2.104
2.105 theorem le_normalize:
2.106 - "[| Ord(a); cont_Ord(F); !!x. Ord(x) ==> Ord(F(x)) |]
2.107 - ==> F(a) \<le> normalize(F,a)"
2.108 -apply (erule trans_induct3)
2.109 -apply (simp_all add: def_transrec2 [OF normalize_def])
2.110 -apply (simp add: Un_upper1_le)
2.111 -apply (simp add: cont_Ord_def)
2.112 -apply (blast intro: ltD le_implies_OUN_le_OUN)
2.113 -done
2.114 + assumes a: "Ord(a)" and coF: "cont_Ord(F)" and F: "!!x. Ord(x) ==> Ord(F(x))"
2.115 + shows "F(a) \<le> normalize(F,a)"
2.116 +using a
2.117 +proof (induct a rule: trans_induct3)
2.118 + case 0 thus ?case by (simp add: F def_transrec2 [OF normalize_def])
2.119 +next
2.120 + case (succ a)
2.121 + thus ?case
2.122 + by (simp add: def_transrec2 [OF normalize_def] Un_upper1_le F )
2.123 +next
2.124 + case (limit l)
2.125 + thus ?case using F coF [unfolded cont_Ord_def]
2.126 + by (simp add: def_transrec2 [OF normalize_def] le_implies_OUN_le_OUN ltD)
2.127 +qed
2.128
2.129
2.130 subsection {*The Alephs*}
2.131 @@ -442,18 +469,30 @@
2.132 def_transrec2 [OF Aleph_def])
2.133 done
2.134
2.135 -lemma Aleph_lemma [rule_format]:
2.136 - "Ord(b) ==> \<forall>a. a < b \<longrightarrow> Aleph(a) < Aleph(b)"
2.137 -apply (erule trans_induct3)
2.138 -apply (simp_all add: le_iff def_transrec2 [OF Aleph_def])
2.139 -apply (blast intro: lt_trans lt_csucc Card_is_Ord, clarify)
2.140 -apply (drule Limit_has_succ, assumption)
2.141 -apply (blast intro: Card_is_Ord Card_Aleph OUN_upper_lt ltD lt_Ord)
2.142 -done
2.143 -
2.144 lemma Aleph_increasing:
2.145 - "a < b ==> Aleph(a) < Aleph(b)"
2.146 -by (blast intro!: Aleph_lemma intro: lt_Ord2)
2.147 + assumes ab: "a < b" shows "Aleph(a) < Aleph(b)"
2.148 +proof -
2.149 + { fix x
2.150 + have "Ord(b)" using ab by (blast intro: lt_Ord2)
2.151 + hence "x < b \<Longrightarrow> Aleph(x) < Aleph(b)"
2.152 + proof (induct b arbitrary: x rule: trans_induct3)
2.153 + case 0 thus ?case by simp
2.154 + next
2.155 + case (succ b)
2.156 + thus ?case
2.157 + by (force simp add: le_iff def_transrec2 [OF Aleph_def]
2.158 + intro: lt_trans lt_csucc Card_is_Ord)
2.159 + next
2.160 + case (limit l)
2.161 + hence sc: "succ(x) < l"
2.162 + by (blast intro: Limit_has_succ)
2.163 + hence "\<aleph> x < (\<Union>j<l. \<aleph>j)" using limit
2.164 + by (blast intro: OUN_upper_lt Card_is_Ord ltD lt_Ord)
2.165 + thus ?case using limit
2.166 + by (simp add: def_transrec2 [OF Aleph_def])
2.167 + qed
2.168 + } thus ?thesis using ab .
2.169 +qed
2.170
2.171 theorem Normal_Aleph: "Normal(Aleph)"
2.172 apply (rule NormalI)