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