Polished the presentation making it completely definitional.

--- a/src/HOL/Lambda/Confluence.ML	Thu May 18 11:51:23 1995 +0200
+++ b/src/HOL/Lambda/Confluence.ML	Mon May 22 14:12:40 1995 +0200
@@ -8,18 +8,32 @@
 
 open Confluence;
 
-goalw Confluence.thy [confluent_def,confluent1_def,diamondP_def]
-  "!!R. confluent1(R) ==> diamondP(R^*)";
+goalw Confluence.thy [confluent1_def,diamond_def]
+  "!!R. confluent1(R) ==> diamond(R^*)";
 by(strip_tac 1);
 be rtrancl_induct 1;
-by(ALLGOALS(fast_tac (HOL_cs addIs [rtrancl_refl] addEs [rtrancl_comp])));
-qed "confluent1";
+by(ALLGOALS(fast_tac (HOL_cs addIs [rtrancl_refl] 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);
+be rtrancl_induct 1;
+by(fast_tac (HOL_cs addSIs [rtrancl_refl]) 1);
+by(fast_tac (HOL_cs addSEs [rtrancl_into_rtrancl]) 1);
+qed "diamond_confluent2";
 
 goalw Confluence.thy [confluent_def]
-  "!!R.[| diamondP(R); T <= R; R <= T^* |] ==> confluent(T)";
+  "!!R.[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)";
 bd rtrancl_mono 1;
 bd rtrancl_mono 1;
-by(fast_tac (HOL_cs addIs [diamondP_confluent1,confluent1]
+by(fast_tac (HOL_cs addIs [diamond_confluent2, confluent2_confluent1,
+                           confluent1_diamond]
                     addDs [subset_antisym]
                     addss (HOL_ss addsimps [rtrancl_idemp])) 1);
 qed "diamond_to_confluence";

--- a/src/HOL/Lambda/Confluence.thy	Thu May 18 11:51:23 1995 +0200
+++ b/src/HOL/Lambda/Confluence.thy	Mon May 22 14:12:40 1995 +0200
@@ -9,19 +9,20 @@
 Confluence = Trancl +
 
 consts
-  confluent, confluent1, diamondP :: "('a*'a)set => bool"
+  confluent, confluent1, confluent2, diamond :: "('a*'a)set => bool"
 
 defs
-  diamondP_def
-  "diamondP(R) ==   \
-\  !x y. (x,y):R --> (!z. (x,z):R --> (EX u. (y,u):R & (z,u):R))" 
+  diamond_def
+  "diamond(R) == !x y z. (x,y):R --> (x,z):R --> (EX u. (y,u):R & (z,u):R)" 
 
-  confluent_def "confluent(R) == diamondP(R^*)"
+  confluent_def "confluent(R) == diamond(R^*)"
 
   confluent1_def
   "confluent1(R) ==
-   !x y. (x,y):R --> (!z. (x,z):R^* --> (EX u. (y,u):R^* & (z,u):R^*))"
+   !x y z. (x,y):R --> (x,z):R^* --> (EX u. (y,u):R^* & (z,u):R^*)"
 
-rules
-  diamondP_confluent1 "diamondP R ==> confluent1(R)"
+  confluent2_def
+  "confluent2(R) ==
+   !x y z. (x,y):R --> (x,z):R^* --> (EX u. (y,u):R^* & (z,u):R)"
+
 end

--- a/src/HOL/Lambda/Lambda.ML	Thu May 18 11:51:23 1995 +0200
+++ b/src/HOL/Lambda/Lambda.ML	Mon May 22 14:12:40 1995 +0200
@@ -78,22 +78,22 @@
 
 goal Lambda.thy "!!s. [| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'";
 by (fast_tac (lambda_cs addIs
-                [rtrancl_beta_AppL,rtrancl_beta_AppR,rtrancl_comp]) 1);
+                [rtrancl_beta_AppL,rtrancl_beta_AppR,rtrancl_trans]) 1);
 qed "rtrancl_beta_App";
 
 (*** subst and lift ***)
 
 fun addsplit ss = ss addsimps [subst_Var] setloop (split_tac [expand_if]);
 
-goal Lambda.thy "subst u (Var n) n = u";
+goal Lambda.thy "(Var n)[u/n] = u";
 by (asm_full_simp_tac (addsplit lambda_ss) 1);
 qed "subst_eq";
 
-goal Lambda.thy "!!s. m<n ==> subst u (Var n) m = Var(pred n)";
+goal Lambda.thy "!!s. m<n ==> (Var n)[u/m] = Var(pred n)";
 by (asm_full_simp_tac (addsplit lambda_ss) 1);
 qed "subst_gt";
 
-goal Lambda.thy "!!s. n<m ==> subst u (Var n) m = Var(n)";
+goal Lambda.thy "!!s. n<m ==> (Var n)[u/m] = Var(n)";
 by (asm_full_simp_tac (addsplit lambda_ss addsimps
                           [less_not_refl2 RS not_sym,less_SucI]) 1);
 qed "subst_lt";
@@ -111,7 +111,7 @@
 qed"lift_lift";
 
 goal Lambda.thy "!m n s. n < Suc m --> \
-\         lift (subst s t n) m = subst (lift s m) (lift t (Suc m)) n";
+\         lift (t[s/n]) m = (lift t (Suc m)) [lift s m / n]";
 by(db.induct_tac "t" 1);
 by(ALLGOALS(asm_simp_tac (lambda_ss addsimps [lift_lift])));
 by(strip_tac 1);
@@ -130,7 +130,7 @@
 
 goal Lambda.thy
   "!n m u. m < Suc n -->\
-\         lift (subst u v n) m = subst (lift u m) (lift v m) (Suc n)";
+\         lift (v[u/n]) m = (lift v m) [lift u m / Suc n]";
 by(db.induct_tac "v" 1);
 by(ALLGOALS(asm_simp_tac (lambda_ss addsimps [lift_lift])));
 by(strip_tac 1);
@@ -146,7 +146,7 @@
 by (asm_full_simp_tac (lambda_ss addsimps [less_SucI]) 1);
 qed "lift_subst_lt";
 
-goal Lambda.thy "!n v. subst v (lift u n) n = u";
+goal Lambda.thy "!n v. (lift u n)[v/n] = u";
 by(db.induct_tac "u" 1);
 by(ALLGOALS(asm_simp_tac lambda_ss));
 by(split_tac [expand_if] 1);
@@ -156,8 +156,7 @@
 
 
 goal Lambda.thy "!m n u w. m < Suc n --> \
-\ subst (subst w u n) (subst (lift w m) v (Suc n)) m = \
-\ subst w (subst u v m) n";
+\ (v[lift w m / Suc n]) [u[w/n]/m] = (v[u/m])[w/n]";
 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])));

--- a/src/HOL/Lambda/Lambda.thy	Thu May 18 11:51:23 1995 +0200
+++ b/src/HOL/Lambda/Lambda.thy	Mon May 22 14:12:40 1995 +0200
@@ -12,14 +12,14 @@
 datatype db = Var nat | "@" db db (infixl 200) | Fun db
 
 consts
-  subst  :: "[db,db,nat]=>db"
+  subst  :: "[db,db,nat]=>db" ("_[_'/_]" [300,0,0] 300)
   lift   :: "[db,nat] => db"
 
 primrec subst db
-  subst_Var "subst s (Var i) n = (if n < i then Var(pred i)
-                                  else if i = n then s else Var i)"
-  subst_App "subst s (t @ u) n = (subst s t n) @ (subst s u n)"
-  subst_Fun "subst s (Fun t) n = Fun (subst (lift s 0) t (Suc n))"
+  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])"
 
 primrec lift db
   lift_Var "lift (Var i) n = (if i < n then Var i else Var(Suc i))"
@@ -36,7 +36,7 @@
 
 inductive "beta"
 intrs
-   beta  "(Fun s) @ t -> subst t s 0"
+   beta  "(Fun s) @ t -> s[t/0]"
    appL  "s -> t ==> s@u -> t@u"
    appR  "s -> t ==> u@s -> u@t"
    abs   "s -> t ==> Fun s -> Fun t"

--- a/src/HOL/Lambda/ParRed.ML	Thu May 18 11:51:23 1995 +0200
+++ b/src/HOL/Lambda/ParRed.ML	Mon May 22 14:12:40 1995 +0200
@@ -46,7 +46,7 @@
 be (par_beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1;
 by (ALLGOALS(fast_tac (parred_cs addIs
        [rtrancl_beta_Fun,rtrancl_beta_App,rtrancl_refl,
-        rtrancl_into_rtrancl] addEs [rtrancl_comp])));
+        rtrancl_into_rtrancl] addEs [rtrancl_trans])));
 qed "par_beta_subset_beta";
 
 (*** cd ***)
@@ -59,7 +59,7 @@
 by(simp_tac (parred_ss addsimps [cd_App]) 1);
 qed"cd_App_App";
 
-goal ParRed.thy "cd((Fun s) @ t) = subst (cd t) (cd s) 0";
+goal ParRed.thy "cd((Fun s) @ t) = (cd s)[cd t/0]";
 by(simp_tac (parred_ss addsimps [cd_App,deFun_Fun]) 1);
 qed"cd_App_Fun";
 
@@ -74,7 +74,7 @@
 val parred_ss = parred_ss addsimps [par_beta_lift];
 
 goal ParRed.thy
-  "!s s' t' n. s => s' --> t => t' --> subst s t n => subst s' t' n";
+  "!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]";
 by(db.induct_tac "t" 1);
   by(asm_simp_tac (addsplit parred_ss) 1);
  by(strip_tac 1);
@@ -97,11 +97,11 @@
 
 (*** Confluence ***)
 
-goalw ParRed.thy [diamondP_def] "diamondP par_beta";
+goalw ParRed.thy [diamond_def] "diamond(par_beta)";
 by(fast_tac (HOL_cs addIs [par_beta_cd]) 1);
-qed "diamondP_par_beta";
+qed "diamond_par_beta";
 
 goal ParRed.thy "confluent(beta)";
-by(fast_tac (HOL_cs addIs [diamondP_par_beta,diamond_to_confluence,
+by(fast_tac (HOL_cs addIs [diamond_par_beta,diamond_to_confluence,
                            par_beta_subset_beta,beta_subset_par_beta]) 1);
 qed"beta_confluent";

--- a/src/HOL/Lambda/ParRed.thy	Thu May 18 11:51:23 1995 +0200
+++ b/src/HOL/Lambda/ParRed.thy	Mon May 22 14:12:40 1995 +0200
@@ -4,6 +4,11 @@
     Copyright   1995 TU Muenchen
 
 Parallel reduction and a complete developments function "cd".
+Follows the first two pages of
+
+@article{Takahashi-IC-95,author="Masako Takahashi",
+title="Parallel Reductions in $\lambda$-Calculus",
+journal=IC,year=1995,volume=118,pages="120--127"}
 *)
 
 ParRed = Lambda + Confluence +
@@ -20,7 +25,7 @@
     var   "Var n => Var n"
     abs   "s => t ==> Fun s => Fun t"
     app   "[| s => s'; t => t' |] ==> s @ t => s' @ t'"
-    beta  "[| s => s'; t => t' |] ==> (Fun s) @ t => subst t' s' 0"
+    beta  "[| s => s'; t => t' |] ==> (Fun s) @ t => s'[t'/0]"
 
 consts
   cd  :: "db => db"
@@ -31,7 +36,7 @@
   cd_App "cd(s @ t) = (case s of
             Var n => s @ (cd t) |
             s1 @ s2 => (cd s) @ (cd t) |
-            Fun u => subst (cd t) (deFun(cd s)) 0)"
+            Fun u => deFun(cd s)[cd t/0])"
   cd_Fun "cd(Fun s) = Fun(cd s)"
 
 primrec deFun db