# HG changeset patch
# User nipkow
# Date 907259444 -7200
# Node ID 5293b6f5c66c0161cd1f726fbb9b1199786a6821
# Parent  b6456ccd9e3e329bd8a4cce39fb4c85133f6ce3d
Improved definition of foldSet.

diff -r b6456ccd9e3e -r 5293b6f5c66c src/HOL/Induct/FoldSet.ML
--- a/src/HOL/Induct/FoldSet.ML	Thu Oct 01 18:30:05 1998 +0200
+++ b/src/HOL/Induct/FoldSet.ML	Thu Oct 01 18:30:44 1998 +0200
@@ -4,6 +4,7 @@
     Copyright   1998  University of Cambridge
 
 A "fold" functional for finite sets
+use_thy"FS";
 *)
 
 val empty_foldSetE = foldSet.mk_cases [] "({}, x) : foldSet f e";
@@ -30,29 +31,10 @@
 qed "finite_imp_foldSet";
 
 
-Open_locale "ACI"; 
+Open_locale "LC"; 
 
 (*Strip meta-quantifiers: perhaps the locale should do this?*)
-val f_ident   = forall_elim_vars 0 (thm "ident");
-val f_commute = forall_elim_vars 0 (thm "commute");
-val f_assoc   = forall_elim_vars 0 (thm "assoc");
-
-
-Goal "f x (f y z) = f y (f x z)";
-by (rtac (f_commute RS trans) 1);
-by (rtac (f_assoc RS trans) 1);
-by (rtac (f_commute RS arg_cong) 1);
-qed "f_left_commute";
-
-(*Addition is an AC-operator*)
-val f_ac = [f_assoc, f_commute, f_left_commute];
-
-Goal "f e x = x";
-by (stac f_commute 1);
-by (rtac f_ident 1);
-qed "f_left_ident";
-
-Addsimps [f_left_ident, f_ident];
+val f_lcomm = forall_elim_vars 0 (thm "lcomm");
 
 
 Goal "ALL A x. card(A) < n --> (A, x) : foldSet f e --> \
@@ -94,7 +76,7 @@
  by (Asm_full_simp_tac 2);
 by (subgoal_tac "yb = f xa x" 1);
  by (blast_tac (claset() addDs [Diff_foldSet]) 2);
-by (asm_simp_tac (simpset() addsimps f_ac) 1);
+by (asm_simp_tac (simpset() addsimps [f_lcomm]) 1);
 val lemma = result();
 
 
@@ -130,24 +112,73 @@
 		        addsimps [symmetric fold_def,
 				  fold_equality]));
 qed "fold_insert";
-Addsimps [fold_insert];
+
+Close_locale();
+
+Open_locale "ACe"; 
+
+(*Strip meta-quantifiers: perhaps the locale should do this?*)
+val f_ident   = forall_elim_vars 0 (thm "ident");
+val f_commute = forall_elim_vars 0 (thm "commute");
+val f_assoc   = forall_elim_vars 0 (thm "assoc");
+
+
+Goal "f x (f y z) = f y (f x z)";
+by (rtac (f_commute RS trans) 1);
+by (rtac (f_assoc RS trans) 1);
+by (rtac (f_commute RS arg_cong) 1);
+qed "f_left_commute";
+
+val f_ac = [f_assoc, f_commute, f_left_commute];
+
+Goal "f e x = x";
+by (stac f_commute 1);
+by (rtac f_ident 1);
+qed "f_left_ident";
+
+val f_idents = [f_left_ident, f_ident];
 
 Goal "[| finite A; finite B |] \
 \     ==> f (fold f e A) (fold f e B) =  \
 \         f (fold f e (A Un B)) (fold f e (A Int B))";
 by (etac finite_induct 1);
-by (Simp_tac 1);
-by (asm_simp_tac
-    (simpset() addsimps f_ac @ [insert_absorb, Int_insert_left]) 1);
-by (rtac impI 1);
-by (stac f_commute 1 THEN rtac refl 1);
+by (simp_tac (simpset() addsimps f_idents) 1);
+by (asm_simp_tac (simpset() addsimps f_ac @ f_idents @
+           [export fold_insert,insert_absorb, Int_insert_left]) 1);
 qed "fold_Un_Int";
 
 Goal "[| finite A; finite B; A Int B = {} |] \
 \     ==> fold f e (A Un B) = f (fold f e A) (fold f e B)";
-by (asm_simp_tac (simpset() addsimps [fold_Un_Int]) 1);
+by (asm_simp_tac (simpset() addsimps fold_Un_Int::f_idents) 1);
 qed "fold_Un_disjoint";
 
-
 Close_locale();
 
+
+(*** setsum ***)
+
+Goalw [setsum_def] "setsum f {} = 0";
+by(Simp_tac 1);
+qed "setsum_empty";
+Addsimps [setsum_empty];
+
+Goalw [setsum_def]
+ "[| finite F; a ~: F |] ==> setsum f (insert a F) = f(a) + setsum f F";
+by(asm_simp_tac (simpset() addsimps [export fold_insert]) 1);
+qed "setsum_insert";
+Addsimps [setsum_insert];
+
+Goal "[| finite A; finite B |] ==> A Int B = {} --> \
+\     setsum f (A Un B) = setsum f A + setsum f B";
+by (etac finite_induct 1);
+by(Simp_tac 1);
+by(asm_simp_tac (simpset() addsimps [Int_insert_left]) 1);
+qed_spec_mp "setsum_disj_Un";
+
+Goal "[| finite F |] ==> \
+\     setsum f (F-{a}) = (if a:F then setsum f F - f a else setsum f F)";
+be finite_induct 1;
+by(auto_tac (claset(), simpset() addsimps [insert_Diff_if]));
+by(dres_inst_tac [("a","a")] mk_disjoint_insert 1);
+by(Auto_tac);
+qed_spec_mp "setsum_diff1";
diff -r b6456ccd9e3e -r 5293b6f5c66c src/HOL/Induct/FoldSet.thy
--- a/src/HOL/Induct/FoldSet.thy	Thu Oct 01 18:30:05 1998 +0200
+++ b/src/HOL/Induct/FoldSet.thy	Thu Oct 01 18:30:44 1998 +0200
@@ -1,16 +1,16 @@
 (*  Title:      HOL/FoldSet
     ID:         $Id$
-    Author:     Lawrence C Paulson
+    Author:     Lawrence C Paulson, Tobias Nipkow
     Copyright   1998  University of Cambridge
 
 A "fold" functional for finite sets.  For n non-negative we have
     fold f e {x1,...,xn} = f x1 (... (f xn e))
-where f is an associative-commutative function and e is its identity.
+where f is at least left-commutative.
 *)
 
 FoldSet = Finite +
 
-consts foldSet :: "[['a,'a] => 'a, 'a] => ('a set * 'a) set"
+consts foldSet :: "[['b,'a] => 'a, 'a] => ('b set * 'a) set"
 
 inductive "foldSet f e"
   intrs
@@ -19,10 +19,22 @@
     insertI  "[| x ~: A;  (A,y) : foldSet f e |]
 	      ==> (insert x A, f x y) : foldSet f e"
 
-constdefs fold :: "[['a,'a] => 'a, 'a, 'a set] => 'a"
+constdefs
+   fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a"
   "fold f e A == @x. (A,x) : foldSet f e"
-  
-locale ACI =
+  (* A frequent instance: *)
+   setsum :: ('a => nat) => 'a set => nat
+  "setsum f == fold (%x n. f x + n) 0"
+
+locale LC =
+  fixes
+    f    :: ['b,'a] => 'a
+  assumes
+    lcomm    "!! x y z. f x (f y z) = f y (f x z)"
+  defines
+    (*nothing*)
+
+locale ACe =
   fixes 
     f    :: ['a,'a] => 'a
     e    :: 'a
@@ -32,6 +44,5 @@
     assoc    "!! x y z. f (f x y) z = f x (f y z)"
   defines
     (*nothing*)
+
 end
-
-