--- a/src/ZF/Resid/Cube.ML Mon Sep 21 23:25:27 1998 +0200
+++ b/src/ZF/Resid/Cube.ML Tue Sep 22 13:48:32 1998 +0200
@@ -7,9 +7,8 @@
open Cube;
-val prism_ss = (res1L_ss addsimps
- [commutation,residuals_preserve_comp,sub_preserve_reg,
- residuals_preserve_reg,sub_comp,sub_comp RS comp_sym]);
+Addsimps [commutation, residuals_preserve_comp, sub_preserve_reg,
+ residuals_preserve_reg, sub_comp, sub_comp RS comp_sym];
(* ------------------------------------------------------------------------- *)
(* Prism theorem *)
@@ -18,24 +17,17 @@
(* Having more assumptions than needed -- removed below *)
Goal "v<==u ==> \
-\ regular(u)-->(ALL w. w~v-->w~u--> \
-\ w |> u = (w|>v) |> (u|>v))";
+\ regular(u) --> (ALL w. w~v --> w~u --> \
+\ w |> u = (w|>v) |> (u|>v))";
by (etac Ssub.induct 1);
-by (ALLGOALS (asm_simp_tac prism_ss));
-by (dresolve_tac [spec RS mp RS mp] 1 THEN resolve_tac [Scomp.Comp_Fun] 1
- THEN resolve_tac [Scomp.Comp_Fun] 2 THEN (REPEAT(assume_tac 1)));
-by (asm_full_simp_tac prism_ss 1);
-by (dresolve_tac [spec RS mp RS mp] 1 THEN resolve_tac [Scomp.Comp_Fun] 1
- THEN resolve_tac [Scomp.Comp_Fun] 2 THEN (REPEAT(assume_tac 1)));
-by (asm_full_simp_tac prism_ss 1);
+by Auto_tac;
qed_spec_mp "prism_l";
Goal "[|v <== u; regular(u); w~v|]==> \
\ w |> u = (w|>v) |> (u|>v)";
by (rtac prism_l 1);
by (rtac comp_trans 4);
-by (assume_tac 4);
-by (ALLGOALS(asm_simp_tac prism_ss));
+by Auto_tac;
qed "prism";
@@ -53,9 +45,9 @@
by (asm_full_simp_tac (simpset() addsimps
[prism RS sym,union_l,union_preserve_regular,
comp_sym_iff, union_sym]) 4);
-by (asm_full_simp_tac (simpset() addsimps [union_r, comp_sym_iff]) 1);
-by (asm_full_simp_tac (simpset() addsimps
- [union_preserve_regular, comp_sym_iff]) 1);
+by (asm_simp_tac (simpset() addsimps [union_r, comp_sym_iff]) 1);
+by (asm_simp_tac (simpset() addsimps
+ [union_preserve_regular, comp_sym_iff]) 1);
by (etac comp_trans 1);
by (atac 1);
qed "cube";
@@ -71,7 +63,7 @@
by (subgoal_tac "u~v" 1);
by (safe_tac (claset() addSIs [exI]));
by (rtac cube 1);
-by (ALLGOALS (asm_simp_tac (prism_ss addsimps [comp_sym_iff])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [comp_sym_iff])));
by (ALLGOALS (blast_tac (claset() addIs [residuals_preserve_comp,
comp_trans, comp_sym])));
qed "paving";
--- a/src/ZF/Resid/Reduction.ML Mon Sep 21 23:25:27 1998 +0200
+++ b/src/ZF/Resid/Reduction.ML Tue Sep 22 13:48:32 1998 +0200
@@ -31,7 +31,6 @@
[Spar_red.one_step, substL_type, redD1, redD2, par_redD1,
par_redD2, par_red1D2, unmark_type]);
-val reducL_ss = simpset() setloop (SELECT_GOAL Safe_tac);
(* ------------------------------------------------------------------------- *)
(* Lemmas for reduction *)
@@ -73,7 +72,7 @@
Goal "m:lambda==> m =1=> m";
-by (eresolve_tac [lambda.induct] 1);
+by (etac lambda.induct 1);
by (ALLGOALS (Asm_simp_tac ));
qed "refl_par_red1";
@@ -113,17 +112,16 @@
(* commuting of unmark and subst *)
(* ------------------------------------------------------------------------- *)
-Goal "u:redexes ==> \
-\ ALL k:nat. unmark(lift_rec(u,k)) = lift_rec(unmark(u),k)";
-by (eresolve_tac [redexes.induct] 1);
-by (ALLGOALS (asm_full_simp_tac (addsplit (simpset()))));
+Goal "u:redexes ==> ALL k:nat. unmark(lift_rec(u,k)) = lift_rec(unmark(u),k)";
+by (etac redexes.induct 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [lift_rec_Var])));
qed "unmmark_lift_rec";
Goal "v:redexes ==> ALL k:nat. ALL u:redexes. \
\ unmark(subst_rec(u,v,k)) = subst_rec(unmark(u),unmark(v),k)";
-by (eresolve_tac [redexes.induct] 1);
-by (ALLGOALS (asm_full_simp_tac
- ((addsplit (simpset())) addsimps [unmmark_lift_rec])));
+by (etac redexes.induct 1);
+by (ALLGOALS (asm_simp_tac
+ (simpset() addsimps [unmmark_lift_rec, subst_Var])));
qed "unmmark_subst_rec";
@@ -133,9 +131,10 @@
Goal "u~v ==> regular(v) --> unmark(u) =1=> unmark(u|>v)";
by (etac Scomp.induct 1);
-by (ALLGOALS (asm_full_simp_tac (reducL_ss addsimps [unmmark_subst_rec]) ));
+by (auto_tac (claset(),
+ simpset() addsimps [unmmark_subst_rec]));
by (dres_inst_tac [("psi", "Fun(?u) =1=> ?w")] asm_rl 1);
-by (asm_full_simp_tac reducL_ss 1);
+by Auto_tac;
qed_spec_mp "completeness_l";
Goal "[|u:lambda; u~v; regular(v)|]==> u =1=> unmark(u|>v)";
--- a/src/ZF/Resid/Residuals.ML Mon Sep 21 23:25:27 1998 +0200
+++ b/src/ZF/Resid/Residuals.ML Tue Sep 22 13:48:32 1998 +0200
@@ -9,8 +9,7 @@
(* Setting up rule lists *)
(* ------------------------------------------------------------------------- *)
-AddIs (Sres.intrs @ redexes.intrs @ Sreg.intrs @
- [subst_type] @ nat_typechecks);
+AddIs (Sres.intrs @ redexes.intrs @ Sreg.intrs @ [subst_type]);
AddSEs (redexes.free_SEs @
(map (Sres.mk_cases redexes.con_defs)
["residuals(Var(n),Var(n),v)",
@@ -93,13 +92,11 @@
Goal "[|s~t; regular(t)|]==> regular(t) --> s |> t:redexes";
by (etac Scomp.induct 1);
-by (ALLGOALS (asm_full_simp_tac
- (simpset() addsimps [res_Var,res_Fun,res_App,res_redex]
- setloop (SELECT_GOAL Safe_tac))));
+by (auto_tac (claset(),
+ simpset() addsimps [res_Var,res_Fun,res_App,res_redex]));
by (dres_inst_tac [("psi", "Fun(?u) |> ?v : redexes")] asm_rl 1);
-by (asm_full_simp_tac
- (simpset() addsimps [res_Fun]
- setloop (SELECT_GOAL Safe_tac)) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [res_Fun]));
qed "resfunc_type";
Addsimps ([res_Var, res_Fun, res_App, res_redex, lift_rec_preserve_comp,
@@ -107,7 +104,6 @@
subst_rec_preserve_reg] @
redexes.free_iffs);
-val res1L_ss = simpset() setloop (SELECT_GOAL Safe_tac);
(* ------------------------------------------------------------------------- *)
(* Commutation theorem *)
@@ -120,15 +116,17 @@
Goal "u<==v ==> regular(v) --> regular(u)";
by (etac Ssub.induct 1);
-by (ALLGOALS (asm_simp_tac res1L_ss));
-qed "sub_preserve_reg";
+by Auto_tac;
+qed_spec_mp "sub_preserve_reg";
Goal "[|u~v; k:nat|]==> regular(v)--> (ALL n:nat. \
\ lift_rec(u,n) |> lift_rec(v,n) = lift_rec(u |> v,n))";
by (etac Scomp.induct 1);
by Safe_tac;
-by (ALLGOALS (asm_full_simp_tac ((addsplit (simpset())) addsimps [lift_subst])));
-by (dres_inst_tac [("psi", "ALL x:nat. Fun(?u(x)) |> ?v(x) = ?w(x)")] asm_rl 1);
+by (ALLGOALS
+ (asm_simp_tac
+ (simpset() addsimps [lift_rec_Var,subst_Var,lift_subst])));
+by (rotate_tac ~2 1);
by (Asm_full_simp_tac 1);
qed "residuals_lift_rec";
@@ -138,15 +136,16 @@
by (etac Scomp.induct 1);
by Safe_tac;
by (ALLGOALS
- (asm_full_simp_tac ((addsplit (simpset())) addsimps ([residuals_lift_rec]))));
+ (asm_simp_tac
+ (simpset() addsimps [lift_rec_Var,subst_Var,residuals_lift_rec])));
by (dres_inst_tac [("psi", "ALL x.?P(x)")] asm_rl 1);
-by (asm_full_simp_tac (simpset() addsimps ([substitution])) 1);
+by (asm_full_simp_tac (simpset() addsimps [substitution]) 1);
qed "residuals_subst_rec";
Goal "[|u1~u2; v1~v2; regular(u2); regular(v2)|]==>\
\ (v1/u1) |> (v2/u2) = (v1 |> v2)/(u1 |> u2)";
-by (asm_simp_tac (simpset() addsimps ([residuals_subst_rec])) 1);
+by (asm_simp_tac (simpset() addsimps [residuals_subst_rec]) 1);
qed "commutation";
(* ------------------------------------------------------------------------- *)
@@ -155,12 +154,7 @@
Goal "u~v ==> ALL w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)";
by (etac Scomp.induct 1);
-by (ALLGOALS (asm_simp_tac res1L_ss));
-by (dresolve_tac [spec RS mp RS mp RS mp] 1
- THEN resolve_tac Scomp.intrs 1 THEN resolve_tac Scomp.intrs 2
- THEN resolve_tac Sreg.intrs 3);
-by (REPEAT(assume_tac 1));
-by (asm_full_simp_tac res1L_ss 1);
+by Auto_tac;
qed_spec_mp "residuals_preserve_comp";
@@ -168,8 +162,8 @@
by (etac Scomp.induct 1);
by Safe_tac;
by (TRYALL (dres_inst_tac [("psi", "regular(Fun(?u) |> ?v)")] asm_rl));
-by (ALLGOALS (asm_full_simp_tac res1L_ss));
-qed "residuals_preserve_reg";
+by Auto_tac;
+qed_spec_mp "residuals_preserve_reg";
(* ------------------------------------------------------------------------- *)
(* Preservation lemma *)
@@ -177,15 +171,15 @@
Goal "u~v ==> v ~ (u un v)";
by (etac Scomp.induct 1);
-by (ALLGOALS Asm_full_simp_tac);
+by (ALLGOALS Asm_simp_tac);
qed "union_preserve_comp";
Goal "u ~ v ==> regular(v) --> u|>v = (u un v)|>v";
by (etac Scomp.induct 1);
by Safe_tac;
by (dres_inst_tac [("psi", "Fun(?u) |> ?v = ?w")] asm_rl 3);
-by (ALLGOALS (asm_full_simp_tac (res1L_ss addsimps
- [union_preserve_comp,comp_sym_iff])));
+by (auto_tac (claset(),
+ simpset() addsimps [union_preserve_comp,comp_sym_iff]));
by (asm_full_simp_tac (simpset() addsimps
[union_preserve_comp RS comp_sym,
comp_sym RS union_preserve_comp RS comp_sym]) 1);
--- a/src/ZF/Resid/SubUnion.ML Mon Sep 21 23:25:27 1998 +0200
+++ b/src/ZF/Resid/SubUnion.ML Tue Sep 22 13:48:32 1998 +0200
@@ -66,7 +66,7 @@
(* ------------------------------------------------------------------------- *)
Goal "u:redexes ==> u ~ u";
-by (eresolve_tac [redexes.induct] 1);
+by (etac redexes.induct 1);
by (ALLGOALS Fast_tac);
qed "comp_refl";
@@ -92,13 +92,13 @@
Goal "u ~ v ==> u <== (u un v)";
by (etac Scomp.induct 1);
by (etac boolE 3);
-by (ALLGOALS Asm_full_simp_tac);
+by (ALLGOALS Asm_simp_tac);
qed "union_l";
Goal "u ~ v ==> v <== (u un v)";
by (etac Scomp.induct 1);
by (eres_inst_tac [("c","b2")] boolE 3);
-by (ALLGOALS Asm_full_simp_tac);
+by (ALLGOALS Asm_simp_tac);
qed "union_r";
Goal "u ~ v ==> u un v = v un u";
@@ -112,8 +112,7 @@
Goal "u ~ v ==> regular(u)-->regular(v)-->regular(u un v)";
by (etac Scomp.induct 1);
-by (ALLGOALS(asm_full_simp_tac
- (simpset() setloop(SELECT_GOAL Safe_tac))));
+by Auto_tac;
by (dres_inst_tac [("psi", "regular(Fun(?u) un ?v)")] asm_rl 1);
by (Asm_full_simp_tac 1);
qed_spec_mp "union_preserve_regular";
--- a/src/ZF/Resid/Substitution.ML Mon Sep 21 23:25:27 1998 +0200
+++ b/src/ZF/Resid/Substitution.ML Tue Sep 22 13:48:32 1998 +0200
@@ -44,29 +44,29 @@
(* ------------------------------------------------------------------------- *)
Goalw [lift_rec_def]
"[|n:nat; i:nat|]==> lift_rec(Var(i),n) =if(i<n,Var(i),Var(succ(i)))";
-by (Asm_full_simp_tac 1);
+by (Asm_simp_tac 1);
qed "lift_rec_Var";
Goalw [lift_rec_def]
"[|n:nat; i:nat; k:nat; k le i|]==> lift_rec(Var(i),k) = Var(succ(i))";
-by (Asm_full_simp_tac 1);
+by (Asm_simp_tac 1);
qed "lift_rec_le";
Goalw [lift_rec_def]
"[|i:nat; k:nat; i<k |]==> lift_rec(Var(i),k) = Var(i)";
-by (Asm_full_simp_tac 1);
+by (Asm_simp_tac 1);
qed "lift_rec_gt";
Goalw [lift_rec_def]
"[|n:nat; k:nat|]==> \
\ lift_rec(Fun(t),k) = Fun(lift_rec(t,succ(k)))";
-by (Asm_full_simp_tac 1);
+by (Asm_simp_tac 1);
qed "lift_rec_Fun";
Goalw [lift_rec_def]
"[|n:nat; k:nat|]==> \
\ lift_rec(App(b,f,a),k) = App(b,lift_rec(f,k),lift_rec(a,k))";
-by (Asm_full_simp_tac 1);
+by (Asm_simp_tac 1);
qed "lift_rec_App";
(* ------------------------------------------------------------------------- *)
@@ -76,59 +76,57 @@
Goalw [subst_rec_def]
"[|i:nat; k:nat; u:redexes|]==> \
\ subst_rec(u,Var(i),k) = if(k<i,Var(i #- 1),if(k=i,u,Var(i)))";
-by (asm_full_simp_tac (simpset() addsimps [gt_not_eq,leI]) 1);
+by (asm_simp_tac (simpset() addsimps [gt_not_eq,leI]) 1);
qed "subst_Var";
Goalw [subst_rec_def]
"[|n:nat; u:redexes|]==> subst_rec(u,Var(n),n) = u";
-by (asm_full_simp_tac (simpset()) 1);
+by (Asm_simp_tac 1);
qed "subst_eq";
Goalw [subst_rec_def]
"[|n:nat; u:redexes; p:nat; p<n|]==> \
\ subst_rec(u,Var(n),p) = Var(n #- 1)";
-by (asm_full_simp_tac (simpset()) 1);
+by (Asm_simp_tac 1);
qed "subst_gt";
Goalw [subst_rec_def]
"[|n:nat; u:redexes; p:nat; n<p|]==> \
\ subst_rec(u,Var(n),p) = Var(n)";
-by (asm_full_simp_tac (simpset() addsimps [gt_not_eq,leI]) 1);
+by (asm_simp_tac (simpset() addsimps [gt_not_eq,leI]) 1);
qed "subst_lt";
Goalw [subst_rec_def]
"[|p:nat; u:redexes|]==> \
\ subst_rec(u,Fun(t),p) = Fun(subst_rec(lift(u),t,succ(p))) ";
-by (asm_full_simp_tac (simpset()) 1);
+by (Asm_simp_tac 1);
qed "subst_Fun";
Goalw [subst_rec_def]
"[|p:nat; u:redexes|]==> \
\ subst_rec(u,App(b,f,a),p) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))";
-by (asm_full_simp_tac (simpset()) 1);
+by (Asm_simp_tac 1);
qed "subst_App";
-fun addsplit ss = (ss setloop (split_inside_tac [split_if])
- addsimps [lift_rec_Var,subst_Var]);
-
+Addsimps [subst_Fun, subst_App];
Goal "u:redexes ==> ALL k:nat. lift_rec(u,k):redexes";
-by (eresolve_tac [redexes.induct] 1);
-by (ALLGOALS(asm_full_simp_tac
- ((addsplit (simpset())) addsimps [lift_rec_Fun,lift_rec_App])));
+by (etac redexes.induct 1);
+by (ALLGOALS
+ (asm_simp_tac (simpset() addsimps [lift_rec_Var,
+ lift_rec_Fun, lift_rec_App])));
qed "lift_rec_type_a";
val lift_rec_type = lift_rec_type_a RS bspec;
Goal "v:redexes ==> ALL n:nat. ALL u:redexes. subst_rec(u,v,n):redexes";
-by (eresolve_tac [redexes.induct] 1);
-by (ALLGOALS(asm_full_simp_tac
- ((addsplit (simpset())) addsimps [subst_Fun,subst_App,
- lift_rec_type])));
+by (etac redexes.induct 1);
+by (ALLGOALS(asm_simp_tac
+ (simpset() addsimps [subst_Var, lift_rec_type])));
qed "subst_type_a";
val subst_type = subst_type_a RS bspec RS bspec;
-Addsimps [subst_eq, subst_gt, subst_lt, subst_Fun, subst_App, subst_type,
+Addsimps [subst_eq, subst_gt, subst_lt, subst_type,
lift_rec_le, lift_rec_gt, lift_rec_Fun, lift_rec_App,
lift_rec_type];
@@ -139,11 +137,11 @@
Goal "u:redexes ==> ALL n:nat. ALL i:nat. i le n --> \
\ (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))";
-by ((eresolve_tac [redexes.induct] 1) THEN (ALLGOALS Asm_simp_tac));
+by ((etac redexes.induct 1) THEN (ALLGOALS Asm_simp_tac));
by Safe_tac;
-by (excluded_middle_tac "n < xa" 1);
-by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2));
-by (ALLGOALS (asm_full_simp_tac (addsplit (simpset()) addsimps [leI])));
+by (case_tac "n < xa" 1);
+by ((forward_tac [lt_trans2] 1) THEN (assume_tac 1));
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lift_rec_Var, leI])));
qed "lift_lift_rec";
@@ -156,24 +154,25 @@
\ ALL n:nat. ALL m:nat. ALL u:redexes. n le m-->\
\ lift_rec(subst_rec(u,v,n),m) = \
\ subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)";
-by ((eresolve_tac [redexes.induct] 1)
+by ((etac redexes.induct 1)
THEN (ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift]))));
by Safe_tac;
by (excluded_middle_tac "n < x" 1);
-by (asm_full_simp_tac (simpset()) 1);
+by (Asm_full_simp_tac 1);
by (eres_inst_tac [("j","n")] leE 1);
-by (asm_full_simp_tac ((addsplit (simpset()))
- addsimps [leI,gt_pred,succ_pred]) 1);
+by (asm_simp_tac (simpset() setloop (split_inside_tac [split_if])
+ addsimps [lift_rec_Var,subst_Var,
+ leI,gt_pred,succ_pred]) 1);
by (hyp_subst_tac 1);
-by (asm_full_simp_tac (simpset()) 1);
+by (Asm_simp_tac 1);
by (forw_inst_tac [("j","x")] lt_trans2 1);
by (assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [leI]) 1);
+by (asm_simp_tac (simpset() addsimps [leI]) 1);
qed "lift_rec_subst_rec";
Goal "[|v:redexes; u:redexes; n:nat|]==> \
\ lift_rec(u/v,n) = lift_rec(u,n)/lift_rec(v,succ(n))";
-by (asm_full_simp_tac (simpset() addsimps [lift_rec_subst_rec]) 1);
+by (asm_simp_tac (simpset() addsimps [lift_rec_subst_rec]) 1);
qed "lift_subst";
@@ -181,43 +180,40 @@
\ ALL n:nat. ALL m:nat. ALL u:redexes. m le n-->\
\ lift_rec(subst_rec(u,v,n),m) = \
\ subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))";
-by ((eresolve_tac [redexes.induct] 1)
- THEN (ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift]))));
+by (etac redexes.induct 1
+ THEN ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift])));
by Safe_tac;
by (excluded_middle_tac "n < x" 1);
-by (asm_full_simp_tac (simpset()) 1);
+by (Asm_full_simp_tac 1);
by (eres_inst_tac [("i","x")] leE 1);
by (forward_tac [lt_trans1] 1 THEN assume_tac 1);
-by (ALLGOALS(asm_full_simp_tac
+by (ALLGOALS(asm_simp_tac
(simpset() addsimps [succ_pred,leI,gt_pred])));
by (asm_full_simp_tac (simpset() addsimps [leI]) 1);
-by (excluded_middle_tac "n < xa" 1);
-by (asm_full_simp_tac (simpset()) 1);
-by (asm_full_simp_tac (simpset() addsimps [leI]) 1);
+by (case_tac "n < xa" 1);
+by (Asm_full_simp_tac 2);
+by (asm_simp_tac (simpset() addsimps [leI]) 1);
qed "lift_rec_subst_rec_lt";
Goal "u:redexes ==> \
\ ALL n:nat. ALL v:redexes. subst_rec(v,lift_rec(u,n),n) = u";
-by ((eresolve_tac [redexes.induct] 1)
- THEN (ALLGOALS Asm_simp_tac));
-by Safe_tac;
-by (excluded_middle_tac "n < x" 1);
-(* x <= n *)
-by (asm_full_simp_tac (simpset()) 1);
-by (asm_full_simp_tac (simpset()) 1);
+by (etac redexes.induct 1);
+by Auto_tac;
+by (case_tac "n < x" 1);
+by Auto_tac;
qed "subst_rec_lift_rec";
Goal "v:redexes ==> \
\ ALL m:nat. ALL n:nat. ALL u:redexes. ALL w:redexes. m le n --> \
\ subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m)=\
\ subst_rec(w,subst_rec(u,v,m),n)";
-by ((eresolve_tac [redexes.induct] 1) THEN
- (ALLGOALS(asm_simp_tac (simpset() addsimps
- [lift_lift RS sym,lift_rec_subst_rec_lt]))));
+by (etac redexes.induct 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsimps
+ [lift_lift RS sym,lift_rec_subst_rec_lt])));
by Safe_tac;
by (excluded_middle_tac "n le succ(xa)" 1);
-by (asm_full_simp_tac (simpset()) 1);
+by (Asm_full_simp_tac 1);
by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1);
by (etac leE 1);
by (asm_simp_tac (simpset() addsimps [succ_pred,lt_pred]) 2);
@@ -226,10 +222,9 @@
(nat_into_Ord RS le_refl RS lt_trans) 1 THEN assume_tac 1);
by (asm_simp_tac (simpset() addsimps [succ_pred,lt_pred]) 1);
by (eres_inst_tac [("i","n")] leE 1);
-by (asm_full_simp_tac
- (simpset() addsimps [succ_pred,subst_rec_lift_rec,leI]) 2);
+by (asm_simp_tac (simpset() addsimps [succ_pred,subst_rec_lift_rec,leI]) 2);
by (excluded_middle_tac "n < x" 1);
-by (asm_full_simp_tac (simpset()) 1);
+by (Asm_full_simp_tac 1);
by (eres_inst_tac [("j","n")] leE 1);
by (asm_simp_tac (simpset() addsimps [gt_pred]) 1);
by (asm_simp_tac (simpset() addsimps [subst_rec_lift_rec]) 1);
@@ -257,18 +252,19 @@
Goal "u2 ~ v2 ==> ALL m:nat. ALL u1:redexes. ALL v1:redexes.\
\ u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)";
by (etac Scomp.induct 1);
-by (ALLGOALS(asm_full_simp_tac ((addsplit (simpset())) addsimps
- ([lift_rec_preserve_comp,comp_refl]))));
+by (ALLGOALS
+ (asm_simp_tac
+ (simpset() addsimps [subst_Var, lift_rec_preserve_comp, comp_refl])));
qed "subst_rec_preserve_comp";
Goal "regular(u) ==> ALL m:nat. regular(lift_rec(u,m))";
-by (eresolve_tac [Sreg.induct] 1);
-by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()))));
+by (etac Sreg.induct 1);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lift_rec_Var])));
qed "lift_rec_preserve_reg";
Goal "regular(v) ==> \
\ ALL m:nat. ALL u:redexes. regular(u)-->regular(subst_rec(u,v,m))";
-by (eresolve_tac [Sreg.induct] 1);
-by (ALLGOALS(asm_full_simp_tac ((addsplit (simpset())) addsimps
- [lift_rec_preserve_reg])));
+by (etac Sreg.induct 1);
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [subst_Var,
+ lift_rec_preserve_reg])));
qed "subst_rec_preserve_reg";
--- a/src/ZF/Resid/Terms.ML Mon Sep 21 23:25:27 1998 +0200
+++ b/src/ZF/Resid/Terms.ML Tue Sep 22 13:48:32 1998 +0200
@@ -40,12 +40,12 @@
Goalw [unmark_def]
"u:redexes ==> unmark(u):lambda";
-by (eresolve_tac [redexes.induct] 1);
+by (etac redexes.induct 1);
by (ALLGOALS Asm_simp_tac);
qed "unmark_type";
Goal "u:lambda ==> unmark(u) = u";
-by (eresolve_tac [lambda.induct] 1);
+by (etac lambda.induct 1);
by (ALLGOALS Asm_simp_tac);
qed "lambda_unmark";
@@ -54,15 +54,15 @@
(* lift and subst preserve lambda *)
(* ------------------------------------------------------------------------- *)
-Goal "[|v:lambda|]==> ALL k:nat. lift_rec(v,k):lambda";
-by (eresolve_tac [lambda.induct] 1);
-by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()))));
+Goal "v:lambda ==> ALL k:nat. lift_rec(v,k):lambda";
+by (etac lambda.induct 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [lift_rec_Var])));
qed "liftL_typea";
val liftL_type =liftL_typea RS bspec ;
-Goal "[|v:lambda|]==> ALL n:nat. ALL u:lambda. subst_rec(u,v,n):lambda";
-by (eresolve_tac [lambda.induct] 1);
-by (ALLGOALS(asm_full_simp_tac ((addsplit (simpset())) addsimps [liftL_type])));
+Goal "v:lambda ==> ALL n:nat. ALL u:lambda. subst_rec(u,v,n):lambda";
+by (etac lambda.induct 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [liftL_type,subst_Var])));
qed "substL_typea";
val substL_type = substL_typea RS bspec RS bspec ;