src/HOL/IMP/Hoare.thy
changeset 23746 a455e69c31cc
parent 20503 503ac4c5ef91
child 27362 a6dc1769fdda
     1.1 --- a/src/HOL/IMP/Hoare.thy	Wed Jul 11 11:13:08 2007 +0200
     1.2 +++ b/src/HOL/IMP/Hoare.thy	Wed Jul 11 11:14:51 2007 +0200
     1.3 @@ -13,20 +13,17 @@
     1.4  constdefs hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50)
     1.5            "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t"
     1.6  
     1.7 -consts hoare :: "(assn * com * assn) set"
     1.8 -syntax "_hoare" :: "[bool,com,bool] => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
     1.9 -translations "|- {P}c{Q}" == "(P,c,Q) : hoare"
    1.10 -
    1.11 -inductive hoare
    1.12 -intros
    1.13 +inductive
    1.14 +  hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
    1.15 +where
    1.16    skip: "|- {P}\<SKIP>{P}"
    1.17 -  ass:  "|- {%s. P(s[x\<mapsto>a s])} x:==a {P}"
    1.18 -  semi: "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
    1.19 -  If: "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
    1.20 +| ass:  "|- {%s. P(s[x\<mapsto>a s])} x:==a {P}"
    1.21 +| semi: "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
    1.22 +| If: "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
    1.23        |- {P} \<IF> b \<THEN> c \<ELSE> d {Q}"
    1.24 -  While: "|- {%s. P s & b s} c {P} ==>
    1.25 +| While: "|- {%s. P s & b s} c {P} ==>
    1.26           |- {P} \<WHILE> b \<DO> c {%s. P s & ~b s}"
    1.27 -  conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
    1.28 +| conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
    1.29            |- {P'}c{Q'}"
    1.30  
    1.31  constdefs wp :: "com => assn => assn"