# HG changeset patch
# User paulson
# Date 884254905 -3600
# Node ID c7f56322a84bf4e3ccabe54ff9f2d4ed02fc4299
# Parent  d430a1b349282d855455d95c84ff3f0aa737eaf9
Tidied by adding more default simprules

diff -r d430a1b34928 -r c7f56322a84b src/HOL/Induct/LFilter.ML
--- a/src/HOL/Induct/LFilter.ML	Wed Jan 07 13:55:54 1998 +0100
+++ b/src/HOL/Induct/LFilter.ML	Thu Jan 08 11:21:45 1998 +0100
@@ -71,32 +71,34 @@
 goalw thy [find_def] "find p LNil = LNil";
 by (blast_tac (claset() addIs [select_equality]) 1);
 qed "find_LNil";
+Addsimps [find_LNil];
 
 goalw thy [find_def] "!!p. (l,l') : findRel p ==> find p l = l'";
 by (blast_tac (claset() addIs [select_equality] addDs [findRel_functional]) 1);
 qed "findRel_imp_find";
+Addsimps [findRel_imp_find];
 
 goal thy "!!p. p x ==> find p (LCons x l) = LCons x l";
 by (blast_tac (claset() addIs (findRel_imp_find::findRel.intrs)) 1);
 qed "find_LCons_found";
+Addsimps [find_LCons_found];
 
 goalw thy [find_def] "!!p. l ~: Domain(findRel p) ==> find p l = LNil";
 by (blast_tac (claset() addIs [select_equality]) 1);
 qed "diverge_find_LNil";
-
 Addsimps [diverge_find_LNil];
 
 goal thy "!!p. ~ (p x) ==> find p (LCons x l) = find p l";
 by (case_tac "LCons x l : Domain(findRel p)" 1);
 by (Asm_full_simp_tac 2);
 by (Clarify_tac 1);
-by (asm_simp_tac (simpset() addsimps [findRel_imp_find]) 1);
+by (Asm_simp_tac 1);
 by (blast_tac (claset() addIs (findRel_imp_find::findRel.intrs)) 1);
 qed "find_LCons_seek";
+Addsimps [find_LCons_seek];
 
 goal thy "find p (LCons x l) = (if p x then LCons x l else find p l)";
-by (asm_simp_tac (simpset() addsimps [find_LCons_found, find_LCons_seek]
-                           addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
 qed "find_LCons";
 
 
@@ -105,54 +107,60 @@
 
 goal thy "lfilter p LNil = LNil";
 by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
-by (simp_tac (simpset() addsimps [find_LNil]) 1);
+by (Simp_tac 1);
 qed "lfilter_LNil";
+Addsimps [lfilter_LNil];
 
 goal thy "!!p. l ~: Domain(findRel p) ==> lfilter p l = LNil";
 by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
 by (Asm_simp_tac 1);
 qed "diverge_lfilter_LNil";
 
+Addsimps [diverge_lfilter_LNil];
+
 
 goal thy "!!p. p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)";
 by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
-by (asm_simp_tac (simpset() addsimps [find_LCons_found]) 1);
+by (Asm_simp_tac 1);
 qed "lfilter_LCons_found";
+(*This rewrite and lfilter_LCons_seek are NOT added because lfilter_LCons
+  subsumes both*)
 
 
 goal thy "!!p. (l, LCons x l') : findRel p \
 \              ==> lfilter p l = LCons x (lfilter p l')";
 by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
-by (asm_simp_tac (simpset() addsimps [findRel_imp_find]) 1);
+by (Asm_simp_tac 1);
 qed "findRel_imp_lfilter";
 
+Addsimps [findRel_imp_lfilter];
+
+
 goal thy "!!p. ~ (p x) ==> lfilter p (LCons x l) = lfilter p l";
 by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
 by (case_tac "LCons x l : Domain(findRel p)" 1);
-by (asm_full_simp_tac (simpset() addsimps [diverge_lfilter_LNil]) 2);
+by (Asm_full_simp_tac 2);
 by (etac Domain_findRelE 1);
 by (safe_tac (claset() delrules [conjI]));
-by (asm_full_simp_tac 
-    (simpset() addsimps [findRel_imp_lfilter, findRel_imp_find,
-                        find_LCons_seek]) 1);
+by (Asm_full_simp_tac 1);
 qed "lfilter_LCons_seek";
 
 
 goal thy "lfilter p (LCons x l) = \
 \         (if p x then LCons x (lfilter p l) else lfilter p l)";
 by (asm_simp_tac (simpset() addsimps [lfilter_LCons_found, lfilter_LCons_seek]
-                           addsplits [expand_if]) 1);
+                            addsplits [expand_if]) 1);
 qed "lfilter_LCons";
 
 AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
-Addsimps [lfilter_LNil, lfilter_LCons];
+Addsimps [lfilter_LCons];
 
 
 goal thy "!!p. lfilter p l = LNil ==> l ~: Domain(findRel p)";
 by (rtac notI 1);
 by (etac Domain_findRelE 1);
 by (etac rev_mp 1);
-by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter]) 1);
+by (Asm_simp_tac 1);
 qed "lfilter_eq_LNil";
 
 
@@ -162,7 +170,7 @@
 by (case_tac "l : Domain(findRel p)" 1);
 by (etac Domain_findRelE 1);
 by (Asm_simp_tac 2);
-by (asm_simp_tac (simpset() addsimps [findRel_imp_find]) 1);
+by (Asm_simp_tac 1);
 by (Blast_tac 1);
 qed_spec_mp "lfilter_eq_LCons";
 
@@ -170,9 +178,9 @@
 goal thy "lfilter p l = LNil  |  \
 \         (EX y l'. lfilter p l = LCons y (lfilter p l') & p y)";
 by (case_tac "l : Domain(findRel p)" 1);
-by (asm_simp_tac (simpset() addsimps [diverge_lfilter_LNil]) 2);
+by (Asm_simp_tac 2);
 by (blast_tac (claset() addSEs [Domain_findRelE] 
-                       addIs [findRel_imp_lfilter]) 1);
+                        addIs  [findRel_imp_lfilter]) 1);
 qed "lfilter_cases";
 
 
@@ -228,7 +236,7 @@
 \                  --> l : Domain (findRel(%x. p x & q x))";
 by (etac findRel.induct 1);
 by (blast_tac (claset() addSDs [sym RS lfilter_eq_LCons]
-                       addIs  [findRel_conj]) 1);
+                        addIs  [findRel_conj]) 1);
 by Auto_tac;
 by (dtac (sym RS lfilter_eq_LCons) 1);
 by Auto_tac;
@@ -256,14 +264,13 @@
 by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
 by (blast_tac (claset() addIs [impOfSubs Domain_findRel_mono]) 3);
 (*There are no qs in l: both lists are LNil*)
-by (asm_simp_tac (simpset() addsimps [diverge_lfilter_LNil]) 2);
+by (Asm_simp_tac 2);
 by (etac Domain_findRelE 1);
 (*case q x*)
 by (case_tac "p x" 1);
-by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter,
-                                     findRel_conj RS findRel_imp_lfilter]) 1);
+by (asm_simp_tac (simpset() addsimps [findRel_conj RS findRel_imp_lfilter]) 1);
 (*case q x and ~(p x) *)
-by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter]) 1);
+by (Asm_simp_tac 1);
 by (case_tac "l' : Domain (findRel (%x. p x & q x))" 1);
 (*subcase: there is no p&q in l' and therefore none in l*)
 by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
@@ -271,14 +278,14 @@
 by (subgoal_tac "lfilter q l' ~: Domain(findRel p)" 2);
 by (blast_tac (claset() addIs [findRel_lfilter_Domain_conj]) 3);
 (*    ...and therefore too, no p in lfilter q l'.  Both results are Lnil*)
-by (asm_simp_tac (simpset() addsimps [diverge_lfilter_LNil]) 2);
+by (Asm_simp_tac 2);
 (*subcase: there is a p&q in l' and therefore also one in l*)
 by (etac Domain_findRelE 1);
 by (subgoal_tac "(l, LCons xa l'a) : findRel(%x. p x & q x)" 1);
 by (blast_tac (claset() addIs [findRel_conj2]) 2);
 by (subgoal_tac "(lfilter q l', LCons xa (lfilter q l'a)) : findRel p" 1);
 by (blast_tac (claset() addIs [findRel_conj_lfilter]) 2);
-by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter]) 1);
+by (Asm_simp_tac 1);
 val lemma = result();
 
 
@@ -327,9 +334,9 @@
 by (case_tac "lmap f l : Domain (findRel p)" 1);
 by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2);
 by (blast_tac (claset() addIs [findRel_lmap_Domain]) 3);
-by (asm_simp_tac (simpset() addsimps [diverge_lfilter_LNil]) 2);
+by (Asm_simp_tac 2);
 by (etac Domain_findRelE 1);
 by (forward_tac [lmap_LCons_findRel] 1);
 by (Clarify_tac 1);
-by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter]) 1);
+by (Asm_simp_tac 1);
 qed "lfilter_lmap";
diff -r d430a1b34928 -r c7f56322a84b src/HOL/Induct/LList.ML
--- a/src/HOL/Induct/LList.ML	Wed Jan 07 13:55:54 1998 +0100
+++ b/src/HOL/Induct/LList.ML	Thu Jan 08 11:21:45 1998 +0100
@@ -14,11 +14,6 @@
 
 simpset_ref() := simpset() addsplits [expand_split, expand_sum_case];
 
-(*For adding _eqI rules to a simpset; we must remove Pair_eq because
-  it may turn an instance of reflexivity into a conjunction!*)
-fun add_eqI ss = ss addsimps [range_eqI, image_eqI] 
-                    delsimps [Pair_eq];
-
 
 (*This justifies using llist in other recursive type definitions*)
 goalw LList.thy llist.defs "!!A B. A<=B ==> llist(A) <= llist(B)";
@@ -49,11 +44,14 @@
 goalw LList.thy [list_Fun_def, NIL_def] "NIL: list_Fun A X";
 by (Fast_tac 1);
 qed "list_Fun_NIL_I";
+AddIffs [list_Fun_NIL_I];
 
 goalw LList.thy [list_Fun_def,CONS_def]
     "!!M N. [| M: A;  N: X |] ==> CONS M N : list_Fun A X";
 by (Fast_tac 1);
 qed "list_Fun_CONS_I";
+Addsimps [list_Fun_CONS_I];
+AddSIs   [list_Fun_CONS_I];
 
 (*Utilise the "strong" part, i.e. gfp(f)*)
 goalw LList.thy (llist.defs @ [list_Fun_def])
@@ -130,8 +128,7 @@
 by (rtac rangeI 1);
 by Safe_tac;
 by (stac LList_corec 1);
-by (simp_tac (simpset() addsimps [list_Fun_NIL_I, list_Fun_CONS_I, CollectI]
-                       |> add_eqI) 1);
+by (Simp_tac 1);
 qed "LList_corec_type";
 
 (*Lemma for the proof of llist_corec*)
@@ -142,8 +139,7 @@
 by (rtac rangeI 1);
 by Safe_tac;
 by (stac LList_corec 1);
-by (asm_simp_tac (simpset() addsimps [list_Fun_NIL_I]) 1);
-by (fast_tac (claset() addSIs [list_Fun_CONS_I]) 1);
+by (Asm_simp_tac 1);
 qed "LList_corec_type2";
 
 
@@ -163,11 +159,11 @@
 by (etac LListD.elim 1);
 by (safe_tac (claset_of Prod.thy delrules [equalityI] addSEs [diagE]));
 by (res_inst_tac [("n", "n")] natE 1);
-by (asm_simp_tac (simpset() addsimps [ntrunc_0]) 1);
+by (Asm_simp_tac 1);
 by (rename_tac "n'" 1);
 by (res_inst_tac [("n", "n'")] natE 1);
-by (asm_simp_tac (simpset() addsimps [CONS_def, ntrunc_one_In1]) 1);
-by (asm_simp_tac (simpset() addsimps [CONS_def, ntrunc_In1, ntrunc_Scons, less_Suc_eq]) 1);
+by (asm_simp_tac (simpset() addsimps [CONS_def]) 1);
+by (asm_simp_tac (simpset() addsimps [CONS_def, less_Suc_eq]) 1);
 qed "LListD_implies_ntrunc_equality";
 
 (*The domain of the LListD relation*)
@@ -234,7 +230,7 @@
 by (eresolve_tac [llist.elim] 1);
 by (ALLGOALS
     (asm_simp_tac (simpset() addsimps [diagI, LListD_Fun_NIL_I,
-                                      LListD_Fun_CONS_I])));
+				       LListD_Fun_CONS_I])));
 qed "diag_subset_LListD";
 
 goal LList.thy "LListD(diag(A)) = diag(llist(A))";
@@ -265,6 +261,12 @@
 
 (*** Finality of llist(A): Uniqueness of functions defined by corecursion ***)
 
+(*We must remove Pair_eq because it may turn an instance of reflexivity
+  (h1 b, h2 b) = (h1 ?x17, h2 ?x17) into a conjunction! 
+  (or strengthen the Solver?) 
+*)
+Delsimps [Pair_eq];
+
 (*abstract proof using a bisimulation*)
 val [prem1,prem2] = goal LList.thy
  "[| !!x. h1(x) = sum_case (%u. NIL) (split(%z w. CONS z (h1 w))) (f x);  \
@@ -279,8 +281,7 @@
 by (stac prem1 1);
 by (stac prem2 1);
 by (simp_tac (simpset() addsimps [LListD_Fun_NIL_I,
-                                 CollectI RS LListD_Fun_CONS_I]
-                       |> add_eqI) 1);
+				  CollectI RS LListD_Fun_CONS_I]) 1);
 qed "LList_corec_unique";
 
 val [prem] = goal LList.thy
@@ -298,9 +299,12 @@
 
 goalw LList.thy [CONS_def]
     "ntrunc (Suc(Suc(k))) (CONS M N) = CONS (ntrunc k M) (ntrunc k N)";
-by (simp_tac (simpset() addsimps [ntrunc_Scons,ntrunc_In1]) 1);
+by (Simp_tac 1);
 qed "ntrunc_CONS";
 
+Addsimps [ntrunc_one_CONS, ntrunc_CONS];
+
+
 val [prem1,prem2] = goal LList.thy
  "[| !!x. h1(x) = sum_case (%u. NIL) (split(%z w. CONS z (h1 w))) (f x);  \
 \    !!x. h2(x) = sum_case (%u. NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
@@ -319,8 +323,7 @@
 by (res_inst_tac [("n", "n")] natE 1);
 by (rename_tac "m" 2);
 by (res_inst_tac [("n", "m")] natE 2);
-by (ALLGOALS(asm_simp_tac(simpset() addsimps
-            [ntrunc_0,ntrunc_one_CONS,ntrunc_CONS, less_Suc_eq])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
 result();
 
 
@@ -436,9 +439,7 @@
 \ |] ==> f(M) = g(M)";
 by (rtac LList_equalityI 1);
 by (rtac (Mlist RS imageI) 1);
-by (rtac subsetI 1);
-by (etac imageE 1);
-by (etac ssubst 1);
+by (rtac image_subsetI 1);
 by (etac llist.elim 1);
 by (etac ssubst 1);
 by (stac NILcase 1);
@@ -460,13 +461,15 @@
 by (Simp_tac 1);
 qed "Lmap_CONS";
 
+Addsimps [Lmap_NIL, Lmap_CONS];
+
 (*Another type-checking proof by coinduction*)
 val [major,minor] = goal LList.thy
     "[| M: llist(A);  !!x. x:A ==> f(x):B |] ==> Lmap f M: llist(B)";
 by (rtac (major RS imageI RS llist_coinduct) 1);
 by Safe_tac;
 by (etac llist.elim 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [Lmap_NIL,Lmap_CONS])));
+by (ALLGOALS Asm_simp_tac);
 by (REPEAT (ares_tac [list_Fun_NIL_I, list_Fun_CONS_I, 
                       minor, imageI, UnI1] 1));
 qed "Lmap_type";
@@ -484,7 +487,7 @@
 by (rtac (prem RS imageI RS LList_equalityI) 1);
 by Safe_tac;
 by (etac llist.elim 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [Lmap_NIL,Lmap_CONS])));
+by (ALLGOALS Asm_simp_tac);
 by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI, UnI1,
                       rangeI RS LListD_Fun_CONS_I] 1));
 qed "Lmap_compose";
@@ -493,7 +496,7 @@
 by (rtac (prem RS imageI RS LList_equalityI) 1);
 by Safe_tac;
 by (etac llist.elim 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [Lmap_NIL,Lmap_CONS])));
+by (ALLGOALS Asm_simp_tac);
 by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI RS UnI1,
                       rangeI RS LListD_Fun_CONS_I] 1));
 qed "Lmap_ident";
@@ -520,7 +523,7 @@
 
 Addsimps [llist.NIL_I, Lappend_NIL_NIL, Lappend_NIL_CONS,
           Lappend_CONS, LListD_Fun_CONS_I, range_eqI, image_eqI];
-Delsimps [Pair_eq];
+
 
 goal LList.thy "!!M. M: llist(A) ==> Lappend NIL M = M";
 by (etac LList_fun_equalityI 1);
@@ -532,6 +535,9 @@
 by (ALLGOALS Asm_simp_tac);
 qed "Lappend_NIL2";
 
+Addsimps [Lappend_NIL, Lappend_NIL2];
+
+
 (** Alternative type-checking proofs for Lappend **)
 
 (*weak co-induction: bisimulation and case analysis on both variables*)
@@ -543,9 +549,8 @@
 by Safe_tac;
 by (eres_inst_tac [("a", "u")] llist.elim 1);
 by (eres_inst_tac [("a", "v")] llist.elim 1);
-by (ALLGOALS
-    (Asm_simp_tac THEN'
-     fast_tac (claset() addSIs [llist.NIL_I, list_Fun_NIL_I, list_Fun_CONS_I])));
+by (ALLGOALS Asm_simp_tac);
+by (Blast_tac 1);
 qed "Lappend_type";
 
 (*strong co-induction: bisimulation and case analysis on one variable*)
@@ -553,12 +558,10 @@
     "!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
 by (res_inst_tac [("X", "(%u. Lappend u N)``llist(A)")] llist_coinduct 1);
 by (etac imageI 1);
-by (rtac subsetI 1);
-by (etac imageE 1);
-by (eres_inst_tac [("a", "u")] llist.elim 1);
-by (asm_simp_tac (simpset() addsimps [Lappend_NIL, list_Fun_llist_I]) 1);
+by (rtac image_subsetI 1);
+by (eres_inst_tac [("a", "x")] llist.elim 1);
+by (asm_simp_tac (simpset() addsimps [list_Fun_llist_I]) 1);
 by (Asm_simp_tac 1);
-by (fast_tac (claset() addSIs [list_Fun_CONS_I]) 1);
 qed "Lappend_type";
 
 (**** Lazy lists as the type 'a llist -- strongly typed versions of above ****)
@@ -587,7 +590,8 @@
 by (assume_tac 1);
 by (etac rangeE 1);
 by (rtac (inj_Rep_llist RS injD RS prem2) 1);
-by (asm_simp_tac (simpset() delsimps [CONS_CONS_eq] addsimps [Rep_llist_LCons]) 1);
+by (asm_simp_tac (simpset() delsimps [CONS_CONS_eq] 
+		            addsimps [Rep_llist_LCons]) 1);
 by (etac (Abs_llist_inverse RS ssubst) 1);
 by (rtac refl 1);
 qed "llistE";
@@ -629,7 +633,8 @@
 goal LList.thy
     "prod_fun Rep_llist Rep_llist `` r <= \
 \    (llist(range Leaf)) Times (llist(range Leaf))";
-by (fast_tac (claset() addIs [Rep_llist]) 1);
+by (fast_tac (claset() delrules [image_subsetI]
+		       addIs [Rep_llist]) 1);
 qed "subset_Sigma_llist";
 
 val [prem] = goal LList.thy
@@ -638,7 +643,7 @@
 by Safe_tac;
 by (rtac (prem RS subsetD RS SigmaE2) 1);
 by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [o_def,prod_fun,Abs_llist_inverse]) 1);
+by (asm_simp_tac (simpset() addsimps [Abs_llist_inverse]) 1);
 qed "prod_fun_lemma";
 
 goal LList.thy
diff -r d430a1b34928 -r c7f56322a84b src/HOL/Induct/SList.ML
--- a/src/HOL/Induct/SList.ML	Wed Jan 07 13:55:54 1998 +0100
+++ b/src/HOL/Induct/SList.ML	Thu Jan 08 11:21:45 1998 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/ex/SList.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
+    Copyright   1998  University of Cambridge
 
 Definition of type 'a list by a least fixed point
 *)
@@ -138,9 +138,12 @@
 qed "List_case_NIL";
 
 goalw SList.thy [List_case_def,CONS_def]  "List_case c h (CONS M N) = h M N";
-by (simp_tac (simpset() addsimps [Split,Case_In1]) 1);
+by (Simp_tac 1);
 qed "List_case_CONS";
 
+Addsimps [List_case_NIL, List_case_CONS];
+
+
 (*** List_rec -- by wf recursion on pred_sexp ***)
 
 (* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not
@@ -185,23 +188,25 @@
 
 goal SList.thy "List_rec NIL c h = c";
 by (rtac (List_rec_unfold RS trans) 1);
-by (simp_tac (simpset() addsimps [List_case_NIL]) 1);
+by (Simp_tac 1);
 qed "List_rec_NIL";
 
 goal SList.thy "!!M. [| M: sexp;  N: sexp |] ==> \
 \    List_rec (CONS M N) c h = h M N (List_rec N c h)";
 by (rtac (List_rec_unfold RS trans) 1);
-by (asm_simp_tac (simpset() addsimps [List_case_CONS, pred_sexp_CONS_I2]) 1);
+by (asm_simp_tac (simpset() addsimps [pred_sexp_CONS_I2]) 1);
 qed "List_rec_CONS";
 
+Addsimps [List_rec_NIL, List_rec_CONS];
+
+
 (*** list_rec -- by List_rec ***)
 
 val Rep_list_in_sexp =
     [range_Leaf_subset_sexp RS list_subset_sexp, Rep_list] MRS subsetD;
 
 local
-  val list_rec_simps = [List_rec_NIL, List_rec_CONS, 
-                        Abs_list_inverse, Rep_list_inverse,
+  val list_rec_simps = [Abs_list_inverse, Rep_list_inverse,
                         Rep_list, rangeI, inj_Leaf, inv_f_f,
                         sexp.LeafI, Rep_list_in_sexp]
 in
@@ -364,8 +369,8 @@
 goal SList.thy "!!f. (!!x. f(x): sexp) ==> \
 \       Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs";
 by (list_ind_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac(simpset() addsimps
-       [Rep_map_type,list_sexp RS subsetD])));
+by (ALLGOALS (asm_simp_tac(simpset() addsimps
+			   [Rep_map_type, list_sexp RS subsetD])));
 qed "Abs_Rep_map";
 
 Addsimps [append_Nil4, map_ident2];
diff -r d430a1b34928 -r c7f56322a84b src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Wed Jan 07 13:55:54 1998 +0100
+++ b/src/HOL/Prod.ML	Thu Jan 08 11:21:45 1998 +0100
@@ -241,19 +241,21 @@
 goalw Prod.thy [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";
 by (rtac split 1);
 qed "prod_fun";
+Addsimps [prod_fun];
 
 goal Prod.thy 
     "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
 by (rtac ext 1);
 by (res_inst_tac [("p","x")] PairE 1);
-by (asm_simp_tac (simpset() addsimps [prod_fun,o_def]) 1);
+by (Asm_simp_tac 1);
 qed "prod_fun_compose";
 
 goal Prod.thy "prod_fun (%x. x) (%y. y) = (%z. z)";
 by (rtac ext 1);
 by (res_inst_tac [("p","z")] PairE 1);
-by (asm_simp_tac (simpset() addsimps [prod_fun]) 1);
+by (Asm_simp_tac 1);
 qed "prod_fun_ident";
+Addsimps [prod_fun_ident];
 
 val prems = goal Prod.thy "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
 by (rtac image_eqI 1);
@@ -271,6 +273,7 @@
 by (blast_tac (claset() addIs [prod_fun]) 1);
 qed "prod_fun_imageE";
 
+
 (*** Disjoint union of a family of sets - Sigma ***)
 
 qed_goalw "SigmaI" Prod.thy [Sigma_def]
diff -r d430a1b34928 -r c7f56322a84b src/HOL/Sexp.ML
--- a/src/HOL/Sexp.ML	Wed Jan 07 13:55:54 1998 +0100
+++ b/src/HOL/Sexp.ML	Thu Jan 08 11:21:45 1998 +0100
@@ -22,6 +22,8 @@
 by (blast_tac (claset() addSIs [select_equality]) 1);
 qed "sexp_case_Scons";
 
+Addsimps [sexp_case_Leaf, sexp_case_Numb, sexp_case_Scons];
+
 
 (** Introduction rules for sexp constructors **)
 
@@ -100,6 +102,13 @@
    "(%M. sexp_rec M c d e) = wfrec pred_sexp \
                        \ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))";
 by (simp_tac (HOL_ss addsimps [sexp_rec_def]) 1);
+
+(* sexp_rec a c d e =
+   sexp_case c d
+    (%N1 N2.
+        e N1 N2 (cut (%M. sexp_rec M c d e) pred_sexp a N1)
+         (cut (%M. sexp_rec M c d e) pred_sexp a N2)) a
+*)
 bind_thm("sexp_rec_unfold", 
 	 [result() RS eq_reflection, wf_pred_sexp] MRS def_wfrec);
 
@@ -118,6 +127,5 @@
 goal Sexp.thy "!!M. [| M: sexp;  N: sexp |] ==> \
 \    sexp_rec (M$N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
 by (rtac (sexp_rec_unfold RS trans) 1);
-by (asm_simp_tac (simpset() addsimps [sexp_case_Scons,pred_sexpI1,pred_sexpI2])
-    1);
+by (asm_simp_tac (simpset() addsimps [pred_sexpI1, pred_sexpI2]) 1);
 qed "sexp_rec_Scons";
diff -r d430a1b34928 -r c7f56322a84b src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Wed Jan 07 13:55:54 1998 +0100
+++ b/src/HOL/Univ.ML	Thu Jan 08 11:21:45 1998 +0100
@@ -265,30 +265,35 @@
             assume_tac 1));
 qed "ntrunc_Scons";
 
+Addsimps [ntrunc_0, ntrunc_Atom, ntrunc_Leaf, ntrunc_Numb, ntrunc_Scons];
+
+
 (** Injection nodes **)
 
 goalw Univ.thy [In0_def] "ntrunc (Suc 0) (In0 M) = {}";
-by (simp_tac (simpset() addsimps [ntrunc_Scons,ntrunc_0]) 1);
+by (Simp_tac 1);
 by (rewtac Scons_def);
 by (Blast_tac 1);
 qed "ntrunc_one_In0";
 
 goalw Univ.thy [In0_def]
     "ntrunc (Suc (Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)";
-by (simp_tac (simpset() addsimps [ntrunc_Scons,ntrunc_Numb]) 1);
+by (Simp_tac 1);
 qed "ntrunc_In0";
 
 goalw Univ.thy [In1_def] "ntrunc (Suc 0) (In1 M) = {}";
-by (simp_tac (simpset() addsimps [ntrunc_Scons,ntrunc_0]) 1);
+by (Simp_tac 1);
 by (rewtac Scons_def);
 by (Blast_tac 1);
 qed "ntrunc_one_In1";
 
 goalw Univ.thy [In1_def]
     "ntrunc (Suc (Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)";
-by (simp_tac (simpset() addsimps [ntrunc_Scons,ntrunc_Numb]) 1);
+by (Simp_tac 1);
 qed "ntrunc_In1";
 
+Addsimps [ntrunc_one_In0, ntrunc_In0, ntrunc_one_In1, ntrunc_In1];
+
 
 (*** Cartesian Product ***)
 
@@ -383,7 +388,7 @@
 val [major] = goalw Univ.thy [ntrunc_def]
     "(!!k. ntrunc k M <= N) ==> M<=N";
 by (blast_tac (claset() addIs [less_add_Suc1, less_add_Suc2, 
-                            major RS subsetD]) 1);
+			       major RS subsetD]) 1);
 qed "ntrunc_subsetD";
 
 (*A generalized form of the take-lemma*)
@@ -438,6 +443,9 @@
 by (blast_tac (claset() addIs [select_equality]) 1);
 qed "Case_In1";
 
+Addsimps [Split, Case_In0, Case_In1];
+
+
 (**** UN x. B(x) rules ****)
 
 goalw Univ.thy [ntrunc_def] "ntrunc k (UN x. f(x)) = (UN x. ntrunc k (f x))";
@@ -562,15 +570,15 @@
 (*** Domain ***)
 
 goal Univ.thy "fst `` diag(A) = A";
-by (Blast_tac 1);
+by Auto_tac;
 qed "fst_image_diag";
 
 goal Univ.thy "fst `` (r<**>s) = (fst``r) <*> (fst``s)";
-by (Blast_tac 1);
+by Auto_tac;
 qed "fst_image_dprod";
 
 goal Univ.thy "fst `` (r<++>s) = (fst``r) <+> (fst``s)";
-by (Blast_tac 1);
+by Auto_tac;
 qed "fst_image_dsum";
 
 Addsimps [fst_image_diag, fst_image_dprod, fst_image_dsum];