# HG changeset patch
# User paulson
# Date 1103017516 -3600
# Node ID a063687d24ebf9e292f1782607ef8785be64f916
# Parent  6001135caa918b4e374138de1ee046c6afbf468d
new and stronger lemmas and improved simplification for finite sets

diff -r 6001135caa91 -r a063687d24eb src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Dec 14 10:40:07 2004 +0100
+++ b/src/HOL/Finite_Set.thy	Tue Dec 14 10:45:16 2004 +0100
@@ -303,6 +303,37 @@
    apply (erule finite_SigmaI, auto)
   done
 
+lemma finite_cartesian_productD1:
+     "[| finite (A <*> B); B \<noteq> {} |] ==> finite A"
+apply (auto simp add: finite_conv_nat_seg_image) 
+apply (drule_tac x=n in spec) 
+apply (drule_tac x="fst o f" in spec) 
+apply (auto simp add: o_def) 
+ prefer 2 apply (force dest!: equalityD2) 
+apply (drule equalityD1) 
+apply (rename_tac y x)
+apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)") 
+ prefer 2 apply force
+apply clarify
+apply (rule_tac x=k in image_eqI, auto)
+done
+
+lemma finite_cartesian_productD2:
+     "[| finite (A <*> B); A \<noteq> {} |] ==> finite B"
+apply (auto simp add: finite_conv_nat_seg_image) 
+apply (drule_tac x=n in spec) 
+apply (drule_tac x="snd o f" in spec) 
+apply (auto simp add: o_def) 
+ prefer 2 apply (force dest!: equalityD2) 
+apply (drule equalityD1)
+apply (rename_tac x y)
+apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)") 
+ prefer 2 apply force
+apply clarify
+apply (rule_tac x=k in image_eqI, auto)
+done
+
+
 instance unit :: finite
 proof
   have "finite {()}" by simp
@@ -889,6 +920,9 @@
     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   by (simp add: setsum_def ACf.fold_insert [OF ACf_add])
 
+lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0"
+  by (simp add: setsum_def)
+
 lemma setsum_reindex:
      "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
 by(auto simp add: setsum_def ACf.fold_reindex[OF ACf_add] dest!:finite_imageD)
@@ -926,36 +960,44 @@
   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
 by (subst setsum_Un_Int [symmetric], auto)
 
-(* FIXME get rid of finite I. If infinite, rhs is directly 0, and UNION I A
-is also infinite and hence also 0 *)
+(*But we can't get rid of finite I. If infinite, although the rhs is 0, 
+  the lhs need not be, since UNION I A could still be finite.*)
 lemma setsum_UN_disjoint:
     "finite I ==> (ALL i:I. finite (A i)) ==>
         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
       setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
 by(simp add: setsum_def ACe.fold_UN_disjoint[OF ACe_add] cong: setsum_cong)
 
-
-(* FIXME get rid of finite C. If infinite, rhs is directly 0, and Union C
-is also infinite and hence also 0 *)
+text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
+directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
 lemma setsum_Union_disjoint:
-  "finite C ==> (ALL A:C. finite A) ==>
-        (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
-      setsum f (Union C) = setsum (setsum f) C"
+  "[| (ALL A:C. finite A);
+      (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
+   ==> setsum f (Union C) = setsum (setsum f) C"
+apply (cases "finite C") 
+ prefer 2 apply (force dest: finite_UnionD simp add: setsum_def)
   apply (frule setsum_UN_disjoint [of C id f])
-  apply (unfold Union_def id_def, assumption+)
-  done
+ apply (unfold Union_def id_def, assumption+)
+done
 
-(* FIXME get rid of finite A. If infinite, lhs is directly 0, and SIGMA A B
-is either infinite or empty, and in both cases the rhs is also 0 *)
+(*But we can't get rid of finite A. If infinite, although the lhs is 0, 
+  the rhs need not be, since SIGMA A B could still be finite.*)
 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
     (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) =
     (\<Sum>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))"
 by(simp add:setsum_def ACe.fold_Sigma[OF ACe_add] split_def cong:setsum_cong)
 
-lemma setsum_cartesian_product: "finite A ==> finite B ==>
-    (\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) =
-    (\<Sum>z\<in>A <*> B. f (fst z) (snd z))"
-  by (erule setsum_Sigma, auto)
+text{*Here we can eliminate the finiteness assumptions, by cases.*}
+lemma setsum_cartesian_product: 
+   "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>z\<in>A <*> B. f (fst z) (snd z))"
+apply (cases "finite A") 
+ apply (cases "finite B") 
+  apply (simp add: setsum_Sigma)
+ apply (cases "A={}", simp)
+ apply (simp add: setsum_0) 
+apply (auto simp add: setsum_def
+            dest: finite_cartesian_productD1 finite_cartesian_productD2) 
+done
 
 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
 by(simp add:setsum_def ACe.fold_distrib[OF ACe_add])
@@ -1176,6 +1218,9 @@
     setprod f (insert a A) = f a * setprod f A"
 by (simp add: setprod_def ACf.fold_insert [OF ACf_mult])
 
+lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
+  by (simp add: setprod_def)
+
 lemma setprod_reindex:
      "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
 by(auto simp: setprod_def ACf.fold_reindex[OF ACf_mult] dest!:finite_imageD)
@@ -1195,7 +1240,6 @@
 lemma setprod_1: "setprod (%i. 1) A = 1"
   apply (case_tac "finite A")
   apply (erule finite_induct, auto simp add: mult_ac)
-  apply (simp add: setprod_def)
   done
 
 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
@@ -1219,25 +1263,34 @@
 by(simp add: setprod_def ACe.fold_UN_disjoint[OF ACe_mult] cong: setprod_cong)
 
 lemma setprod_Union_disjoint:
-  "finite C ==> (ALL A:C. finite A) ==>
-        (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
-      setprod f (Union C) = setprod (setprod f) C"
+  "[| (ALL A:C. finite A);
+      (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |] 
+   ==> setprod f (Union C) = setprod (setprod f) C"
+apply (cases "finite C") 
+ prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
   apply (frule setprod_UN_disjoint [of C id f])
-  apply (unfold Union_def id_def, assumption+)
-  done
+ apply (unfold Union_def id_def, assumption+)
+done
 
 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
     (\<Prod>x:A. (\<Prod>y: B x. f x y)) =
     (\<Prod>z:(SIGMA x:A. B x). f (fst z) (snd z))"
 by(simp add:setprod_def ACe.fold_Sigma[OF ACe_mult] split_def cong:setprod_cong)
 
-lemma setprod_cartesian_product: "finite A ==> finite B ==>
-    (\<Prod>x:A. (\<Prod>y: B. f x y)) =
-    (\<Prod>z:(A <*> B). f (fst z) (snd z))"
-  by (erule setprod_Sigma, auto)
+text{*Here we can eliminate the finiteness assumptions, by cases.*}
+lemma setprod_cartesian_product: 
+     "(\<Prod>x:A. (\<Prod>y: B. f x y)) = (\<Prod>z:(A <*> B). f (fst z) (snd z))"
+apply (cases "finite A") 
+ apply (cases "finite B") 
+  apply (simp add: setprod_Sigma)
+ apply (cases "A={}", simp)
+ apply (simp add: setprod_1) 
+apply (auto simp add: setprod_def
+            dest: finite_cartesian_productD1 finite_cartesian_productD2) 
+done
 
 lemma setprod_timesf:
-  "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
+     "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
 by(simp add:setprod_def ACe.fold_distrib[OF ACe_mult])
 
 
@@ -1348,6 +1401,9 @@
 lemma card_empty [simp]: "card {} = 0"
   by (simp add: card_def)
 
+lemma card_infinite [simp]: "~ finite A ==> card A = 0"
+  by (simp add: card_def)
+
 lemma card_eq_setsum: "card A = setsum (%x. 1) A"
 by (simp add: card_def)
 
@@ -1365,6 +1421,9 @@
   apply (auto)
   done
 
+lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
+by auto
+
 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
 apply(simp del:insert_Diff_single)
@@ -1452,11 +1511,12 @@
 done
 
 
-lemma setsum_constant_nat:
-    "finite A ==> (\<Sum>x\<in>A. y) = (card A) * y"
+lemma setsum_constant_nat: "(\<Sum>x\<in>A. y) = (card A) * y"
   -- {* Generalized to any @{text comm_semiring_1_cancel} in
         @{text IntDef} as @{text setsum_constant}. *}
-by (erule finite_induct, auto)
+apply (cases "finite A") 
+apply (erule finite_induct, auto)
+done
 
 lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::recpower)) = y^(card A)"
   apply (erule finite_induct)
@@ -1537,18 +1597,17 @@
   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
 by(simp add:card_def setsum_Sigma)
 
-(* FIXME get rid of prems *)
-lemma card_cartesian_product:
-     "[| finite A; finite B |] ==> card (A <*> B) = card(A) * card(B)"
-  by (simp add: setsum_constant_nat)
+lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
+apply (cases "finite A") 
+apply (cases "finite B") 
+  apply (simp add: setsum_constant_nat) 
+apply (auto simp add: card_eq_0_iff
+            dest: finite_cartesian_productD1 finite_cartesian_productD2) 
+done
 
-(* FIXME should really be a consequence of card_cartesian_product *)
 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
-  apply (subgoal_tac "inj_on (%y .(x,y)) A")
-  apply (frule card_image)
-  apply (subgoal_tac "(Pair x ` A) = {x} <*> A")
-  apply (auto simp add: inj_on_def)
-  done
+by (simp add: card_cartesian_product) 
+
 
 
 subsubsection {* Cardinality of the Powerset *}
diff -r 6001135caa91 -r a063687d24eb src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Tue Dec 14 10:40:07 2004 +0100
+++ b/src/HOL/Integ/IntDef.thy	Tue Dec 14 10:45:16 2004 +0100
@@ -843,13 +843,11 @@
 lemma setsum_of_nat: "of_nat (setsum f A) = setsum (of_nat \<circ> f) A"
   apply (case_tac "finite A")
   apply (erule finite_induct, auto)
-  apply (simp add: setsum_def)
   done
 
 lemma setsum_of_int: "of_int (setsum f A) = setsum (of_int \<circ> f) A"
   apply (case_tac "finite A")
   apply (erule finite_induct, auto)
-  apply (simp add: setsum_def)
   done
 
 lemma int_setsum: "int (setsum f A) = setsum (int \<circ> f) A"
@@ -858,13 +856,11 @@
 lemma setprod_of_nat: "of_nat (setprod f A) = setprod (of_nat \<circ> f) A"
   apply (case_tac "finite A")
   apply (erule finite_induct, auto)
-  apply (simp add: setprod_def)
   done
 
 lemma setprod_of_int: "of_int (setprod f A) = setprod (of_int \<circ> f) A"
   apply (case_tac "finite A")
   apply (erule finite_induct, auto)
-  apply (simp add: setprod_def)
   done
 
 lemma int_setprod: "int (setprod f A) = setprod (int \<circ> f) A"