# HG changeset patch
# User berghofe
# Date 839496869 -7200
# Node ID c7a8692290917c6092d0cba806f5aa51069905da
# Parent  0075a8d26a8016dd04c6b60028dd1362cedf60f7
Simplified primrec definitions.

diff -r 0075a8d26a80 -r c7a869229091 src/HOL/IMP/Expr.thy
--- a/src/HOL/IMP/Expr.thy	Fri Aug 02 12:25:26 1996 +0200
+++ b/src/HOL/IMP/Expr.thy	Thu Aug 08 11:34:29 1996 +0200
@@ -73,17 +73,18 @@
   B     :: bexp => state => bool
 
 primrec A aexp
-  A_nat "A(N(n)) = (%s. n)"
-  A_loc "A(X(x)) = (%s. s(x))" 
-  A_op1 "A(Op1 f a) = (%s. f(A a s))"
-  A_op2 "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
+  "A(N(n)) = (%s. n)"
+  "A(X(x)) = (%s. s(x))"
+  "A(Op1 f a) = (%s. f(A a s))"
+  "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
 
 primrec B bexp
-  B_true  "B(true) = (%s. True)"
-  B_false "B(false) = (%s. False)"
-  B_op    "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))" 
-  B_not   "B(noti(b)) = (%s. ~(B b s))"
-  B_and   "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
-  B_or    "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
+  "B(true) = (%s. True)"
+  "B(false) = (%s. False)"
+  "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))"
+  "B(noti(b)) = (%s. ~(B b s))"
+  "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
+  "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
 
 end
+
diff -r 0075a8d26a80 -r c7a869229091 src/HOL/IMP/VC.thy
--- a/src/HOL/IMP/VC.thy	Fri Aug 02 12:25:26 1996 +0200
+++ b/src/HOL/IMP/VC.thy	Thu Aug 08 11:34:29 1996 +0200
@@ -22,43 +22,38 @@
   astrip :: acom => com
 
 primrec wp acom
-  wp_Askip  "wp Askip Q = Q"
-  wp_Aass   "wp (Aass x a) Q = (%s.Q(s[a s/x]))"
-  wp_Asemi  "wp (Asemi c d) Q = wp c (wp d Q)"
-  wp_Aif    "wp (Aif b c d) Q = (%s. (b s-->wp c Q s) & (~b s-->wp d Q s))" 
-  wp_Awhile "wp (Awhile b I c) Q = I"
+  "wp Askip Q = Q"
+  "wp (Aass x a) Q = (%s.Q(s[a s/x]))"
+  "wp (Asemi c d) Q = wp c (wp d Q)"
+  "wp (Aif b c d) Q = (%s. (b s-->wp c Q s) & (~b s-->wp d Q s))" 
+  "wp (Awhile b I c) Q = I"
 
 primrec vc acom
-  vc_Askip  "vc Askip Q = (%s.True)"
-  vc_Aass   "vc (Aass x a) Q = (%s.True)"
-  vc_Asemi  "vc (Asemi c d) Q = (%s. vc c (wp d Q) s & vc d Q s)"
-  vc_Aif    "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)" 
-  vc_Awhile "vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) &
+  "vc Askip Q = (%s.True)"
+  "vc (Aass x a) Q = (%s.True)"
+  "vc (Asemi c d) Q = (%s. vc c (wp d Q) s & vc d Q s)"
+  "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)" 
+  "vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) &
                               (I s & b s --> wp c I s) & vc c I s)"
 
 primrec astrip acom
-  astrip_Askip  "astrip Askip = SKIP"
-  astrip_Aass   "astrip (Aass x a) = (x:=a)"
-  astrip_Asemi  "astrip (Asemi c d) = (astrip c;astrip d)"
-  astrip_Aif    "astrip (Aif b c d) = (IF b THEN astrip c ELSE astrip d)"
-  astrip_Awhile "astrip (Awhile b I c) = (WHILE b DO astrip c)"
+  "astrip Askip = SKIP"
+  "astrip (Aass x a) = (x:=a)"
+  "astrip (Asemi c d) = (astrip c;astrip d)"
+  "astrip (Aif b c d) = (IF b THEN astrip c ELSE astrip d)"
+  "astrip (Awhile b I c) = (WHILE b DO astrip c)"
 
 (* simultaneous computation of vc and wp: *)
 primrec vcwp acom
-  vcwp_Askip
   "vcwp Askip Q = (%s.True, Q)"
-  vcwp_Aass
   "vcwp (Aass x a) Q = (%s.True, %s.Q(s[a s/x]))"
-  vcwp_Asemi
   "vcwp (Asemi c d) Q = (let (vcd,wpd) = vcwp d Q;
                             (vcc,wpc) = vcwp c wpd
                          in (%s. vcc s & vcd s, wpc))"
-  vcwp_Aif
   "vcwp (Aif b c d) Q = (let (vcd,wpd) = vcwp d Q;
                             (vcc,wpc) = vcwp c Q
                          in (%s. vcc s & vcd s,
                              %s.(b s-->wpc s) & (~b s-->wpd s)))"
-  vcwp_Awhile
   "vcwp (Awhile b I c) Q = (let (vcc,wpc) = vcwp c I
                             in (%s. (I s & ~b s --> Q s) &
                                     (I s & b s --> wpc s) & vcc s, I))"
diff -r 0075a8d26a80 -r c7a869229091 src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Fri Aug 02 12:25:26 1996 +0200
+++ b/src/HOL/Lambda/Eta.thy	Thu Aug 08 11:34:29 1996 +0200
@@ -20,9 +20,9 @@
   "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)"
+  "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]"
@@ -34,3 +34,4 @@
    appR  "s -e> t ==> u@s -e> u@t"
    abs   "s -e> t ==> Fun s -e> Fun t"
 end
+
diff -r 0075a8d26a80 -r c7a869229091 src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Fri Aug 02 12:25:26 1996 +0200
+++ b/src/HOL/Lambda/Lambda.thy	Thu Aug 08 11:34:29 1996 +0200
@@ -19,9 +19,9 @@
   liftn  :: [nat,db,nat] => db
 
 primrec lift db
-  lift_Var "lift (Var i) k = (if i < k then Var i else Var(Suc i))"
-  lift_App "lift (s @ t) k = (lift s k) @ (lift t k)"
-  lift_Fun "lift (Fun s) k = Fun(lift s (Suc k))"
+  "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))"
 
 primrec subst db
   subst_Var "(Var i)[s/k] = (if k < i then Var(pred i)
@@ -30,15 +30,15 @@
   subst_Fun "(Fun t)[s/k] = Fun (t[lift s 0 / Suc k])"
 
 primrec liftn db
-  liftn_Var "liftn n (Var i) k = (if i < k then Var i else Var(i+n))"
-  liftn_App "liftn n (s @ t) k = (liftn n s k) @ (liftn n t k)"
-  liftn_Fun "liftn n (Fun s) k = Fun(liftn n s (Suc k))"
+  "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))"
 
 primrec substn db
-  substn_Var "substn (Var i) s k = (if k < i then Var(pred i)
+  "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_App "substn (t @ u) s k = (substn t s k) @ (substn u s k)"
-  substn_Fun "substn (Fun t) s k = Fun (substn t s (Suc k))"
+  "substn (t @ u) s k = (substn t s k) @ (substn u s k)"
+  "substn (Fun t) s k = Fun (substn t s (Suc k))"
 
 consts  beta :: "(db * db) set"
 
diff -r 0075a8d26a80 -r c7a869229091 src/HOL/Lambda/ParRed.thy
--- a/src/HOL/Lambda/ParRed.thy	Fri Aug 02 12:25:26 1996 +0200
+++ b/src/HOL/Lambda/ParRed.thy	Thu Aug 08 11:34:29 1996 +0200
@@ -27,15 +27,15 @@
   deFun :: db => db
 
 primrec cd db
-  cd_Var "cd(Var n) = Var n"
-  cd_App "cd(s @ t) = (case s of
+  "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 "cd(Fun s) = Fun(cd s)"
+  "cd(Fun s) = Fun(cd s)"
 
 primrec deFun db
-  deFun_Var "deFun(Var n) = Var n"
-  deFun_App "deFun(s @ t) = s @ t"
-  deFun_Fun "deFun(Fun s) = s"
+  "deFun(Var n) = Var n"
+  "deFun(s @ t) = s @ t"
+  "deFun(Fun s) = s"
 end
diff -r 0075a8d26a80 -r c7a869229091 src/HOL/Lex/AutoChopper.thy
--- a/src/HOL/Lex/AutoChopper.thy	Fri Aug 02 12:25:26 1996 +0200
+++ b/src/HOL/Lex/AutoChopper.thy	Thu Aug 08 11:34:29 1996 +0200
@@ -29,9 +29,9 @@
   auto_chopper_def "auto_chopper A xs == acc xs (start A) [] [] ([],xs) A"
 
 primrec acc List.list
-  acc_Nil  "acc [] st ys zs chopsr A =
+  "acc [] st ys zs chopsr A =
               (if ys=[] then chopsr else (ys#fst(chopsr),snd(chopsr)))" 
-  acc_Cons "acc(x#xs) st ys zs chopsr A =
+  "acc(x#xs) st ys zs chopsr A =
             (let s0 = start(A); nxt = next(A); fin = fin(A)
              in if fin(nxt st x)
                 then acc xs (nxt st x) (zs@[x]) (zs@[x])
diff -r 0075a8d26a80 -r c7a869229091 src/HOL/MiniML/I.thy
--- a/src/HOL/MiniML/I.thy	Fri Aug 02 12:25:26 1996 +0200
+++ b/src/HOL/MiniML/I.thy	Thu Aug 08 11:34:29 1996 +0200
@@ -11,11 +11,11 @@
         I :: [expr, typ list, nat, subst] => result_W
 
 primrec I expr
-        I_Var   "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
+        "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
                                     else Fail)"
-        I_Abs   "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
+        "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
                                      Ok(s, TVar n -> t, m) )"
-        I_App   "I (App e1 e2) a n s =
+        "I (App e1 e2) a n s =
                    ( (s1,t1,m1) := I e1 a n s;
                      (s2,t2,m2) := I e2 a m1 s1;
                      u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
diff -r 0075a8d26a80 -r c7a869229091 src/HOL/MiniML/Type.thy
--- a/src/HOL/MiniML/Type.thy	Fri Aug 02 12:25:26 1996 +0200
+++ b/src/HOL/MiniML/Type.thy	Thu Aug 08 11:34:29 1996 +0200
@@ -48,12 +48,12 @@
         free_tv :: ['a::type_struct] => nat set
 
 primrec free_tv typ
-  free_tv_TVar    "free_tv (TVar m) = {m}"
-  free_tv_Fun     "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
+  "free_tv (TVar m) = {m}"
+  "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
 
 primrec free_tv List.list
-  free_tv_Nil     "free_tv [] = {}"
-  free_tv_Cons    "free_tv (x#l) = (free_tv x) Un (free_tv l)"
+  "free_tv [] = {}"
+  "free_tv (x#l) = (free_tv x) Un (free_tv l)"
 
 (* domain of a substitution *)
 constdefs
diff -r 0075a8d26a80 -r c7a869229091 src/HOL/MiniML/W.thy
--- a/src/HOL/MiniML/W.thy	Fri Aug 02 12:25:26 1996 +0200
+++ b/src/HOL/MiniML/W.thy	Thu Aug 08 11:34:29 1996 +0200
@@ -16,11 +16,11 @@
         W :: [expr, typ list, nat] => result_W
 
 primrec W expr
-  W_Var "W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n)
+  "W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n)
                           else Fail)"
-  W_Abs "W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);
+  "W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);
                            Ok(s, (s n) -> t, m) )"
-  W_App "W (App e1 e2) a n =
+  "W (App e1 e2) a n =
                  ( (s1,t1,m1) := W e1 a n;
                    (s2,t2,m2) := W e2 ($s1 a) m1;
                    u := mgu ($s2 t1) (t2 -> (TVar m2));