author | wenzelm |
Wed, 22 Apr 2020 19:22:43 +0200 | |
changeset 71787 | acfe72ff00c2 |
parent 69597 | ff784d5a5bfb |
child 72990 | db8f94656024 |
permissions | -rw-r--r-- |
13903 | 1 |
(* Title: HOL/Hoare/Separation.thy |
2 |
Author: Tobias Nipkow |
|
3 |
Copyright 2003 TUM |
|
4 |
||
5 |
A first attempt at a nice syntactic embedding of separation logic. |
|
14074 | 6 |
Already builds on the theory for list abstractions. |
7 |
||
8 |
If we suppress the H parameter for "List", we have to hardwired this |
|
9 |
into parser and pretty printer, which is not very modular. |
|
10 |
Alternative: some syntax like <P> which stands for P H. No more |
|
11 |
compact, but avoids the funny H. |
|
12 |
||
13903 | 13 |
*) |
14 |
||
35316
870dfea4f9c0
dropped axclass; dropped Id; session theory Hoare.thy
haftmann
parents:
35113
diff
changeset
|
15 |
theory Separation imports Hoare_Logic_Abort SepLogHeap begin |
13857 | 16 |
|
62042 | 17 |
text\<open>The semantic definition of a few connectives:\<close> |
13857 | 18 |
|
38353 | 19 |
definition ortho :: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix "\<bottom>" 55) |
20 |
where "h1 \<bottom> h2 \<longleftrightarrow> dom h1 \<inter> dom h2 = {}" |
|
13857 | 21 |
|
38353 | 22 |
definition is_empty :: "heap \<Rightarrow> bool" |
68451 | 23 |
where "is_empty h \<longleftrightarrow> h = Map.empty" |
13857 | 24 |
|
38353 | 25 |
definition singl:: "heap \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" |
26 |
where "singl h x y \<longleftrightarrow> dom h = {x} & h x = Some y" |
|
13857 | 27 |
|
38353 | 28 |
definition star:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)" |
29 |
where "star P Q = (\<lambda>h. \<exists>h1 h2. h = h1++h2 \<and> h1 \<bottom> h2 \<and> P h1 \<and> Q h2)" |
|
13875 | 30 |
|
38353 | 31 |
definition wand:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)" |
32 |
where "wand P Q = (\<lambda>h. \<forall>h'. h' \<bottom> h \<and> P h' \<longrightarrow> Q(h++h'))" |
|
13875 | 33 |
|
62042 | 34 |
text\<open>This is what assertions look like without any syntactic sugar:\<close> |
13903 | 35 |
|
13857 | 36 |
lemma "VARS x y z w h |
37 |
{star (%h. singl h x y) (%h. singl h z w) h} |
|
38 |
SKIP |
|
39 |
{x \<noteq> z}" |
|
40 |
apply vcg |
|
13875 | 41 |
apply(auto simp:star_def ortho_def singl_def) |
13857 | 42 |
done |
43 |
||
62042 | 44 |
text\<open>Now we add nice input syntax. To suppress the heap parameter |
13903 | 45 |
of the connectives, we assume it is always called H and add/remove it |
46 |
upon parsing/printing. Thus every pointer program needs to have a |
|
47 |
program variable H, and assertions should not contain any locally |
|
62042 | 48 |
bound Hs - otherwise they may bind the implicit H.\<close> |
13857 | 49 |
|
50 |
syntax |
|
35101 | 51 |
"_emp" :: "bool" ("emp") |
52 |
"_singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" ("[_ \<mapsto> _]") |
|
53 |
"_star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60) |
|
54 |
"_wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "-*" 60) |
|
13857 | 55 |
|
17781 | 56 |
(* FIXME does not handle "_idtdummy" *) |
67444 | 57 |
ML \<open> |
58 |
\<comment> \<open>\<open>free_tr\<close> takes care of free vars in the scope of separation logic connectives: |
|
59 |
they are implicitly applied to the heap\<close> |
|
13875 | 60 |
fun free_tr(t as Free _) = t $ Syntax.free "H" |
67444 | 61 |
\<^cancel>\<open>| free_tr((list as Free("List",_))$ p $ ps) = list $ Syntax.free "H" $ p $ ps\<close> |
13875 | 62 |
| free_tr t = t |
63 |
||
69597 | 64 |
fun emp_tr [] = Syntax.const \<^const_syntax>\<open>is_empty\<close> $ Syntax.free "H" |
13875 | 65 |
| emp_tr ts = raise TERM ("emp_tr", ts); |
69597 | 66 |
fun singl_tr [p, q] = Syntax.const \<^const_syntax>\<open>singl\<close> $ Syntax.free "H" $ p $ q |
13857 | 67 |
| singl_tr ts = raise TERM ("singl_tr", ts); |
69597 | 68 |
fun star_tr [P,Q] = Syntax.const \<^const_syntax>\<open>star\<close> $ |
44241 | 69 |
absfree ("H", dummyT) (free_tr P) $ absfree ("H", dummyT) (free_tr Q) $ |
13875 | 70 |
Syntax.free "H" |
71 |
| star_tr ts = raise TERM ("star_tr", ts); |
|
69597 | 72 |
fun wand_tr [P, Q] = Syntax.const \<^const_syntax>\<open>wand\<close> $ |
44241 | 73 |
absfree ("H", dummyT) P $ absfree ("H", dummyT) Q $ Syntax.free "H" |
13875 | 74 |
| wand_tr ts = raise TERM ("wand_tr", ts); |
62042 | 75 |
\<close> |
13857 | 76 |
|
62042 | 77 |
parse_translation \<open> |
69597 | 78 |
[(\<^syntax_const>\<open>_emp\<close>, K emp_tr), |
79 |
(\<^syntax_const>\<open>_singl\<close>, K singl_tr), |
|
80 |
(\<^syntax_const>\<open>_star\<close>, K star_tr), |
|
81 |
(\<^syntax_const>\<open>_wand\<close>, K wand_tr)] |
|
62042 | 82 |
\<close> |
13857 | 83 |
|
62042 | 84 |
text\<open>Now it looks much better:\<close> |
13903 | 85 |
|
13857 | 86 |
lemma "VARS H x y z w |
87 |
{[x\<mapsto>y] ** [z\<mapsto>w]} |
|
88 |
SKIP |
|
89 |
{x \<noteq> z}" |
|
90 |
apply vcg |
|
13875 | 91 |
apply(auto simp:star_def ortho_def singl_def) |
92 |
done |
|
93 |
||
94 |
lemma "VARS H x y z w |
|
95 |
{emp ** emp} |
|
96 |
SKIP |
|
97 |
{emp}" |
|
98 |
apply vcg |
|
99 |
apply(auto simp:star_def ortho_def is_empty_def) |
|
13857 | 100 |
done |
101 |
||
62042 | 102 |
text\<open>But the output is still unreadable. Thus we also strip the heap |
103 |
parameters upon output:\<close> |
|
13903 | 104 |
|
62042 | 105 |
ML \<open> |
35113 | 106 |
local |
13857 | 107 |
|
13903 | 108 |
fun strip (Abs(_,_,(t as Const("_free",_) $ Free _) $ Bound 0)) = t |
109 |
| strip (Abs(_,_,(t as Free _) $ Bound 0)) = t |
|
67444 | 110 |
\<^cancel>\<open>| strip (Abs(_,_,((list as Const("List",_))$ Bound 0 $ p $ ps))) = list$p$ps\<close> |
13903 | 111 |
| strip (Abs(_,_,(t as Const("_var",_) $ Var _) $ Bound 0)) = t |
13875 | 112 |
| strip (Abs(_,_,P)) = P |
69597 | 113 |
| strip (Const(\<^const_syntax>\<open>is_empty\<close>,_)) = Syntax.const \<^syntax_const>\<open>_emp\<close> |
13875 | 114 |
| strip t = t; |
35113 | 115 |
|
13875 | 116 |
in |
35113 | 117 |
|
69597 | 118 |
fun is_empty_tr' [_] = Syntax.const \<^syntax_const>\<open>_emp\<close> |
119 |
fun singl_tr' [_,p,q] = Syntax.const \<^syntax_const>\<open>_singl\<close> $ p $ q |
|
120 |
fun star_tr' [P,Q,_] = Syntax.const \<^syntax_const>\<open>_star\<close> $ strip P $ strip Q |
|
121 |
fun wand_tr' [P,Q,_] = Syntax.const \<^syntax_const>\<open>_wand\<close> $ strip P $ strip Q |
|
35113 | 122 |
|
13875 | 123 |
end |
62042 | 124 |
\<close> |
13857 | 125 |
|
62042 | 126 |
print_translation \<open> |
69597 | 127 |
[(\<^const_syntax>\<open>is_empty\<close>, K is_empty_tr'), |
128 |
(\<^const_syntax>\<open>singl\<close>, K singl_tr'), |
|
129 |
(\<^const_syntax>\<open>star\<close>, K star_tr'), |
|
130 |
(\<^const_syntax>\<open>wand\<close>, K wand_tr')] |
|
62042 | 131 |
\<close> |
13903 | 132 |
|
62042 | 133 |
text\<open>Now the intermediate proof states are also readable:\<close> |
13857 | 134 |
|
135 |
lemma "VARS H x y z w |
|
136 |
{[x\<mapsto>y] ** [z\<mapsto>w]} |
|
13867 | 137 |
y := w |
13857 | 138 |
{x \<noteq> z}" |
139 |
apply vcg |
|
13875 | 140 |
apply(auto simp:star_def ortho_def singl_def) |
141 |
done |
|
142 |
||
143 |
lemma "VARS H x y z w |
|
144 |
{emp ** emp} |
|
145 |
SKIP |
|
146 |
{emp}" |
|
147 |
apply vcg |
|
148 |
apply(auto simp:star_def ortho_def is_empty_def) |
|
149 |
done |
|
150 |
||
62042 | 151 |
text\<open>So far we have unfolded the separation logic connectives in |
13903 | 152 |
proofs. Here comes a simple example of a program proof that uses a law |
62042 | 153 |
of separation logic instead.\<close> |
13903 | 154 |
|
67410 | 155 |
\<comment> \<open>a law of separation logic\<close> |
13875 | 156 |
lemma star_comm: "P ** Q = Q ** P" |
18447 | 157 |
by(auto simp add:star_def ortho_def dest: map_add_comm) |
13875 | 158 |
|
159 |
lemma "VARS H x y z w |
|
160 |
{P ** Q} |
|
161 |
SKIP |
|
162 |
{Q ** P}" |
|
163 |
apply vcg |
|
164 |
apply(simp add: star_comm) |
|
165 |
done |
|
166 |
||
14074 | 167 |
|
168 |
lemma "VARS H |
|
169 |
{p\<noteq>0 \<and> [p \<mapsto> x] ** List H q qs} |
|
170 |
H := H(p \<mapsto> q) |
|
171 |
{List H p (p#qs)}" |
|
172 |
apply vcg |
|
173 |
apply(simp add: star_def ortho_def singl_def) |
|
174 |
apply clarify |
|
175 |
apply(subgoal_tac "p \<notin> set qs") |
|
176 |
prefer 2 |
|
177 |
apply(blast dest:list_in_heap) |
|
178 |
apply simp |
|
179 |
done |
|
180 |
||
181 |
lemma "VARS H p q r |
|
182 |
{List H p Ps ** List H q Qs} |
|
183 |
WHILE p \<noteq> 0 |
|
184 |
INV {\<exists>ps qs. (List H p ps ** List H q qs) \<and> rev ps @ qs = rev Ps @ Qs} |
|
185 |
DO r := p; p := the(H p); H := H(r \<mapsto> q); q := r OD |
|
186 |
{List H q (rev Ps @ Qs)}" |
|
187 |
apply vcg |
|
188 |
apply(simp_all add: star_def ortho_def singl_def) |
|
189 |
||
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44241
diff
changeset
|
190 |
apply fastforce |
14074 | 191 |
|
192 |
apply (clarsimp simp add:List_non_null) |
|
193 |
apply(rename_tac ps') |
|
194 |
apply(rule_tac x = ps' in exI) |
|
195 |
apply(rule_tac x = "p#qs" in exI) |
|
196 |
apply simp |
|
197 |
apply(rule_tac x = "h1(p:=None)" in exI) |
|
198 |
apply(rule_tac x = "h2(p\<mapsto>q)" in exI) |
|
199 |
apply simp |
|
200 |
apply(rule conjI) |
|
201 |
apply(rule ext) |
|
202 |
apply(simp add:map_add_def split:option.split) |
|
203 |
apply(rule conjI) |
|
204 |
apply blast |
|
205 |
apply(simp add:map_add_def split:option.split) |
|
206 |
apply(rule conjI) |
|
207 |
apply(subgoal_tac "p \<notin> set qs") |
|
208 |
prefer 2 |
|
209 |
apply(blast dest:list_in_heap) |
|
210 |
apply(simp) |
|
211 |
apply fast |
|
212 |
||
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44241
diff
changeset
|
213 |
apply(fastforce) |
14074 | 214 |
done |
215 |
||
13875 | 216 |
end |