|
1 (* Title: HOL/Hoare/Separation.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 2003 TUM |
|
5 |
|
6 A first attempt at a nice syntactic embedding of separation logic. |
|
7 *) |
|
8 |
1 theory Separation = HoareAbort: |
9 theory Separation = HoareAbort: |
2 |
10 |
3 types heap = "(nat \<Rightarrow> nat option)" |
11 types heap = "(nat \<Rightarrow> nat option)" |
4 |
|
5 |
12 |
6 text{* The semantic definition of a few connectives: *} |
13 text{* The semantic definition of a few connectives: *} |
7 |
14 |
8 constdefs |
15 constdefs |
9 ortho:: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix "\<bottom>" 55) |
16 ortho:: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix "\<bottom>" 55) |
19 "star P Q == \<lambda>h. \<exists>h1 h2. h = h1++h2 \<and> h1 \<bottom> h2 \<and> P h1 \<and> Q h2" |
26 "star P Q == \<lambda>h. \<exists>h1 h2. h = h1++h2 \<and> h1 \<bottom> h2 \<and> P h1 \<and> Q h2" |
20 |
27 |
21 wand:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)" |
28 wand:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)" |
22 "wand P Q == \<lambda>h. \<forall>h'. h' \<bottom> h \<and> P h' \<longrightarrow> Q(h++h')" |
29 "wand P Q == \<lambda>h. \<forall>h'. h' \<bottom> h \<and> P h' \<longrightarrow> Q(h++h')" |
23 |
30 |
|
31 text{*This is what assertions look like without any syntactic sugar: *} |
|
32 |
24 lemma "VARS x y z w h |
33 lemma "VARS x y z w h |
25 {star (%h. singl h x y) (%h. singl h z w) h} |
34 {star (%h. singl h x y) (%h. singl h z w) h} |
26 SKIP |
35 SKIP |
27 {x \<noteq> z}" |
36 {x \<noteq> z}" |
28 apply vcg |
37 apply vcg |
29 apply(auto simp:star_def ortho_def singl_def) |
38 apply(auto simp:star_def ortho_def singl_def) |
30 done |
39 done |
31 |
40 |
32 text{* To suppress the heap parameter of the connectives, we assume it |
41 text{* Now we add nice input syntax. To suppress the heap parameter |
33 is always called H and add/remove it upon parsing/printing. Thus |
42 of the connectives, we assume it is always called H and add/remove it |
34 every pointer program needs to have a program variable H, and |
43 upon parsing/printing. Thus every pointer program needs to have a |
35 assertions should not contain any locally bound Hs - otherwise they |
44 program variable H, and assertions should not contain any locally |
36 may bind the implicit H. *} |
45 bound Hs - otherwise they may bind the implicit H. *} |
37 |
|
38 text{* Nice input syntax: *} |
|
39 |
46 |
40 syntax |
47 syntax |
41 "@emp" :: "bool" ("emp") |
48 "@emp" :: "bool" ("emp") |
42 "@singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" ("[_ \<mapsto> _]") |
49 "@singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" ("[_ \<mapsto> _]") |
43 "@star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60) |
50 "@star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60) |
44 "@wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "-o" 60) |
51 "@wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "-*" 60) |
45 |
52 |
46 ML{* |
53 ML{* |
47 (* free_tr takes care of free vars in the scope of sep. logic connectives: |
54 (* free_tr takes care of free vars in the scope of sep. logic connectives: |
48 they are implicitly applied to the heap *) |
55 they are implicitly applied to the heap *) |
49 fun free_tr(t as Free _) = t $ Syntax.free "H" |
56 fun free_tr(t as Free _) = t $ Syntax.free "H" |
64 |
71 |
65 parse_translation |
72 parse_translation |
66 {* [("@emp", emp_tr), ("@singl", singl_tr), |
73 {* [("@emp", emp_tr), ("@singl", singl_tr), |
67 ("@star", star_tr), ("@wand", wand_tr)] *} |
74 ("@star", star_tr), ("@wand", wand_tr)] *} |
68 |
75 |
|
76 text{* Now it looks much better: *} |
|
77 |
69 lemma "VARS H x y z w |
78 lemma "VARS H x y z w |
70 {[x\<mapsto>y] ** [z\<mapsto>w]} |
79 {[x\<mapsto>y] ** [z\<mapsto>w]} |
71 SKIP |
80 SKIP |
72 {x \<noteq> z}" |
81 {x \<noteq> z}" |
73 apply vcg |
82 apply vcg |
80 {emp}" |
89 {emp}" |
81 apply vcg |
90 apply vcg |
82 apply(auto simp:star_def ortho_def is_empty_def) |
91 apply(auto simp:star_def ortho_def is_empty_def) |
83 done |
92 done |
84 |
93 |
85 text{* Nice output syntax: *} |
94 text{* But the output is still unreadable. Thus we also strip the heap |
|
95 parameters upon output: *} |
|
96 |
|
97 (* debugging code: |
|
98 fun sot(Free(s,_)) = s |
|
99 | sot(Var((s,i),_)) = "?" ^ s ^ string_of_int i |
|
100 | sot(Const(s,_)) = s |
|
101 | sot(Bound i) = "B." ^ string_of_int i |
|
102 | sot(s $ t) = "(" ^ sot s ^ " " ^ sot t ^ ")" |
|
103 | sot(Abs(_,_,t)) = "(% " ^ sot t ^ ")"; |
|
104 *) |
86 |
105 |
87 ML{* |
106 ML{* |
88 local |
107 local |
89 fun strip (Abs(_,_,(t as Free _) $ Bound 0)) = t |
108 fun strip (Abs(_,_,(t as Const("_free",_) $ Free _) $ Bound 0)) = t |
90 | strip (Abs(_,_,(t as Var _) $ Bound 0)) = t |
109 | strip (Abs(_,_,(t as Free _) $ Bound 0)) = t |
|
110 | strip (Abs(_,_,(t as Const("_var",_) $ Var _) $ Bound 0)) = t |
91 | strip (Abs(_,_,P)) = P |
111 | strip (Abs(_,_,P)) = P |
92 | strip (Const("is_empty",_)) = Syntax.const "@emp" |
112 | strip (Const("is_empty",_)) = Syntax.const "@emp" |
93 | strip t = t; |
113 | strip t = t; |
94 in |
114 in |
95 fun is_empty_tr' [_] = Syntax.const "@emp" |
115 fun is_empty_tr' [_] = Syntax.const "@emp" |
98 fun wand_tr' [P,Q,_] = Syntax.const "@wand" $ strip P $ strip Q |
118 fun wand_tr' [P,Q,_] = Syntax.const "@wand" $ strip P $ strip Q |
99 end |
119 end |
100 *} |
120 *} |
101 |
121 |
102 print_translation |
122 print_translation |
103 {* [("is_empty", is_empty_tr'),("singl", singl_tr'),("star", star_tr')] *} |
123 {* [("is_empty", is_empty_tr'),("singl", singl_tr'), |
|
124 ("star", star_tr'),("wand", wand_tr')] *} |
|
125 |
|
126 text{* Now the intermediate proof states are also readable: *} |
104 |
127 |
105 lemma "VARS H x y z w |
128 lemma "VARS H x y z w |
106 {[x\<mapsto>y] ** [z\<mapsto>w]} |
129 {[x\<mapsto>y] ** [z\<mapsto>w]} |
107 y := w |
130 y := w |
108 {x \<noteq> z}" |
131 {x \<noteq> z}" |
116 {emp}" |
139 {emp}" |
117 apply vcg |
140 apply vcg |
118 apply(auto simp:star_def ortho_def is_empty_def) |
141 apply(auto simp:star_def ortho_def is_empty_def) |
119 done |
142 done |
120 |
143 |
|
144 text{* So far we have unfolded the separation logic connectives in |
|
145 proofs. Here comes a simple example of a program proof that uses a law |
|
146 of separation logic instead. *} |
|
147 |
121 (* move to Map.thy *) |
148 (* move to Map.thy *) |
122 lemma override_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1" |
149 lemma override_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1" |
123 apply(rule ext) |
150 apply(rule ext) |
124 apply(fastsimp simp:override_def split:option.split) |
151 apply(fastsimp simp:override_def split:option.split) |
125 done |
152 done |
126 |
153 |
127 (* a law of separation logic *) |
154 (* a law of separation logic *) |
128 (* something is wrong with the pretty printer, but I cannot figure out what. *) |
|
129 |
|
130 lemma star_comm: "P ** Q = Q ** P" |
155 lemma star_comm: "P ** Q = Q ** P" |
131 apply(simp add:star_def ortho_def) |
156 apply(simp add:star_def ortho_def) |
132 apply(blast intro:override_comm) |
157 apply(blast intro:override_comm) |
133 done |
158 done |
134 |
159 |
139 apply vcg |
164 apply vcg |
140 apply(simp add: star_comm) |
165 apply(simp add: star_comm) |
141 done |
166 done |
142 |
167 |
143 end |
168 end |
144 (* |
|
145 consts llist :: "(heap * nat)set" |
|
146 inductive llist |
|
147 intros |
|
148 empty: "(%n. None, 0) : llist" |
|
149 cons: "\<lbrakk> R h h1 h2; pto h1 p q; (h2,q):llist \<rbrakk> \<Longrightarrow> (h,p):llist" |
|
150 |
|
151 lemma "VARS p q h |
|
152 {(h,p) : llist} |
|
153 h := h(q \<mapsto> p) |
|
154 {(h,q) : llist}" |
|
155 apply vcg |
|
156 apply(rule_tac "h1.0" = "%n. if n=q then Some p else None" in llist.cons) |
|
157 prefer 3 apply assumption |
|
158 prefer 2 apply(simp add:singl_def dom_def) |
|
159 apply(simp add:R_def dom_def) |
|
160 *) |
|