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