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