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