Tidied by adding more default simprules
authorpaulson
Thu Jan 08 11:21:45 1998 +0100 (1998-01-08)
changeset 4521c7f56322a84b
parent 4520 d430a1b34928
child 4522 0218c486cf07
Tidied by adding more default simprules
src/HOL/Induct/LFilter.ML
src/HOL/Induct/LList.ML
src/HOL/Induct/SList.ML
src/HOL/Prod.ML
src/HOL/Sexp.ML
src/HOL/Univ.ML
     1.1 --- a/src/HOL/Induct/LFilter.ML	Wed Jan 07 13:55:54 1998 +0100
     1.2 +++ b/src/HOL/Induct/LFilter.ML	Thu Jan 08 11:21:45 1998 +0100
     1.3 @@ -71,32 +71,34 @@
     1.4  goalw thy [find_def] "find p LNil = LNil";
     1.5  by (blast_tac (claset() addIs [select_equality]) 1);
     1.6  qed "find_LNil";
     1.7 +Addsimps [find_LNil];
     1.8  
     1.9  goalw thy [find_def] "!!p. (l,l') : findRel p ==> find p l = l'";
    1.10  by (blast_tac (claset() addIs [select_equality] addDs [findRel_functional]) 1);
    1.11  qed "findRel_imp_find";
    1.12 +Addsimps [findRel_imp_find];
    1.13  
    1.14  goal thy "!!p. p x ==> find p (LCons x l) = LCons x l";
    1.15  by (blast_tac (claset() addIs (findRel_imp_find::findRel.intrs)) 1);
    1.16  qed "find_LCons_found";
    1.17 +Addsimps [find_LCons_found];
    1.18  
    1.19  goalw thy [find_def] "!!p. l ~: Domain(findRel p) ==> find p l = LNil";
    1.20  by (blast_tac (claset() addIs [select_equality]) 1);
    1.21  qed "diverge_find_LNil";
    1.22 -
    1.23  Addsimps [diverge_find_LNil];
    1.24  
    1.25  goal thy "!!p. ~ (p x) ==> find p (LCons x l) = find p l";
    1.26  by (case_tac "LCons x l : Domain(findRel p)" 1);
    1.27  by (Asm_full_simp_tac 2);
    1.28  by (Clarify_tac 1);
    1.29 -by (asm_simp_tac (simpset() addsimps [findRel_imp_find]) 1);
    1.30 +by (Asm_simp_tac 1);
    1.31  by (blast_tac (claset() addIs (findRel_imp_find::findRel.intrs)) 1);
    1.32  qed "find_LCons_seek";
    1.33 +Addsimps [find_LCons_seek];
    1.34  
    1.35  goal thy "find p (LCons x l) = (if p x then LCons x l else find p l)";
    1.36 -by (asm_simp_tac (simpset() addsimps [find_LCons_found, find_LCons_seek]
    1.37 -                           addsplits [expand_if]) 1);
    1.38 +by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
    1.39  qed "find_LCons";
    1.40  
    1.41  
    1.42 @@ -105,54 +107,60 @@
    1.43  
    1.44  goal thy "lfilter p LNil = LNil";
    1.45  by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
    1.46 -by (simp_tac (simpset() addsimps [find_LNil]) 1);
    1.47 +by (Simp_tac 1);
    1.48  qed "lfilter_LNil";
    1.49 +Addsimps [lfilter_LNil];
    1.50  
    1.51  goal thy "!!p. l ~: Domain(findRel p) ==> lfilter p l = LNil";
    1.52  by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
    1.53  by (Asm_simp_tac 1);
    1.54  qed "diverge_lfilter_LNil";
    1.55  
    1.56 +Addsimps [diverge_lfilter_LNil];
    1.57 +
    1.58  
    1.59  goal thy "!!p. p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)";
    1.60  by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
    1.61 -by (asm_simp_tac (simpset() addsimps [find_LCons_found]) 1);
    1.62 +by (Asm_simp_tac 1);
    1.63  qed "lfilter_LCons_found";
    1.64 +(*This rewrite and lfilter_LCons_seek are NOT added because lfilter_LCons
    1.65 +  subsumes both*)
    1.66  
    1.67  
    1.68  goal thy "!!p. (l, LCons x l') : findRel p \
    1.69  \              ==> lfilter p l = LCons x (lfilter p l')";
    1.70  by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
    1.71 -by (asm_simp_tac (simpset() addsimps [findRel_imp_find]) 1);
    1.72 +by (Asm_simp_tac 1);
    1.73  qed "findRel_imp_lfilter";
    1.74  
    1.75 +Addsimps [findRel_imp_lfilter];
    1.76 +
    1.77 +
    1.78  goal thy "!!p. ~ (p x) ==> lfilter p (LCons x l) = lfilter p l";
    1.79  by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
    1.80  by (case_tac "LCons x l : Domain(findRel p)" 1);
    1.81 -by (asm_full_simp_tac (simpset() addsimps [diverge_lfilter_LNil]) 2);
    1.82 +by (Asm_full_simp_tac 2);
    1.83  by (etac Domain_findRelE 1);
    1.84  by (safe_tac (claset() delrules [conjI]));
    1.85 -by (asm_full_simp_tac 
    1.86 -    (simpset() addsimps [findRel_imp_lfilter, findRel_imp_find,
    1.87 -                        find_LCons_seek]) 1);
    1.88 +by (Asm_full_simp_tac 1);
    1.89  qed "lfilter_LCons_seek";
    1.90  
    1.91  
    1.92  goal thy "lfilter p (LCons x l) = \
    1.93  \         (if p x then LCons x (lfilter p l) else lfilter p l)";
    1.94  by (asm_simp_tac (simpset() addsimps [lfilter_LCons_found, lfilter_LCons_seek]
    1.95 -                           addsplits [expand_if]) 1);
    1.96 +                            addsplits [expand_if]) 1);
    1.97  qed "lfilter_LCons";
    1.98  
    1.99  AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
   1.100 -Addsimps [lfilter_LNil, lfilter_LCons];
   1.101 +Addsimps [lfilter_LCons];
   1.102  
   1.103  
   1.104  goal thy "!!p. lfilter p l = LNil ==> l ~: Domain(findRel p)";
   1.105  by (rtac notI 1);
   1.106  by (etac Domain_findRelE 1);
   1.107  by (etac rev_mp 1);
   1.108 -by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter]) 1);
   1.109 +by (Asm_simp_tac 1);
   1.110  qed "lfilter_eq_LNil";
   1.111  
   1.112  
   1.113 @@ -162,7 +170,7 @@
   1.114  by (case_tac "l : Domain(findRel p)" 1);
   1.115  by (etac Domain_findRelE 1);
   1.116  by (Asm_simp_tac 2);
   1.117 -by (asm_simp_tac (simpset() addsimps [findRel_imp_find]) 1);
   1.118 +by (Asm_simp_tac 1);
   1.119  by (Blast_tac 1);
   1.120  qed_spec_mp "lfilter_eq_LCons";
   1.121  
   1.122 @@ -170,9 +178,9 @@
   1.123  goal thy "lfilter p l = LNil  |  \
   1.124  \         (EX y l'. lfilter p l = LCons y (lfilter p l') & p y)";
   1.125  by (case_tac "l : Domain(findRel p)" 1);
   1.126 -by (asm_simp_tac (simpset() addsimps [diverge_lfilter_LNil]) 2);
   1.127 +by (Asm_simp_tac 2);
   1.128  by (blast_tac (claset() addSEs [Domain_findRelE] 
   1.129 -                       addIs [findRel_imp_lfilter]) 1);
   1.130 +                        addIs  [findRel_imp_lfilter]) 1);
   1.131  qed "lfilter_cases";
   1.132  
   1.133  
   1.134 @@ -228,7 +236,7 @@
   1.135  \                  --> l : Domain (findRel(%x. p x & q x))";
   1.136  by (etac findRel.induct 1);
   1.137  by (blast_tac (claset() addSDs [sym RS lfilter_eq_LCons]
   1.138 -                       addIs  [findRel_conj]) 1);
   1.139 +                        addIs  [findRel_conj]) 1);
   1.140  by Auto_tac;
   1.141  by (dtac (sym RS lfilter_eq_LCons) 1);
   1.142  by Auto_tac;
   1.143 @@ -256,14 +264,13 @@
   1.144  by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
   1.145  by (blast_tac (claset() addIs [impOfSubs Domain_findRel_mono]) 3);
   1.146  (*There are no qs in l: both lists are LNil*)
   1.147 -by (asm_simp_tac (simpset() addsimps [diverge_lfilter_LNil]) 2);
   1.148 +by (Asm_simp_tac 2);
   1.149  by (etac Domain_findRelE 1);
   1.150  (*case q x*)
   1.151  by (case_tac "p x" 1);
   1.152 -by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter,
   1.153 -                                     findRel_conj RS findRel_imp_lfilter]) 1);
   1.154 +by (asm_simp_tac (simpset() addsimps [findRel_conj RS findRel_imp_lfilter]) 1);
   1.155  (*case q x and ~(p x) *)
   1.156 -by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter]) 1);
   1.157 +by (Asm_simp_tac 1);
   1.158  by (case_tac "l' : Domain (findRel (%x. p x & q x))" 1);
   1.159  (*subcase: there is no p&q in l' and therefore none in l*)
   1.160  by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
   1.161 @@ -271,14 +278,14 @@
   1.162  by (subgoal_tac "lfilter q l' ~: Domain(findRel p)" 2);
   1.163  by (blast_tac (claset() addIs [findRel_lfilter_Domain_conj]) 3);
   1.164  (*    ...and therefore too, no p in lfilter q l'.  Both results are Lnil*)
   1.165 -by (asm_simp_tac (simpset() addsimps [diverge_lfilter_LNil]) 2);
   1.166 +by (Asm_simp_tac 2);
   1.167  (*subcase: there is a p&q in l' and therefore also one in l*)
   1.168  by (etac Domain_findRelE 1);
   1.169  by (subgoal_tac "(l, LCons xa l'a) : findRel(%x. p x & q x)" 1);
   1.170  by (blast_tac (claset() addIs [findRel_conj2]) 2);
   1.171  by (subgoal_tac "(lfilter q l', LCons xa (lfilter q l'a)) : findRel p" 1);
   1.172  by (blast_tac (claset() addIs [findRel_conj_lfilter]) 2);
   1.173 -by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter]) 1);
   1.174 +by (Asm_simp_tac 1);
   1.175  val lemma = result();
   1.176  
   1.177  
   1.178 @@ -327,9 +334,9 @@
   1.179  by (case_tac "lmap f l : Domain (findRel p)" 1);
   1.180  by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2);
   1.181  by (blast_tac (claset() addIs [findRel_lmap_Domain]) 3);
   1.182 -by (asm_simp_tac (simpset() addsimps [diverge_lfilter_LNil]) 2);
   1.183 +by (Asm_simp_tac 2);
   1.184  by (etac Domain_findRelE 1);
   1.185  by (forward_tac [lmap_LCons_findRel] 1);
   1.186  by (Clarify_tac 1);
   1.187 -by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter]) 1);
   1.188 +by (Asm_simp_tac 1);
   1.189  qed "lfilter_lmap";
     2.1 --- a/src/HOL/Induct/LList.ML	Wed Jan 07 13:55:54 1998 +0100
     2.2 +++ b/src/HOL/Induct/LList.ML	Thu Jan 08 11:21:45 1998 +0100
     2.3 @@ -14,11 +14,6 @@
     2.4  
     2.5  simpset_ref() := simpset() addsplits [expand_split, expand_sum_case];
     2.6  
     2.7 -(*For adding _eqI rules to a simpset; we must remove Pair_eq because
     2.8 -  it may turn an instance of reflexivity into a conjunction!*)
     2.9 -fun add_eqI ss = ss addsimps [range_eqI, image_eqI] 
    2.10 -                    delsimps [Pair_eq];
    2.11 -
    2.12  
    2.13  (*This justifies using llist in other recursive type definitions*)
    2.14  goalw LList.thy llist.defs "!!A B. A<=B ==> llist(A) <= llist(B)";
    2.15 @@ -49,11 +44,14 @@
    2.16  goalw LList.thy [list_Fun_def, NIL_def] "NIL: list_Fun A X";
    2.17  by (Fast_tac 1);
    2.18  qed "list_Fun_NIL_I";
    2.19 +AddIffs [list_Fun_NIL_I];
    2.20  
    2.21  goalw LList.thy [list_Fun_def,CONS_def]
    2.22      "!!M N. [| M: A;  N: X |] ==> CONS M N : list_Fun A X";
    2.23  by (Fast_tac 1);
    2.24  qed "list_Fun_CONS_I";
    2.25 +Addsimps [list_Fun_CONS_I];
    2.26 +AddSIs   [list_Fun_CONS_I];
    2.27  
    2.28  (*Utilise the "strong" part, i.e. gfp(f)*)
    2.29  goalw LList.thy (llist.defs @ [list_Fun_def])
    2.30 @@ -130,8 +128,7 @@
    2.31  by (rtac rangeI 1);
    2.32  by Safe_tac;
    2.33  by (stac LList_corec 1);
    2.34 -by (simp_tac (simpset() addsimps [list_Fun_NIL_I, list_Fun_CONS_I, CollectI]
    2.35 -                       |> add_eqI) 1);
    2.36 +by (Simp_tac 1);
    2.37  qed "LList_corec_type";
    2.38  
    2.39  (*Lemma for the proof of llist_corec*)
    2.40 @@ -142,8 +139,7 @@
    2.41  by (rtac rangeI 1);
    2.42  by Safe_tac;
    2.43  by (stac LList_corec 1);
    2.44 -by (asm_simp_tac (simpset() addsimps [list_Fun_NIL_I]) 1);
    2.45 -by (fast_tac (claset() addSIs [list_Fun_CONS_I]) 1);
    2.46 +by (Asm_simp_tac 1);
    2.47  qed "LList_corec_type2";
    2.48  
    2.49  
    2.50 @@ -163,11 +159,11 @@
    2.51  by (etac LListD.elim 1);
    2.52  by (safe_tac (claset_of Prod.thy delrules [equalityI] addSEs [diagE]));
    2.53  by (res_inst_tac [("n", "n")] natE 1);
    2.54 -by (asm_simp_tac (simpset() addsimps [ntrunc_0]) 1);
    2.55 +by (Asm_simp_tac 1);
    2.56  by (rename_tac "n'" 1);
    2.57  by (res_inst_tac [("n", "n'")] natE 1);
    2.58 -by (asm_simp_tac (simpset() addsimps [CONS_def, ntrunc_one_In1]) 1);
    2.59 -by (asm_simp_tac (simpset() addsimps [CONS_def, ntrunc_In1, ntrunc_Scons, less_Suc_eq]) 1);
    2.60 +by (asm_simp_tac (simpset() addsimps [CONS_def]) 1);
    2.61 +by (asm_simp_tac (simpset() addsimps [CONS_def, less_Suc_eq]) 1);
    2.62  qed "LListD_implies_ntrunc_equality";
    2.63  
    2.64  (*The domain of the LListD relation*)
    2.65 @@ -234,7 +230,7 @@
    2.66  by (eresolve_tac [llist.elim] 1);
    2.67  by (ALLGOALS
    2.68      (asm_simp_tac (simpset() addsimps [diagI, LListD_Fun_NIL_I,
    2.69 -                                      LListD_Fun_CONS_I])));
    2.70 +				       LListD_Fun_CONS_I])));
    2.71  qed "diag_subset_LListD";
    2.72  
    2.73  goal LList.thy "LListD(diag(A)) = diag(llist(A))";
    2.74 @@ -265,6 +261,12 @@
    2.75  
    2.76  (*** Finality of llist(A): Uniqueness of functions defined by corecursion ***)
    2.77  
    2.78 +(*We must remove Pair_eq because it may turn an instance of reflexivity
    2.79 +  (h1 b, h2 b) = (h1 ?x17, h2 ?x17) into a conjunction! 
    2.80 +  (or strengthen the Solver?) 
    2.81 +*)
    2.82 +Delsimps [Pair_eq];
    2.83 +
    2.84  (*abstract proof using a bisimulation*)
    2.85  val [prem1,prem2] = goal LList.thy
    2.86   "[| !!x. h1(x) = sum_case (%u. NIL) (split(%z w. CONS z (h1 w))) (f x);  \
    2.87 @@ -279,8 +281,7 @@
    2.88  by (stac prem1 1);
    2.89  by (stac prem2 1);
    2.90  by (simp_tac (simpset() addsimps [LListD_Fun_NIL_I,
    2.91 -                                 CollectI RS LListD_Fun_CONS_I]
    2.92 -                       |> add_eqI) 1);
    2.93 +				  CollectI RS LListD_Fun_CONS_I]) 1);
    2.94  qed "LList_corec_unique";
    2.95  
    2.96  val [prem] = goal LList.thy
    2.97 @@ -298,9 +299,12 @@
    2.98  
    2.99  goalw LList.thy [CONS_def]
   2.100      "ntrunc (Suc(Suc(k))) (CONS M N) = CONS (ntrunc k M) (ntrunc k N)";
   2.101 -by (simp_tac (simpset() addsimps [ntrunc_Scons,ntrunc_In1]) 1);
   2.102 +by (Simp_tac 1);
   2.103  qed "ntrunc_CONS";
   2.104  
   2.105 +Addsimps [ntrunc_one_CONS, ntrunc_CONS];
   2.106 +
   2.107 +
   2.108  val [prem1,prem2] = goal LList.thy
   2.109   "[| !!x. h1(x) = sum_case (%u. NIL) (split(%z w. CONS z (h1 w))) (f x);  \
   2.110  \    !!x. h2(x) = sum_case (%u. NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
   2.111 @@ -319,8 +323,7 @@
   2.112  by (res_inst_tac [("n", "n")] natE 1);
   2.113  by (rename_tac "m" 2);
   2.114  by (res_inst_tac [("n", "m")] natE 2);
   2.115 -by (ALLGOALS(asm_simp_tac(simpset() addsimps
   2.116 -            [ntrunc_0,ntrunc_one_CONS,ntrunc_CONS, less_Suc_eq])));
   2.117 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
   2.118  result();
   2.119  
   2.120  
   2.121 @@ -436,9 +439,7 @@
   2.122  \ |] ==> f(M) = g(M)";
   2.123  by (rtac LList_equalityI 1);
   2.124  by (rtac (Mlist RS imageI) 1);
   2.125 -by (rtac subsetI 1);
   2.126 -by (etac imageE 1);
   2.127 -by (etac ssubst 1);
   2.128 +by (rtac image_subsetI 1);
   2.129  by (etac llist.elim 1);
   2.130  by (etac ssubst 1);
   2.131  by (stac NILcase 1);
   2.132 @@ -460,13 +461,15 @@
   2.133  by (Simp_tac 1);
   2.134  qed "Lmap_CONS";
   2.135  
   2.136 +Addsimps [Lmap_NIL, Lmap_CONS];
   2.137 +
   2.138  (*Another type-checking proof by coinduction*)
   2.139  val [major,minor] = goal LList.thy
   2.140      "[| M: llist(A);  !!x. x:A ==> f(x):B |] ==> Lmap f M: llist(B)";
   2.141  by (rtac (major RS imageI RS llist_coinduct) 1);
   2.142  by Safe_tac;
   2.143  by (etac llist.elim 1);
   2.144 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [Lmap_NIL,Lmap_CONS])));
   2.145 +by (ALLGOALS Asm_simp_tac);
   2.146  by (REPEAT (ares_tac [list_Fun_NIL_I, list_Fun_CONS_I, 
   2.147                        minor, imageI, UnI1] 1));
   2.148  qed "Lmap_type";
   2.149 @@ -484,7 +487,7 @@
   2.150  by (rtac (prem RS imageI RS LList_equalityI) 1);
   2.151  by Safe_tac;
   2.152  by (etac llist.elim 1);
   2.153 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [Lmap_NIL,Lmap_CONS])));
   2.154 +by (ALLGOALS Asm_simp_tac);
   2.155  by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI, UnI1,
   2.156                        rangeI RS LListD_Fun_CONS_I] 1));
   2.157  qed "Lmap_compose";
   2.158 @@ -493,7 +496,7 @@
   2.159  by (rtac (prem RS imageI RS LList_equalityI) 1);
   2.160  by Safe_tac;
   2.161  by (etac llist.elim 1);
   2.162 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [Lmap_NIL,Lmap_CONS])));
   2.163 +by (ALLGOALS Asm_simp_tac);
   2.164  by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI RS UnI1,
   2.165                        rangeI RS LListD_Fun_CONS_I] 1));
   2.166  qed "Lmap_ident";
   2.167 @@ -520,7 +523,7 @@
   2.168  
   2.169  Addsimps [llist.NIL_I, Lappend_NIL_NIL, Lappend_NIL_CONS,
   2.170            Lappend_CONS, LListD_Fun_CONS_I, range_eqI, image_eqI];
   2.171 -Delsimps [Pair_eq];
   2.172 +
   2.173  
   2.174  goal LList.thy "!!M. M: llist(A) ==> Lappend NIL M = M";
   2.175  by (etac LList_fun_equalityI 1);
   2.176 @@ -532,6 +535,9 @@
   2.177  by (ALLGOALS Asm_simp_tac);
   2.178  qed "Lappend_NIL2";
   2.179  
   2.180 +Addsimps [Lappend_NIL, Lappend_NIL2];
   2.181 +
   2.182 +
   2.183  (** Alternative type-checking proofs for Lappend **)
   2.184  
   2.185  (*weak co-induction: bisimulation and case analysis on both variables*)
   2.186 @@ -543,9 +549,8 @@
   2.187  by Safe_tac;
   2.188  by (eres_inst_tac [("a", "u")] llist.elim 1);
   2.189  by (eres_inst_tac [("a", "v")] llist.elim 1);
   2.190 -by (ALLGOALS
   2.191 -    (Asm_simp_tac THEN'
   2.192 -     fast_tac (claset() addSIs [llist.NIL_I, list_Fun_NIL_I, list_Fun_CONS_I])));
   2.193 +by (ALLGOALS Asm_simp_tac);
   2.194 +by (Blast_tac 1);
   2.195  qed "Lappend_type";
   2.196  
   2.197  (*strong co-induction: bisimulation and case analysis on one variable*)
   2.198 @@ -553,12 +558,10 @@
   2.199      "!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
   2.200  by (res_inst_tac [("X", "(%u. Lappend u N)``llist(A)")] llist_coinduct 1);
   2.201  by (etac imageI 1);
   2.202 -by (rtac subsetI 1);
   2.203 -by (etac imageE 1);
   2.204 -by (eres_inst_tac [("a", "u")] llist.elim 1);
   2.205 -by (asm_simp_tac (simpset() addsimps [Lappend_NIL, list_Fun_llist_I]) 1);
   2.206 +by (rtac image_subsetI 1);
   2.207 +by (eres_inst_tac [("a", "x")] llist.elim 1);
   2.208 +by (asm_simp_tac (simpset() addsimps [list_Fun_llist_I]) 1);
   2.209  by (Asm_simp_tac 1);
   2.210 -by (fast_tac (claset() addSIs [list_Fun_CONS_I]) 1);
   2.211  qed "Lappend_type";
   2.212  
   2.213  (**** Lazy lists as the type 'a llist -- strongly typed versions of above ****)
   2.214 @@ -587,7 +590,8 @@
   2.215  by (assume_tac 1);
   2.216  by (etac rangeE 1);
   2.217  by (rtac (inj_Rep_llist RS injD RS prem2) 1);
   2.218 -by (asm_simp_tac (simpset() delsimps [CONS_CONS_eq] addsimps [Rep_llist_LCons]) 1);
   2.219 +by (asm_simp_tac (simpset() delsimps [CONS_CONS_eq] 
   2.220 +		            addsimps [Rep_llist_LCons]) 1);
   2.221  by (etac (Abs_llist_inverse RS ssubst) 1);
   2.222  by (rtac refl 1);
   2.223  qed "llistE";
   2.224 @@ -629,7 +633,8 @@
   2.225  goal LList.thy
   2.226      "prod_fun Rep_llist Rep_llist `` r <= \
   2.227  \    (llist(range Leaf)) Times (llist(range Leaf))";
   2.228 -by (fast_tac (claset() addIs [Rep_llist]) 1);
   2.229 +by (fast_tac (claset() delrules [image_subsetI]
   2.230 +		       addIs [Rep_llist]) 1);
   2.231  qed "subset_Sigma_llist";
   2.232  
   2.233  val [prem] = goal LList.thy
   2.234 @@ -638,7 +643,7 @@
   2.235  by Safe_tac;
   2.236  by (rtac (prem RS subsetD RS SigmaE2) 1);
   2.237  by (assume_tac 1);
   2.238 -by (asm_simp_tac (simpset() addsimps [o_def,prod_fun,Abs_llist_inverse]) 1);
   2.239 +by (asm_simp_tac (simpset() addsimps [Abs_llist_inverse]) 1);
   2.240  qed "prod_fun_lemma";
   2.241  
   2.242  goal LList.thy
     3.1 --- a/src/HOL/Induct/SList.ML	Wed Jan 07 13:55:54 1998 +0100
     3.2 +++ b/src/HOL/Induct/SList.ML	Thu Jan 08 11:21:45 1998 +0100
     3.3 @@ -1,7 +1,7 @@
     3.4  (*  Title:      HOL/ex/SList.ML
     3.5      ID:         $Id$
     3.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 -    Copyright   1993  University of Cambridge
     3.8 +    Copyright   1998  University of Cambridge
     3.9  
    3.10  Definition of type 'a list by a least fixed point
    3.11  *)
    3.12 @@ -138,9 +138,12 @@
    3.13  qed "List_case_NIL";
    3.14  
    3.15  goalw SList.thy [List_case_def,CONS_def]  "List_case c h (CONS M N) = h M N";
    3.16 -by (simp_tac (simpset() addsimps [Split,Case_In1]) 1);
    3.17 +by (Simp_tac 1);
    3.18  qed "List_case_CONS";
    3.19  
    3.20 +Addsimps [List_case_NIL, List_case_CONS];
    3.21 +
    3.22 +
    3.23  (*** List_rec -- by wf recursion on pred_sexp ***)
    3.24  
    3.25  (* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not
    3.26 @@ -185,23 +188,25 @@
    3.27  
    3.28  goal SList.thy "List_rec NIL c h = c";
    3.29  by (rtac (List_rec_unfold RS trans) 1);
    3.30 -by (simp_tac (simpset() addsimps [List_case_NIL]) 1);
    3.31 +by (Simp_tac 1);
    3.32  qed "List_rec_NIL";
    3.33  
    3.34  goal SList.thy "!!M. [| M: sexp;  N: sexp |] ==> \
    3.35  \    List_rec (CONS M N) c h = h M N (List_rec N c h)";
    3.36  by (rtac (List_rec_unfold RS trans) 1);
    3.37 -by (asm_simp_tac (simpset() addsimps [List_case_CONS, pred_sexp_CONS_I2]) 1);
    3.38 +by (asm_simp_tac (simpset() addsimps [pred_sexp_CONS_I2]) 1);
    3.39  qed "List_rec_CONS";
    3.40  
    3.41 +Addsimps [List_rec_NIL, List_rec_CONS];
    3.42 +
    3.43 +
    3.44  (*** list_rec -- by List_rec ***)
    3.45  
    3.46  val Rep_list_in_sexp =
    3.47      [range_Leaf_subset_sexp RS list_subset_sexp, Rep_list] MRS subsetD;
    3.48  
    3.49  local
    3.50 -  val list_rec_simps = [List_rec_NIL, List_rec_CONS, 
    3.51 -                        Abs_list_inverse, Rep_list_inverse,
    3.52 +  val list_rec_simps = [Abs_list_inverse, Rep_list_inverse,
    3.53                          Rep_list, rangeI, inj_Leaf, inv_f_f,
    3.54                          sexp.LeafI, Rep_list_in_sexp]
    3.55  in
    3.56 @@ -364,8 +369,8 @@
    3.57  goal SList.thy "!!f. (!!x. f(x): sexp) ==> \
    3.58  \       Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs";
    3.59  by (list_ind_tac "xs" 1);
    3.60 -by (ALLGOALS(asm_simp_tac(simpset() addsimps
    3.61 -       [Rep_map_type,list_sexp RS subsetD])));
    3.62 +by (ALLGOALS (asm_simp_tac(simpset() addsimps
    3.63 +			   [Rep_map_type, list_sexp RS subsetD])));
    3.64  qed "Abs_Rep_map";
    3.65  
    3.66  Addsimps [append_Nil4, map_ident2];
     4.1 --- a/src/HOL/Prod.ML	Wed Jan 07 13:55:54 1998 +0100
     4.2 +++ b/src/HOL/Prod.ML	Thu Jan 08 11:21:45 1998 +0100
     4.3 @@ -241,19 +241,21 @@
     4.4  goalw Prod.thy [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";
     4.5  by (rtac split 1);
     4.6  qed "prod_fun";
     4.7 +Addsimps [prod_fun];
     4.8  
     4.9  goal Prod.thy 
    4.10      "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
    4.11  by (rtac ext 1);
    4.12  by (res_inst_tac [("p","x")] PairE 1);
    4.13 -by (asm_simp_tac (simpset() addsimps [prod_fun,o_def]) 1);
    4.14 +by (Asm_simp_tac 1);
    4.15  qed "prod_fun_compose";
    4.16  
    4.17  goal Prod.thy "prod_fun (%x. x) (%y. y) = (%z. z)";
    4.18  by (rtac ext 1);
    4.19  by (res_inst_tac [("p","z")] PairE 1);
    4.20 -by (asm_simp_tac (simpset() addsimps [prod_fun]) 1);
    4.21 +by (Asm_simp_tac 1);
    4.22  qed "prod_fun_ident";
    4.23 +Addsimps [prod_fun_ident];
    4.24  
    4.25  val prems = goal Prod.thy "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
    4.26  by (rtac image_eqI 1);
    4.27 @@ -271,6 +273,7 @@
    4.28  by (blast_tac (claset() addIs [prod_fun]) 1);
    4.29  qed "prod_fun_imageE";
    4.30  
    4.31 +
    4.32  (*** Disjoint union of a family of sets - Sigma ***)
    4.33  
    4.34  qed_goalw "SigmaI" Prod.thy [Sigma_def]
     5.1 --- a/src/HOL/Sexp.ML	Wed Jan 07 13:55:54 1998 +0100
     5.2 +++ b/src/HOL/Sexp.ML	Thu Jan 08 11:21:45 1998 +0100
     5.3 @@ -22,6 +22,8 @@
     5.4  by (blast_tac (claset() addSIs [select_equality]) 1);
     5.5  qed "sexp_case_Scons";
     5.6  
     5.7 +Addsimps [sexp_case_Leaf, sexp_case_Numb, sexp_case_Scons];
     5.8 +
     5.9  
    5.10  (** Introduction rules for sexp constructors **)
    5.11  
    5.12 @@ -100,6 +102,13 @@
    5.13     "(%M. sexp_rec M c d e) = wfrec pred_sexp \
    5.14                         \ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))";
    5.15  by (simp_tac (HOL_ss addsimps [sexp_rec_def]) 1);
    5.16 +
    5.17 +(* sexp_rec a c d e =
    5.18 +   sexp_case c d
    5.19 +    (%N1 N2.
    5.20 +        e N1 N2 (cut (%M. sexp_rec M c d e) pred_sexp a N1)
    5.21 +         (cut (%M. sexp_rec M c d e) pred_sexp a N2)) a
    5.22 +*)
    5.23  bind_thm("sexp_rec_unfold", 
    5.24  	 [result() RS eq_reflection, wf_pred_sexp] MRS def_wfrec);
    5.25  
    5.26 @@ -118,6 +127,5 @@
    5.27  goal Sexp.thy "!!M. [| M: sexp;  N: sexp |] ==> \
    5.28  \    sexp_rec (M$N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
    5.29  by (rtac (sexp_rec_unfold RS trans) 1);
    5.30 -by (asm_simp_tac (simpset() addsimps [sexp_case_Scons,pred_sexpI1,pred_sexpI2])
    5.31 -    1);
    5.32 +by (asm_simp_tac (simpset() addsimps [pred_sexpI1, pred_sexpI2]) 1);
    5.33  qed "sexp_rec_Scons";
     6.1 --- a/src/HOL/Univ.ML	Wed Jan 07 13:55:54 1998 +0100
     6.2 +++ b/src/HOL/Univ.ML	Thu Jan 08 11:21:45 1998 +0100
     6.3 @@ -265,30 +265,35 @@
     6.4              assume_tac 1));
     6.5  qed "ntrunc_Scons";
     6.6  
     6.7 +Addsimps [ntrunc_0, ntrunc_Atom, ntrunc_Leaf, ntrunc_Numb, ntrunc_Scons];
     6.8 +
     6.9 +
    6.10  (** Injection nodes **)
    6.11  
    6.12  goalw Univ.thy [In0_def] "ntrunc (Suc 0) (In0 M) = {}";
    6.13 -by (simp_tac (simpset() addsimps [ntrunc_Scons,ntrunc_0]) 1);
    6.14 +by (Simp_tac 1);
    6.15  by (rewtac Scons_def);
    6.16  by (Blast_tac 1);
    6.17  qed "ntrunc_one_In0";
    6.18  
    6.19  goalw Univ.thy [In0_def]
    6.20      "ntrunc (Suc (Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)";
    6.21 -by (simp_tac (simpset() addsimps [ntrunc_Scons,ntrunc_Numb]) 1);
    6.22 +by (Simp_tac 1);
    6.23  qed "ntrunc_In0";
    6.24  
    6.25  goalw Univ.thy [In1_def] "ntrunc (Suc 0) (In1 M) = {}";
    6.26 -by (simp_tac (simpset() addsimps [ntrunc_Scons,ntrunc_0]) 1);
    6.27 +by (Simp_tac 1);
    6.28  by (rewtac Scons_def);
    6.29  by (Blast_tac 1);
    6.30  qed "ntrunc_one_In1";
    6.31  
    6.32  goalw Univ.thy [In1_def]
    6.33      "ntrunc (Suc (Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)";
    6.34 -by (simp_tac (simpset() addsimps [ntrunc_Scons,ntrunc_Numb]) 1);
    6.35 +by (Simp_tac 1);
    6.36  qed "ntrunc_In1";
    6.37  
    6.38 +Addsimps [ntrunc_one_In0, ntrunc_In0, ntrunc_one_In1, ntrunc_In1];
    6.39 +
    6.40  
    6.41  (*** Cartesian Product ***)
    6.42  
    6.43 @@ -383,7 +388,7 @@
    6.44  val [major] = goalw Univ.thy [ntrunc_def]
    6.45      "(!!k. ntrunc k M <= N) ==> M<=N";
    6.46  by (blast_tac (claset() addIs [less_add_Suc1, less_add_Suc2, 
    6.47 -                            major RS subsetD]) 1);
    6.48 +			       major RS subsetD]) 1);
    6.49  qed "ntrunc_subsetD";
    6.50  
    6.51  (*A generalized form of the take-lemma*)
    6.52 @@ -438,6 +443,9 @@
    6.53  by (blast_tac (claset() addIs [select_equality]) 1);
    6.54  qed "Case_In1";
    6.55  
    6.56 +Addsimps [Split, Case_In0, Case_In1];
    6.57 +
    6.58 +
    6.59  (**** UN x. B(x) rules ****)
    6.60  
    6.61  goalw Univ.thy [ntrunc_def] "ntrunc k (UN x. f(x)) = (UN x. ntrunc k (f x))";
    6.62 @@ -562,15 +570,15 @@
    6.63  (*** Domain ***)
    6.64  
    6.65  goal Univ.thy "fst `` diag(A) = A";
    6.66 -by (Blast_tac 1);
    6.67 +by Auto_tac;
    6.68  qed "fst_image_diag";
    6.69  
    6.70  goal Univ.thy "fst `` (r<**>s) = (fst``r) <*> (fst``s)";
    6.71 -by (Blast_tac 1);
    6.72 +by Auto_tac;
    6.73  qed "fst_image_dprod";
    6.74  
    6.75  goal Univ.thy "fst `` (r<++>s) = (fst``r) <+> (fst``s)";
    6.76 -by (Blast_tac 1);
    6.77 +by Auto_tac;
    6.78  qed "fst_image_dsum";
    6.79  
    6.80  Addsimps [fst_image_diag, fst_image_dprod, fst_image_dsum];