tuned proofs; removed duplicated facts
authortraytel
Tue Mar 18 11:47:59 2014 +0100 (2014-03-18)
changeset 56191159b0c88b4a4
parent 56190 f0d2609c4cdc
child 56192 d666cb0e4cf9
tuned proofs; removed duplicated facts
src/HOL/BNF_Cardinal_Arithmetic.thy
src/HOL/BNF_Cardinal_Order_Relation.thy
src/HOL/BNF_Constructions_on_Wellorders.thy
src/HOL/Cardinals/Cardinal_Order_Relation.thy
     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"
     2.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Tue Mar 18 10:12:58 2014 +0100
     2.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Tue Mar 18 11:47:59 2014 +0100
     2.3 @@ -98,7 +98,7 @@
     2.4    have 4: "p' =o ?p \<and> Well_order ?p"
     2.5    using 0 2 3 by (auto simp add: dir_image_ordIso Well_order_dir_image)
     2.6    moreover have "Field ?p =  Field r"
     2.7 -  using 0 3 by (auto simp add: dir_image_Field2 order_on_defs)
     2.8 +  using 0 3 by (auto simp add: dir_image_Field)
     2.9    ultimately have "well_order_on (Field r) ?p" by auto
    2.10    hence "r \<le>o ?p" using CO unfolding card_order_on_def by auto
    2.11    thus "r' \<le>o p'"
    2.12 @@ -709,10 +709,6 @@
    2.13    thus ?thesis using card_of_ordLeq by blast
    2.14  qed
    2.15  
    2.16 -corollary card_of_Sigma_Times:
    2.17 -"\<forall>i \<in> I. |A i| \<le>o |B| \<Longrightarrow> |SIGMA i : I. A i| \<le>o |I \<times> B|"
    2.18 -by (fact card_of_Sigma_mono1)
    2.19 -
    2.20  lemma card_of_UNION_Sigma:
    2.21  "|\<Union>i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
    2.22  using Ex_inj_on_UNION_Sigma[of I A] card_of_ordLeq by blast
    2.23 @@ -791,6 +787,14 @@
    2.24          ordLeq_total[of "|A|"] by blast
    2.25  qed
    2.26  
    2.27 +lemma card_of_Times_Plus_distrib:
    2.28 +  "|A <*> (B <+> C)| =o |A <*> B <+> A <*> C|" (is "|?RHS| =o |?LHS|")
    2.29 +proof -
    2.30 +  let ?f = "\<lambda>(a, bc). case bc of Inl b \<Rightarrow> Inl (a, b) | Inr c \<Rightarrow> Inr (a, c)"
    2.31 +  have "bij_betw ?f ?RHS ?LHS" unfolding bij_betw_def inj_on_def by force
    2.32 +  thus ?thesis using card_of_ordIso by blast
    2.33 +qed
    2.34 +
    2.35  lemma card_of_ordLeq_finite:
    2.36  assumes "|A| \<le>o |B|" and "finite B"
    2.37  shows "finite A"
    2.38 @@ -1011,7 +1015,7 @@
    2.39  proof(cases "I = {}", simp add: card_of_empty)
    2.40    assume *: "I \<noteq> {}"
    2.41    have "|SIGMA i : I. A i| \<le>o |I \<times> B|"
    2.42 -  using LEQ card_of_Sigma_Times by blast
    2.43 +  using card_of_Sigma_mono1[OF LEQ] by blast
    2.44    moreover have "|I \<times> B| =o |B|"
    2.45    using INF * LEQ_I by (auto simp add: card_of_Times_infinite)
    2.46    ultimately show ?thesis using ordLeq_ordIso_trans by blast
    2.47 @@ -1656,4 +1660,27 @@
    2.48    qed(unfold Func_def fun_eq_iff, auto)
    2.49  qed
    2.50  
    2.51 +lemma Func_Times_Range:
    2.52 +  "|Func A (B <*> C)| =o |Func A B <*> Func A C|" (is "|?LHS| =o |?RHS|")
    2.53 +proof -
    2.54 +  let ?F = "\<lambda>fg. (\<lambda>x. if x \<in> A then fst (fg x) else undefined,
    2.55 +                  \<lambda>x. if x \<in> A then snd (fg x) else undefined)"
    2.56 +  let ?G = "\<lambda>(f, g) x. if x \<in> A then (f x, g x) else undefined"
    2.57 +  have "bij_betw ?F ?LHS ?RHS" unfolding bij_betw_def inj_on_def
    2.58 +  proof (intro conjI impI ballI equalityI subsetI)
    2.59 +    fix f g assume *: "f \<in> Func A (B \<times> C)" "g \<in> Func A (B \<times> C)" "?F f = ?F g"
    2.60 +    show "f = g"
    2.61 +    proof
    2.62 +      fix x from * have "fst (f x) = fst (g x) \<and> snd (f x) = snd (g x)"
    2.63 +        by (case_tac "x \<in> A") (auto simp: Func_def fun_eq_iff split: if_splits)
    2.64 +      then show "f x = g x" by (subst (1 2) surjective_pairing) simp
    2.65 +    qed
    2.66 +  next
    2.67 +    fix fg assume "fg \<in> Func A B \<times> Func A C"
    2.68 +    thus "fg \<in> ?F ` Func A (B \<times> C)"
    2.69 +      by (intro image_eqI[of _ _ "?G fg"]) (auto simp: Func_def)
    2.70 +  qed (auto simp: Func_def fun_eq_iff)
    2.71 +  thus ?thesis using card_of_ordIso by blast
    2.72 +qed
    2.73 +
    2.74  end
     3.1 --- a/src/HOL/BNF_Constructions_on_Wellorders.thy	Tue Mar 18 10:12:58 2014 +0100
     3.2 +++ b/src/HOL/BNF_Constructions_on_Wellorders.thy	Tue Mar 18 11:47:59 2014 +0100
     3.3 @@ -894,8 +894,8 @@
     3.4  "dir_image r f = {(f a, f b)| a b. (a,b) \<in> r}"
     3.5  
     3.6  lemma dir_image_Field:
     3.7 -"Field(dir_image r f) \<le> f ` (Field r)"
     3.8 -unfolding dir_image_def Field_def by auto
     3.9 +"Field(dir_image r f) = f ` (Field r)"
    3.10 +unfolding dir_image_def Field_def Range_def Domain_def by fast
    3.11  
    3.12  lemma dir_image_minus_Id:
    3.13  "inj_on f (Field r) \<Longrightarrow> (dir_image r f) - Id = dir_image (r - Id) f"
    3.14 @@ -965,7 +965,7 @@
    3.15    fix a' b'
    3.16    assume "a' \<in> Field (dir_image r f)" "b' \<in> Field (dir_image r f)"
    3.17    then obtain a and b where 1: "a \<in> Field r \<and> b \<in> Field r \<and> f a = a' \<and> f b = b'"
    3.18 -  using dir_image_Field[of r f] by blast
    3.19 +    unfolding dir_image_Field[of r f] by blast
    3.20    moreover assume "a' \<noteq> b'"
    3.21    ultimately have "a \<noteq> b" using INJ unfolding inj_on_def by auto
    3.22    hence "(a,b) \<in> r \<or> (b,a) \<in> r" using 1 TOT unfolding total_on_def by auto
    3.23 @@ -984,10 +984,9 @@
    3.24    fix A'::"'b set"
    3.25    assume SUB: "A' \<le> Field(dir_image r f)" and NE: "A' \<noteq> {}"
    3.26    obtain A where A_def: "A = {a \<in> Field r. f a \<in> A'}" by blast
    3.27 -  have "A \<noteq> {} \<and> A \<le> Field r"
    3.28 -  using A_def dir_image_Field[of r f] SUB NE by blast
    3.29 +  have "A \<noteq> {} \<and> A \<le> Field r" using A_def SUB NE by (auto simp: dir_image_Field)
    3.30    then obtain a where 1: "a \<in> A \<and> (\<forall>b \<in> A. (b,a) \<notin> r)"
    3.31 -  using WF unfolding wf_eq_minimal2 by blast
    3.32 +  using spec[OF WF[unfolded wf_eq_minimal2], of A] by blast
    3.33    have "\<forall>b' \<in> A'. (b',f a) \<notin> dir_image r f"
    3.34    proof(clarify)
    3.35      fix b' assume *: "b' \<in> A'" and **: "(b',f a) \<in> dir_image r f"
    3.36 @@ -1010,14 +1009,9 @@
    3.37    subset_inj_on[of f "Field r" "Field(r - Id)"]
    3.38    mono_Field[of "r - Id" r] by auto
    3.39  
    3.40 -lemma dir_image_Field2:
    3.41 -"Refl r \<Longrightarrow> Field(dir_image r f) = f ` (Field r)"
    3.42 -unfolding Field_def dir_image_def refl_on_def Domain_def Range_def by blast
    3.43 -
    3.44  lemma dir_image_bij_betw:
    3.45 -"\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> bij_betw f (Field r) (Field (dir_image r f))"
    3.46 -unfolding bij_betw_def
    3.47 -by (simp add: dir_image_Field2 order_on_defs)
    3.48 +"\<lbrakk>inj_on f (Field r)\<rbrakk> \<Longrightarrow> bij_betw f (Field r) (Field (dir_image r f))"
    3.49 +unfolding bij_betw_def by (simp add: dir_image_Field order_on_defs)
    3.50  
    3.51  lemma dir_image_compat:
    3.52  "compat r (dir_image r f) f"
     4.1 --- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Tue Mar 18 10:12:58 2014 +0100
     4.2 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Tue Mar 18 11:47:59 2014 +0100
     4.3 @@ -430,10 +430,6 @@
     4.4  using assms card_of_cong card_of_Sigma_cong
     4.5        [of f I J "\<lambda> j. Field(p j)" "\<lambda> j. Field(r j)"] by blast
     4.6  
     4.7 -corollary ordLeq_Sigma_Times:
     4.8 -"\<forall>i \<in> I. p i \<le>o r \<Longrightarrow> |SIGMA i : I. Field (p i)| \<le>o |I \<times> (Field r)|"
     4.9 -by (auto simp add: card_of_Sigma_Times)
    4.10 -
    4.11  lemma card_of_UNION_Sigma2:
    4.12  assumes
    4.13  "!! i j. \<lbrakk>{i,j} <= I; i ~= j\<rbrakk> \<Longrightarrow> A i Int A j = {}"