Used nat_trans_tac. New Eta. various smaller changes.
authornipkow
Mon Nov 04 17:23:37 1996 +0100 (1996-11-04)
changeset 2159e650a3f6f600
parent 2158 77dfe65b5bb3
child 2160 ad4382e546fc
Used nat_trans_tac. New Eta. various smaller changes.
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
     1.1 --- a/src/HOL/Lambda/Eta.ML	Mon Nov 04 10:56:15 1996 +0100
     1.2 +++ b/src/HOL/Lambda/Eta.ML	Mon Nov 04 17:23:37 1996 +0100
     1.3 @@ -13,20 +13,28 @@
     1.4  
     1.5  Addsimps eta.intrs;
     1.6  
     1.7 -val eta_cases = map (eta.mk_cases db.simps)
     1.8 -    ["Fun s -e> z","s @ t -e> u","Var i -e> t"];
     1.9 +val eta_cases = map (eta.mk_cases dB.simps)
    1.10 +    ["Abs s -e> z","s @ t -e> u","Var i -e> t"];
    1.11  
    1.12 -val beta_cases = map (beta.mk_cases db.simps)
    1.13 +val beta_cases = map (beta.mk_cases dB.simps)
    1.14      ["s @ t -> u","Var i -> t"];
    1.15  
    1.16  AddIs eta.intrs;
    1.17  AddSEs (beta_cases@eta_cases);
    1.18  
    1.19 -section "decr and free";
    1.20 +section "eta, subst and free";
    1.21 +
    1.22 +goal Eta.thy "!i t u. ~free s i --> s[t/i] = s[u/i]";
    1.23 +by (dB.induct_tac "s" 1);
    1.24 +by (ALLGOALS(simp_tac (addsplit (!simpset))));
    1.25 +by (fast_tac HOL_cs 1);
    1.26 +by (fast_tac HOL_cs 1);
    1.27 +qed_spec_mp "subst_not_free";
    1.28 +Addsimps [subst_not_free RS eqTrueI];
    1.29  
    1.30  goal Eta.thy "!i k. free (lift t k) i = \
    1.31  \                   (i < k & free t i | k < i & free t (pred i))";
    1.32 -by (db.induct_tac "t" 1);
    1.33 +by (dB.induct_tac "t" 1);
    1.34  by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addcongs [conj_cong])));
    1.35  by (fast_tac HOL_cs 2);
    1.36  by(simp_tac (!simpset addsimps [pred_def]
    1.37 @@ -38,7 +46,7 @@
    1.38  
    1.39  goal Eta.thy "!i k t. free (s[t/k]) i = \
    1.40  \              (free s k & free t i | free s (if i<k then i else Suc i))";
    1.41 -by (db.induct_tac "s" 1);
    1.42 +by (dB.induct_tac "s" 1);
    1.43  by (Asm_simp_tac 2);
    1.44  by (Fast_tac 2);
    1.45  by (asm_full_simp_tac (addsplit (!simpset)) 2);
    1.46 @@ -51,59 +59,43 @@
    1.47  
    1.48  goal Eta.thy "!!s. s -e> t ==> !i. free t i = free s i";
    1.49  by (etac eta.induct 1);
    1.50 -by (ALLGOALS(asm_simp_tac (!simpset addsimps [decr_def] addcongs [conj_cong])));
    1.51 +by (ALLGOALS(asm_simp_tac (!simpset addcongs [conj_cong])));
    1.52  qed_spec_mp "free_eta";
    1.53  
    1.54  goal Eta.thy "!!s. [| s -e> t; ~free s i |] ==> ~free t i";
    1.55  by (asm_simp_tac (!simpset addsimps [free_eta]) 1);
    1.56  qed "not_free_eta";
    1.57  
    1.58 -goal Eta.thy "!i t u. ~free s i --> s[t/i] = s[u/i]";
    1.59 -by (db.induct_tac "s" 1);
    1.60 -by (ALLGOALS(simp_tac (addsplit (!simpset))));
    1.61 -by (fast_tac HOL_cs 1);
    1.62 -by (fast_tac HOL_cs 1);
    1.63 -qed_spec_mp "subst_not_free";
    1.64 -
    1.65 -goalw Eta.thy [decr_def] "!!s. ~free s i ==> s[t/i] = decr s i";
    1.66 -by (etac subst_not_free 1);
    1.67 -qed "subst_decr";
    1.68 -
    1.69  goal Eta.thy "!!s. s -e> t ==> !u i. s[u/i] -e> t[u/i]";
    1.70  by (etac eta.induct 1);
    1.71 -by (ALLGOALS(asm_simp_tac (!simpset addsimps [subst_subst RS sym,decr_def])));
    1.72 -by (asm_simp_tac (!simpset addsimps [subst_decr]) 1);
    1.73 +by (ALLGOALS(asm_simp_tac (!simpset addsimps [subst_subst RS sym])));
    1.74  qed_spec_mp "eta_subst";
    1.75  Addsimps [eta_subst];
    1.76  
    1.77 -goalw Eta.thy [decr_def] "!!s. s -e> t ==> decr s i -e> decr t i";
    1.78 -by (etac eta_subst 1);
    1.79 -qed "eta_decr";
    1.80 -
    1.81  section "Confluence of -e>";
    1.82  
    1.83  goalw Eta.thy [square_def,id_def]  "square eta eta (eta^=) (eta^=)";
    1.84  by (rtac (impI RS allI RS allI) 1);
    1.85  by (Simp_tac 1);
    1.86  by (etac eta.induct 1);
    1.87 -by (best_tac (!claset addSIs [eta_decr]
    1.88 +by (slow_tac (!claset addIs [subst_not_free,eta_subst]
    1.89                        addIs [free_eta RS iffD1] addss !simpset) 1);
    1.90  by (slow_tac (!claset) 1);
    1.91  by (slow_tac (!claset) 1);
    1.92 -by (slow_tac (!claset addSIs [eta_decr]
    1.93 -                     addIs [free_eta RS iffD1]) 1);
    1.94 -val lemma = result();
    1.95 +by (slow_tac (!claset addSIs [eta_subst]
    1.96 +                           addIs [free_eta RS iffD1]) 1);
    1.97 +qed "square_eta";
    1.98  
    1.99  goal Eta.thy "confluent(eta)";
   1.100 -by (rtac (lemma RS square_reflcl_confluent) 1);
   1.101 +by (rtac (square_eta RS square_reflcl_confluent) 1);
   1.102  qed "eta_confluent";
   1.103  
   1.104  section "Congruence rules for -e>>";
   1.105  
   1.106 -goal Eta.thy "!!s. s -e>> s' ==> Fun s -e>> Fun s'";
   1.107 +goal Eta.thy "!!s. s -e>> s' ==> Abs s -e>> Abs s'";
   1.108  by (etac rtrancl_induct 1);
   1.109  by (ALLGOALS(fast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl])));
   1.110 -qed "rtrancl_eta_Fun";
   1.111 +qed "rtrancl_eta_Abs";
   1.112  
   1.113  goal Eta.thy "!!s. s -e>> s' ==> s @ t -e>> s' @ t";
   1.114  by (etac rtrancl_induct 1);
   1.115 @@ -127,62 +119,43 @@
   1.116  by (ALLGOALS(Asm_full_simp_tac));
   1.117  qed_spec_mp "free_beta";
   1.118  
   1.119 -goalw Eta.thy [decr_def] "!!s t. s -> t ==> (!i. decr s i -> decr t i)";
   1.120 +goal Eta.thy "!!s t. s -> t ==> !u i. s[u/i] -> t[u/i]";
   1.121  by (etac beta.induct 1);
   1.122  by (ALLGOALS(asm_full_simp_tac (!simpset addsimps [subst_subst RS sym])));
   1.123 -qed_spec_mp "beta_decr";
   1.124 -
   1.125 -goalw Eta.thy [decr_def]
   1.126 -  "decr (Var i) k = (if i<=k then Var i else Var(pred i))";
   1.127 -by (simp_tac (addsplit (!simpset) addsimps [le_def]) 1);
   1.128 -qed "decr_Var";
   1.129 -Addsimps [decr_Var];
   1.130 +qed_spec_mp "beta_subst";
   1.131 +AddIs [beta_subst];
   1.132  
   1.133 -goalw Eta.thy [decr_def] "decr (s@t) i = (decr s i)@(decr t i)";
   1.134 -by (Simp_tac 1);
   1.135 -qed "decr_App";
   1.136 -Addsimps [decr_App];
   1.137 -
   1.138 -goalw Eta.thy [decr_def] "decr (Fun s) i = Fun (decr s (Suc i))";
   1.139 -by (Simp_tac 1);
   1.140 -qed "decr_Fun";
   1.141 -Addsimps [decr_Fun];
   1.142 -
   1.143 -goal Eta.thy "!i. ~free t (Suc i) --> decr t (Suc i) = decr t i";
   1.144 -by (db.induct_tac "t" 1);
   1.145 -by (ALLGOALS
   1.146 -    (asm_simp_tac (addsplit (!simpset) addsimps [le_def, less_Suc_eq])));
   1.147 -qed_spec_mp "decr_not_free";
   1.148 -Addsimps [decr_not_free];
   1.149 +goal Eta.thy "!i. t[Var i/i] = t[Var(i)/Suc i]";
   1.150 +by (dB.induct_tac "t" 1);
   1.151 +by (ALLGOALS (asm_simp_tac (addsplit (!simpset))));
   1.152 +by(safe_tac (HOL_cs addSEs [nat_neqE]));
   1.153 +by(ALLGOALS trans_tac);
   1.154 +qed_spec_mp "subst_Var_Suc";
   1.155 +Addsimps [subst_Var_Suc];
   1.156  
   1.157  goal Eta.thy "!!s t. s -e> t ==> (!i. lift s i -e> lift t i)";
   1.158  by (etac eta.induct 1);
   1.159 -by (ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [decr_def])));
   1.160 -by (asm_simp_tac (!simpset addsimps [subst_decr]) 1);
   1.161 +by (ALLGOALS(asm_simp_tac (addsplit (!simpset))));
   1.162  qed_spec_mp "eta_lift";
   1.163  Addsimps [eta_lift];
   1.164  
   1.165  goal Eta.thy "!s t i. s -e> t --> u[s/i] -e>> u[t/i]";
   1.166 -by (db.induct_tac "u" 1);
   1.167 +by (dB.induct_tac "u" 1);
   1.168  by (ALLGOALS(asm_simp_tac (addsplit (!simpset))));
   1.169  by (fast_tac (!claset addIs [r_into_rtrancl]) 1);
   1.170  by (fast_tac (!claset addSIs [rtrancl_eta_App]) 1);
   1.171 -by (fast_tac (!claset addSIs [rtrancl_eta_Fun,eta_lift]) 1);
   1.172 +by (fast_tac (!claset addSIs [rtrancl_eta_Abs,eta_lift]) 1);
   1.173  qed_spec_mp "rtrancl_eta_subst";
   1.174  
   1.175  goalw Eta.thy [square_def] "square beta eta (eta^*) (beta^=)";
   1.176  by (rtac (impI RS allI RS allI) 1);
   1.177  by (etac beta.induct 1);
   1.178 -by (strip_tac 1);
   1.179 -by (eresolve_tac eta_cases 1);
   1.180 -by (eresolve_tac eta_cases 1);
   1.181 -by (fast_tac (!claset addss (!simpset addsimps [subst_decr])) 1);
   1.182 -by (slow_tac (!claset addIs [r_into_rtrancl,eta_subst]) 1);
   1.183 -by (slow_tac (!claset addIs [rtrancl_eta_subst]) 1);
   1.184 +by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_subst,eta_subst]
   1.185 +                      addss !simpset) 1);
   1.186  by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppL]) 1);
   1.187  by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppR]) 1);
   1.188 -by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_Fun,free_beta,beta_decr]
   1.189 -                  addss (!simpset addsimps[subst_decr,symmetric decr_def])) 1);
   1.190 +by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_Abs,free_beta]
   1.191 +                      addss !simpset) 1);
   1.192  qed "square_beta_eta";
   1.193  
   1.194  goal Eta.thy "confluent(beta Un eta)";
   1.195 @@ -190,23 +163,21 @@
   1.196                      beta_confluent,eta_confluent,square_beta_eta] 1));
   1.197  qed "confluent_beta_eta";
   1.198  
   1.199 -
   1.200 -section "Implicit definition of -e>: Fun(lift s 0 @ Var 0) -e> s";
   1.201 +section "Implicit definition of -e>: Abs(lift s 0 @ Var 0) -e> s";
   1.202  
   1.203  goal Eta.thy "!i. (~free s i) = (? t. s = lift t i)";
   1.204 -by (db.induct_tac "s" 1);
   1.205 +by (dB.induct_tac "s" 1);
   1.206    by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   1.207    by (SELECT_GOAL(safe_tac HOL_cs)1);
   1.208 -   by (res_inst_tac [("m","nat"),("n","i")] nat_less_cases 1);
   1.209 -     by (res_inst_tac [("x","Var nat")] exI 1);
   1.210 -     by (Asm_simp_tac 1);
   1.211 -    by (fast_tac HOL_cs 1);
   1.212 +   by(etac nat_neqE 1);
   1.213 +    by (res_inst_tac [("x","Var nat")] exI 1);
   1.214 +    by (Asm_simp_tac 1);
   1.215     by (res_inst_tac [("x","Var(pred nat)")] exI 1);
   1.216     by (Asm_simp_tac 1);
   1.217    by (rtac notE 1);
   1.218     by (assume_tac 2);
   1.219    by (etac thin_rl 1);
   1.220 -  by (res_inst_tac [("db","t")] db_case_distinction 1);
   1.221 +  by (res_inst_tac [("dB","t")] dB_case_distinction 1);
   1.222      by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   1.223      by (fast_tac (HOL_cs addDs [less_not_refl2]) 1);
   1.224     by (Simp_tac 1);
   1.225 @@ -222,7 +193,7 @@
   1.226    by (Asm_simp_tac 1);
   1.227   by (etac exE 1);
   1.228   by (etac rev_mp 1);
   1.229 - by (res_inst_tac [("db","t")] db_case_distinction 1);
   1.230 + by (res_inst_tac [("dB","t")] dB_case_distinction 1);
   1.231     by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   1.232    by (Simp_tac 1);
   1.233    by (fast_tac HOL_cs 1);
   1.234 @@ -232,19 +203,18 @@
   1.235  by (rtac allI 1);
   1.236  by (rtac iffI 1);
   1.237   by (etac exE 1);
   1.238 - by (res_inst_tac [("x","Fun t")] exI 1);
   1.239 + by (res_inst_tac [("x","Abs t")] exI 1);
   1.240   by (Asm_simp_tac 1);
   1.241  by (etac exE 1);
   1.242  by (etac rev_mp 1);
   1.243 -by (res_inst_tac [("db","t")] db_case_distinction 1);
   1.244 +by (res_inst_tac [("dB","t")] dB_case_distinction 1);
   1.245    by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   1.246   by (Simp_tac 1);
   1.247  by (Simp_tac 1);
   1.248  by (fast_tac HOL_cs 1);
   1.249  qed_spec_mp "not_free_iff_lifted";
   1.250  
   1.251 -goalw Eta.thy [decr_def]
   1.252 - "(!s. (~free s 0) --> R(Fun(s @ Var 0))(decr s 0)) = \
   1.253 -\ (!s. R(Fun(lift s 0 @ Var 0))(s))";
   1.254 -by (fast_tac (HOL_cs addss (!simpset addsimps [lemma,not_free_iff_lifted])) 1);
   1.255 +goal Eta.thy "(!s u. (~free s 0) --> R(Abs(s @ Var 0))(s[u/0])) = \
   1.256 +\             (!s. R(Abs(lift s 0 @ Var 0))(s))";
   1.257 +by (fast_tac (HOL_cs addss (!simpset addsimps [not_free_iff_lifted])) 1);
   1.258  qed "explicit_is_implicit";
     2.1 --- a/src/HOL/Lambda/Eta.thy	Mon Nov 04 10:56:15 1996 +0100
     2.2 +++ b/src/HOL/Lambda/Eta.thy	Mon Nov 04 17:23:37 1996 +0100
     2.3 @@ -7,11 +7,11 @@
     2.4  *)
     2.5  
     2.6  Eta = ParRed + Commutation +
     2.7 -consts free :: db => nat => bool
     2.8 -       decr :: [db,nat] => db
     2.9 -       eta  :: "(db * db) set"
    2.10 +consts free :: dB => nat => bool
    2.11 +       decr :: dB => dB
    2.12 +       eta  :: "(dB * dB) set"
    2.13  
    2.14 -syntax  "-e>", "-e>>", "-e>=" , "->=" :: [db,db] => bool (infixl 50)
    2.15 +syntax  "-e>", "-e>>", "-e>=" , "->=" :: [dB,dB] => bool (infixl 50)
    2.16  
    2.17  translations
    2.18    "s -e>  t" == "(s,t) : eta"
    2.19 @@ -19,19 +19,16 @@
    2.20    "s -e>= t" == "(s,t) : eta^="
    2.21    "s ->=  t" == "(s,t) : beta^="
    2.22  
    2.23 -primrec free Lambda.db
    2.24 +primrec free Lambda.dB
    2.25    "free (Var j) i = (j=i)"
    2.26    "free (s @ t) i = (free s i | free t i)"
    2.27 -  "free (Fun s) i = free s (Suc i)"
    2.28 -
    2.29 -defs
    2.30 -  decr_def "decr t i == t[Var i/i]"
    2.31 +  "free (Abs s) i = free s (Suc 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 +   eta  "~free s 0 ==> Abs(s @ Var 0) -e> s[dummy/0]"
    2.37     appL  "s -e> t ==> s@u -e> t@u"
    2.38     appR  "s -e> t ==> u@s -e> u@t"
    2.39 -   abs   "s -e> t ==> Fun s -e> Fun t"
    2.40 +   abs   "s -e> t ==> Abs s -e> Abs t"
    2.41  end
    2.42  
     3.1 --- a/src/HOL/Lambda/Lambda.ML	Mon Nov 04 10:56:15 1996 +0100
     3.2 +++ b/src/HOL/Lambda/Lambda.ML	Mon Nov 04 17:23:37 1996 +0100
     3.3 @@ -16,16 +16,16 @@
     3.4  (* don't add r_into_rtrancl! *)
     3.5  AddSIs beta.intrs;
     3.6  
     3.7 -val db_case_distinction =
     3.8 -  rule_by_tactic(EVERY[etac thin_rl 2,etac thin_rl 2,etac thin_rl 3])db.induct;
     3.9 +val dB_case_distinction =
    3.10 +  rule_by_tactic(EVERY[etac thin_rl 2,etac thin_rl 2,etac thin_rl 3])dB.induct;
    3.11  
    3.12  (*** Congruence rules for ->> ***)
    3.13  
    3.14 -goal Lambda.thy "!!s. s ->> s' ==> Fun s ->> Fun s'";
    3.15 +goal Lambda.thy "!!s. s ->> s' ==> Abs s ->> Abs s'";
    3.16  by (etac rtrancl_induct 1);
    3.17  by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl])));
    3.18 -qed "rtrancl_beta_Fun";
    3.19 -AddSIs [rtrancl_beta_Fun];
    3.20 +qed "rtrancl_beta_Abs";
    3.21 +AddSIs [rtrancl_beta_Abs];
    3.22  
    3.23  goal Lambda.thy "!!s. s ->> s' ==> s @ t ->> s' @ t";
    3.24  by (etac rtrancl_induct 1);
    3.25 @@ -64,7 +64,7 @@
    3.26  
    3.27  goal Lambda.thy
    3.28    "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
    3.29 -by (db.induct_tac "t" 1);
    3.30 +by (dB.induct_tac "t" 1);
    3.31  by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])
    3.32                                      addsolver (cut_trans_tac))));
    3.33  by (safe_tac HOL_cs);
    3.34 @@ -73,7 +73,7 @@
    3.35  
    3.36  goal Lambda.thy "!i j s. j < Suc i --> \
    3.37  \         lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
    3.38 -by (db.induct_tac "t" 1);
    3.39 +by (dB.induct_tac "t" 1);
    3.40  by (ALLGOALS(asm_simp_tac (!simpset addsimps [pred_def,subst_Var,lift_lift]
    3.41                                  setloop (split_tac [expand_if,expand_nat_case])
    3.42                                  addsolver (cut_trans_tac))));
    3.43 @@ -85,7 +85,7 @@
    3.44  goal Lambda.thy
    3.45    "!i j s. i < Suc j -->\
    3.46  \         lift (t[s/j]) i = (lift t i) [lift s i / Suc j]";
    3.47 -by (db.induct_tac "t" 1);
    3.48 +by (dB.induct_tac "t" 1);
    3.49  by (ALLGOALS(asm_simp_tac (!simpset addsimps [subst_Var,lift_lift]
    3.50                                  setloop (split_tac [expand_if])
    3.51                                  addsolver (cut_trans_tac))));
    3.52 @@ -94,7 +94,7 @@
    3.53  qed "lift_subst_lt";
    3.54  
    3.55  goal Lambda.thy "!k s. (lift t k)[s/k] = t";
    3.56 -by (db.induct_tac "t" 1);
    3.57 +by (dB.induct_tac "t" 1);
    3.58  by (ALLGOALS (asm_full_simp_tac (!simpset setloop (split_tac[expand_if]))));
    3.59  qed "subst_lift";
    3.60  Addsimps [subst_lift];
    3.61 @@ -102,7 +102,7 @@
    3.62  
    3.63  goal Lambda.thy "!i j u v. i < Suc j --> \
    3.64  \ t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]";
    3.65 -by (db.induct_tac "t" 1);
    3.66 +by (dB.induct_tac "t" 1);
    3.67  by (ALLGOALS(asm_simp_tac
    3.68        (!simpset addsimps [pred_def,subst_Var,lift_lift RS sym,lift_subst_lt]
    3.69                  setloop (split_tac [expand_if,expand_nat_case])
    3.70 @@ -115,20 +115,20 @@
    3.71  (*** Equivalence proof for optimized substitution ***)
    3.72  
    3.73  goal Lambda.thy "!k. liftn 0 t k = t";
    3.74 -by (db.induct_tac "t" 1);
    3.75 +by (dB.induct_tac "t" 1);
    3.76  by (ALLGOALS(asm_simp_tac(addsplit(!simpset))));
    3.77  qed "liftn_0";
    3.78  Addsimps [liftn_0];
    3.79  
    3.80  goal Lambda.thy "!k. liftn (Suc n) t k = lift (liftn n t k) k";
    3.81 -by (db.induct_tac "t" 1);
    3.82 +by (dB.induct_tac "t" 1);
    3.83  by (ALLGOALS(asm_simp_tac(addsplit(!simpset))));
    3.84  by (fast_tac (HOL_cs addDs [add_lessD1]) 1);
    3.85  qed "liftn_lift";
    3.86  Addsimps [liftn_lift];
    3.87  
    3.88  goal Lambda.thy "!n. substn t s n = t[liftn n s 0 / n]";
    3.89 -by (db.induct_tac "t" 1);
    3.90 +by (dB.induct_tac "t" 1);
    3.91  by (ALLGOALS(asm_simp_tac(addsplit(!simpset))));
    3.92  qed "substn_subst_n";
    3.93  Addsimps [substn_subst_n];
     4.1 --- a/src/HOL/Lambda/Lambda.thy	Mon Nov 04 10:56:15 1996 +0100
     4.2 +++ b/src/HOL/Lambda/Lambda.thy	Mon Nov 04 17:23:37 1996 +0100
     4.3 @@ -9,40 +9,40 @@
     4.4  
     4.5  Lambda = Arith +
     4.6  
     4.7 -datatype db = Var nat | "@" db db (infixl 200) | Fun db
     4.8 +datatype dB = Var nat | "@" dB dB (infixl 200) | Abs dB
     4.9  
    4.10  consts
    4.11 -  subst  :: [db,db,nat]=>db ("_[_'/_]" [300,0,0] 300)
    4.12 -  lift   :: [db,nat] => db
    4.13 +  subst  :: [dB,dB,nat]=>dB ("_[_'/_]" [300,0,0] 300)
    4.14 +  lift   :: [dB,nat] => dB
    4.15    (* optimized versions *)
    4.16 -  substn :: [db,db,nat] => db
    4.17 -  liftn  :: [nat,db,nat] => db
    4.18 +  substn :: [dB,dB,nat] => dB
    4.19 +  liftn  :: [nat,dB,nat] => dB
    4.20  
    4.21 -primrec lift db
    4.22 +primrec lift dB
    4.23    "lift (Var i) k = (if i < k then Var i else Var(Suc i))"
    4.24    "lift (s @ t) k = (lift s k) @ (lift t k)"
    4.25 -  "lift (Fun s) k = Fun(lift s (Suc k))"
    4.26 +  "lift (Abs s) k = Abs(lift s (Suc k))"
    4.27  
    4.28 -primrec subst db
    4.29 +primrec subst dB
    4.30    subst_Var "(Var i)[s/k] = (if k < i then Var(pred i)
    4.31                              else if i = k then s else Var i)"
    4.32    subst_App "(t @ u)[s/k] = t[s/k] @ u[s/k]"
    4.33 -  subst_Fun "(Fun t)[s/k] = Fun (t[lift s 0 / Suc k])"
    4.34 +  subst_Abs "(Abs t)[s/k] = Abs (t[lift s 0 / Suc k])"
    4.35  
    4.36 -primrec liftn db
    4.37 +primrec liftn dB
    4.38    "liftn n (Var i) k = (if i < k then Var i else Var(i+n))"
    4.39    "liftn n (s @ t) k = (liftn n s k) @ (liftn n t k)"
    4.40 -  "liftn n (Fun s) k = Fun(liftn n s (Suc k))"
    4.41 +  "liftn n (Abs s) k = Abs(liftn n s (Suc k))"
    4.42  
    4.43 -primrec substn db
    4.44 +primrec substn dB
    4.45    "substn (Var i) s k = (if k < i then Var(pred i)
    4.46                           else if i = k then liftn k s 0 else Var i)"
    4.47    "substn (t @ u) s k = (substn t s k) @ (substn u s k)"
    4.48 -  "substn (Fun t) s k = Fun (substn t s (Suc k))"
    4.49 +  "substn (Abs t) s k = Abs (substn t s (Suc k))"
    4.50  
    4.51 -consts  beta :: "(db * db) set"
    4.52 +consts  beta :: "(dB * dB) set"
    4.53  
    4.54 -syntax  "->", "->>" :: [db,db] => bool (infixl 50)
    4.55 +syntax  "->", "->>" :: [dB,dB] => bool (infixl 50)
    4.56  
    4.57  translations
    4.58    "s -> t"  == "(s,t) : beta"
    4.59 @@ -50,8 +50,8 @@
    4.60  
    4.61  inductive beta
    4.62  intrs
    4.63 -   beta  "(Fun s) @ t -> s[t/0]"
    4.64 +   beta  "(Abs s) @ t -> s[t/0]"
    4.65     appL  "s -> t ==> s@u -> t@u"
    4.66     appR  "s -> t ==> u@s -> u@t"
    4.67 -   abs   "s -> t ==> Fun s -> Fun t"
    4.68 +   abs   "s -> t ==> Abs s -> Abs t"
    4.69  end
     5.1 --- a/src/HOL/Lambda/ParRed.ML	Mon Nov 04 10:56:15 1996 +0100
     5.2 +++ b/src/HOL/Lambda/ParRed.ML	Mon Nov 04 17:23:37 1996 +0100
     5.3 @@ -11,9 +11,9 @@
     5.4  
     5.5  Addsimps par_beta.intrs;
     5.6  
     5.7 -val par_beta_cases = map (par_beta.mk_cases db.simps)
     5.8 -    ["Var n => t", "Fun s => Fun t",
     5.9 -     "(Fun s) @ t => u", "s @ t => u", "Fun s => t"];
    5.10 +val par_beta_cases = map (par_beta.mk_cases dB.simps)
    5.11 +    ["Var n => t", "Abs s => Abs t",
    5.12 +     "(Abs s) @ t => u", "s @ t => u", "Abs s => t"];
    5.13  
    5.14  AddSIs par_beta.intrs;
    5.15  AddSEs par_beta_cases;
    5.16 @@ -26,7 +26,7 @@
    5.17  Addsimps [par_beta_varL];
    5.18  
    5.19  goal ParRed.thy "t => t";
    5.20 -by (db.induct_tac "t" 1);
    5.21 +by (dB.induct_tac "t" 1);
    5.22  by (ALLGOALS Asm_simp_tac);
    5.23  qed"par_beta_refl";
    5.24  Addsimps [par_beta_refl];
    5.25 @@ -50,14 +50,14 @@
    5.26  (*** => ***)
    5.27  
    5.28  goal ParRed.thy "!t' n. t => t' --> lift t n => lift t' n";
    5.29 -by (db.induct_tac "t" 1);
    5.30 +by (dB.induct_tac "t" 1);
    5.31  by (ALLGOALS(fast_tac (!claset addss (!simpset))));
    5.32  qed_spec_mp "par_beta_lift";
    5.33  Addsimps [par_beta_lift];
    5.34  
    5.35  goal ParRed.thy
    5.36    "!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]";
    5.37 -by (db.induct_tac "t" 1);
    5.38 +by (dB.induct_tac "t" 1);
    5.39    by (asm_simp_tac (addsplit(!simpset)) 1);
    5.40   by (strip_tac 1);
    5.41   by (eresolve_tac par_beta_cases 1);
    5.42 @@ -79,10 +79,10 @@
    5.43  (*** cd ***)
    5.44  
    5.45  goal ParRed.thy "!t. s => t --> t => cd s";
    5.46 -by (db.induct_tac "s" 1);
    5.47 +by (dB.induct_tac "s" 1);
    5.48    by (Simp_tac 1);
    5.49   by (etac rev_mp 1);
    5.50 - by (db.induct_tac "db1" 1);
    5.51 + by (dB.induct_tac "dB1" 1);
    5.52   by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] addss !simpset)));
    5.53  qed_spec_mp "par_beta_cd";
    5.54  
     6.1 --- a/src/HOL/Lambda/ParRed.thy	Mon Nov 04 10:56:15 1996 +0100
     6.2 +++ b/src/HOL/Lambda/ParRed.thy	Mon Nov 04 17:23:37 1996 +0100
     6.3 @@ -8,9 +8,9 @@
     6.4  
     6.5  ParRed = Lambda + Commutation +
     6.6  
     6.7 -consts  par_beta :: "(db * db) set"
     6.8 +consts  par_beta :: "(dB * dB) set"
     6.9  
    6.10 -syntax  "=>" :: [db,db] => bool (infixl 50)
    6.11 +syntax  "=>" :: [dB,dB] => bool (infixl 50)
    6.12  
    6.13  translations
    6.14    "s => t" == "(s,t) : par_beta"
    6.15 @@ -18,24 +18,24 @@
    6.16  inductive par_beta
    6.17    intrs
    6.18      var   "Var n => Var n"
    6.19 -    abs   "s => t ==> Fun s => Fun t"
    6.20 +    abs   "s => t ==> Abs s => Abs t"
    6.21      app   "[| s => s'; t => t' |] ==> s @ t => s' @ t'"
    6.22 -    beta  "[| s => s'; t => t' |] ==> (Fun s) @ t => s'[t'/0]"
    6.23 +    beta  "[| s => s'; t => t' |] ==> (Abs s) @ t => s'[t'/0]"
    6.24  
    6.25  consts
    6.26 -  cd  :: db => db
    6.27 -  deFun :: db => db
    6.28 +  cd  :: dB => dB
    6.29 +  deAbs :: dB => dB
    6.30  
    6.31 -primrec cd db
    6.32 +primrec cd dB
    6.33    "cd(Var n) = Var n"
    6.34    "cd(s @ t) = (case s of
    6.35              Var n => s @ (cd t) |
    6.36              s1 @ s2 => (cd s) @ (cd t) |
    6.37 -            Fun u => deFun(cd s)[cd t/0])"
    6.38 -  "cd(Fun s) = Fun(cd s)"
    6.39 +            Abs u => deAbs(cd s)[cd t/0])"
    6.40 +  "cd(Abs s) = Abs(cd s)"
    6.41  
    6.42 -primrec deFun db
    6.43 -  "deFun(Var n) = Var n"
    6.44 -  "deFun(s @ t) = s @ t"
    6.45 -  "deFun(Fun s) = s"
    6.46 +primrec deAbs dB
    6.47 +  "deAbs(Var n) = Var n"
    6.48 +  "deAbs(s @ t) = s @ t"
    6.49 +  "deAbs(Abs s) = s"
    6.50  end