# HG changeset patch
# User ballarin
# Date 981791376 -3600
# Node ID 69c1abb9a12992e4de7cd4720418790807ee93e2
# Parent  45ffef3d3e752dab4e4cffce29b50c78071a2221
Definition of setsum (sort constraint) relaxed to {zero, plus}.

diff -r 45ffef3d3e75 -r 69c1abb9a129 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Sat Feb 10 08:48:10 2001 +0100
+++ b/src/HOL/Finite.ML	Sat Feb 10 08:49:36 2001 +0100
@@ -719,13 +719,14 @@
 Addsimps [setsum_empty];
 
 Goalw [setsum_def]
- "[| finite F; a ~: F |] ==> setsum f (insert a F) = f(a) + setsum f F";
+ "!!f::'a=>'b::plus_ac0. [| finite F; a ~: F |] ==> \
+\      setsum f (insert a F) = f(a) + setsum f F";
 by (asm_simp_tac (simpset() addsimps [export fold_insert,
 				      thm "plus_ac0_left_commute"]) 1);
 qed "setsum_insert";
 Addsimps [setsum_insert];
 
-Goal "setsum (%i. 0) A = 0";
+Goal "setsum (%i. 0) A = (0::'a::plus_ac0)";
 by (case_tac "finite A" 1);
  by (asm_simp_tac (simpset() addsimps [setsum_def]) 2); 
 by (etac finite_induct 1);
@@ -753,7 +754,7 @@
 qed "card_eq_setsum";
 
 (*The reversed orientation looks more natural, but LOOPS as a simprule!*)
-Goal "[| finite A; finite B |] \
+Goal "!!g::'a=>'b::plus_ac0. [| finite A; finite B |] \
 \     ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B";
 by (etac finite_induct 1);
 by (Simp_tac 1);
@@ -762,12 +763,12 @@
 qed "setsum_Un_Int";
 
 Goal "[| finite A; finite B; A Int B = {} |] \
-\     ==> setsum g (A Un B) = setsum g A + setsum g B";  
+\     ==> setsum g (A Un B) = (setsum g A + setsum g B::'a::plus_ac0)";  
 by (stac (setsum_Un_Int RS sym) 1);
 by Auto_tac;
 qed "setsum_Un_disjoint";
 
-Goal "finite I \
+Goal "!!f::'a=>'b::plus_ac0. finite I \
 \     ==> (ALL i:I. finite (A i)) --> \
 \         (ALL i:I. ALL j:I. i~=j --> A i Int A j = {}) --> \
 \         setsum f (UNION I A) = setsum (%i. setsum f (A i)) I"; 
@@ -781,7 +782,7 @@
 by (asm_simp_tac (simpset() addsimps [setsum_Un_disjoint]) 1);
 qed_spec_mp "setsum_UN_disjoint";
 
-Goal "setsum (%x. f x + g x) A = setsum f A + setsum g A";
+Goal "setsum (%x. f x + g x) A = (setsum f A + setsum g A::'a::plus_ac0)";
 by (case_tac "finite A" 1);
  by (asm_full_simp_tac (simpset() addsimps [setsum_def]) 2); 
 by (etac finite_induct 1);
@@ -809,7 +810,8 @@
 qed_spec_mp "setsum_diff1";
 
 val prems = Goal
-    "[| A = B; !!x. x:B ==> f x = g x|] ==> setsum f A = setsum g B";
+    "[| A = B; !!x. x:B ==> f x = g x|] \
+\    ==> setsum f A = (setsum g B::'a::plus_ac0)";
 by (case_tac "finite B" 1);
  by (asm_simp_tac (simpset() addsimps [setsum_def]@prems) 2); 
 by (simp_tac (simpset() addsimps prems) 1);
diff -r 45ffef3d3e75 -r 69c1abb9a129 src/HOL/Finite.thy
--- a/src/HOL/Finite.thy	Sat Feb 10 08:48:10 2001 +0100
+++ b/src/HOL/Finite.thy	Sat Feb 10 08:49:36 2001 +0100
@@ -58,7 +58,7 @@
    fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a"
   "fold f e A == @x. (A,x) : foldSet f e"
 
-   setsum :: "('a => 'b) => 'a set => ('b::plus_ac0)"
+   setsum :: "('a => 'b) => 'a set => ('b::{plus, zero})"
   "setsum f A == if finite A then fold (op+ o f) 0 A else 0"
 
 locale LC =