--- a/src/HOL/BNF_Cardinal_Arithmetic.thy Fri Feb 28 22:00:13 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy Fri Feb 28 17:54:52 2014 +0100
@@ -57,15 +57,19 @@
\<lambda>x. if x \<in> A then snd (fg x) else undefined)"
let ?G = "\<lambda>(f, g) x. if x \<in> A then (f x, g x) else undefined"
have "bij_betw ?F ?LHS ?RHS" unfolding bij_betw_def inj_on_def
- apply safe
- apply (simp add: Func_def fun_eq_iff)
- apply (metis (no_types) pair_collapse)
- apply (auto simp: Func_def fun_eq_iff)[2]
- proof -
- fix f g assume "f \<in> Func A B" "g \<in> Func A C"
- thus "(f, g) \<in> ?F ` Func A (B \<times> C)"
- by (intro image_eqI[of _ _ "?G (f, g)"]) (auto simp: Func_def)
- qed
+ proof (intro conjI impI ballI equalityI subsetI)
+ fix f g assume *: "f \<in> Func A (B \<times> C)" "g \<in> Func A (B \<times> C)" "?F f = ?F g"
+ show "f = g"
+ proof
+ fix x from * have "fst (f x) = fst (g x) \<and> snd (f x) = snd (g x)"
+ by (case_tac "x \<in> A") (auto simp: Func_def fun_eq_iff split: if_splits)
+ then show "f x = g x" by (subst (1 2) surjective_pairing) simp
+ qed
+ next
+ fix fg assume "fg \<in> Func A B \<times> Func A C"
+ thus "fg \<in> ?F ` Func A (B \<times> C)"
+ by (intro image_eqI[of _ _ "?G fg"]) (auto simp: Func_def)
+ qed (auto simp: Func_def fun_eq_iff)
thus ?thesis using card_of_ordIso by blast
qed
@@ -89,7 +93,7 @@
(*helper*)
lemma Cnotzero_imp_not_empty: "Cnotzero r \<Longrightarrow> Field r \<noteq> {}"
-by (metis Card_order_iff_ordIso_card_of czero_def)
+ unfolding Card_order_iff_ordIso_card_of czero_def by force
lemma czeroI:
"\<lbrakk>Card_order r; Field r = {}\<rbrakk> \<Longrightarrow> r =o czero"
@@ -127,33 +131,35 @@
lemma Cfinite_ordLess_Cinfinite: "\<lbrakk>Cfinite r; Cinfinite s\<rbrakk> \<Longrightarrow> r <o s"
unfolding cfinite_def cinfinite_def
- by (metis card_order_on_well_order_on finite_ordLess_infinite)
+ by (blast intro: finite_ordLess_infinite card_order_on_well_order_on)
lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq]
lemma natLeq_cinfinite: "cinfinite natLeq"
-unfolding cinfinite_def Field_natLeq by (metis infinite_UNIV_nat)
+unfolding cinfinite_def Field_natLeq by (rule infinite_UNIV_nat)
lemma natLeq_ordLeq_cinfinite:
assumes inf: "Cinfinite r"
shows "natLeq \<le>o r"
proof -
- from inf have "natLeq \<le>o |Field r|" by (metis cinfinite_def infinite_iff_natLeq_ordLeq)
+ from inf have "natLeq \<le>o |Field r|" unfolding cinfinite_def
+ using infinite_iff_natLeq_ordLeq by blast
also from inf have "|Field r| =o r" by (simp add: card_of_unique ordIso_symmetric)
finally show ?thesis .
qed
lemma cinfinite_not_czero: "cinfinite r \<Longrightarrow> \<not> (r =o (czero :: 'a rel))"
-unfolding cinfinite_def by (metis czeroE finite.emptyI)
+unfolding cinfinite_def by (cases "Field r = {}") (auto dest: czeroE)
lemma Cinfinite_Cnotzero: "Cinfinite r \<Longrightarrow> Cnotzero r"
-by (metis cinfinite_not_czero)
+by (rule conjI[OF cinfinite_not_czero]) simp_all
lemma Cinfinite_cong: "\<lbrakk>r1 =o r2; Cinfinite r1\<rbrakk> \<Longrightarrow> Cinfinite r2"
-by (metis Card_order_ordIso2 card_of_mono2 card_of_ordLeq_infinite cinfinite_def ordIso_iff_ordLeq)
+using Card_order_ordIso2[of r1 r2] unfolding cinfinite_def ordIso_iff_ordLeq
+by (auto dest: card_of_ordLeq_infinite[OF card_of_mono2])
lemma cinfinite_mono: "\<lbrakk>r1 \<le>o r2; cinfinite r1\<rbrakk> \<Longrightarrow> cinfinite r2"
-by (metis card_of_mono2 card_of_ordLeq_infinite cinfinite_def)
+unfolding cinfinite_def by (auto dest: card_of_ordLeq_infinite[OF card_of_mono2])
subsection {* Binary sum *}
@@ -170,8 +176,8 @@
lemma csum_Cnotzero1:
"Cnotzero r1 \<Longrightarrow> Cnotzero (r1 +c r2)"
-unfolding csum_def
-by (metis Cnotzero_imp_not_empty Plus_eq_empty_conv card_of_Card_order card_of_ordIso_czero_iff_empty)
+unfolding csum_def using Cnotzero_imp_not_empty[of r1] Plus_eq_empty_conv[of "Field r1" "Field r2"]
+ card_of_ordIso_czero_iff_empty[of "Field r1 <+> Field r2"] by (auto intro: card_of_Card_order)
lemma card_order_csum:
assumes "card_order r1" "card_order r2"
@@ -187,15 +193,15 @@
lemma Cinfinite_csum1:
"Cinfinite r1 \<Longrightarrow> Cinfinite (r1 +c r2)"
-unfolding cinfinite_def csum_def by (metis Field_card_of card_of_Card_order finite_Plus_iff)
+unfolding cinfinite_def csum_def by (rule conjI[OF _ card_of_Card_order]) (auto simp: Field_card_of)
lemma Cinfinite_csum:
"Cinfinite r1 \<or> Cinfinite r2 \<Longrightarrow> Cinfinite (r1 +c r2)"
-unfolding cinfinite_def csum_def by (metis Field_card_of card_of_Card_order finite_Plus_iff)
+unfolding cinfinite_def csum_def by (rule conjI[OF _ card_of_Card_order]) (auto simp: Field_card_of)
lemma Cinfinite_csum_strong:
"\<lbrakk>Cinfinite r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 +c r2)"
-by (metis Cinfinite_csum)
+by (erule Cinfinite_csum1)
lemma csum_cong: "\<lbrakk>p1 =o r1; p2 =o r2\<rbrakk> \<Longrightarrow> p1 +c p2 =o r1 +c r2"
by (simp only: csum_def ordIso_Plus_cong)
@@ -233,15 +239,15 @@
lemma csum_csum: "(r1 +c r2) +c (r3 +c r4) =o (r1 +c r3) +c (r2 +c r4)"
proof -
have "(r1 +c r2) +c (r3 +c r4) =o r1 +c r2 +c (r3 +c r4)"
- by (metis csum_assoc)
+ by (rule csum_assoc)
also have "r1 +c r2 +c (r3 +c r4) =o r1 +c (r2 +c r3) +c r4"
- by (metis csum_assoc csum_cong2 ordIso_symmetric)
+ by (intro csum_assoc csum_cong2 ordIso_symmetric)
also have "r1 +c (r2 +c r3) +c r4 =o r1 +c (r3 +c r2) +c r4"
- by (metis csum_com csum_cong1 csum_cong2)
+ by (intro csum_com csum_cong1 csum_cong2)
also have "r1 +c (r3 +c r2) +c r4 =o r1 +c r3 +c r2 +c r4"
- by (metis csum_assoc csum_cong2 ordIso_symmetric)
+ by (intro csum_assoc csum_cong2 ordIso_symmetric)
also have "r1 +c r3 +c r2 +c r4 =o (r1 +c r3) +c (r2 +c r4)"
- by (metis csum_assoc ordIso_symmetric)
+ by (intro csum_assoc ordIso_symmetric)
finally show ?thesis .
qed
@@ -264,10 +270,10 @@
unfolding cfinite_def by (simp add: Card_order_cone)
lemma cone_not_czero: "\<not> (cone =o czero)"
-unfolding czero_def cone_def by (metis empty_not_insert card_of_empty3[of "{()}"] ordIso_iff_ordLeq)
+unfolding czero_def cone_def ordIso_iff_ordLeq using card_of_empty3 empty_not_insert by blast
lemma cone_ordLeq_Cnotzero: "Cnotzero r \<Longrightarrow> cone \<le>o r"
-unfolding cone_def by (metis Card_order_singl_ordLeq czeroI)
+unfolding cone_def by (rule Card_order_singl_ordLeq) (auto intro: czeroI)
subsection {* Two *}
@@ -280,7 +286,7 @@
lemma ctwo_not_czero: "\<not> (ctwo =o czero)"
using card_of_empty3[of "UNIV :: bool set"] ordIso_iff_ordLeq
-unfolding czero_def ctwo_def by (metis UNIV_not_empty)
+unfolding czero_def ctwo_def using UNIV_not_empty by auto
lemma ctwo_Cnotzero: "Cnotzero ctwo"
by (simp add: ctwo_not_czero Card_order_ctwo)
@@ -330,13 +336,13 @@
by (simp only: cprod_def ordLeq_Times_mono2)
lemma ordLeq_cprod2: "\<lbrakk>Cnotzero p1; Card_order p2\<rbrakk> \<Longrightarrow> p2 \<le>o p1 *c p2"
-unfolding cprod_def by (metis Card_order_Times2 czeroI)
+unfolding cprod_def by (rule Card_order_Times2) (auto intro: czeroI)
lemma cinfinite_cprod: "\<lbrakk>cinfinite r1; cinfinite r2\<rbrakk> \<Longrightarrow> cinfinite (r1 *c r2)"
by (simp add: cinfinite_def cprod_def Field_card_of infinite_cartesian_product)
lemma cinfinite_cprod2: "\<lbrakk>Cnotzero r1; Cinfinite r2\<rbrakk> \<Longrightarrow> cinfinite (r1 *c r2)"
-by (metis cinfinite_mono ordLeq_cprod2)
+by (rule cinfinite_mono) (auto intro: ordLeq_cprod2)
lemma Cinfinite_cprod2: "\<lbrakk>Cnotzero r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 *c r2)"
by (blast intro: cinfinite_cprod2 Card_order_cprod)
@@ -364,7 +370,8 @@
unfolding csum_def cprod_def by (simp add: Field_card_of card_of_Times_Plus_distrib ordIso_symmetric)
lemma csum_absorb2': "\<lbrakk>Card_order r2; r1 \<le>o r2; cinfinite r1 \<or> cinfinite r2\<rbrakk> \<Longrightarrow> r1 +c r2 =o r2"
-unfolding csum_def by (metis Card_order_Plus_infinite cinfinite_def cinfinite_mono)
+unfolding csum_def by (rule conjunct2[OF Card_order_Plus_infinite])
+ (auto simp: cinfinite_def dest: cinfinite_mono)
lemma csum_absorb1':
assumes card: "Card_order r2"
@@ -390,10 +397,10 @@
shows "p1 ^c p2 \<le>o r1 ^c r2"
proof(cases "Field p1 = {}")
case True
- hence "|Field |Func (Field p2) (Field p1)|| \<le>o cone"
+ hence "Field p2 \<noteq> {} \<Longrightarrow> Func (Field p2) {} = {}" unfolding Func_is_emp by simp
+ with True have "|Field |Func (Field p2) (Field p1)|| \<le>o cone"
unfolding cone_def Field_card_of
- by (cases "Field p2 = {}", auto intro: card_of_ordLeqI2 simp: Func_empty)
- (metis Func_is_emp card_of_empty ex_in_conv)
+ by (cases "Field p2 = {}", auto intro: surj_imp_ordLeq simp: Func_empty)
hence "|Func (Field p2) (Field p1)| \<le>o cone" by (simp add: Field_card_of cexp_def)
hence "p1 ^c p2 \<le>o cone" unfolding cexp_def .
thus ?thesis
@@ -429,7 +436,7 @@
assumes 1: "p1 \<le>o r1" and 2: "p2 \<le>o r2"
and n: "p2 =o czero \<Longrightarrow> r2 =o czero" and card: "Card_order p2"
shows "p1 ^c p2 \<le>o r1 ^c r2"
- by (metis (full_types) "1" "2" card cexp_mono' czeroE czeroI n)
+ by (rule cexp_mono'[OF 1 2 czeroE[OF n[OF czeroI[OF card]]]])
lemma cexp_mono1:
assumes 1: "p1 \<le>o r1" and q: "Card_order q"
@@ -451,7 +458,7 @@
lemma cexp_mono2_Cnotzero:
assumes "p2 \<le>o r2" "Card_order q" "Cnotzero p2"
shows "q ^c p2 \<le>o q ^c r2"
-by (metis assms cexp_mono2' czeroI)
+using assms(3) czeroI by (blast intro: cexp_mono2'[OF assms(1,2)])
lemma cexp_cong:
assumes 1: "p1 =o r1" and 2: "p2 =o r2"
@@ -466,7 +473,7 @@
and p: "r2 =o czero \<Longrightarrow> p2 =o czero"
using 0 Cr Cp czeroE czeroI by auto
show ?thesis using 0 1 2 unfolding ordIso_iff_ordLeq
- using r p cexp_mono[OF _ _ _ Cp] cexp_mono[OF _ _ _ Cr] by metis
+ using r p cexp_mono[OF _ _ _ Cp] cexp_mono[OF _ _ _ Cr] by blast
qed
lemma cexp_cong1:
@@ -575,7 +582,7 @@
qed
lemma cinfinite_cexp: "\<lbrakk>ctwo \<le>o q; Cinfinite r\<rbrakk> \<Longrightarrow> cinfinite (q ^c r)"
-by (metis assms cinfinite_mono ordLeq_cexp2)
+by (rule cinfinite_mono[OF ordLeq_cexp2]) simp_all
lemma Cinfinite_cexp:
"\<lbrakk>ctwo \<le>o q; Cinfinite r\<rbrakk> \<Longrightarrow> Cinfinite (q ^c r)"
@@ -586,7 +593,7 @@
by (intro Cfinite_ordLess_Cinfinite) (auto simp: cfinite_def card_of_Card_order)
lemma ctwo_ordLess_Cinfinite: "Cinfinite r \<Longrightarrow> ctwo <o r"
-by (metis ctwo_ordLess_natLeq natLeq_ordLeq_cinfinite ordLess_ordLeq_trans)
+by (rule ordLess_ordLeq_trans[OF ctwo_ordLess_natLeq natLeq_ordLeq_cinfinite])
lemma ctwo_ordLeq_Cinfinite:
assumes "Cinfinite r"
@@ -663,9 +670,10 @@
case True thus ?thesis using t by (blast intro: cexp_mono1)
next
case False
- hence "ctwo \<le>o s" by (metis card_order_on_well_order_on ctwo_Cnotzero ordLeq_total s)
- hence "Cnotzero s" by (metis Cnotzero_mono ctwo_Cnotzero s)
- hence st: "Cnotzero (s *c t)" by (metis Cinfinite_cprod2 cinfinite_not_czero t)
+ hence "ctwo \<le>o s" using ordLeq_total[of s ctwo] Card_order_ctwo s
+ by (auto intro: card_order_on_well_order_on)
+ hence "Cnotzero s" using Cnotzero_mono[OF ctwo_Cnotzero] s by blast
+ hence st: "Cnotzero (s *c t)" by (intro Cinfinite_Cnotzero[OF Cinfinite_cprod2]) (auto simp: t)
have "s ^c t \<le>o (ctwo ^c s) ^c t"
using assms by (blast intro: cexp_mono1 ordLess_imp_ordLeq[OF ordLess_ctwo_cexp])
also have "(ctwo ^c s) ^c t =o ctwo ^c (s *c t)"