24 | ":=" loc exp (infixl 60) |
25 | ":=" loc exp (infixl 60) |
25 | Semi com com ("_;;_" [60, 60] 60) |
26 | Semi com com ("_;;_" [60, 60] 60) |
26 | Cond exp com com ("IF _ THEN _ ELSE _" 60) |
27 | Cond exp com com ("IF _ THEN _ ELSE _" 60) |
27 | While exp com ("WHILE _ DO _" 60) |
28 | While exp com ("WHILE _ DO _" 60) |
28 |
29 |
29 (** Execution of commands **) |
30 text{* Execution of commands *} |
30 consts exec :: "((exp*state) * (nat*state)) set => ((com*state)*state)set" |
31 consts exec :: "((exp*state) * (nat*state)) set => ((com*state)*state)set" |
31 "@exec" :: "((exp*state) * (nat*state)) set => |
32 "@exec" :: "((exp*state) * (nat*state)) set => |
32 [com*state,state] => bool" ("_/ -[_]-> _" [50,0,50] 50) |
33 [com*state,state] => bool" ("_/ -[_]-> _" [50,0,50] 50) |
33 |
34 |
34 translations "csig -[eval]-> s" == "(csig,s) : exec eval" |
35 translations "csig -[eval]-> s" == "(csig,s) \<in> exec eval" |
35 |
36 |
36 syntax eval' :: "[exp*state,nat*state] => |
37 syntax eval' :: "[exp*state,nat*state] => |
37 ((exp*state) * (nat*state)) set => bool" |
38 ((exp*state) * (nat*state)) set => bool" |
38 ("_/ -|[_]-> _" [50,0,50] 50) |
39 ("_/ -|[_]-> _" [50,0,50] 50) |
|
40 |
39 translations |
41 translations |
40 "esig -|[eval]-> ns" => "(esig,ns) : eval" |
42 "esig -|[eval]-> ns" => "(esig,ns) \<in> eval" |
41 |
43 |
42 (*Command execution. Natural numbers represent Booleans: 0=True, 1=False*) |
44 text{*Command execution. Natural numbers represent Booleans: 0=True, 1=False*} |
43 inductive "exec eval" |
45 inductive "exec eval" |
44 intrs |
46 intros |
45 Skip "(SKIP,s) -[eval]-> s" |
47 Skip: "(SKIP,s) -[eval]-> s" |
46 |
48 |
47 Assign "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)" |
49 Assign: "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)" |
48 |
50 |
49 Semi "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] |
51 Semi: "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] |
50 ==> (c0 ;; c1, s) -[eval]-> s1" |
52 ==> (c0 ;; c1, s) -[eval]-> s1" |
51 |
53 |
52 IfTrue "[| (e,s) -|[eval]-> (0,s'); (c0,s') -[eval]-> s1 |] |
54 IfTrue: "[| (e,s) -|[eval]-> (0,s'); (c0,s') -[eval]-> s1 |] |
53 ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1" |
|
54 |
|
55 IfFalse "[| (e,s) -|[eval]-> (Suc 0, s'); (c1,s') -[eval]-> s1 |] |
|
56 ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1" |
55 ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1" |
57 |
56 |
58 WhileFalse "(e,s) -|[eval]-> (Suc 0, s1) ==> (WHILE e DO c, s) -[eval]-> s1" |
57 IfFalse: "[| (e,s) -|[eval]-> (Suc 0, s'); (c1,s') -[eval]-> s1 |] |
59 |
58 ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1" |
60 WhileTrue "[| (e,s) -|[eval]-> (0,s1); |
59 |
61 (c,s1) -[eval]-> s2; (WHILE e DO c, s2) -[eval]-> s3 |] |
60 WhileFalse: "(e,s) -|[eval]-> (Suc 0, s1) |
62 ==> (WHILE e DO c, s) -[eval]-> s3" |
61 ==> (WHILE e DO c, s) -[eval]-> s1" |
|
62 |
|
63 WhileTrue: "[| (e,s) -|[eval]-> (0,s1); |
|
64 (c,s1) -[eval]-> s2; (WHILE e DO c, s2) -[eval]-> s3 |] |
|
65 ==> (WHILE e DO c, s) -[eval]-> s3" |
|
66 |
|
67 declare exec.intros [intro] |
|
68 |
|
69 |
|
70 inductive_cases |
|
71 [elim!]: "(SKIP,s) -[eval]-> t" |
|
72 and [elim!]: "(x:=a,s) -[eval]-> t" |
|
73 and [elim!]: "(c1;;c2, s) -[eval]-> t" |
|
74 and [elim!]: "(IF e THEN c1 ELSE c2, s) -[eval]-> t" |
|
75 and exec_WHILE_case: "(WHILE b DO c,s) -[eval]-> t" |
|
76 |
|
77 |
|
78 text{*Justifies using "exec" in the inductive definition of "eval"*} |
|
79 lemma exec_mono: "A<=B ==> exec(A) <= exec(B)" |
|
80 apply (unfold exec.defs ) |
|
81 apply (rule lfp_mono) |
|
82 apply (assumption | rule basic_monos)+ |
|
83 done |
|
84 |
|
85 ML {* |
|
86 Unify.trace_bound := 30; |
|
87 Unify.search_bound := 60; |
|
88 *} |
|
89 |
|
90 text{*Command execution is functional (deterministic) provided evaluation is*} |
|
91 theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)" |
|
92 apply (simp add: single_valued_def) |
|
93 apply (intro allI) |
|
94 apply (rule impI) |
|
95 apply (erule exec.induct) |
|
96 apply (blast elim: exec_WHILE_case)+ |
|
97 done |
|
98 |
|
99 |
|
100 section {* Expressions *} |
|
101 |
|
102 text{* Evaluation of arithmetic expressions *} |
|
103 consts eval :: "((exp*state) * (nat*state)) set" |
|
104 "-|->" :: "[exp*state,nat*state] => bool" (infixl 50) |
|
105 |
|
106 translations |
|
107 "esig -|-> (n,s)" <= "(esig,n,s) \<in> eval" |
|
108 "esig -|-> ns" == "(esig,ns ) \<in> eval" |
|
109 |
|
110 inductive eval |
|
111 intros |
|
112 N [intro!]: "(N(n),s) -|-> (n,s)" |
|
113 |
|
114 X [intro!]: "(X(x),s) -|-> (s(x),s)" |
|
115 |
|
116 Op [intro]: "[| (e0,s) -|-> (n0,s0); (e1,s0) -|-> (n1,s1) |] |
|
117 ==> (Op f e0 e1, s) -|-> (f n0 n1, s1)" |
|
118 |
|
119 valOf [intro]: "[| (c,s) -[eval]-> s0; (e,s0) -|-> (n,s1) |] |
|
120 ==> (VALOF c RESULTIS e, s) -|-> (n, s1)" |
|
121 |
|
122 monos exec_mono |
|
123 |
|
124 |
|
125 inductive_cases |
|
126 [elim!]: "(N(n),sigma) -|-> (n',s')" |
|
127 and [elim!]: "(X(x),sigma) -|-> (n,s')" |
|
128 and [elim!]: "(Op f a1 a2,sigma) -|-> (n,s')" |
|
129 and [elim!]: "(VALOF c RESULTIS e, s) -|-> (n, s1)" |
|
130 |
|
131 |
|
132 lemma var_assign_eval [intro!]: "(X x, s(x:=n)) -|-> (n, s(x:=n))" |
|
133 by (rule fun_upd_same [THEN subst], fast) |
|
134 |
|
135 |
|
136 text{* Make the induction rule look nicer -- though eta_contract makes the new |
|
137 version look worse than it is...*} |
|
138 |
|
139 lemma split_lemma: |
|
140 "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))" |
|
141 by auto |
|
142 |
|
143 text{*New induction rule. Note the form of the VALOF induction hypothesis*} |
|
144 lemma eval_induct: |
|
145 "[| (e,s) -|-> (n,s'); |
|
146 !!n s. P (N n) s n s; |
|
147 !!s x. P (X x) s (s x) s; |
|
148 !!e0 e1 f n0 n1 s s0 s1. |
|
149 [| (e0,s) -|-> (n0,s0); P e0 s n0 s0; |
|
150 (e1,s0) -|-> (n1,s1); P e1 s0 n1 s1 |
|
151 |] ==> P (Op f e0 e1) s (f n0 n1) s1; |
|
152 !!c e n s s0 s1. |
|
153 [| (c,s) -[eval Int {((e,s),(n,s')). P e s n s'}]-> s0; |
|
154 (c,s) -[eval]-> s0; |
|
155 (e,s0) -|-> (n,s1); P e s0 n s1 |] |
|
156 ==> P (VALOF c RESULTIS e) s n s1 |
|
157 |] ==> P e s n s'" |
|
158 apply (erule eval.induct, blast) |
|
159 apply blast |
|
160 apply blast |
|
161 apply (frule Int_lower1 [THEN exec_mono, THEN subsetD]) |
|
162 apply (auto simp add: split_lemma) |
|
163 done |
|
164 |
|
165 |
|
166 text{*Lemma for Function_eval. The major premise is that (c,s) executes to s1 |
|
167 using eval restricted to its functional part. Note that the execution |
|
168 (c,s) -[eval]-> s2 can use unrestricted eval! The reason is that |
|
169 the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is |
|
170 functional on the argument (c,s). |
|
171 *} |
|
172 lemma com_Unique: |
|
173 "(c,s) -[eval Int {((e,s),(n,t)). \<forall>nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1 |
|
174 ==> \<forall>s2. (c,s) -[eval]-> s2 --> s2=s1" |
|
175 apply (erule exec.induct, simp_all) |
|
176 apply blast |
|
177 apply force |
|
178 apply blast |
|
179 apply blast |
|
180 apply blast |
|
181 apply (blast elim: exec_WHILE_case) |
|
182 apply (erule_tac V = "(?c,s2) -[?ev]-> s3" in thin_rl) |
|
183 apply clarify |
|
184 apply (erule exec_WHILE_case, blast+) |
|
185 done |
|
186 |
|
187 |
|
188 text{*Expression evaluation is functional, or deterministic*} |
|
189 theorem single_valued_eval: "single_valued eval" |
|
190 apply (unfold single_valued_def) |
|
191 apply (intro allI, rule impI) |
|
192 apply (simp (no_asm_simp) only: split_tupled_all) |
|
193 apply (erule eval_induct) |
|
194 apply (drule_tac [4] com_Unique) |
|
195 apply (simp_all (no_asm_use)) |
|
196 apply blast+ |
|
197 done |
|
198 |
|
199 |
|
200 lemma eval_N_E_lemma: "(e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)" |
|
201 by (erule eval_induct, simp_all) |
|
202 |
|
203 lemmas eval_N_E [dest!] = eval_N_E_lemma [THEN mp, OF _ refl] |
|
204 |
|
205 |
|
206 text{*This theorem says that "WHILE TRUE DO c" cannot terminate*} |
|
207 lemma while_true_E [rule_format]: |
|
208 "(c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False" |
|
209 by (erule exec.induct, auto) |
|
210 |
|
211 |
|
212 subsection{* Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP and |
|
213 WHILE e DO c *} |
|
214 |
|
215 lemma while_if1 [rule_format]: |
|
216 "(c',s) -[eval]-> t |
|
217 ==> (c' = WHILE e DO c) --> |
|
218 (IF e THEN c;;c' ELSE SKIP, s) -[eval]-> t" |
|
219 by (erule exec.induct, auto) |
|
220 |
|
221 lemma while_if2 [rule_format]: |
|
222 "(c',s) -[eval]-> t |
|
223 ==> (c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP) --> |
|
224 (WHILE e DO c, s) -[eval]-> t" |
|
225 by (erule exec.induct, auto) |
|
226 |
|
227 |
|
228 theorem while_if: |
|
229 "((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) -[eval]-> t) = |
|
230 ((WHILE e DO c, s) -[eval]-> t)" |
|
231 by (blast intro: while_if1 while_if2) |
|
232 |
|
233 |
|
234 |
|
235 subsection{* Equivalence of (IF e THEN c1 ELSE c2);;c |
|
236 and IF e THEN (c1;;c) ELSE (c2;;c) *} |
|
237 |
|
238 lemma if_semi1 [rule_format]: |
|
239 "(c',s) -[eval]-> t |
|
240 ==> (c' = (IF e THEN c1 ELSE c2);;c) --> |
|
241 (IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t" |
|
242 by (erule exec.induct, auto) |
|
243 |
|
244 lemma if_semi2 [rule_format]: |
|
245 "(c',s) -[eval]-> t |
|
246 ==> (c' = IF e THEN (c1;;c) ELSE (c2;;c)) --> |
|
247 ((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t" |
|
248 by (erule exec.induct, auto) |
|
249 |
|
250 theorem if_semi: "(((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t) = |
|
251 ((IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t)" |
|
252 by (blast intro: if_semi1 if_semi2) |
|
253 |
|
254 |
|
255 |
|
256 subsection{* Equivalence of VALOF c1 RESULTIS (VALOF c2 RESULTIS e) |
|
257 and VALOF c1;;c2 RESULTIS e |
|
258 *} |
|
259 |
|
260 lemma valof_valof1 [rule_format]: |
|
261 "(e',s) -|-> (v,s') |
|
262 ==> (e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e)) --> |
|
263 (VALOF c1;;c2 RESULTIS e, s) -|-> (v,s')" |
|
264 by (erule eval_induct, auto) |
|
265 |
|
266 |
|
267 lemma valof_valof2 [rule_format]: |
|
268 "(e',s) -|-> (v,s') |
|
269 ==> (e' = VALOF c1;;c2 RESULTIS e) --> |
|
270 (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')" |
|
271 by (erule eval_induct, auto) |
|
272 |
|
273 theorem valof_valof: |
|
274 "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')) = |
|
275 ((VALOF c1;;c2 RESULTIS e, s) -|-> (v,s'))" |
|
276 by (blast intro: valof_valof1 valof_valof2) |
|
277 |
|
278 |
|
279 subsection{* Equivalence of VALOF SKIP RESULTIS e and e *} |
|
280 |
|
281 lemma valof_skip1 [rule_format]: |
|
282 "(e',s) -|-> (v,s') |
|
283 ==> (e' = VALOF SKIP RESULTIS e) --> |
|
284 (e, s) -|-> (v,s')" |
|
285 by (erule eval_induct, auto) |
|
286 |
|
287 lemma valof_skip2: |
|
288 "(e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')" |
|
289 by blast |
|
290 |
|
291 theorem valof_skip: |
|
292 "((VALOF SKIP RESULTIS e, s) -|-> (v,s')) = ((e, s) -|-> (v,s'))" |
|
293 by (blast intro: valof_skip1 valof_skip2) |
|
294 |
|
295 |
|
296 subsection{* Equivalence of VALOF x:=e RESULTIS x and e *} |
|
297 |
|
298 lemma valof_assign1 [rule_format]: |
|
299 "(e',s) -|-> (v,s'') |
|
300 ==> (e' = VALOF x:=e RESULTIS X x) --> |
|
301 (\<exists>s'. (e, s) -|-> (v,s') & (s'' = s'(x:=v)))" |
|
302 apply (erule eval_induct) |
|
303 apply (simp_all del: fun_upd_apply, clarify, auto) |
|
304 done |
|
305 |
|
306 lemma valof_assign2: |
|
307 "(e,s) -|-> (v,s') ==> (VALOF x:=e RESULTIS X x, s) -|-> (v,s'(x:=v))" |
|
308 by blast |
|
309 |
|
310 |
63 end |
311 end |