src/HOL/Hoare/HeapSyntax.thy
author nipkow
Sun Mar 23 11:57:07 2003 +0100 (2003-03-23)
changeset 13875 12997e3ddd8d
child 16417 9bc16273c2d4
permissions -rw-r--r--
*** empty log message ***
     1 (*  Title:      HOL/Hoare/HeapSyntax.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   2002 TUM
     5 *)
     6 
     7 theory HeapSyntax = Hoare + Heap:
     8 
     9 subsection "Field access and update"
    10 
    11 syntax
    12   "@refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
    13    ("_/'((_ \<rightarrow> _)')" [1000,0] 900)
    14   "@fassign"  :: "'a ref => id => 'v => 's com"
    15    ("(2_^._ :=/ _)" [70,1000,65] 61)
    16   "@faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
    17    ("_^._" [65,1000] 65)
    18 translations
    19   "f(r \<rightarrow> v)"  ==  "f(addr r := v)"
    20   "p^.f := e"  =>  "f := f(p \<rightarrow> e)"
    21   "p^.f"       =>  "f(addr p)"
    22 
    23 
    24 declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]
    25 
    26 
    27 text "An example due to Suzuki:"
    28 
    29 lemma "VARS v n
    30   {w = Ref w0 & x = Ref x0 & y = Ref y0 & z = Ref z0 &
    31    distinct[w0,x0,y0,z0]}
    32   w^.v := (1::int); w^.n := x;
    33   x^.v := 2; x^.n := y;
    34   y^.v := 3; y^.n := z;
    35   z^.v := 4; x^.n := z
    36   {w^.n^.n^.v = 4}"
    37 by vcg_simp
    38 
    39 end