# HG changeset patch # User nipkow # Date 803817908 -7200 # Node ID 5c5daf97cf2d3cf9954a9a8be7f1ae9434ae2152 # Parent b6e1e74695f6582e977f080eecde79616c7e3c2d Simplified the confluence proofs. Added optimized substitution. diff -r b6e1e74695f6 -r 5c5daf97cf2d src/HOL/Lambda/Confluence.ML --- a/src/HOL/Lambda/Confluence.ML Thu Jun 22 12:44:29 1995 +0200 +++ b/src/HOL/Lambda/Confluence.ML Thu Jun 22 12:45:08 1995 +0200 @@ -8,32 +8,28 @@ open Confluence; -goalw Confluence.thy [confluent1_def,diamond_def] - "!!R. confluent1(R) ==> diamond(R^*)"; -by(strip_tac 1); -be rtrancl_induct 1; -by(ALLGOALS(fast_tac (trancl_cs addEs [rtrancl_trans]))); -qed "confluent1_diamond"; - -goalw Confluence.thy [confluent1_def,confluent2_def] - "!!R. confluent2(R) ==> confluent1(R)"; -by(fast_tac (HOL_cs addIs [r_into_rtrancl]) 1); -qed "confluent2_confluent1"; - -goalw Confluence.thy [confluent2_def,diamond_def] - "!!R. diamond(R) ==> confluent2(R)"; -by(strip_tac 1); +goal Confluence.thy + "!!R. [| !x y z. (x,y):R --> (x,z):S --> (? u. (y,u):S & (z,u):R); \ +\ (x,y):R; (x,z):S^* |] ==> ? u. (y,u):S^* & (z,u):R"; be rtrancl_induct 1; by(fast_tac trancl_cs 1); by(fast_tac (HOL_cs addSEs [rtrancl_into_rtrancl]) 1); -qed "diamond_confluent2"; +qed "commute_rtrancl"; + +goal HOL.thy "!!P. ? x.P(x) & Q(x) ==> ? x. Q(x) & P(x)"; +by(fast_tac HOL_cs 1); +val lemma = result(); + +goalw Confluence.thy [diamond_def] + "!!R. diamond(R) ==> diamond(R^*)"; +by(best_tac (HOL_cs addIs [commute_rtrancl,commute_rtrancl RS lemma]) 1); +qed "diamond_diamond_rtrancl"; goalw Confluence.thy [confluent_def] "!!R.[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)"; bd rtrancl_mono 1; bd rtrancl_mono 1; -by(fast_tac (HOL_cs addIs [diamond_confluent2, confluent2_confluent1, - confluent1_diamond] +by(fast_tac (HOL_cs addIs [diamond_diamond_rtrancl] addDs [subset_antisym] addss (HOL_ss addsimps [rtrancl_idemp])) 1); qed "diamond_to_confluence"; diff -r b6e1e74695f6 -r 5c5daf97cf2d src/HOL/Lambda/Confluence.thy --- a/src/HOL/Lambda/Confluence.thy Thu Jun 22 12:44:29 1995 +0200 +++ b/src/HOL/Lambda/Confluence.thy Thu Jun 22 12:45:08 1995 +0200 @@ -18,14 +18,6 @@ confluent_def "confluent(R) == diamond(R^*)" - confluent1_def - "confluent1(R) == - !x y z. (x,y):R --> (x,z):R^* --> (EX u. (y,u):R^* & (z,u):R^*)" - - confluent2_def - "confluent2(R) == - !x y z. (x,y):R --> (x,z):R^* --> (EX u. (y,u):R^* & (z,u):R)" - Church_Rosser_def "Church_Rosser(R) == - !x y. (x,y) : (R Un converse(R))^* --> (? z. (x,z) : R^* & (y,z) : R^*)" + !x y. (x,y) : (R Un converse(R))^* --> (? z. (x,z) : R^* & (y,z) : R^*)" end diff -r b6e1e74695f6 -r 5c5daf97cf2d src/HOL/Lambda/Lambda.ML --- a/src/HOL/Lambda/Lambda.ML Thu Jun 22 12:44:29 1995 +0200 +++ b/src/HOL/Lambda/Lambda.ML Thu Jun 22 12:45:08 1995 +0200 @@ -47,6 +47,7 @@ by (asm_simp_tac (arith_ss addsimps [Suc_pred]) 1); qed "gt_pred"; + (*** Lambda ***) open Lambda; @@ -85,15 +86,15 @@ fun addsplit ss = ss addsimps [subst_Var] setloop (split_tac [expand_if]); -goal Lambda.thy "(Var n)[u/n] = u"; +goal Lambda.thy "(Var k)[u/k] = u"; by (asm_full_simp_tac (addsplit lambda_ss) 1); qed "subst_eq"; -goal Lambda.thy "!!s. m (Var n)[u/m] = Var(pred n)"; +goal Lambda.thy "!!s. i (Var j)[u/i] = Var(pred j)"; by (asm_full_simp_tac (addsplit lambda_ss) 1); qed "subst_gt"; -goal Lambda.thy "!!s. n (Var n)[u/m] = Var(n)"; +goal Lambda.thy "!!s. j (Var j)[u/i] = Var(j)"; by (asm_full_simp_tac (addsplit lambda_ss addsimps [less_not_refl2 RS not_sym,less_SucI]) 1); qed "subst_lt"; @@ -101,7 +102,7 @@ val lambda_ss = lambda_ss addsimps [subst_eq,subst_gt,subst_lt]; goal Lambda.thy - "!n i. i < Suc n --> lift (lift s i) (Suc n) = lift (lift s n) i"; + "!i k. i < Suc k --> lift (lift s i) (Suc k) = lift (lift s k) i"; by(db.induct_tac "s" 1); by(ALLGOALS(asm_simp_tac lambda_ss)); by(strip_tac 1); @@ -110,33 +111,33 @@ by (ALLGOALS(asm_full_simp_tac ((addsplit lambda_ss) addsimps [less_SucI]))); qed"lift_lift"; -goal Lambda.thy "!m n s. n < Suc m --> \ -\ lift (t[s/n]) m = (lift t (Suc m)) [lift s m / n]"; +goal Lambda.thy "!i j s. j < Suc i --> \ +\ lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]"; by(db.induct_tac "t" 1); by(ALLGOALS(asm_simp_tac (lambda_ss addsimps [lift_lift]))); by(strip_tac 1); -by (excluded_middle_tac "nat < n" 1); +by (excluded_middle_tac "nat < j" 1); by (asm_full_simp_tac lambda_ss 1); by (eres_inst_tac [("j","nat")] leqE 1); by (asm_full_simp_tac ((addsplit lambda_ss) addsimps [less_SucI,gt_pred,Suc_pred]) 1); by (hyp_subst_tac 1); by (asm_simp_tac lambda_ss 1); -by (forw_inst_tac [("j","n")] lt_trans2 1); +by (forw_inst_tac [("j","j")] lt_trans2 1); by (assume_tac 1); by (asm_full_simp_tac (addsplit lambda_ss addsimps [less_SucI]) 1); qed "lift_subst"; val lambda_ss = lambda_ss addsimps [lift_subst]; goal Lambda.thy - "!n m u. m < Suc n -->\ -\ lift (v[u/n]) m = (lift v m) [lift u m / Suc n]"; + "!i j u. i < Suc j -->\ +\ lift (v[u/j]) i = (lift v i) [lift u i / Suc j]"; by(db.induct_tac "v" 1); by(ALLGOALS(asm_simp_tac (lambda_ss addsimps [lift_lift]))); by(strip_tac 1); -by (excluded_middle_tac "nat < n" 1); +by (excluded_middle_tac "nat < j" 1); by (asm_full_simp_tac lambda_ss 1); -by (eres_inst_tac [("i","n")] leqE 1); +by (eres_inst_tac [("i","j")] leqE 1); by (forward_tac [lt_trans1] 1 THEN assume_tac 1); by (ALLGOALS(asm_full_simp_tac (lambda_ss addsimps [Suc_pred,less_SucI,gt_pred]))); @@ -146,7 +147,7 @@ by (asm_full_simp_tac (lambda_ss addsimps [less_SucI]) 1); qed "lift_subst_lt"; -goal Lambda.thy "!n v. (lift u n)[v/n] = u"; +goal Lambda.thy "!k v. (lift u k)[v/k] = u"; by(db.induct_tac "u" 1); by(ALLGOALS(asm_simp_tac lambda_ss)); by(split_tac [expand_if] 1); @@ -155,23 +156,23 @@ val lambda_ss = lambda_ss addsimps [subst_lift]; -goal Lambda.thy "!m n u w. m < Suc n --> \ -\ (v[lift w m / Suc n]) [u[w/n]/m] = (v[u/m])[w/n]"; +goal Lambda.thy "!i j u w. i < Suc j --> \ +\ (v[lift w i / Suc j]) [u[w/j]/i] = (v[u/i])[w/j]"; by(db.induct_tac "v" 1); by (ALLGOALS(asm_simp_tac (lambda_ss addsimps [lift_lift RS spec RS spec RS mp RS sym,lift_subst_lt]))); by(strip_tac 1); -by (excluded_middle_tac "nat < Suc(Suc n)" 1); +by (excluded_middle_tac "nat < Suc(Suc j)" 1); by(asm_full_simp_tac lambda_ss 1); by (forward_tac [lessI RS less_trans] 1); by (eresolve_tac [leqE] 1); by (asm_simp_tac (lambda_ss addsimps [Suc_pred,lt_pred]) 2); by (forward_tac [Suc_mono RS less_trans] 1 THEN assume_tac 1); -by (forw_inst_tac [("i","m")] (lessI RS less_trans) 1); +by (forw_inst_tac [("i","i")] (lessI RS less_trans) 1); by (asm_simp_tac (lambda_ss addsimps [Suc_pred,lt_pred]) 1); by (eres_inst_tac [("i","nat")] leqE 1); by (asm_full_simp_tac (lambda_ss addsimps [Suc_pred,less_SucI]) 2); -by (excluded_middle_tac "nat < m" 1); +by (excluded_middle_tac "nat < i" 1); by (asm_full_simp_tac lambda_ss 1); by (eres_inst_tac [("j","nat")] leqE 1); by (asm_simp_tac (lambda_ss addsimps [gt_pred]) 1); @@ -179,3 +180,31 @@ by (forward_tac [lt_trans2] 1 THEN assume_tac 1); by (asm_simp_tac (lambda_ss addsimps [gt_pred]) 1); bind_thm("subst_subst", result() RS spec RS spec RS spec RS spec RS mp); + +val lambda_ss = lambda_ss addsimps + [liftn_Var,liftn_App,liftn_Fun,substn_Var,substn_App,substn_Fun]; + +(*** Equivalence proof for optimized substitution ***) + +goal Lambda.thy "!k. liftn 0 t k = t"; +by(db.induct_tac "t" 1); +by(ALLGOALS(asm_simp_tac (addsplit lambda_ss))); +qed "liftn_0"; +val lambda_ss = lambda_ss addsimps [liftn_0]; + +goal Lambda.thy "!k. liftn (Suc n) t k = lift (liftn n t k) k"; +by(db.induct_tac "t" 1); +by(ALLGOALS(asm_simp_tac (addsplit lambda_ss))); +by(fast_tac (HOL_cs addDs [add_lessD1]) 1); +qed "liftn_lift"; +val lambda_ss = lambda_ss addsimps [liftn_lift]; + +goal Lambda.thy "!n. substn t s n = t[liftn n s 0 / n]"; +by(db.induct_tac "t" 1); +by(ALLGOALS(asm_simp_tac (addsplit lambda_ss))); +qed "substn_subst_n"; +val lambda_ss = lambda_ss addsimps [substn_subst_n]; + +goal Lambda.thy "substn t s 0 = t[s/0]"; +by(simp_tac lambda_ss 1); +qed "substn_subst_0"; diff -r b6e1e74695f6 -r 5c5daf97cf2d src/HOL/Lambda/Lambda.thy --- a/src/HOL/Lambda/Lambda.thy Thu Jun 22 12:44:29 1995 +0200 +++ b/src/HOL/Lambda/Lambda.thy Thu Jun 22 12:45:08 1995 +0200 @@ -14,17 +14,31 @@ consts subst :: "[db,db,nat]=>db" ("_[_'/_]" [300,0,0] 300) lift :: "[db,nat] => db" + (* optimized versions *) + substn :: "[db,db,nat] => db" + liftn :: "[nat,db,nat] => db" + +primrec lift db + lift_Var "lift (Var i) k = (if i < k then Var i else Var(Suc i))" + lift_App "lift (s @ t) k = (lift s k) @ (lift t k)" + lift_Fun "lift (Fun s) k = Fun(lift s (Suc k))" primrec subst db - subst_Var "(Var i)[s/n] = (if n < i then Var(pred i) - else if i = n then s else Var i)" - subst_App "(t @ u)[s/n] = t[s/n] @ u[s/n]" - subst_Fun "(Fun t)[s/n] = Fun (t[lift s 0 / Suc n])" + subst_Var "(Var i)[s/k] = (if k < i then Var(pred i) + else if i = k then s else Var i)" + subst_App "(t @ u)[s/k] = t[s/k] @ u[s/k]" + subst_Fun "(Fun t)[s/k] = Fun (t[lift s 0 / Suc k])" -primrec lift db - lift_Var "lift (Var i) n = (if i < n then Var i else Var(Suc i))" - lift_App "lift (s @ t) n = (lift s n) @ (lift t n)" - lift_Fun "lift (Fun s) n = Fun(lift s (Suc n))" +primrec liftn db + liftn_Var "liftn n (Var i) k = (if i < k then Var i else Var(i+n))" + liftn_App "liftn n (s @ t) k = (liftn n s k) @ (liftn n t k)" + liftn_Fun "liftn n (Fun s) k = Fun(liftn n s (Suc k))" + +primrec substn db + substn_Var "substn (Var i) s k = (if k < i then Var(pred i) + else if i = k then liftn k s 0 else Var i)" + substn_App "substn (t @ u) s k = (substn t s k) @ (substn u s k)" + substn_Fun "substn (Fun t) s k = Fun (substn t s (Suc k))" consts beta :: "(db * db) set"