|
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 |