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