# HG changeset patch
# User nipkow
# Date 812972711 -3600
# Node ID ee011b365770b95cdd82faae342a738385fca5d6
# Parent  f6ef556b3eded75b3bc3627b5d6d84ea09e73077
New version with eta reduction.

diff -r f6ef556b3ede -r ee011b365770 src/HOL/Lambda/Eta.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/Eta.ML	Fri Oct 06 10:45:11 1995 +0100
@@ -0,0 +1,248 @@
+(*  Title:      HOL/Lambda/Eta.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1995 TU Muenchen
+
+Eta reduction,
+confluence ot eta,
+commutation of beta/eta,
+confluence of beta+eta
+*)
+
+open Eta;
+
+(* FIXME: add Suc_pred glovbally *)
+Addsimps (Suc_pred :: eta.intrs);
+
+
+val eta_cases = map (eta.mk_cases db.simps)
+    ["Fun s -e> z","s @ t -e> u","Var i -e> t"];
+
+val beta_cases = map (beta.mk_cases db.simps)
+    ["s @ t -> u","Var i -> t"];
+
+(* FIXME: add r_into_rtrancl to trancl_cs ???
+          build on lambda_ss which should build on trancl_cs *)
+val eta_cs = trancl_cs addIs (beta.intrs@eta.intrs)
+                       addSEs (beta_cases@eta_cases);
+
+(*** Arithmetic lemmas ***)
+
+goal Nat.thy "~ Suc n <= n";
+by(simp_tac (simpset_of "Nat" addsimps [le_def]) 1);
+qed "Suc_n_not_le_n";
+
+(* FIXME: move into Nat.ML *)
+goalw Nat.thy [le_def] "(i <= 0) = (i = 0)";
+by(nat_ind_tac "i" 1);
+by(ALLGOALS(Asm_simp_tac));
+qed "le_0";
+Addsimps [le_0];
+
+goal HOL.thy "!!P. P ==> P=True";
+by(fast_tac HOL_cs 1);
+qed "True_eq";
+
+Addsimps [less_not_sym RS True_eq];
+
+(* FIXME: move into Nat.ML *)
+goal Arith.thy "!!i. i<j ==> j<k --> Suc i < k";
+by(nat_ind_tac "k" 1);
+by(ALLGOALS(asm_simp_tac(simpset_of "Arith")));
+by(fast_tac (HOL_cs addDs [Suc_lessD]) 1);
+bind_thm("less_trans_Suc",result() RS mp);
+
+goal Arith.thy "i < j --> pred i < j";
+by(nat_ind_tac "j" 1);
+by(ALLGOALS(asm_simp_tac(simpset_of "Arith")));
+by(nat_ind_tac "j1" 1);
+by(ALLGOALS(asm_simp_tac(simpset_of "Arith")));
+bind_thm("less_imp_pred_less",result() RS mp);
+
+goal Arith.thy "i<j --> ~ pred j < i";
+by(nat_ind_tac "j" 1);
+by(ALLGOALS(asm_simp_tac(simpset_of "Arith")));
+by(fast_tac (HOL_cs addDs [less_imp_pred_less]) 1);
+bind_thm("less_imp_not_pred_less", result() RS mp);
+Addsimps [less_imp_not_pred_less];
+
+goal Nat.thy "i < j --> j < Suc(Suc i) --> j = Suc i";
+by(nat_ind_tac "j" 1);
+by(ALLGOALS(simp_tac(simpset_of "Nat")));
+by(fast_tac (HOL_cs addDs [less_not_sym]) 1);
+bind_thm("less_interval1", result() RS mp RS mp);
+
+
+(*** decr and free ***)
+
+goal Eta.thy "!i k. free (lift t k) i = \
+\                   (i < k & free t i | k < i & free t (pred i))";
+by(db.induct_tac "t" 1);
+by(ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addcongs [conj_cong])));
+by(fast_tac HOL_cs 2);
+by(safe_tac (HOL_cs addSIs [iffI]));
+bd Suc_mono 1;
+by(ALLGOALS(Asm_full_simp_tac));
+by(dtac less_trans_Suc 1 THEN atac 1);
+by(dtac less_trans_Suc 2 THEN atac 2);
+by(ALLGOALS(Asm_full_simp_tac));
+qed "free_lift";
+Addsimps [free_lift];
+
+goal Eta.thy "!i k t. free (s[t/k]) i = \
+\              (free s k & free t i | free s (if i<k then i else Suc i))";
+by(db.induct_tac "s" 1);
+by(ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addsimps
+[less_not_refl2,less_not_refl2 RS not_sym])));
+by(fast_tac HOL_cs 2);
+by(safe_tac (HOL_cs addSIs [iffI]));
+by(ALLGOALS(Asm_simp_tac));
+by(fast_tac (HOL_cs addEs [less_imp_not_pred_less RS notE]) 1);
+by(fast_tac (HOL_cs addDs [less_not_sym]) 1);
+bd Suc_mono 1;
+by(dtac less_interval1 1 THEN atac 1);
+by(asm_full_simp_tac (simpset_of "Nat" addsimps [eq_sym_conv]) 1);
+by(dtac less_trans_Suc 1 THEN atac 1);
+by(Asm_full_simp_tac 1);
+qed "free_subst";
+Addsimps [free_subst];
+
+goal Eta.thy "!!s. s -e> t ==> !i. free t i = free s i";
+be (eta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1;
+by(ALLGOALS(asm_simp_tac (!simpset addsimps [decr_def] addcongs [conj_cong])));
+bind_thm("free_eta",result() RS spec);
+
+goal Eta.thy "!!s. [| s -e> t; ~free s i |] ==> ~free t i";
+by(asm_simp_tac (!simpset addsimps [free_eta]) 1);
+qed "not_free_eta";
+
+goal Eta.thy "!i t u. ~free s i --> s[t/i] = s[u/i]";
+by(db.induct_tac "s" 1);
+by(ALLGOALS(simp_tac (addsplit (!simpset))));
+by(fast_tac HOL_cs 1);
+by(fast_tac HOL_cs 1);
+bind_thm("subst_not_free", result() RS spec RS spec RS spec RS mp);
+
+goalw Eta.thy [decr_def] "!!s. ~free s i ==> s[t/i] = decr s i";
+be subst_not_free 1;
+qed "subst_decr";
+
+goal Eta.thy "!!s. s -e> t ==> !u i. s[u/i] -e> t[u/i]";
+be (eta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1;
+by(ALLGOALS(asm_simp_tac (!simpset addsimps [subst_subst RS sym,decr_def])));
+by(asm_simp_tac (!simpset addsimps [subst_decr]) 1);
+bind_thm("eta_subst",result() RS spec RS spec);
+Addsimps [eta_subst];
+
+goalw Eta.thy [decr_def] "!!s. s -e> t ==> decr s i -e> decr t i";
+be eta_subst 1;
+qed "eta_decr";
+
+(*** Confluence of eta ***)
+
+goalw Eta.thy [id_def]
+  "!x y. x-e> y --> (!z. x-e>z --> (? u. y -e>= u & z -e>= u))";
+br eta.mutual_induct 1;
+by(ALLGOALS(fast_tac (eta_cs addSEs [eta_decr,not_free_eta] addss !simpset)));
+val lemma = result() RS spec RS spec RS mp RS spec RS mp;
+
+goalw Eta.thy [diamond_def,commute_def,square_def] "diamond(eta^=)";
+by(fast_tac (eta_cs addEs [lemma]) 1);
+qed "diamond_refl_eta";
+
+goal Eta.thy "confluent(eta)";
+by(stac (rtrancl_reflcl RS sym) 1);
+by(rtac (diamond_refl_eta RS diamond_confluent) 1);
+qed "eta_confluent";
+
+(*** Congruence rules for ->> ***)
+
+goal Eta.thy "!!s. s -e>> s' ==> Fun s -e>> Fun s'";
+be rtrancl_induct 1;
+by (ALLGOALS(fast_tac (eta_cs addIs [rtrancl_refl,rtrancl_into_rtrancl])));
+qed "rtrancl_eta_Fun";
+
+goal Eta.thy "!!s. s -e>> s' ==> s @ t -e>> s' @ t";
+be rtrancl_induct 1;
+by (ALLGOALS(fast_tac (eta_cs addIs [rtrancl_refl,rtrancl_into_rtrancl])));
+qed "rtrancl_eta_AppL";
+
+goal Eta.thy "!!s. t -e>> t' ==> s @ t -e>> s @ t'";
+be rtrancl_induct 1;
+by (ALLGOALS(fast_tac (eta_cs addIs [rtrancl_refl,rtrancl_into_rtrancl])));
+qed "rtrancl_eta_AppR";
+
+goal Eta.thy "!!s. [| s -e>> s'; t -e>> t' |] ==> s @ t -e>> s' @ t'";
+by (fast_tac (eta_cs addSIs [rtrancl_eta_AppL,rtrancl_eta_AppR]
+                     addIs [rtrancl_trans]) 1);
+qed "rtrancl_eta_App";
+
+(*** Commutation of beta and eta ***)
+
+goal Eta.thy "!!s. s -> t ==> !i. free t i --> free s i";
+be (beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1;
+by(ALLGOALS(Asm_full_simp_tac));
+bind_thm("free_beta", result() RS spec RS mp);
+
+goalw Eta.thy [decr_def] "!s t. s -> t --> (!i. decr s i -> decr t i)";
+br beta.mutual_induct 1;
+by(ALLGOALS(asm_full_simp_tac (!simpset addsimps [subst_subst RS sym])));
+bind_thm("beta_decr", result() RS spec RS spec RS mp RS spec);
+
+goalw Eta.thy [decr_def]
+  "decr (Var i) k = (if i<=k then Var i else Var(pred i))";
+by(simp_tac (addsplit (!simpset) addsimps [le_def]) 1);
+qed "decr_Var";
+Addsimps [decr_Var];
+
+goalw Eta.thy [decr_def] "decr (s@t) i = (decr s i)@(decr t i)";
+by(Simp_tac 1);
+qed "decr_App";
+Addsimps [decr_App];
+
+goalw Eta.thy [decr_def] "decr (Fun s) i = Fun (decr s (Suc i))";
+by(Simp_tac 1);
+qed "decr_Fun";
+Addsimps [decr_Fun];
+
+goal Eta.thy "!i. ~free t (Suc i) --> decr t i = decr t (Suc i)";
+by(db.induct_tac "t" 1);
+by(ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [le_def])));
+by(fast_tac (HOL_cs addDs [less_interval1]) 1);
+by(fast_tac HOL_cs 1);
+qed "decr_not_free";
+Addsimps [decr_not_free];
+
+goal Eta.thy "!s t. s -e> t --> (!i. lift s i -e> lift t i)";
+br eta.mutual_induct 1;
+by(ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [decr_def])));
+by(asm_simp_tac (addsplit (!simpset) addsimps [subst_decr]) 1);
+bind_thm("eta_lift",result() RS spec RS spec RS mp RS spec);
+Addsimps [eta_lift];
+
+goal Eta.thy "!s t i. s -e> t --> u[s/i] -e>> u[t/i]";
+by(db.induct_tac "u" 1);
+by(ALLGOALS(asm_simp_tac (addsplit (!simpset))));
+by(fast_tac (eta_cs addIs [r_into_rtrancl]) 1);
+by(fast_tac (eta_cs addIs [rtrancl_eta_App]) 1);
+by(fast_tac (eta_cs addSIs [rtrancl_eta_Fun,eta_lift]) 1);
+bind_thm("rtrancl_eta_subst", result() RS spec RS spec RS spec RS mp);
+
+goalw Eta.thy [square_def] "square beta eta (eta^*) (beta^=)";
+br beta.mutual_induct 1;
+by(strip_tac 1);
+bes eta_cases 1;
+bes eta_cases 1;
+by(fast_tac (eta_cs addss (!simpset addsimps [subst_decr])) 1);
+by(fast_tac (eta_cs addIs [r_into_rtrancl,eta_subst]) 1);
+by(fast_tac (eta_cs addIs [rtrancl_eta_subst]) 1);
+by(fast_tac (eta_cs addIs [r_into_rtrancl,rtrancl_eta_AppL]) 1);
+by(fast_tac (eta_cs addIs [r_into_rtrancl,rtrancl_eta_AppR]) 1);
+by(fast_tac (eta_cs addIs [r_into_rtrancl,rtrancl_eta_Fun,free_beta,beta_decr]
+                  addss (!simpset addsimps[subst_decr,symmetric decr_def])) 1);
+qed "square_beta_eta";
+
+goal Eta.thy "confluent(beta Un eta)";
+by(REPEAT(ares_tac [square_rtrancl_reflcl_commute,confluent_Un,
+                    beta_confluent,eta_confluent,square_beta_eta] 1));
+qed "confluent_beta_eta";
diff -r f6ef556b3ede -r ee011b365770 src/HOL/Lambda/Eta.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/Eta.thy	Fri Oct 06 10:45:11 1995 +0100
@@ -0,0 +1,36 @@
+(*  Title:      HOL/Lambda/Eta.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1995 TU Muenchen
+
+Eta-reduction and relatives.
+*)
+
+Eta = ParRed + Commutation +
+consts free :: "db => nat => bool"
+       decr :: "[db,nat] => db"
+       eta  :: "(db * db) set"
+
+syntax  "-e>", "-e>>", "-e>=" , "->=" :: "[db,db] => bool" (infixl 50)
+
+translations
+  "s -e>  t" == "(s,t) : eta"
+  "s -e>> t" == "(s,t) : eta^*"
+  "s -e>= t" == "(s,t) : eta^="
+  "s ->=  t" == "(s,t) : beta^="
+
+primrec free Lambda.db
+  free_Var "free (Var j) i = (j=i)"
+  free_App "free (s @ t) i = (free s i | free t i)"
+  free_Fun "free (Fun s) i = free s (Suc i)"
+
+defs
+  decr_def "decr t i == t[Var i/i]"
+
+inductive "eta"
+intrs
+   eta  "~free s 0 ==> Fun(s @ Var 0) -e> decr s 0"
+   appL  "s -e> t ==> s@u -e> t@u"
+   appR  "s -e> t ==> u@s -e> u@t"
+   abs   "s -e> t ==> Fun s -e> Fun t"
+end
diff -r f6ef556b3ede -r ee011b365770 src/HOL/Lambda/Lambda.ML
--- a/src/HOL/Lambda/Lambda.ML	Thu Oct 05 14:45:54 1995 +0100
+++ b/src/HOL/Lambda/Lambda.ML	Fri Oct 06 10:45:11 1995 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Lambda.thy
+(*  Title:      HOL/Lambda/Lambda.ML
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1995 TU Muenchen
@@ -7,7 +7,6 @@
 are ported from Ole Rasmussen's ZF development.  In ZF, m<=n is syntactic
 sugar for m<Suc(n). In HOL <= is a separate operator. Hence we have to prove
 some compatibility lemmas.
-
 *)
 
 (*** Nat ***)
@@ -52,7 +51,8 @@
 
 open Lambda;
 
-Addsimps [if_not_P, not_less_eq];
+Delsimps [less_Suc_eq, subst_Var];
+Addsimps ([if_not_P, not_less_eq] @ beta.intrs);
 
 val lambda_cs = HOL_cs addSIs beta.intrs;
 
@@ -80,50 +80,48 @@
 
 (*** subst and lift ***)
 
-val split_ss = !simpset delsimps [less_Suc_eq,subst_Var]
-                        addsimps [subst_Var]
-                        setloop (split_tac [expand_if]);
+fun addsplit ss = ss addsimps [subst_Var] setloop (split_tac [expand_if]);
 
 goal Lambda.thy "(Var k)[u/k] = u";
-by (asm_full_simp_tac split_ss 1);
+by (asm_full_simp_tac(addsplit(!simpset)) 1);
 qed "subst_eq";
 
 goal Lambda.thy "!!s. i<j ==> (Var j)[u/i] = Var(pred j)";
-by (asm_full_simp_tac split_ss 1);
+by (asm_full_simp_tac(addsplit(!simpset)) 1);
 qed "subst_gt";
 
 goal Lambda.thy "!!s. j<i ==> (Var j)[u/i] = Var(j)";
-by (asm_full_simp_tac (split_ss addsimps
+by (asm_full_simp_tac (addsplit(!simpset) addsimps
                           [less_not_refl2 RS not_sym,less_SucI]) 1);
 qed "subst_lt";
 
 Addsimps [subst_eq,subst_gt,subst_lt];
-val ss = !simpset delsimps [less_Suc_eq, subst_Var];
 
 goal Lambda.thy
   "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
 by(db.induct_tac "t" 1);
-by(ALLGOALS (asm_simp_tac ss));
+by(ALLGOALS Asm_simp_tac);
 by(strip_tac 1);
 by (excluded_middle_tac "nat < i" 1);
 by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2));
-by (ALLGOALS(asm_full_simp_tac (split_ss addsimps [less_SucI])));
+by (ALLGOALS(asm_full_simp_tac (addsplit(!simpset) addsimps [less_SucI])));
 qed"lift_lift";
 
 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 (ss addsimps [lift_lift])));
+by(ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift])));
 by(strip_tac 1);
 by (excluded_middle_tac "nat < j" 1);
-by (asm_full_simp_tac ss 1);
+by (Asm_full_simp_tac 1);
 by (eres_inst_tac [("j","nat")] leqE 1);
-by (asm_full_simp_tac (split_ss addsimps [less_SucI,gt_pred,Suc_pred]) 1);
+by (asm_full_simp_tac (addsplit(!simpset)
+                       addsimps [less_SucI,gt_pred,Suc_pred]) 1);
 by (hyp_subst_tac 1);
 by (Asm_simp_tac 1);
 by (forw_inst_tac [("j","j")] lt_trans2 1);
 by (assume_tac 1);
-by (asm_full_simp_tac (split_ss addsimps [less_SucI]) 1);
+by (asm_full_simp_tac (addsplit(!simpset) addsimps [less_SucI]) 1);
 qed "lift_subst";
 Addsimps [lift_subst];
 
@@ -131,15 +129,16 @@
   "!i j s. i < Suc j -->\
 \         lift (t[s/j]) i = (lift t i) [lift s i / Suc j]";
 by(db.induct_tac "t" 1);
-by(ALLGOALS(asm_simp_tac (ss addsimps [lift_lift])));
+by(ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift])));
 by(strip_tac 1);
 by (excluded_middle_tac "nat < j" 1);
-by (asm_full_simp_tac ss 1);
+by (Asm_full_simp_tac 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 (ss addsimps [Suc_pred,less_SucI,gt_pred])));
+by (ALLGOALS(asm_full_simp_tac
+               (!simpset addsimps [Suc_pred,less_SucI,gt_pred])));
 by (hyp_subst_tac 1);
-by (asm_full_simp_tac (ss addsimps [less_SucI]) 1);
+by (asm_full_simp_tac (!simpset addsimps [less_SucI]) 1);
 by(split_tac [expand_if] 1);
 by (asm_full_simp_tac (!simpset addsimps [less_SucI]) 1);
 qed "lift_subst_lt";
@@ -156,22 +155,21 @@
 goal Lambda.thy "!i j u v. i < Suc j --> \
 \ t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]";
 by(db.induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac (ss addsimps
+by (ALLGOALS(asm_simp_tac (!simpset 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 j)" 1);
-by(asm_full_simp_tac ss 1);
+by(Asm_full_simp_tac 1);
 by (forward_tac [lessI RS less_trans] 1);
 by (eresolve_tac [leqE] 1);
-by (asm_simp_tac (ss addsimps [Suc_pred,lt_pred]) 2);
+by (asm_simp_tac (!simpset addsimps [Suc_pred,lt_pred]) 2);
 by (forward_tac [Suc_mono RS less_trans] 1 THEN assume_tac 1);
 by (forw_inst_tac [("i","i")] (lessI RS less_trans) 1);
-by (asm_simp_tac (ss addsimps [Suc_pred,lt_pred]) 1);
+by (asm_simp_tac (!simpset addsimps [Suc_pred,lt_pred]) 1);
 by (eres_inst_tac [("i","nat")] leqE 1);
-by (asm_full_simp_tac (!simpset delsimps [less_Suc_eq]
-                                addsimps [Suc_pred,less_SucI]) 2);
+by (asm_full_simp_tac (!simpset addsimps [Suc_pred,less_SucI]) 2);
 by (excluded_middle_tac "nat < i" 1);
-by (asm_full_simp_tac ss 1);
+by (Asm_full_simp_tac 1);
 by (eres_inst_tac [("j","nat")] leqE 1);
 by (asm_simp_tac (!simpset addsimps [gt_pred]) 1);
 by (Asm_simp_tac 1);
@@ -184,20 +182,20 @@
 
 goal Lambda.thy "!k. liftn 0 t k = t";
 by(db.induct_tac "t" 1);
-by(ALLGOALS(asm_simp_tac split_ss));
+by(ALLGOALS(asm_simp_tac(addsplit(!simpset))));
 qed "liftn_0";
 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 split_ss));
+by(ALLGOALS(asm_simp_tac(addsplit(!simpset))));
 by(fast_tac (HOL_cs addDs [add_lessD1]) 1);
 qed "liftn_lift";
 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 (!simpset setloop (split_tac [expand_if]))));
+by(ALLGOALS(asm_simp_tac(addsplit(!simpset))));
 qed "substn_subst_n";
 Addsimps [substn_subst_n];
 
diff -r f6ef556b3ede -r ee011b365770 src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Thu Oct 05 14:45:54 1995 +0100
+++ b/src/HOL/Lambda/Lambda.thy	Fri Oct 06 10:45:11 1995 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Lambda.thy
+(*  Title:      HOL/Lambda/Lambda.thy
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1995 TU Muenchen
diff -r f6ef556b3ede -r ee011b365770 src/HOL/Lambda/ParRed.ML
--- a/src/HOL/Lambda/ParRed.ML	Thu Oct 05 14:45:54 1995 +0100
+++ b/src/HOL/Lambda/ParRed.ML	Fri Oct 06 10:45:11 1995 +0100
@@ -59,7 +59,7 @@
 goal ParRed.thy
   "!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]";
 by(db.induct_tac "t" 1);
-  by(asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+  by(asm_simp_tac (addsplit(!simpset)) 1);
  by(strip_tac 1);
  bes par_beta_cases 1;
   by(Asm_simp_tac 1);
@@ -72,7 +72,7 @@
 
 (*** Confluence (directly) ***)
 
-goalw ParRed.thy [diamond_def] "diamond(par_beta)";
+goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
 by(REPEAT(rtac allI 1));
 br impI 1;
 be (par_beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1;
@@ -82,20 +82,6 @@
 
 (*** cd ***)
 
-goal ParRed.thy "cd(Var n @ t) = Var n @ cd t";
-by(Simp_tac 1);
-qed"cd_App_Var";
-
-goal ParRed.thy "cd((r @ s) @ t) = cd(r @ s) @ cd t";
-by(Simp_tac 1);
-qed"cd_App_App";
-
-goal ParRed.thy "cd((Fun s) @ t) = (cd s)[cd t/0]";
-by(Simp_tac 1);
-qed"cd_App_Fun";
-
-Addsimps [cd_App_Var,cd_App_App,cd_App_Fun];
-
 goal ParRed.thy "!t. s => t --> t => cd s";
 by(db.induct_tac "s" 1);
   by(Simp_tac 1);
@@ -106,7 +92,7 @@
 
 (*** Confluence (via cd) ***)
 
-goalw ParRed.thy [diamond_def] "diamond(par_beta)";
+goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
 by(fast_tac (HOL_cs addIs [par_beta_cd]) 1);
 qed "diamond_par_beta2";
 
diff -r f6ef556b3ede -r ee011b365770 src/HOL/Lambda/ParRed.thy
--- a/src/HOL/Lambda/ParRed.thy	Thu Oct 05 14:45:54 1995 +0100
+++ b/src/HOL/Lambda/ParRed.thy	Fri Oct 06 10:45:11 1995 +0100
@@ -6,7 +6,7 @@
 Parallel reduction and a complete developments function "cd".
 *)
 
-ParRed = Lambda + Confluence +
+ParRed = Lambda + Commutation +
 
 consts  par_beta :: "(db * db) set"
 
diff -r f6ef556b3ede -r ee011b365770 src/HOL/Lambda/ROOT.ML
--- a/src/HOL/Lambda/ROOT.ML	Thu Oct 05 14:45:54 1995 +0100
+++ b/src/HOL/Lambda/ROOT.ML	Fri Oct 06 10:45:11 1995 +0100
@@ -1,10 +1,13 @@
-(*  Title: 	HOL/IMP/ROOT.ML
+(*  Title: 	HOL/Lambda/ROOT.ML
     ID:         $Id$
     Author: 	Tobias Nipkow
     Copyright   1995 TUM
 
 Confluence proof for untyped lambda-calculus using de Bruijn's notation.
-Extremely slick proof; follows the first two pages of
+Covers beta, eta, and beta+eta.
+
+Beta is proved confluent both in the traditional way and also following the
+first two pages of
 
 @article{Takahashi-IC-95,author="Masako Takahashi",
 title="Parallel Reductions in $\lambda$-Calculus",
@@ -16,4 +19,4 @@
 
 writeln"Root file for HOL/Lambda";
 loadpath := [".","Lambda"];
-time_use_thy "ParRed";
+time_use_thy "Eta";