author | haftmann |
Fri, 22 Mar 2019 19:18:08 +0000 | |
changeset 69946 | 494934c30f38 |
parent 69505 | cc2d676d5395 |
child 74500 | 40f03761f77f |
permissions | -rw-r--r-- |
63070 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
68776
403dd13cf6e9
avoid session qualification because no tex is generated when used;
nipkow
parents:
67406
diff
changeset
|
3 |
subsubsection "\<open>nat\<close>-Indexed Invariant" |
403dd13cf6e9
avoid session qualification because no tex is generated when used;
nipkow
parents:
67406
diff
changeset
|
4 |
|
63538
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
63070
diff
changeset
|
5 |
theory Hoare_Total_EX |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
63070
diff
changeset
|
6 |
imports Hoare |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
63070
diff
changeset
|
7 |
begin |
63070 | 8 |
|
67406 | 9 |
text\<open>This is the standard set of rules that you find in many publications. |
63070 | 10 |
The While-rule is different from the one in Concrete Semantics in that the |
11 |
invariant is indexed by natural numbers and goes down by 1 with |
|
12 |
every iteration. The completeness proof is easier but the rule is harder |
|
67406 | 13 |
to apply in program proofs.\<close> |
63070 | 14 |
|
15 |
definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" |
|
16 |
("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where |
|
17 |
"\<Turnstile>\<^sub>t {P}c{Q} \<longleftrightarrow> (\<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t))" |
|
18 |
||
19 |
inductive |
|
20 |
hoaret :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile>\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50) |
|
21 |
where |
|
22 |
||
23 |
Skip: "\<turnstile>\<^sub>t {P} SKIP {P}" | |
|
24 |
||
25 |
Assign: "\<turnstile>\<^sub>t {\<lambda>s. P(s[a/x])} x::=a {P}" | |
|
26 |
||
27 |
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}" | |
|
28 |
||
29 |
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> |
|
30 |
\<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}" | |
|
31 |
||
32 |
While: |
|
33 |
"\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {P (Suc n)} c {P n}; |
|
34 |
\<forall>n s. P (Suc n) s \<longrightarrow> bval b s; \<forall>s. P 0 s \<longrightarrow> \<not> bval b s \<rbrakk> |
|
35 |
\<Longrightarrow> \<turnstile>\<^sub>t {\<lambda>s. \<exists>n. P n s} WHILE b DO c {P 0}" | |
|
36 |
||
37 |
conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow> |
|
38 |
\<turnstile>\<^sub>t {P'}c{Q'}" |
|
39 |
||
67406 | 40 |
text\<open>Building in the consequence rule:\<close> |
63070 | 41 |
|
42 |
lemma strengthen_pre: |
|
43 |
"\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P'} c {Q}" |
|
44 |
by (metis conseq) |
|
45 |
||
46 |
lemma weaken_post: |
|
47 |
"\<lbrakk> \<turnstile>\<^sub>t {P} c {Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P} c {Q'}" |
|
48 |
by (metis conseq) |
|
49 |
||
50 |
lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile>\<^sub>t {P} x ::= a {Q}" |
|
51 |
by (simp add: strengthen_pre[OF _ Assign]) |
|
52 |
||
67406 | 53 |
text\<open>The soundness theorem:\<close> |
63070 | 54 |
|
55 |
theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<Turnstile>\<^sub>t {P}c{Q}" |
|
56 |
proof(unfold hoare_tvalid_def, induction rule: hoaret.induct) |
|
57 |
case (While P c b) |
|
67019
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
58 |
have "P n s \<Longrightarrow> \<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P 0 t" for n s |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
59 |
proof(induction "n" arbitrary: s) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
60 |
case 0 thus ?case using While.hyps(3) WhileFalse by blast |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
61 |
next |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
62 |
case Suc |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
63 |
thus ?case by (meson While.IH While.hyps(2) WhileTrue) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
64 |
qed |
63070 | 65 |
thus ?case by auto |
66 |
next |
|
67 |
case If thus ?case by auto blast |
|
68 |
qed fastforce+ |
|
69 |
||
70 |
||
71 |
definition wpt :: "com \<Rightarrow> assn \<Rightarrow> assn" ("wp\<^sub>t") where |
|
72 |
"wp\<^sub>t c Q = (\<lambda>s. \<exists>t. (c,s) \<Rightarrow> t \<and> Q t)" |
|
73 |
||
74 |
lemma [simp]: "wp\<^sub>t SKIP Q = Q" |
|
75 |
by(auto intro!: ext simp: wpt_def) |
|
76 |
||
77 |
lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>s. Q(s(x := aval e s)))" |
|
78 |
by(auto intro!: ext simp: wpt_def) |
|
79 |
||
80 |
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)" |
|
81 |
unfolding wpt_def |
|
82 |
apply(rule ext) |
|
83 |
apply auto |
|
84 |
done |
|
85 |
||
86 |
lemma [simp]: |
|
87 |
"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)" |
|
88 |
apply(unfold wpt_def) |
|
89 |
apply(rule ext) |
|
90 |
apply auto |
|
91 |
done |
|
92 |
||
93 |
||
69505 | 94 |
text\<open>Function \<open>wpw\<close> computes the weakest precondition of a While-loop |
67406 | 95 |
that is unfolded a fixed number of times.\<close> |
63070 | 96 |
|
97 |
fun wpw :: "bexp \<Rightarrow> com \<Rightarrow> nat \<Rightarrow> assn \<Rightarrow> assn" where |
|
98 |
"wpw b c 0 Q s = (\<not> bval b s \<and> Q s)" | |
|
99 |
"wpw b c (Suc n) Q s = (bval b s \<and> (\<exists>s'. (c,s) \<Rightarrow> s' \<and> wpw b c n Q s'))" |
|
100 |
||
101 |
lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> Q t \<Longrightarrow> \<exists>n. wpw b c n Q s" |
|
102 |
proof(induction "WHILE b DO c" s t rule: big_step_induct) |
|
103 |
case WhileFalse thus ?case using wpw.simps(1) by blast |
|
104 |
next |
|
105 |
case WhileTrue thus ?case using wpw.simps(2) by blast |
|
106 |
qed |
|
107 |
||
108 |
lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}" |
|
109 |
proof (induction c arbitrary: Q) |
|
110 |
case SKIP show ?case by (auto intro:hoaret.Skip) |
|
111 |
next |
|
112 |
case Assign show ?case by (auto intro:hoaret.Assign) |
|
113 |
next |
|
114 |
case Seq thus ?case by (auto intro:hoaret.Seq) |
|
115 |
next |
|
116 |
case If thus ?case by (auto intro:hoaret.If hoaret.conseq) |
|
117 |
next |
|
118 |
case (While b c) |
|
119 |
let ?w = "WHILE b DO c" |
|
120 |
have c1: "\<forall>s. wp\<^sub>t ?w Q s \<longrightarrow> (\<exists>n. wpw b c n Q s)" |
|
121 |
unfolding wpt_def by (metis WHILE_Its) |
|
122 |
have c3: "\<forall>s. wpw b c 0 Q s \<longrightarrow> Q s" by simp |
|
123 |
have w2: "\<forall>n s. wpw b c (Suc n) Q s \<longrightarrow> bval b s" by simp |
|
124 |
have w3: "\<forall>s. wpw b c 0 Q s \<longrightarrow> \<not> bval b s" by simp |
|
67019
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
125 |
have "\<turnstile>\<^sub>t {wpw b c (Suc n) Q} c {wpw b c n Q}" for n |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
126 |
proof - |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
127 |
have *: "\<forall>s. wpw b c (Suc n) Q s \<longrightarrow> (\<exists>t. (c, s) \<Rightarrow> t \<and> wpw b c n Q t)" by simp |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
128 |
show ?thesis by(rule strengthen_pre[OF * While.IH[of "wpw b c n Q", unfolded wpt_def]]) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
129 |
qed |
63070 | 130 |
from conseq[OF c1 hoaret.While[OF this w2 w3] c3] |
131 |
show ?case . |
|
132 |
qed |
|
133 |
||
134 |
theorem hoaret_complete: "\<Turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<turnstile>\<^sub>t {P}c{Q}" |
|
135 |
apply(rule strengthen_pre[OF _ wpt_is_pre]) |
|
136 |
apply(auto simp: hoare_tvalid_def wpt_def) |
|
137 |
done |
|
138 |
||
139 |
corollary hoaret_sound_complete: "\<turnstile>\<^sub>t {P}c{Q} \<longleftrightarrow> \<Turnstile>\<^sub>t {P}c{Q}" |
|
140 |
by (metis hoaret_sound hoaret_complete) |
|
141 |
||
142 |
end |