src/HOL/Hoare/HeapSyntaxAbort.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 35316 870dfea4f9c0
child 41959 b460124855b8
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
nipkow@13875
     1
(*  Title:      HOL/Hoare/HeapSyntax.thy
nipkow@13875
     2
    Author:     Tobias Nipkow
nipkow@13875
     3
    Copyright   2002 TUM
nipkow@13875
     4
*)
nipkow@13875
     5
haftmann@35316
     6
theory HeapSyntaxAbort imports Hoare_Logic_Abort Heap begin
nipkow@13875
     7
nipkow@13875
     8
subsection "Field access and update"
nipkow@13875
     9
nipkow@13875
    10
text{* Heap update @{text"p^.h := e"} is now guarded against @{term p}
nipkow@13875
    11
being Null. However, @{term p} may still be illegal,
nipkow@13875
    12
e.g. uninitialized or dangling. To guard against that, one needs a
nipkow@13875
    13
more detailed model of the heap where allocated and free addresses are
nipkow@13875
    14
distinguished, e.g. by making the heap a map, or by carrying the set
nipkow@13875
    15
of free addresses around. This is needed anyway as soon as we want to
nipkow@13875
    16
reason about storage allocation/deallocation. *}
nipkow@13875
    17
nipkow@13875
    18
syntax
wenzelm@35101
    19
  "_refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
nipkow@13875
    20
   ("_/'((_ \<rightarrow> _)')" [1000,0] 900)
wenzelm@35101
    21
  "_fassign"  :: "'a ref => id => 'v => 's com"
nipkow@13875
    22
   ("(2_^._ :=/ _)" [70,1000,65] 61)
wenzelm@35101
    23
  "_faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
nipkow@13875
    24
   ("_^._" [65,1000] 65)
nipkow@13875
    25
translations
wenzelm@35113
    26
  "_refupdate f r v" == "f(CONST addr r := v)"
wenzelm@35113
    27
  "p^.f := e" => "(p \<noteq> CONST Null) \<rightarrow> (f := _refupdate f p e)"
wenzelm@35113
    28
  "p^.f" => "f(CONST addr p)"
nipkow@13875
    29
nipkow@13875
    30
nipkow@13875
    31
declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]
nipkow@13875
    32
nipkow@13875
    33
nipkow@13875
    34
text "An example due to Suzuki:"
nipkow@13875
    35
nipkow@13875
    36
lemma "VARS v n
nipkow@13875
    37
  {w = Ref w0 & x = Ref x0 & y = Ref y0 & z = Ref z0 &
nipkow@13875
    38
   distinct[w0,x0,y0,z0]}
nipkow@13875
    39
  w^.v := (1::int); w^.n := x;
nipkow@13875
    40
  x^.v := 2; x^.n := y;
nipkow@13875
    41
  y^.v := 3; y^.n := z;
nipkow@13875
    42
  z^.v := 4; x^.n := z
nipkow@13875
    43
  {w^.n^.n^.v = 4}"
nipkow@13875
    44
by vcg_simp
nipkow@13875
    45
nipkow@13875
    46
end