Installation of new simplifier for ZF. Deleted all congruence rules not
authorlcp
Fri Sep 17 16:16:38 1993 +0200 (1993-09-17)
changeset 68ce8c4d13d4d
parent 5 75e163863e16
child 7 268f93ab3bc4
Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.
src/ZF/Arith.ML
src/ZF/Arith.thy
src/ZF/Bool.ML
src/ZF/Epsilon.ML
src/ZF/List.ML
src/ZF/ListFn.ML
src/ZF/Nat.ML
src/ZF/Nat.thy
src/ZF/Ord.ML
src/ZF/Pair.ML
src/ZF/Perm.ML
src/ZF/QPair.ML
src/ZF/QUniv.ML
src/ZF/ROOT.ML
src/ZF/Sum.ML
src/ZF/Univ.ML
src/ZF/WF.ML
src/ZF/ZF.ML
src/ZF/arith.ML
src/ZF/arith.thy
src/ZF/bool.ML
src/ZF/constructor.ML
src/ZF/epsilon.ML
src/ZF/fin.ML
src/ZF/func.ML
src/ZF/ind-syntax.ML
src/ZF/ind_syntax.ML
src/ZF/list.ML
src/ZF/listfn.ML
src/ZF/nat.ML
src/ZF/nat.thy
src/ZF/ord.ML
src/ZF/pair.ML
src/ZF/perm.ML
src/ZF/qpair.ML
src/ZF/quniv.ML
src/ZF/simpdata.ML
src/ZF/sum.ML
src/ZF/univ.ML
src/ZF/upair.ML
src/ZF/wf.ML
src/ZF/zf.ML
     1.1 --- a/src/ZF/Arith.ML	Fri Sep 17 12:53:53 1993 +0200
     1.2 +++ b/src/ZF/Arith.ML	Fri Sep 17 16:16:38 1993 +0200
     1.3 @@ -29,10 +29,9 @@
     1.4  
     1.5  goal Arith.thy "rec(succ(m),a,b) = b(m, rec(m,a,b))";
     1.6  val rec_ss = ZF_ss 
     1.7 -      addcongs (mk_typed_congs Arith.thy [("b", "[i,i]=>i")])
     1.8 -      addrews [nat_case_succ, nat_succI];
     1.9 +      addsimps [nat_case_succ, nat_succI];
    1.10  by (rtac rec_trans 1);
    1.11 -by (SIMP_TAC rec_ss 1);
    1.12 +by (simp_tac rec_ss 1);
    1.13  val rec_succ = result();
    1.14  
    1.15  val major::prems = goal Arith.thy
    1.16 @@ -42,20 +41,12 @@
    1.17  \    |] ==> rec(n,a,b) : C(n)";
    1.18  by (rtac (major RS nat_induct) 1);
    1.19  by (ALLGOALS
    1.20 -    (ASM_SIMP_TAC (ZF_ss addrews (prems@[rec_0,rec_succ]))));
    1.21 +    (asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ]))));
    1.22  val rec_type = result();
    1.23  
    1.24 -val prems = goalw Arith.thy [rec_def]
    1.25 -    "[| n=n';  a=a';  !!m z. b(m,z)=b'(m,z)  \
    1.26 -\    |] ==> rec(n,a,b)=rec(n',a',b')";
    1.27 -by (SIMP_TAC (ZF_ss addcongs [transrec_cong,nat_case_cong] 
    1.28 -		    addrews (prems RL [sym])) 1);
    1.29 -val rec_cong = result();
    1.30 -
    1.31  val nat_typechecks = [rec_type,nat_0I,nat_1I,nat_succI,Ord_nat];
    1.32  
    1.33 -val nat_ss = ZF_ss addcongs [nat_case_cong,rec_cong]
    1.34 -	       	   addrews ([rec_0,rec_succ] @ nat_typechecks);
    1.35 +val nat_ss = ZF_ss addsimps ([rec_0,rec_succ] @ nat_typechecks);
    1.36  
    1.37  
    1.38  (** Addition **)
    1.39 @@ -101,16 +92,16 @@
    1.40      "n:nat ==> 0 #- n = 0"
    1.41   (fn [prem]=>
    1.42    [ (rtac (prem RS nat_induct) 1),
    1.43 -    (ALLGOALS (ASM_SIMP_TAC nat_ss)) ]);
    1.44 +    (ALLGOALS (asm_simp_tac nat_ss)) ]);
    1.45  
    1.46  (*Must simplify BEFORE the induction!!  (Else we get a critical pair)
    1.47    succ(m) #- succ(n)   rewrites to   pred(succ(m) #- n)  *)
    1.48  val diff_succ_succ = prove_goalw Arith.thy [diff_def]
    1.49      "[| m:nat;  n:nat |] ==> succ(m) #- succ(n) = m #- n"
    1.50   (fn prems=>
    1.51 -  [ (ASM_SIMP_TAC (nat_ss addrews prems) 1),
    1.52 +  [ (asm_simp_tac (nat_ss addsimps prems) 1),
    1.53      (nat_ind_tac "n" prems 1),
    1.54 -    (ALLGOALS (ASM_SIMP_TAC (nat_ss addrews prems))) ]);
    1.55 +    (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
    1.56  
    1.57  val prems = goal Arith.thy 
    1.58      "[| m:nat;  n:nat |] ==> m #- n : succ(m)";
    1.59 @@ -119,8 +110,8 @@
    1.60  by (resolve_tac prems 1);
    1.61  by (etac succE 3);
    1.62  by (ALLGOALS
    1.63 -    (ASM_SIMP_TAC
    1.64 -     (nat_ss addrews (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
    1.65 +    (asm_simp_tac
    1.66 +     (nat_ss addsimps (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
    1.67  val diff_leq = result();
    1.68  
    1.69  (*** Simplification over add, mult, diff ***)
    1.70 @@ -130,10 +121,7 @@
    1.71  		  mult_0, mult_succ,
    1.72  		  diff_0, diff_0_eq_0, diff_succ_succ];
    1.73  
    1.74 -val arith_congs = mk_congs Arith.thy ["op #+", "op #-", "op #*"];
    1.75 -
    1.76 -val arith_ss = nat_ss addcongs arith_congs
    1.77 -                      addrews  (arith_rews@arith_typechecks);
    1.78 +val arith_ss = nat_ss addsimps (arith_rews@arith_typechecks);
    1.79  
    1.80  (*** Addition ***)
    1.81  
    1.82 @@ -142,7 +130,7 @@
    1.83      "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)"
    1.84   (fn prems=>
    1.85    [ (nat_ind_tac "m" prems 1),
    1.86 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
    1.87 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
    1.88  
    1.89  (*The following two lemmas are used for add_commute and sometimes
    1.90    elsewhere, since they are safe for rewriting.*)
    1.91 @@ -150,13 +138,13 @@
    1.92      "m:nat ==> m #+ 0 = m"
    1.93   (fn prems=>
    1.94    [ (nat_ind_tac "m" prems 1),
    1.95 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]); 
    1.96 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
    1.97  
    1.98  val add_succ_right = prove_goal Arith.thy
    1.99      "m:nat ==> m #+ succ(n) = succ(m #+ n)"
   1.100   (fn prems=>
   1.101    [ (nat_ind_tac "m" prems 1),
   1.102 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]); 
   1.103 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
   1.104  
   1.105  (*Commutative law for addition*)  
   1.106  val add_commute = prove_goal Arith.thy 
   1.107 @@ -164,15 +152,15 @@
   1.108   (fn prems=>
   1.109    [ (nat_ind_tac "n" prems 1),
   1.110      (ALLGOALS
   1.111 -     (ASM_SIMP_TAC
   1.112 -      (arith_ss addrews (prems@[add_0_right, add_succ_right])))) ]);
   1.113 +     (asm_simp_tac
   1.114 +      (arith_ss addsimps (prems@[add_0_right, add_succ_right])))) ]);
   1.115  
   1.116  (*Cancellation law on the left*)
   1.117  val [knat,eqn] = goal Arith.thy 
   1.118      "[| k:nat;  k #+ m = k #+ n |] ==> m=n";
   1.119  by (rtac (eqn RS rev_mp) 1);
   1.120  by (nat_ind_tac "k" [knat] 1);
   1.121 -by (ALLGOALS (SIMP_TAC arith_ss));
   1.122 +by (ALLGOALS (simp_tac arith_ss));
   1.123  by (fast_tac ZF_cs 1);
   1.124  val add_left_cancel = result();
   1.125  
   1.126 @@ -183,39 +171,40 @@
   1.127      "m:nat ==> m #* 0 = 0"
   1.128   (fn prems=>
   1.129    [ (nat_ind_tac "m" prems 1),
   1.130 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems)))  ]);
   1.131 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems)))  ]);
   1.132  
   1.133  (*right successor law for multiplication*)
   1.134  val mult_succ_right = prove_goal Arith.thy 
   1.135 -    "[| m:nat;  n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
   1.136 - (fn prems=>
   1.137 -  [ (nat_ind_tac "m" prems 1),
   1.138 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))),
   1.139 +    "!!m n. [| m:nat;  n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
   1.140 + (fn _=>
   1.141 +  [ (nat_ind_tac "m" [] 1),
   1.142 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))),
   1.143         (*The final goal requires the commutative law for addition*)
   1.144 -    (REPEAT (ares_tac (prems@[refl,add_commute]@ZF_congs@arith_congs) 1))  ]);
   1.145 +    (rtac (add_commute RS subst_context) 1),
   1.146 +    (REPEAT (assume_tac 1))  ]);
   1.147  
   1.148  (*Commutative law for multiplication*)
   1.149  val mult_commute = prove_goal Arith.thy 
   1.150      "[| m:nat;  n:nat |] ==> m #* n = n #* m"
   1.151   (fn prems=>
   1.152    [ (nat_ind_tac "m" prems 1),
   1.153 -    (ALLGOALS (ASM_SIMP_TAC
   1.154 -	       (arith_ss addrews (prems@[mult_0_right, mult_succ_right])))) ]);
   1.155 +    (ALLGOALS (asm_simp_tac
   1.156 +	     (arith_ss addsimps (prems@[mult_0_right, mult_succ_right])))) ]);
   1.157  
   1.158  (*addition distributes over multiplication*)
   1.159  val add_mult_distrib = prove_goal Arith.thy 
   1.160      "[| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
   1.161   (fn prems=>
   1.162    [ (nat_ind_tac "m" prems 1),
   1.163 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))) ]);
   1.164 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps ([add_assoc RS sym]@prems)))) ]);
   1.165  
   1.166  (*Distributive law on the left; requires an extra typing premise*)
   1.167  val add_mult_distrib_left = prove_goal Arith.thy 
   1.168      "[| m:nat;  n:nat;  k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"
   1.169   (fn prems=>
   1.170        let val mult_commute' = read_instantiate [("m","k")] mult_commute
   1.171 -          val ss = arith_ss addrews ([mult_commute',add_mult_distrib]@prems)
   1.172 -      in [ (SIMP_TAC ss 1) ]
   1.173 +          val ss = arith_ss addsimps ([mult_commute',add_mult_distrib]@prems)
   1.174 +      in [ (simp_tac ss 1) ]
   1.175        end);
   1.176  
   1.177  (*Associative law for multiplication*)
   1.178 @@ -223,7 +212,7 @@
   1.179      "[| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
   1.180   (fn prems=>
   1.181    [ (nat_ind_tac "m" prems 1),
   1.182 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews (prems@[add_mult_distrib])))) ]);
   1.183 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps (prems@[add_mult_distrib])))) ]);
   1.184  
   1.185  
   1.186  (*** Difference ***)
   1.187 @@ -232,7 +221,7 @@
   1.188      "m:nat ==> m #- m = 0"
   1.189   (fn prems=>
   1.190    [ (nat_ind_tac "m" prems 1),
   1.191 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
   1.192 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
   1.193  
   1.194  (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
   1.195  val notless::prems = goal Arith.thy
   1.196 @@ -241,8 +230,8 @@
   1.197  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.198  by (resolve_tac prems 1);
   1.199  by (resolve_tac prems 1);
   1.200 -by (ALLGOALS (ASM_SIMP_TAC
   1.201 -	      (arith_ss addrews (prems@[succ_mem_succ_iff, Ord_0_mem_succ, 
   1.202 +by (ALLGOALS (asm_simp_tac
   1.203 +	      (arith_ss addsimps (prems@[succ_mem_succ_iff, Ord_0_mem_succ, 
   1.204  				  naturals_are_ordinals]))));
   1.205  val add_diff_inverse = result();
   1.206  
   1.207 @@ -251,29 +240,24 @@
   1.208  val [mnat,nnat] = goal Arith.thy
   1.209      "[| m:nat;  n:nat |] ==> (n#+m) #-n = m";
   1.210  by (rtac (nnat RS nat_induct) 1);
   1.211 -by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mnat])));
   1.212 +by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
   1.213  val diff_add_inverse = result();
   1.214  
   1.215  val [mnat,nnat] = goal Arith.thy
   1.216      "[| m:nat;  n:nat |] ==> n #- (n#+m) = 0";
   1.217  by (rtac (nnat RS nat_induct) 1);
   1.218 -by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mnat])));
   1.219 +by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
   1.220  val diff_add_0 = result();
   1.221  
   1.222  
   1.223  (*** Remainder ***)
   1.224  
   1.225  (*In ordinary notation: if 0<n and n<=m then m-n < m *)
   1.226 -val prems = goal Arith.thy
   1.227 -    "[| 0:n; ~ m:n;  m:nat;  n:nat |] ==> m #- n : m";
   1.228 -by (cut_facts_tac prems 1);
   1.229 +goal Arith.thy "!!m n. [| 0:n; ~ m:n;  m:nat;  n:nat |] ==> m #- n : m";
   1.230  by (etac rev_mp 1);
   1.231  by (etac rev_mp 1);
   1.232  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.233 -by (resolve_tac prems 1);
   1.234 -by (resolve_tac prems 1);
   1.235 -by (ALLGOALS (ASM_SIMP_TAC
   1.236 -	      (nat_ss addrews (prems@[diff_leq,diff_succ_succ]))));
   1.237 +by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_leq,diff_succ_succ])));
   1.238  val div_termination = result();
   1.239  
   1.240  val div_rls =
   1.241 @@ -286,17 +270,17 @@
   1.242  by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
   1.243  val mod_type = result();
   1.244  
   1.245 -val div_ss = ZF_ss addrews [naturals_are_ordinals,div_termination];
   1.246 +val div_ss = ZF_ss addsimps [naturals_are_ordinals,div_termination];
   1.247  
   1.248  val prems = goal Arith.thy "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m mod n = m";
   1.249  by (rtac (mod_def RS def_transrec RS trans) 1);
   1.250 -by (SIMP_TAC (div_ss addrews prems) 1);
   1.251 +by (simp_tac (div_ss addsimps prems) 1);
   1.252  val mod_less = result();
   1.253  
   1.254  val prems = goal Arith.thy
   1.255      "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m mod n = (m#-n) mod n";
   1.256  by (rtac (mod_def RS def_transrec RS trans) 1);
   1.257 -by (SIMP_TAC (div_ss addrews prems) 1);
   1.258 +by (simp_tac (div_ss addsimps prems) 1);
   1.259  val mod_geq = result();
   1.260  
   1.261  (*** Quotient ***)
   1.262 @@ -310,13 +294,13 @@
   1.263  val prems = goal Arith.thy
   1.264      "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m div n = 0";
   1.265  by (rtac (div_def RS def_transrec RS trans) 1);
   1.266 -by (SIMP_TAC (div_ss addrews prems) 1);
   1.267 +by (simp_tac (div_ss addsimps prems) 1);
   1.268  val div_less = result();
   1.269  
   1.270  val prems = goal Arith.thy
   1.271      "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m div n = succ((m#-n) div n)";
   1.272  by (rtac (div_def RS def_transrec RS trans) 1);
   1.273 -by (SIMP_TAC (div_ss addrews prems) 1);
   1.274 +by (simp_tac (div_ss addsimps prems) 1);
   1.275  val div_geq = result();
   1.276  
   1.277  (*Main Result.*)
   1.278 @@ -326,8 +310,8 @@
   1.279  by (resolve_tac prems 1);
   1.280  by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1);
   1.281  by (ALLGOALS 
   1.282 -    (ASM_SIMP_TAC
   1.283 -     (arith_ss addrews ([mod_type,div_type] @ prems @
   1.284 +    (asm_simp_tac
   1.285 +     (arith_ss addsimps ([mod_type,div_type] @ prems @
   1.286          [mod_less,mod_geq, div_less, div_geq,
   1.287  	 add_assoc, add_diff_inverse, div_termination]))));
   1.288  val mod_div_equality = result();
   1.289 @@ -338,7 +322,7 @@
   1.290  val [mnat,nnat] = goal Arith.thy
   1.291      "[| m:nat;  n:nat |] ==> ~ (m #+ n) : n";
   1.292  by (rtac (mnat RS nat_induct) 1);
   1.293 -by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mem_not_refl])));
   1.294 +by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mem_not_refl])));
   1.295  by (rtac notI 1);
   1.296  by (etac notE 1);
   1.297  by (etac (succI1 RS Ord_trans) 1);
     2.1 --- a/src/ZF/Arith.thy	Fri Sep 17 12:53:53 1993 +0200
     2.2 +++ b/src/ZF/Arith.thy	Fri Sep 17 16:16:38 1993 +0200
     2.3 @@ -16,7 +16,7 @@
     2.4      "#-" :: "[i,i]=>i"      		(infixl 65)
     2.5  
     2.6  rules
     2.7 -    rec_def  "rec(k,a,b) ==  transrec(k, %n f. nat_case(n, a, %m. b(m, f`m)))"
     2.8 +    rec_def  "rec(k,a,b) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
     2.9  
    2.10      add_def  "m#+n == rec(m, n, %u v.succ(v))"
    2.11      diff_def "m#-n == rec(n, m, %u v. rec(v, 0, %x y.x))"
     3.1 --- a/src/ZF/Bool.ML	Fri Sep 17 12:53:53 1993 +0200
     3.2 +++ b/src/ZF/Bool.ML	Fri Sep 17 16:16:38 1993 +0200
     3.3 @@ -53,9 +53,6 @@
     3.4  by (resolve_tac prems 1);
     3.5  val cond_type = result();
     3.6  
     3.7 -val [cond_cong] = mk_congs Bool.thy ["cond"];
     3.8 -val bool_congs = mk_congs Bool.thy ["cond","not","op and","op or","op xor"];
     3.9 -
    3.10  val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
    3.11  by (rewtac rew);
    3.12  by (rtac cond_1 1);
     4.1 --- a/src/ZF/Epsilon.ML	Fri Sep 17 12:53:53 1993 +0200
     4.2 +++ b/src/ZF/Epsilon.ML	Fri Sep 17 16:16:38 1993 +0200
     4.3 @@ -64,8 +64,8 @@
     4.4      "!!X A n. [| Transset(X);  A<=X;  n: nat |] ==> \
     4.5  \             nat_rec(n, A, %m r. Union(r)) <= X";
     4.6  by (etac nat_induct 1);
     4.7 -by (ASM_SIMP_TAC (ZF_ss addrews [nat_rec_0]) 1);
     4.8 -by (ASM_SIMP_TAC (ZF_ss addrews [nat_rec_succ]) 1);
     4.9 +by (asm_simp_tac (ZF_ss addsimps [nat_rec_0]) 1);
    4.10 +by (asm_simp_tac (ZF_ss addsimps [nat_rec_succ]) 1);
    4.11  by (fast_tac ZF_cs 1);
    4.12  val eclose_least_lemma = result();
    4.13  
    4.14 @@ -126,8 +126,8 @@
    4.15  by (rtac (kmemj RS eclose_induct) 1);
    4.16  by (rtac wfrec_ssubst 1);
    4.17  by (rtac wfrec_ssubst 1);
    4.18 -by (ASM_SIMP_TAC (wf_ss addrews [under_Memrel_eclose,
    4.19 -				 jmemi RSN (2,mem_eclose_sing_trans)]) 1);
    4.20 +by (asm_simp_tac (ZF_ss addsimps [under_Memrel_eclose,
    4.21 +				  jmemi RSN (2,mem_eclose_sing_trans)]) 1);
    4.22  val wfrec_eclose_eq = result();
    4.23  
    4.24  val [prem] = goal Epsilon.thy
    4.25 @@ -139,8 +139,8 @@
    4.26  goalw Epsilon.thy [transrec_def]
    4.27      "transrec(a,H) = H(a, lam x:a. transrec(x,H))";
    4.28  by (rtac wfrec_ssubst 1);
    4.29 -by (SIMP_TAC (wf_ss addrews [wfrec_eclose_eq2,
    4.30 -			     arg_in_eclose_sing, under_Memrel_eclose]) 1);
    4.31 +by (simp_tac (ZF_ss addsimps [wfrec_eclose_eq2, arg_in_eclose_sing,
    4.32 +			      under_Memrel_eclose]) 1);
    4.33  val transrec = result();
    4.34  
    4.35  (*Avoids explosions in proofs; resolve it with a meta-level definition.*)
    4.36 @@ -173,23 +173,12 @@
    4.37  by (DEPTH_SOLVE (ares_tac prems 1 ORELSE eresolve_tac [ssubst,Ord_trans] 1));
    4.38  val Ord_transrec_type = result();
    4.39  
    4.40 -(*Congruence*)
    4.41 -val prems = goalw Epsilon.thy [transrec_def,Memrel_def]
    4.42 -    "[| a=a';  !!x u. H(x,u)=H'(x,u) |]  ==> transrec(a,H)=transrec(a',H')";
    4.43 -val transrec_ss = 
    4.44 -    ZF_ss addcongs ([wfrec_cong] @ mk_congs Epsilon.thy ["eclose"])
    4.45 -	  addrews (prems RL [sym]);
    4.46 -by (SIMP_TAC transrec_ss 1);
    4.47 -val transrec_cong = result();
    4.48 -
    4.49  (*** Rank ***)
    4.50  
    4.51 -val ord_ss = ZF_ss addcongs (mk_congs Ord.thy ["Ord"]);
    4.52 -
    4.53  (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
    4.54  goal Epsilon.thy "rank(a) = (UN y:a. succ(rank(y)))";
    4.55  by (rtac (rank_def RS def_transrec RS ssubst) 1);
    4.56 -by (SIMP_TAC ZF_ss 1);
    4.57 +by (simp_tac ZF_ss 1);
    4.58  val rank = result();
    4.59  
    4.60  goal Epsilon.thy "Ord(rank(a))";
    4.61 @@ -203,7 +192,7 @@
    4.62  val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i";
    4.63  by (rtac (major RS trans_induct) 1);
    4.64  by (rtac (rank RS ssubst) 1);
    4.65 -by (ASM_SIMP_TAC (ord_ss addrews [Ord_equality]) 1);
    4.66 +by (asm_simp_tac (ZF_ss addsimps [Ord_equality]) 1);
    4.67  val rank_of_Ord = result();
    4.68  
    4.69  val [prem] = goal Epsilon.thy "a:b ==> rank(a) : rank(b)";
     5.1 --- a/src/ZF/List.ML	Fri Sep 17 12:53:53 1993 +0200
     5.2 +++ b/src/ZF/List.ML	Fri Sep 17 16:16:38 1993 +0200
     5.3 @@ -62,7 +62,7 @@
     5.4  \       !!x y. [| x: A;  y: list(A) |] ==> h(x,y): C(<x,y>)  \
     5.5  \    |] ==> list_case(l,c,h) : C(l)";
     5.6  by (rtac (major RS list_induct) 1);
     5.7 -by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
     5.8 +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
     5.9  			    ([list_case_0,list_case_Pair]@prems))));
    5.10  val list_case_type = result();
    5.11  ****)
    5.12 @@ -71,10 +71,10 @@
    5.13  (** For recursion **)
    5.14  
    5.15  goalw List.thy List.con_defs "rank(a) : rank(Cons(a,l))";
    5.16 -by (SIMP_TAC rank_ss 1);
    5.17 +by (simp_tac rank_ss 1);
    5.18  val rank_Cons1 = result();
    5.19  
    5.20  goalw List.thy List.con_defs "rank(l) : rank(Cons(a,l))";
    5.21 -by (SIMP_TAC rank_ss 1);
    5.22 +by (simp_tac rank_ss 1);
    5.23  val rank_Cons2 = result();
    5.24  
     6.1 --- a/src/ZF/ListFn.ML	Fri Sep 17 12:53:53 1993 +0200
     6.2 +++ b/src/ZF/ListFn.ML	Fri Sep 17 16:16:38 1993 +0200
     6.3 @@ -11,19 +11,14 @@
     6.4  
     6.5  (** list_rec -- by Vset recursion **)
     6.6  
     6.7 -(*Used to verify list_rec*)
     6.8 -val list_rec_ss = ZF_ss 
     6.9 -      addcongs (mk_typed_congs ListFn.thy [("h", "[i,i,i]=>i")])
    6.10 -      addrews List.case_eqns;
    6.11 -
    6.12  goal ListFn.thy "list_rec(Nil,c,h) = c";
    6.13  by (rtac (list_rec_def RS def_Vrec RS trans) 1);
    6.14 -by (SIMP_TAC list_rec_ss 1);
    6.15 +by (simp_tac (ZF_ss addsimps List.case_eqns) 1);
    6.16  val list_rec_Nil = result();
    6.17  
    6.18  goal ListFn.thy "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))";
    6.19  by (rtac (list_rec_def RS def_Vrec RS trans) 1);
    6.20 -by (SIMP_TAC (list_rec_ss addrews [Vset_rankI, rank_Cons2]) 1);
    6.21 +by (simp_tac (ZF_ss addsimps (List.case_eqns @ [Vset_rankI, rank_Cons2])) 1);
    6.22  val list_rec_Cons = result();
    6.23  
    6.24  (*Type checking -- proved by induction, as usual*)
    6.25 @@ -33,8 +28,8 @@
    6.26  \       !!x y r. [| x:A;  y: list(A);  r: C(y) |] ==> h(x,y,r): C(Cons(x,y))  \
    6.27  \    |] ==> list_rec(l,c,h) : C(l)";
    6.28  by (list_ind_tac "l" prems 1);
    6.29 -by (ALLGOALS (ASM_SIMP_TAC
    6.30 -	      (ZF_ss addrews (prems@[list_rec_Nil,list_rec_Cons]))));
    6.31 +by (ALLGOALS (asm_simp_tac
    6.32 +	      (ZF_ss addsimps (prems@[list_rec_Nil,list_rec_Cons]))));
    6.33  val list_rec_type = result();
    6.34  
    6.35  (** Versions for use with definitions **)
    6.36 @@ -122,47 +117,42 @@
    6.37         map_type, map_type2, app_type, length_type, rev_type, flat_type,
    6.38         list_add_type];
    6.39  
    6.40 -val list_congs = 
    6.41 -    List.congs @ 
    6.42 -    mk_congs ListFn.thy
    6.43 -        ["list_rec","map","op @","length","rev","flat","list_add"];
    6.44 -
    6.45  val list_ss = arith_ss 
    6.46 -    addcongs list_congs
    6.47 -    addrews List.case_eqns
    6.48 -    addrews list_typechecks
    6.49 -    addrews [list_rec_Nil, list_rec_Cons, 
    6.50 +    addsimps List.case_eqns
    6.51 +    addsimps [list_rec_Nil, list_rec_Cons, 
    6.52  	     map_Nil, map_Cons,
    6.53  	     app_Nil, app_Cons,
    6.54  	     length_Nil, length_Cons,
    6.55  	     rev_Nil, rev_Cons,
    6.56  	     flat_Nil, flat_Cons,
    6.57 -	     list_add_Nil, list_add_Cons];
    6.58 +	     list_add_Nil, list_add_Cons]
    6.59 +    setsolver (type_auto_tac list_typechecks);
    6.60 +(*Could also rewrite using the list_typechecks...*)
    6.61  
    6.62  (*** theorems about map ***)
    6.63  
    6.64  val prems = goal ListFn.thy
    6.65      "l: list(A) ==> map(%u.u, l) = l";
    6.66  by (list_ind_tac "l" prems 1);
    6.67 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
    6.68 +by (ALLGOALS (asm_simp_tac list_ss));
    6.69  val map_ident = result();
    6.70  
    6.71  val prems = goal ListFn.thy
    6.72      "l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)";
    6.73  by (list_ind_tac "l" prems 1);
    6.74 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
    6.75 +by (ALLGOALS (asm_simp_tac list_ss));
    6.76  val map_compose = result();
    6.77  
    6.78  val prems = goal ListFn.thy
    6.79      "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
    6.80  by (list_ind_tac "xs" prems 1);
    6.81 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
    6.82 +by (ALLGOALS (asm_simp_tac list_ss));
    6.83  val map_app_distrib = result();
    6.84  
    6.85  val prems = goal ListFn.thy
    6.86      "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";
    6.87  by (list_ind_tac "ls" prems 1);
    6.88 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [map_app_distrib])));
    6.89 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib])));
    6.90  val map_flat = result();
    6.91  
    6.92  val prems = goal ListFn.thy
    6.93 @@ -170,9 +160,7 @@
    6.94  \    list_rec(map(h,l), c, d) = \
    6.95  \    list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))";
    6.96  by (list_ind_tac "l" prems 1);
    6.97 -by (ALLGOALS 
    6.98 -    (ASM_SIMP_TAC 
    6.99 -     (list_ss addcongs (mk_typed_congs ListFn.thy [("d", "[i,i,i]=>i")]))));
   6.100 +by (ALLGOALS (asm_simp_tac list_ss));
   6.101  val list_rec_map = result();
   6.102  
   6.103  (** theorems about list(Collect(A,P)) -- used in ex/term.ML **)
   6.104 @@ -183,7 +171,7 @@
   6.105  val prems = goal ListFn.thy
   6.106      "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
   6.107  by (list_ind_tac "l" prems 1);
   6.108 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
   6.109 +by (ALLGOALS (asm_simp_tac list_ss));
   6.110  val map_list_Collect = result();
   6.111  
   6.112  (*** theorems about length ***)
   6.113 @@ -191,13 +179,13 @@
   6.114  val prems = goal ListFn.thy
   6.115      "xs: list(A) ==> length(map(h,xs)) = length(xs)";
   6.116  by (list_ind_tac "xs" prems 1);
   6.117 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
   6.118 +by (ALLGOALS (asm_simp_tac list_ss));
   6.119  val length_map = result();
   6.120  
   6.121  val prems = goal ListFn.thy
   6.122      "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
   6.123  by (list_ind_tac "xs" prems 1);
   6.124 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
   6.125 +by (ALLGOALS (asm_simp_tac list_ss));
   6.126  val length_app = result();
   6.127  
   6.128  (* [| m: nat; n: nat |] ==> m #+ succ(n) = succ(n) #+ m 
   6.129 @@ -207,60 +195,59 @@
   6.130  val prems = goal ListFn.thy
   6.131      "xs: list(A) ==> length(rev(xs)) = length(xs)";
   6.132  by (list_ind_tac "xs" prems 1);
   6.133 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [length_app, add_commute_succ])));
   6.134 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app, add_commute_succ])));
   6.135  val length_rev = result();
   6.136  
   6.137  val prems = goal ListFn.thy
   6.138      "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
   6.139  by (list_ind_tac "ls" prems 1);
   6.140 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [length_app])));
   6.141 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app])));
   6.142  val length_flat = result();
   6.143  
   6.144  (*** theorems about app ***)
   6.145  
   6.146  val [major] = goal ListFn.thy "xs: list(A) ==> xs@Nil=xs";
   6.147  by (rtac (major RS List.induct) 1);
   6.148 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
   6.149 +by (ALLGOALS (asm_simp_tac list_ss));
   6.150  val app_right_Nil = result();
   6.151  
   6.152  val prems = goal ListFn.thy "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
   6.153  by (list_ind_tac "xs" prems 1);
   6.154 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
   6.155 +by (ALLGOALS (asm_simp_tac list_ss));
   6.156  val app_assoc = result();
   6.157  
   6.158  val prems = goal ListFn.thy
   6.159      "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
   6.160  by (list_ind_tac "ls" prems 1);
   6.161 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [app_assoc])));
   6.162 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_assoc])));
   6.163  val flat_app_distrib = result();
   6.164  
   6.165  (*** theorems about rev ***)
   6.166  
   6.167  val prems = goal ListFn.thy "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
   6.168  by (list_ind_tac "l" prems 1);
   6.169 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [map_app_distrib])));
   6.170 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib])));
   6.171  val rev_map_distrib = result();
   6.172  
   6.173  (*Simplifier needs the premises as assumptions because rewriting will not
   6.174    instantiate the variable ?A in the rules' typing conditions; note that
   6.175    rev_type does not instantiate ?A.  Only the premises do.
   6.176  *)
   6.177 -val prems = goal ListFn.thy
   6.178 -    "[| xs: list(A);  ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
   6.179 -by (cut_facts_tac prems 1);
   6.180 +goal ListFn.thy
   6.181 +    "!!xs. [| xs: list(A);  ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
   6.182  by (etac List.induct 1);
   6.183 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [app_right_Nil,app_assoc])));
   6.184 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_right_Nil,app_assoc])));
   6.185  val rev_app_distrib = result();
   6.186  
   6.187  val prems = goal ListFn.thy "l: list(A) ==> rev(rev(l))=l";
   6.188  by (list_ind_tac "l" prems 1);
   6.189 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [rev_app_distrib])));
   6.190 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [rev_app_distrib])));
   6.191  val rev_rev_ident = result();
   6.192  
   6.193  val prems = goal ListFn.thy
   6.194      "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
   6.195  by (list_ind_tac "ls" prems 1);
   6.196 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews 
   6.197 +by (ALLGOALS (asm_simp_tac (list_ss addsimps 
   6.198         [map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil])));
   6.199  val rev_flat = result();
   6.200  
   6.201 @@ -273,22 +260,22 @@
   6.202  by (cut_facts_tac prems 1);
   6.203  by (list_ind_tac "xs" prems 1);
   6.204  by (ALLGOALS 
   6.205 -    (ASM_SIMP_TAC (list_ss addrews [add_0_right, add_assoc RS sym])));
   6.206 -by (resolve_tac arith_congs 1);
   6.207 -by (REPEAT (ares_tac [refl, list_add_type, add_commute] 1));
   6.208 +    (asm_simp_tac (list_ss addsimps [add_0_right, add_assoc RS sym])));
   6.209 +by (rtac (add_commute RS subst_context) 1);
   6.210 +by (REPEAT (ares_tac [refl, list_add_type] 1));
   6.211  val list_add_app = result();
   6.212  
   6.213  val prems = goal ListFn.thy
   6.214      "l: list(nat) ==> list_add(rev(l)) = list_add(l)";
   6.215  by (list_ind_tac "l" prems 1);
   6.216  by (ALLGOALS
   6.217 -    (ASM_SIMP_TAC (list_ss addrews [list_add_app, add_0_right])));
   6.218 +    (asm_simp_tac (list_ss addsimps [list_add_app, add_0_right])));
   6.219  val list_add_rev = result();
   6.220  
   6.221  val prems = goal ListFn.thy
   6.222      "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
   6.223  by (list_ind_tac "ls" prems 1);
   6.224 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [list_add_app])));
   6.225 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [list_add_app])));
   6.226  by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1));
   6.227  val list_add_flat = result();
   6.228  
   6.229 @@ -301,6 +288,6 @@
   6.230  \    |] ==> P(l)";
   6.231  by (rtac (major RS rev_rev_ident RS subst) 1);
   6.232  by (rtac (major RS rev_type RS List.induct) 1);
   6.233 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews prems)));
   6.234 +by (ALLGOALS (asm_simp_tac (list_ss addsimps prems)));
   6.235  val list_append_induct = result();
   6.236  
     7.1 --- a/src/ZF/Nat.ML	Fri Sep 17 12:53:53 1993 +0200
     7.2 +++ b/src/ZF/Nat.ML	Fri Sep 17 16:16:38 1993 +0200
     7.3 @@ -95,8 +95,8 @@
     7.4  \    |] ==> m <= n --> P(m) --> P(n)";
     7.5  by (nat_ind_tac "n" prems 1);
     7.6  by (ALLGOALS
     7.7 -    (ASM_SIMP_TAC
     7.8 -     (ZF_ss addrews (prems@distrib_rews@[subset_empty_iff, subset_succ_iff, 
     7.9 +    (asm_simp_tac
    7.10 +     (ZF_ss addsimps (prems@distrib_rews@[subset_empty_iff, subset_succ_iff, 
    7.11  					 Ord_nat RS Ord_in_Ord]))));
    7.12  val nat_induct_from_lemma = result();
    7.13  
    7.14 @@ -127,17 +127,17 @@
    7.15  
    7.16  (** nat_case **)
    7.17  
    7.18 -goalw Nat.thy [nat_case_def] "nat_case(0,a,b) = a";
    7.19 +goalw Nat.thy [nat_case_def] "nat_case(a,b,0) = a";
    7.20  by (fast_tac (ZF_cs addIs [the_equality]) 1);
    7.21  val nat_case_0 = result();
    7.22  
    7.23 -goalw Nat.thy [nat_case_def] "nat_case(succ(m),a,b) = b(m)";
    7.24 +goalw Nat.thy [nat_case_def] "nat_case(a,b,succ(m)) = b(m)";
    7.25  by (fast_tac (ZF_cs addIs [the_equality]) 1);
    7.26  val nat_case_succ = result();
    7.27  
    7.28  val major::prems = goal Nat.thy
    7.29      "[| n: nat;  a: C(0);  !!m. m: nat ==> b(m): C(succ(m))  \
    7.30 -\    |] ==> nat_case(n,a,b) : C(n)";
    7.31 +\    |] ==> nat_case(a,b,n) : C(n)";
    7.32  by (rtac (major RS nat_induct) 1);
    7.33  by (REPEAT (resolve_tac [nat_case_0 RS ssubst,
    7.34  			 nat_case_succ RS ssubst] 1 
    7.35 @@ -145,13 +145,6 @@
    7.36  by (assume_tac 1);
    7.37  val nat_case_type = result();
    7.38  
    7.39 -val prems = goalw Nat.thy [nat_case_def]
    7.40 -    "[| n=n';  a=a';  !!m z. b(m)=b'(m)  \
    7.41 -\    |] ==> nat_case(n,a,b)=nat_case(n',a',b')";
    7.42 -by (REPEAT (resolve_tac [the_cong,disj_cong,ex_cong] 1
    7.43 -     ORELSE EVERY1 (map rtac ((prems RL [ssubst]) @ [iff_refl]))));
    7.44 -val nat_case_cong = result();
    7.45 -
    7.46  
    7.47  (** nat_rec -- used to define eclose and transrec, then obsolete **)
    7.48  
    7.49 @@ -165,11 +158,10 @@
    7.50  val [prem] = goal Nat.thy 
    7.51      "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))";
    7.52  val nat_rec_ss = ZF_ss 
    7.53 -      addcongs (mk_typed_congs Nat.thy [("b", "[i,i]=>i")])
    7.54 -      addrews [prem, nat_case_succ, nat_succI, Memrel_iff, 
    7.55 -	       vimage_singleton_iff];
    7.56 +      addsimps [prem, nat_case_succ, nat_succI, Memrel_iff, 
    7.57 +		vimage_singleton_iff];
    7.58  by (rtac nat_rec_trans 1);
    7.59 -by (SIMP_TAC nat_rec_ss 1);
    7.60 +by (simp_tac nat_rec_ss 1);
    7.61  val nat_rec_succ = result();
    7.62  
    7.63  (** The union of two natural numbers is a natural number -- their maximum **)
     8.1 --- a/src/ZF/Nat.thy	Fri Sep 17 12:53:53 1993 +0200
     8.2 +++ b/src/ZF/Nat.thy	Fri Sep 17 16:16:38 1993 +0200
     8.3 @@ -9,7 +9,7 @@
     8.4  Nat = Ord + Bool + 
     8.5  consts
     8.6      nat 	::      "i"
     8.7 -    nat_case    ::      "[i, i, i=>i]=>i"
     8.8 +    nat_case    ::      "[i, i=>i, i]=>i"
     8.9      nat_rec     ::      "[i, i, [i,i]=>i]=>i"
    8.10  
    8.11  rules
    8.12 @@ -17,10 +17,10 @@
    8.13      nat_def     "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})"
    8.14  
    8.15      nat_case_def
    8.16 -	"nat_case(k,a,b) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
    8.17 +	"nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
    8.18  
    8.19      nat_rec_def
    8.20  	"nat_rec(k,a,b) ==   \
    8.21 -\   	  wfrec(Memrel(nat), k, %n f. nat_case(n, a, %m. b(m, f`m)))"
    8.22 +\   	  wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
    8.23  
    8.24  end
     9.1 --- a/src/ZF/Ord.ML	Fri Sep 17 12:53:53 1993 +0200
     9.2 +++ b/src/ZF/Ord.ML	Fri Sep 17 16:16:38 1993 +0200
     9.3 @@ -318,7 +318,7 @@
     9.4  
     9.5  goal Ord.thy
     9.6      "!!i j. [| Ord(i);  Ord(j) |] ==> i<=succ(j) <-> i<=j | i=succ(j)";
     9.7 -by (ASM_SIMP_TAC (ZF_ss addrews [member_succ_iff RS iff_sym, Ord_succ]) 1);
     9.8 +by (asm_simp_tac (ZF_ss addsimps [member_succ_iff RS iff_sym, Ord_succ]) 1);
     9.9  by (fast_tac ZF_cs 1);
    9.10  val subset_succ_iff = result();
    9.11  
    9.12 @@ -356,17 +356,17 @@
    9.13  goal Ord.thy "!!i j k. [| i:k;  j:k;  Ord(k) |] ==> i Un j : k";
    9.14  by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);
    9.15  by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
    9.16 -by (ASM_SIMP_TAC (ZF_ss addrews [subset_Un_iff RS iffD1]) 1);
    9.17 +by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1);
    9.18  by (rtac (Un_commute RS ssubst) 1);
    9.19 -by (ASM_SIMP_TAC (ZF_ss addrews [subset_Un_iff RS iffD1]) 1);
    9.20 +by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1);
    9.21  val Ord_member_UnI = result();
    9.22  
    9.23  goal Ord.thy "!!i j k. [| i:k;  j:k;  Ord(k) |] ==> i Int j : k";
    9.24  by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);
    9.25  by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
    9.26 -by (ASM_SIMP_TAC (ZF_ss addrews [subset_Int_iff RS iffD1]) 1);
    9.27 +by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1);
    9.28  by (rtac (Int_commute RS ssubst) 1);
    9.29 -by (ASM_SIMP_TAC (ZF_ss addrews [subset_Int_iff RS iffD1]) 1);
    9.30 +by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1);
    9.31  val Ord_member_IntI = result();
    9.32  
    9.33  
    10.1 --- a/src/ZF/Pair.ML	Fri Sep 17 12:53:53 1993 +0200
    10.2 +++ b/src/ZF/Pair.ML	Fri Sep 17 16:16:38 1993 +0200
    10.3 @@ -15,7 +15,7 @@
    10.4  
    10.5  val Pair_iff = prove_goalw ZF.thy [Pair_def]
    10.6      "<a,b> = <c,d> <-> a=c & b=d"
    10.7 - (fn _=> [ (SIMP_TAC (FOL_ss addrews [doubleton_iff]) 1),
    10.8 + (fn _=> [ (simp_tac (FOL_ss addsimps [doubleton_iff]) 1),
    10.9             (fast_tac FOL_cs 1) ]);
   10.10  
   10.11  val Pair_inject = standard (Pair_iff RS iffD1 RS conjE);
   10.12 @@ -89,7 +89,7 @@
   10.13  val Sigma_cong = prove_goalw ZF.thy [Sigma_def]
   10.14      "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \
   10.15  \    Sigma(A,B) = Sigma(A',B')"
   10.16 - (fn prems=> [ (prove_cong_tac (prems@[RepFun_cong]) 1) ]);
   10.17 + (fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1) ]);
   10.18  
   10.19  val Sigma_empty1 = prove_goal ZF.thy "Sigma(0,B) = 0"
   10.20   (fn _ => [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [SigmaE]) 1) ]);
   10.21 @@ -114,13 +114,6 @@
   10.22      (etac ssubst 1),
   10.23      (REPEAT (ares_tac (prems @ [split RS ssubst]) 1)) ]);
   10.24  
   10.25 -(*This congruence rule uses NO typing information...*)
   10.26 -val split_cong = prove_goalw ZF.thy [split_def] 
   10.27 -    "[| p=p';  !!x y.c(x,y) = c'(x,y) |] ==> \
   10.28 -\    split(%x y.c(x,y), p) = split(%x y.c'(x,y), p')"
   10.29 - (fn prems=> [ (prove_cong_tac (prems@[the_cong]) 1) ]);
   10.30 -
   10.31 -
   10.32  (*** conversions for fst and snd ***)
   10.33  
   10.34  val fst_conv = prove_goalw ZF.thy [fst_def] "fst(<a,b>) = a"
    11.1 --- a/src/ZF/Perm.ML	Fri Sep 17 12:53:53 1993 +0200
    11.2 +++ b/src/ZF/Perm.ML	Fri Sep 17 16:16:38 1993 +0200
    11.3 @@ -52,6 +52,7 @@
    11.4  (* f: bij(A,B) ==> f: A->B *)
    11.5  val bij_is_fun = standard (bij_is_inj RS inj_is_fun);
    11.6  
    11.7 +
    11.8  (** Identity function **)
    11.9  
   11.10  val [prem] = goalw Perm.thy [id_def] "a:A ==> <a,a> : id(A)";  
   11.11 @@ -76,7 +77,7 @@
   11.12  
   11.13  goalw Perm.thy [inj_def,id_def] "id(A): inj(A,A)";
   11.14  by (REPEAT (ares_tac [CollectI,lam_type] 1));
   11.15 -by (SIMP_TAC ZF_ss 1);
   11.16 +by (simp_tac ZF_ss 1);
   11.17  val id_inj = result();
   11.18  
   11.19  goalw Perm.thy [id_def,surj_def] "id(A): surj(A,A)";
   11.20 @@ -262,7 +263,7 @@
   11.21      "!!f g. [| (f O g): inj(A,C);  g: A->B;  f: B->C |] ==> g: inj(A,B)";
   11.22  by (safe_tac comp_cs);
   11.23  by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
   11.24 -by (ASM_SIMP_TAC (ZF_ss addrews [comp_func_apply]) 1);
   11.25 +by (asm_simp_tac (FOL_ss addsimps [comp_func_apply]) 1);
   11.26  val comp_mem_injD1 = result();
   11.27  
   11.28  goalw Perm.thy [inj_def,surj_def]
   11.29 @@ -271,9 +272,10 @@
   11.30  by (res_inst_tac [("x1", "x")] (bspec RS bexE) 1);
   11.31  by (eres_inst_tac [("x1", "w")] (bspec RS bexE) 3);
   11.32  by (REPEAT (assume_tac 1));
   11.33 -by (safe_tac (comp_cs addSIs ZF_congs));
   11.34 +by (safe_tac comp_cs);
   11.35 +by (res_inst_tac [("t", "op `(g)")] subst_context 1);
   11.36  by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
   11.37 -by (ASM_SIMP_TAC (ZF_ss addrews [comp_func_apply]) 1);
   11.38 +by (asm_simp_tac (FOL_ss addsimps [comp_func_apply]) 1);
   11.39  val comp_mem_injD2 = result();
   11.40  
   11.41  goalw Perm.thy [surj_def]
   11.42 @@ -427,7 +429,9 @@
   11.43  by (etac fun_extend 1);
   11.44  by (REPEAT (ares_tac [ballI] 1));
   11.45  by (REPEAT_FIRST (eresolve_tac [consE,ssubst]));
   11.46 -(*Assumption ALL w:A. ALL x:A. f`w = f`x --> w=x makes ASM_SIMP_TAC loop!*)
   11.47 -by (ALLGOALS (SIMP_TAC (ZF_ss addrews [fun_extend_apply2,fun_extend_apply1])));
   11.48 +(*Assumption ALL w:A. ALL x:A. f`w = f`x --> w=x would make asm_simp_tac loop
   11.49 +  using ZF_ss!  But FOL_ss ignores the assumption...*)
   11.50 +by (ALLGOALS (asm_simp_tac 
   11.51 +	      (FOL_ss addsimps [fun_extend_apply2,fun_extend_apply1])));
   11.52  by (ALLGOALS (fast_tac (ZF_cs addIs [apply_type])));
   11.53  val inj_extend = result();
    12.1 --- a/src/ZF/QPair.ML	Fri Sep 17 12:53:53 1993 +0200
    12.2 +++ b/src/ZF/QPair.ML	Fri Sep 17 16:16:38 1993 +0200
    12.3 @@ -74,7 +74,7 @@
    12.4  val QSigma_cong = prove_goalw QPair.thy [QSigma_def]
    12.5      "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \
    12.6  \    QSigma(A,B) = QSigma(A',B')"
    12.7 - (fn prems=> [ (prove_cong_tac (prems@[RepFun_cong]) 1) ]);
    12.8 + (fn prems=> [ (simp_tac (ZF_ss addsimps prems) 1) ]);
    12.9  
   12.10  val QSigma_empty1 = prove_goal QPair.thy "QSigma(0,B) = 0"
   12.11   (fn _ => [ (fast_tac (ZF_cs addIs [equalityI] addSEs [QSigmaE]) 1) ]);
   12.12 @@ -98,12 +98,6 @@
   12.13      (etac ssubst 1),
   12.14      (REPEAT (ares_tac (prems @ [qsplit RS ssubst]) 1)) ]);
   12.15  
   12.16 -(*This congruence rule uses NO typing information...*)
   12.17 -val qsplit_cong = prove_goalw QPair.thy [qsplit_def] 
   12.18 -    "[| p=p';  !!x y.c(x,y) = c'(x,y) |] ==> \
   12.19 -\    qsplit(%x y.c(x,y), p) = qsplit(%x y.c'(x,y), p')"
   12.20 - (fn prems=> [ (prove_cong_tac (prems@[the_cong]) 1) ]);
   12.21 -
   12.22  
   12.23  val qpair_cs = ZF_cs addSIs [QSigmaI] addSEs [QSigmaE2, QSigmaE, QPair_inject];
   12.24  
   12.25 @@ -243,7 +237,7 @@
   12.26  val qsum_subset_iff = result();
   12.27  
   12.28  goal QPair.thy "A <+> B = C <+> D <-> A=C & B=D";
   12.29 -by (SIMP_TAC (ZF_ss addrews [extension,qsum_subset_iff]) 1);
   12.30 +by (simp_tac (ZF_ss addsimps [extension,qsum_subset_iff]) 1);
   12.31  by (fast_tac ZF_cs 1);
   12.32  val qsum_equal_iff = result();
   12.33  
   12.34 @@ -259,12 +253,6 @@
   12.35  by (rtac cond_1 1);
   12.36  val qcase_QInr = result();
   12.37  
   12.38 -val prems = goalw QPair.thy [qcase_def]
   12.39 -    "[| u=u'; !!x. c(x)=c'(x);  !!y. d(y)=d'(y) |] ==>    \
   12.40 -\    qcase(c,d,u)=qcase(c',d',u')";
   12.41 -by (REPEAT (resolve_tac ([refl,qsplit_cong,cond_cong] @ prems) 1));
   12.42 -val qcase_cong = result();
   12.43 -
   12.44  val major::prems = goal QPair.thy
   12.45      "[| u: A <+> B; \
   12.46  \       !!x. x: A ==> c(x): C(QInl(x));   \
   12.47 @@ -272,7 +260,7 @@
   12.48  \    |] ==> qcase(c,d,u) : C(u)";
   12.49  by (rtac (major RS qsumE) 1);
   12.50  by (ALLGOALS (etac ssubst));
   12.51 -by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
   12.52 +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
   12.53  			    (prems@[qcase_QInl,qcase_QInr]))));
   12.54  val qcase_type = result();
   12.55  
    13.1 --- a/src/ZF/QUniv.ML	Fri Sep 17 12:53:53 1993 +0200
    13.2 +++ b/src/ZF/QUniv.ML	Fri Sep 17 16:16:38 1993 +0200
    13.3 @@ -205,7 +205,7 @@
    13.4  
    13.5  goalw QUniv.thy [QPair_def,sum_def]
    13.6      "<a;b> Int quniv(A) = <a;b> Int univ(eclose(A))";
    13.7 -by (SIMP_TAC (ZF_ss addrews [Int_Un_distrib, product_Int_quniv_eq]) 1);
    13.8 +by (simp_tac (ZF_ss addsimps [Int_Un_distrib, product_Int_quniv_eq]) 1);
    13.9  val QPair_Int_quniv_eq = result();
   13.10  
   13.11  (**** "Take-lemma" rules for proving c: quniv(A) ****)
    14.1 --- a/src/ZF/ROOT.ML	Fri Sep 17 12:53:53 1993 +0200
    14.2 +++ b/src/ZF/ROOT.ML	Fri Sep 17 16:16:38 1993 +0200
    14.3 @@ -1,4 +1,5 @@
    14.4  (*  Title: 	ZF/ROOT
    14.5 +    ID:         $Id$
    14.6      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    14.7      Copyright   1993  University of Cambridge
    14.8  
    15.1 --- a/src/ZF/Sum.ML	Fri Sep 17 12:53:53 1993 +0200
    15.2 +++ b/src/ZF/Sum.ML	Fri Sep 17 16:16:38 1993 +0200
    15.3 @@ -83,7 +83,7 @@
    15.4  val sum_subset_iff = result();
    15.5  
    15.6  goal Sum.thy "A+B = C+D <-> A=C & B=D";
    15.7 -by (SIMP_TAC (ZF_ss addrews [extension,sum_subset_iff]) 1);
    15.8 +by (simp_tac (ZF_ss addsimps [extension,sum_subset_iff]) 1);
    15.9  by (fast_tac ZF_cs 1);
   15.10  val sum_equal_iff = result();
   15.11  
   15.12 @@ -99,12 +99,6 @@
   15.13  by (rtac cond_1 1);
   15.14  val case_Inr = result();
   15.15  
   15.16 -val prems = goalw Sum.thy [case_def]
   15.17 -    "[| u=u'; !!x. c(x)=c'(x);  !!y. d(y)=d'(y) |] ==>    \
   15.18 -\    case(c,d,u)=case(c',d',u')";
   15.19 -by (REPEAT (resolve_tac ([refl,split_cong,cond_cong] @ prems) 1));
   15.20 -val case_cong = result();
   15.21 -
   15.22  val major::prems = goal Sum.thy
   15.23      "[| u: A+B; \
   15.24  \       !!x. x: A ==> c(x): C(Inl(x));   \
   15.25 @@ -112,7 +106,7 @@
   15.26  \    |] ==> case(c,d,u) : C(u)";
   15.27  by (rtac (major RS sumE) 1);
   15.28  by (ALLGOALS (etac ssubst));
   15.29 -by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
   15.30 +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
   15.31  			    (prems@[case_Inl,case_Inr]))));
   15.32  val case_type = result();
   15.33  
    16.1 --- a/src/ZF/Univ.ML	Fri Sep 17 12:53:53 1993 +0200
    16.2 +++ b/src/ZF/Univ.ML	Fri Sep 17 16:16:38 1993 +0200
    16.3 @@ -11,7 +11,7 @@
    16.4  (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
    16.5  goal Univ.thy "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))";
    16.6  by (rtac (Vfrom_def RS def_transrec RS ssubst) 1);
    16.7 -by (SIMP_TAC ZF_ss 1);
    16.8 +by (simp_tac ZF_ss 1);
    16.9  val Vfrom = result();
   16.10  
   16.11  (** Monotonicity **)
   16.12 @@ -122,9 +122,8 @@
   16.13  
   16.14  goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
   16.15  by (rtac (Vfrom RS trans) 1);
   16.16 -brs ([refl] RL ZF_congs) 1;
   16.17 -by (rtac equalityI 1);
   16.18 -by (rtac (succI1 RS RepFunI RS Union_upper) 2);
   16.19 +by (rtac (succI1 RS RepFunI RS Union_upper RSN
   16.20 +	      (2, equalityI RS subst_context)) 1);
   16.21  by (rtac UN_least 1);
   16.22  by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1);
   16.23  by (etac member_succD 1);
   16.24 @@ -473,16 +472,16 @@
   16.25  val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [rank_trans]));
   16.26  
   16.27  val rank_ss = ZF_ss 
   16.28 -    addrews [split, case_Inl, case_Inr, Vset_rankI]
   16.29 -    addrews rank_trans_rls;
   16.30 +    addsimps [case_Inl, case_Inr, Vset_rankI]
   16.31 +    addsimps rank_trans_rls;
   16.32  
   16.33  (** Recursion over Vset levels! **)
   16.34  
   16.35  (*NOT SUITABLE FOR REWRITING: recursive!*)
   16.36  goalw Univ.thy [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))";
   16.37  by (rtac (transrec RS ssubst) 1);
   16.38 -by (SIMP_TAC (wf_ss addrews [Ord_rank, Ord_succ, Vset_D RS beta, 
   16.39 -			     VsetI RS beta]) 1);
   16.40 +by (simp_tac (ZF_ss addsimps [Ord_rank, Ord_succ, Vset_D RS beta, 
   16.41 +			      VsetI RS beta]) 1);
   16.42  val Vrec = result();
   16.43  
   16.44  (*This form avoids giant explosions in proofs.  NOTE USE OF == *)
   16.45 @@ -493,13 +492,6 @@
   16.46  by (rtac Vrec 1);
   16.47  val def_Vrec = result();
   16.48  
   16.49 -val prems = goalw Univ.thy [Vrec_def]
   16.50 -    "[| a=a';  !!x u. H(x,u)=H'(x,u) |]  ==> Vrec(a,H)=Vrec(a',H')";
   16.51 -val Vrec_ss = ZF_ss addcongs ([transrec_cong] @ mk_congs Univ.thy ["rank"])
   16.52 -		      addrews (prems RL [sym]);
   16.53 -by (SIMP_TAC Vrec_ss 1);
   16.54 -val Vrec_cong = result();
   16.55 -
   16.56  
   16.57  (*** univ(A) ***)
   16.58  
    17.1 --- a/src/ZF/WF.ML	Fri Sep 17 12:53:53 1993 +0200
    17.2 +++ b/src/ZF/WF.ML	Fri Sep 17 16:16:38 1993 +0200
    17.3 @@ -19,10 +19,6 @@
    17.4  
    17.5  open WF;
    17.6  
    17.7 -val [H_cong] = mk_typed_congs WF.thy[("H","[i,i]=>i")];
    17.8 -
    17.9 -val wf_ss = ZF_ss addcongs [H_cong];
   17.10 -
   17.11  
   17.12  (*** Well-founded relations ***)
   17.13  
   17.14 @@ -138,13 +134,13 @@
   17.15  (*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE
   17.16    spec RS mp  instantiates induction hypotheses*)
   17.17  fun indhyp_tac hyps =
   17.18 -    ares_tac (TrueI::hyps) ORELSE' 
   17.19 +    resolve_tac (TrueI::refl::hyps) ORELSE' 
   17.20      (cut_facts_tac hyps THEN'
   17.21         DEPTH_SOLVE_1 o (ares_tac [TrueI, ballI] ORELSE'
   17.22  		        eresolve_tac [underD, transD, spec RS mp]));
   17.23  
   17.24 -(*** NOTE! some simplifications need a different auto_tac!! ***)
   17.25 -val wf_super_ss = wf_ss setauto indhyp_tac;
   17.26 +(*** NOTE! some simplifications need a different solver!! ***)
   17.27 +val wf_super_ss = ZF_ss setsolver indhyp_tac;
   17.28  
   17.29  val prems = goalw WF.thy [is_recfun_def]
   17.30      "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |] ==> \
   17.31 @@ -153,7 +149,7 @@
   17.32  by (wf_ind_tac "x" prems 1);
   17.33  by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
   17.34  by (rewtac restrict_def);
   17.35 -by (ASM_SIMP_TAC (wf_super_ss addrews [vimage_singleton_iff]) 1);
   17.36 +by (asm_simp_tac (wf_super_ss addsimps [vimage_singleton_iff]) 1);
   17.37  val is_recfun_equal_lemma = result();
   17.38  val is_recfun_equal = standard (is_recfun_equal_lemma RS mp RS mp);
   17.39  
   17.40 @@ -165,7 +161,7 @@
   17.41  by (rtac (consI1 RS restrict_type RS fun_extension) 1);
   17.42  by (etac is_recfun_type 1);
   17.43  by (ALLGOALS
   17.44 -    (ASM_SIMP_TAC (wf_super_ss addrews
   17.45 +    (asm_simp_tac (wf_super_ss addsimps
   17.46  		   [ [wfr,transr,recf,recg] MRS is_recfun_equal ])));
   17.47  val is_recfun_cut = result();
   17.48  
   17.49 @@ -195,13 +191,13 @@
   17.50  by (REPEAT (assume_tac 2));
   17.51  by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
   17.52  (*Applying the substitution: must keep the quantified assumption!!*)
   17.53 -by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong, H_cong] 1));
   17.54 +by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong] 1));
   17.55  by (fold_tac [is_recfun_def]);
   17.56 -by (rtac (consI1 RS restrict_type RSN (2,fun_extension)) 1);
   17.57 +by (rtac (consI1 RS restrict_type RSN (2,fun_extension) RS subst_context) 1);
   17.58  by (rtac is_recfun_type 1);
   17.59  by (ALLGOALS
   17.60 -    (ASM_SIMP_TAC
   17.61 -     (wf_super_ss addrews [underI RS beta, apply_recfun, is_recfun_cut])));
   17.62 +    (asm_simp_tac
   17.63 +     (wf_super_ss addsimps [underI RS beta, apply_recfun, is_recfun_cut])));
   17.64  val unfold_the_recfun = result();
   17.65  
   17.66  
   17.67 @@ -214,13 +210,12 @@
   17.68  val the_recfun_cut = result();
   17.69  
   17.70  (*NOT SUITABLE FOR REWRITING since it is recursive!*)
   17.71 -val prems = goalw WF.thy [wftrec_def]
   17.72 -    "[| wf(r);  trans(r) |] ==> \
   17.73 -\    wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))";
   17.74 +goalw WF.thy [wftrec_def]
   17.75 +    "!!r. [| wf(r);  trans(r) |] ==> \
   17.76 +\         wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))";
   17.77  by (rtac (rewrite_rule [is_recfun_def] unfold_the_recfun RS ssubst) 1);
   17.78 -by (ALLGOALS (ASM_SIMP_TAC
   17.79 -	      (wf_ss addrews (prems@[vimage_singleton_iff RS iff_sym, 
   17.80 -				     the_recfun_cut]))));
   17.81 +by (ALLGOALS (asm_simp_tac
   17.82 +	(ZF_ss addsimps [vimage_singleton_iff RS iff_sym, the_recfun_cut])));
   17.83  val wftrec = result();
   17.84  
   17.85  (** Removal of the premise trans(r) **)
   17.86 @@ -230,8 +225,7 @@
   17.87      "wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))";
   17.88  by (rtac (wfr RS wf_trancl RS wftrec RS ssubst) 1);
   17.89  by (rtac trans_trancl 1);
   17.90 -by (rtac (refl RS H_cong) 1);
   17.91 -by (rtac (vimage_pair_mono RS restrict_lam_eq) 1);
   17.92 +by (rtac (vimage_pair_mono RS restrict_lam_eq RS subst_context) 1);
   17.93  by (etac r_into_trancl 1);
   17.94  by (rtac subset_refl 1);
   17.95  val wfrec = result();
   17.96 @@ -253,10 +247,3 @@
   17.97  by (REPEAT (ares_tac (prems@[lam_type]) 1
   17.98       ORELSE eresolve_tac [spec RS mp, underD] 1));
   17.99  val wfrec_type = result();
  17.100 -
  17.101 -val prems = goalw WF.thy [wfrec_def,wftrec_def,the_recfun_def,is_recfun_def]
  17.102 -    "[| r=r';  !!x u. H(x,u)=H'(x,u);  a=a' |] \
  17.103 -\    ==> wfrec(r,a,H)=wfrec(r',a',H')";
  17.104 -by (EVERY1 (map rtac (prems RL [subst])));
  17.105 -by (SIMP_TAC (wf_ss addrews (prems RL [sym])) 1);
  17.106 -val wfrec_cong = result();
    18.1 --- a/src/ZF/ZF.ML	Fri Sep 17 12:53:53 1993 +0200
    18.2 +++ b/src/ZF/ZF.ML	Fri Sep 17 16:16:38 1993 +0200
    18.3 @@ -13,9 +13,8 @@
    18.4    val ballE : thm
    18.5    val ballI : thm
    18.6    val ball_cong : thm
    18.7 -  val ball_rew : thm
    18.8 +  val ball_simp : thm
    18.9    val ball_tac : int -> tactic
   18.10 -  val basic_ZF_congs : thm list
   18.11    val bexCI : thm
   18.12    val bexE : thm
   18.13    val bexI : thm
   18.14 @@ -45,7 +44,6 @@
   18.15    val lemmas_cs : claset
   18.16    val PowD : thm
   18.17    val PowI : thm
   18.18 -  val prove_cong_tac : thm list -> int -> tactic
   18.19    val RepFunE : thm
   18.20    val RepFunI : thm
   18.21    val RepFun_eqI : thm
   18.22 @@ -75,14 +73,6 @@
   18.23  structure ZF_Lemmas : ZF_LEMMAS = 
   18.24  struct
   18.25  
   18.26 -val basic_ZF_congs = mk_congs ZF.thy 
   18.27 -    ["op `", "op ``", "op Int", "op Un", "op -", "op <=", "op :", 
   18.28 -     "Pow", "Union", "Inter", "fst", "snd", "succ", "Pair", "Upair", "cons",
   18.29 -     "domain", "range", "restrict"];
   18.30 -
   18.31 -fun prove_cong_tac prems i =
   18.32 -    REPEAT (ares_tac (prems@[refl]@FOL_congs@basic_ZF_congs) i);
   18.33 -
   18.34  (*** Bounded universal quantifier ***)
   18.35  
   18.36  val ballI = prove_goalw ZF.thy [Ball_def]
   18.37 @@ -118,14 +108,13 @@
   18.38  val ball_tac = dtac bspec THEN' assume_tac;
   18.39  
   18.40  (*Trival rewrite rule;   (ALL x:A.P)<->P holds only if A is nonempty!*)
   18.41 -val ball_rew = prove_goal ZF.thy "(ALL x:A. True) <-> True"
   18.42 - (fn prems=> [ (REPEAT (ares_tac [TrueI,ballI,iffI] 1)) ]);
   18.43 +val ball_simp = prove_goal ZF.thy "(ALL x:A. True) <-> True"
   18.44 + (fn _=> [ (REPEAT (ares_tac [TrueI,ballI,iffI] 1)) ]);
   18.45  
   18.46  (*Congruence rule for rewriting*)
   18.47  val ball_cong = prove_goalw ZF.thy [Ball_def]
   18.48 -    "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) \
   18.49 -\    |] ==> (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))"
   18.50 - (fn prems=> [ (prove_cong_tac prems 1) ]);
   18.51 +    "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> Ball(A,P) <-> Ball(A',P')"
   18.52 + (fn prems=> [ (simp_tac (FOL_ss addsimps prems) 1) ]);
   18.53  
   18.54  (*** Bounded existential quantifier ***)
   18.55  
   18.56 @@ -151,8 +140,8 @@
   18.57  
   18.58  val bex_cong = prove_goalw ZF.thy [Bex_def]
   18.59      "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) \
   18.60 -\    |] ==> (EX x:A. P(x)) <-> (EX x:A'. P'(x))"
   18.61 - (fn prems=> [ (prove_cong_tac prems 1) ]);
   18.62 +\    |] ==> Bex(A,P) <-> Bex(A',P')"
   18.63 + (fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ]);
   18.64  
   18.65  (*** Rules for subsets ***)
   18.66  
   18.67 @@ -265,7 +254,7 @@
   18.68  
   18.69  val Replace_cong = prove_goal ZF.thy
   18.70      "[| A=B;  !!x y. x:B ==> P(x,y) <-> Q(x,y) |] ==> \
   18.71 -\    {y. x:A, P(x,y)} = {y. x:B, Q(x,y)}"
   18.72 +\    Replace(A,P) = Replace(B,Q)"
   18.73   (fn prems=>
   18.74     let val substprems = prems RL [subst, ssubst]
   18.75         and iffprems = prems RL [iffD1,iffD2]
   18.76 @@ -275,7 +264,6 @@
   18.77  	 ORELSE (resolve_tac iffprems 1 THEN assume_tac 2))) ]
   18.78     end);
   18.79  
   18.80 -
   18.81  (*** Rules for RepFun ***)
   18.82  
   18.83  val RepFunI = prove_goalw ZF.thy [RepFun_def]
   18.84 @@ -296,9 +284,8 @@
   18.85      (REPEAT (ares_tac prems 1)) ]);
   18.86  
   18.87  val RepFun_cong = prove_goalw ZF.thy [RepFun_def]
   18.88 -    "[| A=B;  !!x. x:B ==> f(x)=g(x) |] ==> \
   18.89 -\    {f(x). x:A} = {g(x). x:B}"
   18.90 - (fn prems=> [ (prove_cong_tac (prems@[Replace_cong]) 1) ]);
   18.91 +    "[| A=B;  !!x. x:B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)"
   18.92 + (fn prems=> [ (simp_tac (FOL_ss addcongs [Replace_cong] addsimps prems) 1) ]);
   18.93  
   18.94  
   18.95  (*** Rules for Collect -- forming a subset by separation ***)
   18.96 @@ -332,9 +319,8 @@
   18.97      (assume_tac 1) ]);
   18.98  
   18.99  val Collect_cong = prove_goalw ZF.thy [Collect_def] 
  18.100 -    "[| A=B;  !!x. x:B ==> P(x) <-> Q(x) |] ==> \
  18.101 -\    {x:A. P(x)} = {x:B. Q(x)}"
  18.102 - (fn prems=> [ (prove_cong_tac (prems@[Replace_cong]) 1) ]);
  18.103 +    "[| A=B;  !!x. x:B ==> P(x) <-> Q(x) |] ==> Collect(A,P) = Collect(B,Q)"
  18.104 + (fn prems=> [ (simp_tac (FOL_ss addcongs [Replace_cong] addsimps prems) 1) ]);
  18.105  
  18.106  (*** Rules for Unions ***)
  18.107  
    19.1 --- a/src/ZF/arith.ML	Fri Sep 17 12:53:53 1993 +0200
    19.2 +++ b/src/ZF/arith.ML	Fri Sep 17 16:16:38 1993 +0200
    19.3 @@ -29,10 +29,9 @@
    19.4  
    19.5  goal Arith.thy "rec(succ(m),a,b) = b(m, rec(m,a,b))";
    19.6  val rec_ss = ZF_ss 
    19.7 -      addcongs (mk_typed_congs Arith.thy [("b", "[i,i]=>i")])
    19.8 -      addrews [nat_case_succ, nat_succI];
    19.9 +      addsimps [nat_case_succ, nat_succI];
   19.10  by (rtac rec_trans 1);
   19.11 -by (SIMP_TAC rec_ss 1);
   19.12 +by (simp_tac rec_ss 1);
   19.13  val rec_succ = result();
   19.14  
   19.15  val major::prems = goal Arith.thy
   19.16 @@ -42,20 +41,12 @@
   19.17  \    |] ==> rec(n,a,b) : C(n)";
   19.18  by (rtac (major RS nat_induct) 1);
   19.19  by (ALLGOALS
   19.20 -    (ASM_SIMP_TAC (ZF_ss addrews (prems@[rec_0,rec_succ]))));
   19.21 +    (asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ]))));
   19.22  val rec_type = result();
   19.23  
   19.24 -val prems = goalw Arith.thy [rec_def]
   19.25 -    "[| n=n';  a=a';  !!m z. b(m,z)=b'(m,z)  \
   19.26 -\    |] ==> rec(n,a,b)=rec(n',a',b')";
   19.27 -by (SIMP_TAC (ZF_ss addcongs [transrec_cong,nat_case_cong] 
   19.28 -		    addrews (prems RL [sym])) 1);
   19.29 -val rec_cong = result();
   19.30 -
   19.31  val nat_typechecks = [rec_type,nat_0I,nat_1I,nat_succI,Ord_nat];
   19.32  
   19.33 -val nat_ss = ZF_ss addcongs [nat_case_cong,rec_cong]
   19.34 -	       	   addrews ([rec_0,rec_succ] @ nat_typechecks);
   19.35 +val nat_ss = ZF_ss addsimps ([rec_0,rec_succ] @ nat_typechecks);
   19.36  
   19.37  
   19.38  (** Addition **)
   19.39 @@ -101,16 +92,16 @@
   19.40      "n:nat ==> 0 #- n = 0"
   19.41   (fn [prem]=>
   19.42    [ (rtac (prem RS nat_induct) 1),
   19.43 -    (ALLGOALS (ASM_SIMP_TAC nat_ss)) ]);
   19.44 +    (ALLGOALS (asm_simp_tac nat_ss)) ]);
   19.45  
   19.46  (*Must simplify BEFORE the induction!!  (Else we get a critical pair)
   19.47    succ(m) #- succ(n)   rewrites to   pred(succ(m) #- n)  *)
   19.48  val diff_succ_succ = prove_goalw Arith.thy [diff_def]
   19.49      "[| m:nat;  n:nat |] ==> succ(m) #- succ(n) = m #- n"
   19.50   (fn prems=>
   19.51 -  [ (ASM_SIMP_TAC (nat_ss addrews prems) 1),
   19.52 +  [ (asm_simp_tac (nat_ss addsimps prems) 1),
   19.53      (nat_ind_tac "n" prems 1),
   19.54 -    (ALLGOALS (ASM_SIMP_TAC (nat_ss addrews prems))) ]);
   19.55 +    (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
   19.56  
   19.57  val prems = goal Arith.thy 
   19.58      "[| m:nat;  n:nat |] ==> m #- n : succ(m)";
   19.59 @@ -119,8 +110,8 @@
   19.60  by (resolve_tac prems 1);
   19.61  by (etac succE 3);
   19.62  by (ALLGOALS
   19.63 -    (ASM_SIMP_TAC
   19.64 -     (nat_ss addrews (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
   19.65 +    (asm_simp_tac
   19.66 +     (nat_ss addsimps (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
   19.67  val diff_leq = result();
   19.68  
   19.69  (*** Simplification over add, mult, diff ***)
   19.70 @@ -130,10 +121,7 @@
   19.71  		  mult_0, mult_succ,
   19.72  		  diff_0, diff_0_eq_0, diff_succ_succ];
   19.73  
   19.74 -val arith_congs = mk_congs Arith.thy ["op #+", "op #-", "op #*"];
   19.75 -
   19.76 -val arith_ss = nat_ss addcongs arith_congs
   19.77 -                      addrews  (arith_rews@arith_typechecks);
   19.78 +val arith_ss = nat_ss addsimps (arith_rews@arith_typechecks);
   19.79  
   19.80  (*** Addition ***)
   19.81  
   19.82 @@ -142,7 +130,7 @@
   19.83      "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)"
   19.84   (fn prems=>
   19.85    [ (nat_ind_tac "m" prems 1),
   19.86 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
   19.87 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
   19.88  
   19.89  (*The following two lemmas are used for add_commute and sometimes
   19.90    elsewhere, since they are safe for rewriting.*)
   19.91 @@ -150,13 +138,13 @@
   19.92      "m:nat ==> m #+ 0 = m"
   19.93   (fn prems=>
   19.94    [ (nat_ind_tac "m" prems 1),
   19.95 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]); 
   19.96 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
   19.97  
   19.98  val add_succ_right = prove_goal Arith.thy
   19.99      "m:nat ==> m #+ succ(n) = succ(m #+ n)"
  19.100   (fn prems=>
  19.101    [ (nat_ind_tac "m" prems 1),
  19.102 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]); 
  19.103 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
  19.104  
  19.105  (*Commutative law for addition*)  
  19.106  val add_commute = prove_goal Arith.thy 
  19.107 @@ -164,15 +152,15 @@
  19.108   (fn prems=>
  19.109    [ (nat_ind_tac "n" prems 1),
  19.110      (ALLGOALS
  19.111 -     (ASM_SIMP_TAC
  19.112 -      (arith_ss addrews (prems@[add_0_right, add_succ_right])))) ]);
  19.113 +     (asm_simp_tac
  19.114 +      (arith_ss addsimps (prems@[add_0_right, add_succ_right])))) ]);
  19.115  
  19.116  (*Cancellation law on the left*)
  19.117  val [knat,eqn] = goal Arith.thy 
  19.118      "[| k:nat;  k #+ m = k #+ n |] ==> m=n";
  19.119  by (rtac (eqn RS rev_mp) 1);
  19.120  by (nat_ind_tac "k" [knat] 1);
  19.121 -by (ALLGOALS (SIMP_TAC arith_ss));
  19.122 +by (ALLGOALS (simp_tac arith_ss));
  19.123  by (fast_tac ZF_cs 1);
  19.124  val add_left_cancel = result();
  19.125  
  19.126 @@ -183,39 +171,40 @@
  19.127      "m:nat ==> m #* 0 = 0"
  19.128   (fn prems=>
  19.129    [ (nat_ind_tac "m" prems 1),
  19.130 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems)))  ]);
  19.131 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems)))  ]);
  19.132  
  19.133  (*right successor law for multiplication*)
  19.134  val mult_succ_right = prove_goal Arith.thy 
  19.135 -    "[| m:nat;  n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
  19.136 - (fn prems=>
  19.137 -  [ (nat_ind_tac "m" prems 1),
  19.138 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))),
  19.139 +    "!!m n. [| m:nat;  n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
  19.140 + (fn _=>
  19.141 +  [ (nat_ind_tac "m" [] 1),
  19.142 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))),
  19.143         (*The final goal requires the commutative law for addition*)
  19.144 -    (REPEAT (ares_tac (prems@[refl,add_commute]@ZF_congs@arith_congs) 1))  ]);
  19.145 +    (rtac (add_commute RS subst_context) 1),
  19.146 +    (REPEAT (assume_tac 1))  ]);
  19.147  
  19.148  (*Commutative law for multiplication*)
  19.149  val mult_commute = prove_goal Arith.thy 
  19.150      "[| m:nat;  n:nat |] ==> m #* n = n #* m"
  19.151   (fn prems=>
  19.152    [ (nat_ind_tac "m" prems 1),
  19.153 -    (ALLGOALS (ASM_SIMP_TAC
  19.154 -	       (arith_ss addrews (prems@[mult_0_right, mult_succ_right])))) ]);
  19.155 +    (ALLGOALS (asm_simp_tac
  19.156 +	     (arith_ss addsimps (prems@[mult_0_right, mult_succ_right])))) ]);
  19.157  
  19.158  (*addition distributes over multiplication*)
  19.159  val add_mult_distrib = prove_goal Arith.thy 
  19.160      "[| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
  19.161   (fn prems=>
  19.162    [ (nat_ind_tac "m" prems 1),
  19.163 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))) ]);
  19.164 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps ([add_assoc RS sym]@prems)))) ]);
  19.165  
  19.166  (*Distributive law on the left; requires an extra typing premise*)
  19.167  val add_mult_distrib_left = prove_goal Arith.thy 
  19.168      "[| m:nat;  n:nat;  k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"
  19.169   (fn prems=>
  19.170        let val mult_commute' = read_instantiate [("m","k")] mult_commute
  19.171 -          val ss = arith_ss addrews ([mult_commute',add_mult_distrib]@prems)
  19.172 -      in [ (SIMP_TAC ss 1) ]
  19.173 +          val ss = arith_ss addsimps ([mult_commute',add_mult_distrib]@prems)
  19.174 +      in [ (simp_tac ss 1) ]
  19.175        end);
  19.176  
  19.177  (*Associative law for multiplication*)
  19.178 @@ -223,7 +212,7 @@
  19.179      "[| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
  19.180   (fn prems=>
  19.181    [ (nat_ind_tac "m" prems 1),
  19.182 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews (prems@[add_mult_distrib])))) ]);
  19.183 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps (prems@[add_mult_distrib])))) ]);
  19.184  
  19.185  
  19.186  (*** Difference ***)
  19.187 @@ -232,7 +221,7 @@
  19.188      "m:nat ==> m #- m = 0"
  19.189   (fn prems=>
  19.190    [ (nat_ind_tac "m" prems 1),
  19.191 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
  19.192 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
  19.193  
  19.194  (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
  19.195  val notless::prems = goal Arith.thy
  19.196 @@ -241,8 +230,8 @@
  19.197  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
  19.198  by (resolve_tac prems 1);
  19.199  by (resolve_tac prems 1);
  19.200 -by (ALLGOALS (ASM_SIMP_TAC
  19.201 -	      (arith_ss addrews (prems@[succ_mem_succ_iff, Ord_0_mem_succ, 
  19.202 +by (ALLGOALS (asm_simp_tac
  19.203 +	      (arith_ss addsimps (prems@[succ_mem_succ_iff, Ord_0_mem_succ, 
  19.204  				  naturals_are_ordinals]))));
  19.205  val add_diff_inverse = result();
  19.206  
  19.207 @@ -251,29 +240,24 @@
  19.208  val [mnat,nnat] = goal Arith.thy
  19.209      "[| m:nat;  n:nat |] ==> (n#+m) #-n = m";
  19.210  by (rtac (nnat RS nat_induct) 1);
  19.211 -by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mnat])));
  19.212 +by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
  19.213  val diff_add_inverse = result();
  19.214  
  19.215  val [mnat,nnat] = goal Arith.thy
  19.216      "[| m:nat;  n:nat |] ==> n #- (n#+m) = 0";
  19.217  by (rtac (nnat RS nat_induct) 1);
  19.218 -by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mnat])));
  19.219 +by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
  19.220  val diff_add_0 = result();
  19.221  
  19.222  
  19.223  (*** Remainder ***)
  19.224  
  19.225  (*In ordinary notation: if 0<n and n<=m then m-n < m *)
  19.226 -val prems = goal Arith.thy
  19.227 -    "[| 0:n; ~ m:n;  m:nat;  n:nat |] ==> m #- n : m";
  19.228 -by (cut_facts_tac prems 1);
  19.229 +goal Arith.thy "!!m n. [| 0:n; ~ m:n;  m:nat;  n:nat |] ==> m #- n : m";
  19.230  by (etac rev_mp 1);
  19.231  by (etac rev_mp 1);
  19.232  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
  19.233 -by (resolve_tac prems 1);
  19.234 -by (resolve_tac prems 1);
  19.235 -by (ALLGOALS (ASM_SIMP_TAC
  19.236 -	      (nat_ss addrews (prems@[diff_leq,diff_succ_succ]))));
  19.237 +by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_leq,diff_succ_succ])));
  19.238  val div_termination = result();
  19.239  
  19.240  val div_rls =
  19.241 @@ -286,17 +270,17 @@
  19.242  by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
  19.243  val mod_type = result();
  19.244  
  19.245 -val div_ss = ZF_ss addrews [naturals_are_ordinals,div_termination];
  19.246 +val div_ss = ZF_ss addsimps [naturals_are_ordinals,div_termination];
  19.247  
  19.248  val prems = goal Arith.thy "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m mod n = m";
  19.249  by (rtac (mod_def RS def_transrec RS trans) 1);
  19.250 -by (SIMP_TAC (div_ss addrews prems) 1);
  19.251 +by (simp_tac (div_ss addsimps prems) 1);
  19.252  val mod_less = result();
  19.253  
  19.254  val prems = goal Arith.thy
  19.255      "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m mod n = (m#-n) mod n";
  19.256  by (rtac (mod_def RS def_transrec RS trans) 1);
  19.257 -by (SIMP_TAC (div_ss addrews prems) 1);
  19.258 +by (simp_tac (div_ss addsimps prems) 1);
  19.259  val mod_geq = result();
  19.260  
  19.261  (*** Quotient ***)
  19.262 @@ -310,13 +294,13 @@
  19.263  val prems = goal Arith.thy
  19.264      "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m div n = 0";
  19.265  by (rtac (div_def RS def_transrec RS trans) 1);
  19.266 -by (SIMP_TAC (div_ss addrews prems) 1);
  19.267 +by (simp_tac (div_ss addsimps prems) 1);
  19.268  val div_less = result();
  19.269  
  19.270  val prems = goal Arith.thy
  19.271      "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m div n = succ((m#-n) div n)";
  19.272  by (rtac (div_def RS def_transrec RS trans) 1);
  19.273 -by (SIMP_TAC (div_ss addrews prems) 1);
  19.274 +by (simp_tac (div_ss addsimps prems) 1);
  19.275  val div_geq = result();
  19.276  
  19.277  (*Main Result.*)
  19.278 @@ -326,8 +310,8 @@
  19.279  by (resolve_tac prems 1);
  19.280  by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1);
  19.281  by (ALLGOALS 
  19.282 -    (ASM_SIMP_TAC
  19.283 -     (arith_ss addrews ([mod_type,div_type] @ prems @
  19.284 +    (asm_simp_tac
  19.285 +     (arith_ss addsimps ([mod_type,div_type] @ prems @
  19.286          [mod_less,mod_geq, div_less, div_geq,
  19.287  	 add_assoc, add_diff_inverse, div_termination]))));
  19.288  val mod_div_equality = result();
  19.289 @@ -338,7 +322,7 @@
  19.290  val [mnat,nnat] = goal Arith.thy
  19.291      "[| m:nat;  n:nat |] ==> ~ (m #+ n) : n";
  19.292  by (rtac (mnat RS nat_induct) 1);
  19.293 -by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mem_not_refl])));
  19.294 +by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mem_not_refl])));
  19.295  by (rtac notI 1);
  19.296  by (etac notE 1);
  19.297  by (etac (succI1 RS Ord_trans) 1);
    20.1 --- a/src/ZF/arith.thy	Fri Sep 17 12:53:53 1993 +0200
    20.2 +++ b/src/ZF/arith.thy	Fri Sep 17 16:16:38 1993 +0200
    20.3 @@ -16,7 +16,7 @@
    20.4      "#-" :: "[i,i]=>i"      		(infixl 65)
    20.5  
    20.6  rules
    20.7 -    rec_def  "rec(k,a,b) ==  transrec(k, %n f. nat_case(n, a, %m. b(m, f`m)))"
    20.8 +    rec_def  "rec(k,a,b) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
    20.9  
   20.10      add_def  "m#+n == rec(m, n, %u v.succ(v))"
   20.11      diff_def "m#-n == rec(n, m, %u v. rec(v, 0, %x y.x))"
    21.1 --- a/src/ZF/bool.ML	Fri Sep 17 12:53:53 1993 +0200
    21.2 +++ b/src/ZF/bool.ML	Fri Sep 17 16:16:38 1993 +0200
    21.3 @@ -53,9 +53,6 @@
    21.4  by (resolve_tac prems 1);
    21.5  val cond_type = result();
    21.6  
    21.7 -val [cond_cong] = mk_congs Bool.thy ["cond"];
    21.8 -val bool_congs = mk_congs Bool.thy ["cond","not","op and","op or","op xor"];
    21.9 -
   21.10  val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
   21.11  by (rewtac rew);
   21.12  by (rtac cond_1 1);
    22.1 --- a/src/ZF/constructor.ML	Fri Sep 17 12:53:53 1993 +0200
    22.2 +++ b/src/ZF/constructor.ML	Fri Sep 17 16:16:38 1993 +0200
    22.3 @@ -40,7 +40,6 @@
    22.4    val free_iffs  : thm list		(*freeness rewrite rules*)
    22.5    val free_SEs   : thm list		(*freeness destruct rules*)
    22.6    val mk_free    : string -> thm	(*makes freeness theorems*)
    22.7 -  val congs	 : thm list		(*congruence rules for simplifier*)
    22.8    end;
    22.9  
   22.10  
   22.11 @@ -194,7 +193,6 @@
   22.12  val case_eqns = map prove_case_equation 
   22.13  		    (flat con_ty_lists ~~ big_case_args ~~ tl con_defs);
   22.14  
   22.15 -val congs = mk_congs con_thy (flat (map #1 (const_decs @ ext_constants ext)));
   22.16  end;
   22.17  
   22.18  
    23.1 --- a/src/ZF/epsilon.ML	Fri Sep 17 12:53:53 1993 +0200
    23.2 +++ b/src/ZF/epsilon.ML	Fri Sep 17 16:16:38 1993 +0200
    23.3 @@ -64,8 +64,8 @@
    23.4      "!!X A n. [| Transset(X);  A<=X;  n: nat |] ==> \
    23.5  \             nat_rec(n, A, %m r. Union(r)) <= X";
    23.6  by (etac nat_induct 1);
    23.7 -by (ASM_SIMP_TAC (ZF_ss addrews [nat_rec_0]) 1);
    23.8 -by (ASM_SIMP_TAC (ZF_ss addrews [nat_rec_succ]) 1);
    23.9 +by (asm_simp_tac (ZF_ss addsimps [nat_rec_0]) 1);
   23.10 +by (asm_simp_tac (ZF_ss addsimps [nat_rec_succ]) 1);
   23.11  by (fast_tac ZF_cs 1);
   23.12  val eclose_least_lemma = result();
   23.13  
   23.14 @@ -126,8 +126,8 @@
   23.15  by (rtac (kmemj RS eclose_induct) 1);
   23.16  by (rtac wfrec_ssubst 1);
   23.17  by (rtac wfrec_ssubst 1);
   23.18 -by (ASM_SIMP_TAC (wf_ss addrews [under_Memrel_eclose,
   23.19 -				 jmemi RSN (2,mem_eclose_sing_trans)]) 1);
   23.20 +by (asm_simp_tac (ZF_ss addsimps [under_Memrel_eclose,
   23.21 +				  jmemi RSN (2,mem_eclose_sing_trans)]) 1);
   23.22  val wfrec_eclose_eq = result();
   23.23  
   23.24  val [prem] = goal Epsilon.thy
   23.25 @@ -139,8 +139,8 @@
   23.26  goalw Epsilon.thy [transrec_def]
   23.27      "transrec(a,H) = H(a, lam x:a. transrec(x,H))";
   23.28  by (rtac wfrec_ssubst 1);
   23.29 -by (SIMP_TAC (wf_ss addrews [wfrec_eclose_eq2,
   23.30 -			     arg_in_eclose_sing, under_Memrel_eclose]) 1);
   23.31 +by (simp_tac (ZF_ss addsimps [wfrec_eclose_eq2, arg_in_eclose_sing,
   23.32 +			      under_Memrel_eclose]) 1);
   23.33  val transrec = result();
   23.34  
   23.35  (*Avoids explosions in proofs; resolve it with a meta-level definition.*)
   23.36 @@ -173,23 +173,12 @@
   23.37  by (DEPTH_SOLVE (ares_tac prems 1 ORELSE eresolve_tac [ssubst,Ord_trans] 1));
   23.38  val Ord_transrec_type = result();
   23.39  
   23.40 -(*Congruence*)
   23.41 -val prems = goalw Epsilon.thy [transrec_def,Memrel_def]
   23.42 -    "[| a=a';  !!x u. H(x,u)=H'(x,u) |]  ==> transrec(a,H)=transrec(a',H')";
   23.43 -val transrec_ss = 
   23.44 -    ZF_ss addcongs ([wfrec_cong] @ mk_congs Epsilon.thy ["eclose"])
   23.45 -	  addrews (prems RL [sym]);
   23.46 -by (SIMP_TAC transrec_ss 1);
   23.47 -val transrec_cong = result();
   23.48 -
   23.49  (*** Rank ***)
   23.50  
   23.51 -val ord_ss = ZF_ss addcongs (mk_congs Ord.thy ["Ord"]);
   23.52 -
   23.53  (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
   23.54  goal Epsilon.thy "rank(a) = (UN y:a. succ(rank(y)))";
   23.55  by (rtac (rank_def RS def_transrec RS ssubst) 1);
   23.56 -by (SIMP_TAC ZF_ss 1);
   23.57 +by (simp_tac ZF_ss 1);
   23.58  val rank = result();
   23.59  
   23.60  goal Epsilon.thy "Ord(rank(a))";
   23.61 @@ -203,7 +192,7 @@
   23.62  val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i";
   23.63  by (rtac (major RS trans_induct) 1);
   23.64  by (rtac (rank RS ssubst) 1);
   23.65 -by (ASM_SIMP_TAC (ord_ss addrews [Ord_equality]) 1);
   23.66 +by (asm_simp_tac (ZF_ss addsimps [Ord_equality]) 1);
   23.67  val rank_of_Ord = result();
   23.68  
   23.69  val [prem] = goal Epsilon.thy "a:b ==> rank(a) : rank(b)";
    24.1 --- a/src/ZF/fin.ML	Fri Sep 17 12:53:53 1993 +0200
    24.2 +++ b/src/ZF/fin.ML	Fri Sep 17 16:16:38 1993 +0200
    24.3 @@ -55,19 +55,19 @@
    24.4  val Fin_induct = result();
    24.5  
    24.6  (** Simplification for Fin **)
    24.7 -val Fin_ss = arith_ss addcongs mk_congs Fin.thy ["Fin"] addrews Fin.intrs;
    24.8 +val Fin_ss = arith_ss addsimps Fin.intrs;
    24.9  
   24.10  (*The union of two finite sets is fin*)
   24.11  val major::prems = goal Fin.thy
   24.12      "[| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)";
   24.13  by (rtac (major RS Fin_induct) 1);
   24.14 -by (ALLGOALS (ASM_SIMP_TAC (Fin_ss addrews (prems@[Un_0, Un_cons]))));
   24.15 +by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_0, Un_cons]))));
   24.16  val Fin_UnI = result();
   24.17  
   24.18  (*The union of a set of finite sets is fin*)
   24.19  val [major] = goal Fin.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
   24.20  by (rtac (major RS Fin_induct) 1);
   24.21 -by (ALLGOALS (ASM_SIMP_TAC (Fin_ss addrews [Union_0, Union_cons, Fin_UnI])));
   24.22 +by (ALLGOALS (asm_simp_tac (Fin_ss addsimps [Union_0, Union_cons, Fin_UnI])));
   24.23  val Fin_UnionI = result();
   24.24  
   24.25  (*Every subset of a finite set is fin*)
   24.26 @@ -76,10 +76,10 @@
   24.27  	    etac (spec RS mp),
   24.28  	    rtac subs]);
   24.29  by (rtac (fin RS Fin_induct) 1);
   24.30 -by (SIMP_TAC (Fin_ss addrews [subset_empty_iff]) 1);
   24.31 +by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1);
   24.32  by (safe_tac (ZF_cs addSDs [subset_cons_iff RS iffD1]));
   24.33  by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 2);
   24.34 -by (ALLGOALS (ASM_SIMP_TAC Fin_ss));
   24.35 +by (ALLGOALS (asm_simp_tac Fin_ss));
   24.36  val Fin_subset = result();
   24.37  
   24.38  val major::prems = goal Fin.thy 
   24.39 @@ -89,7 +89,7 @@
   24.40  \    |] ==> c<=b --> P(b-c)";
   24.41  by (rtac (major RS Fin_induct) 1);
   24.42  by (rtac (Diff_cons RS ssubst) 2);
   24.43 -by (ALLGOALS (ASM_SIMP_TAC (Fin_ss addrews (prems@[Diff_0, cons_subset_iff, 
   24.44 +by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Diff_0, cons_subset_iff, 
   24.45  				Diff_subset RS Fin_subset]))));
   24.46  val Fin_0_induct_lemma = result();
   24.47  
    25.1 --- a/src/ZF/func.ML	Fri Sep 17 12:53:53 1993 +0200
    25.2 +++ b/src/ZF/func.ML	Fri Sep 17 16:16:38 1993 +0200
    25.3 @@ -37,7 +37,7 @@
    25.4  
    25.5  val prems = goalw ZF.thy [Pi_def]
    25.6      "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> Pi(A,B) = Pi(A',B')";
    25.7 -by (prove_cong_tac (prems@[Collect_cong,Sigma_cong,ball_cong]) 1);
    25.8 +by (simp_tac (FOL_ss addsimps prems addcongs [Sigma_cong]) 1);
    25.9  val Pi_cong = result();
   25.10  
   25.11  (*Weaking one function type to another*)
   25.12 @@ -84,8 +84,7 @@
   25.13  by (rtac refl 1);
   25.14  val memberPiE = result();
   25.15  
   25.16 -(*Conclusion is flexible -- use res_inst_tac or else RS with a theorem
   25.17 -  of the form f:A->B *)
   25.18 +(*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*)
   25.19  goal ZF.thy "!!f. [| f: Pi(A,B);  a:A |] ==> f`a : B(a)"; 
   25.20  by (rtac (fun_unique_Pair RS ex1E) 1);
   25.21  by (REPEAT (assume_tac 1));
   25.22 @@ -94,6 +93,11 @@
   25.23  by (REPEAT (assume_tac 1));
   25.24  val apply_type = result();
   25.25  
   25.26 +(*This version is acceptable to the simplifier*)
   25.27 +goal ZF.thy "!!f. [| f: A->B;  a:A |] ==> f`a : B"; 
   25.28 +by (REPEAT (ares_tac [apply_type] 1));
   25.29 +val apply_funtype = result();
   25.30 +
   25.31  goal ZF.thy "!!f. [| f: Pi(A,B);  a:A |] ==> <a,f`a>: f";
   25.32  by (rtac (fun_unique_Pair RS ex1E) 1);
   25.33  by (resolve_tac [apply_equality RS ssubst] 3);
   25.34 @@ -169,11 +173,8 @@
   25.35  
   25.36  (*congruence rule for lambda abstraction*)
   25.37  val prems = goalw ZF.thy [lam_def] 
   25.38 -    "[| A=A';  !!x. x:A' ==> b(x)=b'(x) |] ==>  \
   25.39 -\    (lam x:A.b(x)) = (lam x:A'.b'(x))";
   25.40 -by (rtac RepFun_cong 1);
   25.41 -by (res_inst_tac [("t","Pair")] subst_context2 2);
   25.42 -by (REPEAT (ares_tac (prems@[refl]) 1));
   25.43 +    "[| A=A';  !!x. x:A' ==> b(x)=b'(x) |] ==> Lambda(A,b) = Lambda(A',b')";
   25.44 +by (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1);
   25.45  val lam_cong = result();
   25.46  
   25.47  val [major] = goal ZF.thy
   25.48 @@ -259,7 +260,7 @@
   25.49  val [prem] = goalw ZF.thy [restrict_def]
   25.50      "A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))";
   25.51  by (rtac (refl RS lam_cong) 1);
   25.52 -be (prem RS subsetD RS beta) 1;	(*easier than calling SIMP_TAC*)
   25.53 +be (prem RS subsetD RS beta) 1;	(*easier than calling simp_tac*)
   25.54  val restrict_lam_eq = result();
   25.55  
   25.56  
    26.1 --- a/src/ZF/ind-syntax.ML	Fri Sep 17 12:53:53 1993 +0200
    26.2 +++ b/src/ZF/ind-syntax.ML	Fri Sep 17 16:16:38 1993 +0200
    26.3 @@ -37,7 +37,6 @@
    26.4         flatten_term sign (Logic.mk_equals (lhs,rhs)))
    26.5    end;
    26.6  
    26.7 -(*export to Pure/sign?  Used in Provers/simp.ML...*)
    26.8  fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
    26.9  
   26.10  (*export to Pure/library?  *)
    27.1 --- a/src/ZF/ind_syntax.ML	Fri Sep 17 12:53:53 1993 +0200
    27.2 +++ b/src/ZF/ind_syntax.ML	Fri Sep 17 16:16:38 1993 +0200
    27.3 @@ -37,7 +37,6 @@
    27.4         flatten_term sign (Logic.mk_equals (lhs,rhs)))
    27.5    end;
    27.6  
    27.7 -(*export to Pure/sign?  Used in Provers/simp.ML...*)
    27.8  fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
    27.9  
   27.10  (*export to Pure/library?  *)
    28.1 --- a/src/ZF/list.ML	Fri Sep 17 12:53:53 1993 +0200
    28.2 +++ b/src/ZF/list.ML	Fri Sep 17 16:16:38 1993 +0200
    28.3 @@ -62,7 +62,7 @@
    28.4  \       !!x y. [| x: A;  y: list(A) |] ==> h(x,y): C(<x,y>)  \
    28.5  \    |] ==> list_case(l,c,h) : C(l)";
    28.6  by (rtac (major RS list_induct) 1);
    28.7 -by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
    28.8 +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
    28.9  			    ([list_case_0,list_case_Pair]@prems))));
   28.10  val list_case_type = result();
   28.11  ****)
   28.12 @@ -71,10 +71,10 @@
   28.13  (** For recursion **)
   28.14  
   28.15  goalw List.thy List.con_defs "rank(a) : rank(Cons(a,l))";
   28.16 -by (SIMP_TAC rank_ss 1);
   28.17 +by (simp_tac rank_ss 1);
   28.18  val rank_Cons1 = result();
   28.19  
   28.20  goalw List.thy List.con_defs "rank(l) : rank(Cons(a,l))";
   28.21 -by (SIMP_TAC rank_ss 1);
   28.22 +by (simp_tac rank_ss 1);
   28.23  val rank_Cons2 = result();
   28.24  
    29.1 --- a/src/ZF/listfn.ML	Fri Sep 17 12:53:53 1993 +0200
    29.2 +++ b/src/ZF/listfn.ML	Fri Sep 17 16:16:38 1993 +0200
    29.3 @@ -11,19 +11,14 @@
    29.4  
    29.5  (** list_rec -- by Vset recursion **)
    29.6  
    29.7 -(*Used to verify list_rec*)
    29.8 -val list_rec_ss = ZF_ss 
    29.9 -      addcongs (mk_typed_congs ListFn.thy [("h", "[i,i,i]=>i")])
   29.10 -      addrews List.case_eqns;
   29.11 -
   29.12  goal ListFn.thy "list_rec(Nil,c,h) = c";
   29.13  by (rtac (list_rec_def RS def_Vrec RS trans) 1);
   29.14 -by (SIMP_TAC list_rec_ss 1);
   29.15 +by (simp_tac (ZF_ss addsimps List.case_eqns) 1);
   29.16  val list_rec_Nil = result();
   29.17  
   29.18  goal ListFn.thy "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))";
   29.19  by (rtac (list_rec_def RS def_Vrec RS trans) 1);
   29.20 -by (SIMP_TAC (list_rec_ss addrews [Vset_rankI, rank_Cons2]) 1);
   29.21 +by (simp_tac (ZF_ss addsimps (List.case_eqns @ [Vset_rankI, rank_Cons2])) 1);
   29.22  val list_rec_Cons = result();
   29.23  
   29.24  (*Type checking -- proved by induction, as usual*)
   29.25 @@ -33,8 +28,8 @@
   29.26  \       !!x y r. [| x:A;  y: list(A);  r: C(y) |] ==> h(x,y,r): C(Cons(x,y))  \
   29.27  \    |] ==> list_rec(l,c,h) : C(l)";
   29.28  by (list_ind_tac "l" prems 1);
   29.29 -by (ALLGOALS (ASM_SIMP_TAC
   29.30 -	      (ZF_ss addrews (prems@[list_rec_Nil,list_rec_Cons]))));
   29.31 +by (ALLGOALS (asm_simp_tac
   29.32 +	      (ZF_ss addsimps (prems@[list_rec_Nil,list_rec_Cons]))));
   29.33  val list_rec_type = result();
   29.34  
   29.35  (** Versions for use with definitions **)
   29.36 @@ -122,47 +117,42 @@
   29.37         map_type, map_type2, app_type, length_type, rev_type, flat_type,
   29.38         list_add_type];
   29.39  
   29.40 -val list_congs = 
   29.41 -    List.congs @ 
   29.42 -    mk_congs ListFn.thy
   29.43 -        ["list_rec","map","op @","length","rev","flat","list_add"];
   29.44 -
   29.45  val list_ss = arith_ss 
   29.46 -    addcongs list_congs
   29.47 -    addrews List.case_eqns
   29.48 -    addrews list_typechecks
   29.49 -    addrews [list_rec_Nil, list_rec_Cons, 
   29.50 +    addsimps List.case_eqns
   29.51 +    addsimps [list_rec_Nil, list_rec_Cons, 
   29.52  	     map_Nil, map_Cons,
   29.53  	     app_Nil, app_Cons,
   29.54  	     length_Nil, length_Cons,
   29.55  	     rev_Nil, rev_Cons,
   29.56  	     flat_Nil, flat_Cons,
   29.57 -	     list_add_Nil, list_add_Cons];
   29.58 +	     list_add_Nil, list_add_Cons]
   29.59 +    setsolver (type_auto_tac list_typechecks);
   29.60 +(*Could also rewrite using the list_typechecks...*)
   29.61  
   29.62  (*** theorems about map ***)
   29.63  
   29.64  val prems = goal ListFn.thy
   29.65      "l: list(A) ==> map(%u.u, l) = l";
   29.66  by (list_ind_tac "l" prems 1);
   29.67 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
   29.68 +by (ALLGOALS (asm_simp_tac list_ss));
   29.69  val map_ident = result();
   29.70  
   29.71  val prems = goal ListFn.thy
   29.72      "l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)";
   29.73  by (list_ind_tac "l" prems 1);
   29.74 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
   29.75 +by (ALLGOALS (asm_simp_tac list_ss));
   29.76  val map_compose = result();
   29.77  
   29.78  val prems = goal ListFn.thy
   29.79      "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
   29.80  by (list_ind_tac "xs" prems 1);
   29.81 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
   29.82 +by (ALLGOALS (asm_simp_tac list_ss));
   29.83  val map_app_distrib = result();
   29.84  
   29.85  val prems = goal ListFn.thy
   29.86      "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";
   29.87  by (list_ind_tac "ls" prems 1);
   29.88 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [map_app_distrib])));
   29.89 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib])));
   29.90  val map_flat = result();
   29.91  
   29.92  val prems = goal ListFn.thy
   29.93 @@ -170,9 +160,7 @@
   29.94  \    list_rec(map(h,l), c, d) = \
   29.95  \    list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))";
   29.96  by (list_ind_tac "l" prems 1);
   29.97 -by (ALLGOALS 
   29.98 -    (ASM_SIMP_TAC 
   29.99 -     (list_ss addcongs (mk_typed_congs ListFn.thy [("d", "[i,i,i]=>i")]))));
  29.100 +by (ALLGOALS (asm_simp_tac list_ss));
  29.101  val list_rec_map = result();
  29.102  
  29.103  (** theorems about list(Collect(A,P)) -- used in ex/term.ML **)
  29.104 @@ -183,7 +171,7 @@
  29.105  val prems = goal ListFn.thy
  29.106      "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
  29.107  by (list_ind_tac "l" prems 1);
  29.108 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
  29.109 +by (ALLGOALS (asm_simp_tac list_ss));
  29.110  val map_list_Collect = result();
  29.111  
  29.112  (*** theorems about length ***)
  29.113 @@ -191,13 +179,13 @@
  29.114  val prems = goal ListFn.thy
  29.115      "xs: list(A) ==> length(map(h,xs)) = length(xs)";
  29.116  by (list_ind_tac "xs" prems 1);
  29.117 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
  29.118 +by (ALLGOALS (asm_simp_tac list_ss));
  29.119  val length_map = result();
  29.120  
  29.121  val prems = goal ListFn.thy
  29.122      "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
  29.123  by (list_ind_tac "xs" prems 1);
  29.124 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
  29.125 +by (ALLGOALS (asm_simp_tac list_ss));
  29.126  val length_app = result();
  29.127  
  29.128  (* [| m: nat; n: nat |] ==> m #+ succ(n) = succ(n) #+ m 
  29.129 @@ -207,60 +195,59 @@
  29.130  val prems = goal ListFn.thy
  29.131      "xs: list(A) ==> length(rev(xs)) = length(xs)";
  29.132  by (list_ind_tac "xs" prems 1);
  29.133 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [length_app, add_commute_succ])));
  29.134 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app, add_commute_succ])));
  29.135  val length_rev = result();
  29.136  
  29.137  val prems = goal ListFn.thy
  29.138      "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
  29.139  by (list_ind_tac "ls" prems 1);
  29.140 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [length_app])));
  29.141 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app])));
  29.142  val length_flat = result();
  29.143  
  29.144  (*** theorems about app ***)
  29.145  
  29.146  val [major] = goal ListFn.thy "xs: list(A) ==> xs@Nil=xs";
  29.147  by (rtac (major RS List.induct) 1);
  29.148 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
  29.149 +by (ALLGOALS (asm_simp_tac list_ss));
  29.150  val app_right_Nil = result();
  29.151  
  29.152  val prems = goal ListFn.thy "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
  29.153  by (list_ind_tac "xs" prems 1);
  29.154 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
  29.155 +by (ALLGOALS (asm_simp_tac list_ss));
  29.156  val app_assoc = result();
  29.157  
  29.158  val prems = goal ListFn.thy
  29.159      "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
  29.160  by (list_ind_tac "ls" prems 1);
  29.161 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [app_assoc])));
  29.162 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_assoc])));
  29.163  val flat_app_distrib = result();
  29.164  
  29.165  (*** theorems about rev ***)
  29.166  
  29.167  val prems = goal ListFn.thy "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
  29.168  by (list_ind_tac "l" prems 1);
  29.169 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [map_app_distrib])));
  29.170 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib])));
  29.171  val rev_map_distrib = result();
  29.172  
  29.173  (*Simplifier needs the premises as assumptions because rewriting will not
  29.174    instantiate the variable ?A in the rules' typing conditions; note that
  29.175    rev_type does not instantiate ?A.  Only the premises do.
  29.176  *)
  29.177 -val prems = goal ListFn.thy
  29.178 -    "[| xs: list(A);  ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
  29.179 -by (cut_facts_tac prems 1);
  29.180 +goal ListFn.thy
  29.181 +    "!!xs. [| xs: list(A);  ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
  29.182  by (etac List.induct 1);
  29.183 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [app_right_Nil,app_assoc])));
  29.184 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_right_Nil,app_assoc])));
  29.185  val rev_app_distrib = result();
  29.186  
  29.187  val prems = goal ListFn.thy "l: list(A) ==> rev(rev(l))=l";
  29.188  by (list_ind_tac "l" prems 1);
  29.189 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [rev_app_distrib])));
  29.190 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [rev_app_distrib])));
  29.191  val rev_rev_ident = result();
  29.192  
  29.193  val prems = goal ListFn.thy
  29.194      "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
  29.195  by (list_ind_tac "ls" prems 1);
  29.196 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews 
  29.197 +by (ALLGOALS (asm_simp_tac (list_ss addsimps 
  29.198         [map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil])));
  29.199  val rev_flat = result();
  29.200  
  29.201 @@ -273,22 +260,22 @@
  29.202  by (cut_facts_tac prems 1);
  29.203  by (list_ind_tac "xs" prems 1);
  29.204  by (ALLGOALS 
  29.205 -    (ASM_SIMP_TAC (list_ss addrews [add_0_right, add_assoc RS sym])));
  29.206 -by (resolve_tac arith_congs 1);
  29.207 -by (REPEAT (ares_tac [refl, list_add_type, add_commute] 1));
  29.208 +    (asm_simp_tac (list_ss addsimps [add_0_right, add_assoc RS sym])));
  29.209 +by (rtac (add_commute RS subst_context) 1);
  29.210 +by (REPEAT (ares_tac [refl, list_add_type] 1));
  29.211  val list_add_app = result();
  29.212  
  29.213  val prems = goal ListFn.thy
  29.214      "l: list(nat) ==> list_add(rev(l)) = list_add(l)";
  29.215  by (list_ind_tac "l" prems 1);
  29.216  by (ALLGOALS
  29.217 -    (ASM_SIMP_TAC (list_ss addrews [list_add_app, add_0_right])));
  29.218 +    (asm_simp_tac (list_ss addsimps [list_add_app, add_0_right])));
  29.219  val list_add_rev = result();
  29.220  
  29.221  val prems = goal ListFn.thy
  29.222      "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
  29.223  by (list_ind_tac "ls" prems 1);
  29.224 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [list_add_app])));
  29.225 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [list_add_app])));
  29.226  by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1));
  29.227  val list_add_flat = result();
  29.228  
  29.229 @@ -301,6 +288,6 @@
  29.230  \    |] ==> P(l)";
  29.231  by (rtac (major RS rev_rev_ident RS subst) 1);
  29.232  by (rtac (major RS rev_type RS List.induct) 1);
  29.233 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews prems)));
  29.234 +by (ALLGOALS (asm_simp_tac (list_ss addsimps prems)));
  29.235  val list_append_induct = result();
  29.236  
    30.1 --- a/src/ZF/nat.ML	Fri Sep 17 12:53:53 1993 +0200
    30.2 +++ b/src/ZF/nat.ML	Fri Sep 17 16:16:38 1993 +0200
    30.3 @@ -95,8 +95,8 @@
    30.4  \    |] ==> m <= n --> P(m) --> P(n)";
    30.5  by (nat_ind_tac "n" prems 1);
    30.6  by (ALLGOALS
    30.7 -    (ASM_SIMP_TAC
    30.8 -     (ZF_ss addrews (prems@distrib_rews@[subset_empty_iff, subset_succ_iff, 
    30.9 +    (asm_simp_tac
   30.10 +     (ZF_ss addsimps (prems@distrib_rews@[subset_empty_iff, subset_succ_iff, 
   30.11  					 Ord_nat RS Ord_in_Ord]))));
   30.12  val nat_induct_from_lemma = result();
   30.13  
   30.14 @@ -127,17 +127,17 @@
   30.15  
   30.16  (** nat_case **)
   30.17  
   30.18 -goalw Nat.thy [nat_case_def] "nat_case(0,a,b) = a";
   30.19 +goalw Nat.thy [nat_case_def] "nat_case(a,b,0) = a";
   30.20  by (fast_tac (ZF_cs addIs [the_equality]) 1);
   30.21  val nat_case_0 = result();
   30.22  
   30.23 -goalw Nat.thy [nat_case_def] "nat_case(succ(m),a,b) = b(m)";
   30.24 +goalw Nat.thy [nat_case_def] "nat_case(a,b,succ(m)) = b(m)";
   30.25  by (fast_tac (ZF_cs addIs [the_equality]) 1);
   30.26  val nat_case_succ = result();
   30.27  
   30.28  val major::prems = goal Nat.thy
   30.29      "[| n: nat;  a: C(0);  !!m. m: nat ==> b(m): C(succ(m))  \
   30.30 -\    |] ==> nat_case(n,a,b) : C(n)";
   30.31 +\    |] ==> nat_case(a,b,n) : C(n)";
   30.32  by (rtac (major RS nat_induct) 1);
   30.33  by (REPEAT (resolve_tac [nat_case_0 RS ssubst,
   30.34  			 nat_case_succ RS ssubst] 1 
   30.35 @@ -145,13 +145,6 @@
   30.36  by (assume_tac 1);
   30.37  val nat_case_type = result();
   30.38  
   30.39 -val prems = goalw Nat.thy [nat_case_def]
   30.40 -    "[| n=n';  a=a';  !!m z. b(m)=b'(m)  \
   30.41 -\    |] ==> nat_case(n,a,b)=nat_case(n',a',b')";
   30.42 -by (REPEAT (resolve_tac [the_cong,disj_cong,ex_cong] 1
   30.43 -     ORELSE EVERY1 (map rtac ((prems RL [ssubst]) @ [iff_refl]))));
   30.44 -val nat_case_cong = result();
   30.45 -
   30.46  
   30.47  (** nat_rec -- used to define eclose and transrec, then obsolete **)
   30.48  
   30.49 @@ -165,11 +158,10 @@
   30.50  val [prem] = goal Nat.thy 
   30.51      "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))";
   30.52  val nat_rec_ss = ZF_ss 
   30.53 -      addcongs (mk_typed_congs Nat.thy [("b", "[i,i]=>i")])
   30.54 -      addrews [prem, nat_case_succ, nat_succI, Memrel_iff, 
   30.55 -	       vimage_singleton_iff];
   30.56 +      addsimps [prem, nat_case_succ, nat_succI, Memrel_iff, 
   30.57 +		vimage_singleton_iff];
   30.58  by (rtac nat_rec_trans 1);
   30.59 -by (SIMP_TAC nat_rec_ss 1);
   30.60 +by (simp_tac nat_rec_ss 1);
   30.61  val nat_rec_succ = result();
   30.62  
   30.63  (** The union of two natural numbers is a natural number -- their maximum **)
    31.1 --- a/src/ZF/nat.thy	Fri Sep 17 12:53:53 1993 +0200
    31.2 +++ b/src/ZF/nat.thy	Fri Sep 17 16:16:38 1993 +0200
    31.3 @@ -9,7 +9,7 @@
    31.4  Nat = Ord + Bool + 
    31.5  consts
    31.6      nat 	::      "i"
    31.7 -    nat_case    ::      "[i, i, i=>i]=>i"
    31.8 +    nat_case    ::      "[i, i=>i, i]=>i"
    31.9      nat_rec     ::      "[i, i, [i,i]=>i]=>i"
   31.10  
   31.11  rules
   31.12 @@ -17,10 +17,10 @@
   31.13      nat_def     "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})"
   31.14  
   31.15      nat_case_def
   31.16 -	"nat_case(k,a,b) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
   31.17 +	"nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
   31.18  
   31.19      nat_rec_def
   31.20  	"nat_rec(k,a,b) ==   \
   31.21 -\   	  wfrec(Memrel(nat), k, %n f. nat_case(n, a, %m. b(m, f`m)))"
   31.22 +\   	  wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
   31.23  
   31.24  end
    32.1 --- a/src/ZF/ord.ML	Fri Sep 17 12:53:53 1993 +0200
    32.2 +++ b/src/ZF/ord.ML	Fri Sep 17 16:16:38 1993 +0200
    32.3 @@ -318,7 +318,7 @@
    32.4  
    32.5  goal Ord.thy
    32.6      "!!i j. [| Ord(i);  Ord(j) |] ==> i<=succ(j) <-> i<=j | i=succ(j)";
    32.7 -by (ASM_SIMP_TAC (ZF_ss addrews [member_succ_iff RS iff_sym, Ord_succ]) 1);
    32.8 +by (asm_simp_tac (ZF_ss addsimps [member_succ_iff RS iff_sym, Ord_succ]) 1);
    32.9  by (fast_tac ZF_cs 1);
   32.10  val subset_succ_iff = result();
   32.11  
   32.12 @@ -356,17 +356,17 @@
   32.13  goal Ord.thy "!!i j k. [| i:k;  j:k;  Ord(k) |] ==> i Un j : k";
   32.14  by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);
   32.15  by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
   32.16 -by (ASM_SIMP_TAC (ZF_ss addrews [subset_Un_iff RS iffD1]) 1);
   32.17 +by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1);
   32.18  by (rtac (Un_commute RS ssubst) 1);
   32.19 -by (ASM_SIMP_TAC (ZF_ss addrews [subset_Un_iff RS iffD1]) 1);
   32.20 +by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1);
   32.21  val Ord_member_UnI = result();
   32.22  
   32.23  goal Ord.thy "!!i j k. [| i:k;  j:k;  Ord(k) |] ==> i Int j : k";
   32.24  by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);
   32.25  by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
   32.26 -by (ASM_SIMP_TAC (ZF_ss addrews [subset_Int_iff RS iffD1]) 1);
   32.27 +by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1);
   32.28  by (rtac (Int_commute RS ssubst) 1);
   32.29 -by (ASM_SIMP_TAC (ZF_ss addrews [subset_Int_iff RS iffD1]) 1);
   32.30 +by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1);
   32.31  val Ord_member_IntI = result();
   32.32  
   32.33  
    33.1 --- a/src/ZF/pair.ML	Fri Sep 17 12:53:53 1993 +0200
    33.2 +++ b/src/ZF/pair.ML	Fri Sep 17 16:16:38 1993 +0200
    33.3 @@ -15,7 +15,7 @@
    33.4  
    33.5  val Pair_iff = prove_goalw ZF.thy [Pair_def]
    33.6      "<a,b> = <c,d> <-> a=c & b=d"
    33.7 - (fn _=> [ (SIMP_TAC (FOL_ss addrews [doubleton_iff]) 1),
    33.8 + (fn _=> [ (simp_tac (FOL_ss addsimps [doubleton_iff]) 1),
    33.9             (fast_tac FOL_cs 1) ]);
   33.10  
   33.11  val Pair_inject = standard (Pair_iff RS iffD1 RS conjE);
   33.12 @@ -89,7 +89,7 @@
   33.13  val Sigma_cong = prove_goalw ZF.thy [Sigma_def]
   33.14      "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \
   33.15  \    Sigma(A,B) = Sigma(A',B')"
   33.16 - (fn prems=> [ (prove_cong_tac (prems@[RepFun_cong]) 1) ]);
   33.17 + (fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1) ]);
   33.18  
   33.19  val Sigma_empty1 = prove_goal ZF.thy "Sigma(0,B) = 0"
   33.20   (fn _ => [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [SigmaE]) 1) ]);
   33.21 @@ -114,13 +114,6 @@
   33.22      (etac ssubst 1),
   33.23      (REPEAT (ares_tac (prems @ [split RS ssubst]) 1)) ]);
   33.24  
   33.25 -(*This congruence rule uses NO typing information...*)
   33.26 -val split_cong = prove_goalw ZF.thy [split_def] 
   33.27 -    "[| p=p';  !!x y.c(x,y) = c'(x,y) |] ==> \
   33.28 -\    split(%x y.c(x,y), p) = split(%x y.c'(x,y), p')"
   33.29 - (fn prems=> [ (prove_cong_tac (prems@[the_cong]) 1) ]);
   33.30 -
   33.31 -
   33.32  (*** conversions for fst and snd ***)
   33.33  
   33.34  val fst_conv = prove_goalw ZF.thy [fst_def] "fst(<a,b>) = a"
    34.1 --- a/src/ZF/perm.ML	Fri Sep 17 12:53:53 1993 +0200
    34.2 +++ b/src/ZF/perm.ML	Fri Sep 17 16:16:38 1993 +0200
    34.3 @@ -52,6 +52,7 @@
    34.4  (* f: bij(A,B) ==> f: A->B *)
    34.5  val bij_is_fun = standard (bij_is_inj RS inj_is_fun);
    34.6  
    34.7 +
    34.8  (** Identity function **)
    34.9  
   34.10  val [prem] = goalw Perm.thy [id_def] "a:A ==> <a,a> : id(A)";  
   34.11 @@ -76,7 +77,7 @@
   34.12  
   34.13  goalw Perm.thy [inj_def,id_def] "id(A): inj(A,A)";
   34.14  by (REPEAT (ares_tac [CollectI,lam_type] 1));
   34.15 -by (SIMP_TAC ZF_ss 1);
   34.16 +by (simp_tac ZF_ss 1);
   34.17  val id_inj = result();
   34.18  
   34.19  goalw Perm.thy [id_def,surj_def] "id(A): surj(A,A)";
   34.20 @@ -262,7 +263,7 @@
   34.21      "!!f g. [| (f O g): inj(A,C);  g: A->B;  f: B->C |] ==> g: inj(A,B)";
   34.22  by (safe_tac comp_cs);
   34.23  by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
   34.24 -by (ASM_SIMP_TAC (ZF_ss addrews [comp_func_apply]) 1);
   34.25 +by (asm_simp_tac (FOL_ss addsimps [comp_func_apply]) 1);
   34.26  val comp_mem_injD1 = result();
   34.27  
   34.28  goalw Perm.thy [inj_def,surj_def]
   34.29 @@ -271,9 +272,10 @@
   34.30  by (res_inst_tac [("x1", "x")] (bspec RS bexE) 1);
   34.31  by (eres_inst_tac [("x1", "w")] (bspec RS bexE) 3);
   34.32  by (REPEAT (assume_tac 1));
   34.33 -by (safe_tac (comp_cs addSIs ZF_congs));
   34.34 +by (safe_tac comp_cs);
   34.35 +by (res_inst_tac [("t", "op `(g)")] subst_context 1);
   34.36  by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
   34.37 -by (ASM_SIMP_TAC (ZF_ss addrews [comp_func_apply]) 1);
   34.38 +by (asm_simp_tac (FOL_ss addsimps [comp_func_apply]) 1);
   34.39  val comp_mem_injD2 = result();
   34.40  
   34.41  goalw Perm.thy [surj_def]
   34.42 @@ -427,7 +429,9 @@
   34.43  by (etac fun_extend 1);
   34.44  by (REPEAT (ares_tac [ballI] 1));
   34.45  by (REPEAT_FIRST (eresolve_tac [consE,ssubst]));
   34.46 -(*Assumption ALL w:A. ALL x:A. f`w = f`x --> w=x makes ASM_SIMP_TAC loop!*)
   34.47 -by (ALLGOALS (SIMP_TAC (ZF_ss addrews [fun_extend_apply2,fun_extend_apply1])));
   34.48 +(*Assumption ALL w:A. ALL x:A. f`w = f`x --> w=x would make asm_simp_tac loop
   34.49 +  using ZF_ss!  But FOL_ss ignores the assumption...*)
   34.50 +by (ALLGOALS (asm_simp_tac 
   34.51 +	      (FOL_ss addsimps [fun_extend_apply2,fun_extend_apply1])));
   34.52  by (ALLGOALS (fast_tac (ZF_cs addIs [apply_type])));
   34.53  val inj_extend = result();
    35.1 --- a/src/ZF/qpair.ML	Fri Sep 17 12:53:53 1993 +0200
    35.2 +++ b/src/ZF/qpair.ML	Fri Sep 17 16:16:38 1993 +0200
    35.3 @@ -74,7 +74,7 @@
    35.4  val QSigma_cong = prove_goalw QPair.thy [QSigma_def]
    35.5      "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \
    35.6  \    QSigma(A,B) = QSigma(A',B')"
    35.7 - (fn prems=> [ (prove_cong_tac (prems@[RepFun_cong]) 1) ]);
    35.8 + (fn prems=> [ (simp_tac (ZF_ss addsimps prems) 1) ]);
    35.9  
   35.10  val QSigma_empty1 = prove_goal QPair.thy "QSigma(0,B) = 0"
   35.11   (fn _ => [ (fast_tac (ZF_cs addIs [equalityI] addSEs [QSigmaE]) 1) ]);
   35.12 @@ -98,12 +98,6 @@
   35.13      (etac ssubst 1),
   35.14      (REPEAT (ares_tac (prems @ [qsplit RS ssubst]) 1)) ]);
   35.15  
   35.16 -(*This congruence rule uses NO typing information...*)
   35.17 -val qsplit_cong = prove_goalw QPair.thy [qsplit_def] 
   35.18 -    "[| p=p';  !!x y.c(x,y) = c'(x,y) |] ==> \
   35.19 -\    qsplit(%x y.c(x,y), p) = qsplit(%x y.c'(x,y), p')"
   35.20 - (fn prems=> [ (prove_cong_tac (prems@[the_cong]) 1) ]);
   35.21 -
   35.22  
   35.23  val qpair_cs = ZF_cs addSIs [QSigmaI] addSEs [QSigmaE2, QSigmaE, QPair_inject];
   35.24  
   35.25 @@ -243,7 +237,7 @@
   35.26  val qsum_subset_iff = result();
   35.27  
   35.28  goal QPair.thy "A <+> B = C <+> D <-> A=C & B=D";
   35.29 -by (SIMP_TAC (ZF_ss addrews [extension,qsum_subset_iff]) 1);
   35.30 +by (simp_tac (ZF_ss addsimps [extension,qsum_subset_iff]) 1);
   35.31  by (fast_tac ZF_cs 1);
   35.32  val qsum_equal_iff = result();
   35.33  
   35.34 @@ -259,12 +253,6 @@
   35.35  by (rtac cond_1 1);
   35.36  val qcase_QInr = result();
   35.37  
   35.38 -val prems = goalw QPair.thy [qcase_def]
   35.39 -    "[| u=u'; !!x. c(x)=c'(x);  !!y. d(y)=d'(y) |] ==>    \
   35.40 -\    qcase(c,d,u)=qcase(c',d',u')";
   35.41 -by (REPEAT (resolve_tac ([refl,qsplit_cong,cond_cong] @ prems) 1));
   35.42 -val qcase_cong = result();
   35.43 -
   35.44  val major::prems = goal QPair.thy
   35.45      "[| u: A <+> B; \
   35.46  \       !!x. x: A ==> c(x): C(QInl(x));   \
   35.47 @@ -272,7 +260,7 @@
   35.48  \    |] ==> qcase(c,d,u) : C(u)";
   35.49  by (rtac (major RS qsumE) 1);
   35.50  by (ALLGOALS (etac ssubst));
   35.51 -by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
   35.52 +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
   35.53  			    (prems@[qcase_QInl,qcase_QInr]))));
   35.54  val qcase_type = result();
   35.55  
    36.1 --- a/src/ZF/quniv.ML	Fri Sep 17 12:53:53 1993 +0200
    36.2 +++ b/src/ZF/quniv.ML	Fri Sep 17 16:16:38 1993 +0200
    36.3 @@ -205,7 +205,7 @@
    36.4  
    36.5  goalw QUniv.thy [QPair_def,sum_def]
    36.6      "<a;b> Int quniv(A) = <a;b> Int univ(eclose(A))";
    36.7 -by (SIMP_TAC (ZF_ss addrews [Int_Un_distrib, product_Int_quniv_eq]) 1);
    36.8 +by (simp_tac (ZF_ss addsimps [Int_Un_distrib, product_Int_quniv_eq]) 1);
    36.9  val QPair_Int_quniv_eq = result();
   36.10  
   36.11  (**** "Take-lemma" rules for proving c: quniv(A) ****)
    37.1 --- a/src/ZF/simpdata.ML	Fri Sep 17 12:53:53 1993 +0200
    37.2 +++ b/src/ZF/simpdata.ML	Fri Sep 17 16:16:38 1993 +0200
    37.3 @@ -10,7 +10,7 @@
    37.4      (writeln s;  prove_goal ZF.thy s
    37.5         (fn prems => [ (cut_facts_tac prems 1), (fast_tac ZF_cs 1) ]));
    37.6  
    37.7 -val mem_rews = map prove_fun
    37.8 +val mem_simps = map prove_fun
    37.9   [ "a:0 <-> False",
   37.10     "a : A Un B <-> a:A | a:B",
   37.11     "a : A Int B <-> a:A & a:B",
   37.12 @@ -45,7 +45,7 @@
   37.13    NOT TERRIBLY USEFUL because it does not simplify conjunctions*)
   37.14  fun type_auto_tac tyrls hyps = SELECT_GOAL
   37.15      (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
   37.16 -           ORELSE ares_tac [TrueI,ballI,allI,conjI,impI] 1));
   37.17 +           ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));
   37.18  
   37.19  (** New version of mk_rew_rules **)
   37.20  
   37.21 @@ -80,41 +80,19 @@
   37.22        | _ $ A => tryrules atomize_pairs A
   37.23    end;
   37.24  
   37.25 -fun ZF_mk_rew_rules th = map mk_eq (atomize th);
   37.26 +fun ZF_mk_rew_rules th = map mk_meta_eq (atomize th);
   37.27  
   37.28  
   37.29 -fun auto_tac rls hyps = SELECT_GOAL (DEPTH_SOLVE_1 (ares_tac (rls@hyps) 1));
   37.30 -
   37.31 -structure ZF_SimpData : SIMP_DATA =
   37.32 -  struct
   37.33 -  val refl_thms		= FOL_SimpData.refl_thms
   37.34 -  val trans_thms	= FOL_SimpData.trans_thms
   37.35 -  val red1		= FOL_SimpData.red1
   37.36 -  val red2		= FOL_SimpData.red2
   37.37 -  val mk_rew_rules	= ZF_mk_rew_rules 
   37.38 -  val norm_thms		= FOL_SimpData.norm_thms
   37.39 -  val subst_thms	= FOL_SimpData.subst_thms
   37.40 -  val dest_red		= FOL_SimpData.dest_red
   37.41 -  end;
   37.42 -
   37.43 -structure ZF_Simp = SimpFun(ZF_SimpData);
   37.44 -
   37.45 -open ZF_Simp;
   37.46 +val ZF_simps = [empty_subsetI, ball_simp, if_true, if_false, 
   37.47 +		beta, eta, restrict, fst_conv, snd_conv, split];
   37.48  
   37.49 -(*Redeclared because the previous FOL_ss belongs to a different instance
   37.50 -  of type simpset*)
   37.51 -val FOL_ss = empty_ss addcongs FOL_congs addrews FOL_rews 
   37.52 -		      setauto auto_tac[TrueI,ballI];
   37.53 -
   37.54 -(** Basic congruence and rewrite rules for ZF set theory **)
   37.55 +(*Sigma_cong, Pi_cong NOT included by default since they cause
   37.56 +  flex-flex pairs and the "Check your prover" error -- because most
   37.57 +  Sigma's and Pi's are abbreviated as * or -> *)
   37.58 +val ZF_congs =
   37.59 +   [ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong];
   37.60  
   37.61 -val ZF_congs = 
   37.62 -   [ball_cong,bex_cong,Replace_cong,RepFun_cong,Collect_cong,the_cong,
   37.63 -    if_cong,Sigma_cong,split_cong,Pi_cong,lam_cong] @ basic_ZF_congs;
   37.64 -
   37.65 -val ZF_rews = [empty_subsetI, ball_rew, if_true, if_false, 
   37.66 -	       beta, eta, restrict,
   37.67 -	       fst_conv, snd_conv, split];
   37.68 -
   37.69 -val ZF_ss = FOL_ss addcongs ZF_congs addrews (ZF_rews@mem_rews);
   37.70 -
   37.71 +val ZF_ss = FOL_ss 
   37.72 +      setmksimps ZF_mk_rew_rules
   37.73 +      addsimps (ZF_simps@mem_simps)
   37.74 +      addcongs ZF_congs;
    38.1 --- a/src/ZF/sum.ML	Fri Sep 17 12:53:53 1993 +0200
    38.2 +++ b/src/ZF/sum.ML	Fri Sep 17 16:16:38 1993 +0200
    38.3 @@ -83,7 +83,7 @@
    38.4  val sum_subset_iff = result();
    38.5  
    38.6  goal Sum.thy "A+B = C+D <-> A=C & B=D";
    38.7 -by (SIMP_TAC (ZF_ss addrews [extension,sum_subset_iff]) 1);
    38.8 +by (simp_tac (ZF_ss addsimps [extension,sum_subset_iff]) 1);
    38.9  by (fast_tac ZF_cs 1);
   38.10  val sum_equal_iff = result();
   38.11  
   38.12 @@ -99,12 +99,6 @@
   38.13  by (rtac cond_1 1);
   38.14  val case_Inr = result();
   38.15  
   38.16 -val prems = goalw Sum.thy [case_def]
   38.17 -    "[| u=u'; !!x. c(x)=c'(x);  !!y. d(y)=d'(y) |] ==>    \
   38.18 -\    case(c,d,u)=case(c',d',u')";
   38.19 -by (REPEAT (resolve_tac ([refl,split_cong,cond_cong] @ prems) 1));
   38.20 -val case_cong = result();
   38.21 -
   38.22  val major::prems = goal Sum.thy
   38.23      "[| u: A+B; \
   38.24  \       !!x. x: A ==> c(x): C(Inl(x));   \
   38.25 @@ -112,7 +106,7 @@
   38.26  \    |] ==> case(c,d,u) : C(u)";
   38.27  by (rtac (major RS sumE) 1);
   38.28  by (ALLGOALS (etac ssubst));
   38.29 -by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
   38.30 +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
   38.31  			    (prems@[case_Inl,case_Inr]))));
   38.32  val case_type = result();
   38.33  
    39.1 --- a/src/ZF/univ.ML	Fri Sep 17 12:53:53 1993 +0200
    39.2 +++ b/src/ZF/univ.ML	Fri Sep 17 16:16:38 1993 +0200
    39.3 @@ -11,7 +11,7 @@
    39.4  (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
    39.5  goal Univ.thy "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))";
    39.6  by (rtac (Vfrom_def RS def_transrec RS ssubst) 1);
    39.7 -by (SIMP_TAC ZF_ss 1);
    39.8 +by (simp_tac ZF_ss 1);
    39.9  val Vfrom = result();
   39.10  
   39.11  (** Monotonicity **)
   39.12 @@ -122,9 +122,8 @@
   39.13  
   39.14  goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
   39.15  by (rtac (Vfrom RS trans) 1);
   39.16 -brs ([refl] RL ZF_congs) 1;
   39.17 -by (rtac equalityI 1);
   39.18 -by (rtac (succI1 RS RepFunI RS Union_upper) 2);
   39.19 +by (rtac (succI1 RS RepFunI RS Union_upper RSN
   39.20 +	      (2, equalityI RS subst_context)) 1);
   39.21  by (rtac UN_least 1);
   39.22  by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1);
   39.23  by (etac member_succD 1);
   39.24 @@ -473,16 +472,16 @@
   39.25  val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [rank_trans]));
   39.26  
   39.27  val rank_ss = ZF_ss 
   39.28 -    addrews [split, case_Inl, case_Inr, Vset_rankI]
   39.29 -    addrews rank_trans_rls;
   39.30 +    addsimps [case_Inl, case_Inr, Vset_rankI]
   39.31 +    addsimps rank_trans_rls;
   39.32  
   39.33  (** Recursion over Vset levels! **)
   39.34  
   39.35  (*NOT SUITABLE FOR REWRITING: recursive!*)
   39.36  goalw Univ.thy [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))";
   39.37  by (rtac (transrec RS ssubst) 1);
   39.38 -by (SIMP_TAC (wf_ss addrews [Ord_rank, Ord_succ, Vset_D RS beta, 
   39.39 -			     VsetI RS beta]) 1);
   39.40 +by (simp_tac (ZF_ss addsimps [Ord_rank, Ord_succ, Vset_D RS beta, 
   39.41 +			      VsetI RS beta]) 1);
   39.42  val Vrec = result();
   39.43  
   39.44  (*This form avoids giant explosions in proofs.  NOTE USE OF == *)
   39.45 @@ -493,13 +492,6 @@
   39.46  by (rtac Vrec 1);
   39.47  val def_Vrec = result();
   39.48  
   39.49 -val prems = goalw Univ.thy [Vrec_def]
   39.50 -    "[| a=a';  !!x u. H(x,u)=H'(x,u) |]  ==> Vrec(a,H)=Vrec(a',H')";
   39.51 -val Vrec_ss = ZF_ss addcongs ([transrec_cong] @ mk_congs Univ.thy ["rank"])
   39.52 -		      addrews (prems RL [sym]);
   39.53 -by (SIMP_TAC Vrec_ss 1);
   39.54 -val Vrec_cong = result();
   39.55 -
   39.56  
   39.57  (*** univ(A) ***)
   39.58  
    40.1 --- a/src/ZF/upair.ML	Fri Sep 17 12:53:53 1993 +0200
    40.2 +++ b/src/ZF/upair.ML	Fri Sep 17 16:16:38 1993 +0200
    40.3 @@ -167,10 +167,6 @@
    40.4      (resolve_tac [major RS the_equality2 RS ssubst] 1),
    40.5      (REPEAT (assume_tac 1)) ]);
    40.6  
    40.7 -val the_cong = prove_goalw ZF.thy [the_def]
    40.8 -    "[| !!y. P(y) <-> Q(y) |] ==> (THE x. P(x)) = (THE x. Q(x))"
    40.9 - (fn prems=> [ (prove_cong_tac (prems@[Replace_cong]) 1) ]);
   40.10 -
   40.11  
   40.12  (*** if -- a conditional expression for formulae ***)
   40.13  
   40.14 @@ -182,38 +178,34 @@
   40.15  by (fast_tac (lemmas_cs addIs [the_equality]) 1);
   40.16  val if_false = result();
   40.17  
   40.18 +(*Never use with case splitting, or if P is known to be true or false*)
   40.19  val prems = goalw ZF.thy [if_def]
   40.20 -    "[| P<->Q;  a=c;  b=d |] ==> if(P,a,b) = if(Q,c,d)";
   40.21 -by (REPEAT (resolve_tac (prems@[refl,the_cong]@FOL_congs) 1));
   40.22 +    "[| P<->Q;  Q ==> a=c;  ~Q ==> b=d |] ==> if(P,a,b) = if(Q,c,d)";
   40.23 +by (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1);
   40.24  val if_cong = result();
   40.25  
   40.26  (*Not needed for rewriting, since P would rewrite to True anyway*)
   40.27 -val prems = goalw ZF.thy [if_def] "P ==> if(P,a,b) = a";
   40.28 -by (cut_facts_tac prems 1);
   40.29 +goalw ZF.thy [if_def] "!!P. P ==> if(P,a,b) = a";
   40.30  by (fast_tac (lemmas_cs addSIs [the_equality]) 1);
   40.31  val if_P = result();
   40.32  
   40.33  (*Not needed for rewriting, since P would rewrite to False anyway*)
   40.34 -val prems = goalw ZF.thy [if_def] "~P ==> if(P,a,b) = b";
   40.35 -by (cut_facts_tac prems 1);
   40.36 +goalw ZF.thy [if_def] "!!P. ~P ==> if(P,a,b) = b";
   40.37  by (fast_tac (lemmas_cs addSIs [the_equality]) 1);
   40.38  val if_not_P = result();
   40.39  
   40.40 -val if_ss =
   40.41 -    FOL_ss addcongs (if_cong :: mk_typed_congs ZF.thy [("P", "i=>o")]
   40.42 -			      @ basic_ZF_congs)
   40.43 -	   addrews  [if_true,if_false];
   40.44 +val if_ss = FOL_ss addsimps  [if_true,if_false];
   40.45  
   40.46  val expand_if = prove_goal ZF.thy
   40.47      "P(if(Q,x,y)) <-> ((Q --> P(x)) & (~Q --> P(y)))"
   40.48   (fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1),
   40.49 -	   (ASM_SIMP_TAC if_ss 1),
   40.50 -	   (ASM_SIMP_TAC if_ss 1) ]);
   40.51 +	   (asm_simp_tac if_ss 1),
   40.52 +	   (asm_simp_tac if_ss 1) ]);
   40.53  
   40.54  val prems = goal ZF.thy
   40.55      "[| P ==> a: A;  ~P ==> b: A |] ==> if(P,a,b): A";
   40.56  by (res_inst_tac [("Q","P")] (excluded_middle RS disjE) 1);
   40.57 -by (ALLGOALS (ASM_SIMP_TAC (if_ss addrews prems)));
   40.58 +by (ALLGOALS (asm_simp_tac (if_ss addsimps prems)));
   40.59  val if_type = result();
   40.60  
   40.61  
    41.1 --- a/src/ZF/wf.ML	Fri Sep 17 12:53:53 1993 +0200
    41.2 +++ b/src/ZF/wf.ML	Fri Sep 17 16:16:38 1993 +0200
    41.3 @@ -19,10 +19,6 @@
    41.4  
    41.5  open WF;
    41.6  
    41.7 -val [H_cong] = mk_typed_congs WF.thy[("H","[i,i]=>i")];
    41.8 -
    41.9 -val wf_ss = ZF_ss addcongs [H_cong];
   41.10 -
   41.11  
   41.12  (*** Well-founded relations ***)
   41.13  
   41.14 @@ -138,13 +134,13 @@
   41.15  (*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE
   41.16    spec RS mp  instantiates induction hypotheses*)
   41.17  fun indhyp_tac hyps =
   41.18 -    ares_tac (TrueI::hyps) ORELSE' 
   41.19 +    resolve_tac (TrueI::refl::hyps) ORELSE' 
   41.20      (cut_facts_tac hyps THEN'
   41.21         DEPTH_SOLVE_1 o (ares_tac [TrueI, ballI] ORELSE'
   41.22  		        eresolve_tac [underD, transD, spec RS mp]));
   41.23  
   41.24 -(*** NOTE! some simplifications need a different auto_tac!! ***)
   41.25 -val wf_super_ss = wf_ss setauto indhyp_tac;
   41.26 +(*** NOTE! some simplifications need a different solver!! ***)
   41.27 +val wf_super_ss = ZF_ss setsolver indhyp_tac;
   41.28  
   41.29  val prems = goalw WF.thy [is_recfun_def]
   41.30      "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |] ==> \
   41.31 @@ -153,7 +149,7 @@
   41.32  by (wf_ind_tac "x" prems 1);
   41.33  by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
   41.34  by (rewtac restrict_def);
   41.35 -by (ASM_SIMP_TAC (wf_super_ss addrews [vimage_singleton_iff]) 1);
   41.36 +by (asm_simp_tac (wf_super_ss addsimps [vimage_singleton_iff]) 1);
   41.37  val is_recfun_equal_lemma = result();
   41.38  val is_recfun_equal = standard (is_recfun_equal_lemma RS mp RS mp);
   41.39  
   41.40 @@ -165,7 +161,7 @@
   41.41  by (rtac (consI1 RS restrict_type RS fun_extension) 1);
   41.42  by (etac is_recfun_type 1);
   41.43  by (ALLGOALS
   41.44 -    (ASM_SIMP_TAC (wf_super_ss addrews
   41.45 +    (asm_simp_tac (wf_super_ss addsimps
   41.46  		   [ [wfr,transr,recf,recg] MRS is_recfun_equal ])));
   41.47  val is_recfun_cut = result();
   41.48  
   41.49 @@ -195,13 +191,13 @@
   41.50  by (REPEAT (assume_tac 2));
   41.51  by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
   41.52  (*Applying the substitution: must keep the quantified assumption!!*)
   41.53 -by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong, H_cong] 1));
   41.54 +by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong] 1));
   41.55  by (fold_tac [is_recfun_def]);
   41.56 -by (rtac (consI1 RS restrict_type RSN (2,fun_extension)) 1);
   41.57 +by (rtac (consI1 RS restrict_type RSN (2,fun_extension) RS subst_context) 1);
   41.58  by (rtac is_recfun_type 1);
   41.59  by (ALLGOALS
   41.60 -    (ASM_SIMP_TAC
   41.61 -     (wf_super_ss addrews [underI RS beta, apply_recfun, is_recfun_cut])));
   41.62 +    (asm_simp_tac
   41.63 +     (wf_super_ss addsimps [underI RS beta, apply_recfun, is_recfun_cut])));
   41.64  val unfold_the_recfun = result();
   41.65  
   41.66  
   41.67 @@ -214,13 +210,12 @@
   41.68  val the_recfun_cut = result();
   41.69  
   41.70  (*NOT SUITABLE FOR REWRITING since it is recursive!*)
   41.71 -val prems = goalw WF.thy [wftrec_def]
   41.72 -    "[| wf(r);  trans(r) |] ==> \
   41.73 -\    wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))";
   41.74 +goalw WF.thy [wftrec_def]
   41.75 +    "!!r. [| wf(r);  trans(r) |] ==> \
   41.76 +\         wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))";
   41.77  by (rtac (rewrite_rule [is_recfun_def] unfold_the_recfun RS ssubst) 1);
   41.78 -by (ALLGOALS (ASM_SIMP_TAC
   41.79 -	      (wf_ss addrews (prems@[vimage_singleton_iff RS iff_sym, 
   41.80 -				     the_recfun_cut]))));
   41.81 +by (ALLGOALS (asm_simp_tac
   41.82 +	(ZF_ss addsimps [vimage_singleton_iff RS iff_sym, the_recfun_cut])));
   41.83  val wftrec = result();
   41.84  
   41.85  (** Removal of the premise trans(r) **)
   41.86 @@ -230,8 +225,7 @@
   41.87      "wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))";
   41.88  by (rtac (wfr RS wf_trancl RS wftrec RS ssubst) 1);
   41.89  by (rtac trans_trancl 1);
   41.90 -by (rtac (refl RS H_cong) 1);
   41.91 -by (rtac (vimage_pair_mono RS restrict_lam_eq) 1);
   41.92 +by (rtac (vimage_pair_mono RS restrict_lam_eq RS subst_context) 1);
   41.93  by (etac r_into_trancl 1);
   41.94  by (rtac subset_refl 1);
   41.95  val wfrec = result();
   41.96 @@ -253,10 +247,3 @@
   41.97  by (REPEAT (ares_tac (prems@[lam_type]) 1
   41.98       ORELSE eresolve_tac [spec RS mp, underD] 1));
   41.99  val wfrec_type = result();
  41.100 -
  41.101 -val prems = goalw WF.thy [wfrec_def,wftrec_def,the_recfun_def,is_recfun_def]
  41.102 -    "[| r=r';  !!x u. H(x,u)=H'(x,u);  a=a' |] \
  41.103 -\    ==> wfrec(r,a,H)=wfrec(r',a',H')";
  41.104 -by (EVERY1 (map rtac (prems RL [subst])));
  41.105 -by (SIMP_TAC (wf_ss addrews (prems RL [sym])) 1);
  41.106 -val wfrec_cong = result();
    42.1 --- a/src/ZF/zf.ML	Fri Sep 17 12:53:53 1993 +0200
    42.2 +++ b/src/ZF/zf.ML	Fri Sep 17 16:16:38 1993 +0200
    42.3 @@ -13,9 +13,8 @@
    42.4    val ballE : thm
    42.5    val ballI : thm
    42.6    val ball_cong : thm
    42.7 -  val ball_rew : thm
    42.8 +  val ball_simp : thm
    42.9    val ball_tac : int -> tactic
   42.10 -  val basic_ZF_congs : thm list
   42.11    val bexCI : thm
   42.12    val bexE : thm
   42.13    val bexI : thm
   42.14 @@ -45,7 +44,6 @@
   42.15    val lemmas_cs : claset
   42.16    val PowD : thm
   42.17    val PowI : thm
   42.18 -  val prove_cong_tac : thm list -> int -> tactic
   42.19    val RepFunE : thm
   42.20    val RepFunI : thm
   42.21    val RepFun_eqI : thm
   42.22 @@ -75,14 +73,6 @@
   42.23  structure ZF_Lemmas : ZF_LEMMAS = 
   42.24  struct
   42.25  
   42.26 -val basic_ZF_congs = mk_congs ZF.thy 
   42.27 -    ["op `", "op ``", "op Int", "op Un", "op -", "op <=", "op :", 
   42.28 -     "Pow", "Union", "Inter", "fst", "snd", "succ", "Pair", "Upair", "cons",
   42.29 -     "domain", "range", "restrict"];
   42.30 -
   42.31 -fun prove_cong_tac prems i =
   42.32 -    REPEAT (ares_tac (prems@[refl]@FOL_congs@basic_ZF_congs) i);
   42.33 -
   42.34  (*** Bounded universal quantifier ***)
   42.35  
   42.36  val ballI = prove_goalw ZF.thy [Ball_def]
   42.37 @@ -118,14 +108,13 @@
   42.38  val ball_tac = dtac bspec THEN' assume_tac;
   42.39  
   42.40  (*Trival rewrite rule;   (ALL x:A.P)<->P holds only if A is nonempty!*)
   42.41 -val ball_rew = prove_goal ZF.thy "(ALL x:A. True) <-> True"
   42.42 - (fn prems=> [ (REPEAT (ares_tac [TrueI,ballI,iffI] 1)) ]);
   42.43 +val ball_simp = prove_goal ZF.thy "(ALL x:A. True) <-> True"
   42.44 + (fn _=> [ (REPEAT (ares_tac [TrueI,ballI,iffI] 1)) ]);
   42.45  
   42.46  (*Congruence rule for rewriting*)
   42.47  val ball_cong = prove_goalw ZF.thy [Ball_def]
   42.48 -    "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) \
   42.49 -\    |] ==> (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))"
   42.50 - (fn prems=> [ (prove_cong_tac prems 1) ]);
   42.51 +    "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> Ball(A,P) <-> Ball(A',P')"
   42.52 + (fn prems=> [ (simp_tac (FOL_ss addsimps prems) 1) ]);
   42.53  
   42.54  (*** Bounded existential quantifier ***)
   42.55  
   42.56 @@ -151,8 +140,8 @@
   42.57  
   42.58  val bex_cong = prove_goalw ZF.thy [Bex_def]
   42.59      "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) \
   42.60 -\    |] ==> (EX x:A. P(x)) <-> (EX x:A'. P'(x))"
   42.61 - (fn prems=> [ (prove_cong_tac prems 1) ]);
   42.62 +\    |] ==> Bex(A,P) <-> Bex(A',P')"
   42.63 + (fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ]);
   42.64  
   42.65  (*** Rules for subsets ***)
   42.66  
   42.67 @@ -265,7 +254,7 @@
   42.68  
   42.69  val Replace_cong = prove_goal ZF.thy
   42.70      "[| A=B;  !!x y. x:B ==> P(x,y) <-> Q(x,y) |] ==> \
   42.71 -\    {y. x:A, P(x,y)} = {y. x:B, Q(x,y)}"
   42.72 +\    Replace(A,P) = Replace(B,Q)"
   42.73   (fn prems=>
   42.74     let val substprems = prems RL [subst, ssubst]
   42.75         and iffprems = prems RL [iffD1,iffD2]
   42.76 @@ -275,7 +264,6 @@
   42.77  	 ORELSE (resolve_tac iffprems 1 THEN assume_tac 2))) ]
   42.78     end);
   42.79  
   42.80 -
   42.81  (*** Rules for RepFun ***)
   42.82  
   42.83  val RepFunI = prove_goalw ZF.thy [RepFun_def]
   42.84 @@ -296,9 +284,8 @@
   42.85      (REPEAT (ares_tac prems 1)) ]);
   42.86  
   42.87  val RepFun_cong = prove_goalw ZF.thy [RepFun_def]
   42.88 -    "[| A=B;  !!x. x:B ==> f(x)=g(x) |] ==> \
   42.89 -\    {f(x). x:A} = {g(x). x:B}"
   42.90 - (fn prems=> [ (prove_cong_tac (prems@[Replace_cong]) 1) ]);
   42.91 +    "[| A=B;  !!x. x:B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)"
   42.92 + (fn prems=> [ (simp_tac (FOL_ss addcongs [Replace_cong] addsimps prems) 1) ]);
   42.93  
   42.94  
   42.95  (*** Rules for Collect -- forming a subset by separation ***)
   42.96 @@ -332,9 +319,8 @@
   42.97      (assume_tac 1) ]);
   42.98  
   42.99  val Collect_cong = prove_goalw ZF.thy [Collect_def] 
  42.100 -    "[| A=B;  !!x. x:B ==> P(x) <-> Q(x) |] ==> \
  42.101 -\    {x:A. P(x)} = {x:B. Q(x)}"
  42.102 - (fn prems=> [ (prove_cong_tac (prems@[Replace_cong]) 1) ]);
  42.103 +    "[| A=B;  !!x. x:B ==> P(x) <-> Q(x) |] ==> Collect(A,P) = Collect(B,Q)"
  42.104 + (fn prems=> [ (simp_tac (FOL_ss addcongs [Replace_cong] addsimps prems) 1) ]);
  42.105  
  42.106  (*** Rules for Unions ***)
  42.107