src/HOL/BNF_Cardinal_Arithmetic.thy
changeset 56191 159b0c88b4a4
parent 55866 a6fa341a6d66
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Tue Mar 18 10:12:58 2014 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Tue Mar 18 11:47:59 2014 +0100
     1.3 @@ -14,10 +14,6 @@
     1.4  lemma dir_image: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); Card_order r\<rbrakk> \<Longrightarrow> r =o dir_image r f"
     1.5  by (rule dir_image_ordIso) (auto simp add: inj_on_def card_order_on_def)
     1.6  
     1.7 -(*should supersede a weaker lemma from the library*)
     1.8 -lemma dir_image_Field: "Field (dir_image r f) = f ` Field r"
     1.9 -unfolding dir_image_def Field_def Range_def Domain_def by fast
    1.10 -
    1.11  lemma card_order_dir_image:
    1.12    assumes bij: "bij f" and co: "card_order r"
    1.13    shows "card_order (dir_image r f)"
    1.14 @@ -42,37 +38,6 @@
    1.15  lemma Field_card_order: "card_order r \<Longrightarrow> Field r = UNIV"
    1.16  using card_order_on_Card_order[of UNIV r] by simp
    1.17  
    1.18 -lemma card_of_Times_Plus_distrib:
    1.19 -  "|A <*> (B <+> C)| =o |A <*> B <+> A <*> C|" (is "|?RHS| =o |?LHS|")
    1.20 -proof -
    1.21 -  let ?f = "\<lambda>(a, bc). case bc of Inl b \<Rightarrow> Inl (a, b) | Inr c \<Rightarrow> Inr (a, c)"
    1.22 -  have "bij_betw ?f ?RHS ?LHS" unfolding bij_betw_def inj_on_def by force
    1.23 -  thus ?thesis using card_of_ordIso by blast
    1.24 -qed
    1.25 -
    1.26 -lemma Func_Times_Range:
    1.27 -  "|Func A (B <*> C)| =o |Func A B <*> Func A C|" (is "|?LHS| =o |?RHS|")
    1.28 -proof -
    1.29 -  let ?F = "\<lambda>fg. (\<lambda>x. if x \<in> A then fst (fg x) else undefined,
    1.30 -                  \<lambda>x. if x \<in> A then snd (fg x) else undefined)"
    1.31 -  let ?G = "\<lambda>(f, g) x. if x \<in> A then (f x, g x) else undefined"
    1.32 -  have "bij_betw ?F ?LHS ?RHS" unfolding bij_betw_def inj_on_def
    1.33 -  proof (intro conjI impI ballI equalityI subsetI)
    1.34 -    fix f g assume *: "f \<in> Func A (B \<times> C)" "g \<in> Func A (B \<times> C)" "?F f = ?F g"
    1.35 -    show "f = g"
    1.36 -    proof
    1.37 -      fix x from * have "fst (f x) = fst (g x) \<and> snd (f x) = snd (g x)"
    1.38 -        by (case_tac "x \<in> A") (auto simp: Func_def fun_eq_iff split: if_splits)
    1.39 -      then show "f x = g x" by (subst (1 2) surjective_pairing) simp
    1.40 -    qed
    1.41 -  next
    1.42 -    fix fg assume "fg \<in> Func A B \<times> Func A C"
    1.43 -    thus "fg \<in> ?F ` Func A (B \<times> C)"
    1.44 -      by (intro image_eqI[of _ _ "?G fg"]) (auto simp: Func_def)
    1.45 -  qed (auto simp: Func_def fun_eq_iff)
    1.46 -  thus ?thesis using card_of_ordIso by blast
    1.47 -qed
    1.48 -
    1.49  
    1.50  subsection {* Zero *}
    1.51  
    1.52 @@ -364,7 +329,7 @@
    1.53  
    1.54  lemma card_of_Csum_Times:
    1.55    "\<forall>i \<in> I. |A i| \<le>o |B| \<Longrightarrow> (CSUM i : |I|. |A i| ) \<le>o |I| *c |B|"
    1.56 -by (simp only: Csum_def cprod_def Field_card_of card_of_Sigma_Times)
    1.57 +by (simp only: Csum_def cprod_def Field_card_of card_of_Sigma_mono1)
    1.58  
    1.59  lemma card_of_Csum_Times':
    1.60    assumes "Card_order r" "\<forall>i \<in> I. |A i| \<le>o r"