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