1476
|
1 |
(* Title: HOL/IMP/Hoare.thy
|
|
2 |
Author: Tobias Nipkow
|
936
|
3 |
*)
|
|
4 |
|
12431
|
5 |
header "Inductive Definition of Hoare Logic"
|
|
6 |
|
35754
|
7 |
theory Hoare imports Natural begin
|
1447
|
8 |
|
12431
|
9 |
types assn = "state => bool"
|
1447
|
10 |
|
23746
|
11 |
inductive
|
|
12 |
hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
|
|
13 |
where
|
12431
|
14 |
skip: "|- {P}\<SKIP>{P}"
|
23746
|
15 |
| ass: "|- {%s. P(s[x\<mapsto>a s])} x:==a {P}"
|
|
16 |
| semi: "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
|
|
17 |
| If: "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
|
12431
|
18 |
|- {P} \<IF> b \<THEN> c \<ELSE> d {Q}"
|
23746
|
19 |
| While: "|- {%s. P s & b s} c {P} ==>
|
12431
|
20 |
|- {P} \<WHILE> b \<DO> c {%s. P s & ~b s}"
|
23746
|
21 |
| conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
|
1486
|
22 |
|- {P'}c{Q'}"
|
1481
|
23 |
|
35735
|
24 |
lemma strengthen_pre: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}"
|
|
25 |
by (blast intro: conseq)
|
12431
|
26 |
|
35735
|
27 |
lemma weaken_post: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}"
|
|
28 |
by (blast intro: conseq)
|
12431
|
29 |
|
35754
|
30 |
lemma While':
|
|
31 |
assumes "|- {%s. P s & b s} c {P}" and "ALL s. P s & \<not> b s \<longrightarrow> Q s"
|
|
32 |
shows "|- {P} \<WHILE> b \<DO> c {Q}"
|
|
33 |
by(rule weaken_post[OF While[OF assms(1)] assms(2)])
|
35735
|
34 |
|
12431
|
35 |
|
35754
|
36 |
lemmas [simp] = skip ass semi If
|
12431
|
37 |
|
18372
|
38 |
lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If
|
12431
|
39 |
|
939
|
40 |
end
|