# HG changeset patch
# User nipkow
# Date 907677593 -7200
# Node ID 497eeeace3fcd1362daba69185f425b4545bc854
# Parent  9ea709aa275cb023f7eb8ab65a7dac8feefdd787
Merges FoldSet into Finite

diff -r 9ea709aa275c -r 497eeeace3fc src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Mon Oct 05 10:33:34 1998 +0200
+++ b/src/HOL/Finite.ML	Tue Oct 06 14:39:53 1998 +0200
@@ -447,3 +447,191 @@
 by (Blast_tac 1);
 qed_spec_mp "dvd_partition";
 
+
+(*** foldSet ***)
+
+val empty_foldSetE = foldSet.mk_cases [] "({}, x) : foldSet f e";
+
+AddSEs [empty_foldSetE];
+AddIs foldSet.intrs;
+
+Goal "[| (A-{x},y) : foldSet f e;  x: A |] ==> (A, f x y) : foldSet f e";
+by (etac (insert_Diff RS subst) 1 THEN resolve_tac foldSet.intrs 1);
+by Auto_tac;
+qed "Diff_foldSet";
+
+Goal "(A, x) : foldSet f e ==> finite(A)";
+by (eresolve_tac [foldSet.induct] 1);
+by Auto_tac;
+qed "foldSet_imp_finite";
+
+Addsimps [foldSet_imp_finite];
+
+
+Goal "finite(A) ==> EX x. (A, x) : foldSet f e";
+by (etac finite_induct 1);
+by Auto_tac;
+qed "finite_imp_foldSet";
+
+
+Open_locale "LC"; 
+
+(*Strip meta-quantifiers: perhaps the locale should do this?*)
+val f_lcomm = forall_elim_vars 0 (thm "lcomm");
+
+
+Goal "ALL A x. card(A) < n --> (A, x) : foldSet f e --> \
+\            (ALL y. (A, y) : foldSet f e --> y=x)";
+by (induct_tac "n" 1);
+by (auto_tac (claset(), simpset() addsimps [less_Suc_eq]));
+by (etac foldSet.elim 1);
+by (Blast_tac 1);
+by (etac foldSet.elim 1);
+by (Blast_tac 1);
+by (Clarify_tac 1);
+(*force simplification of "card A < card (insert ...)"*)
+by (etac rev_mp 1);
+by (asm_simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
+by (rtac impI 1);
+(** LEVEL 10 **)
+by (rename_tac "Aa xa ya Ab xb yb" 1);
+ by (case_tac "xa=xb" 1);
+ by (subgoal_tac "Aa = Ab" 1);
+ by (blast_tac (claset() addEs [equalityE]) 2);
+ by (Blast_tac 1);
+(*case xa ~= xb*)
+by (subgoal_tac "Aa-{xb} = Ab-{xa} & xb : Aa & xa : Ab" 1);
+ by (blast_tac (claset() addEs [equalityE]) 2);
+by (Clarify_tac 1);
+by (subgoal_tac "Aa = insert xb Ab - {xa}" 1);
+ by (blast_tac (claset() addEs [equalityE]) 2);
+(** LEVEL 20 **)
+by (subgoal_tac "card Aa <= card Ab" 1);
+ by (rtac (Suc_le_mono RS subst) 2);
+ by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 2);
+by (res_inst_tac [("A1", "Aa-{xb}"), ("f1","f")] 
+    (finite_imp_foldSet RS exE) 1);
+by (blast_tac (claset() addIs [foldSet_imp_finite, finite_Diff]) 1);
+by (forward_tac [Diff_foldSet] 1 THEN assume_tac 1);
+by (subgoal_tac "ya = f xb x" 1);
+ by (Blast_tac 2);
+by (subgoal_tac "(Ab - {xa}, x) : foldSet f e" 1);
+ 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_lcomm]) 1);
+val lemma = result();
+
+
+Goal "[| (A, x) : foldSet f e;  (A, y) : foldSet f e |] ==> y=x";
+by (blast_tac (claset() addIs [normalize_thm [RSspec, RSmp] lemma]) 1);
+qed "foldSet_determ";
+
+Goalw [fold_def] "(A,y) : foldSet f e ==> fold f e A = y";
+by (blast_tac (claset() addIs [foldSet_determ]) 1);
+qed "fold_equality";
+
+Goalw [fold_def] "fold f e {} = e";
+by (Blast_tac 1);
+qed "fold_empty";
+Addsimps [fold_empty];
+
+Goal "x ~: A ==> \
+\     ((insert x A, v) : foldSet f e) =  \
+\     (EX y. (A, y) : foldSet f e & v = f x y)";
+by Auto_tac;
+by (res_inst_tac [("A1", "A"), ("f1","f")] (finite_imp_foldSet RS exE) 1);
+by (force_tac (claset() addDs [foldSet_imp_finite], simpset()) 1);
+by (blast_tac (claset() addIs [foldSet_determ]) 1);
+val lemma = result();
+
+
+Goalw [fold_def]
+     "[| finite A; x ~: A |] ==> fold f e (insert x A) = f x (fold f e A)";
+by (asm_simp_tac (simpset() addsimps [lemma]) 1);
+by (rtac select_equality 1);
+by (auto_tac (claset() addIs [finite_imp_foldSet],
+	      simpset() addcongs [conj_cong]
+		        addsimps [symmetric fold_def,
+				  fold_equality]));
+qed "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 (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::f_idents) 1);
+qed "fold_Un_disjoint";
+
+Goal
+ "[| finite A; finite B |] ==> A Int B = {} --> \
+\ fold (f o g) e (A Un B) = f (fold (f o g) e A) (fold (f o g) e B)";
+by (etac finite_induct 1);
+by (simp_tac (simpset() addsimps f_idents) 1);
+by (asm_full_simp_tac (simpset() addsimps f_ac @ f_idents @
+           [export fold_insert,insert_absorb, Int_insert_left]) 1);
+qed "fold_Un_disjoint2";
+
+Close_locale();
+
+Delrules ([empty_foldSetE] @ foldSet.intrs);
+Delsimps [foldSet_imp_finite];
+
+(*** 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];
+
+Goalw [setsum_def]
+ "[| finite A; finite B; A Int B = {} |] ==> \
+\ setsum f (A Un B) = setsum f A + setsum f B";
+by(asm_simp_tac (simpset() addsimps [export fold_Un_disjoint2]) 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 9ea709aa275c -r 497eeeace3fc src/HOL/Finite.thy
--- a/src/HOL/Finite.thy	Mon Oct 05 10:33:34 1998 +0200
+++ b/src/HOL/Finite.thy	Tue Oct 06 14:39:53 1998 +0200
@@ -3,7 +3,7 @@
     Author:     Lawrence C Paulson & Tobias Nipkow
     Copyright   1995  University of Cambridge & TU Muenchen
 
-Finite sets and their cardinality
+Finite sets, their cardinality, and a fold functional.
 *)
 
 Finite = Divides + Power + Inductive +
@@ -22,4 +22,44 @@
   card :: 'a set => nat
   "card A == LEAST n. ? f. A = {f i |i. i<n}"
 
+(*
+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 at least left-commutative.
+*)
+
+consts foldSet :: "[['b,'a] => 'a, 'a] => ('b set * 'a) set"
+
+inductive "foldSet f e"
+  intrs
+    emptyI   "({}, e) : foldSet f e"
+
+    insertI  "[| x ~: A;  (A,y) : foldSet f e |]
+	      ==> (insert x A, f x y) : foldSet f e"
+
+constdefs
+   fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a"
+  "fold f e A == @x. (A,x) : foldSet f e"
+  (* A frequent instance: *)
+   setsum :: ('a => nat) => 'a set => nat
+  "setsum f == fold (op+ o f) 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
+  assumes
+    ident    "!! x. f x e = x"
+    commute  "!! x y. f x y = f y x"
+    assoc    "!! x y z. f (f x y) z = f x (f y z)"
+  defines
+
 end
diff -r 9ea709aa275c -r 497eeeace3fc src/HOL/Induct/FoldSet.ML
--- a/src/HOL/Induct/FoldSet.ML	Mon Oct 05 10:33:34 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,184 +0,0 @@
-(*  Title:      HOL/FoldSet
-    ID:         $Id$
-    Author:     Lawrence C Paulson
-    Copyright   1998  University of Cambridge
-
-A "fold" functional for finite sets
-use_thy"FS";
-*)
-
-val empty_foldSetE = foldSet.mk_cases [] "({}, x) : foldSet f e";
-
-AddSEs [empty_foldSetE];
-AddIs foldSet.intrs;
-
-Goal "[| (A-{x},y) : foldSet f e;  x: A |] ==> (A, f x y) : foldSet f e";
-by (etac (insert_Diff RS subst) 1 THEN resolve_tac foldSet.intrs 1);
-by Auto_tac;
-qed "Diff_foldSet";
-
-Goal "(A, x) : foldSet f e ==> finite(A)";
-by (eresolve_tac [foldSet.induct] 1);
-by Auto_tac;
-qed "foldSet_imp_finite";
-
-Addsimps [foldSet_imp_finite];
-
-
-Goal "finite(A) ==> EX x. (A, x) : foldSet f e";
-by (etac finite_induct 1);
-by Auto_tac;
-qed "finite_imp_foldSet";
-
-
-Open_locale "LC"; 
-
-(*Strip meta-quantifiers: perhaps the locale should do this?*)
-val f_lcomm = forall_elim_vars 0 (thm "lcomm");
-
-
-Goal "ALL A x. card(A) < n --> (A, x) : foldSet f e --> \
-\            (ALL y. (A, y) : foldSet f e --> y=x)";
-by (induct_tac "n" 1);
-by (auto_tac (claset(), simpset() addsimps [less_Suc_eq]));
-by (etac foldSet.elim 1);
-by (Blast_tac 1);
-by (etac foldSet.elim 1);
-by (Blast_tac 1);
-by (Clarify_tac 1);
-(*force simplification of "card A < card (insert ...)"*)
-by (etac rev_mp 1);
-by (asm_simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
-by (rtac impI 1);
-(** LEVEL 10 **)
-by (rename_tac "Aa xa ya Ab xb yb" 1);
- by (case_tac "xa=xb" 1);
- by (subgoal_tac "Aa = Ab" 1);
- by (blast_tac (claset() addEs [equalityE]) 2);
- by (Blast_tac 1);
-(*case xa ~= xb*)
-by (subgoal_tac "Aa-{xb} = Ab-{xa} & xb : Aa & xa : Ab" 1);
- by (blast_tac (claset() addEs [equalityE]) 2);
-by (Clarify_tac 1);
-by (subgoal_tac "Aa = insert xb Ab - {xa}" 1);
- by (blast_tac (claset() addEs [equalityE]) 2);
-(** LEVEL 20 **)
-by (subgoal_tac "card Aa <= card Ab" 1);
- by (rtac (Suc_le_mono RS subst) 2);
- by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 2);
-by (res_inst_tac [("A1", "Aa-{xb}"), ("f1","f")] 
-    (finite_imp_foldSet RS exE) 1);
-by (blast_tac (claset() addIs [foldSet_imp_finite, finite_Diff]) 1);
-by (forward_tac [Diff_foldSet] 1 THEN assume_tac 1);
-by (subgoal_tac "ya = f xb x" 1);
- by (Blast_tac 2);
-by (subgoal_tac "(Ab - {xa}, x) : foldSet f e" 1);
- 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_lcomm]) 1);
-val lemma = result();
-
-
-Goal "[| (A, x) : foldSet f e;  (A, y) : foldSet f e |] ==> y=x";
-by (blast_tac (claset() addIs [normalize_thm [RSspec, RSmp] lemma]) 1);
-qed "foldSet_determ";
-
-Goalw [fold_def] "(A,y) : foldSet f e ==> fold f e A = y";
-by (blast_tac (claset() addIs [foldSet_determ]) 1);
-qed "fold_equality";
-
-Goalw [fold_def] "fold f e {} = e";
-by (Blast_tac 1);
-qed "fold_empty";
-Addsimps [fold_empty];
-
-Goal "x ~: A ==> \
-\     ((insert x A, v) : foldSet f e) =  \
-\     (EX y. (A, y) : foldSet f e & v = f x y)";
-by Auto_tac;
-by (res_inst_tac [("A1", "A"), ("f1","f")] (finite_imp_foldSet RS exE) 1);
-by (force_tac (claset() addDs [foldSet_imp_finite], simpset()) 1);
-by (blast_tac (claset() addIs [foldSet_determ]) 1);
-val lemma = result();
-
-
-Goalw [fold_def]
-     "[| finite A; x ~: A |] ==> fold f e (insert x A) = f x (fold f e A)";
-by (asm_simp_tac (simpset() addsimps [lemma]) 1);
-by (rtac select_equality 1);
-by (auto_tac (claset() addIs [finite_imp_foldSet],
-	      simpset() addcongs [conj_cong]
-		        addsimps [symmetric fold_def,
-				  fold_equality]));
-qed "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 (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::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 9ea709aa275c -r 497eeeace3fc src/HOL/Induct/FoldSet.thy
--- a/src/HOL/Induct/FoldSet.thy	Mon Oct 05 10:33:34 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-(*  Title:      HOL/FoldSet
-    ID:         $Id$
-    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 at least left-commutative.
-*)
-
-FoldSet = Finite +
-
-consts foldSet :: "[['b,'a] => 'a, 'a] => ('b set * 'a) set"
-
-inductive "foldSet f e"
-  intrs
-    emptyI   "({}, e) : foldSet f e"
-
-    insertI  "[| x ~: A;  (A,y) : foldSet f e |]
-	      ==> (insert x A, f x y) : foldSet f e"
-
-constdefs
-   fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a"
-  "fold f e A == @x. (A,x) : foldSet f e"
-  (* 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
-  assumes
-    ident    "!! x. f x e = x"
-    commute  "!! x y. f x y = f y x"
-    assoc    "!! x y z. f (f x y) z = f x (f y z)"
-  defines
-    (*nothing*)
-
-end
diff -r 9ea709aa275c -r 497eeeace3fc src/HOL/Induct/ROOT.ML
--- a/src/HOL/Induct/ROOT.ML	Mon Oct 05 10:33:34 1998 +0200
+++ b/src/HOL/Induct/ROOT.ML	Tue Oct 06 14:39:53 1998 +0200
@@ -11,7 +11,6 @@
 writeln"Root file for HOL/Induct";
 set proof_timing;
 time_use_thy "Perm";
-time_use_thy "FoldSet";
 time_use_thy "Comb";
 time_use_thy "Mutil";
 time_use_thy "Acc";
diff -r 9ea709aa275c -r 497eeeace3fc src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Oct 05 10:33:34 1998 +0200
+++ b/src/HOL/IsaMakefile	Tue Oct 06 14:39:53 1998 +0200
@@ -79,8 +79,7 @@
 
 $(LOG)/HOL-Induct.gz: $(OUT)/HOL Induct/Acc.ML Induct/Acc.thy \
   Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \
-  Induct/Exp.ML Induct/Exp.thy Induct/FoldSet.ML Induct/FoldSet.thy \
-  Induct/LFilter.ML Induct/LFilter.thy \
+  Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \
   Induct/LList.ML Induct/LList.thy Induct/Mutil.ML Induct/Mutil.thy \
   Induct/Perm.ML Induct/Perm.thy Induct/PropLog.ML Induct/PropLog.thy \
   Induct/ROOT.ML Induct/SList.ML Induct/SList.thy Induct/Simult.ML \