--- 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";