1.1 --- a/src/HOL/IMP/VC.thy	Wed Jun 25 21:25:51 2008 +0200
     1.2 +++ b/src/HOL/IMP/VC.thy	Wed Jun 25 22:01:34 2008 +0200
     1.3 @@ -18,46 +18,44 @@
     1.4                 | Aif    bexp acom acom
     1.5                 | Awhile bexp assn acom
     1.6  
     1.7 -consts
     1.8 -  vc :: "acom => assn => assn"
     1.9 -  awp :: "acom => assn => assn"
    1.10 -  vcawp :: "acom => assn => assn \<times> assn"
    1.11 -  astrip :: "acom => com"
    1.12 +primrec awp :: "acom => assn => assn"
    1.13 +where
    1.14 +  "awp Askip Q = Q"
    1.15 +| "awp (Aass x a) Q = (\<lambda>s. Q(s[x\<mapsto>a s]))"
    1.16 +| "awp (Asemi c d) Q = awp c (awp d Q)"
    1.17 +| "awp (Aif b c d) Q = (\<lambda>s. (b s-->awp c Q s) & (~b s-->awp d Q s))"
    1.18 +| "awp (Awhile b I c) Q = I"
    1.19  
    1.20 -primrec
    1.21 -  "awp Askip Q = Q"
    1.22 -  "awp (Aass x a) Q = (\<lambda>s. Q(s[x\<mapsto>a s]))"
    1.23 -  "awp (Asemi c d) Q = awp c (awp d Q)"
    1.24 -  "awp (Aif b c d) Q = (\<lambda>s. (b s-->awp c Q s) & (~b s-->awp d Q s))"
    1.25 -  "awp (Awhile b I c) Q = I"
    1.26 -
    1.27 -primrec
    1.28 +primrec vc :: "acom => assn => assn"
    1.29 +where
    1.30    "vc Askip Q = (\<lambda>s. True)"
    1.31 -  "vc (Aass x a) Q = (\<lambda>s. True)"
    1.32 -  "vc (Asemi c d) Q = (\<lambda>s. vc c (awp d Q) s & vc d Q s)"
    1.33 -  "vc (Aif b c d) Q = (\<lambda>s. vc c Q s & vc d Q s)"
    1.34 -  "vc (Awhile b I c) Q = (\<lambda>s. (I s & ~b s --> Q s) &
    1.35 +| "vc (Aass x a) Q = (\<lambda>s. True)"
    1.36 +| "vc (Asemi c d) Q = (\<lambda>s. vc c (awp d Q) s & vc d Q s)"
    1.37 +| "vc (Aif b c d) Q = (\<lambda>s. vc c Q s & vc d Q s)"
    1.38 +| "vc (Awhile b I c) Q = (\<lambda>s. (I s & ~b s --> Q s) &
    1.39                                (I s & b s --> awp c I s) & vc c I s)"
    1.40  
    1.41 -primrec
    1.42 +primrec astrip :: "acom => com"
    1.43 +where
    1.44    "astrip Askip = SKIP"
    1.45 -  "astrip (Aass x a) = (x:==a)"
    1.46 -  "astrip (Asemi c d) = (astrip c;astrip d)"
    1.47 -  "astrip (Aif b c d) = (\<IF> b \<THEN> astrip c \<ELSE> astrip d)"
    1.48 -  "astrip (Awhile b I c) = (\<WHILE> b \<DO> astrip c)"
    1.49 +| "astrip (Aass x a) = (x:==a)"
    1.50 +| "astrip (Asemi c d) = (astrip c;astrip d)"
    1.51 +| "astrip (Aif b c d) = (\<IF> b \<THEN> astrip c \<ELSE> astrip d)"
    1.52 +| "astrip (Awhile b I c) = (\<WHILE> b \<DO> astrip c)"
    1.53  
    1.54  (* simultaneous computation of vc and awp: *)
    1.55 -primrec
    1.56 +primrec vcawp :: "acom => assn => assn \<times> assn"
    1.57 +where
    1.58    "vcawp Askip Q = (\<lambda>s. True, Q)"
    1.59 -  "vcawp (Aass x a) Q = (\<lambda>s. True, \<lambda>s. Q(s[x\<mapsto>a s]))"
    1.60 -  "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
    1.61 +| "vcawp (Aass x a) Q = (\<lambda>s. True, \<lambda>s. Q(s[x\<mapsto>a s]))"
    1.62 +| "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
    1.63                                (vcc,wpc) = vcawp c wpd
    1.64                            in (\<lambda>s. vcc s & vcd s, wpc))"
    1.65 -  "vcawp (Aif b c d) Q = (let (vcd,wpd) = vcawp d Q;
    1.66 +| "vcawp (Aif b c d) Q = (let (vcd,wpd) = vcawp d Q;
    1.67                                (vcc,wpc) = vcawp c Q
    1.68                            in (\<lambda>s. vcc s & vcd s,
    1.69                                \<lambda>s.(b s --> wpc s) & (~b s --> wpd s)))"
    1.70 -  "vcawp (Awhile b I c) Q = (let (vcc,wpc) = vcawp c I
    1.71 +| "vcawp (Awhile b I c) Q = (let (vcc,wpc) = vcawp c I
    1.72                               in (\<lambda>s. (I s & ~b s --> Q s) &
    1.73                                       (I s & b s --> wpc s) & vcc s, I))"
    1.74