# HG changeset patch
# User nipkow
# Date 1345532549 -7200
# Node ID 3db108d14239da44f9f1a261079f168b2038bd62
# Parent  aeea516440c847a643d9fec04b9fce183556794a
abstracted lemmas

diff -r aeea516440c8 -r 3db108d14239 src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Mon Aug 20 21:52:31 2012 +0200
+++ b/src/HOL/Big_Operators.thy	Tue Aug 21 09:02:29 2012 +0200
@@ -108,6 +108,24 @@
 lemma F_fun_f: "F (%x. g x * h x) A = (F g A * F h A)"
 by (cases "finite A") (simp_all add: distrib)
 
+
+text {* for ad-hoc proofs for @{const fold_image} *}
+lemma comm_monoid_mult:  "class.comm_monoid_mult (op *) 1"
+proof qed (auto intro: assoc commute)
+
+lemma F_Un_neutral:
+  assumes fS: "finite S" and fT: "finite T"
+  and I1: "\<forall>x \<in> S\<inter>T. g x = 1"
+  shows "F g (S \<union> T) = F g S  * F g T"
+proof -
+  interpret comm_monoid_mult "op *" 1 by (fact comm_monoid_mult)
+  show ?thesis
+  using fS fT
+  apply (simp add: F_eq)
+  apply (rule fold_image_Un_one)
+  using I1 by auto
+qed
+
 lemma If_cases:
   fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
   assumes fA: "finite A"
@@ -373,6 +391,28 @@
 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
 by (fact setsum.F_fun_f)
 
+lemma setsum_Un_zero:  
+  "\<lbrakk> finite S; finite T; \<forall>x \<in> S\<inter>T. f x = 0 \<rbrakk> \<Longrightarrow>
+  setsum f (S \<union> T) = setsum f S + setsum f T"
+by(fact setsum.F_Un_neutral)
+
+lemma setsum_UNION_zero: 
+  assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
+  and f0: "\<And>T1 T2 x. T1\<in>S \<Longrightarrow> T2\<in>S \<Longrightarrow> T1 \<noteq> T2 \<Longrightarrow> x \<in> T1 \<Longrightarrow> x \<in> T2 \<Longrightarrow> f x = 0"
+  shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S"
+  using fSS f0
+proof(induct rule: finite_induct[OF fS])
+  case 1 thus ?case by simp
+next
+  case (2 T F)
+  then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F" 
+    and H: "setsum f (\<Union> F) = setsum (setsum f) F" by auto
+  from fTF have fUF: "finite (\<Union>F)" by auto
+  from "2.prems" TF fTF
+  show ?case 
+    by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f])
+qed
+
 
 subsubsection {* Properties in more restricted classes of structures *}
 
@@ -421,36 +461,6 @@
   done
 qed
 
-lemma (in comm_monoid_add) setsum_Un_zero:  
-  assumes fS: "finite S" and fT: "finite T"
-  and I0: "\<forall>x \<in> S\<inter>T. f x = 0"
-  shows "setsum f (S \<union> T) = setsum f S  + setsum f T"
-proof -
-  interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
-  show ?thesis
-  using fS fT
-  apply (simp add: setsum_def)
-  apply (rule fold_image_Un_one)
-  using I0 by auto
-qed
-
-lemma setsum_UNION_zero: 
-  assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
-  and f0: "\<And>T1 T2 x. T1\<in>S \<Longrightarrow> T2\<in>S \<Longrightarrow> T1 \<noteq> T2 \<Longrightarrow> x \<in> T1 \<Longrightarrow> x \<in> T2 \<Longrightarrow> f x = 0"
-  shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S"
-  using fSS f0
-proof(induct rule: finite_induct[OF fS])
-  case 1 thus ?case by simp
-next
-  case (2 T F)
-  then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F" 
-    and H: "setsum f (\<Union> F) = setsum (setsum f) F" by auto
-  from fTF have fUF: "finite (\<Union>F)" by auto
-  from "2.prems" TF fTF
-  show ?case 
-    by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f])
-qed
-
 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
   (if a:A then setsum f A - f a else setsum f A)"
 apply (case_tac "finite A")
@@ -959,15 +969,9 @@
       by (simp add: eq)
 qed
 
-lemma setprod_Un_one:  
-  assumes fS: "finite S" and fT: "finite T"
-  and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
-  shows "setprod f (S \<union> T) = setprod f S  * setprod f T"
-  using fS fT
-  apply (simp add: setprod_def)
-  apply (rule fold_image_Un_one)
-  using I0 by auto
-
+lemma setprod_Un_one: "\<lbrakk> finite S; finite T; \<forall>x \<in> S\<inter>T. f x = 1 \<rbrakk>
+  \<Longrightarrow> setprod f (S \<union> T) = setprod f S  * setprod f T"
+by(fact setprod.F_Un_neutral)
 
 lemmas setprod_1 = setprod.F_neutral
 lemmas setprod_1' = setprod.F_neutral'