Added vcwp
authornipkow
Tue Jan 23 14:25:55 1996 +0100 (1996-01-23)
changeset 14516803ecb9b198
parent 1450 19a256c8086d
child 1452 ee54d2c15d66
Added vcwp
src/HOL/IMP/VC.ML
src/HOL/IMP/VC.thy
     1.1 --- a/src/HOL/IMP/VC.ML	Tue Jan 23 11:33:46 1996 +0100
     1.2 +++ b/src/HOL/IMP/VC.ML	Tue Jan 23 14:25:55 1996 +0100
     1.3 @@ -77,3 +77,8 @@
     1.4  by(Asm_simp_tac 1);
     1.5  by(fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1);
     1.6  qed "vc_complete";
     1.7 +
     1.8 +goal VC.thy "!Q. vcwp c Q = (vc c Q, wp c Q)";
     1.9 +by(acom.induct_tac "c" 1);
    1.10 +by(ALLGOALS (asm_simp_tac (!simpset addsimps [Let_def])));
    1.11 +qed "vcwp_vc_wp";
     2.1 --- a/src/HOL/IMP/VC.thy	Tue Jan 23 11:33:46 1996 +0100
     2.2 +++ b/src/HOL/IMP/VC.thy	Tue Jan 23 14:25:55 1996 +0100
     2.3 @@ -18,6 +18,7 @@
     2.4  
     2.5  consts
     2.6    vc,wp :: acom => assn => assn
     2.7 +  vcwp :: "acom => assn => assn * assn"
     2.8    astrip :: acom => com
     2.9  
    2.10  primrec wp acom
    2.11 @@ -41,5 +42,25 @@
    2.12    astrip_Asemi  "astrip (Asemi c d) = (astrip c;astrip d)"
    2.13    astrip_Aif    "astrip (Aif b c d) = ifC b (astrip c) (astrip d)"
    2.14    astrip_Awhile "astrip (Awhile b I c) = whileC b (astrip c)"
    2.15 -  
    2.16 +
    2.17 +(* simultaneous computation of vc and wp: *)
    2.18 +primrec vcwp acom
    2.19 +  vcwp_Askip
    2.20 +  "vcwp Askip Q = (%s.True, Q)"
    2.21 +  vcwp_Aass
    2.22 +  "vcwp (Aass x a) Q = (%s.True, %s.Q(s[A a s/x]))"
    2.23 +  vcwp_Asemi
    2.24 +  "vcwp (Asemi c d) Q = (let (vcd,wpd) = vcwp d Q;
    2.25 +                            (vcc,wpc) = vcwp c wpd
    2.26 +                         in (%s. vcc s & vcd s, wpc))"
    2.27 +  vcwp_Aif
    2.28 +  "vcwp (Aif b c d) Q = (let (vcd,wpd) = vcwp d Q;
    2.29 +                            (vcc,wpc) = vcwp c Q
    2.30 +                         in (%s. vcc s & vcd s,
    2.31 +                             %s.(B b s-->wpc s) & (~B b s-->wpd s)))"
    2.32 +  vcwp_Awhile
    2.33 +  "vcwp (Awhile b I c) Q = (let (vcc,wpc) = vcwp c I
    2.34 +                            in (%s. (I s & ~B b s --> Q s) &
    2.35 +                                    (I s & B b s --> wpc s) & vcc s, I))"
    2.36 +
    2.37  end