31 syntax (* IN Natural.thy *) |
20 syntax (* IN Natural.thy *) |
32 loc :: "state => locals" ("_<_>" [75,0] 75) |
21 loc :: "state => locals" ("_<_>" [75,0] 75) |
33 translations |
22 translations |
34 "s<X>" == "getlocs s X" |
23 "s<X>" == "getlocs s X" |
35 |
24 |
36 inductive evalc |
25 inductive |
37 intros |
26 evalc :: "[com,state, state] => bool" ("<_,_>/ -c-> _" [0,0, 51] 51) |
|
27 where |
38 Skip: "<SKIP,s> -c-> s" |
28 Skip: "<SKIP,s> -c-> s" |
39 |
29 |
40 Assign: "<X :== a,s> -c-> s[X::=a s]" |
30 | Assign: "<X :== a,s> -c-> s[X::=a s]" |
41 |
31 |
42 Local: "<c, s0[Loc Y::= a s0]> -c-> s1 ==> |
32 | Local: "<c, s0[Loc Y::= a s0]> -c-> s1 ==> |
43 <LOCAL Y := a IN c, s0> -c-> s1[Loc Y::=s0<Y>]" |
33 <LOCAL Y := a IN c, s0> -c-> s1[Loc Y::=s0<Y>]" |
44 |
34 |
45 Semi: "[| <c0,s0> -c-> s1; <c1,s1> -c-> s2 |] ==> |
35 | Semi: "[| <c0,s0> -c-> s1; <c1,s1> -c-> s2 |] ==> |
46 <c0;; c1, s0> -c-> s2" |
36 <c0;; c1, s0> -c-> s2" |
47 |
37 |
48 IfTrue: "[| b s; <c0,s> -c-> s1 |] ==> |
38 | IfTrue: "[| b s; <c0,s> -c-> s1 |] ==> |
49 <IF b THEN c0 ELSE c1, s> -c-> s1" |
39 <IF b THEN c0 ELSE c1, s> -c-> s1" |
50 |
40 |
51 IfFalse: "[| ~b s; <c1,s> -c-> s1 |] ==> |
41 | IfFalse: "[| ~b s; <c1,s> -c-> s1 |] ==> |
52 <IF b THEN c0 ELSE c1, s> -c-> s1" |
42 <IF b THEN c0 ELSE c1, s> -c-> s1" |
53 |
43 |
54 WhileFalse: "~b s ==> <WHILE b DO c,s> -c-> s" |
44 | WhileFalse: "~b s ==> <WHILE b DO c,s> -c-> s" |
55 |
45 |
56 WhileTrue: "[| b s0; <c,s0> -c-> s1; <WHILE b DO c, s1> -c-> s2 |] ==> |
46 | WhileTrue: "[| b s0; <c,s0> -c-> s1; <WHILE b DO c, s1> -c-> s2 |] ==> |
57 <WHILE b DO c, s0> -c-> s2" |
47 <WHILE b DO c, s0> -c-> s2" |
58 |
48 |
59 Body: "<the (body pn), s0> -c-> s1 ==> |
49 | Body: "<the (body pn), s0> -c-> s1 ==> |
60 <BODY pn, s0> -c-> s1" |
50 <BODY pn, s0> -c-> s1" |
61 |
51 |
62 Call: "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -c-> s1 ==> |
52 | Call: "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -c-> s1 ==> |
63 <X:=CALL pn(a), s0> -c-> (setlocs s1 (getlocs s0)) |
53 <X:=CALL pn(a), s0> -c-> (setlocs s1 (getlocs s0)) |
64 [X::=s1<Res>]" |
54 [X::=s1<Res>]" |
65 |
55 |
66 inductive evaln |
56 inductive |
67 intros |
57 evaln :: "[com,state,nat,state] => bool" ("<_,_>/ -_-> _" [0,0,0,51] 51) |
|
58 where |
68 Skip: "<SKIP,s> -n-> s" |
59 Skip: "<SKIP,s> -n-> s" |
69 |
60 |
70 Assign: "<X :== a,s> -n-> s[X::=a s]" |
61 | Assign: "<X :== a,s> -n-> s[X::=a s]" |
71 |
62 |
72 Local: "<c, s0[Loc Y::= a s0]> -n-> s1 ==> |
63 | Local: "<c, s0[Loc Y::= a s0]> -n-> s1 ==> |
73 <LOCAL Y := a IN c, s0> -n-> s1[Loc Y::=s0<Y>]" |
64 <LOCAL Y := a IN c, s0> -n-> s1[Loc Y::=s0<Y>]" |
74 |
65 |
75 Semi: "[| <c0,s0> -n-> s1; <c1,s1> -n-> s2 |] ==> |
66 | Semi: "[| <c0,s0> -n-> s1; <c1,s1> -n-> s2 |] ==> |
76 <c0;; c1, s0> -n-> s2" |
67 <c0;; c1, s0> -n-> s2" |
77 |
68 |
78 IfTrue: "[| b s; <c0,s> -n-> s1 |] ==> |
69 | IfTrue: "[| b s; <c0,s> -n-> s1 |] ==> |
79 <IF b THEN c0 ELSE c1, s> -n-> s1" |
70 <IF b THEN c0 ELSE c1, s> -n-> s1" |
80 |
71 |
81 IfFalse: "[| ~b s; <c1,s> -n-> s1 |] ==> |
72 | IfFalse: "[| ~b s; <c1,s> -n-> s1 |] ==> |
82 <IF b THEN c0 ELSE c1, s> -n-> s1" |
73 <IF b THEN c0 ELSE c1, s> -n-> s1" |
83 |
74 |
84 WhileFalse: "~b s ==> <WHILE b DO c,s> -n-> s" |
75 | WhileFalse: "~b s ==> <WHILE b DO c,s> -n-> s" |
85 |
76 |
86 WhileTrue: "[| b s0; <c,s0> -n-> s1; <WHILE b DO c, s1> -n-> s2 |] ==> |
77 | WhileTrue: "[| b s0; <c,s0> -n-> s1; <WHILE b DO c, s1> -n-> s2 |] ==> |
87 <WHILE b DO c, s0> -n-> s2" |
78 <WHILE b DO c, s0> -n-> s2" |
88 |
79 |
89 Body: "<the (body pn), s0> - n-> s1 ==> |
80 | Body: "<the (body pn), s0> - n-> s1 ==> |
90 <BODY pn, s0> -Suc n-> s1" |
81 <BODY pn, s0> -Suc n-> s1" |
91 |
82 |
92 Call: "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -n-> s1 ==> |
83 | Call: "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -n-> s1 ==> |
93 <X:=CALL pn(a), s0> -n-> (setlocs s1 (getlocs s0)) |
84 <X:=CALL pn(a), s0> -n-> (setlocs s1 (getlocs s0)) |
94 [X::=s1<Res>]" |
85 [X::=s1<Res>]" |
95 |
86 |
96 |
87 |
97 inductive_cases evalc_elim_cases: |
88 inductive_cases evalc_elim_cases: |