author | haftmann |
Sat, 05 Jul 2014 11:01:53 +0200 | |
changeset 57514 | bdc2c6b40bf2 |
parent 53015 | a1119cf551e8 |
child 58889 | 5b7a9633cfa8 |
permissions | -rw-r--r-- |
43158 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
header "Hoare Logic" |
|
4 |
||
5 |
theory Hoare imports Big_Step begin |
|
6 |
||
7 |
subsection "Hoare Logic for Partial Correctness" |
|
8 |
||
9 |
type_synonym assn = "state \<Rightarrow> bool" |
|
10 |
||
52165 | 11 |
definition |
12 |
hoare_valid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where |
|
52167 | 13 |
"\<Turnstile> {P}c{Q} = (\<forall>s t. P s \<and> (c,s) \<Rightarrow> t \<longrightarrow> Q t)" |
52165 | 14 |
|
45212 | 15 |
abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> vname \<Rightarrow> state" |
43158 | 16 |
("_[_'/_]" [1000,0,0] 999) |
17 |
where "s[a/x] == s(x := aval a s)" |
|
18 |
||
19 |
inductive |
|
20 |
hoare :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile> ({(1_)}/ (_)/ {(1_)})" 50) |
|
21 |
where |
|
22 |
Skip: "\<turnstile> {P} SKIP {P}" | |
|
23 |
||
24 |
Assign: "\<turnstile> {\<lambda>s. P(s[a/x])} x::=a {P}" | |
|
25 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52167
diff
changeset
|
26 |
Seq: "\<lbrakk> \<turnstile> {P} c\<^sub>1 {Q}; \<turnstile> {Q} c\<^sub>2 {R} \<rbrakk> |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52167
diff
changeset
|
27 |
\<Longrightarrow> \<turnstile> {P} c\<^sub>1;;c\<^sub>2 {R}" | |
43158 | 28 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52167
diff
changeset
|
29 |
If: "\<lbrakk> \<turnstile> {\<lambda>s. P s \<and> bval b s} c\<^sub>1 {Q}; \<turnstile> {\<lambda>s. P s \<and> \<not> bval b s} c\<^sub>2 {Q} \<rbrakk> |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52167
diff
changeset
|
30 |
\<Longrightarrow> \<turnstile> {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}" | |
43158 | 31 |
|
32 |
While: "\<turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow> |
|
33 |
\<turnstile> {P} WHILE b DO c {\<lambda>s. P s \<and> \<not> bval b s}" | |
|
34 |
||
35 |
conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile> {P} c {Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> |
|
36 |
\<Longrightarrow> \<turnstile> {P'} c {Q'}" |
|
37 |
||
47818 | 38 |
lemmas [simp] = hoare.Skip hoare.Assign hoare.Seq If |
43158 | 39 |
|
47818 | 40 |
lemmas [intro!] = hoare.Skip hoare.Assign hoare.Seq hoare.If |
43158 | 41 |
|
42 |
lemma strengthen_pre: |
|
43 |
"\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile> {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile> {P'} c {Q}" |
|
44 |
by (blast intro: conseq) |
|
45 |
||
46 |
lemma weaken_post: |
|
47 |
"\<lbrakk> \<turnstile> {P} c {Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow> \<turnstile> {P} c {Q'}" |
|
48 |
by (blast intro: conseq) |
|
49 |
||
50 |
text{* The assignment and While rule are awkward to use in actual proofs |
|
51 |
because their pre and postcondition are of a very special form and the actual |
|
52 |
goal would have to match this form exactly. Therefore we derive two variants |
|
53 |
with arbitrary pre and postconditions. *} |
|
54 |
||
55 |
lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile> {P} x ::= a {Q}" |
|
56 |
by (simp add: strengthen_pre[OF _ Assign]) |
|
57 |
||
58 |
lemma While': |
|
59 |
assumes "\<turnstile> {\<lambda>s. P s \<and> bval b s} c {P}" and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s" |
|
60 |
shows "\<turnstile> {P} WHILE b DO c {Q}" |
|
61 |
by(rule weaken_post[OF While[OF assms(1)] assms(2)]) |
|
62 |
||
63 |
end |