equal
deleted
inserted
replaced
1 (* Title: HOL/Hoare/Pointers.thy |
1 (* Title: HOL/Hoare/Pointers.thy |
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
2 Author: Tobias Nipkow |
4 Copyright 2002 TUM |
3 Copyright 2002 TUM |
5 |
4 |
6 This is like Pointers.thy, but instead of a type constructor 'a ref |
5 This is like Pointers.thy, but instead of a type constructor 'a ref |
7 that adjoins Null to a type, Null is simply a distinguished element of |
6 that adjoins Null to a type, Null is simply a distinguished element of |
18 consts Null :: "'a::ref" |
17 consts Null :: "'a::ref" |
19 |
18 |
20 subsection "Field access and update" |
19 subsection "Field access and update" |
21 |
20 |
22 syntax |
21 syntax |
23 "@fassign" :: "'a::ref => id => 'v => 's com" |
22 "_fassign" :: "'a::ref => id => 'v => 's com" |
24 ("(2_^._ :=/ _)" [70,1000,65] 61) |
23 ("(2_^._ :=/ _)" [70,1000,65] 61) |
25 "@faccess" :: "'a::ref => ('a::ref \<Rightarrow> 'v) => 'v" |
24 "_faccess" :: "'a::ref => ('a::ref \<Rightarrow> 'v) => 'v" |
26 ("_^._" [65,1000] 65) |
25 ("_^._" [65,1000] 65) |
27 translations |
26 translations |
28 "p^.f := e" => "f := fun_upd f p e" |
27 "p^.f := e" => "f := CONST fun_upd f p e" |
29 "p^.f" => "f p" |
28 "p^.f" => "f p" |
30 |
29 |
31 |
30 |
32 text "An example due to Suzuki:" |
31 text "An example due to Suzuki:" |
33 |
32 |