New version with eta reduction.
authornipkow
Fri Oct 06 10:45:11 1995 +0100 (1995-10-06)
changeset 1269ee011b365770
parent 1268 f6ef556b3ede
child 1270 e3a391e848a9
New version with eta reduction.
src/HOL/Lambda/Eta.ML
src/HOL/Lambda/Eta.thy
src/HOL/Lambda/Lambda.ML
src/HOL/Lambda/Lambda.thy
src/HOL/Lambda/ParRed.ML
src/HOL/Lambda/ParRed.thy
src/HOL/Lambda/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Lambda/Eta.ML	Fri Oct 06 10:45:11 1995 +0100
     1.3 @@ -0,0 +1,248 @@
     1.4 +(*  Title:      HOL/Lambda/Eta.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow
     1.7 +    Copyright   1995 TU Muenchen
     1.8 +
     1.9 +Eta reduction,
    1.10 +confluence ot eta,
    1.11 +commutation of beta/eta,
    1.12 +confluence of beta+eta
    1.13 +*)
    1.14 +
    1.15 +open Eta;
    1.16 +
    1.17 +(* FIXME: add Suc_pred glovbally *)
    1.18 +Addsimps (Suc_pred :: eta.intrs);
    1.19 +
    1.20 +
    1.21 +val eta_cases = map (eta.mk_cases db.simps)
    1.22 +    ["Fun s -e> z","s @ t -e> u","Var i -e> t"];
    1.23 +
    1.24 +val beta_cases = map (beta.mk_cases db.simps)
    1.25 +    ["s @ t -> u","Var i -> t"];
    1.26 +
    1.27 +(* FIXME: add r_into_rtrancl to trancl_cs ???
    1.28 +          build on lambda_ss which should build on trancl_cs *)
    1.29 +val eta_cs = trancl_cs addIs (beta.intrs@eta.intrs)
    1.30 +                       addSEs (beta_cases@eta_cases);
    1.31 +
    1.32 +(*** Arithmetic lemmas ***)
    1.33 +
    1.34 +goal Nat.thy "~ Suc n <= n";
    1.35 +by(simp_tac (simpset_of "Nat" addsimps [le_def]) 1);
    1.36 +qed "Suc_n_not_le_n";
    1.37 +
    1.38 +(* FIXME: move into Nat.ML *)
    1.39 +goalw Nat.thy [le_def] "(i <= 0) = (i = 0)";
    1.40 +by(nat_ind_tac "i" 1);
    1.41 +by(ALLGOALS(Asm_simp_tac));
    1.42 +qed "le_0";
    1.43 +Addsimps [le_0];
    1.44 +
    1.45 +goal HOL.thy "!!P. P ==> P=True";
    1.46 +by(fast_tac HOL_cs 1);
    1.47 +qed "True_eq";
    1.48 +
    1.49 +Addsimps [less_not_sym RS True_eq];
    1.50 +
    1.51 +(* FIXME: move into Nat.ML *)
    1.52 +goal Arith.thy "!!i. i<j ==> j<k --> Suc i < k";
    1.53 +by(nat_ind_tac "k" 1);
    1.54 +by(ALLGOALS(asm_simp_tac(simpset_of "Arith")));
    1.55 +by(fast_tac (HOL_cs addDs [Suc_lessD]) 1);
    1.56 +bind_thm("less_trans_Suc",result() RS mp);
    1.57 +
    1.58 +goal Arith.thy "i < j --> pred i < j";
    1.59 +by(nat_ind_tac "j" 1);
    1.60 +by(ALLGOALS(asm_simp_tac(simpset_of "Arith")));
    1.61 +by(nat_ind_tac "j1" 1);
    1.62 +by(ALLGOALS(asm_simp_tac(simpset_of "Arith")));
    1.63 +bind_thm("less_imp_pred_less",result() RS mp);
    1.64 +
    1.65 +goal Arith.thy "i<j --> ~ pred j < i";
    1.66 +by(nat_ind_tac "j" 1);
    1.67 +by(ALLGOALS(asm_simp_tac(simpset_of "Arith")));
    1.68 +by(fast_tac (HOL_cs addDs [less_imp_pred_less]) 1);
    1.69 +bind_thm("less_imp_not_pred_less", result() RS mp);
    1.70 +Addsimps [less_imp_not_pred_less];
    1.71 +
    1.72 +goal Nat.thy "i < j --> j < Suc(Suc i) --> j = Suc i";
    1.73 +by(nat_ind_tac "j" 1);
    1.74 +by(ALLGOALS(simp_tac(simpset_of "Nat")));
    1.75 +by(fast_tac (HOL_cs addDs [less_not_sym]) 1);
    1.76 +bind_thm("less_interval1", result() RS mp RS mp);
    1.77 +
    1.78 +
    1.79 +(*** decr and free ***)
    1.80 +
    1.81 +goal Eta.thy "!i k. free (lift t k) i = \
    1.82 +\                   (i < k & free t i | k < i & free t (pred i))";
    1.83 +by(db.induct_tac "t" 1);
    1.84 +by(ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addcongs [conj_cong])));
    1.85 +by(fast_tac HOL_cs 2);
    1.86 +by(safe_tac (HOL_cs addSIs [iffI]));
    1.87 +bd Suc_mono 1;
    1.88 +by(ALLGOALS(Asm_full_simp_tac));
    1.89 +by(dtac less_trans_Suc 1 THEN atac 1);
    1.90 +by(dtac less_trans_Suc 2 THEN atac 2);
    1.91 +by(ALLGOALS(Asm_full_simp_tac));
    1.92 +qed "free_lift";
    1.93 +Addsimps [free_lift];
    1.94 +
    1.95 +goal Eta.thy "!i k t. free (s[t/k]) i = \
    1.96 +\              (free s k & free t i | free s (if i<k then i else Suc i))";
    1.97 +by(db.induct_tac "s" 1);
    1.98 +by(ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addsimps
    1.99 +[less_not_refl2,less_not_refl2 RS not_sym])));
   1.100 +by(fast_tac HOL_cs 2);
   1.101 +by(safe_tac (HOL_cs addSIs [iffI]));
   1.102 +by(ALLGOALS(Asm_simp_tac));
   1.103 +by(fast_tac (HOL_cs addEs [less_imp_not_pred_less RS notE]) 1);
   1.104 +by(fast_tac (HOL_cs addDs [less_not_sym]) 1);
   1.105 +bd Suc_mono 1;
   1.106 +by(dtac less_interval1 1 THEN atac 1);
   1.107 +by(asm_full_simp_tac (simpset_of "Nat" addsimps [eq_sym_conv]) 1);
   1.108 +by(dtac less_trans_Suc 1 THEN atac 1);
   1.109 +by(Asm_full_simp_tac 1);
   1.110 +qed "free_subst";
   1.111 +Addsimps [free_subst];
   1.112 +
   1.113 +goal Eta.thy "!!s. s -e> t ==> !i. free t i = free s i";
   1.114 +be (eta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1;
   1.115 +by(ALLGOALS(asm_simp_tac (!simpset addsimps [decr_def] addcongs [conj_cong])));
   1.116 +bind_thm("free_eta",result() RS spec);
   1.117 +
   1.118 +goal Eta.thy "!!s. [| s -e> t; ~free s i |] ==> ~free t i";
   1.119 +by(asm_simp_tac (!simpset addsimps [free_eta]) 1);
   1.120 +qed "not_free_eta";
   1.121 +
   1.122 +goal Eta.thy "!i t u. ~free s i --> s[t/i] = s[u/i]";
   1.123 +by(db.induct_tac "s" 1);
   1.124 +by(ALLGOALS(simp_tac (addsplit (!simpset))));
   1.125 +by(fast_tac HOL_cs 1);
   1.126 +by(fast_tac HOL_cs 1);
   1.127 +bind_thm("subst_not_free", result() RS spec RS spec RS spec RS mp);
   1.128 +
   1.129 +goalw Eta.thy [decr_def] "!!s. ~free s i ==> s[t/i] = decr s i";
   1.130 +be subst_not_free 1;
   1.131 +qed "subst_decr";
   1.132 +
   1.133 +goal Eta.thy "!!s. s -e> t ==> !u i. s[u/i] -e> t[u/i]";
   1.134 +be (eta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1;
   1.135 +by(ALLGOALS(asm_simp_tac (!simpset addsimps [subst_subst RS sym,decr_def])));
   1.136 +by(asm_simp_tac (!simpset addsimps [subst_decr]) 1);
   1.137 +bind_thm("eta_subst",result() RS spec RS spec);
   1.138 +Addsimps [eta_subst];
   1.139 +
   1.140 +goalw Eta.thy [decr_def] "!!s. s -e> t ==> decr s i -e> decr t i";
   1.141 +be eta_subst 1;
   1.142 +qed "eta_decr";
   1.143 +
   1.144 +(*** Confluence of eta ***)
   1.145 +
   1.146 +goalw Eta.thy [id_def]
   1.147 +  "!x y. x-e> y --> (!z. x-e>z --> (? u. y -e>= u & z -e>= u))";
   1.148 +br eta.mutual_induct 1;
   1.149 +by(ALLGOALS(fast_tac (eta_cs addSEs [eta_decr,not_free_eta] addss !simpset)));
   1.150 +val lemma = result() RS spec RS spec RS mp RS spec RS mp;
   1.151 +
   1.152 +goalw Eta.thy [diamond_def,commute_def,square_def] "diamond(eta^=)";
   1.153 +by(fast_tac (eta_cs addEs [lemma]) 1);
   1.154 +qed "diamond_refl_eta";
   1.155 +
   1.156 +goal Eta.thy "confluent(eta)";
   1.157 +by(stac (rtrancl_reflcl RS sym) 1);
   1.158 +by(rtac (diamond_refl_eta RS diamond_confluent) 1);
   1.159 +qed "eta_confluent";
   1.160 +
   1.161 +(*** Congruence rules for ->> ***)
   1.162 +
   1.163 +goal Eta.thy "!!s. s -e>> s' ==> Fun s -e>> Fun s'";
   1.164 +be rtrancl_induct 1;
   1.165 +by (ALLGOALS(fast_tac (eta_cs addIs [rtrancl_refl,rtrancl_into_rtrancl])));
   1.166 +qed "rtrancl_eta_Fun";
   1.167 +
   1.168 +goal Eta.thy "!!s. s -e>> s' ==> s @ t -e>> s' @ t";
   1.169 +be rtrancl_induct 1;
   1.170 +by (ALLGOALS(fast_tac (eta_cs addIs [rtrancl_refl,rtrancl_into_rtrancl])));
   1.171 +qed "rtrancl_eta_AppL";
   1.172 +
   1.173 +goal Eta.thy "!!s. t -e>> t' ==> s @ t -e>> s @ t'";
   1.174 +be rtrancl_induct 1;
   1.175 +by (ALLGOALS(fast_tac (eta_cs addIs [rtrancl_refl,rtrancl_into_rtrancl])));
   1.176 +qed "rtrancl_eta_AppR";
   1.177 +
   1.178 +goal Eta.thy "!!s. [| s -e>> s'; t -e>> t' |] ==> s @ t -e>> s' @ t'";
   1.179 +by (fast_tac (eta_cs addSIs [rtrancl_eta_AppL,rtrancl_eta_AppR]
   1.180 +                     addIs [rtrancl_trans]) 1);
   1.181 +qed "rtrancl_eta_App";
   1.182 +
   1.183 +(*** Commutation of beta and eta ***)
   1.184 +
   1.185 +goal Eta.thy "!!s. s -> t ==> !i. free t i --> free s i";
   1.186 +be (beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1;
   1.187 +by(ALLGOALS(Asm_full_simp_tac));
   1.188 +bind_thm("free_beta", result() RS spec RS mp);
   1.189 +
   1.190 +goalw Eta.thy [decr_def] "!s t. s -> t --> (!i. decr s i -> decr t i)";
   1.191 +br beta.mutual_induct 1;
   1.192 +by(ALLGOALS(asm_full_simp_tac (!simpset addsimps [subst_subst RS sym])));
   1.193 +bind_thm("beta_decr", result() RS spec RS spec RS mp RS spec);
   1.194 +
   1.195 +goalw Eta.thy [decr_def]
   1.196 +  "decr (Var i) k = (if i<=k then Var i else Var(pred i))";
   1.197 +by(simp_tac (addsplit (!simpset) addsimps [le_def]) 1);
   1.198 +qed "decr_Var";
   1.199 +Addsimps [decr_Var];
   1.200 +
   1.201 +goalw Eta.thy [decr_def] "decr (s@t) i = (decr s i)@(decr t i)";
   1.202 +by(Simp_tac 1);
   1.203 +qed "decr_App";
   1.204 +Addsimps [decr_App];
   1.205 +
   1.206 +goalw Eta.thy [decr_def] "decr (Fun s) i = Fun (decr s (Suc i))";
   1.207 +by(Simp_tac 1);
   1.208 +qed "decr_Fun";
   1.209 +Addsimps [decr_Fun];
   1.210 +
   1.211 +goal Eta.thy "!i. ~free t (Suc i) --> decr t i = decr t (Suc i)";
   1.212 +by(db.induct_tac "t" 1);
   1.213 +by(ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [le_def])));
   1.214 +by(fast_tac (HOL_cs addDs [less_interval1]) 1);
   1.215 +by(fast_tac HOL_cs 1);
   1.216 +qed "decr_not_free";
   1.217 +Addsimps [decr_not_free];
   1.218 +
   1.219 +goal Eta.thy "!s t. s -e> t --> (!i. lift s i -e> lift t i)";
   1.220 +br eta.mutual_induct 1;
   1.221 +by(ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [decr_def])));
   1.222 +by(asm_simp_tac (addsplit (!simpset) addsimps [subst_decr]) 1);
   1.223 +bind_thm("eta_lift",result() RS spec RS spec RS mp RS spec);
   1.224 +Addsimps [eta_lift];
   1.225 +
   1.226 +goal Eta.thy "!s t i. s -e> t --> u[s/i] -e>> u[t/i]";
   1.227 +by(db.induct_tac "u" 1);
   1.228 +by(ALLGOALS(asm_simp_tac (addsplit (!simpset))));
   1.229 +by(fast_tac (eta_cs addIs [r_into_rtrancl]) 1);
   1.230 +by(fast_tac (eta_cs addIs [rtrancl_eta_App]) 1);
   1.231 +by(fast_tac (eta_cs addSIs [rtrancl_eta_Fun,eta_lift]) 1);
   1.232 +bind_thm("rtrancl_eta_subst", result() RS spec RS spec RS spec RS mp);
   1.233 +
   1.234 +goalw Eta.thy [square_def] "square beta eta (eta^*) (beta^=)";
   1.235 +br beta.mutual_induct 1;
   1.236 +by(strip_tac 1);
   1.237 +bes eta_cases 1;
   1.238 +bes eta_cases 1;
   1.239 +by(fast_tac (eta_cs addss (!simpset addsimps [subst_decr])) 1);
   1.240 +by(fast_tac (eta_cs addIs [r_into_rtrancl,eta_subst]) 1);
   1.241 +by(fast_tac (eta_cs addIs [rtrancl_eta_subst]) 1);
   1.242 +by(fast_tac (eta_cs addIs [r_into_rtrancl,rtrancl_eta_AppL]) 1);
   1.243 +by(fast_tac (eta_cs addIs [r_into_rtrancl,rtrancl_eta_AppR]) 1);
   1.244 +by(fast_tac (eta_cs addIs [r_into_rtrancl,rtrancl_eta_Fun,free_beta,beta_decr]
   1.245 +                  addss (!simpset addsimps[subst_decr,symmetric decr_def])) 1);
   1.246 +qed "square_beta_eta";
   1.247 +
   1.248 +goal Eta.thy "confluent(beta Un eta)";
   1.249 +by(REPEAT(ares_tac [square_rtrancl_reflcl_commute,confluent_Un,
   1.250 +                    beta_confluent,eta_confluent,square_beta_eta] 1));
   1.251 +qed "confluent_beta_eta";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Lambda/Eta.thy	Fri Oct 06 10:45:11 1995 +0100
     2.3 @@ -0,0 +1,36 @@
     2.4 +(*  Title:      HOL/Lambda/Eta.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Tobias Nipkow
     2.7 +    Copyright   1995 TU Muenchen
     2.8 +
     2.9 +Eta-reduction and relatives.
    2.10 +*)
    2.11 +
    2.12 +Eta = ParRed + Commutation +
    2.13 +consts free :: "db => nat => bool"
    2.14 +       decr :: "[db,nat] => db"
    2.15 +       eta  :: "(db * db) set"
    2.16 +
    2.17 +syntax  "-e>", "-e>>", "-e>=" , "->=" :: "[db,db] => bool" (infixl 50)
    2.18 +
    2.19 +translations
    2.20 +  "s -e>  t" == "(s,t) : eta"
    2.21 +  "s -e>> t" == "(s,t) : eta^*"
    2.22 +  "s -e>= t" == "(s,t) : eta^="
    2.23 +  "s ->=  t" == "(s,t) : beta^="
    2.24 +
    2.25 +primrec free Lambda.db
    2.26 +  free_Var "free (Var j) i = (j=i)"
    2.27 +  free_App "free (s @ t) i = (free s i | free t i)"
    2.28 +  free_Fun "free (Fun s) i = free s (Suc i)"
    2.29 +
    2.30 +defs
    2.31 +  decr_def "decr t i == t[Var i/i]"
    2.32 +
    2.33 +inductive "eta"
    2.34 +intrs
    2.35 +   eta  "~free s 0 ==> Fun(s @ Var 0) -e> decr s 0"
    2.36 +   appL  "s -e> t ==> s@u -e> t@u"
    2.37 +   appR  "s -e> t ==> u@s -e> u@t"
    2.38 +   abs   "s -e> t ==> Fun s -e> Fun t"
    2.39 +end
     3.1 --- a/src/HOL/Lambda/Lambda.ML	Thu Oct 05 14:45:54 1995 +0100
     3.2 +++ b/src/HOL/Lambda/Lambda.ML	Fri Oct 06 10:45:11 1995 +0100
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:      HOL/Lambda.thy
     3.5 +(*  Title:      HOL/Lambda/Lambda.ML
     3.6      ID:         $Id$
     3.7      Author:     Tobias Nipkow
     3.8      Copyright   1995 TU Muenchen
     3.9 @@ -7,7 +7,6 @@
    3.10  are ported from Ole Rasmussen's ZF development.  In ZF, m<=n is syntactic
    3.11  sugar for m<Suc(n). In HOL <= is a separate operator. Hence we have to prove
    3.12  some compatibility lemmas.
    3.13 -
    3.14  *)
    3.15  
    3.16  (*** Nat ***)
    3.17 @@ -52,7 +51,8 @@
    3.18  
    3.19  open Lambda;
    3.20  
    3.21 -Addsimps [if_not_P, not_less_eq];
    3.22 +Delsimps [less_Suc_eq, subst_Var];
    3.23 +Addsimps ([if_not_P, not_less_eq] @ beta.intrs);
    3.24  
    3.25  val lambda_cs = HOL_cs addSIs beta.intrs;
    3.26  
    3.27 @@ -80,50 +80,48 @@
    3.28  
    3.29  (*** subst and lift ***)
    3.30  
    3.31 -val split_ss = !simpset delsimps [less_Suc_eq,subst_Var]
    3.32 -                        addsimps [subst_Var]
    3.33 -                        setloop (split_tac [expand_if]);
    3.34 +fun addsplit ss = ss addsimps [subst_Var] setloop (split_tac [expand_if]);
    3.35  
    3.36  goal Lambda.thy "(Var k)[u/k] = u";
    3.37 -by (asm_full_simp_tac split_ss 1);
    3.38 +by (asm_full_simp_tac(addsplit(!simpset)) 1);
    3.39  qed "subst_eq";
    3.40  
    3.41  goal Lambda.thy "!!s. i<j ==> (Var j)[u/i] = Var(pred j)";
    3.42 -by (asm_full_simp_tac split_ss 1);
    3.43 +by (asm_full_simp_tac(addsplit(!simpset)) 1);
    3.44  qed "subst_gt";
    3.45  
    3.46  goal Lambda.thy "!!s. j<i ==> (Var j)[u/i] = Var(j)";
    3.47 -by (asm_full_simp_tac (split_ss addsimps
    3.48 +by (asm_full_simp_tac (addsplit(!simpset) addsimps
    3.49                            [less_not_refl2 RS not_sym,less_SucI]) 1);
    3.50  qed "subst_lt";
    3.51  
    3.52  Addsimps [subst_eq,subst_gt,subst_lt];
    3.53 -val ss = !simpset delsimps [less_Suc_eq, subst_Var];
    3.54  
    3.55  goal Lambda.thy
    3.56    "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
    3.57  by(db.induct_tac "t" 1);
    3.58 -by(ALLGOALS (asm_simp_tac ss));
    3.59 +by(ALLGOALS Asm_simp_tac);
    3.60  by(strip_tac 1);
    3.61  by (excluded_middle_tac "nat < i" 1);
    3.62  by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2));
    3.63 -by (ALLGOALS(asm_full_simp_tac (split_ss addsimps [less_SucI])));
    3.64 +by (ALLGOALS(asm_full_simp_tac (addsplit(!simpset) addsimps [less_SucI])));
    3.65  qed"lift_lift";
    3.66  
    3.67  goal Lambda.thy "!i j s. j < Suc i --> \
    3.68  \         lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
    3.69  by(db.induct_tac "t" 1);
    3.70 -by(ALLGOALS(asm_simp_tac (ss addsimps [lift_lift])));
    3.71 +by(ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift])));
    3.72  by(strip_tac 1);
    3.73  by (excluded_middle_tac "nat < j" 1);
    3.74 -by (asm_full_simp_tac ss 1);
    3.75 +by (Asm_full_simp_tac 1);
    3.76  by (eres_inst_tac [("j","nat")] leqE 1);
    3.77 -by (asm_full_simp_tac (split_ss addsimps [less_SucI,gt_pred,Suc_pred]) 1);
    3.78 +by (asm_full_simp_tac (addsplit(!simpset)
    3.79 +                       addsimps [less_SucI,gt_pred,Suc_pred]) 1);
    3.80  by (hyp_subst_tac 1);
    3.81  by (Asm_simp_tac 1);
    3.82  by (forw_inst_tac [("j","j")] lt_trans2 1);
    3.83  by (assume_tac 1);
    3.84 -by (asm_full_simp_tac (split_ss addsimps [less_SucI]) 1);
    3.85 +by (asm_full_simp_tac (addsplit(!simpset) addsimps [less_SucI]) 1);
    3.86  qed "lift_subst";
    3.87  Addsimps [lift_subst];
    3.88  
    3.89 @@ -131,15 +129,16 @@
    3.90    "!i j s. i < Suc j -->\
    3.91  \         lift (t[s/j]) i = (lift t i) [lift s i / Suc j]";
    3.92  by(db.induct_tac "t" 1);
    3.93 -by(ALLGOALS(asm_simp_tac (ss addsimps [lift_lift])));
    3.94 +by(ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift])));
    3.95  by(strip_tac 1);
    3.96  by (excluded_middle_tac "nat < j" 1);
    3.97 -by (asm_full_simp_tac ss 1);
    3.98 +by (Asm_full_simp_tac 1);
    3.99  by (eres_inst_tac [("i","j")] leqE 1);
   3.100  by (forward_tac  [lt_trans1] 1 THEN assume_tac 1);
   3.101 -by (ALLGOALS(asm_full_simp_tac (ss addsimps [Suc_pred,less_SucI,gt_pred])));
   3.102 +by (ALLGOALS(asm_full_simp_tac
   3.103 +               (!simpset addsimps [Suc_pred,less_SucI,gt_pred])));
   3.104  by (hyp_subst_tac 1);
   3.105 -by (asm_full_simp_tac (ss addsimps [less_SucI]) 1);
   3.106 +by (asm_full_simp_tac (!simpset addsimps [less_SucI]) 1);
   3.107  by(split_tac [expand_if] 1);
   3.108  by (asm_full_simp_tac (!simpset addsimps [less_SucI]) 1);
   3.109  qed "lift_subst_lt";
   3.110 @@ -156,22 +155,21 @@
   3.111  goal Lambda.thy "!i j u v. i < Suc j --> \
   3.112  \ t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]";
   3.113  by(db.induct_tac "t" 1);
   3.114 -by (ALLGOALS(asm_simp_tac (ss addsimps
   3.115 +by (ALLGOALS(asm_simp_tac (!simpset addsimps
   3.116                     [lift_lift RS spec RS spec RS mp RS sym,lift_subst_lt])));
   3.117  by(strip_tac 1);
   3.118  by (excluded_middle_tac "nat < Suc(Suc j)" 1);
   3.119 -by(asm_full_simp_tac ss 1);
   3.120 +by(Asm_full_simp_tac 1);
   3.121  by (forward_tac [lessI RS less_trans] 1);
   3.122  by (eresolve_tac [leqE] 1);
   3.123 -by (asm_simp_tac (ss addsimps [Suc_pred,lt_pred]) 2);
   3.124 +by (asm_simp_tac (!simpset addsimps [Suc_pred,lt_pred]) 2);
   3.125  by (forward_tac [Suc_mono RS less_trans] 1 THEN assume_tac 1);
   3.126  by (forw_inst_tac [("i","i")] (lessI RS less_trans) 1);
   3.127 -by (asm_simp_tac (ss addsimps [Suc_pred,lt_pred]) 1);
   3.128 +by (asm_simp_tac (!simpset addsimps [Suc_pred,lt_pred]) 1);
   3.129  by (eres_inst_tac [("i","nat")] leqE 1);
   3.130 -by (asm_full_simp_tac (!simpset delsimps [less_Suc_eq]
   3.131 -                                addsimps [Suc_pred,less_SucI]) 2);
   3.132 +by (asm_full_simp_tac (!simpset addsimps [Suc_pred,less_SucI]) 2);
   3.133  by (excluded_middle_tac "nat < i" 1);
   3.134 -by (asm_full_simp_tac ss 1);
   3.135 +by (Asm_full_simp_tac 1);
   3.136  by (eres_inst_tac [("j","nat")] leqE 1);
   3.137  by (asm_simp_tac (!simpset addsimps [gt_pred]) 1);
   3.138  by (Asm_simp_tac 1);
   3.139 @@ -184,20 +182,20 @@
   3.140  
   3.141  goal Lambda.thy "!k. liftn 0 t k = t";
   3.142  by(db.induct_tac "t" 1);
   3.143 -by(ALLGOALS(asm_simp_tac split_ss));
   3.144 +by(ALLGOALS(asm_simp_tac(addsplit(!simpset))));
   3.145  qed "liftn_0";
   3.146  Addsimps [liftn_0];
   3.147  
   3.148  goal Lambda.thy "!k. liftn (Suc n) t k = lift (liftn n t k) k";
   3.149  by(db.induct_tac "t" 1);
   3.150 -by(ALLGOALS(asm_simp_tac split_ss));
   3.151 +by(ALLGOALS(asm_simp_tac(addsplit(!simpset))));
   3.152  by(fast_tac (HOL_cs addDs [add_lessD1]) 1);
   3.153  qed "liftn_lift";
   3.154  Addsimps [liftn_lift];
   3.155  
   3.156  goal Lambda.thy "!n. substn t s n = t[liftn n s 0 / n]";
   3.157  by(db.induct_tac "t" 1);
   3.158 -by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   3.159 +by(ALLGOALS(asm_simp_tac(addsplit(!simpset))));
   3.160  qed "substn_subst_n";
   3.161  Addsimps [substn_subst_n];
   3.162  
     4.1 --- a/src/HOL/Lambda/Lambda.thy	Thu Oct 05 14:45:54 1995 +0100
     4.2 +++ b/src/HOL/Lambda/Lambda.thy	Fri Oct 06 10:45:11 1995 +0100
     4.3 @@ -1,4 +1,4 @@
     4.4 -(*  Title:      HOL/Lambda.thy
     4.5 +(*  Title:      HOL/Lambda/Lambda.thy
     4.6      ID:         $Id$
     4.7      Author:     Tobias Nipkow
     4.8      Copyright   1995 TU Muenchen
     5.1 --- a/src/HOL/Lambda/ParRed.ML	Thu Oct 05 14:45:54 1995 +0100
     5.2 +++ b/src/HOL/Lambda/ParRed.ML	Fri Oct 06 10:45:11 1995 +0100
     5.3 @@ -59,7 +59,7 @@
     5.4  goal ParRed.thy
     5.5    "!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]";
     5.6  by(db.induct_tac "t" 1);
     5.7 -  by(asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
     5.8 +  by(asm_simp_tac (addsplit(!simpset)) 1);
     5.9   by(strip_tac 1);
    5.10   bes par_beta_cases 1;
    5.11    by(Asm_simp_tac 1);
    5.12 @@ -72,7 +72,7 @@
    5.13  
    5.14  (*** Confluence (directly) ***)
    5.15  
    5.16 -goalw ParRed.thy [diamond_def] "diamond(par_beta)";
    5.17 +goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
    5.18  by(REPEAT(rtac allI 1));
    5.19  br impI 1;
    5.20  be (par_beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1;
    5.21 @@ -82,20 +82,6 @@
    5.22  
    5.23  (*** cd ***)
    5.24  
    5.25 -goal ParRed.thy "cd(Var n @ t) = Var n @ cd t";
    5.26 -by(Simp_tac 1);
    5.27 -qed"cd_App_Var";
    5.28 -
    5.29 -goal ParRed.thy "cd((r @ s) @ t) = cd(r @ s) @ cd t";
    5.30 -by(Simp_tac 1);
    5.31 -qed"cd_App_App";
    5.32 -
    5.33 -goal ParRed.thy "cd((Fun s) @ t) = (cd s)[cd t/0]";
    5.34 -by(Simp_tac 1);
    5.35 -qed"cd_App_Fun";
    5.36 -
    5.37 -Addsimps [cd_App_Var,cd_App_App,cd_App_Fun];
    5.38 -
    5.39  goal ParRed.thy "!t. s => t --> t => cd s";
    5.40  by(db.induct_tac "s" 1);
    5.41    by(Simp_tac 1);
    5.42 @@ -106,7 +92,7 @@
    5.43  
    5.44  (*** Confluence (via cd) ***)
    5.45  
    5.46 -goalw ParRed.thy [diamond_def] "diamond(par_beta)";
    5.47 +goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
    5.48  by(fast_tac (HOL_cs addIs [par_beta_cd]) 1);
    5.49  qed "diamond_par_beta2";
    5.50  
     6.1 --- a/src/HOL/Lambda/ParRed.thy	Thu Oct 05 14:45:54 1995 +0100
     6.2 +++ b/src/HOL/Lambda/ParRed.thy	Fri Oct 06 10:45:11 1995 +0100
     6.3 @@ -6,7 +6,7 @@
     6.4  Parallel reduction and a complete developments function "cd".
     6.5  *)
     6.6  
     6.7 -ParRed = Lambda + Confluence +
     6.8 +ParRed = Lambda + Commutation +
     6.9  
    6.10  consts  par_beta :: "(db * db) set"
    6.11  
     7.1 --- a/src/HOL/Lambda/ROOT.ML	Thu Oct 05 14:45:54 1995 +0100
     7.2 +++ b/src/HOL/Lambda/ROOT.ML	Fri Oct 06 10:45:11 1995 +0100
     7.3 @@ -1,10 +1,13 @@
     7.4 -(*  Title: 	HOL/IMP/ROOT.ML
     7.5 +(*  Title: 	HOL/Lambda/ROOT.ML
     7.6      ID:         $Id$
     7.7      Author: 	Tobias Nipkow
     7.8      Copyright   1995 TUM
     7.9  
    7.10  Confluence proof for untyped lambda-calculus using de Bruijn's notation.
    7.11 -Extremely slick proof; follows the first two pages of
    7.12 +Covers beta, eta, and beta+eta.
    7.13 +
    7.14 +Beta is proved confluent both in the traditional way and also following the
    7.15 +first two pages of
    7.16  
    7.17  @article{Takahashi-IC-95,author="Masako Takahashi",
    7.18  title="Parallel Reductions in $\lambda$-Calculus",
    7.19 @@ -16,4 +19,4 @@
    7.20  
    7.21  writeln"Root file for HOL/Lambda";
    7.22  loadpath := [".","Lambda"];
    7.23 -time_use_thy "ParRed";
    7.24 +time_use_thy "Eta";