# HG changeset patch # User paulson # Date 875526712 -7200 # Node ID 33f355f56f8204cc53d1df1f77fe0da5889722a8 # Parent 1baedb1d4627cfb9b99e451a2fc29db7527ea094 Much tidying including "qed" instead of result(), and even qed_spec_mp, and Safe_tac instead of step_tac diff -r 1baedb1d4627 -r 33f355f56f82 src/ZF/Resid/Confluence.ML --- a/src/ZF/Resid/Confluence.ML Mon Sep 29 11:51:09 1997 +0200 +++ b/src/ZF/Resid/Confluence.ML Mon Sep 29 11:51:52 1997 +0200 @@ -8,19 +8,6 @@ open Confluence; (* ------------------------------------------------------------------------- *) -(* Confluence *) -(* ------------------------------------------------------------------------- *) - -goalw Confluence.thy [confluence_def] - "!!u.[|confluence(Spar_red)|]==> confluence(Sred)"; -by (step_tac (!claset) 1); -by (dres_inst_tac [("x4","x"),("x3","y"),("x1","z")] - (spec RS spec RS mp RS spec RS mp) 1); -by (ALLGOALS(asm_simp_tac (!simpset addsimps [red_par_red]))); -by (fast_tac (!claset addIs [par_red_red]) 1); -val lemma1 = result(); - -(* ------------------------------------------------------------------------- *) (* strip lemmas *) (* ------------------------------------------------------------------------- *) @@ -30,7 +17,7 @@ by (etac Spar_red.induct 1); by (Fast_tac 1); by (fast_tac (!claset addIs [Spar_red.trans]) 1); -val strip_lemma_r = result(); +qed "strip_lemma_r"; goalw Confluence.thy [confluence_def,strip_def] @@ -38,42 +25,37 @@ by (resolve_tac [impI RS allI RS allI] 1); by (etac Spar_red.induct 1); by (Fast_tac 1); -by (step_tac (!claset) 1); +by (Clarify_tac 1); by (dres_inst_tac [("x1","z")] (spec RS mp) 1); by (REPEAT(eresolve_tac [exE,conjE] 2)); by (dres_inst_tac [("x1","ua")] (spec RS mp) 2); by (fast_tac (!claset addIs [Spar_red.trans]) 3); by (TRYALL assume_tac ); -val strip_lemma_l = result(); +qed "strip_lemma_l"; (* ------------------------------------------------------------------------- *) (* Confluence *) (* ------------------------------------------------------------------------- *) -goal Confluence.thy - "!!u.confluence(Spar_red1)==> confluence(Spar_red)"; -by (resolve_tac [strip_lemma_r RS strip_lemma_l] 1); -by (assume_tac 1); -val lemma2 = result(); - - goalw Confluence.thy [confluence_def] "confluence(Spar_red1)"; -by (step_tac (!claset) 1); +by (Clarify_tac 1); by (forward_tac [simulation] 1); by (forw_inst_tac [("n","z")] simulation 1); -by (step_tac (!claset) 1); +by (Clarify_tac 1); by (forw_inst_tac [("v","va")] paving 1); by (TRYALL assume_tac); -by (REPEAT(step_tac (!claset) 1)); -by (res_inst_tac [("v","vu")] completeness 1); -by (ALLGOALS(asm_simp_tac (!simpset addsimps [completeness]))); -val parallel_moves = result(); +by (fast_tac (!claset addIs [completeness] addss (!simpset)) 1); +qed "parallel_moves"; + +bind_thm ("confluence_parallel_reduction", + parallel_moves RS strip_lemma_r RS strip_lemma_l); -goal Confluence.thy "confluence(Spar_red)"; -by (resolve_tac [parallel_moves RS lemma2] 1); -val confluence_parallel_reduction = result(); +goalw Confluence.thy [confluence_def] + "!!u.[|confluence(Spar_red)|]==> confluence(Sred)"; +by(blast_tac (!claset addIs [par_red_red, red_par_red]) 1); +val lemma1 = result(); -goal Confluence.thy "confluence(Sred)"; -by (resolve_tac [confluence_parallel_reduction RS lemma1] 1); -val confluence_beta_reduction = result(); +bind_thm ("confluence_beta_reduction", + confluence_parallel_reduction RS lemma1); + diff -r 1baedb1d4627 -r 33f355f56f82 src/ZF/Resid/Conversion.ML --- a/src/ZF/Resid/Conversion.ML Mon Sep 29 11:51:09 1997 +0200 +++ b/src/ZF/Resid/Conversion.ML Mon Sep 29 11:51:52 1997 +0200 @@ -7,15 +7,14 @@ open Conversion; -val (!simpset) = (!simpset) addsimps (Sconv1.intrs@[Sconv.one_step,Sconv.refl]); +AddIs (Sconv.intrs @ Sconv1.intrs); goal Conversion.thy "!!u.m<--->n ==> n<--->m"; by (etac Sconv.induct 1); by (etac Sconv1.induct 1); -by (resolve_tac [Sconv.trans] 4); -by (ALLGOALS(asm_simp_tac (!simpset) )); -val conv_sym = result(); +by (ALLGOALS Blast_tac); +qed "conv_sym"; (* ------------------------------------------------------------------------- *) (* Church_Rosser Theorem *) @@ -25,20 +24,11 @@ "!!u.m<--->n ==> EX p.(m --->p) & (n ---> p)"; by (etac Sconv.induct 1); by (etac Sconv1.induct 1); -by (fast_tac (!claset addIs [red1D1,redD2]) 1); -by (fast_tac (!claset addIs [red1D1,redD2]) 1); -by (fast_tac (!claset addIs [red1D1,redD2]) 1); +by (blast_tac (!claset addIs [red1D1,redD2]) 1); +by (blast_tac (!claset addIs [red1D1,redD2]) 1); +by (blast_tac (!claset addIs [red1D1,redD2]) 1); by (cut_facts_tac [confluence_beta_reduction] 1); by (rewtac confluence_def); -by (step_tac (!claset) 1); -by (dres_inst_tac [("x4","n"),("x3","pa"),("x1","pb")] - (spec RS spec RS mp RS spec RS mp) 1); -by (TRYALL assume_tac); -by (step_tac (!claset) 1); -by (step_tac (!claset) 1); -by (step_tac (!claset) 1); -by (res_inst_tac [("n","pa")]Sred.trans 1); -by (res_inst_tac [("n","pb"),("p","ua")] Sred.trans 3); -by (TRYALL assume_tac); -val Church_Rosser = result(); +by (blast_tac (!claset addIs [Sred.trans]) 1); +qed "Church_Rosser"; diff -r 1baedb1d4627 -r 33f355f56f82 src/ZF/Resid/Cube.ML --- a/src/ZF/Resid/Cube.ML Mon Sep 29 11:51:09 1997 +0200 +++ b/src/ZF/Resid/Cube.ML Mon Sep 29 11:51:52 1997 +0200 @@ -16,32 +16,29 @@ (* ============= *) (* ------------------------------------------------------------------------- *) -(* Having more ssumptions than needed -- removed below *) +(* Having more assumptions than needed -- removed below *) goal Cube.thy "!!u.v<==u ==> \ \ regular(u)-->(ALL w.w~v-->w~u--> \ \ w |> u = (w|>v) |> (u|>v))"; by (etac Ssub.induct 1); -by (asm_simp_tac prism_ss 1); -by (asm_simp_tac prism_ss 1); -by (asm_simp_tac prism_ss 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 (asm_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); -val prism_l = result(); +qed_spec_mp "prism_l"; goal Cube.thy "!!u.[|v <== u; regular(u); w~v|]==> \ \ w |> u = (w|>v) |> (u|>v)"; -by (resolve_tac [prism_l RS mp RS spec RS mp RS mp ] 1); +by (resolve_tac [prism_l] 1); by (rtac comp_trans 4); by (assume_tac 4); by (ALLGOALS(asm_simp_tac prism_ss)); -val prism = result(); +qed "prism"; (* ------------------------------------------------------------------------- *) @@ -51,11 +48,10 @@ goal Cube.thy "!!u.[|u~v; regular(v); regular(u); w~u|]==> \ \ (w|>u) |> (v|>u) = (w|>v) |> (u|>v)"; -by (res_inst_tac [("u2","u"),("v2","v")](preservation RS ssubst) 1 +by (rtac (preservation RS ssubst) 1 THEN assume_tac 1 THEN assume_tac 1); -by (res_inst_tac [("u2","v"),("v2","u")](preservation RS ssubst) 1); -by (etac comp_sym 1); -by (atac 1); +by (rtac (preservation RS ssubst) 1 + THEN etac comp_sym 1 THEN assume_tac 1); by (stac (prism RS sym) 1); by (asm_full_simp_tac (!simpset addsimps [prism RS sym,union_l,union_preserve_regular, @@ -65,7 +61,7 @@ [union_preserve_regular, comp_sym_iff]) 1); by (etac comp_trans 1); by (atac 1); -val cube = result(); +qed "cube"; (* ------------------------------------------------------------------------- *) @@ -76,19 +72,11 @@ "!!u.[|w~u; w~v; regular(u); regular(v)|]==> \ \ EX uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &\ \ regular(vu) & (w|>v)~uv & regular(uv) "; -by (forw_inst_tac [("x1","v")] (comp_sym RS comp_trans) 1); -by (step_tac (!claset addSIs [exI]) 1); +by (subgoal_tac "u~v" 1); +by (safe_tac (!claset addSIs [exI])); by (rtac cube 1); -by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1); -by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1); -by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1); -by (atac 1); -by (etac (residuals_preserve_comp RS spec RS mp RS mp RS mp) 1); - by(atac 1); - by(etac comp_sym 1); - by(atac 1); -by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1); -by (asm_simp_tac prism_ss 1); -by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1); -val paving = result(); +by (ALLGOALS (asm_simp_tac (prism_ss addsimps [comp_sym_iff]))); +by (ALLGOALS (blast_tac (!claset addIs [residuals_preserve_comp, + comp_trans, comp_sym]))); +qed "paving"; diff -r 1baedb1d4627 -r 33f355f56f82 src/ZF/Resid/Redex.ML --- a/src/ZF/Resid/Redex.ML Mon Sep 29 11:51:09 1997 +0200 +++ b/src/ZF/Resid/Redex.ML Mon Sep 29 11:51:52 1997 +0200 @@ -14,18 +14,18 @@ goal Redex.thy "redex_rec(Var(n),b,c,d) = b(n)"; by (rtac (redex_rec_def RS def_Vrec RS trans) 1); by (simp_tac (rank_ss addsimps redexes.con_defs) 1); -val redex_rec_Var = result(); +qed "redex_rec_Var"; goal Redex.thy "redex_rec(Fun(t),b,c,d) = c(t,redex_rec(t,b,c,d))"; by (rtac (redex_rec_def RS def_Vrec RS trans) 1); by (simp_tac (rank_ss addsimps redexes.con_defs) 1); -val redex_rec_Fun = result(); +qed "redex_rec_Fun"; goal Redex.thy "redex_rec(App(m,f,a),b,c,d) = \ \ d(m,f,a,redex_rec(f,b,c,d),redex_rec(a,b,c,d))"; by (rtac (redex_rec_def RS def_Vrec RS trans) 1); by (simp_tac (rank_ss addsimps redexes.con_defs) 1); -val redex_rec_App = result(); +qed "redex_rec_App"; Addsimps ([redex_rec_App,redex_rec_Fun,redex_rec_Var]@redexes.intrs); diff -r 1baedb1d4627 -r 33f355f56f82 src/ZF/Resid/Reduction.ML --- a/src/ZF/Resid/Reduction.ML Mon Sep 29 11:51:09 1997 +0200 +++ b/src/ZF/Resid/Reduction.ML Mon Sep 29 11:51:52 1997 +0200 @@ -41,34 +41,34 @@ by (etac Sred.induct 1); by (resolve_tac [Sred.trans] 3); by (ALLGOALS (Asm_simp_tac )); -val red_Fun = result(); +qed "red_Fun"; goal Reduction.thy "!!u.[|n:lambda; m ---> m'|]==> Apl(m,n)--->Apl(m',n)"; by (etac Sred.induct 1); by (resolve_tac [Sred.trans] 3); by (ALLGOALS (Asm_simp_tac )); -val red_Apll = result(); +qed "red_Apll"; goal Reduction.thy "!!u.[|n:lambda; m ---> m'|]==> Apl(n,m)--->Apl(n,m')"; by (etac Sred.induct 1); by (resolve_tac [Sred.trans] 3); by (ALLGOALS (Asm_simp_tac )); -val red_Aplr = result(); +qed "red_Aplr"; goal Reduction.thy "!!u.[|m ---> m'; n--->n'|]==> Apl(m,n)--->Apl(m',n')"; by (res_inst_tac [("n","Apl(m',n)")] Sred.trans 1); by (ALLGOALS (asm_simp_tac (!simpset addsimps [red_Apll,red_Aplr]) )); -val red_Apl = result(); +qed "red_Apl"; goal Reduction.thy "!!u.[|m:lambda; m':lambda; n:lambda; n':lambda; m ---> m'; n--->n'|]==> \ \ Apl(Fun(m),n)---> n'/m'"; by (res_inst_tac [("n","Apl(Fun(m'),n')")] Sred.trans 1); by (ALLGOALS (asm_simp_tac (!simpset addsimps [red_Apl,red_Fun]) )); -val red_beta = result(); +qed "red_beta"; (* ------------------------------------------------------------------------- *) @@ -79,25 +79,25 @@ goal Reduction.thy "!!u.m:lambda==> m =1=> m"; by (eresolve_tac [lambda.induct] 1); by (ALLGOALS (Asm_simp_tac )); -val refl_par_red1 = result(); +qed "refl_par_red1"; goal Reduction.thy "!!u.m-1->n ==> m=1=>n"; by (etac Sred1.induct 1); by (ALLGOALS (asm_simp_tac (!simpset addsimps [refl_par_red1]) )); -val red1_par_red1 = result(); +qed "red1_par_red1"; goal Reduction.thy "!!u.m--->n ==> m===>n"; by (etac Sred.induct 1); by (resolve_tac [Spar_red.trans] 3); by (ALLGOALS (asm_simp_tac (!simpset addsimps [refl_par_red1,red1_par_red1]) )); -val red_par_red = result(); +qed "red_par_red"; goal Reduction.thy "!!u.m===>n ==> m--->n"; by (etac Spar_red.induct 1); by (etac Spar_red1.induct 1); by (resolve_tac [Sred.trans] 5); by (ALLGOALS (asm_simp_tac (!simpset addsimps [red_Fun,red_beta,red_Apl]) )); -val par_red_red = result(); +qed "par_red_red"; (* ------------------------------------------------------------------------- *) @@ -107,11 +107,11 @@ goal Reduction.thy "!!u.m=1=>n ==> EX v. m|>v = n & m~v & regular(v)"; by (etac Spar_red1.induct 1); -by (step_tac (!claset) 1); +by Safe_tac; by (ALLGOALS (REPEAT o (resolve_tac [exI,conjI]))); by (TRYALL(resolve_tac [res_redex,res_App,res_Fun,res_Var])); by (ALLGOALS (asm_simp_tac (!simpset))); -val simulation = result(); +qed "simulation"; (* ------------------------------------------------------------------------- *) @@ -123,7 +123,7 @@ \ 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)))); -val unmmark_lift_rec = result(); +qed "unmmark_lift_rec"; goal Reduction.thy "!!u.v:redexes ==> ALL k:nat.ALL u:redexes. \ @@ -131,7 +131,7 @@ by (eresolve_tac [redexes.induct] 1); by (ALLGOALS (asm_full_simp_tac ((addsplit (!simpset)) addsimps [unmmark_lift_rec]))); -val unmmark_subst_rec = result(); +qed "unmmark_subst_rec"; (* ------------------------------------------------------------------------- *) @@ -144,10 +144,11 @@ by (ALLGOALS (asm_full_simp_tac (reducL_ss addsimps [unmmark_subst_rec]) )); by (dres_inst_tac [("psi", "Fun(?u) =1=> ?w")] asm_rl 1); by (asm_full_simp_tac reducL_ss 1); -val completeness_l = result(); +qed_spec_mp "completeness_l"; goal Reduction.thy "!!u.[|u:lambda; u~v; regular(v)|]==> u =1=> unmark(u|>v)"; -by (dres_inst_tac [("u1","u")] (completeness_l RS mp) 1); +by (dtac completeness_l 1); by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [lambda_unmark]) )); -val completeness = result(); +qed "completeness"; + diff -r 1baedb1d4627 -r 33f355f56f82 src/ZF/Resid/Residuals.ML --- a/src/ZF/Resid/Residuals.ML Mon Sep 29 11:51:09 1997 +0200 +++ b/src/ZF/Resid/Residuals.ML Mon Sep 29 11:51:52 1997 +0200 @@ -47,14 +47,13 @@ "!!u.residuals(u,v,w) ==> ALL w1.residuals(u,v,w1) --> w1 = w"; by (etac Sres.induct 1); by (ALLGOALS Fast_tac); -val residuals_function = result(); -val res_is_func = residuals_function RS spec RS mp; +qed_spec_mp "residuals_function"; goal Residuals.thy "!!u.u~v ==> regular(v) --> (EX w.residuals(u,v,w))"; by (etac Scomp.induct 1); by (ALLGOALS Fast_tac); -val residuals_intro = result(); +qed "residuals_intro"; val prems = goal Residuals.thy "[|u~v; residuals(u,v,THE w. residuals(u, v, w))==> R; \ @@ -63,38 +62,38 @@ by (resolve_tac prems 1); by (resolve_tac [residuals_intro RS mp RS exE] 1); by (resolve_tac [the_equality RS ssubst] 3); -by (ALLGOALS (fast_tac (!claset addIs [res_is_func]))); -val comp_resfuncE = result(); +by (ALLGOALS (fast_tac (!claset addIs [residuals_function]))); +qed "comp_resfuncE"; (* ------------------------------------------------------------------------- *) (* Residual function *) (* ------------------------------------------------------------------------- *) -val resfunc_cs = (!claset addIs [the_equality,res_is_func] +val resfunc_cs = (!claset addIs [the_equality,residuals_function] addSEs [comp_resfuncE]); goalw Residuals.thy [res_func_def] "!!n.n:nat ==> Var(n) |> Var(n) = Var(n)"; by (fast_tac resfunc_cs 1); -val res_Var = result(); +qed "res_Var"; goalw Residuals.thy [res_func_def] "!!n.[|s~t; regular(t)|]==> Fun(s) |> Fun(t) = Fun(s |> t)"; by (fast_tac resfunc_cs 1); -val res_Fun = result(); +qed "res_Fun"; goalw Residuals.thy [res_func_def] "!!n.[|s~u; regular(u); t~v; regular(v); b:bool|]==> \ \ App(b,s,t) |> App(0,u,v) = App(b, s |> u, t |> v)"; by (fast_tac resfunc_cs 1); -val res_App = result(); +qed "res_App"; goalw Residuals.thy [res_func_def] "!!n.[|s~u; regular(u); t~v; regular(v); b:bool|]==> \ \ App(b,Fun(s),t) |> App(1,Fun(u),v) = (t |> v)/ (s |> u)"; by (fast_tac resfunc_cs 1); -val res_redex = result(); +qed "res_redex"; goal Residuals.thy "!!n.[|s~t; regular(t)|]==> regular(t) --> s |> t:redexes"; @@ -106,7 +105,7 @@ by (asm_full_simp_tac (!simpset addsimps [res_Fun] setloop (SELECT_GOAL (safe_tac (!claset)))) 1); -val resfunc_type = result(); +qed "resfunc_type"; Addsimps ([res_Var, res_Fun, res_App, res_redex, lift_rec_preserve_comp, lift_rec_preserve_reg, subst_rec_preserve_comp, resfunc_type, @@ -123,42 +122,42 @@ "!!u.u<==v ==> u~v"; by (etac Ssub.induct 1); by (ALLGOALS Asm_simp_tac); -val sub_comp = result(); +qed "sub_comp"; goal Residuals.thy "!!u.u<==v ==> regular(v) --> regular(u)"; by (etac Ssub.induct 1); by (ALLGOALS (asm_simp_tac res1L_ss)); -val sub_preserve_reg = result(); +qed "sub_preserve_reg"; goal Residuals.thy "!!u.[|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 (Step_tac 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 (Asm_full_simp_tac 1); -val residuals_lift_rec = result(); +qed "residuals_lift_rec"; goal Residuals.thy "!!u.u1~u2 ==> ALL v1 v2.v1~v2 --> regular(v2) --> regular(u2) -->\ \ (ALL n:nat.subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) = \ \ subst_rec(v1 |> v2, u1 |> u2,n))"; by (etac Scomp.induct 1); -by (Step_tac 1); +by Safe_tac; by (ALLGOALS (asm_full_simp_tac ((addsplit (!simpset)) addsimps ([residuals_lift_rec])))); by (dres_inst_tac [("psi", "ALL x.?P(x)")] asm_rl 1); by (asm_full_simp_tac (!simpset addsimps ([substitution])) 1); -val residuals_subst_rec = result(); +qed "residuals_subst_rec"; goal Residuals.thy "!!u.[|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); -val commutation = result(); +qed "commutation"; (* ------------------------------------------------------------------------- *) (* Residuals are comp and regular *) @@ -173,7 +172,7 @@ THEN resolve_tac Sreg.intrs 3); by (REPEAT(assume_tac 1)); by (asm_full_simp_tac res1L_ss 1); -val residuals_preserve_comp = result(); +qed_spec_mp "residuals_preserve_comp"; goal Residuals.thy @@ -182,7 +181,7 @@ by (safe_tac (!claset)); by (TRYALL (dres_inst_tac [("psi", "regular(Fun(?u) |> ?v)")] asm_rl)); by (ALLGOALS (asm_full_simp_tac res1L_ss)); -val residuals_preserve_reg = result(); +qed "residuals_preserve_reg"; (* ------------------------------------------------------------------------- *) (* Preservation lemma *) @@ -192,7 +191,7 @@ "!!u.u~v ==> v ~ (u un v)"; by (etac Scomp.induct 1); by (ALLGOALS Asm_full_simp_tac); -val union_preserve_comp = result(); +qed "union_preserve_comp"; goal Residuals.thy "!!u.u ~ v ==> regular(v) --> u|>v = (u un v)|>v"; @@ -204,6 +203,4 @@ by (asm_full_simp_tac (!simpset addsimps [union_preserve_comp RS comp_sym, comp_sym RS union_preserve_comp RS comp_sym]) 1); -val preservation1 = result(); - -val preservation = preservation1 RS mp; +qed_spec_mp "preservation"; diff -r 1baedb1d4627 -r 33f355f56f82 src/ZF/Resid/SubUnion.ML --- a/src/ZF/Resid/SubUnion.ML Mon Sep 29 11:51:09 1997 +0200 +++ b/src/ZF/Resid/SubUnion.ML Mon Sep 29 11:51:52 1997 +0200 @@ -25,20 +25,20 @@ "!!u.n:nat==>Var(n) un Var(n)=Var(n)"; by (Asm_simp_tac 1); by (simp_tac (rank_ss addsimps redexes.con_defs) 1); -val union_Var = result(); +qed "union_Var"; goalw SubUnion.thy [union_def] "!!u.[|u:redexes; v:redexes|]==>Fun(u) un Fun(v)=Fun(u un v)"; by (Asm_simp_tac 1); by (simp_tac (rank_ss addsimps redexes.con_defs) 1); -val union_Fun = result(); +qed "union_Fun"; goalw SubUnion.thy [union_def] "!!u.[|b1:bool; b2:bool; u1:redexes; v1:redexes; u2:redexes; v2:redexes|]==> \ \ App(b1,u1,v1) un App(b2,u2,v2)=App(b1 or b2,u1 un u2,v1 un v2)"; by (Asm_simp_tac 1); by (simp_tac (rank_ss addsimps redexes.con_defs) 1); -val union_App = result(); +qed "union_App"; Addsimps (Ssub.intrs@bool_typechecks@ Sreg.intrs@Scomp.intrs@ @@ -68,27 +68,25 @@ goal SubUnion.thy "!!u.u:redexes ==> u ~ u"; by (eresolve_tac [redexes.induct] 1); by (ALLGOALS Fast_tac); -val comp_refl = result(); +qed "comp_refl"; goal SubUnion.thy "!!u.u ~ v ==> v ~ u"; by (etac Scomp.induct 1); by (ALLGOALS Fast_tac); -val comp_sym = result(); +qed "comp_sym"; goal SubUnion.thy "u ~ v <-> v ~ u"; by (fast_tac (!claset addIs [comp_sym]) 1); -val comp_sym_iff = result(); +qed "comp_sym_iff"; goal SubUnion.thy "!!u.u ~ v ==> ALL w.v ~ w-->u ~ w"; by (etac Scomp.induct 1); by (ALLGOALS Fast_tac); -val comp_trans1 = result(); - -val comp_trans = comp_trans1 RS spec RS mp; +qed_spec_mp "comp_trans"; (* ------------------------------------------------------------------------- *) (* union proofs *) @@ -99,20 +97,20 @@ by (etac Scomp.induct 1); by (etac boolE 3); by (ALLGOALS Asm_full_simp_tac); -val union_l = result(); +qed "union_l"; goal SubUnion.thy "!!u.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); -val union_r = result(); +qed "union_r"; goal SubUnion.thy "!!u.u ~ v ==> u un v = v un u"; by (etac Scomp.induct 1); by (ALLGOALS(asm_simp_tac (!simpset addsimps [or_commute]))); -val union_sym = result(); +qed "union_sym"; (* ------------------------------------------------------------------------- *) (* regular proofs *) @@ -125,4 +123,4 @@ (!simpset setloop(SELECT_GOAL (safe_tac (!claset)))))); by (dres_inst_tac [("psi", "regular(Fun(?u) un ?v)")] asm_rl 1); by (Asm_full_simp_tac 1); -val union_preserve_regular = result(); +qed_spec_mp "union_preserve_regular"; diff -r 1baedb1d4627 -r 33f355f56f82 src/ZF/Resid/Substitution.ML --- a/src/ZF/Resid/Substitution.ML Mon Sep 29 11:51:09 1997 +0200 +++ b/src/ZF/Resid/Substitution.ML Mon Sep 29 11:51:52 1997 +0200 @@ -14,7 +14,7 @@ goal Arith.thy "!!m.[| p < n; n:nat|]==> n~=p"; by (Fast_tac 1); -val gt_not_eq = result(); +qed "gt_not_eq"; val succ_pred = prove_goal Arith.thy "!!i.[|j:nat; i:nat|]==> i < j --> succ(j #- 1) = j" @@ -27,13 +27,13 @@ by (rtac succ_leE 1); by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1); by (asm_simp_tac (!simpset addsimps [succ_pred]) 1); -val lt_pred = result(); +qed "lt_pred"; goal Arith.thy "!!i.[|n < succ(x); p n#-1 < x "; by (rtac succ_leE 1); by (asm_simp_tac (!simpset addsimps [succ_pred]) 1); -val gt_pred = result(); +qed "gt_pred"; Addsimps [nat_into_Ord, not_lt_iff_le, if_P, if_not_P]; @@ -45,29 +45,29 @@ goalw Substitution.thy [lift_rec_def] "!!n.[|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); -val lift_rec_le = result(); +qed "lift_rec_le"; goalw Substitution.thy [lift_rec_def] "!!n.[|i:nat; k:nat; i lift_rec(Var(i),k) = Var(i)"; by (Asm_full_simp_tac 1); -val lift_rec_gt = result(); +qed "lift_rec_gt"; goalw Substitution.thy [lift_rec_def] "!!n.[|n:nat; k:nat|]==> \ \ lift_rec(Fun(t),k) = Fun(lift_rec(t,succ(k)))"; by (Asm_full_simp_tac 1); -val lift_rec_Fun = result(); +qed "lift_rec_Fun"; goalw Substitution.thy [lift_rec_def] "!!n.[|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); -val lift_rec_App = result(); +qed "lift_rec_App"; (* ------------------------------------------------------------------------- *) (* substitution quality rules *) @@ -77,36 +77,36 @@ "!!n.[|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); -val subst_eq = result(); +qed "subst_eq"; goalw Substitution.thy [subst_rec_def] "!!n.[|n:nat; u:redexes; p:nat; p \ \ subst_rec(u,Var(n),p) = Var(n#-1)"; by (asm_full_simp_tac (!simpset) 1); -val subst_gt = result(); +qed "subst_gt"; goalw Substitution.thy [subst_rec_def] "!!n.[|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); -val subst_lt = result(); +qed "subst_lt"; goalw Substitution.thy [subst_rec_def] "!!n.[|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); -val subst_Fun = result(); +qed "subst_Fun"; goalw Substitution.thy [subst_rec_def] "!!n.[|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); -val subst_App = result(); +qed "subst_App"; fun addsplit ss = (ss setloop (split_inside_tac [expand_if]) addsimps [lift_rec_Var,subst_Var]); @@ -117,7 +117,7 @@ by (eresolve_tac [redexes.induct] 1); by (ALLGOALS(asm_full_simp_tac ((addsplit (!simpset)) addsimps [lift_rec_Fun,lift_rec_App]))); -val lift_rec_type_a = result(); +qed "lift_rec_type_a"; val lift_rec_type = lift_rec_type_a RS bspec; goalw Substitution.thy [] @@ -126,7 +126,7 @@ by (ALLGOALS(asm_full_simp_tac ((addsplit (!simpset)) addsimps [subst_Fun,subst_App, lift_rec_type]))); -val subst_type_a = result(); +qed "subst_type_a"; val subst_type = subst_type_a RS bspec RS bspec; @@ -144,19 +144,19 @@ \ (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 (step_tac (!claset) 1); +by Safe_tac; by (excluded_middle_tac "na < xa" 1); by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2)); by (ALLGOALS(asm_full_simp_tac ((addsplit (!simpset)) addsimps [leI]))); -val lift_lift_rec = result(); +qed "lift_lift_rec"; goalw Substitution.thy [] "!!n.[|u:redexes; n:nat|]==> \ \ lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))"; by (asm_simp_tac (!simpset addsimps [lift_lift_rec]) 1); -val lift_lift = result(); +qed "lift_lift"; goal Substitution.thy "!!n.v:redexes ==> \ @@ -165,7 +165,7 @@ \ subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)"; by ((eresolve_tac [redexes.induct] 1) THEN (ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift])))); -by (step_tac (!claset) 1); +by Safe_tac; by (excluded_middle_tac "na < x" 1); by (asm_full_simp_tac (!simpset) 1); by (eres_inst_tac [("j","na")] leE 1); @@ -176,13 +176,13 @@ by (forw_inst_tac [("j","x")] lt_trans2 1); by (assume_tac 1); by (asm_full_simp_tac (!simpset addsimps [leI]) 1); -val lift_rec_subst_rec = result(); +qed "lift_rec_subst_rec"; goalw Substitution.thy [] "!!n.[|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); -val lift_subst = result(); +qed "lift_subst"; goalw Substitution.thy [] @@ -192,7 +192,7 @@ \ 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 (step_tac (!claset) 1); +by Safe_tac; by (excluded_middle_tac "na < x" 1); by (asm_full_simp_tac (!simpset) 1); by (eres_inst_tac [("i","x")] leE 1); @@ -204,7 +204,7 @@ by (excluded_middle_tac "na < xa" 1); by (asm_full_simp_tac (!simpset) 1); by (asm_full_simp_tac (!simpset addsimps [leI]) 1); -val lift_rec_subst_rec_lt = result(); +qed "lift_rec_subst_rec_lt"; goalw Substitution.thy [] @@ -212,12 +212,12 @@ \ 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 (step_tac (!claset) 1); +by Safe_tac; by (excluded_middle_tac "na < x" 1); (* x <= na *) by (asm_full_simp_tac (!simpset) 1); by (asm_full_simp_tac (!simpset) 1); -val subst_rec_lift_rec = result(); +qed "subst_rec_lift_rec"; goal Substitution.thy "!!n.v:redexes ==> \ @@ -227,7 +227,7 @@ by ((eresolve_tac [redexes.induct] 1) THEN (ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift RS sym,lift_rec_subst_rec_lt])))); -by (step_tac (!claset) 1); +by Safe_tac; by (excluded_middle_tac "na le succ(xa)" 1); by (asm_full_simp_tac (!simpset) 1); by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1); @@ -247,14 +247,14 @@ by (asm_simp_tac (!simpset addsimps [subst_rec_lift_rec]) 1); by (forward_tac [lt_trans2] 1 THEN assume_tac 1); by (asm_simp_tac (!simpset addsimps [gt_pred]) 1); -val subst_rec_subst_rec = result(); +qed "subst_rec_subst_rec"; goalw Substitution.thy [] "!!n.[|v:redexes; u:redexes; w:redexes; n:nat|]==> \ \ subst_rec(w,u,n)/subst_rec(lift(w),v,succ(n)) = subst_rec(w,u/v,n)"; by (asm_simp_tac (!simpset addsimps [subst_rec_subst_rec]) 1); -val substitution = result(); +qed "substitution"; (* ------------------------------------------------------------------------- *) (* Preservation lemmas *) @@ -266,7 +266,7 @@ "!!n.[|n:nat; u ~ v|]==> ALL m:nat.lift_rec(u,m) ~ lift_rec(v,m)"; by (etac Scomp.induct 1); by (ALLGOALS(asm_simp_tac (!simpset addsimps [comp_refl]))); -val lift_rec_preserve_comp = result(); +qed "lift_rec_preserve_comp"; goal Substitution.thy "!!n.u2 ~ v2 ==> ALL m:nat.ALL u1:redexes.ALL v1:redexes.\ @@ -274,13 +274,13 @@ by (etac Scomp.induct 1); by (ALLGOALS(asm_full_simp_tac ((addsplit (!simpset)) addsimps ([lift_rec_preserve_comp,comp_refl])))); -val subst_rec_preserve_comp = result(); +qed "subst_rec_preserve_comp"; goal Substitution.thy "!!n.regular(u) ==> ALL m:nat.regular(lift_rec(u,m))"; by (eresolve_tac [Sreg.induct] 1); by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset)))); -val lift_rec_preserve_reg = result(); +qed "lift_rec_preserve_reg"; goal Substitution.thy "!!n.regular(v) ==> \ @@ -288,4 +288,4 @@ by (eresolve_tac [Sreg.induct] 1); by (ALLGOALS(asm_full_simp_tac ((addsplit (!simpset)) addsimps [lift_rec_preserve_reg]))); -val subst_rec_preserve_reg = result(); +qed "subst_rec_preserve_reg"; diff -r 1baedb1d4627 -r 33f355f56f82 src/ZF/Resid/Terms.ML --- a/src/ZF/Resid/Terms.ML Mon Sep 29 11:51:09 1997 +0200 +++ b/src/ZF/Resid/Terms.ML Mon Sep 29 11:51:52 1997 +0200 @@ -14,17 +14,17 @@ goalw Terms.thy [unmark_def] "unmark(Var(n)) = Var(n)"; by (Asm_simp_tac 1); -val unmark_Var = result(); +qed "unmark_Var"; goalw Terms.thy [unmark_def] "unmark(Fun(t)) = Fun(unmark(t))"; by (Asm_simp_tac 1); -val unmark_Fun = result(); +qed "unmark_Fun"; goalw Terms.thy [unmark_def] "unmark(App(b,n,m)) = App(0,unmark(n),unmark(m))"; by (Asm_simp_tac 1); -val unmark_App = result(); +qed "unmark_App"; (* ------------------------------------------------------------------------- *) @@ -45,13 +45,13 @@ "!!u.u:redexes ==> unmark(u):lambda"; by (eresolve_tac [redexes.induct] 1); by (ALLGOALS Asm_simp_tac); -val unmark_type = result(); +qed "unmark_type"; goal Terms.thy "!!u.u:lambda ==> unmark(u) = u"; by (eresolve_tac [lambda.induct] 1); by (ALLGOALS Asm_simp_tac); -val lambda_unmark = result(); +qed "lambda_unmark"; (* ------------------------------------------------------------------------- *) @@ -62,14 +62,14 @@ "!!u.[|v:lambda|]==> ALL k:nat.lift_rec(v,k):lambda"; by (eresolve_tac [lambda.induct] 1); by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset)))); -val liftL_typea = result(); +qed "liftL_typea"; val liftL_type =liftL_typea RS bspec ; goal Terms.thy "!!n.[|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]))); -val substL_typea = result(); +qed "substL_typea"; val substL_type = substL_typea RS bspec RS bspec ;