src/HOL/Cardinals/Cardinal_Arithmetic.thy
changeset 51782 84e7225f5ab6
parent 49310 6e30078de4f0
child 51806 5c53d40a8eed
     1.1 --- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Thu Apr 25 18:27:26 2013 +0200
     1.2 +++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Thu Apr 25 19:18:20 2013 +0200
     1.3 @@ -72,8 +72,8 @@
     1.4  using card_of_empty_ordIso by (simp add: czero_def)
     1.5  
     1.6  lemma card_of_ordIso_czero_iff_empty:
     1.7 -  "|A| =o (czero :: 'a rel) \<longleftrightarrow> A = ({} :: 'a set)"
     1.8 -unfolding czero_def by (rule iffI[OF card_of_empty2]) (auto simp: card_of_refl)
     1.9 +  "|A| =o (czero :: 'b rel) \<longleftrightarrow> A = ({} :: 'a set)"
    1.10 +unfolding czero_def by (rule iffI[OF card_of_empty2]) (auto simp: card_of_refl card_of_empty_ordIso)
    1.11  
    1.12  (* A "not czero" Cardinal predicate *)
    1.13  abbreviation Cnotzero where
    1.14 @@ -389,8 +389,7 @@
    1.15  
    1.16  lemma cexp_mono':
    1.17    assumes 1: "p1 \<le>o r1" and 2: "p2 \<le>o r2"
    1.18 -  and n1: "Field p1 \<noteq> {} \<or> cone \<le>o r1 ^c r2"
    1.19 -  and n2: "Field p2 = {} \<Longrightarrow> Field r2 = {}"
    1.20 +  and n: "Field p2 = {} \<Longrightarrow> Field r2 = {}"
    1.21    shows "p1 ^c p2 \<le>o r1 ^c r2"
    1.22  proof(cases "Field p1 = {}")
    1.23    case True
    1.24 @@ -399,7 +398,18 @@
    1.25      by (cases "Field p2 = {}", auto intro: card_of_ordLeqI2 simp: Func_empty)
    1.26         (metis Func_is_emp card_of_empty ex_in_conv)
    1.27    hence "p1 ^c p2 \<le>o cone" by (simp add: Field_card_of cexp_def)
    1.28 -  thus ?thesis using True n1 ordLeq_transitive by auto
    1.29 +  thus ?thesis
    1.30 +  proof (cases "Field p2 = {}")
    1.31 +    case True
    1.32 +    with n have "Field r2 = {}" .
    1.33 +    hence "cone \<le>o r1 ^c r2" unfolding cone_def cexp_def Func_def by (auto intro: card_of_ordLeqI)
    1.34 +    thus ?thesis using `p1 ^c p2 \<le>o cone` ordLeq_transitive by auto
    1.35 +  next
    1.36 +    case False with True have "|Field (p1 ^c p2)| =o czero"
    1.37 +      unfolding card_of_ordIso_czero_iff_empty cexp_def Func_is_emp Field_card_of by blast
    1.38 +    thus ?thesis unfolding cexp_def card_of_ordIso_czero_iff_empty Field_card_of
    1.39 +      by (simp add: card_of_empty)
    1.40 +  qed
    1.41  next
    1.42    case False
    1.43    have 1: "|Field p1| \<le>o |Field r1|" and 2: "|Field p2| \<le>o |Field r2|"
    1.44 @@ -409,7 +419,7 @@
    1.45    obtain f2 where f2: "inj_on f2 (Field p2)" "f2 ` Field p2 \<subseteq> Field r2"
    1.46      using 2 unfolding card_of_ordLeq[symmetric] by blast
    1.47    have 0: "Func_map (Field p2) f1 f2 ` (Field (r1 ^c r2)) = Field (p1 ^c p2)"
    1.48 -    unfolding cexp_def Field_card_of using Func_map_surj[OF f1 f2 n2, symmetric] .
    1.49 +    unfolding cexp_def Field_card_of using Func_map_surj[OF f1 f2 n, symmetric] .
    1.50    have 00: "Field (p1 ^c p2) \<noteq> {}" unfolding cexp_def Field_card_of Func_is_emp
    1.51      using False by simp
    1.52    show ?thesis
    1.53 @@ -418,57 +428,36 @@
    1.54  
    1.55  lemma cexp_mono:
    1.56    assumes 1: "p1 \<le>o r1" and 2: "p2 \<le>o r2"
    1.57 -  and n1: "Cnotzero p1 \<or> cone \<le>o r1 ^c r2"
    1.58 -  and n2: "p2 =o czero \<Longrightarrow> r2 =o czero" and card: "Card_order p2"
    1.59 +  and n: "p2 =o czero \<Longrightarrow> r2 =o czero" and card: "Card_order p2"
    1.60    shows "p1 ^c p2 \<le>o r1 ^c r2"
    1.61 -proof (rule cexp_mono'[OF 1 2])
    1.62 -  show "Field p1 \<noteq> {} \<or> cone \<le>o r1 ^c r2"
    1.63 -  proof (cases "Cnotzero p1")
    1.64 -    case True show ?thesis using Cnotzero_imp_not_empty[OF True] by (rule disjI1)
    1.65 -  next
    1.66 -    case False with n1 show ?thesis by blast
    1.67 -  qed
    1.68 -qed (rule czeroI[OF card, THEN n2, THEN czeroE])
    1.69 +  by (metis (full_types) "1" "2" card cexp_mono' czeroE czeroI n)
    1.70  
    1.71  lemma cexp_mono1:
    1.72 -  assumes 1: "p1 \<le>o r1"
    1.73 -  and n1: "Cnotzero p1 \<or> cone \<le>o r1 ^c q" and q: "Card_order q"
    1.74 +  assumes 1: "p1 \<le>o r1" and q: "Card_order q"
    1.75    shows "p1 ^c q \<le>o r1 ^c q"
    1.76 -using ordLeq_refl[OF q] by (rule cexp_mono[OF 1 _ n1]) (auto simp: q)
    1.77 -
    1.78 -lemma cexp_mono1_Cnotzero: "\<lbrakk>p1 \<le>o r1; Cnotzero p1; Card_order q\<rbrakk> \<Longrightarrow> p1 ^c q \<le>o r1 ^c q"
    1.79 -by (simp add: cexp_mono1)
    1.80 -
    1.81 -lemma cexp_mono1_cone_ordLeq: "\<lbrakk>p1 \<le>o r1; cone \<le>o r1 ^c q; Card_order q\<rbrakk> \<Longrightarrow> p1 ^c q \<le>o r1 ^c q"
    1.82 -using assms by (simp add: cexp_mono1)
    1.83 +using ordLeq_refl[OF q] by (rule cexp_mono[OF 1]) (auto simp: q)
    1.84  
    1.85  lemma cexp_mono2':
    1.86    assumes 2: "p2 \<le>o r2" and q: "Card_order q"
    1.87 -  and n1: "Field q \<noteq> {} \<or> cone \<le>o q ^c r2"
    1.88 -  and n2: "Field p2 = {} \<Longrightarrow> Field r2 = {}"
    1.89 +  and n: "Field p2 = {} \<Longrightarrow> Field r2 = {}"
    1.90    shows "q ^c p2 \<le>o q ^c r2"
    1.91 -using ordLeq_refl[OF q] by (rule cexp_mono'[OF _ 2 n1 n2]) auto
    1.92 +using ordLeq_refl[OF q] by (rule cexp_mono'[OF _ 2 n]) auto
    1.93  
    1.94  lemma cexp_mono2:
    1.95    assumes 2: "p2 \<le>o r2" and q: "Card_order q"
    1.96 -  and n1: "Cnotzero q \<or> cone \<le>o q ^c r2"
    1.97 -  and n2: "p2 =o czero \<Longrightarrow> r2 =o czero" and card: "Card_order p2"
    1.98 +  and n: "p2 =o czero \<Longrightarrow> r2 =o czero" and card: "Card_order p2"
    1.99    shows "q ^c p2 \<le>o q ^c r2"
   1.100 -using ordLeq_refl[OF q] by (rule cexp_mono[OF _ 2 n1 n2 card]) auto
   1.101 +using ordLeq_refl[OF q] by (rule cexp_mono[OF _ 2 n card]) auto
   1.102  
   1.103  lemma cexp_mono2_Cnotzero:
   1.104 -  assumes "p2 \<le>o r2" "Cnotzero q" and n2: "Cnotzero p2"
   1.105 +  assumes "p2 \<le>o r2" "Card_order q" "Cnotzero p2"
   1.106    shows "q ^c p2 \<le>o q ^c r2"
   1.107 -proof (rule cexp_mono)
   1.108 -  assume *: "p2 =o czero"
   1.109 -  have False using n2 czeroI czeroE[OF *] by blast
   1.110 -  thus "r2 =o czero" by blast
   1.111 -qed (auto simp add: assms ordLeq_refl)
   1.112 +by (metis assms cexp_mono2' czeroI)
   1.113  
   1.114  lemma cexp_cong:
   1.115    assumes 1: "p1 =o r1" and 2: "p2 =o r2"
   1.116 -  and p1: "Cnotzero p1 \<or> cone \<le>o r1 ^c r2" and Cr: "Card_order r2"
   1.117 -  and r1: "Cnotzero r1 \<or> cone \<le>o p1 ^c p2" and Cp: "Card_order p2"
   1.118 +  and Cr: "Card_order r2"
   1.119 +  and Cp: "Card_order p2"
   1.120    shows "p1 ^c p2 =o r1 ^c r2"
   1.121  proof -
   1.122    obtain f where "bij_betw f (Field p2) (Field r2)"
   1.123 @@ -478,32 +467,16 @@
   1.124      and p: "r2 =o czero \<Longrightarrow> p2 =o czero"
   1.125       using 0 Cr Cp czeroE czeroI by auto
   1.126    show ?thesis using 0 1 2 unfolding ordIso_iff_ordLeq
   1.127 -    using r p cexp_mono[OF _ _ p1 _ Cp] cexp_mono[OF _ _ r1 _ Cr]
   1.128 -    by blast
   1.129 +    using r p cexp_mono[OF _ _ _ Cp] cexp_mono[OF _ _ _ Cr] by blast
   1.130  qed
   1.131  
   1.132  lemma cexp_cong1:
   1.133    assumes 1: "p1 =o r1" and q: "Card_order q"
   1.134 -  and p1: "Cnotzero p1 \<or> cone \<le>o r1 ^c q"
   1.135 -  and r1: "Cnotzero r1 \<or> cone \<le>o p1 ^c q"
   1.136    shows "p1 ^c q =o r1 ^c q"
   1.137 -by (rule cexp_cong[OF 1 _ p1 q r1 q]) (rule ordIso_refl[OF q])
   1.138 -
   1.139 -lemma cexp_cong1_Cnotzero:
   1.140 -  assumes "p1 =o r1" "Card_order q" "Cnotzero p1" "Cnotzero r1"
   1.141 -  shows "p1 ^c q =o r1 ^c q"
   1.142 -by (rule cexp_cong1, auto simp add: assms)
   1.143 +by (rule cexp_cong[OF 1 _ q q]) (rule ordIso_refl[OF q])
   1.144  
   1.145  lemma cexp_cong2:
   1.146 -  assumes 2: "p2 =o r2" and q: "Card_order q"
   1.147 -  and p: "Card_order p2" and r: "Card_order r2"
   1.148 -  shows "Cnotzero q \<or> (cone \<le>o q ^c p2 \<and> cone \<le>o q ^c r2) \<Longrightarrow>
   1.149 -    q ^c p2 =o q ^c r2"
   1.150 -by (rule cexp_cong[OF _ 2]) (auto simp only: ordIso_refl q p r)
   1.151 -
   1.152 -lemma cexp_cong2_Cnotzero:
   1.153 -  assumes 2: "p2 =o r2" and q: "Cnotzero q"
   1.154 -  and p: "Card_order p2"
   1.155 +  assumes 2: "p2 =o r2" and q: "Card_order q" and p: "Card_order p2"
   1.156    shows "q ^c p2 =o q ^c r2"
   1.157  by (rule cexp_cong[OF _ 2]) (auto simp only: ordIso_refl Card_order_ordIso2[OF p 2] q p)
   1.158  
   1.159 @@ -523,7 +496,7 @@
   1.160  qed
   1.161  
   1.162  lemma cexp_cprod:
   1.163 -  assumes r1: "Cnotzero r1"
   1.164 +  assumes r1: "Card_order r1"
   1.165    shows "(r1 ^c r2) ^c r3 =o r1 ^c (r2 *c r3)" (is "?L =o ?R")
   1.166  proof -
   1.167    have "?L =o r1 ^c (r3 *c r2)"
   1.168 @@ -535,7 +508,7 @@
   1.169  qed
   1.170  
   1.171  lemma cexp_cprod_ordLeq:
   1.172 -  assumes r1: "Cnotzero r1" and r2: "Cinfinite r2"
   1.173 +  assumes r1: "Card_order r1" and r2: "Cinfinite r2"
   1.174    and r3: "Cnotzero r3" "r3 \<le>o r2"
   1.175    shows "(r1 ^c r2) ^c r3 =o r1 ^c r2" (is "?L =o ?R")
   1.176  proof-
   1.177 @@ -580,14 +553,6 @@
   1.178      apply (rule cone_ordLeq_Cnotzero)
   1.179      apply (rule assms(1))
   1.180      apply (rule assms(2))
   1.181 -    apply (rule disjI1)
   1.182 -    apply (rule conjI)
   1.183 -    apply (rule notI)
   1.184 -    apply (erule notE)
   1.185 -    apply (rule ordIso_transitive)
   1.186 -    apply assumption
   1.187 -    apply (rule czero_ordIso)
   1.188 -    apply (rule assms(2))
   1.189      apply (rule notE)
   1.190      apply (rule cone_not_czero)
   1.191      apply assumption
   1.192 @@ -609,8 +574,6 @@
   1.193      apply (rule assms(2))
   1.194      apply (rule cexp_mono1)
   1.195      apply (rule assms(1))
   1.196 -    apply (rule disjI1)
   1.197 -    apply (rule ctwo_Cnotzero)
   1.198      apply (rule assms(2))
   1.199    done
   1.200  qed
   1.201 @@ -649,9 +612,6 @@
   1.202      apply (rule conjunct2)
   1.203      apply (rule assms(1))
   1.204      apply (rule assms(2))
   1.205 -    apply (simp only: card_of_Card_order czero_def)
   1.206 -    apply (rule disjI1)
   1.207 -    apply (rule assms(1))
   1.208      apply (rule cexp_czero)
   1.209    done
   1.210  qed
   1.211 @@ -752,17 +712,6 @@
   1.212  apply (rule ordLeq_csum1)
   1.213  apply (erule conjunct2)
   1.214  apply assumption
   1.215 -apply (rule disjI2)
   1.216 -apply (rule ordLeq_transitive)
   1.217 -apply (rule cone_ordLeq_ctwo)
   1.218 -apply (rule ordLeq_transitive)
   1.219 -apply assumption
   1.220 -apply (rule ordLeq_cexp1)
   1.221 -apply (rule Cinfinite_Cnotzero)
   1.222 -apply (rule Cinfinite_csum)
   1.223 -apply (rule disjI1)
   1.224 -apply assumption
   1.225 -apply assumption
   1.226  apply (rule notE)
   1.227  apply (rule cinfinite_not_czero[of r1])
   1.228  apply (erule conjunct1)
   1.229 @@ -772,17 +721,6 @@
   1.230  apply (rule ordLeq_csum2)
   1.231  apply (erule conjunct2)
   1.232  apply assumption
   1.233 -apply (rule disjI2)
   1.234 -apply (rule ordLeq_transitive)
   1.235 -apply (rule cone_ordLeq_ctwo)
   1.236 -apply (rule ordLeq_transitive)
   1.237 -apply assumption
   1.238 -apply (rule ordLeq_cexp1)
   1.239 -apply (rule Cinfinite_Cnotzero)
   1.240 -apply (rule Cinfinite_csum)
   1.241 -apply (rule disjI1)
   1.242 -apply assumption
   1.243 -apply assumption
   1.244  apply (rule notE)
   1.245  apply (rule cinfinite_not_czero[of r2])
   1.246  apply (erule conjunct1)