src/HOL/Hoare/Separation.thy
author nipkow
Tue Mar 11 15:04:24 2003 +0100 (2003-03-11)
changeset 13857 11d7c5a8dbb7
child 13867 1fdecd15437f
permissions -rw-r--r--
*** empty log message ***
nipkow@13857
     1
theory Separation = HoareAbort:
nipkow@13857
     2
nipkow@13857
     3
types heap = "(nat \<Rightarrow> nat option)"
nipkow@13857
     4
nipkow@13857
     5
nipkow@13857
     6
text{* The semantic definition of a few connectives: *}
nipkow@13857
     7
nipkow@13857
     8
constdefs
nipkow@13857
     9
 R:: "heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> bool"
nipkow@13857
    10
"R h h1 h2 == dom h1 \<inter> dom h2 = {} \<and> h = h1 ++ h2"
nipkow@13857
    11
nipkow@13857
    12
 star:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)"
nipkow@13857
    13
"star P Q == \<lambda>h. \<exists>h1 h2. R h h1 h2 \<and> P h1 \<and> Q h2"
nipkow@13857
    14
nipkow@13857
    15
 singl:: "heap \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
nipkow@13857
    16
"singl h x y == dom h = {x} & h x = Some y"
nipkow@13857
    17
nipkow@13857
    18
lemma "VARS x y z w h
nipkow@13857
    19
 {star (%h. singl h x y) (%h. singl h z w) h}
nipkow@13857
    20
 SKIP
nipkow@13857
    21
 {x \<noteq> z}"
nipkow@13857
    22
apply vcg
nipkow@13857
    23
apply(auto simp:star_def R_def singl_def)
nipkow@13857
    24
done
nipkow@13857
    25
nipkow@13857
    26
text{* To suppress the heap parameter of the connectives, we assume it
nipkow@13857
    27
is always called H and add/remove it upon parsing/printing. Thus
nipkow@13857
    28
every pointer program needs to have a program variable H, and
nipkow@13857
    29
assertions should not contain any locally bound Hs - otherwise they
nipkow@13857
    30
may bind the implicit H. *}
nipkow@13857
    31
nipkow@13857
    32
text{* Nice input syntax: *}
nipkow@13857
    33
nipkow@13857
    34
syntax
nipkow@13857
    35
 "@singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" ("[_ \<mapsto> _]")
nipkow@13857
    36
 "@star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60)
nipkow@13857
    37
nipkow@13857
    38
ML{*
nipkow@13857
    39
fun singl_tr [p,q] = Syntax.const "singl" $ Syntax.free "H" $ p $ q
nipkow@13857
    40
  | singl_tr ts = raise TERM ("singl_tr", ts);
nipkow@13857
    41
fun star_tr [P,Q] = Syntax.const "star" $
nipkow@13857
    42
      absfree("H",dummyT,P) $ absfree("H",dummyT,Q) $ Syntax.free "H"
nipkow@13857
    43
  | star_tr ts = raise TERM ("star_tr", ts);
nipkow@13857
    44
*}
nipkow@13857
    45
nipkow@13857
    46
parse_translation {* [("@singl", singl_tr),("@star", star_tr)] *}
nipkow@13857
    47
nipkow@13857
    48
lemma "VARS H x y z w
nipkow@13857
    49
 {[x\<mapsto>y] ** [z\<mapsto>w]}
nipkow@13857
    50
 SKIP
nipkow@13857
    51
 {x \<noteq> z}"
nipkow@13857
    52
apply vcg
nipkow@13857
    53
apply(auto simp:star_def R_def singl_def)
nipkow@13857
    54
done
nipkow@13857
    55
nipkow@13857
    56
text{* Nice output syntax: *}
nipkow@13857
    57
nipkow@13857
    58
ML{*
nipkow@13857
    59
fun singl_tr' [_,p,q] = Syntax.const "@singl" $ p $ q
nipkow@13857
    60
fun star_tr' [Abs(_,_,P),Abs(_,_,Q),_] = Syntax.const "@star" $ P $ Q
nipkow@13857
    61
*}
nipkow@13857
    62
nipkow@13857
    63
print_translation {* [("singl", singl_tr'),("star", star_tr')] *}
nipkow@13857
    64
nipkow@13857
    65
lemma "VARS H x y z w
nipkow@13857
    66
 {[x\<mapsto>y] ** [z\<mapsto>w]}
nipkow@13857
    67
 SKIP
nipkow@13857
    68
 {x \<noteq> z}"
nipkow@13857
    69
apply vcg
nipkow@13857
    70
apply(auto simp:star_def R_def singl_def)
nipkow@13857
    71
done
nipkow@13857
    72
nipkow@13857
    73
nipkow@13857
    74
consts llist :: "(heap * nat)set"
nipkow@13857
    75
inductive llist
nipkow@13857
    76
intros
nipkow@13857
    77
empty: "(%n. None, 0) : llist"
nipkow@13857
    78
cons: "\<lbrakk> R h h1 h2; pto h1 p q; (h2,q):llist \<rbrakk> \<Longrightarrow> (h,p):llist"
nipkow@13857
    79
nipkow@13857
    80
lemma "VARS p q h
nipkow@13857
    81
 {(h,p) : llist}
nipkow@13857
    82
 h := h(q \<mapsto> p)
nipkow@13857
    83
 {(h,q) : llist}"
nipkow@13857
    84
apply vcg
nipkow@13857
    85
apply(rule_tac "h1.0" = "%n. if n=q then Some p else None" in llist.cons)
nipkow@13857
    86
prefer 3 apply assumption
nipkow@13857
    87
prefer 2 apply(simp add:singl_def dom_def)
nipkow@13857
    88
apply(simp add:R_def dom_def)
nipkow@13857
    89
nipkow@13857
    90