author | nipkow |
Tue, 09 Jan 2001 15:32:27 +0100 | |
changeset 10834 | a7897aebbffc |
parent 8177 | e59e93ad85eb |
child 17477 | ceb42ea2f223 |
permissions | -rw-r--r-- |
8177 | 1 |
(* Title: HOL/IMPP/Misc.thy |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb |
|
4 |
Copyright 1999 TUM |
|
5 |
||
6 |
Several examples for Hoare logic |
|
7 |
*) |
|
8 |
Misc = Hoare + |
|
9 |
||
10 |
defs |
|
11 |
newlocs_def "newlocs == %x. arbitrary" |
|
12 |
setlocs_def "setlocs s l' == case s of st g l => st g l'" |
|
13 |
getlocs_def "getlocs s == case s of st g l => l" |
|
14 |
update_def "update s vn v == case vn of |
|
15 |
Glb gn => (case s of st g l => st (g(gn:=v)) l) |
|
16 |
| Loc ln => (case s of st g l => st g (l(ln:=v)))" |
|
17 |
||
18 |
end |
|
19 |