Simplified primrec definitions.
authorberghofe
Thu Aug 08 11:34:29 1996 +0200 (1996-08-08)
changeset 1900c7a869229091
parent 1899 0075a8d26a80
child 1901 0a4fbd097ce0
Simplified primrec definitions.
src/HOL/IMP/Expr.thy
src/HOL/IMP/VC.thy
src/HOL/Lambda/Eta.thy
src/HOL/Lambda/Lambda.thy
src/HOL/Lambda/ParRed.thy
src/HOL/Lex/AutoChopper.thy
src/HOL/MiniML/I.thy
src/HOL/MiniML/Type.thy
src/HOL/MiniML/W.thy
     1.1 --- a/src/HOL/IMP/Expr.thy	Fri Aug 02 12:25:26 1996 +0200
     1.2 +++ b/src/HOL/IMP/Expr.thy	Thu Aug 08 11:34:29 1996 +0200
     1.3 @@ -73,17 +73,18 @@
     1.4    B     :: bexp => state => bool
     1.5  
     1.6  primrec A aexp
     1.7 -  A_nat "A(N(n)) = (%s. n)"
     1.8 -  A_loc "A(X(x)) = (%s. s(x))" 
     1.9 -  A_op1 "A(Op1 f a) = (%s. f(A a s))"
    1.10 -  A_op2 "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
    1.11 +  "A(N(n)) = (%s. n)"
    1.12 +  "A(X(x)) = (%s. s(x))"
    1.13 +  "A(Op1 f a) = (%s. f(A a s))"
    1.14 +  "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
    1.15  
    1.16  primrec B bexp
    1.17 -  B_true  "B(true) = (%s. True)"
    1.18 -  B_false "B(false) = (%s. False)"
    1.19 -  B_op    "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))" 
    1.20 -  B_not   "B(noti(b)) = (%s. ~(B b s))"
    1.21 -  B_and   "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
    1.22 -  B_or    "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
    1.23 +  "B(true) = (%s. True)"
    1.24 +  "B(false) = (%s. False)"
    1.25 +  "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))"
    1.26 +  "B(noti(b)) = (%s. ~(B b s))"
    1.27 +  "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
    1.28 +  "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
    1.29  
    1.30  end
    1.31 +
     2.1 --- a/src/HOL/IMP/VC.thy	Fri Aug 02 12:25:26 1996 +0200
     2.2 +++ b/src/HOL/IMP/VC.thy	Thu Aug 08 11:34:29 1996 +0200
     2.3 @@ -22,43 +22,38 @@
     2.4    astrip :: acom => com
     2.5  
     2.6  primrec wp acom
     2.7 -  wp_Askip  "wp Askip Q = Q"
     2.8 -  wp_Aass   "wp (Aass x a) Q = (%s.Q(s[a s/x]))"
     2.9 -  wp_Asemi  "wp (Asemi c d) Q = wp c (wp d Q)"
    2.10 -  wp_Aif    "wp (Aif b c d) Q = (%s. (b s-->wp c Q s) & (~b s-->wp d Q s))" 
    2.11 -  wp_Awhile "wp (Awhile b I c) Q = I"
    2.12 +  "wp Askip Q = Q"
    2.13 +  "wp (Aass x a) Q = (%s.Q(s[a s/x]))"
    2.14 +  "wp (Asemi c d) Q = wp c (wp d Q)"
    2.15 +  "wp (Aif b c d) Q = (%s. (b s-->wp c Q s) & (~b s-->wp d Q s))" 
    2.16 +  "wp (Awhile b I c) Q = I"
    2.17  
    2.18  primrec vc acom
    2.19 -  vc_Askip  "vc Askip Q = (%s.True)"
    2.20 -  vc_Aass   "vc (Aass x a) Q = (%s.True)"
    2.21 -  vc_Asemi  "vc (Asemi c d) Q = (%s. vc c (wp d Q) s & vc d Q s)"
    2.22 -  vc_Aif    "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)" 
    2.23 -  vc_Awhile "vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) &
    2.24 +  "vc Askip Q = (%s.True)"
    2.25 +  "vc (Aass x a) Q = (%s.True)"
    2.26 +  "vc (Asemi c d) Q = (%s. vc c (wp d Q) s & vc d Q s)"
    2.27 +  "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)" 
    2.28 +  "vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) &
    2.29                                (I s & b s --> wp c I s) & vc c I s)"
    2.30  
    2.31  primrec astrip acom
    2.32 -  astrip_Askip  "astrip Askip = SKIP"
    2.33 -  astrip_Aass   "astrip (Aass x a) = (x:=a)"
    2.34 -  astrip_Asemi  "astrip (Asemi c d) = (astrip c;astrip d)"
    2.35 -  astrip_Aif    "astrip (Aif b c d) = (IF b THEN astrip c ELSE astrip d)"
    2.36 -  astrip_Awhile "astrip (Awhile b I c) = (WHILE b DO astrip c)"
    2.37 +  "astrip Askip = SKIP"
    2.38 +  "astrip (Aass x a) = (x:=a)"
    2.39 +  "astrip (Asemi c d) = (astrip c;astrip d)"
    2.40 +  "astrip (Aif b c d) = (IF b THEN astrip c ELSE astrip d)"
    2.41 +  "astrip (Awhile b I c) = (WHILE b DO astrip c)"
    2.42  
    2.43  (* simultaneous computation of vc and wp: *)
    2.44  primrec vcwp acom
    2.45 -  vcwp_Askip
    2.46    "vcwp Askip Q = (%s.True, Q)"
    2.47 -  vcwp_Aass
    2.48    "vcwp (Aass x a) Q = (%s.True, %s.Q(s[a s/x]))"
    2.49 -  vcwp_Asemi
    2.50    "vcwp (Asemi c d) Q = (let (vcd,wpd) = vcwp d Q;
    2.51                              (vcc,wpc) = vcwp c wpd
    2.52                           in (%s. vcc s & vcd s, wpc))"
    2.53 -  vcwp_Aif
    2.54    "vcwp (Aif b c d) Q = (let (vcd,wpd) = vcwp d Q;
    2.55                              (vcc,wpc) = vcwp c Q
    2.56                           in (%s. vcc s & vcd s,
    2.57                               %s.(b s-->wpc s) & (~b s-->wpd s)))"
    2.58 -  vcwp_Awhile
    2.59    "vcwp (Awhile b I c) Q = (let (vcc,wpc) = vcwp c I
    2.60                              in (%s. (I s & ~b s --> Q s) &
    2.61                                      (I s & b s --> wpc s) & vcc s, I))"
     3.1 --- a/src/HOL/Lambda/Eta.thy	Fri Aug 02 12:25:26 1996 +0200
     3.2 +++ b/src/HOL/Lambda/Eta.thy	Thu Aug 08 11:34:29 1996 +0200
     3.3 @@ -20,9 +20,9 @@
     3.4    "s ->=  t" == "(s,t) : beta^="
     3.5  
     3.6  primrec free Lambda.db
     3.7 -  free_Var "free (Var j) i = (j=i)"
     3.8 -  free_App "free (s @ t) i = (free s i | free t i)"
     3.9 -  free_Fun "free (Fun s) i = free s (Suc i)"
    3.10 +  "free (Var j) i = (j=i)"
    3.11 +  "free (s @ t) i = (free s i | free t i)"
    3.12 +  "free (Fun s) i = free s (Suc i)"
    3.13  
    3.14  defs
    3.15    decr_def "decr t i == t[Var i/i]"
    3.16 @@ -34,3 +34,4 @@
    3.17     appR  "s -e> t ==> u@s -e> u@t"
    3.18     abs   "s -e> t ==> Fun s -e> Fun t"
    3.19  end
    3.20 +
     4.1 --- a/src/HOL/Lambda/Lambda.thy	Fri Aug 02 12:25:26 1996 +0200
     4.2 +++ b/src/HOL/Lambda/Lambda.thy	Thu Aug 08 11:34:29 1996 +0200
     4.3 @@ -19,9 +19,9 @@
     4.4    liftn  :: [nat,db,nat] => db
     4.5  
     4.6  primrec lift db
     4.7 -  lift_Var "lift (Var i) k = (if i < k then Var i else Var(Suc i))"
     4.8 -  lift_App "lift (s @ t) k = (lift s k) @ (lift t k)"
     4.9 -  lift_Fun "lift (Fun s) k = Fun(lift s (Suc k))"
    4.10 +  "lift (Var i) k = (if i < k then Var i else Var(Suc i))"
    4.11 +  "lift (s @ t) k = (lift s k) @ (lift t k)"
    4.12 +  "lift (Fun s) k = Fun(lift s (Suc k))"
    4.13  
    4.14  primrec subst db
    4.15    subst_Var "(Var i)[s/k] = (if k < i then Var(pred i)
    4.16 @@ -30,15 +30,15 @@
    4.17    subst_Fun "(Fun t)[s/k] = Fun (t[lift s 0 / Suc k])"
    4.18  
    4.19  primrec liftn db
    4.20 -  liftn_Var "liftn n (Var i) k = (if i < k then Var i else Var(i+n))"
    4.21 -  liftn_App "liftn n (s @ t) k = (liftn n s k) @ (liftn n t k)"
    4.22 -  liftn_Fun "liftn n (Fun s) k = Fun(liftn n s (Suc k))"
    4.23 +  "liftn n (Var i) k = (if i < k then Var i else Var(i+n))"
    4.24 +  "liftn n (s @ t) k = (liftn n s k) @ (liftn n t k)"
    4.25 +  "liftn n (Fun s) k = Fun(liftn n s (Suc k))"
    4.26  
    4.27  primrec substn db
    4.28 -  substn_Var "substn (Var i) s k = (if k < i then Var(pred i)
    4.29 +  "substn (Var i) s k = (if k < i then Var(pred i)
    4.30                                      else if i = k then liftn k s 0 else Var i)"
    4.31 -  substn_App "substn (t @ u) s k = (substn t s k) @ (substn u s k)"
    4.32 -  substn_Fun "substn (Fun t) s k = Fun (substn t s (Suc k))"
    4.33 +  "substn (t @ u) s k = (substn t s k) @ (substn u s k)"
    4.34 +  "substn (Fun t) s k = Fun (substn t s (Suc k))"
    4.35  
    4.36  consts  beta :: "(db * db) set"
    4.37  
     5.1 --- a/src/HOL/Lambda/ParRed.thy	Fri Aug 02 12:25:26 1996 +0200
     5.2 +++ b/src/HOL/Lambda/ParRed.thy	Thu Aug 08 11:34:29 1996 +0200
     5.3 @@ -27,15 +27,15 @@
     5.4    deFun :: db => db
     5.5  
     5.6  primrec cd db
     5.7 -  cd_Var "cd(Var n) = Var n"
     5.8 -  cd_App "cd(s @ t) = (case s of
     5.9 +  "cd(Var n) = Var n"
    5.10 +  "cd(s @ t) = (case s of
    5.11              Var n => s @ (cd t) |
    5.12              s1 @ s2 => (cd s) @ (cd t) |
    5.13              Fun u => deFun(cd s)[cd t/0])"
    5.14 -  cd_Fun "cd(Fun s) = Fun(cd s)"
    5.15 +  "cd(Fun s) = Fun(cd s)"
    5.16  
    5.17  primrec deFun db
    5.18 -  deFun_Var "deFun(Var n) = Var n"
    5.19 -  deFun_App "deFun(s @ t) = s @ t"
    5.20 -  deFun_Fun "deFun(Fun s) = s"
    5.21 +  "deFun(Var n) = Var n"
    5.22 +  "deFun(s @ t) = s @ t"
    5.23 +  "deFun(Fun s) = s"
    5.24  end
     6.1 --- a/src/HOL/Lex/AutoChopper.thy	Fri Aug 02 12:25:26 1996 +0200
     6.2 +++ b/src/HOL/Lex/AutoChopper.thy	Thu Aug 08 11:34:29 1996 +0200
     6.3 @@ -29,9 +29,9 @@
     6.4    auto_chopper_def "auto_chopper A xs == acc xs (start A) [] [] ([],xs) A"
     6.5  
     6.6  primrec acc List.list
     6.7 -  acc_Nil  "acc [] st ys zs chopsr A =
     6.8 +  "acc [] st ys zs chopsr A =
     6.9                (if ys=[] then chopsr else (ys#fst(chopsr),snd(chopsr)))" 
    6.10 -  acc_Cons "acc(x#xs) st ys zs chopsr A =
    6.11 +  "acc(x#xs) st ys zs chopsr A =
    6.12              (let s0 = start(A); nxt = next(A); fin = fin(A)
    6.13               in if fin(nxt st x)
    6.14                  then acc xs (nxt st x) (zs@[x]) (zs@[x])
     7.1 --- a/src/HOL/MiniML/I.thy	Fri Aug 02 12:25:26 1996 +0200
     7.2 +++ b/src/HOL/MiniML/I.thy	Thu Aug 08 11:34:29 1996 +0200
     7.3 @@ -11,11 +11,11 @@
     7.4          I :: [expr, typ list, nat, subst] => result_W
     7.5  
     7.6  primrec I expr
     7.7 -        I_Var   "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
     7.8 +        "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
     7.9                                      else Fail)"
    7.10 -        I_Abs   "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
    7.11 +        "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
    7.12                                       Ok(s, TVar n -> t, m) )"
    7.13 -        I_App   "I (App e1 e2) a n s =
    7.14 +        "I (App e1 e2) a n s =
    7.15                     ( (s1,t1,m1) := I e1 a n s;
    7.16                       (s2,t2,m2) := I e2 a m1 s1;
    7.17                       u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
     8.1 --- a/src/HOL/MiniML/Type.thy	Fri Aug 02 12:25:26 1996 +0200
     8.2 +++ b/src/HOL/MiniML/Type.thy	Thu Aug 08 11:34:29 1996 +0200
     8.3 @@ -48,12 +48,12 @@
     8.4          free_tv :: ['a::type_struct] => nat set
     8.5  
     8.6  primrec free_tv typ
     8.7 -  free_tv_TVar    "free_tv (TVar m) = {m}"
     8.8 -  free_tv_Fun     "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
     8.9 +  "free_tv (TVar m) = {m}"
    8.10 +  "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
    8.11  
    8.12  primrec free_tv List.list
    8.13 -  free_tv_Nil     "free_tv [] = {}"
    8.14 -  free_tv_Cons    "free_tv (x#l) = (free_tv x) Un (free_tv l)"
    8.15 +  "free_tv [] = {}"
    8.16 +  "free_tv (x#l) = (free_tv x) Un (free_tv l)"
    8.17  
    8.18  (* domain of a substitution *)
    8.19  constdefs
     9.1 --- a/src/HOL/MiniML/W.thy	Fri Aug 02 12:25:26 1996 +0200
     9.2 +++ b/src/HOL/MiniML/W.thy	Thu Aug 08 11:34:29 1996 +0200
     9.3 @@ -16,11 +16,11 @@
     9.4          W :: [expr, typ list, nat] => result_W
     9.5  
     9.6  primrec W expr
     9.7 -  W_Var "W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n)
     9.8 +  "W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n)
     9.9                            else Fail)"
    9.10 -  W_Abs "W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);
    9.11 +  "W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);
    9.12                             Ok(s, (s n) -> t, m) )"
    9.13 -  W_App "W (App e1 e2) a n =
    9.14 +  "W (App e1 e2) a n =
    9.15                   ( (s1,t1,m1) := W e1 a n;
    9.16                     (s2,t2,m2) := W e2 ($s1 a) m1;
    9.17                     u := mgu ($s2 t1) (t2 -> (TVar m2));