1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/IMP/VC.thy	Tue Jan 23 10:59:35 1996 +0100
     1.3 @@ -0,0 +1,45 @@
     1.4 +(*  Title: 	HOL/IMP/VC.thy
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Tobias Nipkow
     1.7 +    Copyright   1996 TUM
     1.8 +
     1.9 +acom: annotated commands
    1.10 +vc:   verification-conditions
    1.11 +wp:   weakest (liberal) precondition
    1.12 +*)
    1.13 +
    1.14 +VC  =  Hoare +
    1.15 +
    1.16 +datatype  acom = Askip
    1.17 +               | Aass   loc aexp
    1.18 +               | Asemi  acom acom
    1.19 +               | Aif    bexp acom acom
    1.20 +               | Awhile bexp assn acom
    1.21 +
    1.22 +consts
    1.23 +  vc,wp :: acom => assn => assn
    1.24 +  astrip :: acom => com
    1.25 +
    1.26 +primrec wp acom
    1.27 +  wp_Askip  "wp Askip Q = Q"
    1.28 +  wp_Aass   "wp (Aass x a) Q = (%s.Q(s[A a s/x]))"
    1.29 +  wp_Asemi  "wp (Asemi c d) Q = wp c (wp d Q)"
    1.30 +  wp_Aif    "wp (Aif b c d) Q = (%s. (B b s-->wp c Q s)&(~B b s-->wp d Q s))" 
    1.31 +  wp_Awhile "wp (Awhile b I c) Q = I"
    1.32 +
    1.33 +primrec vc acom
    1.34 +  vc_Askip  "vc Askip Q = (%s.True)"
    1.35 +  vc_Aass   "vc (Aass x a) Q = (%s.True)"
    1.36 +  vc_Asemi  "vc (Asemi c d) Q = (%s. vc c (wp d Q) s & vc d Q s)"
    1.37 +  vc_Aif    "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)" 
    1.38 +  vc_Awhile "vc (Awhile b I c) Q = (%s. (I s & ~B b s --> Q s) &
    1.39 +                              (I s & B b s --> wp c I s) & vc c I s)"
    1.40 +
    1.41 +primrec astrip acom
    1.42 +  astrip_Askip  "astrip Askip = skip"
    1.43 +  astrip_Aass   "astrip (Aass x a) = (x:=a)"
    1.44 +  astrip_Asemi  "astrip (Asemi c d) = (astrip c;astrip d)"
    1.45 +  astrip_Aif    "astrip (Aif b c d) = ifC b (astrip c) (astrip d)"
    1.46 +  astrip_Awhile "astrip (Awhile b I c) = whileC b (astrip c)"
    1.47 +  
    1.48 +end