src/HOL/IMP/VC.thy
changeset 1900 c7a869229091
parent 1696 e84bff5c519b
child 2810 c4e16b36bc57
     1.1 --- a/src/HOL/IMP/VC.thy	Fri Aug 02 12:25:26 1996 +0200
     1.2 +++ b/src/HOL/IMP/VC.thy	Thu Aug 08 11:34:29 1996 +0200
     1.3 @@ -22,43 +22,38 @@
     1.4    astrip :: acom => com
     1.5  
     1.6  primrec wp acom
     1.7 -  wp_Askip  "wp Askip Q = Q"
     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 s-->wp c Q s) & (~b s-->wp d Q s))" 
    1.11 -  wp_Awhile "wp (Awhile b I c) Q = I"
    1.12 +  "wp Askip Q = Q"
    1.13 +  "wp (Aass x a) Q = (%s.Q(s[a s/x]))"
    1.14 +  "wp (Asemi c d) Q = wp c (wp d Q)"
    1.15 +  "wp (Aif b c d) Q = (%s. (b s-->wp c Q s) & (~b s-->wp d Q s))" 
    1.16 +  "wp (Awhile b I c) Q = I"
    1.17  
    1.18  primrec vc acom
    1.19 -  vc_Askip  "vc Askip Q = (%s.True)"
    1.20 -  vc_Aass   "vc (Aass x a) Q = (%s.True)"
    1.21 -  vc_Asemi  "vc (Asemi c d) Q = (%s. vc c (wp d Q) s & vc d Q s)"
    1.22 -  vc_Aif    "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)" 
    1.23 -  vc_Awhile "vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) &
    1.24 +  "vc Askip Q = (%s.True)"
    1.25 +  "vc (Aass x a) Q = (%s.True)"
    1.26 +  "vc (Asemi c d) Q = (%s. vc c (wp d Q) s & vc d Q s)"
    1.27 +  "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)" 
    1.28 +  "vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) &
    1.29                                (I s & b s --> wp c I s) & vc c I s)"
    1.30  
    1.31  primrec astrip acom
    1.32 -  astrip_Askip  "astrip Askip = SKIP"
    1.33 -  astrip_Aass   "astrip (Aass x a) = (x:=a)"
    1.34 -  astrip_Asemi  "astrip (Asemi c d) = (astrip c;astrip d)"
    1.35 -  astrip_Aif    "astrip (Aif b c d) = (IF b THEN astrip c ELSE astrip d)"
    1.36 -  astrip_Awhile "astrip (Awhile b I c) = (WHILE b DO astrip c)"
    1.37 +  "astrip Askip = SKIP"
    1.38 +  "astrip (Aass x a) = (x:=a)"
    1.39 +  "astrip (Asemi c d) = (astrip c;astrip d)"
    1.40 +  "astrip (Aif b c d) = (IF b THEN astrip c ELSE astrip d)"
    1.41 +  "astrip (Awhile b I c) = (WHILE b DO astrip c)"
    1.42  
    1.43  (* simultaneous computation of vc and wp: *)
    1.44  primrec vcwp acom
    1.45 -  vcwp_Askip
    1.46    "vcwp Askip Q = (%s.True, Q)"
    1.47 -  vcwp_Aass
    1.48    "vcwp (Aass x a) Q = (%s.True, %s.Q(s[a s/x]))"
    1.49 -  vcwp_Asemi
    1.50    "vcwp (Asemi c d) Q = (let (vcd,wpd) = vcwp d Q;
    1.51                              (vcc,wpc) = vcwp c wpd
    1.52                           in (%s. vcc s & vcd s, wpc))"
    1.53 -  vcwp_Aif
    1.54    "vcwp (Aif b c d) Q = (let (vcd,wpd) = vcwp d Q;
    1.55                              (vcc,wpc) = vcwp c Q
    1.56                           in (%s. vcc s & vcd s,
    1.57                               %s.(b s-->wpc s) & (~b s-->wpd s)))"
    1.58 -  vcwp_Awhile
    1.59    "vcwp (Awhile b I c) Q = (let (vcc,wpc) = vcwp c I
    1.60                              in (%s. (I s & ~b s --> Q s) &
    1.61                                      (I s & b s --> wpc s) & vcc s, I))"