author | nipkow |
Tue, 23 Jan 1996 10:59:35 +0100 | |
changeset 1447 | bc2c0acbbf29 |
parent 1374 | 5e407f2a3323 |
child 1476 | 608483c2122a |
permissions | -rw-r--r-- |
936 | 1 |
(* Title: HOL/IMP/Hoare.thy |
938 | 2 |
ID: $Id$ |
936 | 3 |
Author: Tobias Nipkow |
4 |
Copyright 1995 TUM |
|
5 |
||
1447 | 6 |
Inductive definition of Hoare logic |
936 | 7 |
*) |
8 |
||
9 |
Hoare = Denotation + |
|
1447 | 10 |
|
11 |
types assn = state => bool |
|
12 |
||
936 | 13 |
consts |
1447 | 14 |
hoare :: "(assn * com * assn) set" |
1374 | 15 |
spec :: [state=>bool,com,state=>bool] => bool |
936 | 16 |
defs |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
939
diff
changeset
|
17 |
spec_def "spec P c Q == !s t. (s,t) : C(c) --> P s --> Q t" |
939 | 18 |
|
1447 | 19 |
syntax "@hoare" :: [bool,com,bool] => bool ("{{(1_)}}/ (_)/ {{(1_)}}" 10) |
20 |
translations "{{P}}c{{Q}}" == "(P,c,Q) : hoare" |
|
939 | 21 |
|
1447 | 22 |
inductive "hoare" |
23 |
intrs |
|
24 |
hoare_skip "{{P}}skip{{P}}" |
|
25 |
hoare_ass "{{%s.P(s[A a s/x])}} x:=a {{P}}" |
|
26 |
hoare_semi "[| {{P}}c{{Q}}; {{Q}}d{{R}} |] ==> {{P}} c;d {{R}}" |
|
27 |
hoare_if "[| {{%s. P s & B b s}}c{{Q}}; {{%s. P s & ~B b s}}d{{Q}} |] ==> |
|
28 |
{{P}} ifc b then c else d {{Q}}" |
|
29 |
hoare_while "[| {{%s. P s & B b s}} c {{P}} |] ==> |
|
30 |
{{P}} while b do c {{%s. P s & ~B b s}}" |
|
31 |
hoare_conseq "[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] ==> |
|
32 |
{{P'}}c{{Q'}}" |
|
939 | 33 |
|
34 |
end |