merged
authorpaulson
Fri Mar 16 16:29:51 2012 +0000 (2012-03-16)
changeset 46964f9533c462457
parent 46962 5bdcdb28be83
parent 46963 67da5904300a
child 46965 0c8fb96cce73
merged
     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)