equal
deleted
inserted
replaced
1 (* Title: HOL/Hoare/HeapSyntax.thy |
1 (* Title: HOL/Hoare/HeapSyntax.thy |
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
2 Author: Tobias Nipkow |
4 Copyright 2002 TUM |
3 Copyright 2002 TUM |
5 *) |
4 *) |
6 |
5 |
7 theory HeapSyntax imports Hoare Heap begin |
6 theory HeapSyntax imports Hoare Heap begin |
8 |
7 |
9 subsection "Field access and update" |
8 subsection "Field access and update" |
10 |
9 |
11 syntax |
10 syntax |
12 "@refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" |
11 "_refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" |
13 ("_/'((_ \<rightarrow> _)')" [1000,0] 900) |
12 ("_/'((_ \<rightarrow> _)')" [1000,0] 900) |
14 "@fassign" :: "'a ref => id => 'v => 's com" |
13 "_fassign" :: "'a ref => id => 'v => 's com" |
15 ("(2_^._ :=/ _)" [70,1000,65] 61) |
14 ("(2_^._ :=/ _)" [70,1000,65] 61) |
16 "@faccess" :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v" |
15 "_faccess" :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v" |
17 ("_^._" [65,1000] 65) |
16 ("_^._" [65,1000] 65) |
18 translations |
17 translations |
19 "f(r \<rightarrow> v)" == "f(addr r := v)" |
18 "f(r \<rightarrow> v)" == "f(CONST addr r := v)" |
20 "p^.f := e" => "f := f(p \<rightarrow> e)" |
19 "p^.f := e" => "f := f(p \<rightarrow> e)" |
21 "p^.f" => "f(addr p)" |
20 "p^.f" => "f(CONST addr p)" |
22 |
21 |
23 |
22 |
24 declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp] |
23 declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp] |
25 |
24 |
26 |
25 |