# HG changeset patch
# User traytel
# Date 1395139679 -3600
# Node ID 159b0c88b4a4f1e6922bcc8b73a0a4696fe7fdfe
# Parent  f0d2609c4cdcc85ae43de7e43a9a63ce0f6654b6
tuned proofs; removed duplicated facts

diff -r f0d2609c4cdc -r 159b0c88b4a4 src/HOL/BNF_Cardinal_Arithmetic.thy
--- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Tue Mar 18 10:12:58 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Tue Mar 18 11:47:59 2014 +0100
@@ -14,10 +14,6 @@
 lemma dir_image: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); Card_order r\<rbrakk> \<Longrightarrow> r =o dir_image r f"
 by (rule dir_image_ordIso) (auto simp add: inj_on_def card_order_on_def)
 
-(*should supersede a weaker lemma from the library*)
-lemma dir_image_Field: "Field (dir_image r f) = f ` Field r"
-unfolding dir_image_def Field_def Range_def Domain_def by fast
-
 lemma card_order_dir_image:
   assumes bij: "bij f" and co: "card_order r"
   shows "card_order (dir_image r f)"
@@ -42,37 +38,6 @@
 lemma Field_card_order: "card_order r \<Longrightarrow> Field r = UNIV"
 using card_order_on_Card_order[of UNIV r] by simp
 
-lemma card_of_Times_Plus_distrib:
-  "|A <*> (B <+> C)| =o |A <*> B <+> A <*> C|" (is "|?RHS| =o |?LHS|")
-proof -
-  let ?f = "\<lambda>(a, bc). case bc of Inl b \<Rightarrow> Inl (a, b) | Inr c \<Rightarrow> Inr (a, c)"
-  have "bij_betw ?f ?RHS ?LHS" unfolding bij_betw_def inj_on_def by force
-  thus ?thesis using card_of_ordIso by blast
-qed
-
-lemma Func_Times_Range:
-  "|Func A (B <*> C)| =o |Func A B <*> Func A C|" (is "|?LHS| =o |?RHS|")
-proof -
-  let ?F = "\<lambda>fg. (\<lambda>x. if x \<in> A then fst (fg x) else undefined,
-                  \<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
-  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
-
 
 subsection {* Zero *}
 
@@ -364,7 +329,7 @@
 
 lemma card_of_Csum_Times:
   "\<forall>i \<in> I. |A i| \<le>o |B| \<Longrightarrow> (CSUM i : |I|. |A i| ) \<le>o |I| *c |B|"
-by (simp only: Csum_def cprod_def Field_card_of card_of_Sigma_Times)
+by (simp only: Csum_def cprod_def Field_card_of card_of_Sigma_mono1)
 
 lemma card_of_Csum_Times':
   assumes "Card_order r" "\<forall>i \<in> I. |A i| \<le>o r"
diff -r f0d2609c4cdc -r 159b0c88b4a4 src/HOL/BNF_Cardinal_Order_Relation.thy
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Tue Mar 18 10:12:58 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Tue Mar 18 11:47:59 2014 +0100
@@ -98,7 +98,7 @@
   have 4: "p' =o ?p \<and> Well_order ?p"
   using 0 2 3 by (auto simp add: dir_image_ordIso Well_order_dir_image)
   moreover have "Field ?p =  Field r"
-  using 0 3 by (auto simp add: dir_image_Field2 order_on_defs)
+  using 0 3 by (auto simp add: dir_image_Field)
   ultimately have "well_order_on (Field r) ?p" by auto
   hence "r \<le>o ?p" using CO unfolding card_order_on_def by auto
   thus "r' \<le>o p'"
@@ -709,10 +709,6 @@
   thus ?thesis using card_of_ordLeq by blast
 qed
 
-corollary card_of_Sigma_Times:
-"\<forall>i \<in> I. |A i| \<le>o |B| \<Longrightarrow> |SIGMA i : I. A i| \<le>o |I \<times> B|"
-by (fact card_of_Sigma_mono1)
-
 lemma card_of_UNION_Sigma:
 "|\<Union>i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
 using Ex_inj_on_UNION_Sigma[of I A] card_of_ordLeq by blast
@@ -791,6 +787,14 @@
         ordLeq_total[of "|A|"] by blast
 qed
 
+lemma card_of_Times_Plus_distrib:
+  "|A <*> (B <+> C)| =o |A <*> B <+> A <*> C|" (is "|?RHS| =o |?LHS|")
+proof -
+  let ?f = "\<lambda>(a, bc). case bc of Inl b \<Rightarrow> Inl (a, b) | Inr c \<Rightarrow> Inr (a, c)"
+  have "bij_betw ?f ?RHS ?LHS" unfolding bij_betw_def inj_on_def by force
+  thus ?thesis using card_of_ordIso by blast
+qed
+
 lemma card_of_ordLeq_finite:
 assumes "|A| \<le>o |B|" and "finite B"
 shows "finite A"
@@ -1011,7 +1015,7 @@
 proof(cases "I = {}", simp add: card_of_empty)
   assume *: "I \<noteq> {}"
   have "|SIGMA i : I. A i| \<le>o |I \<times> B|"
-  using LEQ card_of_Sigma_Times by blast
+  using card_of_Sigma_mono1[OF LEQ] by blast
   moreover have "|I \<times> B| =o |B|"
   using INF * LEQ_I by (auto simp add: card_of_Times_infinite)
   ultimately show ?thesis using ordLeq_ordIso_trans by blast
@@ -1656,4 +1660,27 @@
   qed(unfold Func_def fun_eq_iff, auto)
 qed
 
+lemma Func_Times_Range:
+  "|Func A (B <*> C)| =o |Func A B <*> Func A C|" (is "|?LHS| =o |?RHS|")
+proof -
+  let ?F = "\<lambda>fg. (\<lambda>x. if x \<in> A then fst (fg x) else undefined,
+                  \<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
+  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
+
 end
diff -r f0d2609c4cdc -r 159b0c88b4a4 src/HOL/BNF_Constructions_on_Wellorders.thy
--- a/src/HOL/BNF_Constructions_on_Wellorders.thy	Tue Mar 18 10:12:58 2014 +0100
+++ b/src/HOL/BNF_Constructions_on_Wellorders.thy	Tue Mar 18 11:47:59 2014 +0100
@@ -894,8 +894,8 @@
 "dir_image r f = {(f a, f b)| a b. (a,b) \<in> r}"
 
 lemma dir_image_Field:
-"Field(dir_image r f) \<le> f ` (Field r)"
-unfolding dir_image_def Field_def by auto
+"Field(dir_image r f) = f ` (Field r)"
+unfolding dir_image_def Field_def Range_def Domain_def by fast
 
 lemma dir_image_minus_Id:
 "inj_on f (Field r) \<Longrightarrow> (dir_image r f) - Id = dir_image (r - Id) f"
@@ -965,7 +965,7 @@
   fix a' b'
   assume "a' \<in> Field (dir_image r f)" "b' \<in> Field (dir_image r f)"
   then obtain a and b where 1: "a \<in> Field r \<and> b \<in> Field r \<and> f a = a' \<and> f b = b'"
-  using dir_image_Field[of r f] by blast
+    unfolding dir_image_Field[of r f] by blast
   moreover assume "a' \<noteq> b'"
   ultimately have "a \<noteq> b" using INJ unfolding inj_on_def by auto
   hence "(a,b) \<in> r \<or> (b,a) \<in> r" using 1 TOT unfolding total_on_def by auto
@@ -984,10 +984,9 @@
   fix A'::"'b set"
   assume SUB: "A' \<le> Field(dir_image r f)" and NE: "A' \<noteq> {}"
   obtain A where A_def: "A = {a \<in> Field r. f a \<in> A'}" by blast
-  have "A \<noteq> {} \<and> A \<le> Field r"
-  using A_def dir_image_Field[of r f] SUB NE by blast
+  have "A \<noteq> {} \<and> A \<le> Field r" using A_def SUB NE by (auto simp: dir_image_Field)
   then obtain a where 1: "a \<in> A \<and> (\<forall>b \<in> A. (b,a) \<notin> r)"
-  using WF unfolding wf_eq_minimal2 by blast
+  using spec[OF WF[unfolded wf_eq_minimal2], of A] by blast
   have "\<forall>b' \<in> A'. (b',f a) \<notin> dir_image r f"
   proof(clarify)
     fix b' assume *: "b' \<in> A'" and **: "(b',f a) \<in> dir_image r f"
@@ -1010,14 +1009,9 @@
   subset_inj_on[of f "Field r" "Field(r - Id)"]
   mono_Field[of "r - Id" r] by auto
 
-lemma dir_image_Field2:
-"Refl r \<Longrightarrow> Field(dir_image r f) = f ` (Field r)"
-unfolding Field_def dir_image_def refl_on_def Domain_def Range_def by blast
-
 lemma dir_image_bij_betw:
-"\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> bij_betw f (Field r) (Field (dir_image r f))"
-unfolding bij_betw_def
-by (simp add: dir_image_Field2 order_on_defs)
+"\<lbrakk>inj_on f (Field r)\<rbrakk> \<Longrightarrow> bij_betw f (Field r) (Field (dir_image r f))"
+unfolding bij_betw_def by (simp add: dir_image_Field order_on_defs)
 
 lemma dir_image_compat:
 "compat r (dir_image r f) f"
diff -r f0d2609c4cdc -r 159b0c88b4a4 src/HOL/Cardinals/Cardinal_Order_Relation.thy
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Tue Mar 18 10:12:58 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Tue Mar 18 11:47:59 2014 +0100
@@ -430,10 +430,6 @@
 using assms card_of_cong card_of_Sigma_cong
       [of f I J "\<lambda> j. Field(p j)" "\<lambda> j. Field(r j)"] by blast
 
-corollary ordLeq_Sigma_Times:
-"\<forall>i \<in> I. p i \<le>o r \<Longrightarrow> |SIGMA i : I. Field (p i)| \<le>o |I \<times> (Field r)|"
-by (auto simp add: card_of_Sigma_Times)
-
 lemma card_of_UNION_Sigma2:
 assumes
 "!! i j. \<lbrakk>{i,j} <= I; i ~= j\<rbrakk> \<Longrightarrow> A i Int A j = {}"