src/HOL/Hoare/Separation.thy
 author huffman Fri Mar 30 12:32:35 2012 +0200 (2012-03-30) changeset 47220 52426c62b5d0 parent 44890 22f665a2e91c child 52143 36ffe23b25f8 permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
```     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.
```
```     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
```
```    13 *)
```
```    14
```
```    15 theory Separation imports Hoare_Logic_Abort SepLogHeap begin
```
```    16
```
```    17 text{* The semantic definition of a few connectives: *}
```
```    18
```
```    19 definition ortho :: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix "\<bottom>" 55)
```
```    20   where "h1 \<bottom> h2 \<longleftrightarrow> dom h1 \<inter> dom h2 = {}"
```
```    21
```
```    22 definition is_empty :: "heap \<Rightarrow> bool"
```
```    23   where "is_empty h \<longleftrightarrow> h = empty"
```
```    24
```
```    25 definition singl:: "heap \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
```
```    26   where "singl h x y \<longleftrightarrow> dom h = {x} & h x = Some y"
```
```    27
```
```    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)"
```
```    30
```
```    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'))"
```
```    33
```
```    34 text{*This is what assertions look like without any syntactic sugar: *}
```
```    35
```
```    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
```
```    41 apply(auto simp:star_def ortho_def singl_def)
```
```    42 done
```
```    43
```
```    44 text{* Now we add nice input syntax.  To suppress the heap parameter
```
```    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
```
```    48 bound Hs - otherwise they may bind the implicit H. *}
```
```    49
```
```    50 syntax
```
```    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" *)
```
```    57 ML{*
```
```    58 (* free_tr takes care of free vars in the scope of sep. logic connectives:
```
```    59    they are implicitly applied to the heap *)
```
```    60 fun free_tr(t as Free _) = t \$ Syntax.free "H"
```
```    61 (*
```
```    62   | free_tr((list as Free("List",_))\$ p \$ ps) = list \$ Syntax.free "H" \$ p \$ ps
```
```    63 *)
```
```    64   | free_tr t = t
```
```    65
```
```    66 fun emp_tr [] = Syntax.const @{const_syntax is_empty} \$ Syntax.free "H"
```
```    67   | emp_tr ts = raise TERM ("emp_tr", ts);
```
```    68 fun singl_tr [p, q] = Syntax.const @{const_syntax singl} \$ Syntax.free "H" \$ p \$ q
```
```    69   | singl_tr ts = raise TERM ("singl_tr", ts);
```
```    70 fun star_tr [P,Q] = Syntax.const @{const_syntax star} \$
```
```    71       absfree ("H", dummyT) (free_tr P) \$ absfree ("H", dummyT) (free_tr Q) \$
```
```    72       Syntax.free "H"
```
```    73   | star_tr ts = raise TERM ("star_tr", ts);
```
```    74 fun wand_tr [P, Q] = Syntax.const @{const_syntax wand} \$
```
```    75       absfree ("H", dummyT) P \$ absfree ("H", dummyT) Q \$ Syntax.free "H"
```
```    76   | wand_tr ts = raise TERM ("wand_tr", ts);
```
```    77 *}
```
```    78
```
```    79 parse_translation {*
```
```    80  [(@{syntax_const "_emp"}, emp_tr),
```
```    81   (@{syntax_const "_singl"}, singl_tr),
```
```    82   (@{syntax_const "_star"}, star_tr),
```
```    83   (@{syntax_const "_wand"}, wand_tr)]
```
```    84 *}
```
```    85
```
```    86 text{* Now it looks much better: *}
```
```    87
```
```    88 lemma "VARS H x y z w
```
```    89  {[x\<mapsto>y] ** [z\<mapsto>w]}
```
```    90  SKIP
```
```    91  {x \<noteq> z}"
```
```    92 apply vcg
```
```    93 apply(auto simp:star_def ortho_def singl_def)
```
```    94 done
```
```    95
```
```    96 lemma "VARS H x y z w
```
```    97  {emp ** emp}
```
```    98  SKIP
```
```    99  {emp}"
```
```   100 apply vcg
```
```   101 apply(auto simp:star_def ortho_def is_empty_def)
```
```   102 done
```
```   103
```
```   104 text{* But the output is still unreadable. Thus we also strip the heap
```
```   105 parameters upon output: *}
```
```   106
```
```   107 ML {*
```
```   108 local
```
```   109
```
```   110 fun strip (Abs(_,_,(t as Const("_free",_) \$ Free _) \$ Bound 0)) = t
```
```   111   | strip (Abs(_,_,(t as Free _) \$ Bound 0)) = t
```
```   112 (*
```
```   113   | strip (Abs(_,_,((list as Const("List",_))\$ Bound 0 \$ p \$ ps))) = list\$p\$ps
```
```   114 *)
```
```   115   | strip (Abs(_,_,(t as Const("_var",_) \$ Var _) \$ Bound 0)) = t
```
```   116   | strip (Abs(_,_,P)) = P
```
```   117   | strip (Const(@{const_syntax is_empty},_)) = Syntax.const @{syntax_const "_emp"}
```
```   118   | strip t = t;
```
```   119
```
```   120 in
```
```   121
```
```   122 fun is_empty_tr' [_] = Syntax.const @{syntax_const "_emp"}
```
```   123 fun singl_tr' [_,p,q] = Syntax.const @{syntax_const "_singl"} \$ p \$ q
```
```   124 fun star_tr' [P,Q,_] = Syntax.const @{syntax_const "_star"} \$ strip P \$ strip Q
```
```   125 fun wand_tr' [P,Q,_] = Syntax.const @{syntax_const "_wand"} \$ strip P \$ strip Q
```
```   126
```
```   127 end
```
```   128 *}
```
```   129
```
```   130 print_translation {*
```
```   131  [(@{const_syntax is_empty}, is_empty_tr'),
```
```   132   (@{const_syntax singl}, singl_tr'),
```
```   133   (@{const_syntax star}, star_tr'),
```
```   134   (@{const_syntax wand}, wand_tr')]
```
```   135 *}
```
```   136
```
```   137 text{* Now the intermediate proof states are also readable: *}
```
```   138
```
```   139 lemma "VARS H x y z w
```
```   140  {[x\<mapsto>y] ** [z\<mapsto>w]}
```
```   141  y := w
```
```   142  {x \<noteq> z}"
```
```   143 apply vcg
```
```   144 apply(auto simp:star_def ortho_def singl_def)
```
```   145 done
```
```   146
```
```   147 lemma "VARS H x y z w
```
```   148  {emp ** emp}
```
```   149  SKIP
```
```   150  {emp}"
```
```   151 apply vcg
```
```   152 apply(auto simp:star_def ortho_def is_empty_def)
```
```   153 done
```
```   154
```
```   155 text{* So far we have unfolded the separation logic connectives in
```
```   156 proofs. Here comes a simple example of a program proof that uses a law
```
```   157 of separation logic instead. *}
```
```   158
```
```   159 (* a law of separation logic *)
```
```   160 lemma star_comm: "P ** Q = Q ** P"
```
```   161   by(auto simp add:star_def ortho_def dest: map_add_comm)
```
```   162
```
```   163 lemma "VARS H x y z w
```
```   164  {P ** Q}
```
```   165  SKIP
```
```   166  {Q ** P}"
```
```   167 apply vcg
```
```   168 apply(simp add: star_comm)
```
```   169 done
```
```   170
```
```   171
```
```   172 lemma "VARS H
```
```   173  {p\<noteq>0 \<and> [p \<mapsto> x] ** List H q qs}
```
```   174  H := H(p \<mapsto> q)
```
```   175  {List H p (p#qs)}"
```
```   176 apply vcg
```
```   177 apply(simp add: star_def ortho_def singl_def)
```
```   178 apply clarify
```
```   179 apply(subgoal_tac "p \<notin> set qs")
```
```   180  prefer 2
```
```   181  apply(blast dest:list_in_heap)
```
```   182 apply simp
```
```   183 done
```
```   184
```
```   185 lemma "VARS H p q r
```
```   186   {List H p Ps ** List H q Qs}
```
```   187   WHILE p \<noteq> 0
```
```   188   INV {\<exists>ps qs. (List H p ps ** List H q qs) \<and> rev ps @ qs = rev Ps @ Qs}
```
```   189   DO r := p; p := the(H p); H := H(r \<mapsto> q); q := r OD
```
```   190   {List H q (rev Ps @ Qs)}"
```
```   191 apply vcg
```
```   192 apply(simp_all add: star_def ortho_def singl_def)
```
```   193
```
```   194 apply fastforce
```
```   195
```
```   196 apply (clarsimp simp add:List_non_null)
```
```   197 apply(rename_tac ps')
```
```   198 apply(rule_tac x = ps' in exI)
```
```   199 apply(rule_tac x = "p#qs" in exI)
```
```   200 apply simp
```
```   201 apply(rule_tac x = "h1(p:=None)" in exI)
```
```   202 apply(rule_tac x = "h2(p\<mapsto>q)" in exI)
```
```   203 apply simp
```
```   204 apply(rule conjI)
```
```   205  apply(rule ext)
```
```   206  apply(simp add:map_add_def split:option.split)
```
```   207 apply(rule conjI)
```
```   208  apply blast
```
```   209 apply(simp add:map_add_def split:option.split)
```
```   210 apply(rule conjI)
```
```   211 apply(subgoal_tac "p \<notin> set qs")
```
```   212  prefer 2
```
```   213  apply(blast dest:list_in_heap)
```
```   214 apply(simp)
```
```   215 apply fast
```
```   216
```
```   217 apply(fastforce)
```
```   218 done
```
```   219
```
```   220 end
```