# HG changeset patch # User lcp # Date 797780287 -7200 # Node ID 5ba0314f821423df5d664309d2e9346d3a6c0832 # Parent 5133479a37cffff69ed221b94c81067e512d481c New example by Ole Rasmussen diff -r 5133479a37cf -r 5ba0314f8214 src/ZF/Resid/Confluence.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Resid/Confluence.ML Thu Apr 13 15:38:07 1995 +0200 @@ -0,0 +1,79 @@ +(* Title: Confluence.ML + ID: $Id$ + Author: Ole Rasmussen + Copyright 1995 University of Cambridge + Logic Image: ZF +*) + +open Confluence; + +(* ------------------------------------------------------------------------- *) +(* Confluence *) +(* ------------------------------------------------------------------------- *) + +goalw Confluence.thy [confluence_def] + "!!u.[|confluence(Spar_red)|]==> confluence(Sred)"; +by (step_tac ZF_cs 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 (reduc_ss addsimps [red_par_red]))); +by (fast_tac (reduc_cs addIs [par_red_red]) 1); +val lemma1 = result(); + +(* ------------------------------------------------------------------------- *) +(* strip lemmas *) +(* ------------------------------------------------------------------------- *) + +goalw Confluence.thy [confluence_def,strip_def] + "!!u.[|confluence(Spar_red1)|]==> strip"; +by (resolve_tac [impI RS allI RS allI] 1); +by (eresolve_tac [par_red_induct] 1); +by (fast_tac reduc_cs 1); +by (fast_tac (ZF_cs addIs [Spar_red.trans]) 1); +val strip_lemma_r = result(); + + +goalw Confluence.thy [confluence_def,strip_def] + "!!u.strip==> confluence(Spar_red)"; +by (resolve_tac [impI RS allI RS allI] 1); +by (eresolve_tac [par_red_induct] 1); +by (fast_tac reduc_cs 1); +by (step_tac ZF_cs 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 (ZF_cs addIs [Spar_red.trans]) 3); +by (TRYALL assume_tac ); +val strip_lemma_l = result(); + +(* ------------------------------------------------------------------------- *) +(* 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 ZF_cs 1); +by (forward_tac [simulation] 1); +by (forw_inst_tac [("n","z")] simulation 1); +by (step_tac ZF_cs 1); +by (forw_inst_tac [("v","va")] paving 1); +by (TRYALL assume_tac); +by (REPEAT(step_tac ZF_cs 1)); +by (res_inst_tac [("v","vu")] completeness 1); +by (ALLGOALS(asm_simp_tac (reduc_ss addsimps [completeness]))); +val parallel_moves = result(); + +goal Confluence.thy "confluence(Spar_red)"; +by (resolve_tac [parallel_moves RS lemma2] 1); +val confluence_parallel_reduction = result(); + +goal Confluence.thy "confluence(Sred)"; +by (resolve_tac [confluence_parallel_reduction RS lemma1] 1); +val confluence_beta_reduction = result(); diff -r 5133479a37cf -r 5ba0314f8214 src/ZF/Resid/Confluence.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Resid/Confluence.thy Thu Apr 13 15:38:07 1995 +0200 @@ -0,0 +1,21 @@ +(* Title: Confluence.thy + ID: $Id$ + Author: Ole Rasmussen + Copyright 1995 University of Cambridge + Logic Image: ZF +*) + +Confluence = Reduction+ + +consts + confluence :: "i=>o" + strip :: "o" + +defs + confluence_def "confluence(R) == \ +\ ALL x y. :R --> (ALL z.:R --> \ +\ (EX u.:R & :R))" + strip_def "strip == ALL x y. (x ===> y) --> (ALL z.(x =1=> z) --> \ +\ (EX u.(y =1=> u) & (z===>u)))" +end + diff -r 5133479a37cf -r 5ba0314f8214 src/ZF/Resid/Conversion.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Resid/Conversion.ML Thu Apr 13 15:38:07 1995 +0200 @@ -0,0 +1,47 @@ +(* Title: Conversion.ML + ID: $Id$ + Author: Ole Rasmussen + Copyright 1995 University of Cambridge + Logic Image: ZF +*) + +open Conversion; + +val conv_ss = reduc_ss addsimps (Sconv1.intrs@[Sconv.one_step,Sconv.refl]); + +val conv1_induct = Sconv1.mutual_induct RS spec RS spec RSN (2,rev_mp); +val conv_induct = Sconv.mutual_induct RS spec RS spec RSN (2,rev_mp); + +goal Conversion.thy + "!!u.m<--->n ==> n<--->m"; +by (eresolve_tac [conv_induct] 1); +by (eresolve_tac [conv1_induct] 1); +by (resolve_tac [Sconv.trans] 4); +by (ALLGOALS(asm_simp_tac (conv_ss) )); +val conv_sym = result(); + +(* ------------------------------------------------------------------------- *) +(* Church_Rosser Theorem *) +(* ------------------------------------------------------------------------- *) + +goal Conversion.thy + "!!u.m<--->n ==> EX p.(m --->p) & (n ---> p)"; +by (eresolve_tac [conv_induct] 1); +by (eresolve_tac [conv1_induct] 1); +by (fast_tac (reduc_cs addIs [red1D1,redD2]) 1); +by (fast_tac (reduc_cs addIs [red1D1,redD2]) 1); +by (fast_tac (reduc_cs addIs [red1D1,redD2]) 1); +by (cut_facts_tac [confluence_beta_reduction] 1); +by (rewrite_goals_tac [confluence_def]); +by (step_tac ZF_cs 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 ZF_cs 1); +by (step_tac ZF_cs 1); +by (step_tac ZF_cs 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(); + diff -r 5133479a37cf -r 5ba0314f8214 src/ZF/Resid/Conversion.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Resid/Conversion.thy Thu Apr 13 15:38:07 1995 +0200 @@ -0,0 +1,36 @@ +(* Title: Conversion.thy + ID: $Id$ + Author: Ole Rasmussen + Copyright 1995 University of Cambridge + Logic Image: ZF + +*) + +Conversion = Confluence+ + +consts + Sconv1 :: "i" + "<-1->" :: "[i,i]=>o" (infixl 50) + Sconv :: "i" + "<--->" :: "[i,i]=>o" (infixl 50) + +translations + "a<-1->b" == ":Sconv1" + "a<--->b" == ":Sconv" + +inductive + domains "Sconv1" <= "lambda*lambda" + intrs + red1 "m -1-> n ==> m<-1->n" + expl "n -1-> m ==> m<-1->n" + type_intrs "[red1D1,red1D2]@lambda.intrs@bool_typechecks" + +inductive + domains "Sconv" <= "lambda*lambda" + intrs + one_step "m<-1->n ==> m<--->n" + refl "m:lambda ==> m<--->m" + trans "[|m<--->n; n<--->p|] ==> m<--->p" + type_intrs "[Sconv1.dom_subset RS subsetD]@lambda.intrs@bool_typechecks" +end + diff -r 5133479a37cf -r 5ba0314f8214 src/ZF/Resid/Cube.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Resid/Cube.ML Thu Apr 13 15:38:07 1995 +0200 @@ -0,0 +1,77 @@ +(* Title: Cube.ML + ID: $Id$ + Author: Ole Rasmussen + Copyright 1995 University of Cambridge + Logic Image: ZF +*) + +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]); + +(* ------------------------------------------------------------------------- *) +(* Prism theorem *) +(* ============= *) +(* ------------------------------------------------------------------------- *) + +(* Having more ssumptions 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 (eresolve_tac [sub_induct] 1); +by (asm_simp_tac (prism_ss) 1); +by (asm_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); +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(); + +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 [comp_trans] 4); +by (assume_tac 4); +by (ALLGOALS(asm_simp_tac (prism_ss))); +val prism = result(); + + +(* ------------------------------------------------------------------------- *) +(* Levy's Cube Lemma *) +(* ------------------------------------------------------------------------- *) + +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 + THEN assume_tac 1 THEN assume_tac 1); +by (res_inst_tac [("u2","v"),("v2","u")](preservation RS ssubst) 1); +by (ALLGOALS(asm_full_simp_tac (res1_ss addsimps + [prism RS sym,union_r,union_l,union_preserve_comp,union_preserve_regular, + read_instantiate [("u2","w"),("x1","v")] comp_trans,comp_sym_iff, + union_sym]))); +val cube = result(); + + +(* ------------------------------------------------------------------------- *) +(* paving theorem *) +(* ------------------------------------------------------------------------- *) + +goal Cube.thy + "!!u.[|w~u; w~v; regular(u); regular(v)|]==> \ +\ EX uv.EX 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 (REPEAT(step_tac ZF_cs 1)); +by (resolve_tac [cube] 1); +by (ALLGOALS(asm_simp_tac (prism_ss addsimps [comp_sym_iff]))); +val paving = result(); + diff -r 5133479a37cf -r 5ba0314f8214 src/ZF/Resid/Cube.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Resid/Cube.thy Thu Apr 13 15:38:07 1995 +0200 @@ -0,0 +1,8 @@ +(* Title: Cube.thy + ID: $Id$ + Author: Ole Rasmussen + Copyright 1995 University of Cambridge + Logic Image: ZF +*) + +Cube = Residuals diff -r 5133479a37cf -r 5ba0314f8214 src/ZF/Resid/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Resid/ROOT.ML Thu Apr 13 15:38:07 1995 +0200 @@ -0,0 +1,24 @@ +(* Title: ZF/Resid/ROOT + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1995 University of Cambridge + +Executes the Residuals example. +This is a proof of the Church-Rosser Theorem for the untyped lambda-calculus. + +By Ole Rasmussen, following the Coq proof given in + +Gérard Huet. Residual Theory in Lambda-Calculus: A Formal Development. +J. Functional Programming 4(3) 1994, 371-394. +*) + +ZF_build_completed; (*Make examples fail if ZF did*) + +writeln"Root file for ZF/Resid"; +proof_timing := true; + +loadpath := [".", "Resid"]; + +time_use_thy "Confluence"; + +writeln"END: Root file for ZF/Resid"; diff -r 5133479a37cf -r 5ba0314f8214 src/ZF/Resid/Redex.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Resid/Redex.ML Thu Apr 13 15:38:07 1995 +0200 @@ -0,0 +1,36 @@ +(* Title: Redex.ML + ID: $Id$ + Author: Ole Rasmussen + Copyright 1995 University of Cambridge + Logic Image: ZF +*) + +open Redex; + +(* ------------------------------------------------------------------------- *) +(* redex_rec conversions *) +(* ------------------------------------------------------------------------- *) + +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(); + +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(); + +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(); + +val redexes_ss = (arith_ss addsimps + ([redex_rec_App,redex_rec_Fun,redex_rec_Var]@redexes.intrs)); + + + + + diff -r 5133479a37cf -r 5ba0314f8214 src/ZF/Resid/Redex.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Resid/Redex.thy Thu Apr 13 15:38:07 1995 +0200 @@ -0,0 +1,28 @@ +(* Title: Redex.thy + ID: $Id$ + Author: Ole Rasmussen + Copyright 1995 University of Cambridge + Logic Image: ZF +*) + +Redex = Univ + +consts + redexes :: "i" + +datatype + "redexes" = Var ("n: nat") + | Fun ("t: redexes") + | App ("b:bool" ,"f:redexes" , "a:redexes") + type_intrs "[bool_into_univ]" + + +consts + redex_rec :: "[i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i" + +defs + redex_rec_def + "redex_rec(p,b,c,d) == \ +\ Vrec(p, %p g.redexes_case(b, %x.c(x,g`x), \ +\ %n x y.d(n, x, y, g`x, g`y), p))" +end + diff -r 5133479a37cf -r 5ba0314f8214 src/ZF/Resid/Reduction.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Resid/Reduction.ML Thu Apr 13 15:38:07 1995 +0200 @@ -0,0 +1,160 @@ +(* Title: Reduction.ML + ID: $Id$ + Author: Ole Rasmussen + Copyright 1995 University of Cambridge + Logic Image: ZF +*) + +open Reduction; + + +(* ------------------------------------------------------------------------- *) +(* Setting up rulelists for reduction *) +(* ------------------------------------------------------------------------- *) + +val red1D1 = Sred1.dom_subset RS subsetD RS SigmaD1; +val red1D2 = Sred1.dom_subset RS subsetD RS SigmaD2; +val redD1 = Sred.dom_subset RS subsetD RS SigmaD1; +val redD2 = Sred.dom_subset RS subsetD RS SigmaD2; +val par_red1D1 = Spar_red1.dom_subset RS subsetD RS SigmaD1; +val par_red1D2 = Spar_red1.dom_subset RS subsetD RS SigmaD2; +val par_redD1 = Spar_red.dom_subset RS subsetD RS SigmaD1; +val par_redD2 = Spar_red.dom_subset RS subsetD RS SigmaD2; + + +val reduc_cs = res_cs + addIs (Sred1.intrs@[Sred.one_step,Sred.refl]@Spar_red1.intrs@ + [Spar_red.one_step,lambda.dom_subset RS subsetD, + unmark_type]@lambda.intrs@bool_typechecks) + addSEs [Spar_red1.mk_cases redexes.con_defs "Fun(t) =1=> Fun(u)"]; + +val reduc_ss = term_ss addsimps + (Sred1.intrs@[Sred.one_step,Sred.refl]@Spar_red1.intrs@ + [Spar_red.one_step,substL_type,redD1,redD2,par_redD1, + par_redD2,par_red1D2,unmark_type]); + +val reducL_ss = reduc_ss setloop (SELECT_GOAL (safe_tac reduc_cs)); + +val red1_induct = Sred1.mutual_induct RS spec RS spec RSN (2,rev_mp); +val red_induct = Sred.mutual_induct RS spec RS spec RSN (2,rev_mp); +val par_red1_induct = Spar_red1.mutual_induct RS spec RS spec RSN (2,rev_mp); +val par_red_induct = Spar_red.mutual_induct RS spec RS spec RSN (2,rev_mp); + +(* ------------------------------------------------------------------------- *) +(* Lemmas for reduction *) +(* ------------------------------------------------------------------------- *) + +goal Reduction.thy "!!u. m--->n ==> Fun(m) ---> Fun(n)"; +by (eresolve_tac [red_induct] 1); +by (resolve_tac [Sred.trans] 3); +by (ALLGOALS (asm_simp_tac reduc_ss )); +val red_Fun = result(); + +goal Reduction.thy + "!!u.[|n:lambda; m ---> m'|]==> Apl(m,n)--->Apl(m',n)"; +by (eresolve_tac [red_induct] 1); +by (resolve_tac [Sred.trans] 3); +by (ALLGOALS (asm_simp_tac reduc_ss )); +val red_Apll = result(); + +goal Reduction.thy + "!!u.[|n:lambda; m ---> m'|]==> Apl(n,m)--->Apl(n,m')"; +by (eresolve_tac [red_induct] 1); +by (resolve_tac [Sred.trans] 3); +by (ALLGOALS (asm_simp_tac reduc_ss )); +val red_Aplr = result(); + +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 (reduc_ss addsimps [red_Apll,red_Aplr]) )); +val red_Apl = result(); + +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 (reduc_ss addsimps [red_Apl,red_Fun]) )); +val red_beta = result(); + + +(* ------------------------------------------------------------------------- *) +(* Lemmas for parallel reduction *) +(* ------------------------------------------------------------------------- *) + + +goal Reduction.thy "!!u.m:lambda==> m =1=> m"; +by (eresolve_tac [lambda.induct] 1); +by (ALLGOALS (asm_simp_tac reduc_ss )); +val refl_par_red1 = result(); + +goal Reduction.thy "!!u.m-1->n ==> m=1=>n"; +by (eresolve_tac [red1_induct] 1); +by (ALLGOALS (asm_simp_tac (reduc_ss addsimps [refl_par_red1]) )); +val red1_par_red1 = result(); + +goal Reduction.thy "!!u.m--->n ==> m===>n"; +by (eresolve_tac [red_induct] 1); +by (resolve_tac [Spar_red.trans] 3); +by (ALLGOALS (asm_simp_tac (reduc_ss addsimps [refl_par_red1,red1_par_red1]) )); +val red_par_red = result(); + +goal Reduction.thy "!!u.m===>n ==> m--->n"; +by (eresolve_tac [par_red_induct] 1); +by (eresolve_tac [par_red1_induct] 1); +by (resolve_tac [Sred.trans] 5); +by (ALLGOALS (asm_simp_tac (reduc_ss addsimps [red_Fun,red_beta,red_Apl]) )); +val par_red_red = result(); + + +(* ------------------------------------------------------------------------- *) +(* Simulation *) +(* ------------------------------------------------------------------------- *) + +goal Reduction.thy + "!!u.m=1=>n ==> EX v. m|>v = n & m~v & regular(v)"; +by (eresolve_tac [par_red1_induct] 1); +by (step_tac ZF_cs 1); +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 (reduc_ss))); +val simulation = result(); + + +(* ------------------------------------------------------------------------- *) +(* commuting of unmark and subst *) +(* ------------------------------------------------------------------------- *) + +goal Reduction.thy + "!!u.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 reduc_ss))); +val unmmark_lift_rec = result(); + +goal Reduction.thy + "!!u.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 reduc_ss) addsimps [unmmark_lift_rec]))); +val unmmark_subst_rec = result(); + + +(* ------------------------------------------------------------------------- *) +(* Completeness *) +(* ------------------------------------------------------------------------- *) + +goal Reduction.thy + "!!u.u~v ==> regular(v) --> unmark(u) =1=> unmark(u|>v)"; +by (eresolve_tac [comp_induct] 1); +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(); + +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 (ALLGOALS (asm_full_simp_tac (reduc_ss addsimps [lambda_unmark]) )); +val completeness = result(); diff -r 5133479a37cf -r 5ba0314f8214 src/ZF/Resid/Reduction.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Resid/Reduction.thy Thu Apr 13 15:38:07 1995 +0200 @@ -0,0 +1,60 @@ +(* Title: Reduction.thy + ID: $Id$ + Author: Ole Rasmussen + Copyright 1995 University of Cambridge + Logic Image: ZF +*) + +Reduction = Terms+ + +consts + Sred1, Sred, Spar_red1,Spar_red :: "i" + "-1->","--->","=1=>", "===>" :: "[i,i]=>o" (infixl 50) + +translations + "a -1-> b" == ":Sred1" + "a ---> b" == ":Sred" + "a =1=> b" == ":Spar_red1" + "a ===> b" == ":Spar_red" + + +inductive + domains "Sred1" <= "lambda*lambda" + intrs + beta "[|m:lambda; n:lambda|] ==> Apl(Fun(m),n) -1-> n/m" + rfun "[|m -1-> n|] ==> Fun(m) -1-> Fun(n)" + apl_l "[|m2:lambda; m1 -1-> n1|] ==> \ +\ Apl(m1,m2) -1-> Apl(n1,m2)" + apl_r "[|m1:lambda; m2 -1-> n2|] ==> \ +\ Apl(m1,m2) -1-> Apl(m1,n2)" + type_intrs "red_typechecks" + +inductive + domains "Sred" <= "lambda*lambda" + intrs + one_step "[|m-1->n|] ==> m--->n" + refl "m:lambda==>m --->m" + trans "[|m--->n; n--->p|]==>m--->p" + type_intrs "[Sred1.dom_subset RS subsetD]@red_typechecks" + +inductive + domains "Spar_red1" <= "lambda*lambda" + intrs + beta "[|m =1=> m'; \ +\ n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'" + rvar "n:nat==> Var(n) =1=> Var(n)" + rfun "[|m =1=> m'|]==> Fun(m) =1=> Fun(m')" + rapl "[|m =1=> m'; \ +\ n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')" + type_intrs "red_typechecks" + + inductive + domains "Spar_red" <= "lambda*lambda" + intrs + one_step "[|m =1=> n|] ==> m ===> n" + trans "[|m===>n; n===>p|]==>m===>p" + type_intrs "[Spar_red1.dom_subset RS subsetD]@red_typechecks" + + +end + diff -r 5133479a37cf -r 5ba0314f8214 src/ZF/Resid/Residuals.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Resid/Residuals.ML Thu Apr 13 15:38:07 1995 +0200 @@ -0,0 +1,213 @@ +(* Title: Residuals.ML + ID: $Id$ + Author: Ole Rasmussen + Copyright 1995 University of Cambridge + Logic Image: ZF +*) + +open Residuals; + +(* ------------------------------------------------------------------------- *) +(* Setting up rule lists *) +(* ------------------------------------------------------------------------- *) + +val residuals_induct = standard + (Sres.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)); + +val res_cs = union_cs + addIs (Sres.intrs@redexes.intrs@Sreg.intrs@ + [subst_type]@nat_typechecks) + addSEs (redexes.free_SEs@ + [Sres.mk_cases redexes.con_defs "residuals(Var(n),Var(n),v)", + Sres.mk_cases redexes.con_defs "residuals(Fun(t),Fun(u),v)", + Sres.mk_cases redexes.con_defs + "residuals(App(b, u1, u2), App(0, v1, v2),v)", + Sres.mk_cases redexes.con_defs + "residuals(App(b, u1, u2), App(1, Fun(v1), v2),v)", + Sres.mk_cases redexes.con_defs "residuals(Var(n),u,v)", + Sres.mk_cases redexes.con_defs "residuals(Fun(t),u,v)", + Sres.mk_cases redexes.con_defs "residuals(App(b, u1, u2), w,v)", + Sres.mk_cases redexes.con_defs "residuals(u,Var(n),v)", + Sres.mk_cases redexes.con_defs "residuals(u,Fun(t),v)", + Sres.mk_cases redexes.con_defs "residuals(w,App(b, u1, u2),v)", + Ssub.mk_cases redexes.con_defs "Var(n) <== u", + Ssub.mk_cases redexes.con_defs "Fun(n) <== u", + Ssub.mk_cases redexes.con_defs "u <== Fun(n)", + Ssub.mk_cases redexes.con_defs "App(1,Fun(t),a) <== u", + Ssub.mk_cases redexes.con_defs "App(0,t,a) <== u", + redexes.mk_cases redexes.con_defs "Fun(t):redexes"]); + +val res_ss = subst_ss addsimps (Sres.intrs); +val resD1 =Sres.dom_subset RS subsetD RS SigmaD1; +val resD2 =Sres.dom_subset RS subsetD RS SigmaD2 RS SigmaD1; +val resD3 =Sres.dom_subset RS subsetD RS SigmaD2 RS SigmaD2; + + +(* ------------------------------------------------------------------------- *) +(* residuals is a partial function *) +(* ------------------------------------------------------------------------- *) + +goal Residuals.thy + "!!u.residuals(u,v,w) ==> ALL w1.residuals(u,v,w1) --> w1 = w"; +by (eresolve_tac [residuals_induct] 1); +by (ALLGOALS (fast_tac res_cs )); +val residuals_function = result(); +val res_is_func = residuals_function RS spec RS mp; + +goal Residuals.thy + "!!u.u~v ==> regular(v) --> (EX w.residuals(u,v,w))"; +by (eresolve_tac [comp_induct] 1); +by (ALLGOALS (fast_tac res_cs)); +val residuals_intro = result(); + +val prems = goal Residuals.thy + "[|u~v; residuals(u,v,THE w. residuals(u, v, w))==> R; \ +\ regular(v)|] ==> R"; +by (cut_facts_tac prems 1); +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 (res_cs addIs [res_is_func]))); +val comp_resfuncE = result(); + + +(* ------------------------------------------------------------------------- *) +(* Residual function *) +(* ------------------------------------------------------------------------- *) + +val resfunc_cs = (res_cs addIs [the_equality,res_is_func] + 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(); + +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(); + +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(); + +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(); + +goal Residuals.thy + "!!n.[|s~t; regular(t)|]==> regular(t) --> s |> t:redexes"; +by (eresolve_tac [comp_induct] 1); +by (ALLGOALS (asm_full_simp_tac + (res_ss addsimps [res_Var,res_Fun,res_App,res_redex] + setloop (SELECT_GOAL (safe_tac res_cs))))); +by (dres_inst_tac [("psi", "Fun(?u) |> ?v : redexes")] asm_rl 1); +by (asm_full_simp_tac + (res_ss addsimps [res_Fun] + setloop (SELECT_GOAL (safe_tac res_cs))) 1); +val resfunc_type = result(); + +val res1_ss = (res_ss addsimps + [res_Var,res_Fun,res_App,res_redex,lift_rec_preserve_comp, + lift_rec_preserve_reg,subst_rec_preserve_comp,resfunc_type, + subst_rec_preserve_reg]@redexes.free_iffs); + +val res1L_ss = res1_ss setloop (SELECT_GOAL (safe_tac res_cs)); + +(* ------------------------------------------------------------------------- *) +(* Commutation theorem *) +(* ------------------------------------------------------------------------- *) + +goal Residuals.thy + "!!u.u<==v ==> u~v"; +by (eresolve_tac [sub_induct] 1); +by (ALLGOALS (asm_simp_tac res1_ss)); +val sub_comp = result(); + +goal Residuals.thy + "!!u.u<==v ==> regular(v) --> regular(u)"; +by (eresolve_tac [sub_induct] 1); +by (ALLGOALS (asm_simp_tac res1L_ss)); +val sub_preserve_reg = result(); + +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 (eresolve_tac [comp_induct] 1); +by (step_tac res_cs 1); +by (ALLGOALS (asm_full_simp_tac ((addsplit res1_ss) 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 res1_ss 1); +val residuals_lift_rec = result(); + +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 (eresolve_tac [comp_induct] 1); +by (step_tac (res_cs) 1); +by (ALLGOALS + (asm_full_simp_tac ((addsplit res1_ss) addsimps ([residuals_lift_rec])))); +by (dres_inst_tac [("psi", "ALL x.?P(x)")] asm_rl 1); +by (asm_full_simp_tac (res1_ss addsimps ([substitution])) 1); +val residuals_subst_rec = result(); + + +goal Residuals.thy + "!!u.[|u1~u2; v1~v2; regular(u2); regular(v2)|]==>\ +\ (v1/u1) |> (v2/u2) = (v1 |> v2)/(u1 |> u2)"; +by (asm_simp_tac (res1_ss addsimps ([residuals_subst_rec])) 1); +val commutation = result(); + +(* ------------------------------------------------------------------------- *) +(* Residuals are comp and regular *) +(* ------------------------------------------------------------------------- *) + +goal Residuals.thy + "!!u.u~v ==> ALL w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)"; +by (eresolve_tac [comp_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); +val residuals_preserve_comp = result(); + + +goal Residuals.thy + "!!u.u~v ==> regular(u) --> regular(v) --> regular(u|>v)"; +by (eresolve_tac [comp_induct] 1); +by (safe_tac res_cs); +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(); + +(* ------------------------------------------------------------------------- *) +(* Preservation lemma *) +(* ------------------------------------------------------------------------- *) + +goal Residuals.thy + "!!u.u~v ==> v ~ (u un v)"; +by (eresolve_tac [comp_induct] 1); +by (ALLGOALS (asm_full_simp_tac res_ss)); +val union_preserve_comp = result(); + +goal Residuals.thy + "!!u.u ~ v ==> regular(v) --> u|>v = (u un v)|>v"; +by (eresolve_tac [comp_induct] 1); +by (safe_tac res_cs); +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 (asm_full_simp_tac (res1_ss 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; diff -r 5133479a37cf -r 5ba0314f8214 src/ZF/Resid/Residuals.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Resid/Residuals.thy Thu Apr 13 15:38:07 1995 +0200 @@ -0,0 +1,36 @@ +(* Title: Residuals.thy + ID: $Id$ + Author: Ole Rasmussen + Copyright 1995 University of Cambridge + Logic Image: ZF + +*) + +Residuals = Substitution+ + +consts + Sres :: "i" + residuals :: "[i,i,i]=>i" + "|>" :: "[i,i]=>i" (infixl 70) + +translations + "residuals(u,v,w)" == ":Sres" + +inductive + domains "Sres" <= "redexes*redexes*redexes" + intrs + Res_Var "n:nat ==> residuals(Var(n),Var(n),Var(n))" + Res_Fun "[|residuals(u,v,w)|]==> \ +\ residuals(Fun(u),Fun(v),Fun(w))" + Res_App "[|residuals(u1,v1,w1); \ +\ residuals(u2,v2,w2); b:bool|]==> \ +\ residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))" + Res_redex "[|residuals(u1,v1,w1); \ +\ residuals(u2,v2,w2); b:bool|]==> \ +\ residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)" + type_intrs "[subst_type]@nat_typechecks@redexes.intrs@bool_typechecks" + +rules + res_func_def "u |> v == THE w.residuals(u,v,w)" +end + diff -r 5133479a37cf -r 5ba0314f8214 src/ZF/Resid/SubUnion.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Resid/SubUnion.ML Thu Apr 13 15:38:07 1995 +0200 @@ -0,0 +1,135 @@ +(* Title: SubUnion.ML + ID: $Id$ + Author: Ole Rasmussen + Copyright 1995 University of Cambridge + Logic Image: ZF +*) + +open SubUnion; + +fun rotate n i = EVERY(replicate n (etac revcut_rl i)); +(* ------------------------------------------------------------------------- *) +(* Specialisation of comp-rules *) +(* ------------------------------------------------------------------------- *) + +val comp_induct = standard + (Scomp.mutual_induct RS spec RS spec RSN (2,rev_mp)); + +val compD1 =Scomp.dom_subset RS subsetD RS SigmaD1; +val compD2 =Scomp.dom_subset RS subsetD RS SigmaD2; + +val regD =Sreg.dom_subset RS subsetD; + +(* ------------------------------------------------------------------------- *) +(* Equality rules for union *) +(* ------------------------------------------------------------------------- *) + +goalw SubUnion.thy [union_def] + "!!u.n:nat==>Var(n) un Var(n)=Var(n)"; +by (asm_simp_tac redexes_ss 1); +by (simp_tac (rank_ss addsimps redexes.con_defs) 1); +val union_Var = result(); + +goalw SubUnion.thy [union_def] + "!!u.[|u:redexes; v:redexes|]==>Fun(u) un Fun(v)=Fun(u un v)"; +by (asm_simp_tac redexes_ss 1); +by (simp_tac (rank_ss addsimps redexes.con_defs) 1); +val union_Fun = result(); + +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 redexes_ss 1); +by (simp_tac (rank_ss addsimps redexes.con_defs) 1); +val union_App = result(); + +val union_ss = redexes_ss addsimps + (Ssub.intrs@bool_simps@bool_typechecks@ + Sreg.intrs@Scomp.intrs@ + [or_1 RSN (3,or_commute RS trans), + or_0 RSN (3,or_commute RS trans), + union_App,union_Fun,union_Var,compD2,compD1,regD]); + +val union_cs = (ZF_cs addIs Scomp.intrs addSEs + [Sreg.mk_cases redexes.con_defs "regular(App(b,f,a))", + Sreg.mk_cases redexes.con_defs "regular(Fun(b))", + Sreg.mk_cases redexes.con_defs "regular(Var(b))", + Scomp.mk_cases redexes.con_defs "Fun(u) ~ Fun(t)", + Scomp.mk_cases redexes.con_defs "u ~ Fun(t)", + Scomp.mk_cases redexes.con_defs "u ~ Var(n)", + Scomp.mk_cases redexes.con_defs "u ~ App(b,t,a)", + Scomp.mk_cases redexes.con_defs "Fun(t) ~ v", + Scomp.mk_cases redexes.con_defs "App(b,f,a) ~ v", + Scomp.mk_cases redexes.con_defs "Var(n) ~ u" + ]); + + + +(* ------------------------------------------------------------------------- *) +(* comp proofs *) +(* ------------------------------------------------------------------------- *) + +goal SubUnion.thy "!!u.u:redexes ==> u ~ u"; +by (eresolve_tac [redexes.induct] 1); +by (ALLGOALS(fast_tac union_cs)); +val comp_refl = result(); + +goal SubUnion.thy + "!!u.u ~ v ==> v ~ u"; +by (eresolve_tac [comp_induct] 1); +by (ALLGOALS(fast_tac union_cs)); +val comp_sym = result(); + +goal SubUnion.thy + "u ~ v <-> v ~ u"; +by (fast_tac (ZF_cs addIs [comp_sym]) 1); +val comp_sym_iff = result(); + + +goal SubUnion.thy + "!!u.u ~ v ==> ALL w.v ~ w-->u ~ w"; +by (eresolve_tac [comp_induct] 1); +by (ALLGOALS(fast_tac union_cs)); +val comp_trans1 = result(); + +val comp_trans = comp_trans1 RS spec RS mp; + +(* ------------------------------------------------------------------------- *) +(* union proofs *) +(* ------------------------------------------------------------------------- *) + +val sub_induct = standard + (Ssub.mutual_induct RS spec RS spec RSN (2,rev_mp)); + +goal SubUnion.thy + "!!u.u ~ v ==> u <== (u un v)"; +by (eresolve_tac [comp_induct] 1); +by (eresolve_tac [boolE] 3); +by (ALLGOALS(asm_full_simp_tac union_ss)); +val union_l = result(); + +goal SubUnion.thy + "!!u.u ~ v ==> v <== (u un v)"; +by (eresolve_tac [comp_induct] 1); +by (eres_inst_tac [("c","b2")] boolE 3); +by (ALLGOALS(asm_full_simp_tac union_ss)); +val union_r = result(); + +goal SubUnion.thy + "!!u.u ~ v ==> u un v = v un u"; +by (eresolve_tac [comp_induct] 1); +by (ALLGOALS(asm_simp_tac (union_ss addsimps [or_commute]))); +val union_sym = result(); + +(* ------------------------------------------------------------------------- *) +(* regular proofs *) +(* ------------------------------------------------------------------------- *) + +goal SubUnion.thy + "!!u.u ~ v ==> regular(u)-->regular(v)-->regular(u un v)"; +by (eresolve_tac [comp_induct] 1); +by (ALLGOALS(asm_full_simp_tac + (union_ss setloop(SELECT_GOAL (safe_tac union_cs))))); +by (dres_inst_tac [("psi", "regular(Fun(?u) un ?v)")] asm_rl 1); +by (asm_full_simp_tac union_ss 1); +val union_preserve_regular = result(); diff -r 5133479a37cf -r 5ba0314f8214 src/ZF/Resid/SubUnion.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Resid/SubUnion.thy Thu Apr 13 15:38:07 1995 +0200 @@ -0,0 +1,59 @@ +(* Title: SubUnion.thy + ID: $Id$ + Author: Ole Rasmussen + Copyright 1995 University of Cambridge + Logic Image: ZF +*) + +SubUnion = Redex + + +consts + Ssub,Scomp,Sreg :: "i" + "<==","~" :: "[i,i]=>o" (infixl 70) + un :: "[i,i]=>i" (infixl 70) + regular :: "i=>o" + +translations + "a<==b" == ":Ssub" + "a ~ b" == ":Scomp" + "regular(a)" == "a:Sreg" + +inductive + domains "Ssub" <= "redexes*redexes" + intrs + Sub_Var "n:nat ==> Var(n)<== Var(n)" + Sub_Fun "[|u<== v|]==> Fun(u)<== Fun(v)" + Sub_App1 "[|u1<== v1; u2<== v2; b:bool|]==> \ +\ App(0,u1,u2)<== App(b,v1,v2)" + Sub_App2 "[|u1<== v1; u2<== v2|]==> \ +\ App(1,u1,u2)<== App(1,v1,v2)" + type_intrs "redexes.intrs@bool_typechecks" + +inductive + domains "Scomp" <= "redexes*redexes" + intrs + Comp_Var "n:nat ==> Var(n) ~ Var(n)" + Comp_Fun "[|u ~ v|]==> Fun(u) ~ Fun(v)" + Comp_App "[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==> \ +\ App(b1,u1,u2) ~ App(b2,v1,v2)" + type_intrs "redexes.intrs@bool_typechecks" + +inductive + domains "Sreg" <= "redexes" + intrs + Reg_Var "n:nat ==> regular(Var(n))" + Reg_Fun "[|regular(u)|]==> regular(Fun(u))" + Reg_App1 "[|regular(Fun(u)); regular(v) \ +\ |]==>regular(App(1,Fun(u),v))" + Reg_App2 "[|regular(u); regular(v) \ +\ |]==>regular(App(0,u,v))" + type_intrs "redexes.intrs@bool_typechecks" + +defs + union_def "u un v == redex_rec(u, \ +\ %i.lam t:redexes.redexes_case(%j.Var(i), %x.0, %b x y.0, t), \ +\ %x m.lam t:redexes.redexes_case(%j.0, %y.Fun(m`y), %b y z.0, t), \ +\%b x y m p.lam t:redexes.redexes_case(%j.0, %y.0, \ +\ %c z u. App(b or c, m`z, p`u), t))`v" +end + diff -r 5133479a37cf -r 5ba0314f8214 src/ZF/Resid/Substitution.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Resid/Substitution.ML Thu Apr 13 15:38:07 1995 +0200 @@ -0,0 +1,294 @@ +(* Title: Substitution.ML + ID: $Id$ + Author: Ole Rasmussen + Copyright 1995 University of Cambridge + Logic Image: ZF +*) + +open Substitution; + +(* ------------------------------------------------------------------------- *) +(* Arithmetic extensions *) +(* ------------------------------------------------------------------------- *) + +goal Arith.thy + "!!m.[| p < n; n:nat|]==> n~=p"; +by (fast_tac lt_cs 1); +val gt_not_eq = result(); + +val succ_pred = prove_goal Arith.thy + "!!i.[|j:nat; i:nat|]==> i < j --> succ(j #- 1) = j" + (fn prems =>[(etac nat_induct 1), + (fast_tac lt_cs 1), + (asm_simp_tac arith_ss 1)]); + +goal Arith.thy + "!!i.[|succ(x) x < n#-1 "; +by (resolve_tac [succ_leE] 1); +by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1); +by (asm_simp_tac (arith_ss addsimps [succ_pred]) 1); +val lt_pred = result(); + +goal Arith.thy + "!!i.[|n < succ(x); p n#-1 < x "; +by (resolve_tac [succ_leE] 1); +by (asm_simp_tac (arith_ss addsimps [succ_pred]) 1); +val gt_pred = result(); + + +val lift_ss = (union_ss addsimps + [add_0_right,add_succ_right,nat_into_Ord, + not_lt_iff_le,if_P,if_not_P]); + + +(* ------------------------------------------------------------------------- *) +(* lift_rec equality rules *) +(* ------------------------------------------------------------------------- *) +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 lift_ss 1); +val lift_rec_le = result(); + +goalw Substitution.thy [lift_rec_def] + "!!n.[|i:nat; k:nat; i lift_rec(Var(i),k) = Var(i)"; +by (asm_full_simp_tac lift_ss 1); +val lift_rec_gt = result(); + +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 lift_ss 1); +val lift_rec_Fun = result(); + +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 lift_ss 1); +val lift_rec_App = result(); + +(* ------------------------------------------------------------------------- *) +(* substitution quality rules *) +(* ------------------------------------------------------------------------- *) + +goalw Substitution.thy [subst_rec_def] + "!!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 (lift_ss) 1); +val subst_eq = result(); + +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 (lift_ss) 1); +val subst_gt = result(); + +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 (lift_ss addsimps [gt_not_eq,leI]) 1); +val subst_lt = result(); + +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 (lift_ss) 1); +val subst_Fun = result(); + +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 (lift_ss) 1); +val subst_App = result(); + +fun addsplit ss = (ss setloop (split_tac [expand_if]) + addsimps [lift_rec_Var,subst_Var]); + + +goal Substitution.thy + "!!n.u:redexes ==> ALL k:nat.lift_rec(u,k):redexes"; +by (eresolve_tac [redexes.induct] 1); +by (ALLGOALS(asm_full_simp_tac + ((addsplit lift_ss) addsimps [lift_rec_Fun,lift_rec_App]))); +val lift_rec_type_a = result(); +val lift_rec_type = lift_rec_type_a RS bspec; + +goalw Substitution.thy [] + "!!n.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 lift_ss) addsimps [subst_Fun,subst_App, + lift_rec_type]))); +val subst_type_a = result(); +val subst_type = subst_type_a RS bspec RS bspec; + + +val subst_ss = (lift_ss addsimps + [subst_eq,subst_gt,subst_lt,subst_Fun,subst_App,subst_type, + lift_rec_le,lift_rec_gt,lift_rec_Fun,lift_rec_App, + lift_rec_type]); + + +(* ------------------------------------------------------------------------- *) +(* lift and substitution proofs *) +(* ------------------------------------------------------------------------- *) + +goalw Substitution.thy [] + "!!n.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 subst_ss))); +by (step_tac ZF_cs 1); +by (excluded_middle_tac "na < xa" 1); +by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2)); +by (ALLGOALS(asm_full_simp_tac + ((addsplit subst_ss) addsimps [leI]))); +val lift_lift_rec = result(); + + +goalw Substitution.thy [] + "!!n.[|u:redexes; n:nat|]==> \ +\ lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))"; +by (asm_simp_tac (lift_ss addsimps [lift_lift_rec]) 1); +val lift_lift = result(); + +goal Substitution.thy + "!!n.v:redexes ==> \ +\ 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) + THEN (ALLGOALS(asm_simp_tac (subst_ss addsimps [lift_lift])))); +by (step_tac ZF_cs 1); +by (excluded_middle_tac "na < x" 1); +by (asm_full_simp_tac (subst_ss) 1); +by (eres_inst_tac [("j","na")] leE 1); +by (asm_full_simp_tac ((addsplit subst_ss) + addsimps [leI,gt_pred,succ_pred]) 1); +by (hyp_subst_tac 1); +by (asm_full_simp_tac (subst_ss) 1); +by (forw_inst_tac [("j","x")] lt_trans2 1); +by (assume_tac 1); +by (asm_full_simp_tac (subst_ss addsimps [leI]) 1); +val lift_rec_subst_rec = result(); + +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 (subst_ss addsimps [lift_rec_subst_rec]) 1); +val lift_subst = result(); + + +goalw Substitution.thy [] + "!!n.v:redexes ==> \ +\ 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 (subst_ss addsimps [lift_lift])))); +by (step_tac ZF_cs 1); +by (excluded_middle_tac "na < x" 1); +by (asm_full_simp_tac (subst_ss) 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 + (subst_ss addsimps [succ_pred,leI,gt_pred]))); +by (hyp_subst_tac 1); +by (asm_full_simp_tac (subst_ss addsimps [leI]) 1); +by (excluded_middle_tac "na < xa" 1); +by (asm_full_simp_tac (subst_ss) 1); +by (asm_full_simp_tac (subst_ss addsimps [leI]) 1); +val lift_rec_subst_rec_lt = result(); + + +goalw Substitution.thy [] + "!!n.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 subst_ss))); +by (step_tac ZF_cs 1); +by (excluded_middle_tac "na < x" 1); +(* x <= na *) +by (asm_full_simp_tac (subst_ss) 1); +by (asm_full_simp_tac (subst_ss) 1); +val subst_rec_lift_rec = result(); + +goal Substitution.thy + "!!n.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 (subst_ss addsimps + [lift_lift RS sym,lift_rec_subst_rec_lt])))); +by (step_tac ZF_cs 1); +by (excluded_middle_tac "na le succ(xa)" 1); +by (asm_full_simp_tac (subst_ss) 1); +by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1); +by (eresolve_tac [leE] 1); +by (asm_simp_tac (subst_ss addsimps [succ_pred,lt_pred]) 2); +by (forward_tac [succ_leI RS lt_trans] 1 THEN assume_tac 1); +by (forw_inst_tac [("i","x")] + (nat_into_Ord RS le_refl RS lt_trans) 1 THEN assume_tac 1); +by (asm_simp_tac (subst_ss addsimps [succ_pred,lt_pred]) 1); +by (eres_inst_tac [("i","na")] leE 1); +by (asm_full_simp_tac + (subst_ss addsimps [succ_pred,subst_rec_lift_rec,leI]) 2); +by (excluded_middle_tac "na < x" 1); +by (asm_full_simp_tac (subst_ss) 1); +by (eres_inst_tac [("j","na")] leE 1); +by (asm_simp_tac (subst_ss addsimps [gt_pred]) 1); +by (asm_simp_tac (subst_ss addsimps [subst_rec_lift_rec]) 1); +by (forward_tac [lt_trans2] 1 THEN assume_tac 1); +by (asm_simp_tac (subst_ss addsimps [gt_pred]) 1); +val subst_rec_subst_rec = result(); + + +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 (subst_ss addsimps [subst_rec_subst_rec]) 1); +val substitution = result(); + +(* ------------------------------------------------------------------------- *) +(* Preservation lemmas *) +(* Substitution preserves comp and regular *) +(* ------------------------------------------------------------------------- *) + + +goal Substitution.thy + "!!n.[|n:nat; u ~ v|]==> ALL m:nat.lift_rec(u,m) ~ lift_rec(v,m)"; +by (eresolve_tac [comp_induct] 1); +by (ALLGOALS(asm_simp_tac (subst_ss addsimps [comp_refl]))); +val lift_rec_preserve_comp = result(); + +goal Substitution.thy + "!!n.u2 ~ v2 ==> ALL m:nat.ALL u1:redexes.ALL v1:redexes.\ +\ u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)"; +by (eresolve_tac [comp_induct] 1); +by (ALLGOALS(asm_full_simp_tac ((addsplit subst_ss) addsimps + ([lift_rec_preserve_comp,comp_refl])))); +val subst_rec_preserve_comp = result(); + +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 subst_ss))); +val lift_rec_preserve_reg = result(); + +goal Substitution.thy + "!!n.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 subst_ss) addsimps + [lift_rec_preserve_reg]))); +val subst_rec_preserve_reg = result(); diff -r 5133479a37cf -r 5ba0314f8214 src/ZF/Resid/Substitution.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Resid/Substitution.thy Thu Apr 13 15:38:07 1995 +0200 @@ -0,0 +1,46 @@ +(* Title: Substitution.thy + ID: $Id$ + Author: Ole Rasmussen + Copyright 1995 University of Cambridge + Logic Image: ZF +*) + +Substitution = SubUnion + + +consts + lift_rec :: "[i,i]=> i" + lift :: "i=>i" + subst_rec :: "[i,i,i]=> i" + "'/" :: "[i,i]=>i" (infixl 70) (*subst*) +translations + "lift(r)" == "lift_rec(r,0)" + "u/v" == "subst_rec(u,v,0)" + +defs + lift_rec_def "lift_rec(r,kg) == \ +\ redex_rec(r,%i.(lam k:nat.if(i unmark(u):lambda"; +by (eresolve_tac [redexes.induct] 1); +by (ALLGOALS(asm_simp_tac term_ss)); +val unmark_type = result(); + +goal Terms.thy + "!!u.u:lambda ==> unmark(u) = u"; +by (eresolve_tac [lambda.induct] 1); +by (ALLGOALS(asm_simp_tac term_ss)); +val lambda_unmark = result(); + + +(* ------------------------------------------------------------------------- *) +(* lift and subst preserve lambda *) +(* ------------------------------------------------------------------------- *) + +goal Terms.thy + "!!u.[|v:lambda|]==> ALL k:nat.lift_rec(v,k):lambda"; +by (eresolve_tac [lambda.induct] 1); +by (ALLGOALS(asm_full_simp_tac (addsplit term_ss))); +val liftL_typea = result(); +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 term_ss) addsimps [liftL_type]))); +val substL_typea = result(); +val substL_type = substL_typea RS bspec RS bspec ; + + +(* ------------------------------------------------------------------------- *) +(* type-rule for reduction definitions *) +(* ------------------------------------------------------------------------- *) + +val red_typechecks = [substL_type]@nat_typechecks@lambda.intrs@bool_typechecks; diff -r 5133479a37cf -r 5ba0314f8214 src/ZF/Resid/Terms.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Resid/Terms.thy Thu Apr 13 15:38:07 1995 +0200 @@ -0,0 +1,32 @@ +(* Title: Terms.thy + ID: $Id$ + Author: Ole Rasmussen + Copyright 1995 University of Cambridge + Logic Image: ZF +*) + +Terms = Cube+ + +consts + lambda :: "i" + unmark :: "i=>i" + Apl :: "[i,i]=>i" + +translations + "Apl(n,m)" == "App(0,n,m)" + +inductive + domains "lambda" <= "redexes" + intrs + Lambda_Var " n:nat ==> Var(n):lambda" + Lambda_Fun " u:lambda ==> Fun(u):lambda" + Lambda_App "[|u:lambda; v:lambda|]==> Apl(u,v):lambda" + type_intrs "redexes.intrs@bool_typechecks" + +defs + unmark_def "unmark(u) == redex_rec(u,%i.Var(i), \ +\ %x m.Fun(m), \ +\ %b x y m p.Apl(m,p))" +end + +