|
8177
|
1 |
(* Title: HOL/IMPP/Natural.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
|
|
|
4 |
Copyright 1999 TUM
|
|
|
5 |
|
|
|
6 |
Natural semantics of commands
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Natural = Com +
|
|
|
10 |
|
|
|
11 |
(** Execution of commands **)
|
|
|
12 |
consts evalc :: "(com * state * state) set"
|
|
|
13 |
"@evalc":: [com,state, state] => bool ("<_,_>/ -c-> _" [0,0, 51] 51)
|
|
|
14 |
evaln :: "(com * state * nat * state) set"
|
|
|
15 |
"@evaln":: [com,state,nat,state] => bool ("<_,_>/ -_-> _" [0,0,0,51] 51)
|
|
|
16 |
|
|
|
17 |
translations "<c,s> -c-> s'" == "(c,s, s') : evalc"
|
|
|
18 |
"<c,s> -n-> s'" == "(c,s,n,s') : evaln"
|
|
|
19 |
|
|
|
20 |
consts
|
|
|
21 |
newlocs :: locals
|
|
|
22 |
setlocs :: state => locals => state
|
|
|
23 |
getlocs :: state => locals
|
|
|
24 |
update :: state => vname => val => state ("_/[_/::=/_]" [900,0,0] 900)
|
|
|
25 |
syntax (* IN Natural.thy *)
|
|
|
26 |
loc :: state => locals ("_<_>" [75,0] 75)
|
|
|
27 |
translations
|
|
|
28 |
"s<X>" == "getlocs s X"
|
|
|
29 |
|
|
|
30 |
inductive evalc
|
|
|
31 |
intrs
|
|
|
32 |
Skip "<SKIP,s> -c-> s"
|
|
|
33 |
|
|
|
34 |
Assign "<X :== a,s> -c-> s[X::=a s]"
|
|
|
35 |
|
|
|
36 |
Local "<c, s0[Loc Y::= a s0]> -c-> s1 ==>
|
|
|
37 |
<LOCAL Y := a IN c, s0> -c-> s1[Loc Y::=s0<Y>]"
|
|
|
38 |
|
|
|
39 |
Semi "[| <c0,s0> -c-> s1; <c1,s1> -c-> s2 |] ==>
|
|
|
40 |
<c0;; c1, s0> -c-> s2"
|
|
|
41 |
|
|
|
42 |
IfTrue "[| b s; <c0,s> -c-> s1 |] ==>
|
|
|
43 |
<IF b THEN c0 ELSE c1, s> -c-> s1"
|
|
|
44 |
|
|
|
45 |
IfFalse "[| ~b s; <c1,s> -c-> s1 |] ==>
|
|
|
46 |
<IF b THEN c0 ELSE c1, s> -c-> s1"
|
|
|
47 |
|
|
|
48 |
WhileFalse "~b s ==> <WHILE b DO c,s> -c-> s"
|
|
|
49 |
|
|
|
50 |
WhileTrue "[| b s0; <c,s0> -c-> s1; <WHILE b DO c, s1> -c-> s2 |] ==>
|
|
|
51 |
<WHILE b DO c, s0> -c-> s2"
|
|
|
52 |
|
|
|
53 |
Body "<the (body pn), s0> -c-> s1 ==>
|
|
|
54 |
<BODY pn, s0> -c-> s1"
|
|
|
55 |
|
|
|
56 |
Call "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -c-> s1 ==>
|
|
|
57 |
<X:=CALL pn(a), s0> -c-> (setlocs s1 (getlocs s0))
|
|
|
58 |
[X::=s1<Res>]"
|
|
|
59 |
|
|
|
60 |
inductive evaln
|
|
|
61 |
intrs
|
|
|
62 |
Skip "<SKIP,s> -n-> s"
|
|
|
63 |
|
|
|
64 |
Assign "<X :== a,s> -n-> s[X::=a s]"
|
|
|
65 |
|
|
|
66 |
Local "<c, s0[Loc Y::= a s0]> -n-> s1 ==>
|
|
|
67 |
<LOCAL Y := a IN c, s0> -n-> s1[Loc Y::=s0<Y>]"
|
|
|
68 |
|
|
|
69 |
Semi "[| <c0,s0> -n-> s1; <c1,s1> -n-> s2 |] ==>
|
|
|
70 |
<c0;; c1, s0> -n-> s2"
|
|
|
71 |
|
|
|
72 |
IfTrue "[| b s; <c0,s> -n-> s1 |] ==>
|
|
|
73 |
<IF b THEN c0 ELSE c1, s> -n-> s1"
|
|
|
74 |
|
|
|
75 |
IfFalse "[| ~b s; <c1,s> -n-> s1 |] ==>
|
|
|
76 |
<IF b THEN c0 ELSE c1, s> -n-> s1"
|
|
|
77 |
|
|
|
78 |
WhileFalse "~b s ==> <WHILE b DO c,s> -n-> s"
|
|
|
79 |
|
|
|
80 |
WhileTrue "[| b s0; <c,s0> -n-> s1; <WHILE b DO c, s1> -n-> s2 |] ==>
|
|
|
81 |
<WHILE b DO c, s0> -n-> s2"
|
|
|
82 |
|
|
|
83 |
Body "<the (body pn), s0> - n-> s1 ==>
|
|
|
84 |
<BODY pn, s0> -Suc n-> s1"
|
|
|
85 |
|
|
|
86 |
Call "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -n-> s1 ==>
|
|
|
87 |
<X:=CALL pn(a), s0> -n-> (setlocs s1 (getlocs s0))
|
|
|
88 |
[X::=s1<Res>]"
|
|
|
89 |
end
|