src/HOL/IMP/VC.thy
changeset 2810 c4e16b36bc57
parent 1900 c7a869229091
child 3842 b55686a7b22c
     1.1 --- a/src/HOL/IMP/VC.thy	Tue Mar 18 17:03:55 1997 +0100
     1.2 +++ b/src/HOL/IMP/VC.thy	Tue Mar 18 18:02:19 1997 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  acom: annotated commands
     1.6  vc:   verification-conditions
     1.7 -wp:   weakest (liberal) precondition
     1.8 +awp:   weakest (liberal) precondition
     1.9  *)
    1.10  
    1.11  VC  =  Hoare +
    1.12 @@ -17,24 +17,24 @@
    1.13                 | Awhile bexp assn acom
    1.14  
    1.15  consts
    1.16 -  vc,wp :: acom => assn => assn
    1.17 -  vcwp :: "acom => assn => assn * assn"
    1.18 +  vc,awp :: acom => assn => assn
    1.19 +  vcawp :: "acom => assn => assn * assn"
    1.20    astrip :: acom => com
    1.21  
    1.22 -primrec wp acom
    1.23 -  "wp Askip Q = Q"
    1.24 -  "wp (Aass x a) Q = (%s.Q(s[a s/x]))"
    1.25 -  "wp (Asemi c d) Q = wp c (wp d Q)"
    1.26 -  "wp (Aif b c d) Q = (%s. (b s-->wp c Q s) & (~b s-->wp d Q s))" 
    1.27 -  "wp (Awhile b I c) Q = I"
    1.28 +primrec awp acom
    1.29 +  "awp Askip Q = Q"
    1.30 +  "awp (Aass x a) Q = (%s.Q(s[a s/x]))"
    1.31 +  "awp (Asemi c d) Q = awp c (awp d Q)"
    1.32 +  "awp (Aif b c d) Q = (%s. (b s-->awp c Q s) & (~b s-->awp d Q s))" 
    1.33 +  "awp (Awhile b I c) Q = I"
    1.34  
    1.35  primrec vc acom
    1.36    "vc Askip Q = (%s.True)"
    1.37    "vc (Aass x a) Q = (%s.True)"
    1.38 -  "vc (Asemi c d) Q = (%s. vc c (wp d Q) s & vc d Q s)"
    1.39 +  "vc (Asemi c d) Q = (%s. vc c (awp d Q) s & vc d Q s)"
    1.40    "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)" 
    1.41    "vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) &
    1.42 -                              (I s & b s --> wp c I s) & vc c I s)"
    1.43 +                              (I s & b s --> awp c I s) & vc c I s)"
    1.44  
    1.45  primrec astrip acom
    1.46    "astrip Askip = SKIP"
    1.47 @@ -43,19 +43,19 @@
    1.48    "astrip (Aif b c d) = (IF b THEN astrip c ELSE astrip d)"
    1.49    "astrip (Awhile b I c) = (WHILE b DO astrip c)"
    1.50  
    1.51 -(* simultaneous computation of vc and wp: *)
    1.52 -primrec vcwp acom
    1.53 -  "vcwp Askip Q = (%s.True, Q)"
    1.54 -  "vcwp (Aass x a) Q = (%s.True, %s.Q(s[a s/x]))"
    1.55 -  "vcwp (Asemi c d) Q = (let (vcd,wpd) = vcwp d Q;
    1.56 -                            (vcc,wpc) = vcwp c wpd
    1.57 -                         in (%s. vcc s & vcd s, wpc))"
    1.58 -  "vcwp (Aif b c d) Q = (let (vcd,wpd) = vcwp d Q;
    1.59 -                            (vcc,wpc) = vcwp c Q
    1.60 -                         in (%s. vcc s & vcd s,
    1.61 -                             %s.(b s-->wpc s) & (~b s-->wpd s)))"
    1.62 -  "vcwp (Awhile b I c) Q = (let (vcc,wpc) = vcwp c I
    1.63 -                            in (%s. (I s & ~b s --> Q s) &
    1.64 -                                    (I s & b s --> wpc s) & vcc s, I))"
    1.65 +(* simultaneous computation of vc and awp: *)
    1.66 +primrec vcawp acom
    1.67 +  "vcawp Askip Q = (%s.True, Q)"
    1.68 +  "vcawp (Aass x a) Q = (%s.True, %s.Q(s[a s/x]))"
    1.69 +  "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
    1.70 +                              (vcc,wpc) = vcawp c wpd
    1.71 +                          in (%s. vcc s & vcd s, wpc))"
    1.72 +  "vcawp (Aif b c d) Q = (let (vcd,wpd) = vcawp d Q;
    1.73 +                              (vcc,wpc) = vcawp c Q
    1.74 +                          in (%s. vcc s & vcd s,
    1.75 +                              %s.(b s --> wpc s) & (~b s --> wpd s)))"
    1.76 +  "vcawp (Awhile b I c) Q = (let (vcc,wpc) = vcawp c I
    1.77 +                             in (%s. (I s & ~b s --> Q s) &
    1.78 +                                     (I s & b s --> wpc s) & vcc s, I))"
    1.79  
    1.80  end