--- /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();
--- /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. <x,y>:R --> (ALL z.<x,z>:R --> \
+\ (EX u.<y,u>:R & <z,u>:R))"
+ strip_def "strip == ALL x y. (x ===> y) --> (ALL z.(x =1=> z) --> \
+\ (EX u.(y =1=> u) & (z===>u)))"
+end
+
--- /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();
+
--- /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" == "<a,b>:Sconv1"
+ "a<--->b" == "<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
+
--- /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();
+
--- /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
--- /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";
--- /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));
+
+
+
+
+
--- /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
+
--- /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();
--- /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" == "<a,b>:Sred1"
+ "a ---> b" == "<a,b>:Sred"
+ "a =1=> b" == "<a,b>:Spar_red1"
+ "a ===> b" == "<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
+
--- /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;
--- /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)" == "<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
+
--- /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();
--- /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" == "<a,b>:Ssub"
+ "a ~ b" == "<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
+
--- /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)<n; n:nat; x:nat|]==> 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; p:nat; n:nat; x:nat|]==> 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<n,Var(i),Var(succ(i)))";
+by (asm_full_simp_tac lift_ss 1);
+val lift_rec_Var = result();
+
+goalw Substitution.thy [lift_rec_def]
+ "!!n.[|n:nat; i:nat; k:nat; k le 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<k |]==> 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<i,Var(i#-1),if(k=i,u,Var(i)))";
+by (asm_full_simp_tac (lift_ss addsimps [gt_not_eq,leI]) 1);
+val subst_Var = result();
+
+goalw Substitution.thy [subst_rec_def]
+ "!!n.[|n:nat; u:redexes|]==> 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<n|]==> \
+\ 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<p|]==> \
+\ 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();
--- /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<k,Var(i),Var(succ(i)))), \
+\ %x m.(lam k:nat.Fun(m`(succ(k)))), \
+\ %b x y m p.lam k:nat.App(b,m`k,p`k))`kg"
+
+
+(* subst_rec(u,Var(i),k) = if k<i then Var(i-1)
+ else if k=i then u
+ else Var(i)
+ subst_rec(u,Fun(t),k) = Fun(subst_rec(lift(u),t,succ(k)))
+ subst_rec(u,App(b,f,a),k) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))
+
+*)
+ subst_rec_def "subst_rec(u,t,kg) == \
+\ redex_rec(t, \
+\ %i.(lam r:redexes.lam k:nat. \
+\ if(k<i,Var(i#-1), \
+\ if(k=i,r,Var(i)))), \
+\ %x m.(lam r:redexes.lam k:nat. \
+\ Fun(m`(lift(r))`(succ(k)))), \
+\ %b x y m p.lam r:redexes.lam k:nat. \
+\ App(b,m`r`k,p`r`k))`u`kg"
+
+
+end
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Resid/Terms.ML Thu Apr 13 15:38:07 1995 +0200
@@ -0,0 +1,79 @@
+(* Title: Terms.ML
+ ID: $Id$
+ Author: Ole Rasmussen
+ Copyright 1995 University of Cambridge
+ Logic Image: ZF
+*)
+
+open Terms;
+
+(* ------------------------------------------------------------------------- *)
+(* unmark simplifications *)
+(* ------------------------------------------------------------------------- *)
+
+goalw Terms.thy [unmark_def]
+ "unmark(Var(n)) = Var(n)";
+by (asm_simp_tac lift_ss 1);
+val unmark_Var = result();
+
+goalw Terms.thy [unmark_def]
+ "unmark(Fun(t)) = Fun(unmark(t))";
+by (asm_simp_tac lift_ss 1);
+val unmark_Fun = result();
+
+goalw Terms.thy [unmark_def]
+ "unmark(App(b,n,m)) = App(0,unmark(n),unmark(m))";
+by (asm_simp_tac lift_ss 1);
+val unmark_App = result();
+
+
+(* ------------------------------------------------------------------------- *)
+(* term simplification set *)
+(* ------------------------------------------------------------------------- *)
+
+
+val term_ss = res1_ss addsimps ([unmark_App,unmark_Fun,unmark_Var,
+ lambda.dom_subset RS subsetD]@lambda.intrs);
+
+
+(* ------------------------------------------------------------------------- *)
+(* unmark lemmas *)
+(* ------------------------------------------------------------------------- *)
+
+goalw Terms.thy [unmark_def]
+ "!!u.u:redexes ==> 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;
--- /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
+
+