new theory Induct/FoldSet

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/FoldSet.ML	Tue Sep 01 15:04:59 1998 +0200
@@ -0,0 +1,153 @@
+(*  Title:      HOL/FoldSet
+    ID:         $Id$
+    Author:     Lawrence C Paulson
+    Copyright   1998  University of Cambridge
+
+A "fold" functional for finite sets
+*)
+
+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 "ACI"; 
+
+(*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];
+
+
+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 [le_eq_less_Suc RS sym]) 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_ac) 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";
+Addsimps [fold_insert];
+
+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);
+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);
+qed "fold_Un_disjoint";
+
+
+Close_locale();
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/FoldSet.thy	Tue Sep 01 15:04:59 1998 +0200
@@ -0,0 +1,37 @@
+(*  Title:      HOL/FoldSet
+    ID:         $Id$
+    Author:     Lawrence C Paulson
+    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.
+*)
+
+FoldSet = Finite +
+
+consts foldSet :: "[['a,'a] => 'a, 'a] => ('a 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 :: "[['a,'a] => 'a, 'a, 'a set] => 'a"
+  "fold f e A == @x. (A,x) : foldSet f e"
+  
+locale ACI =
+  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
+
+

--- a/src/HOL/Induct/README.html	Tue Sep 01 15:04:28 1998 +0200
+++ b/src/HOL/Induct/README.html	Tue Sep 01 15:04:59 1998 +0200
@@ -10,6 +10,13 @@
 <UL>
 <LI><KBD>Perm</KBD> is a simple theory of permutations of lists.
 
+<LI><KBD>FoldSet</KBD> declares a <EM>fold</EM> functional for finite sets.
+Let f be an associative-commutative function with identity e.
+For n non-negative we have
+<PRE>
+fold f e {x1,...,xn} = f x1 (... (f xn e))
+</PRE>
+
 <LI><KBD>Comb</KBD> proves the Church-Rosser theorem for combinators (<A
 HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz">paper
 available</A>).

--- a/src/HOL/Induct/ROOT.ML	Tue Sep 01 15:04:28 1998 +0200
+++ b/src/HOL/Induct/ROOT.ML	Tue Sep 01 15:04:59 1998 +0200
@@ -11,6 +11,7 @@
 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";

--- a/src/HOL/IsaMakefile	Tue Sep 01 15:04:28 1998 +0200
+++ b/src/HOL/IsaMakefile	Tue Sep 01 15:04:59 1998 +0200
@@ -76,7 +76,8 @@
 
 $(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/LFilter.ML Induct/LFilter.thy \
+  Induct/Exp.ML Induct/Exp.thy Induct/FoldSet.ML Induct/FoldSet.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 \