src/HOL/BNF_Cardinal_Order_Relation.thy
changeset 56191 159b0c88b4a4
parent 56077 d397030fb27e
child 58127 b7cab82f488e
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Tue Mar 18 10:12:58 2014 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Tue Mar 18 11:47:59 2014 +0100
     1.3 @@ -98,7 +98,7 @@
     1.4    have 4: "p' =o ?p \<and> Well_order ?p"
     1.5    using 0 2 3 by (auto simp add: dir_image_ordIso Well_order_dir_image)
     1.6    moreover have "Field ?p =  Field r"
     1.7 -  using 0 3 by (auto simp add: dir_image_Field2 order_on_defs)
     1.8 +  using 0 3 by (auto simp add: dir_image_Field)
     1.9    ultimately have "well_order_on (Field r) ?p" by auto
    1.10    hence "r \<le>o ?p" using CO unfolding card_order_on_def by auto
    1.11    thus "r' \<le>o p'"
    1.12 @@ -709,10 +709,6 @@
    1.13    thus ?thesis using card_of_ordLeq by blast
    1.14  qed
    1.15  
    1.16 -corollary card_of_Sigma_Times:
    1.17 -"\<forall>i \<in> I. |A i| \<le>o |B| \<Longrightarrow> |SIGMA i : I. A i| \<le>o |I \<times> B|"
    1.18 -by (fact card_of_Sigma_mono1)
    1.19 -
    1.20  lemma card_of_UNION_Sigma:
    1.21  "|\<Union>i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
    1.22  using Ex_inj_on_UNION_Sigma[of I A] card_of_ordLeq by blast
    1.23 @@ -791,6 +787,14 @@
    1.24          ordLeq_total[of "|A|"] by blast
    1.25  qed
    1.26  
    1.27 +lemma card_of_Times_Plus_distrib:
    1.28 +  "|A <*> (B <+> C)| =o |A <*> B <+> A <*> C|" (is "|?RHS| =o |?LHS|")
    1.29 +proof -
    1.30 +  let ?f = "\<lambda>(a, bc). case bc of Inl b \<Rightarrow> Inl (a, b) | Inr c \<Rightarrow> Inr (a, c)"
    1.31 +  have "bij_betw ?f ?RHS ?LHS" unfolding bij_betw_def inj_on_def by force
    1.32 +  thus ?thesis using card_of_ordIso by blast
    1.33 +qed
    1.34 +
    1.35  lemma card_of_ordLeq_finite:
    1.36  assumes "|A| \<le>o |B|" and "finite B"
    1.37  shows "finite A"
    1.38 @@ -1011,7 +1015,7 @@
    1.39  proof(cases "I = {}", simp add: card_of_empty)
    1.40    assume *: "I \<noteq> {}"
    1.41    have "|SIGMA i : I. A i| \<le>o |I \<times> B|"
    1.42 -  using LEQ card_of_Sigma_Times by blast
    1.43 +  using card_of_Sigma_mono1[OF LEQ] by blast
    1.44    moreover have "|I \<times> B| =o |B|"
    1.45    using INF * LEQ_I by (auto simp add: card_of_Times_infinite)
    1.46    ultimately show ?thesis using ordLeq_ordIso_trans by blast
    1.47 @@ -1656,4 +1660,27 @@
    1.48    qed(unfold Func_def fun_eq_iff, auto)
    1.49  qed
    1.50  
    1.51 +lemma Func_Times_Range:
    1.52 +  "|Func A (B <*> C)| =o |Func A B <*> Func A C|" (is "|?LHS| =o |?RHS|")
    1.53 +proof -
    1.54 +  let ?F = "\<lambda>fg. (\<lambda>x. if x \<in> A then fst (fg x) else undefined,
    1.55 +                  \<lambda>x. if x \<in> A then snd (fg x) else undefined)"
    1.56 +  let ?G = "\<lambda>(f, g) x. if x \<in> A then (f x, g x) else undefined"
    1.57 +  have "bij_betw ?F ?LHS ?RHS" unfolding bij_betw_def inj_on_def
    1.58 +  proof (intro conjI impI ballI equalityI subsetI)
    1.59 +    fix f g assume *: "f \<in> Func A (B \<times> C)" "g \<in> Func A (B \<times> C)" "?F f = ?F g"
    1.60 +    show "f = g"
    1.61 +    proof
    1.62 +      fix x from * have "fst (f x) = fst (g x) \<and> snd (f x) = snd (g x)"
    1.63 +        by (case_tac "x \<in> A") (auto simp: Func_def fun_eq_iff split: if_splits)
    1.64 +      then show "f x = g x" by (subst (1 2) surjective_pairing) simp
    1.65 +    qed
    1.66 +  next
    1.67 +    fix fg assume "fg \<in> Func A B \<times> Func A C"
    1.68 +    thus "fg \<in> ?F ` Func A (B \<times> C)"
    1.69 +      by (intro image_eqI[of _ _ "?G fg"]) (auto simp: Func_def)
    1.70 +  qed (auto simp: Func_def fun_eq_iff)
    1.71 +  thus ?thesis using card_of_ordIso by blast
    1.72 +qed
    1.73 +
    1.74  end