src/HOL/IMP/Hoare.thy
changeset 1481 03f096efa26d
parent 1476 608483c2122a
child 1486 7b95d7b49f7a
     1.1 --- a/src/HOL/IMP/Hoare.thy	Tue Feb 06 12:44:31 1996 +0100
     1.2 +++ b/src/HOL/IMP/Hoare.thy	Wed Feb 07 12:22:32 1996 +0100
     1.3 @@ -12,23 +12,26 @@
     1.4  
     1.5  consts
     1.6    hoare :: "(assn * com * assn) set"
     1.7 -  spec :: [state=>bool,com,state=>bool] => bool
     1.8 +  hoare_valid :: [assn,com,assn] => bool ("|= {{_}}_{{_}}")
     1.9  defs
    1.10 -  spec_def "spec 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  
    1.16  inductive "hoare"
    1.17  intrs
    1.18 -  hoare_skip "{{P}}skip{{P}}"
    1.19 -  hoare_ass  "{{%s.P(s[A a s/x])}} x:=a {{P}}"
    1.20 -  hoare_semi "[| {{P}}c{{Q}}; {{Q}}d{{R}} |] ==> {{P}} c;d {{R}}"
    1.21 -  hoare_if   "[| {{%s. P s & B b s}}c{{Q}}; {{%s. P s & ~B b s}}d{{Q}} |] ==>
    1.22 -              {{P}} ifc b then c else d {{Q}}"
    1.23 -  hoare_while "[| {{%s. P s & B b s}} c {{P}} |] ==>
    1.24 -               {{P}} while b do c {{%s. P s & ~B b s}}"
    1.25 -  hoare_conseq "[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] ==>
    1.26 -                {{P'}}c{{Q'}}"
    1.27 +  skip "{{P}}Skip{{P}}"
    1.28 +  ass  "{{%s.P(s[A a s/x])}} x:=a {{P}}"
    1.29 +  semi "[| {{P}}c{{Q}}; {{Q}}d{{R}} |] ==> {{P}} c;d {{R}}"
    1.30 +  If "[| {{%s. P s & B b s}}c{{Q}}; {{%s. P s & ~B b s}}d{{Q}} |] ==>
    1.31 +        {{P}} IF b THEN c ELSE d {{Q}}"
    1.32 +  While "[| {{%s. P s & B b s}} c {{P}} |] ==>
    1.33 +         {{P}} WHILE b DO c {{%s. P s & ~B 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  
    1.40  end