src/HOL/IMP/VC.thy
changeset 1696 e84bff5c519b
parent 1481 03f096efa26d
child 1900 c7a869229091
     1.1 --- a/src/HOL/IMP/VC.thy	Sat Apr 27 12:09:21 1996 +0200
     1.2 +++ b/src/HOL/IMP/VC.thy	Sat Apr 27 18:47:31 1996 +0200
     1.3 @@ -23,9 +23,9 @@
     1.4  
     1.5  primrec wp acom
     1.6    wp_Askip  "wp Askip Q = Q"
     1.7 -  wp_Aass   "wp (Aass x a) Q = (%s.Q(s[A a s/x]))"
     1.8 +  wp_Aass   "wp (Aass x a) Q = (%s.Q(s[a s/x]))"
     1.9    wp_Asemi  "wp (Asemi c d) Q = wp c (wp d Q)"
    1.10 -  wp_Aif    "wp (Aif b c d) Q = (%s. (B b s-->wp c Q s)&(~B b s-->wp d Q s))" 
    1.11 +  wp_Aif    "wp (Aif b c d) Q = (%s. (b s-->wp c Q s) & (~b s-->wp d Q s))" 
    1.12    wp_Awhile "wp (Awhile b I c) Q = I"
    1.13  
    1.14  primrec vc acom
    1.15 @@ -33,11 +33,11 @@
    1.16    vc_Aass   "vc (Aass x a) Q = (%s.True)"
    1.17    vc_Asemi  "vc (Asemi c d) Q = (%s. vc c (wp d Q) s & vc d Q s)"
    1.18    vc_Aif    "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)" 
    1.19 -  vc_Awhile "vc (Awhile b I c) Q = (%s. (I s & ~B b s --> Q s) &
    1.20 -                              (I s & B b s --> wp c I s) & vc c I s)"
    1.21 +  vc_Awhile "vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) &
    1.22 +                              (I s & b s --> wp c I s) & vc c I s)"
    1.23  
    1.24  primrec astrip acom
    1.25 -  astrip_Askip  "astrip Askip = Skip"
    1.26 +  astrip_Askip  "astrip Askip = SKIP"
    1.27    astrip_Aass   "astrip (Aass x a) = (x:=a)"
    1.28    astrip_Asemi  "astrip (Asemi c d) = (astrip c;astrip d)"
    1.29    astrip_Aif    "astrip (Aif b c d) = (IF b THEN astrip c ELSE astrip d)"
    1.30 @@ -48,7 +48,7 @@
    1.31    vcwp_Askip
    1.32    "vcwp Askip Q = (%s.True, Q)"
    1.33    vcwp_Aass
    1.34 -  "vcwp (Aass x a) Q = (%s.True, %s.Q(s[A a s/x]))"
    1.35 +  "vcwp (Aass x a) Q = (%s.True, %s.Q(s[a s/x]))"
    1.36    vcwp_Asemi
    1.37    "vcwp (Asemi c d) Q = (let (vcd,wpd) = vcwp d Q;
    1.38                              (vcc,wpc) = vcwp c wpd
    1.39 @@ -57,10 +57,10 @@
    1.40    "vcwp (Aif b c d) Q = (let (vcd,wpd) = vcwp d Q;
    1.41                              (vcc,wpc) = vcwp c Q
    1.42                           in (%s. vcc s & vcd s,
    1.43 -                             %s.(B b s-->wpc s) & (~B b s-->wpd s)))"
    1.44 +                             %s.(b s-->wpc s) & (~b s-->wpd s)))"
    1.45    vcwp_Awhile
    1.46    "vcwp (Awhile b I c) Q = (let (vcc,wpc) = vcwp c I
    1.47 -                            in (%s. (I s & ~B b s --> Q s) &
    1.48 -                                    (I s & B b s --> wpc s) & vcc s, I))"
    1.49 +                            in (%s. (I s & ~b s --> Q s) &
    1.50 +                                    (I s & b s --> wpc s) & vcc s, I))"
    1.51  
    1.52  end