equal
deleted
inserted
replaced
6 |
6 |
7 theory Misc |
7 theory Misc |
8 imports Hoare |
8 imports Hoare |
9 begin |
9 begin |
10 |
10 |
11 defs |
11 overloading |
12 newlocs_def: "newlocs == %x. undefined" |
12 newlocs \<equiv> newlocs |
13 setlocs_def: "setlocs s l' == case s of st g l => st g l'" |
13 setlocs \<equiv> setlocs |
14 getlocs_def: "getlocs s == case s of st g l => l" |
14 getlocs \<equiv> getlocs |
15 update_def: "update s vn v == case vn of |
15 update \<equiv> update |
16 Glb gn => (case s of st g l => st (g(gn:=v)) l) |
16 begin |
17 | Loc ln => (case s of st g l => st g (l(ln:=v)))" |
17 |
|
18 definition newlocs :: locals |
|
19 where "newlocs == %x. undefined" |
|
20 |
|
21 definition setlocs :: "state => locals => state" |
|
22 where "setlocs s l' == case s of st g l => st g l'" |
|
23 |
|
24 definition getlocs :: "state => locals" |
|
25 where "getlocs s == case s of st g l => l" |
|
26 |
|
27 definition update :: "state => vname => val => state" |
|
28 where "update s vn v == |
|
29 case vn of |
|
30 Glb gn => (case s of st g l => st (g(gn:=v)) l) |
|
31 | Loc ln => (case s of st g l => st g (l(ln:=v)))" |
|
32 |
|
33 end |
18 |
34 |
19 |
35 |
20 subsection "state access" |
36 subsection "state access" |
21 |
37 |
22 lemma getlocs_def2: "getlocs (st g l) = l" |
38 lemma getlocs_def2: "getlocs (st g l) = l" |