Simplified primrec definitions.
--- 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
+
--- 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))"
--- 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
+
--- 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"
--- 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
--- 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])
--- 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);
--- 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
--- 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));