# HG changeset patch
# User nipkow
# Date 900338679 -7200
# Node ID 51f81581e3d9a6d074801babfd07a15239398e0a
# Parent  42a7fe39a63a97c334dc6b6ec24e81235df47f4e
Replace awkward primrec by recdef.

diff -r 42a7fe39a63a -r 51f81581e3d9 src/HOL/Lambda/ParRed.ML
--- a/src/HOL/Lambda/ParRed.ML	Mon Jul 13 16:04:22 1998 +0200
+++ b/src/HOL/Lambda/ParRed.ML	Mon Jul 13 16:04:39 1998 +0200
@@ -80,13 +80,12 @@
 
 (*** cd ***)
 
+Addsimps cd.rules;
+
 Goal "!t. s => t --> t => cd s";
-by (dB.induct_tac "s" 1);
-  by (Simp_tac 1);
- by (etac rev_mp 1);
- by (dB.induct_tac "dB1" 1);
- by (ALLGOALS(fast_tac (claset() addSIs [par_beta_subst] 
-                                addss (simpset()))));
+by(res_inst_tac[("u","s")] cd.induct 1);
+by(Auto_tac);
+by(fast_tac (claset() addSIs [par_beta_subst]) 1);
 qed_spec_mp "par_beta_cd";
 
 (*** Confluence (via cd) ***)
diff -r 42a7fe39a63a -r 51f81581e3d9 src/HOL/Lambda/ParRed.thy
--- a/src/HOL/Lambda/ParRed.thy	Mon Jul 13 16:04:22 1998 +0200
+++ b/src/HOL/Lambda/ParRed.thy	Mon Jul 13 16:04:39 1998 +0200
@@ -6,7 +6,7 @@
 Parallel reduction and a complete developments function "cd".
 *)
 
-ParRed = Lambda + Commutation +
+ParRed = Lambda + Commutation + Recdef +
 
 consts  par_beta :: "(dB * dB) set"
 
@@ -24,17 +24,21 @@
 
 consts
   cd  :: dB => dB
-  deAbs :: dB => dB
 
-primrec cd dB
+recdef cd "measure size"
   "cd(Var n) = Var n"
+  "cd(Var n @ t) = Var n @ cd t"
+  "cd((s1 @ s2) @ t) = cd(s1 @ s2) @ cd t"
+  "cd(Abs u @ t) = (cd u)[cd t/0]"
+(*
   "cd(s @ t) = (case s of Var n   => (s @ cd t)
                         | s1 @ s2 => (cd s @ cd t) 
                         | Abs u   => deAbs(cd s)[cd t/0])"
+*)
   "cd(Abs s) = Abs(cd s)"
-
+(*
 primrec deAbs dB
   "deAbs(Var n) = Var n"
   "deAbs(s @ t) = s @ t"
-  "deAbs(Abs s) = s"
+  "deAbs(Abs s) = s"*)
 end