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