src/HOL/IMP/Hoare.thy
changeset 1696 e84bff5c519b
parent 1486 7b95d7b49f7a
child 1789 aade046ec6d5
     1.1 --- a/src/HOL/IMP/Hoare.thy	Sat Apr 27 12:09:21 1996 +0200
     1.2 +++ b/src/HOL/IMP/Hoare.thy	Sat Apr 27 18:47:31 1996 +0200
     1.3 @@ -10,28 +10,26 @@
     1.4  
     1.5  types assn = state => bool
     1.6  
     1.7 -consts
     1.8 -  hoare :: "(assn * com * assn) set"
     1.9 -  hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50)
    1.10 -defs
    1.11 -  hoare_valid_def "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t"
    1.12 +constdefs hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50)
    1.13 +          "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t"
    1.14  
    1.15 -syntax "@hoare" :: [bool,com,bool] => bool ("|- {(1_)}/ (_)/ {(1_)}" 50)
    1.16 +consts hoare :: "(assn * com * assn) set"
    1.17 +syntax "@hoare" :: [bool,com,bool] => bool ("|- ({(1_)}/ (_)/ {(1_)})" 50)
    1.18  translations "|- {P}c{Q}" == "(P,c,Q) : hoare"
    1.19  
    1.20  inductive "hoare"
    1.21  intrs
    1.22 -  skip "|- {P}Skip{P}"
    1.23 -  ass  "|- {%s.P(s[A a s/x])} x:=a {P}"
    1.24 +  skip "|- {P}SKIP{P}"
    1.25 +  ass  "|- {%s.P(s[a s/x])} x:=a {P}"
    1.26    semi "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
    1.27 -  If "[| |- {%s. P s & B b s}c{Q}; |- {%s. P s & ~B b s}d{Q} |] ==>
    1.28 +  If "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
    1.29        |- {P} IF b THEN c ELSE d {Q}"
    1.30 -  While "|- {%s. P s & B b s} c {P} ==>
    1.31 -         |- {P} WHILE b DO c {%s. P s & ~B b s}"
    1.32 +  While "|- {%s. P s & b s} c {P} ==>
    1.33 +         |- {P} WHILE b DO c {%s. P s & ~b s}"
    1.34    conseq "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
    1.35            |- {P'}c{Q'}"
    1.36  
    1.37 -consts swp :: com => assn => assn
    1.38 -defs swp_def "swp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
    1.39 +constdefs swp :: com => assn => assn
    1.40 +          "swp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
    1.41  
    1.42  end