|
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 |
|
|
17477
|
7 |
header {* Natural semantics of commands *}
|
|
|
8 |
|
|
|
9 |
theory Natural
|
|
|
10 |
imports Com
|
|
|
11 |
begin
|
|
8177
|
12 |
|
|
|
13 |
(** Execution of commands **)
|
|
17477
|
14 |
consts
|
|
|
15 |
evalc :: "(com * state * state) set"
|
|
|
16 |
evaln :: "(com * state * nat * state) set"
|
|
8177
|
17 |
|
|
17477
|
18 |
syntax
|
|
|
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"
|
|
8177
|
25 |
|
|
|
26 |
consts
|
|
|
27 |
newlocs :: locals
|
|
17477
|
28 |
setlocs :: "state => locals => state"
|
|
|
29 |
getlocs :: "state => locals"
|
|
|
30 |
update :: "state => vname => val => state" ("_/[_/::=/_]" [900,0,0] 900)
|
|
8177
|
31 |
syntax (* IN Natural.thy *)
|
|
17477
|
32 |
loc :: "state => locals" ("_<_>" [75,0] 75)
|
|
8177
|
33 |
translations
|
|
|
34 |
"s<X>" == "getlocs s X"
|
|
|
35 |
|
|
|
36 |
inductive evalc
|
|
17477
|
37 |
intros
|
|
|
38 |
Skip: "<SKIP,s> -c-> s"
|
|
8177
|
39 |
|
|
17477
|
40 |
Assign: "<X :== a,s> -c-> s[X::=a s]"
|
|
8177
|
41 |
|
|
17477
|
42 |
Local: "<c, s0[Loc Y::= a s0]> -c-> s1 ==>
|
|
|
43 |
<LOCAL Y := a IN c, s0> -c-> s1[Loc Y::=s0<Y>]"
|
|
8177
|
44 |
|
|
17477
|
45 |
Semi: "[| <c0,s0> -c-> s1; <c1,s1> -c-> s2 |] ==>
|
|
|
46 |
<c0;; c1, s0> -c-> s2"
|
|
8177
|
47 |
|
|
17477
|
48 |
IfTrue: "[| b s; <c0,s> -c-> s1 |] ==>
|
|
|
49 |
<IF b THEN c0 ELSE c1, s> -c-> s1"
|
|
8177
|
50 |
|
|
17477
|
51 |
IfFalse: "[| ~b s; <c1,s> -c-> s1 |] ==>
|
|
|
52 |
<IF b THEN c0 ELSE c1, s> -c-> s1"
|
|
8177
|
53 |
|
|
17477
|
54 |
WhileFalse: "~b s ==> <WHILE b DO c,s> -c-> s"
|
|
8177
|
55 |
|
|
17477
|
56 |
WhileTrue: "[| b s0; <c,s0> -c-> s1; <WHILE b DO c, s1> -c-> s2 |] ==>
|
|
|
57 |
<WHILE b DO c, s0> -c-> s2"
|
|
8177
|
58 |
|
|
17477
|
59 |
Body: "<the (body pn), s0> -c-> s1 ==>
|
|
|
60 |
<BODY pn, s0> -c-> s1"
|
|
8177
|
61 |
|
|
17477
|
62 |
Call: "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -c-> s1 ==>
|
|
|
63 |
<X:=CALL pn(a), s0> -c-> (setlocs s1 (getlocs s0))
|
|
|
64 |
[X::=s1<Res>]"
|
|
8177
|
65 |
|
|
|
66 |
inductive evaln
|
|
17477
|
67 |
intros
|
|
|
68 |
Skip: "<SKIP,s> -n-> s"
|
|
|
69 |
|
|
|
70 |
Assign: "<X :== a,s> -n-> s[X::=a s]"
|
|
8177
|
71 |
|
|
17477
|
72 |
Local: "<c, s0[Loc Y::= a s0]> -n-> s1 ==>
|
|
|
73 |
<LOCAL Y := a IN c, s0> -n-> s1[Loc Y::=s0<Y>]"
|
|
|
74 |
|
|
|
75 |
Semi: "[| <c0,s0> -n-> s1; <c1,s1> -n-> s2 |] ==>
|
|
|
76 |
<c0;; c1, s0> -n-> s2"
|
|
8177
|
77 |
|
|
17477
|
78 |
IfTrue: "[| b s; <c0,s> -n-> s1 |] ==>
|
|
|
79 |
<IF b THEN c0 ELSE c1, s> -n-> s1"
|
|
8177
|
80 |
|
|
17477
|
81 |
IfFalse: "[| ~b s; <c1,s> -n-> s1 |] ==>
|
|
|
82 |
<IF b THEN c0 ELSE c1, s> -n-> s1"
|
|
8177
|
83 |
|
|
17477
|
84 |
WhileFalse: "~b s ==> <WHILE b DO c,s> -n-> s"
|
|
|
85 |
|
|
|
86 |
WhileTrue: "[| b s0; <c,s0> -n-> s1; <WHILE b DO c, s1> -n-> s2 |] ==>
|
|
|
87 |
<WHILE b DO c, s0> -n-> s2"
|
|
8177
|
88 |
|
|
17477
|
89 |
Body: "<the (body pn), s0> - n-> s1 ==>
|
|
|
90 |
<BODY pn, s0> -Suc n-> s1"
|
|
8177
|
91 |
|
|
17477
|
92 |
Call: "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -n-> s1 ==>
|
|
|
93 |
<X:=CALL pn(a), s0> -n-> (setlocs s1 (getlocs s0))
|
|
|
94 |
[X::=s1<Res>]"
|
|
8177
|
95 |
|
|
|
96 |
|
|
17477
|
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"
|
|
8177
|
101 |
|
|
17477
|
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 |
|
|
19803
|
110 |
declare evalc.intros [intro]
|
|
|
111 |
declare evaln.intros [intro]
|
|
|
112 |
|
|
|
113 |
declare evalc_elim_cases [elim!]
|
|
|
114 |
declare evaln_elim_cases [elim!]
|
|
|
115 |
|
|
|
116 |
(* evaluation of com is deterministic *)
|
|
|
117 |
lemma com_det [rule_format (no_asm)]: "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)"
|
|
|
118 |
apply (erule evalc.induct)
|
|
|
119 |
apply (erule_tac [8] V = "<?c,s1> -c-> s2" in thin_rl)
|
|
|
120 |
(*blast_tac needs Unify.search_bound := 40*)
|
|
|
121 |
apply (best elim: evalc_WHILE_case)+
|
|
|
122 |
done
|
|
|
123 |
|
|
|
124 |
lemma evaln_evalc: "<c,s> -n-> t ==> <c,s> -c-> t"
|
|
|
125 |
apply (erule evaln.induct)
|
|
|
126 |
apply (tactic {* ALLGOALS (resolve_tac (thms "evalc.intros") THEN_ALL_NEW atac) *})
|
|
|
127 |
done
|
|
|
128 |
|
|
|
129 |
lemma Suc_le_D_lemma: "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'"
|
|
|
130 |
apply (frule Suc_le_D)
|
|
|
131 |
apply blast
|
|
|
132 |
done
|
|
|
133 |
|
|
|
134 |
lemma evaln_nonstrict [rule_format]: "<c,s> -n-> t ==> !m. n<=m --> <c,s> -m-> t"
|
|
|
135 |
apply (erule evaln.induct)
|
|
|
136 |
apply (tactic {* ALLGOALS (EVERY'[strip_tac,TRY o etac (thm "Suc_le_D_lemma"), REPEAT o smp_tac 1]) *})
|
|
|
137 |
apply (tactic {* ALLGOALS (resolve_tac (thms "evaln.intros") THEN_ALL_NEW atac) *})
|
|
|
138 |
done
|
|
|
139 |
|
|
|
140 |
lemma evaln_Suc: "<c,s> -n-> s' ==> <c,s> -Suc n-> s'"
|
|
|
141 |
apply (erule evaln_nonstrict)
|
|
|
142 |
apply auto
|
|
|
143 |
done
|
|
|
144 |
|
|
|
145 |
lemma evaln_max2: "[| <c1,s1> -n1-> t1; <c2,s2> -n2-> t2 |] ==>
|
|
|
146 |
? n. <c1,s1> -n -> t1 & <c2,s2> -n -> t2"
|
|
|
147 |
apply (cut_tac m = "n1" and n = "n2" in nat_le_linear)
|
|
|
148 |
apply (blast dest: evaln_nonstrict)
|
|
|
149 |
done
|
|
|
150 |
|
|
|
151 |
lemma evalc_evaln: "<c,s> -c-> t ==> ? n. <c,s> -n-> t"
|
|
|
152 |
apply (erule evalc.induct)
|
|
|
153 |
apply (tactic {* ALLGOALS (REPEAT o etac exE) *})
|
|
|
154 |
apply (tactic {* TRYALL (EVERY'[datac (thm "evaln_max2") 1, REPEAT o eresolve_tac [exE, conjE]]) *})
|
|
|
155 |
apply (tactic {* ALLGOALS (rtac exI THEN' resolve_tac (thms "evaln.intros") THEN_ALL_NEW atac) *})
|
|
|
156 |
done
|
|
|
157 |
|
|
|
158 |
lemma eval_eq: "<c,s> -c-> t = (? n. <c,s> -n-> t)"
|
|
|
159 |
apply (fast elim: evalc_evaln evaln_evalc)
|
|
|
160 |
done
|
|
17477
|
161 |
|
|
8177
|
162 |
end
|