src/HOL/Hoare/HeapSyntax.thy
changeset 13875 12997e3ddd8d
child 16417 9bc16273c2d4
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Hoare/HeapSyntax.thy	Sun Mar 23 11:57:07 2003 +0100
     1.3 @@ -0,0 +1,39 @@
     1.4 +(*  Title:      HOL/Hoare/HeapSyntax.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow
     1.7 +    Copyright   2002 TUM
     1.8 +*)
     1.9 +
    1.10 +theory HeapSyntax = Hoare + Heap:
    1.11 +
    1.12 +subsection "Field access and update"
    1.13 +
    1.14 +syntax
    1.15 +  "@refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
    1.16 +   ("_/'((_ \<rightarrow> _)')" [1000,0] 900)
    1.17 +  "@fassign"  :: "'a ref => id => 'v => 's com"
    1.18 +   ("(2_^._ :=/ _)" [70,1000,65] 61)
    1.19 +  "@faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
    1.20 +   ("_^._" [65,1000] 65)
    1.21 +translations
    1.22 +  "f(r \<rightarrow> v)"  ==  "f(addr r := v)"
    1.23 +  "p^.f := e"  =>  "f := f(p \<rightarrow> e)"
    1.24 +  "p^.f"       =>  "f(addr p)"
    1.25 +
    1.26 +
    1.27 +declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]
    1.28 +
    1.29 +
    1.30 +text "An example due to Suzuki:"
    1.31 +
    1.32 +lemma "VARS v n
    1.33 +  {w = Ref w0 & x = Ref x0 & y = Ref y0 & z = Ref z0 &
    1.34 +   distinct[w0,x0,y0,z0]}
    1.35 +  w^.v := (1::int); w^.n := x;
    1.36 +  x^.v := 2; x^.n := y;
    1.37 +  y^.v := 3; y^.n := z;
    1.38 +  z^.v := 4; x^.n := z
    1.39 +  {w^.n^.n^.v = 4}"
    1.40 +by vcg_simp
    1.41 +
    1.42 +end