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)"
```