1476
|
1 |
(* Title: HOL/IMP/Hoare.thy
|
938
|
2 |
ID: $Id$
|
1476
|
3 |
Author: Tobias Nipkow
|
936
|
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 |
|
1696
|
13 |
constdefs hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50)
|
|
14 |
"|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t"
|
939
|
15 |
|
1696
|
16 |
consts hoare :: "(assn * com * assn) set"
|
|
17 |
syntax "@hoare" :: [bool,com,bool] => bool ("|- ({(1_)}/ (_)/ {(1_)})" 50)
|
1486
|
18 |
translations "|- {P}c{Q}" == "(P,c,Q) : hoare"
|
939
|
19 |
|
1789
|
20 |
inductive hoare
|
1447
|
21 |
intrs
|
1696
|
22 |
skip "|- {P}SKIP{P}"
|
|
23 |
ass "|- {%s.P(s[a s/x])} x:=a {P}"
|
1486
|
24 |
semi "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
|
1696
|
25 |
If "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
|
1486
|
26 |
|- {P} IF b THEN c ELSE d {Q}"
|
1696
|
27 |
While "|- {%s. P s & b s} c {P} ==>
|
|
28 |
|- {P} WHILE b DO c {%s. P s & ~b s}"
|
1486
|
29 |
conseq "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
|
|
30 |
|- {P'}c{Q'}"
|
1481
|
31 |
|
1696
|
32 |
constdefs swp :: com => assn => assn
|
|
33 |
"swp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
|
939
|
34 |
|
|
35 |
end
|