# HG changeset patch # User paulson # Date 959357005 -7200 # Node ID fe1f3d52e0277ebd046a1d82383a71864a7c4e22 # Parent 4e55d773d0185f7a003ae223dd660a58bc574c62 new setsum results diff -r 4e55d773d018 -r fe1f3d52e027 src/HOL/Finite.ML --- a/src/HOL/Finite.ML Fri May 26 17:29:07 2000 +0200 +++ b/src/HOL/Finite.ML Fri May 26 18:03:25 2000 +0200 @@ -236,131 +236,10 @@ section "Finite cardinality -- 'card'"; -(* Ugly proofs for the traditional definition - -Goal "{f i |i. (P i | i=n)} = insert (f n) {f i|i. P i}"; -by (Blast_tac 1); -val Collect_conv_insert = result(); - -Goalw [card_def] "card {} = 0"; -by (rtac Least_equality 1); -by (ALLGOALS Asm_full_simp_tac); -qed "card_empty"; -Addsimps [card_empty]; - -Goal "finite A ==> ? (n::nat) f. A = {f i |i. i ? m::nat. m \ -\ (LEAST n. ? f. insert x A = {f i|i. i card(insert x A) = Suc(card A)"; -by (etac lemma 1); -by (assume_tac 1); -qed "card_insert_disjoint"; -Addsimps [card_insert_disjoint]; -*) - -val cardR_emptyE = cardR.mk_cases "({},n) : cardR"; AddSEs [cardR_emptyE]; -val cardR_insertE = cardR.mk_cases "(insert a A,n) : cardR"; AddSIs cardR.intrs; Goal "[| (A,n) : cardR |] ==> a : A --> (? m. n = Suc m)"; @@ -795,7 +674,7 @@ Close_locale "ACe"; -(*** setsum ***) +(*** setsum: generalized summation over a set ***) Goalw [setsum_def] "setsum f {} = 0"; by (Simp_tac 1); @@ -823,6 +702,28 @@ [Int_insert_left, insert_absorb]) 1); qed "setsum_Un_Int"; +Goal "[| finite A; finite B; A Int B = {} |] \ +\ ==> setsum g (A Un B) = setsum g A + setsum g B"; +by (stac (setsum_Un_Int RS sym) 1); +by Auto_tac; +qed "setsum_Un_disjoint"; + +Goal "[| finite I |] \ +\ ==> (ALL i:I. finite (A i)) --> (ALL i:I. ALL j:I. A i Int A j = {}) \ +\ --> setsum f (UNION I A) = setsum (%i. setsum f (A i)) I"; +by (etac finite_induct 1); +by (Simp_tac 1); +by (asm_simp_tac (simpset() addsimps [setsum_Un_disjoint]) 1); +qed_spec_mp "setsum_UN_disjoint"; + +Goal "finite A ==> setsum (%x. f x + g x) A = setsum f A + setsum g A"; +by (etac finite_induct 1); +by Auto_tac; +by (simp_tac (simpset() addsimps (thms "plus_ac0")) 1); +qed "setsum_addf"; + +(** For the natural numbers, we have subtraction **) + Goal "[| finite A; finite B |] \ \ ==> (setsum f (A Un B) :: nat) = \ \ setsum f A + setsum f B - setsum f (A Int B)"; @@ -839,12 +740,6 @@ by Auto_tac; qed_spec_mp "setsum_diff1"; -Goal "finite A ==> setsum (%x. f x + g x) A = setsum f A + setsum g A"; -by (etac finite_induct 1); -by Auto_tac; -by (simp_tac (simpset() addsimps (thms "plus_ac0")) 1); -qed "setsum_addf"; - (*** Basic theorem about "choose". By Florian Kammueller, tidied by LCP ***)