|
8177
|
1 |
(* Title: HOL/IMPP/Misc.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: David von Oheimb
|
|
|
4 |
Copyright 1999 TUM
|
|
17477
|
5 |
*)
|
|
8177
|
6 |
|
|
17477
|
7 |
header {* Several examples for Hoare logic *}
|
|
|
8 |
|
|
|
9 |
theory Misc
|
|
|
10 |
imports Hoare
|
|
|
11 |
begin
|
|
8177
|
12 |
|
|
|
13 |
defs
|
|
17477
|
14 |
newlocs_def: "newlocs == %x. arbitrary"
|
|
|
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"
|
|
|
17 |
update_def: "update s vn v == case vn of
|
|
|
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)))"
|
|
|
20 |
|
|
|
21 |
ML {* use_legacy_bindings (the_context ()) *}
|
|
8177
|
22 |
|
|
|
23 |
end
|