src/HOL/BNF_Cardinal_Arithmetic.thy
changeset 55811 aa1acc25126b
parent 55604 42e4e8c2e8dc
child 55851 3d40cf74726c
     1.1 --- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Fri Feb 28 22:00:13 2014 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Fri Feb 28 17:54:52 2014 +0100
     1.3 @@ -57,15 +57,19 @@
     1.4                    \<lambda>x. if x \<in> A then snd (fg x) else undefined)"
     1.5    let ?G = "\<lambda>(f, g) x. if x \<in> A then (f x, g x) else undefined"
     1.6    have "bij_betw ?F ?LHS ?RHS" unfolding bij_betw_def inj_on_def
     1.7 -  apply safe
     1.8 -     apply (simp add: Func_def fun_eq_iff)
     1.9 -     apply (metis (no_types) pair_collapse)
    1.10 -    apply (auto simp: Func_def fun_eq_iff)[2]
    1.11 -  proof -
    1.12 -    fix f g assume "f \<in> Func A B" "g \<in> Func A C"
    1.13 -    thus "(f, g) \<in> ?F ` Func A (B \<times> C)"
    1.14 -      by (intro image_eqI[of _ _ "?G (f, g)"]) (auto simp: Func_def)
    1.15 -  qed
    1.16 +  proof (intro conjI impI ballI equalityI subsetI)
    1.17 +    fix f g assume *: "f \<in> Func A (B \<times> C)" "g \<in> Func A (B \<times> C)" "?F f = ?F g"
    1.18 +    show "f = g"
    1.19 +    proof
    1.20 +      fix x from * have "fst (f x) = fst (g x) \<and> snd (f x) = snd (g x)"
    1.21 +        by (case_tac "x \<in> A") (auto simp: Func_def fun_eq_iff split: if_splits)
    1.22 +      then show "f x = g x" by (subst (1 2) surjective_pairing) simp
    1.23 +    qed
    1.24 +  next
    1.25 +    fix fg assume "fg \<in> Func A B \<times> Func A C"
    1.26 +    thus "fg \<in> ?F ` Func A (B \<times> C)"
    1.27 +      by (intro image_eqI[of _ _ "?G fg"]) (auto simp: Func_def)
    1.28 +  qed (auto simp: Func_def fun_eq_iff)
    1.29    thus ?thesis using card_of_ordIso by blast
    1.30  qed
    1.31  
    1.32 @@ -89,7 +93,7 @@
    1.33  
    1.34  (*helper*)
    1.35  lemma Cnotzero_imp_not_empty: "Cnotzero r \<Longrightarrow> Field r \<noteq> {}"
    1.36 -by (metis Card_order_iff_ordIso_card_of czero_def)
    1.37 +  unfolding Card_order_iff_ordIso_card_of czero_def by force
    1.38  
    1.39  lemma czeroI:
    1.40    "\<lbrakk>Card_order r; Field r = {}\<rbrakk> \<Longrightarrow> r =o czero"
    1.41 @@ -127,33 +131,35 @@
    1.42  
    1.43  lemma Cfinite_ordLess_Cinfinite: "\<lbrakk>Cfinite r; Cinfinite s\<rbrakk> \<Longrightarrow> r <o s"
    1.44    unfolding cfinite_def cinfinite_def
    1.45 -  by (metis card_order_on_well_order_on finite_ordLess_infinite)
    1.46 +  by (blast intro: finite_ordLess_infinite card_order_on_well_order_on)
    1.47  
    1.48  lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq]
    1.49  
    1.50  lemma natLeq_cinfinite: "cinfinite natLeq"
    1.51 -unfolding cinfinite_def Field_natLeq by (metis infinite_UNIV_nat)
    1.52 +unfolding cinfinite_def Field_natLeq by (rule infinite_UNIV_nat)
    1.53  
    1.54  lemma natLeq_ordLeq_cinfinite:
    1.55    assumes inf: "Cinfinite r"
    1.56    shows "natLeq \<le>o r"
    1.57  proof -
    1.58 -  from inf have "natLeq \<le>o |Field r|" by (metis cinfinite_def infinite_iff_natLeq_ordLeq)
    1.59 +  from inf have "natLeq \<le>o |Field r|" unfolding cinfinite_def
    1.60 +    using infinite_iff_natLeq_ordLeq by blast
    1.61    also from inf have "|Field r| =o r" by (simp add: card_of_unique ordIso_symmetric)
    1.62    finally show ?thesis .
    1.63  qed
    1.64  
    1.65  lemma cinfinite_not_czero: "cinfinite r \<Longrightarrow> \<not> (r =o (czero :: 'a rel))"
    1.66 -unfolding cinfinite_def by (metis czeroE finite.emptyI)
    1.67 +unfolding cinfinite_def by (cases "Field r = {}") (auto dest: czeroE)
    1.68  
    1.69  lemma Cinfinite_Cnotzero: "Cinfinite r \<Longrightarrow> Cnotzero r"
    1.70 -by (metis cinfinite_not_czero)
    1.71 +by (rule conjI[OF cinfinite_not_czero]) simp_all
    1.72  
    1.73  lemma Cinfinite_cong: "\<lbrakk>r1 =o r2; Cinfinite r1\<rbrakk> \<Longrightarrow> Cinfinite r2"
    1.74 -by (metis Card_order_ordIso2 card_of_mono2 card_of_ordLeq_infinite cinfinite_def ordIso_iff_ordLeq)
    1.75 +using Card_order_ordIso2[of r1 r2] unfolding cinfinite_def ordIso_iff_ordLeq
    1.76 +by (auto dest: card_of_ordLeq_infinite[OF card_of_mono2])
    1.77  
    1.78  lemma cinfinite_mono: "\<lbrakk>r1 \<le>o r2; cinfinite r1\<rbrakk> \<Longrightarrow> cinfinite r2"
    1.79 -by (metis card_of_mono2 card_of_ordLeq_infinite cinfinite_def)
    1.80 +unfolding cinfinite_def by (auto dest: card_of_ordLeq_infinite[OF card_of_mono2])
    1.81  
    1.82  
    1.83  subsection {* Binary sum *}
    1.84 @@ -170,8 +176,8 @@
    1.85  
    1.86  lemma csum_Cnotzero1:
    1.87    "Cnotzero r1 \<Longrightarrow> Cnotzero (r1 +c r2)"
    1.88 -unfolding csum_def
    1.89 -by (metis Cnotzero_imp_not_empty Plus_eq_empty_conv card_of_Card_order card_of_ordIso_czero_iff_empty)
    1.90 +unfolding csum_def using Cnotzero_imp_not_empty[of r1] Plus_eq_empty_conv[of "Field r1" "Field r2"]
    1.91 +   card_of_ordIso_czero_iff_empty[of "Field r1 <+> Field r2"] by (auto intro: card_of_Card_order)
    1.92  
    1.93  lemma card_order_csum:
    1.94    assumes "card_order r1" "card_order r2"
    1.95 @@ -187,15 +193,15 @@
    1.96  
    1.97  lemma Cinfinite_csum1:
    1.98    "Cinfinite r1 \<Longrightarrow> Cinfinite (r1 +c r2)"
    1.99 -unfolding cinfinite_def csum_def by (metis Field_card_of card_of_Card_order finite_Plus_iff)
   1.100 +unfolding cinfinite_def csum_def by (rule conjI[OF _ card_of_Card_order]) (auto simp: Field_card_of)
   1.101  
   1.102  lemma Cinfinite_csum:
   1.103    "Cinfinite r1 \<or> Cinfinite r2 \<Longrightarrow> Cinfinite (r1 +c r2)"
   1.104 -unfolding cinfinite_def csum_def by (metis Field_card_of card_of_Card_order finite_Plus_iff)
   1.105 +unfolding cinfinite_def csum_def by (rule conjI[OF _ card_of_Card_order]) (auto simp: Field_card_of)
   1.106  
   1.107  lemma Cinfinite_csum_strong:
   1.108    "\<lbrakk>Cinfinite r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 +c r2)"
   1.109 -by (metis Cinfinite_csum)
   1.110 +by (erule Cinfinite_csum1)
   1.111  
   1.112  lemma csum_cong: "\<lbrakk>p1 =o r1; p2 =o r2\<rbrakk> \<Longrightarrow> p1 +c p2 =o r1 +c r2"
   1.113  by (simp only: csum_def ordIso_Plus_cong)
   1.114 @@ -233,15 +239,15 @@
   1.115  lemma csum_csum: "(r1 +c r2) +c (r3 +c r4) =o (r1 +c r3) +c (r2 +c r4)"
   1.116  proof -
   1.117    have "(r1 +c r2) +c (r3 +c r4) =o r1 +c r2 +c (r3 +c r4)"
   1.118 -    by (metis csum_assoc)
   1.119 +    by (rule csum_assoc)
   1.120    also have "r1 +c r2 +c (r3 +c r4) =o r1 +c (r2 +c r3) +c r4"
   1.121 -    by (metis csum_assoc csum_cong2 ordIso_symmetric)
   1.122 +    by (intro csum_assoc csum_cong2 ordIso_symmetric)
   1.123    also have "r1 +c (r2 +c r3) +c r4 =o r1 +c (r3 +c r2) +c r4"
   1.124 -    by (metis csum_com csum_cong1 csum_cong2)
   1.125 +    by (intro csum_com csum_cong1 csum_cong2)
   1.126    also have "r1 +c (r3 +c r2) +c r4 =o r1 +c r3 +c r2 +c r4"
   1.127 -    by (metis csum_assoc csum_cong2 ordIso_symmetric)
   1.128 +    by (intro csum_assoc csum_cong2 ordIso_symmetric)
   1.129    also have "r1 +c r3 +c r2 +c r4 =o (r1 +c r3) +c (r2 +c r4)"
   1.130 -    by (metis csum_assoc ordIso_symmetric)
   1.131 +    by (intro csum_assoc ordIso_symmetric)
   1.132    finally show ?thesis .
   1.133  qed
   1.134  
   1.135 @@ -264,10 +270,10 @@
   1.136    unfolding cfinite_def by (simp add: Card_order_cone)
   1.137  
   1.138  lemma cone_not_czero: "\<not> (cone =o czero)"
   1.139 -unfolding czero_def cone_def by (metis empty_not_insert card_of_empty3[of "{()}"] ordIso_iff_ordLeq)
   1.140 +unfolding czero_def cone_def ordIso_iff_ordLeq using card_of_empty3 empty_not_insert by blast
   1.141  
   1.142  lemma cone_ordLeq_Cnotzero: "Cnotzero r \<Longrightarrow> cone \<le>o r"
   1.143 -unfolding cone_def by (metis Card_order_singl_ordLeq czeroI)
   1.144 +unfolding cone_def by (rule Card_order_singl_ordLeq) (auto intro: czeroI)
   1.145  
   1.146  
   1.147  subsection {* Two *}
   1.148 @@ -280,7 +286,7 @@
   1.149  
   1.150  lemma ctwo_not_czero: "\<not> (ctwo =o czero)"
   1.151  using card_of_empty3[of "UNIV :: bool set"] ordIso_iff_ordLeq
   1.152 -unfolding czero_def ctwo_def by (metis UNIV_not_empty)
   1.153 +unfolding czero_def ctwo_def using UNIV_not_empty by auto
   1.154  
   1.155  lemma ctwo_Cnotzero: "Cnotzero ctwo"
   1.156  by (simp add: ctwo_not_czero Card_order_ctwo)
   1.157 @@ -330,13 +336,13 @@
   1.158  by (simp only: cprod_def ordLeq_Times_mono2)
   1.159  
   1.160  lemma ordLeq_cprod2: "\<lbrakk>Cnotzero p1; Card_order p2\<rbrakk> \<Longrightarrow> p2 \<le>o p1 *c p2"
   1.161 -unfolding cprod_def by (metis Card_order_Times2 czeroI)
   1.162 +unfolding cprod_def by (rule Card_order_Times2) (auto intro: czeroI)
   1.163  
   1.164  lemma cinfinite_cprod: "\<lbrakk>cinfinite r1; cinfinite r2\<rbrakk> \<Longrightarrow> cinfinite (r1 *c r2)"
   1.165  by (simp add: cinfinite_def cprod_def Field_card_of infinite_cartesian_product)
   1.166  
   1.167  lemma cinfinite_cprod2: "\<lbrakk>Cnotzero r1; Cinfinite r2\<rbrakk> \<Longrightarrow> cinfinite (r1 *c r2)"
   1.168 -by (metis cinfinite_mono ordLeq_cprod2)
   1.169 +by (rule cinfinite_mono) (auto intro: ordLeq_cprod2)
   1.170  
   1.171  lemma Cinfinite_cprod2: "\<lbrakk>Cnotzero r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 *c r2)"
   1.172  by (blast intro: cinfinite_cprod2 Card_order_cprod)
   1.173 @@ -364,7 +370,8 @@
   1.174  unfolding csum_def cprod_def by (simp add: Field_card_of card_of_Times_Plus_distrib ordIso_symmetric)
   1.175  
   1.176  lemma csum_absorb2': "\<lbrakk>Card_order r2; r1 \<le>o r2; cinfinite r1 \<or> cinfinite r2\<rbrakk> \<Longrightarrow> r1 +c r2 =o r2"
   1.177 -unfolding csum_def by (metis Card_order_Plus_infinite cinfinite_def cinfinite_mono)
   1.178 +unfolding csum_def by (rule conjunct2[OF Card_order_Plus_infinite])
   1.179 +  (auto simp: cinfinite_def dest: cinfinite_mono)
   1.180  
   1.181  lemma csum_absorb1':
   1.182    assumes card: "Card_order r2"
   1.183 @@ -390,10 +397,10 @@
   1.184    shows "p1 ^c p2 \<le>o r1 ^c r2"
   1.185  proof(cases "Field p1 = {}")
   1.186    case True
   1.187 -  hence "|Field |Func (Field p2) (Field p1)|| \<le>o cone"
   1.188 +  hence "Field p2 \<noteq> {} \<Longrightarrow> Func (Field p2) {} = {}" unfolding Func_is_emp by simp
   1.189 +  with True have "|Field |Func (Field p2) (Field p1)|| \<le>o cone"
   1.190      unfolding cone_def Field_card_of
   1.191 -    by (cases "Field p2 = {}", auto intro: card_of_ordLeqI2 simp: Func_empty)
   1.192 -       (metis Func_is_emp card_of_empty ex_in_conv)
   1.193 +    by (cases "Field p2 = {}", auto intro: surj_imp_ordLeq simp: Func_empty)
   1.194    hence "|Func (Field p2) (Field p1)| \<le>o cone" by (simp add: Field_card_of cexp_def)
   1.195    hence "p1 ^c p2 \<le>o cone" unfolding cexp_def .
   1.196    thus ?thesis
   1.197 @@ -429,7 +436,7 @@
   1.198    assumes 1: "p1 \<le>o r1" and 2: "p2 \<le>o r2"
   1.199    and n: "p2 =o czero \<Longrightarrow> r2 =o czero" and card: "Card_order p2"
   1.200    shows "p1 ^c p2 \<le>o r1 ^c r2"
   1.201 -  by (metis (full_types) "1" "2" card cexp_mono' czeroE czeroI n)
   1.202 +  by (rule cexp_mono'[OF 1 2 czeroE[OF n[OF czeroI[OF card]]]])
   1.203  
   1.204  lemma cexp_mono1:
   1.205    assumes 1: "p1 \<le>o r1" and q: "Card_order q"
   1.206 @@ -451,7 +458,7 @@
   1.207  lemma cexp_mono2_Cnotzero:
   1.208    assumes "p2 \<le>o r2" "Card_order q" "Cnotzero p2"
   1.209    shows "q ^c p2 \<le>o q ^c r2"
   1.210 -by (metis assms cexp_mono2' czeroI)
   1.211 +using assms(3) czeroI by (blast intro: cexp_mono2'[OF assms(1,2)])
   1.212  
   1.213  lemma cexp_cong:
   1.214    assumes 1: "p1 =o r1" and 2: "p2 =o r2"
   1.215 @@ -466,7 +473,7 @@
   1.216      and p: "r2 =o czero \<Longrightarrow> p2 =o czero"
   1.217       using 0 Cr Cp czeroE czeroI by auto
   1.218    show ?thesis using 0 1 2 unfolding ordIso_iff_ordLeq
   1.219 -    using r p cexp_mono[OF _ _ _ Cp] cexp_mono[OF _ _ _ Cr] by metis
   1.220 +    using r p cexp_mono[OF _ _ _ Cp] cexp_mono[OF _ _ _ Cr] by blast
   1.221  qed
   1.222  
   1.223  lemma cexp_cong1:
   1.224 @@ -575,7 +582,7 @@
   1.225  qed
   1.226  
   1.227  lemma cinfinite_cexp: "\<lbrakk>ctwo \<le>o q; Cinfinite r\<rbrakk> \<Longrightarrow> cinfinite (q ^c r)"
   1.228 -by (metis assms cinfinite_mono ordLeq_cexp2)
   1.229 +by (rule cinfinite_mono[OF ordLeq_cexp2]) simp_all
   1.230  
   1.231  lemma Cinfinite_cexp:
   1.232    "\<lbrakk>ctwo \<le>o q; Cinfinite r\<rbrakk> \<Longrightarrow> Cinfinite (q ^c r)"
   1.233 @@ -586,7 +593,7 @@
   1.234  by (intro Cfinite_ordLess_Cinfinite) (auto simp: cfinite_def card_of_Card_order)
   1.235  
   1.236  lemma ctwo_ordLess_Cinfinite: "Cinfinite r \<Longrightarrow> ctwo <o r"
   1.237 -by (metis ctwo_ordLess_natLeq natLeq_ordLeq_cinfinite ordLess_ordLeq_trans)
   1.238 +by (rule ordLess_ordLeq_trans[OF ctwo_ordLess_natLeq natLeq_ordLeq_cinfinite])
   1.239  
   1.240  lemma ctwo_ordLeq_Cinfinite:
   1.241    assumes "Cinfinite r"
   1.242 @@ -663,9 +670,10 @@
   1.243    case True thus ?thesis using t by (blast intro: cexp_mono1)
   1.244  next
   1.245    case False
   1.246 -  hence "ctwo \<le>o s" by (metis card_order_on_well_order_on ctwo_Cnotzero ordLeq_total s)
   1.247 -  hence "Cnotzero s" by (metis Cnotzero_mono ctwo_Cnotzero s)
   1.248 -  hence st: "Cnotzero (s *c t)" by (metis Cinfinite_cprod2 cinfinite_not_czero t)
   1.249 +  hence "ctwo \<le>o s" using ordLeq_total[of s ctwo] Card_order_ctwo s
   1.250 +    by (auto intro: card_order_on_well_order_on)
   1.251 +  hence "Cnotzero s" using Cnotzero_mono[OF ctwo_Cnotzero] s by blast
   1.252 +  hence st: "Cnotzero (s *c t)" by (intro Cinfinite_Cnotzero[OF Cinfinite_cprod2]) (auto simp: t)
   1.253    have "s ^c t \<le>o (ctwo ^c s) ^c t"
   1.254      using assms by (blast intro: cexp_mono1 ordLess_imp_ordLeq[OF ordLess_ctwo_cexp])
   1.255    also have "(ctwo ^c s) ^c t =o ctwo ^c (s *c t)"