src/HOL/Hoare/HeapSyntaxAbort.thy
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 13875 12997e3ddd8d
child 16417 9bc16273c2d4
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
     1 (*  Title:      HOL/Hoare/HeapSyntax.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   2002 TUM
     5 *)
     6 
     7 theory HeapSyntaxAbort = HoareAbort + Heap:
     8 
     9 subsection "Field access and update"
    10 
    11 text{* Heap update @{text"p^.h := e"} is now guarded against @{term p}
    12 being Null. However, @{term p} may still be illegal,
    13 e.g. uninitialized or dangling. To guard against that, one needs a
    14 more detailed model of the heap where allocated and free addresses are
    15 distinguished, e.g. by making the heap a map, or by carrying the set
    16 of free addresses around. This is needed anyway as soon as we want to
    17 reason about storage allocation/deallocation. *}
    18 
    19 syntax
    20   "refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
    21    ("_/'((_ \<rightarrow> _)')" [1000,0] 900)
    22   "@fassign"  :: "'a ref => id => 'v => 's com"
    23    ("(2_^._ :=/ _)" [70,1000,65] 61)
    24   "@faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
    25    ("_^._" [65,1000] 65)
    26 translations
    27   "refupdate f r v"  ==  "f(addr r := v)"
    28   "p^.f := e"  =>  "(p \<noteq> Null) \<rightarrow> (f := refupdate f p e)"
    29   "p^.f"       =>  "f(addr p)"
    30 
    31 
    32 declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]
    33 
    34 
    35 text "An example due to Suzuki:"
    36 
    37 lemma "VARS v n
    38   {w = Ref w0 & x = Ref x0 & y = Ref y0 & z = Ref z0 &
    39    distinct[w0,x0,y0,z0]}
    40   w^.v := (1::int); w^.n := x;
    41   x^.v := 2; x^.n := y;
    42   y^.v := 3; y^.n := z;
    43   z^.v := 4; x^.n := z
    44   {w^.n^.n^.v = 4}"
    45 by vcg_simp
    46 
    47 end