src/HOL/IMP/VC.thy
changeset 5183 89f162de39cf
parent 4897 be11be0b6ea1
child 9241 f961c1fdff50
     1.1 --- a/src/HOL/IMP/VC.thy	Fri Jul 24 13:02:01 1998 +0200
     1.2 +++ b/src/HOL/IMP/VC.thy	Fri Jul 24 13:03:20 1998 +0200
     1.3 @@ -21,14 +21,14 @@
     1.4    vcawp :: "acom => assn => assn * assn"
     1.5    astrip :: acom => com
     1.6  
     1.7 -primrec awp acom
     1.8 +primrec
     1.9    "awp Askip Q = Q"
    1.10    "awp (Aass x a) Q = (%s. Q(s[x:=a s]))"
    1.11    "awp (Asemi c d) Q = awp c (awp d Q)"
    1.12    "awp (Aif b c d) Q = (%s. (b s-->awp c Q s) & (~b s-->awp d Q s))" 
    1.13    "awp (Awhile b I c) Q = I"
    1.14  
    1.15 -primrec vc acom
    1.16 +primrec
    1.17    "vc Askip Q = (%s. True)"
    1.18    "vc (Aass x a) Q = (%s. True)"
    1.19    "vc (Asemi c d) Q = (%s. vc c (awp d Q) s & vc d Q s)"
    1.20 @@ -36,7 +36,7 @@
    1.21    "vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) &
    1.22                                (I s & b s --> awp c I s) & vc c I s)"
    1.23  
    1.24 -primrec astrip acom
    1.25 +primrec
    1.26    "astrip Askip = SKIP"
    1.27    "astrip (Aass x a) = (x:=a)"
    1.28    "astrip (Asemi c d) = (astrip c;astrip d)"
    1.29 @@ -44,7 +44,7 @@
    1.30    "astrip (Awhile b I c) = (WHILE b DO astrip c)"
    1.31  
    1.32  (* simultaneous computation of vc and awp: *)
    1.33 -primrec vcawp acom
    1.34 +primrec
    1.35    "vcawp Askip Q = (%s. True, Q)"
    1.36    "vcawp (Aass x a) Q = (%s. True, %s. Q(s[x:=a s]))"
    1.37    "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;