author | wenzelm |
Sat, 05 Jan 2019 17:24:33 +0100 | |
changeset 69597 | ff784d5a5bfb |
parent 69505 | cc2d676d5395 |
child 74371 | 4b9876198603 |
permissions | -rw-r--r-- |
50421 | 1 |
(* Author: Tobias Nipkow *) |
43158 | 2 |
|
63538
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
55132
diff
changeset
|
3 |
subsection "Hoare Logic for Total Correctness" |
43158 | 4 |
|
68776
403dd13cf6e9
avoid session qualification because no tex is generated when used;
nipkow
parents:
67406
diff
changeset
|
5 |
subsubsection "Separate Termination Relation" |
403dd13cf6e9
avoid session qualification because no tex is generated when used;
nipkow
parents:
67406
diff
changeset
|
6 |
|
63538
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
55132
diff
changeset
|
7 |
theory Hoare_Total |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
55132
diff
changeset
|
8 |
imports Hoare_Examples |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
55132
diff
changeset
|
9 |
begin |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
55132
diff
changeset
|
10 |
|
69505 | 11 |
text\<open>Note that this definition of total validity \<open>\<Turnstile>\<^sub>t\<close> only |
67406 | 12 |
works if execution is deterministic (which it is in our case).\<close> |
43158 | 13 |
|
14 |
definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" |
|
15 |
("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where |
|
52281 | 16 |
"\<Turnstile>\<^sub>t {P}c{Q} \<longleftrightarrow> (\<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t))" |
43158 | 17 |
|
67406 | 18 |
text\<open>Provability of Hoare triples in the proof system for total |
69505 | 19 |
correctness is written \<open>\<turnstile>\<^sub>t {P}c{Q}\<close> and defined |
20 |
inductively. The rules for \<open>\<turnstile>\<^sub>t\<close> differ from those for |
|
21 |
\<open>\<turnstile>\<close> only in the one place where nontermination can arise: the |
|
69597 | 22 |
\<^term>\<open>While\<close>-rule.\<close> |
43158 | 23 |
|
24 |
inductive |
|
25 |
hoaret :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile>\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50) |
|
26 |
where |
|
52281 | 27 |
|
28 |
Skip: "\<turnstile>\<^sub>t {P} SKIP {P}" | |
|
29 |
||
30 |
Assign: "\<turnstile>\<^sub>t {\<lambda>s. P(s[a/x])} x::=a {P}" | |
|
31 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52529
diff
changeset
|
32 |
Seq: "\<lbrakk> \<turnstile>\<^sub>t {P\<^sub>1} c\<^sub>1 {P\<^sub>2}; \<turnstile>\<^sub>t {P\<^sub>2} c\<^sub>2 {P\<^sub>3} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P\<^sub>1} c\<^sub>1;;c\<^sub>2 {P\<^sub>3}" | |
52281 | 33 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52529
diff
changeset
|
34 |
If: "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s} c\<^sub>1 {Q}; \<turnstile>\<^sub>t {\<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:
52529
diff
changeset
|
35 |
\<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}" | |
52281 | 36 |
|
43158 | 37 |
While: |
52281 | 38 |
"(\<And>n::nat. |
52333 | 39 |
\<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> T s n} c {\<lambda>s. P s \<and> (\<exists>n'<n. T s n')}) |
52281 | 40 |
\<Longrightarrow> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> (\<exists>n. T s n)} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}" | |
41 |
||
43158 | 42 |
conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow> |
43 |
\<turnstile>\<^sub>t {P'}c{Q'}" |
|
44 |
||
69597 | 45 |
text\<open>The \<^term>\<open>While\<close>-rule is like the one for partial correctness but it |
43158 | 46 |
requires additionally that with every execution of the loop body some measure |
52281 | 47 |
relation @{term[source]"T :: state \<Rightarrow> nat \<Rightarrow> bool"} decreases. |
67406 | 48 |
The following functional version is more intuitive:\<close> |
52281 | 49 |
|
50 |
lemma While_fun: |
|
51 |
"\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> n = f s} c {\<lambda>s. P s \<and> f s < n}\<rbrakk> |
|
52 |
\<Longrightarrow> \<turnstile>\<^sub>t {P} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}" |
|
53 |
by (rule While [where T="\<lambda>s n. n = f s", simplified]) |
|
54 |
||
67406 | 55 |
text\<open>Building in the consequence rule:\<close> |
43158 | 56 |
|
57 |
lemma strengthen_pre: |
|
58 |
"\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P'} c {Q}" |
|
59 |
by (metis conseq) |
|
60 |
||
61 |
lemma weaken_post: |
|
62 |
"\<lbrakk> \<turnstile>\<^sub>t {P} c {Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P} c {Q'}" |
|
63 |
by (metis conseq) |
|
64 |
||
65 |
lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile>\<^sub>t {P} x ::= a {Q}" |
|
66 |
by (simp add: strengthen_pre[OF _ Assign]) |
|
67 |
||
52281 | 68 |
lemma While_fun': |
69 |
assumes "\<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> n = f s} c {\<lambda>s. P s \<and> f s < n}" |
|
43158 | 70 |
and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s" |
52281 | 71 |
shows "\<turnstile>\<^sub>t {P} WHILE b DO c {Q}" |
72 |
by(blast intro: assms(1) weaken_post[OF While_fun assms(2)]) |
|
43158 | 73 |
|
52227 | 74 |
|
67406 | 75 |
text\<open>Our standard example:\<close> |
43158 | 76 |
|
52228 | 77 |
lemma "\<turnstile>\<^sub>t {\<lambda>s. s ''x'' = i} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = sum i}" |
47818 | 78 |
apply(rule Seq) |
52228 | 79 |
prefer 2 |
52281 | 80 |
apply(rule While_fun' [where P = "\<lambda>s. (s ''y'' = sum i - sum(s ''x''))" |
81 |
and f = "\<lambda>s. nat(s ''x'')"]) |
|
52228 | 82 |
apply(rule Seq) |
83 |
prefer 2 |
|
84 |
apply(rule Assign) |
|
85 |
apply(rule Assign') |
|
86 |
apply simp |
|
87 |
apply(simp) |
|
43158 | 88 |
apply(rule Assign') |
89 |
apply simp |
|
90 |
done |
|
91 |
||
92 |
||
67406 | 93 |
text\<open>The soundness theorem:\<close> |
43158 | 94 |
|
95 |
theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<Turnstile>\<^sub>t {P}c{Q}" |
|
52282 | 96 |
proof(unfold hoare_tvalid_def, induction rule: hoaret.induct) |
52227 | 97 |
case (While P b T c) |
67019
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
98 |
have "\<lbrakk> P s; T s n \<rbrakk> \<Longrightarrow> \<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P t \<and> \<not> bval b t" for s n |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
99 |
proof(induction "n" arbitrary: s rule: less_induct) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
100 |
case (less n) thus ?case by (metis While.IH WhileFalse WhileTrue) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
101 |
qed |
52227 | 102 |
thus ?case by auto |
43158 | 103 |
next |
104 |
case If thus ?case by auto blast |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44177
diff
changeset
|
105 |
qed fastforce+ |
43158 | 106 |
|
107 |
||
67406 | 108 |
text\<open> |
43158 | 109 |
The completeness proof proceeds along the same lines as the one for partial |
110 |
correctness. First we have to strengthen our notion of weakest precondition |
|
67406 | 111 |
to take termination into account:\<close> |
43158 | 112 |
|
113 |
definition wpt :: "com \<Rightarrow> assn \<Rightarrow> assn" ("wp\<^sub>t") where |
|
52290 | 114 |
"wp\<^sub>t c Q = (\<lambda>s. \<exists>t. (c,s) \<Rightarrow> t \<and> Q t)" |
43158 | 115 |
|
116 |
lemma [simp]: "wp\<^sub>t SKIP Q = Q" |
|
117 |
by(auto intro!: ext simp: wpt_def) |
|
118 |
||
119 |
lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>s. Q(s(x := aval e s)))" |
|
120 |
by(auto intro!: ext simp: wpt_def) |
|
121 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52529
diff
changeset
|
122 |
lemma [simp]: "wp\<^sub>t (c\<^sub>1;;c\<^sub>2) Q = wp\<^sub>t c\<^sub>1 (wp\<^sub>t c\<^sub>2 Q)" |
43158 | 123 |
unfolding wpt_def |
124 |
apply(rule ext) |
|
125 |
apply auto |
|
126 |
done |
|
127 |
||
128 |
lemma [simp]: |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52529
diff
changeset
|
129 |
"wp\<^sub>t (IF b THEN c\<^sub>1 ELSE c\<^sub>2) Q = (\<lambda>s. wp\<^sub>t (if bval b s then c\<^sub>1 else c\<^sub>2) Q s)" |
43158 | 130 |
apply(unfold wpt_def) |
131 |
apply(rule ext) |
|
132 |
apply auto |
|
133 |
done |
|
134 |
||
135 |
||
69597 | 136 |
text\<open>Now we define the number of iterations \<^term>\<open>WHILE b DO c\<close> needs to |
69505 | 137 |
terminate when started in state \<open>s\<close>. Because this is a truly partial |
67406 | 138 |
function, we define it as an (inductive) relation first:\<close> |
43158 | 139 |
|
140 |
inductive Its :: "bexp \<Rightarrow> com \<Rightarrow> state \<Rightarrow> nat \<Rightarrow> bool" where |
|
141 |
Its_0: "\<not> bval b s \<Longrightarrow> Its b c s 0" | |
|
142 |
Its_Suc: "\<lbrakk> bval b s; (c,s) \<Rightarrow> s'; Its b c s' n \<rbrakk> \<Longrightarrow> Its b c s (Suc n)" |
|
143 |
||
67406 | 144 |
text\<open>The relation is in fact a function:\<close> |
43158 | 145 |
|
146 |
lemma Its_fun: "Its b c s n \<Longrightarrow> Its b c s n' \<Longrightarrow> n=n'" |
|
45015 | 147 |
proof(induction arbitrary: n' rule:Its.induct) |
43158 | 148 |
case Its_0 thus ?case by(metis Its.cases) |
149 |
next |
|
150 |
case Its_Suc thus ?case by(metis Its.cases big_step_determ) |
|
151 |
qed |
|
152 |
||
69597 | 153 |
text\<open>For all terminating loops, \<^const>\<open>Its\<close> yields a result:\<close> |
43158 | 154 |
|
155 |
lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> \<exists>n. Its b c s n" |
|
45015 | 156 |
proof(induction "WHILE b DO c" s t rule: big_step_induct) |
43158 | 157 |
case WhileFalse thus ?case by (metis Its_0) |
158 |
next |
|
159 |
case WhileTrue thus ?case by (metis Its_Suc) |
|
160 |
qed |
|
161 |
||
162 |
lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}" |
|
45015 | 163 |
proof (induction c arbitrary: Q) |
52373 | 164 |
case SKIP show ?case by (auto intro:hoaret.Skip) |
43158 | 165 |
next |
52373 | 166 |
case Assign show ?case by (auto intro:hoaret.Assign) |
43158 | 167 |
next |
52373 | 168 |
case Seq thus ?case by (auto intro:hoaret.Seq) |
43158 | 169 |
next |
52373 | 170 |
case If thus ?case by (auto intro:hoaret.If hoaret.conseq) |
43158 | 171 |
next |
172 |
case (While b c) |
|
173 |
let ?w = "WHILE b DO c" |
|
52228 | 174 |
let ?T = "Its b c" |
67019
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
175 |
have 1: "\<forall>s. wp\<^sub>t ?w Q s \<longrightarrow> wp\<^sub>t ?w Q s \<and> (\<exists>n. Its b c s n)" |
52227 | 176 |
unfolding wpt_def by (metis WHILE_Its) |
67019
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
177 |
let ?R = "\<lambda>n s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'<n. ?T s' n')" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
178 |
have "\<forall>s. wp\<^sub>t ?w Q s \<and> bval b s \<and> ?T s n \<longrightarrow> wp\<^sub>t c (?R n) s" for n |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
179 |
proof - |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
180 |
have "wp\<^sub>t c (?R n) s" if "bval b s" and "?T s n" and "(?w, s) \<Rightarrow> t" and "Q t" for s t |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
181 |
proof - |
67406 | 182 |
from \<open>bval b s\<close> and \<open>(?w, s) \<Rightarrow> t\<close> obtain s' where |
52290 | 183 |
"(c,s) \<Rightarrow> s'" "(?w,s') \<Rightarrow> t" by auto |
67406 | 184 |
from \<open>(?w, s') \<Rightarrow> t\<close> obtain n' where "?T s' n'" |
52290 | 185 |
by (blast dest: WHILE_Its) |
67406 | 186 |
with \<open>bval b s\<close> and \<open>(c, s) \<Rightarrow> s'\<close> have "?T s (Suc n')" by (rule Its_Suc) |
187 |
with \<open>?T s n\<close> have "n = Suc n'" by (rule Its_fun) |
|
188 |
with \<open>(c,s) \<Rightarrow> s'\<close> and \<open>(?w,s') \<Rightarrow> t\<close> and \<open>Q t\<close> and \<open>?T s' n'\<close> |
|
67019
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
189 |
show ?thesis by (auto simp: wpt_def) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
190 |
qed |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
191 |
thus ?thesis |
52227 | 192 |
unfolding wpt_def by auto |
193 |
(* by (metis WhileE Its_Suc Its_fun WHILE_Its lessI) *) |
|
67019
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
194 |
qed |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
195 |
note 2 = hoaret.While[OF strengthen_pre[OF this While.IH]] |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
196 |
have "\<forall>s. wp\<^sub>t ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" |
52290 | 197 |
by (auto simp add:wpt_def) |
67019
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
198 |
with 1 2 show ?case by (rule conseq) |
43158 | 199 |
qed |
200 |
||
201 |
||
69597 | 202 |
text\<open>\noindent In the \<^term>\<open>While\<close>-case, \<^const>\<open>Its\<close> provides the obvious |
43158 | 203 |
termination argument. |
204 |
||
205 |
The actual completeness theorem follows directly, in the same manner |
|
67406 | 206 |
as for partial correctness:\<close> |
43158 | 207 |
|
208 |
theorem hoaret_complete: "\<Turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<turnstile>\<^sub>t {P}c{Q}" |
|
209 |
apply(rule strengthen_pre[OF _ wpt_is_pre]) |
|
52290 | 210 |
apply(auto simp: hoare_tvalid_def wpt_def) |
43158 | 211 |
done |
212 |
||
55132 | 213 |
corollary hoaret_sound_complete: "\<turnstile>\<^sub>t {P}c{Q} \<longleftrightarrow> \<Turnstile>\<^sub>t {P}c{Q}" |
214 |
by (metis hoaret_sound hoaret_complete) |
|
215 |
||
43158 | 216 |
end |