equal
deleted
inserted
replaced
9 theory Misc |
9 theory Misc |
10 imports Hoare |
10 imports Hoare |
11 begin |
11 begin |
12 |
12 |
13 defs |
13 defs |
14 newlocs_def: "newlocs == %x. arbitrary" |
14 newlocs_def: "newlocs == %x. undefined" |
15 setlocs_def: "setlocs s l' == case s of st g l => st g l'" |
15 setlocs_def: "setlocs s l' == case s of st g l => st g l'" |
16 getlocs_def: "getlocs s == case s of st g l => l" |
16 getlocs_def: "getlocs s == case s of st g l => l" |
17 update_def: "update s vn v == case vn of |
17 update_def: "update s vn v == case vn of |
18 Glb gn => (case s of st g l => st (g(gn:=v)) l) |
18 Glb gn => (case s of st g l => st (g(gn:=v)) l) |
19 | Loc ln => (case s of st g l => st g (l(ln:=v)))" |
19 | Loc ln => (case s of st g l => st g (l(ln:=v)))" |