src/HOL/IMP/VC.thy
changeset 3842 b55686a7b22c
parent 2810 c4e16b36bc57
child 4897 be11be0b6ea1
     1.1 --- a/src/HOL/IMP/VC.thy	Fri Oct 10 18:37:49 1997 +0200
     1.2 +++ b/src/HOL/IMP/VC.thy	Fri Oct 10 19:02:28 1997 +0200
     1.3 @@ -23,14 +23,14 @@
     1.4  
     1.5  primrec awp acom
     1.6    "awp Askip Q = Q"
     1.7 -  "awp (Aass x a) Q = (%s.Q(s[a s/x]))"
     1.8 +  "awp (Aass x a) Q = (%s. Q(s[a s/x]))"
     1.9    "awp (Asemi c d) Q = awp c (awp d Q)"
    1.10    "awp (Aif b c d) Q = (%s. (b s-->awp c Q s) & (~b s-->awp d Q s))" 
    1.11    "awp (Awhile b I c) Q = I"
    1.12  
    1.13  primrec vc acom
    1.14 -  "vc Askip Q = (%s.True)"
    1.15 -  "vc (Aass x a) Q = (%s.True)"
    1.16 +  "vc Askip Q = (%s. True)"
    1.17 +  "vc (Aass x a) Q = (%s. True)"
    1.18    "vc (Asemi c d) Q = (%s. vc c (awp d Q) s & vc d Q s)"
    1.19    "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)" 
    1.20    "vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) &
    1.21 @@ -45,8 +45,8 @@
    1.22  
    1.23  (* simultaneous computation of vc and awp: *)
    1.24  primrec vcawp acom
    1.25 -  "vcawp Askip Q = (%s.True, Q)"
    1.26 -  "vcawp (Aass x a) Q = (%s.True, %s.Q(s[a s/x]))"
    1.27 +  "vcawp Askip Q = (%s. True, Q)"
    1.28 +  "vcawp (Aass x a) Q = (%s. True, %s. Q(s[a s/x]))"
    1.29    "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
    1.30                                (vcc,wpc) = vcawp c wpd
    1.31                            in (%s. vcc s & vcd s, wpc))"