# HG changeset patch # User paulson # Date 906464912 -7200 # Node ID 38928c4a8eb21d2fa1d65a4a7ce0e6d8e5422615 # Parent e7617b57a3e6d1db5674119fa538265c56cdf30d big tidying of simpsets, etc diff -r e7617b57a3e6 -r 38928c4a8eb2 src/ZF/Resid/Cube.ML --- 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"; diff -r e7617b57a3e6 -r 38928c4a8eb2 src/ZF/Resid/Reduction.ML --- 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)"; diff -r e7617b57a3e6 -r 38928c4a8eb2 src/ZF/Resid/Residuals.ML --- 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); diff -r e7617b57a3e6 -r 38928c4a8eb2 src/ZF/Resid/SubUnion.ML --- 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"; diff -r e7617b57a3e6 -r 38928c4a8eb2 src/ZF/Resid/Substitution.ML --- 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 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 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 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 \ \ 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 \ \ 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"; diff -r e7617b57a3e6 -r 38928c4a8eb2 src/ZF/Resid/Terms.ML --- 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 ;