--- a/src/HOL/IMP/Hoare.thy Tue Feb 06 12:44:31 1996 +0100
+++ b/src/HOL/IMP/Hoare.thy Wed Feb 07 12:22:32 1996 +0100
@@ -12,23 +12,26 @@
consts
hoare :: "(assn * com * assn) set"
- spec :: [state=>bool,com,state=>bool] => bool
+ hoare_valid :: [assn,com,assn] => bool ("|= {{_}}_{{_}}")
defs
- spec_def "spec P c Q == !s t. (s,t) : C(c) --> P s --> Q t"
+ hoare_valid_def "|= {{P}}c{{Q}} == !s t. (s,t) : C(c) --> P s --> Q t"
syntax "@hoare" :: [bool,com,bool] => bool ("{{(1_)}}/ (_)/ {{(1_)}}" 10)
translations "{{P}}c{{Q}}" == "(P,c,Q) : hoare"
inductive "hoare"
intrs
- hoare_skip "{{P}}skip{{P}}"
- hoare_ass "{{%s.P(s[A a s/x])}} x:=a {{P}}"
- hoare_semi "[| {{P}}c{{Q}}; {{Q}}d{{R}} |] ==> {{P}} c;d {{R}}"
- hoare_if "[| {{%s. P s & B b s}}c{{Q}}; {{%s. P s & ~B b s}}d{{Q}} |] ==>
- {{P}} ifc b then c else d {{Q}}"
- hoare_while "[| {{%s. P s & B b s}} c {{P}} |] ==>
- {{P}} while b do c {{%s. P s & ~B b s}}"
- hoare_conseq "[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] ==>
- {{P'}}c{{Q'}}"
+ skip "{{P}}Skip{{P}}"
+ ass "{{%s.P(s[A a s/x])}} x:=a {{P}}"
+ semi "[| {{P}}c{{Q}}; {{Q}}d{{R}} |] ==> {{P}} c;d {{R}}"
+ If "[| {{%s. P s & B b s}}c{{Q}}; {{%s. P s & ~B b s}}d{{Q}} |] ==>
+ {{P}} IF b THEN c ELSE d {{Q}}"
+ While "[| {{%s. P s & B b s}} c {{P}} |] ==>
+ {{P}} WHILE b DO c {{%s. P s & ~B b s}}"
+ conseq "[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] ==>
+ {{P'}}c{{Q'}}"
+
+consts swp :: com => assn => assn
+defs swp_def "swp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
end