# HG changeset patch
# User nipkow
# Date 847124617 -3600
# Node ID e650a3f6f6005c19eabff8cbf0119fe990a4900b
# Parent  77dfe65b5bb347bc26b908916430139f6d455e51
Used nat_trans_tac. New Eta. various smaller changes.

diff -r 77dfe65b5bb3 -r e650a3f6f600 src/HOL/Lambda/Eta.ML
--- a/src/HOL/Lambda/Eta.ML	Mon Nov 04 10:56:15 1996 +0100
+++ b/src/HOL/Lambda/Eta.ML	Mon Nov 04 17:23:37 1996 +0100
@@ -13,20 +13,28 @@
 
 Addsimps eta.intrs;
 
-val eta_cases = map (eta.mk_cases db.simps)
-    ["Fun s -e> z","s @ t -e> u","Var i -e> t"];
+val eta_cases = map (eta.mk_cases dB.simps)
+    ["Abs s -e> z","s @ t -e> u","Var i -e> t"];
 
-val beta_cases = map (beta.mk_cases db.simps)
+val beta_cases = map (beta.mk_cases dB.simps)
     ["s @ t -> u","Var i -> t"];
 
 AddIs eta.intrs;
 AddSEs (beta_cases@eta_cases);
 
-section "decr and free";
+section "eta, subst and free";
+
+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);
+qed_spec_mp "subst_not_free";
+Addsimps [subst_not_free RS eqTrueI];
 
 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 (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addcongs [conj_cong])));
 by (fast_tac HOL_cs 2);
 by(simp_tac (!simpset addsimps [pred_def]
@@ -38,7 +46,7 @@
 
 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 (dB.induct_tac "s" 1);
 by (Asm_simp_tac 2);
 by (Fast_tac 2);
 by (asm_full_simp_tac (addsplit (!simpset)) 2);
@@ -51,59 +59,43 @@
 
 goal Eta.thy "!!s. s -e> t ==> !i. free t i = free s i";
 by (etac eta.induct 1);
-by (ALLGOALS(asm_simp_tac (!simpset addsimps [decr_def] addcongs [conj_cong])));
+by (ALLGOALS(asm_simp_tac (!simpset addcongs [conj_cong])));
 qed_spec_mp "free_eta";
 
 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);
-qed_spec_mp "subst_not_free";
-
-goalw Eta.thy [decr_def] "!!s. ~free s i ==> s[t/i] = decr s i";
-by (etac subst_not_free 1);
-qed "subst_decr";
-
 goal Eta.thy "!!s. s -e> t ==> !u i. s[u/i] -e> t[u/i]";
 by (etac eta.induct 1);
-by (ALLGOALS(asm_simp_tac (!simpset addsimps [subst_subst RS sym,decr_def])));
-by (asm_simp_tac (!simpset addsimps [subst_decr]) 1);
+by (ALLGOALS(asm_simp_tac (!simpset addsimps [subst_subst RS sym])));
 qed_spec_mp "eta_subst";
 Addsimps [eta_subst];
 
-goalw Eta.thy [decr_def] "!!s. s -e> t ==> decr s i -e> decr t i";
-by (etac eta_subst 1);
-qed "eta_decr";
-
 section "Confluence of -e>";
 
 goalw Eta.thy [square_def,id_def]  "square eta eta (eta^=) (eta^=)";
 by (rtac (impI RS allI RS allI) 1);
 by (Simp_tac 1);
 by (etac eta.induct 1);
-by (best_tac (!claset addSIs [eta_decr]
+by (slow_tac (!claset addIs [subst_not_free,eta_subst]
                       addIs [free_eta RS iffD1] addss !simpset) 1);
 by (slow_tac (!claset) 1);
 by (slow_tac (!claset) 1);
-by (slow_tac (!claset addSIs [eta_decr]
-                     addIs [free_eta RS iffD1]) 1);
-val lemma = result();
+by (slow_tac (!claset addSIs [eta_subst]
+                           addIs [free_eta RS iffD1]) 1);
+qed "square_eta";
 
 goal Eta.thy "confluent(eta)";
-by (rtac (lemma RS square_reflcl_confluent) 1);
+by (rtac (square_eta RS square_reflcl_confluent) 1);
 qed "eta_confluent";
 
 section "Congruence rules for -e>>";
 
-goal Eta.thy "!!s. s -e>> s' ==> Fun s -e>> Fun s'";
+goal Eta.thy "!!s. s -e>> s' ==> Abs s -e>> Abs s'";
 by (etac rtrancl_induct 1);
 by (ALLGOALS(fast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl])));
-qed "rtrancl_eta_Fun";
+qed "rtrancl_eta_Abs";
 
 goal Eta.thy "!!s. s -e>> s' ==> s @ t -e>> s' @ t";
 by (etac rtrancl_induct 1);
@@ -127,62 +119,43 @@
 by (ALLGOALS(Asm_full_simp_tac));
 qed_spec_mp "free_beta";
 
-goalw Eta.thy [decr_def] "!!s t. s -> t ==> (!i. decr s i -> decr t i)";
+goal Eta.thy "!!s t. s -> t ==> !u i. s[u/i] -> t[u/i]";
 by (etac beta.induct 1);
 by (ALLGOALS(asm_full_simp_tac (!simpset addsimps [subst_subst RS sym])));
-qed_spec_mp "beta_decr";
-
-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];
+qed_spec_mp "beta_subst";
+AddIs [beta_subst];
 
-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 (Suc i) = decr t i";
-by (db.induct_tac "t" 1);
-by (ALLGOALS
-    (asm_simp_tac (addsplit (!simpset) addsimps [le_def, less_Suc_eq])));
-qed_spec_mp "decr_not_free";
-Addsimps [decr_not_free];
+goal Eta.thy "!i. t[Var i/i] = t[Var(i)/Suc i]";
+by (dB.induct_tac "t" 1);
+by (ALLGOALS (asm_simp_tac (addsplit (!simpset))));
+by(safe_tac (HOL_cs addSEs [nat_neqE]));
+by(ALLGOALS trans_tac);
+qed_spec_mp "subst_Var_Suc";
+Addsimps [subst_Var_Suc];
 
 goal Eta.thy "!!s t. s -e> t ==> (!i. lift s i -e> lift t i)";
 by (etac eta.induct 1);
-by (ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [decr_def])));
-by (asm_simp_tac (!simpset addsimps [subst_decr]) 1);
+by (ALLGOALS(asm_simp_tac (addsplit (!simpset))));
 qed_spec_mp "eta_lift";
 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 (dB.induct_tac "u" 1);
 by (ALLGOALS(asm_simp_tac (addsplit (!simpset))));
 by (fast_tac (!claset addIs [r_into_rtrancl]) 1);
 by (fast_tac (!claset addSIs [rtrancl_eta_App]) 1);
-by (fast_tac (!claset addSIs [rtrancl_eta_Fun,eta_lift]) 1);
+by (fast_tac (!claset addSIs [rtrancl_eta_Abs,eta_lift]) 1);
 qed_spec_mp "rtrancl_eta_subst";
 
 goalw Eta.thy [square_def] "square beta eta (eta^*) (beta^=)";
 by (rtac (impI RS allI RS allI) 1);
 by (etac beta.induct 1);
-by (strip_tac 1);
-by (eresolve_tac eta_cases 1);
-by (eresolve_tac eta_cases 1);
-by (fast_tac (!claset addss (!simpset addsimps [subst_decr])) 1);
-by (slow_tac (!claset addIs [r_into_rtrancl,eta_subst]) 1);
-by (slow_tac (!claset addIs [rtrancl_eta_subst]) 1);
+by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_subst,eta_subst]
+                      addss !simpset) 1);
 by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppL]) 1);
 by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppR]) 1);
-by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_Fun,free_beta,beta_decr]
-                  addss (!simpset addsimps[subst_decr,symmetric decr_def])) 1);
+by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_Abs,free_beta]
+                      addss !simpset) 1);
 qed "square_beta_eta";
 
 goal Eta.thy "confluent(beta Un eta)";
@@ -190,23 +163,21 @@
                     beta_confluent,eta_confluent,square_beta_eta] 1));
 qed "confluent_beta_eta";
 
-
-section "Implicit definition of -e>: Fun(lift s 0 @ Var 0) -e> s";
+section "Implicit definition of -e>: Abs(lift s 0 @ Var 0) -e> s";
 
 goal Eta.thy "!i. (~free s i) = (? t. s = lift t i)";
-by (db.induct_tac "s" 1);
+by (dB.induct_tac "s" 1);
   by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   by (SELECT_GOAL(safe_tac HOL_cs)1);
-   by (res_inst_tac [("m","nat"),("n","i")] nat_less_cases 1);
-     by (res_inst_tac [("x","Var nat")] exI 1);
-     by (Asm_simp_tac 1);
-    by (fast_tac HOL_cs 1);
+   by(etac nat_neqE 1);
+    by (res_inst_tac [("x","Var nat")] exI 1);
+    by (Asm_simp_tac 1);
    by (res_inst_tac [("x","Var(pred nat)")] exI 1);
    by (Asm_simp_tac 1);
   by (rtac notE 1);
    by (assume_tac 2);
   by (etac thin_rl 1);
-  by (res_inst_tac [("db","t")] db_case_distinction 1);
+  by (res_inst_tac [("dB","t")] dB_case_distinction 1);
     by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
     by (fast_tac (HOL_cs addDs [less_not_refl2]) 1);
    by (Simp_tac 1);
@@ -222,7 +193,7 @@
   by (Asm_simp_tac 1);
  by (etac exE 1);
  by (etac rev_mp 1);
- by (res_inst_tac [("db","t")] db_case_distinction 1);
+ by (res_inst_tac [("dB","t")] dB_case_distinction 1);
    by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   by (Simp_tac 1);
   by (fast_tac HOL_cs 1);
@@ -232,19 +203,18 @@
 by (rtac allI 1);
 by (rtac iffI 1);
  by (etac exE 1);
- by (res_inst_tac [("x","Fun t")] exI 1);
+ by (res_inst_tac [("x","Abs t")] exI 1);
  by (Asm_simp_tac 1);
 by (etac exE 1);
 by (etac rev_mp 1);
-by (res_inst_tac [("db","t")] db_case_distinction 1);
+by (res_inst_tac [("dB","t")] dB_case_distinction 1);
   by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  by (Simp_tac 1);
 by (Simp_tac 1);
 by (fast_tac HOL_cs 1);
 qed_spec_mp "not_free_iff_lifted";
 
-goalw Eta.thy [decr_def]
- "(!s. (~free s 0) --> R(Fun(s @ Var 0))(decr s 0)) = \
-\ (!s. R(Fun(lift s 0 @ Var 0))(s))";
-by (fast_tac (HOL_cs addss (!simpset addsimps [lemma,not_free_iff_lifted])) 1);
+goal Eta.thy "(!s u. (~free s 0) --> R(Abs(s @ Var 0))(s[u/0])) = \
+\             (!s. R(Abs(lift s 0 @ Var 0))(s))";
+by (fast_tac (HOL_cs addss (!simpset addsimps [not_free_iff_lifted])) 1);
 qed "explicit_is_implicit";
diff -r 77dfe65b5bb3 -r e650a3f6f600 src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Mon Nov 04 10:56:15 1996 +0100
+++ b/src/HOL/Lambda/Eta.thy	Mon Nov 04 17:23:37 1996 +0100
@@ -7,11 +7,11 @@
 *)
 
 Eta = ParRed + Commutation +
-consts free :: db => nat => bool
-       decr :: [db,nat] => db
-       eta  :: "(db * db) set"
+consts free :: dB => nat => bool
+       decr :: dB => dB
+       eta  :: "(dB * dB) set"
 
-syntax  "-e>", "-e>>", "-e>=" , "->=" :: [db,db] => bool (infixl 50)
+syntax  "-e>", "-e>>", "-e>=" , "->=" :: [dB,dB] => bool (infixl 50)
 
 translations
   "s -e>  t" == "(s,t) : eta"
@@ -19,19 +19,16 @@
   "s -e>= t" == "(s,t) : eta^="
   "s ->=  t" == "(s,t) : beta^="
 
-primrec free Lambda.db
+primrec free Lambda.dB
   "free (Var j) i = (j=i)"
   "free (s @ t) i = (free s i | free t i)"
-  "free (Fun s) i = free s (Suc i)"
-
-defs
-  decr_def "decr t i == t[Var i/i]"
+  "free (Abs s) i = free s (Suc i)"
 
 inductive eta
 intrs
-   eta  "~free s 0 ==> Fun(s @ Var 0) -e> decr s 0"
+   eta  "~free s 0 ==> Abs(s @ Var 0) -e> s[dummy/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"
+   abs   "s -e> t ==> Abs s -e> Abs t"
 end
 
diff -r 77dfe65b5bb3 -r e650a3f6f600 src/HOL/Lambda/Lambda.ML
--- a/src/HOL/Lambda/Lambda.ML	Mon Nov 04 10:56:15 1996 +0100
+++ b/src/HOL/Lambda/Lambda.ML	Mon Nov 04 17:23:37 1996 +0100
@@ -16,16 +16,16 @@
 (* don't add r_into_rtrancl! *)
 AddSIs beta.intrs;
 
-val db_case_distinction =
-  rule_by_tactic(EVERY[etac thin_rl 2,etac thin_rl 2,etac thin_rl 3])db.induct;
+val dB_case_distinction =
+  rule_by_tactic(EVERY[etac thin_rl 2,etac thin_rl 2,etac thin_rl 3])dB.induct;
 
 (*** Congruence rules for ->> ***)
 
-goal Lambda.thy "!!s. s ->> s' ==> Fun s ->> Fun s'";
+goal Lambda.thy "!!s. s ->> s' ==> Abs s ->> Abs s'";
 by (etac rtrancl_induct 1);
 by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl])));
-qed "rtrancl_beta_Fun";
-AddSIs [rtrancl_beta_Fun];
+qed "rtrancl_beta_Abs";
+AddSIs [rtrancl_beta_Abs];
 
 goal Lambda.thy "!!s. s ->> s' ==> s @ t ->> s' @ t";
 by (etac rtrancl_induct 1);
@@ -64,7 +64,7 @@
 
 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 (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])
                                     addsolver (cut_trans_tac))));
 by (safe_tac HOL_cs);
@@ -73,7 +73,7 @@
 
 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 (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (!simpset addsimps [pred_def,subst_Var,lift_lift]
                                 setloop (split_tac [expand_if,expand_nat_case])
                                 addsolver (cut_trans_tac))));
@@ -85,7 +85,7 @@
 goal Lambda.thy
   "!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 (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (!simpset addsimps [subst_Var,lift_lift]
                                 setloop (split_tac [expand_if])
                                 addsolver (cut_trans_tac))));
@@ -94,7 +94,7 @@
 qed "lift_subst_lt";
 
 goal Lambda.thy "!k s. (lift t k)[s/k] = t";
-by (db.induct_tac "t" 1);
+by (dB.induct_tac "t" 1);
 by (ALLGOALS (asm_full_simp_tac (!simpset setloop (split_tac[expand_if]))));
 qed "subst_lift";
 Addsimps [subst_lift];
@@ -102,7 +102,7 @@
 
 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 (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac
       (!simpset addsimps [pred_def,subst_Var,lift_lift RS sym,lift_subst_lt]
                 setloop (split_tac [expand_if,expand_nat_case])
@@ -115,20 +115,20 @@
 (*** Equivalence proof for optimized substitution ***)
 
 goal Lambda.thy "!k. liftn 0 t k = t";
-by (db.induct_tac "t" 1);
+by (dB.induct_tac "t" 1);
 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 (dB.induct_tac "t" 1);
 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 (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac(addsplit(!simpset))));
 qed "substn_subst_n";
 Addsimps [substn_subst_n];
diff -r 77dfe65b5bb3 -r e650a3f6f600 src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Mon Nov 04 10:56:15 1996 +0100
+++ b/src/HOL/Lambda/Lambda.thy	Mon Nov 04 17:23:37 1996 +0100
@@ -9,40 +9,40 @@
 
 Lambda = Arith +
 
-datatype db = Var nat | "@" db db (infixl 200) | Fun db
+datatype dB = Var nat | "@" dB dB (infixl 200) | Abs dB
 
 consts
-  subst  :: [db,db,nat]=>db ("_[_'/_]" [300,0,0] 300)
-  lift   :: [db,nat] => db
+  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
+  substn :: [dB,dB,nat] => dB
+  liftn  :: [nat,dB,nat] => dB
 
-primrec lift db
+primrec lift dB
   "lift (Var i) k = (if i < k then Var i else Var(Suc i))"
   "lift (s @ t) k = (lift s k) @ (lift t k)"
-  "lift (Fun s) k = Fun(lift s (Suc k))"
+  "lift (Abs s) k = Abs(lift s (Suc k))"
 
-primrec subst db
+primrec subst dB
   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])"
+  subst_Abs "(Abs t)[s/k] = Abs (t[lift s 0 / Suc k])"
 
-primrec liftn db
+primrec liftn dB
   "liftn n (Var i) k = (if i < k then Var i else Var(i+n))"
   "liftn n (s @ t) k = (liftn n s k) @ (liftn n t k)"
-  "liftn n (Fun s) k = Fun(liftn n s (Suc k))"
+  "liftn n (Abs s) k = Abs(liftn n s (Suc k))"
 
-primrec substn db
+primrec substn dB
   "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 (t @ u) s k = (substn t s k) @ (substn u s k)"
-  "substn (Fun t) s k = Fun (substn t s (Suc k))"
+  "substn (Abs t) s k = Abs (substn t s (Suc k))"
 
-consts  beta :: "(db * db) set"
+consts  beta :: "(dB * dB) set"
 
-syntax  "->", "->>" :: [db,db] => bool (infixl 50)
+syntax  "->", "->>" :: [dB,dB] => bool (infixl 50)
 
 translations
   "s -> t"  == "(s,t) : beta"
@@ -50,8 +50,8 @@
 
 inductive beta
 intrs
-   beta  "(Fun s) @ t -> s[t/0]"
+   beta  "(Abs 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"
+   abs   "s -> t ==> Abs s -> Abs t"
 end
diff -r 77dfe65b5bb3 -r e650a3f6f600 src/HOL/Lambda/ParRed.ML
--- a/src/HOL/Lambda/ParRed.ML	Mon Nov 04 10:56:15 1996 +0100
+++ b/src/HOL/Lambda/ParRed.ML	Mon Nov 04 17:23:37 1996 +0100
@@ -11,9 +11,9 @@
 
 Addsimps par_beta.intrs;
 
-val par_beta_cases = map (par_beta.mk_cases db.simps)
-    ["Var n => t", "Fun s => Fun t",
-     "(Fun s) @ t => u", "s @ t => u", "Fun s => t"];
+val par_beta_cases = map (par_beta.mk_cases dB.simps)
+    ["Var n => t", "Abs s => Abs t",
+     "(Abs s) @ t => u", "s @ t => u", "Abs s => t"];
 
 AddSIs par_beta.intrs;
 AddSEs par_beta_cases;
@@ -26,7 +26,7 @@
 Addsimps [par_beta_varL];
 
 goal ParRed.thy "t => t";
-by (db.induct_tac "t" 1);
+by (dB.induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed"par_beta_refl";
 Addsimps [par_beta_refl];
@@ -50,14 +50,14 @@
 (*** => ***)
 
 goal ParRed.thy "!t' n. t => t' --> lift t n => lift t' n";
-by (db.induct_tac "t" 1);
+by (dB.induct_tac "t" 1);
 by (ALLGOALS(fast_tac (!claset addss (!simpset))));
 qed_spec_mp "par_beta_lift";
 Addsimps [par_beta_lift];
 
 goal ParRed.thy
   "!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]";
-by (db.induct_tac "t" 1);
+by (dB.induct_tac "t" 1);
   by (asm_simp_tac (addsplit(!simpset)) 1);
  by (strip_tac 1);
  by (eresolve_tac par_beta_cases 1);
@@ -79,10 +79,10 @@
 (*** cd ***)
 
 goal ParRed.thy "!t. s => t --> t => cd s";
-by (db.induct_tac "s" 1);
+by (dB.induct_tac "s" 1);
   by (Simp_tac 1);
  by (etac rev_mp 1);
- by (db.induct_tac "db1" 1);
+ by (dB.induct_tac "dB1" 1);
  by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] addss !simpset)));
 qed_spec_mp "par_beta_cd";
 
diff -r 77dfe65b5bb3 -r e650a3f6f600 src/HOL/Lambda/ParRed.thy
--- a/src/HOL/Lambda/ParRed.thy	Mon Nov 04 10:56:15 1996 +0100
+++ b/src/HOL/Lambda/ParRed.thy	Mon Nov 04 17:23:37 1996 +0100
@@ -8,9 +8,9 @@
 
 ParRed = Lambda + Commutation +
 
-consts  par_beta :: "(db * db) set"
+consts  par_beta :: "(dB * dB) set"
 
-syntax  "=>" :: [db,db] => bool (infixl 50)
+syntax  "=>" :: [dB,dB] => bool (infixl 50)
 
 translations
   "s => t" == "(s,t) : par_beta"
@@ -18,24 +18,24 @@
 inductive par_beta
   intrs
     var   "Var n => Var n"
-    abs   "s => t ==> Fun s => Fun t"
+    abs   "s => t ==> Abs s => Abs t"
     app   "[| s => s'; t => t' |] ==> s @ t => s' @ t'"
-    beta  "[| s => s'; t => t' |] ==> (Fun s) @ t => s'[t'/0]"
+    beta  "[| s => s'; t => t' |] ==> (Abs s) @ t => s'[t'/0]"
 
 consts
-  cd  :: db => db
-  deFun :: db => db
+  cd  :: dB => dB
+  deAbs :: dB => dB
 
-primrec cd db
+primrec cd dB
   "cd(Var n) = Var n"
   "cd(s @ t) = (case s of
             Var n => s @ (cd t) |
             s1 @ s2 => (cd s) @ (cd t) |
-            Fun u => deFun(cd s)[cd t/0])"
-  "cd(Fun s) = Fun(cd s)"
+            Abs u => deAbs(cd s)[cd t/0])"
+  "cd(Abs s) = Abs(cd s)"
 
-primrec deFun db
-  "deFun(Var n) = Var n"
-  "deFun(s @ t) = s @ t"
-  "deFun(Fun s) = s"
+primrec deAbs dB
+  "deAbs(Var n) = Var n"
+  "deAbs(s @ t) = s @ t"
+  "deAbs(Abs s) = s"
 end