src/HOL/Hoare/Separation.thy
author nipkow
Thu Jun 26 18:14:04 2003 +0200 (2003-06-26)
changeset 14074 93dfce3b6f86
parent 14028 ff6eb32b30a1
child 16417 9bc16273c2d4
permissions -rw-r--r--
*** empty log message ***
     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 Already builds on the theory for list abstractions.
     8 
     9 If we suppress the H parameter for "List", we have to hardwired this
    10 into parser and pretty printer, which is not very modular.
    11 Alternative: some syntax like <P> which stands for P H. No more
    12 compact, but avoids the funny H.
    13 
    14 *)
    15 
    16 theory Separation = HoareAbort + SepLogHeap:
    17 
    18 text{* The semantic definition of a few connectives: *}
    19 
    20 constdefs
    21  ortho:: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix "\<bottom>" 55)
    22 "h1 \<bottom> h2 == dom h1 \<inter> dom h2 = {}"
    23 
    24  is_empty :: "heap \<Rightarrow> bool"
    25 "is_empty h == h = empty"
    26 
    27  singl:: "heap \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
    28 "singl h x y == dom h = {x} & h x = Some y"
    29 
    30  star:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)"
    31 "star P Q == \<lambda>h. \<exists>h1 h2. h = h1++h2 \<and> h1 \<bottom> h2 \<and> P h1 \<and> Q h2"
    32 
    33  wand:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)"
    34 "wand P Q == \<lambda>h. \<forall>h'. h' \<bottom> h \<and> P h' \<longrightarrow> Q(h++h')"
    35 
    36 text{*This is what assertions look like without any syntactic sugar: *}
    37 
    38 lemma "VARS x y z w h
    39  {star (%h. singl h x y) (%h. singl h z w) h}
    40  SKIP
    41  {x \<noteq> z}"
    42 apply vcg
    43 apply(auto simp:star_def ortho_def singl_def)
    44 done
    45 
    46 text{* Now we add nice input syntax.  To suppress the heap parameter
    47 of the connectives, we assume it is always called H and add/remove it
    48 upon parsing/printing. Thus every pointer program needs to have a
    49 program variable H, and assertions should not contain any locally
    50 bound Hs - otherwise they may bind the implicit H. *}
    51 
    52 syntax
    53  "@emp" :: "bool" ("emp")
    54  "@singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" ("[_ \<mapsto> _]")
    55  "@star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60)
    56  "@wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "-*" 60)
    57 
    58 ML{*
    59 (* free_tr takes care of free vars in the scope of sep. logic connectives:
    60    they are implicitly applied to the heap *)
    61 fun free_tr(t as Free _) = t $ Syntax.free "H"
    62 (*
    63   | free_tr((list as Free("List",_))$ p $ ps) = list $ Syntax.free "H" $ p $ ps
    64 *)
    65   | free_tr t = t
    66 
    67 fun emp_tr [] = Syntax.const "is_empty" $ Syntax.free "H"
    68   | emp_tr ts = raise TERM ("emp_tr", ts);
    69 fun singl_tr [p,q] = Syntax.const "singl" $ Syntax.free "H" $ p $ q
    70   | singl_tr ts = raise TERM ("singl_tr", ts);
    71 fun star_tr [P,Q] = Syntax.const "star" $
    72       absfree("H",dummyT,free_tr P) $ absfree("H",dummyT,free_tr Q) $
    73       Syntax.free "H"
    74   | star_tr ts = raise TERM ("star_tr", ts);
    75 fun wand_tr [P,Q] = Syntax.const "wand" $
    76       absfree("H",dummyT,P) $ absfree("H",dummyT,Q) $ Syntax.free "H"
    77   | wand_tr ts = raise TERM ("wand_tr", ts);
    78 *}
    79 
    80 parse_translation
    81  {* [("@emp", emp_tr), ("@singl", singl_tr),
    82      ("@star", star_tr), ("@wand", wand_tr)] *}
    83 
    84 text{* Now it looks much better: *}
    85 
    86 lemma "VARS H x y z w
    87  {[x\<mapsto>y] ** [z\<mapsto>w]}
    88  SKIP
    89  {x \<noteq> z}"
    90 apply vcg
    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)
   100 done
   101 
   102 text{* But the output is still unreadable. Thus we also strip the heap
   103 parameters upon output: *}
   104 
   105 (* debugging code:
   106 fun sot(Free(s,_)) = s
   107   | sot(Var((s,i),_)) = "?" ^ s ^ string_of_int i
   108   | sot(Const(s,_)) = s
   109   | sot(Bound i) = "B." ^ string_of_int i
   110   | sot(s $ t) = "(" ^ sot s ^ " " ^ sot t ^ ")"
   111   | sot(Abs(_,_,t)) = "(% " ^ sot t ^ ")";
   112 *)
   113 
   114 ML{*
   115 local
   116 fun strip (Abs(_,_,(t as Const("_free",_) $ Free _) $ Bound 0)) = t
   117   | strip (Abs(_,_,(t as Free _) $ Bound 0)) = t
   118 (*
   119   | strip (Abs(_,_,((list as Const("List",_))$ Bound 0 $ p $ ps))) = list$p$ps
   120 *)
   121   | strip (Abs(_,_,(t as Const("_var",_) $ Var _) $ Bound 0)) = t
   122   | strip (Abs(_,_,P)) = P
   123   | strip (Const("is_empty",_)) = Syntax.const "@emp"
   124   | strip t = t;
   125 in
   126 fun is_empty_tr' [_] = Syntax.const "@emp"
   127 fun singl_tr' [_,p,q] = Syntax.const "@singl" $ p $ q
   128 fun star_tr' [P,Q,_] = Syntax.const "@star" $ strip P $ strip Q
   129 fun wand_tr' [P,Q,_] = Syntax.const "@wand" $ strip P $ strip Q
   130 end
   131 *}
   132 
   133 print_translation
   134  {* [("is_empty", is_empty_tr'),("singl", singl_tr'),
   135      ("star", star_tr'),("wand", wand_tr')] *}
   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 apply(simp add:star_def ortho_def)
   162 apply(blast intro:map_add_comm)
   163 done
   164 
   165 lemma "VARS H x y z w
   166  {P ** Q}
   167  SKIP
   168  {Q ** P}"
   169 apply vcg
   170 apply(simp add: star_comm)
   171 done
   172 
   173 
   174 lemma "VARS H
   175  {p\<noteq>0 \<and> [p \<mapsto> x] ** List H q qs}
   176  H := H(p \<mapsto> q)
   177  {List H p (p#qs)}"
   178 apply vcg
   179 apply(simp add: star_def ortho_def singl_def)
   180 apply clarify
   181 apply(subgoal_tac "p \<notin> set qs")
   182  prefer 2
   183  apply(blast dest:list_in_heap)
   184 apply simp
   185 done
   186 
   187 lemma "VARS H p q r
   188   {List H p Ps ** List H q Qs}
   189   WHILE p \<noteq> 0
   190   INV {\<exists>ps qs. (List H p ps ** List H q qs) \<and> rev ps @ qs = rev Ps @ Qs}
   191   DO r := p; p := the(H p); H := H(r \<mapsto> q); q := r OD
   192   {List H q (rev Ps @ Qs)}"
   193 apply vcg
   194 apply(simp_all add: star_def ortho_def singl_def)
   195 
   196 apply fastsimp
   197 
   198 apply (clarsimp simp add:List_non_null)
   199 apply(rename_tac ps')
   200 apply(rule_tac x = ps' in exI)
   201 apply(rule_tac x = "p#qs" in exI)
   202 apply simp
   203 apply(rule_tac x = "h1(p:=None)" in exI)
   204 apply(rule_tac x = "h2(p\<mapsto>q)" in exI)
   205 apply simp
   206 apply(rule conjI)
   207  apply(rule ext)
   208  apply(simp add:map_add_def split:option.split)
   209 apply(rule conjI)
   210  apply blast
   211 apply(simp add:map_add_def split:option.split)
   212 apply(rule conjI)
   213 apply(subgoal_tac "p \<notin> set qs")
   214  prefer 2
   215  apply(blast dest:list_in_heap)
   216 apply(simp)
   217 apply fast
   218 
   219 apply(fastsimp)
   220 done
   221 
   222 end