# 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<n ==> (Var n)[u/m] = Var(pred n)";
+goal Lambda.thy "!!s. i<j ==> (Var j)[u/i] = Var(pred j)";
 by (asm_full_simp_tac (addsplit lambda_ss) 1);
 qed "subst_gt";
 
-goal Lambda.thy "!!s. n<m ==> (Var n)[u/m] = Var(n)";
+goal Lambda.thy "!!s. j<i ==> (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"