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