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