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