|
1 (* Author: Gerwin Klein *) |
|
2 |
|
3 theory Compiler2 |
|
4 imports Compiler |
|
5 begin |
|
6 |
|
7 section {* Compiler Correctness, Reverse Direction *} |
|
8 |
|
9 subsection {* Definitions *} |
|
10 |
|
11 text {* Execution in @{term n} steps for simpler induction *} |
|
12 primrec |
|
13 exec_n :: "instr list \<Rightarrow> config \<Rightarrow> nat \<Rightarrow> config \<Rightarrow> bool" |
|
14 ("_/ \<turnstile> (_ \<rightarrow>^_/ _)" [65,0,1000,55] 55) |
|
15 where |
|
16 "P \<turnstile> c \<rightarrow>^0 c' = (c'=c)" | |
|
17 "P \<turnstile> c \<rightarrow>^(Suc n) c'' = (\<exists>c'. (P \<turnstile> c \<rightarrow> c') \<and> P \<turnstile> c' \<rightarrow>^n c'')" |
|
18 |
|
19 text {* The possible successor PCs of an instruction at position @{term n} *} |
|
20 text_raw{*\snip{isuccsdef}{0}{1}{% *} |
|
21 definition |
|
22 "isuccs i n \<equiv> case i of |
|
23 JMP j \<Rightarrow> {n + 1 + j} |
|
24 | JMPLESS j \<Rightarrow> {n + 1 + j, n + 1} |
|
25 | JMPGE j \<Rightarrow> {n + 1 + j, n + 1} |
|
26 | _ \<Rightarrow> {n +1}" |
|
27 text_raw{*}%endsnip*} |
|
28 |
|
29 text {* The possible successors PCs of an instruction list *} |
|
30 definition |
|
31 succs :: "instr list \<Rightarrow> int \<Rightarrow> int set" where |
|
32 "succs P n = {s. \<exists>i::int. 0 \<le> i \<and> i < size P \<and> s \<in> isuccs (P!!i) (n+i)}" |
|
33 |
|
34 text {* Possible exit PCs of a program *} |
|
35 definition |
|
36 "exits P = succs P 0 - {0..< size P}" |
|
37 |
|
38 |
|
39 subsection {* Basic properties of @{term exec_n} *} |
|
40 |
|
41 lemma exec_n_exec: |
|
42 "P \<turnstile> c \<rightarrow>^n c' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c'" |
|
43 by (induct n arbitrary: c) (auto simp del: exec1_def) |
|
44 |
|
45 lemma exec_0 [intro!]: "P \<turnstile> c \<rightarrow>^0 c" by simp |
|
46 |
|
47 lemma exec_Suc: |
|
48 "\<lbrakk> P \<turnstile> c \<rightarrow> c'; P \<turnstile> c' \<rightarrow>^n c'' \<rbrakk> \<Longrightarrow> P \<turnstile> c \<rightarrow>^(Suc n) c''" |
|
49 by (fastforce simp del: split_paired_Ex) |
|
50 |
|
51 lemma exec_exec_n: |
|
52 "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> \<exists>n. P \<turnstile> c \<rightarrow>^n c'" |
|
53 by (induct rule: exec.induct) (auto simp del: exec1_def intro: exec_Suc) |
|
54 |
|
55 lemma exec_eq_exec_n: |
|
56 "(P \<turnstile> c \<rightarrow>* c') = (\<exists>n. P \<turnstile> c \<rightarrow>^n c')" |
|
57 by (blast intro: exec_exec_n exec_n_exec) |
|
58 |
|
59 lemma exec_n_Nil [simp]: |
|
60 "[] \<turnstile> c \<rightarrow>^k c' = (c' = c \<and> k = 0)" |
|
61 by (induct k) auto |
|
62 |
|
63 lemma exec1_exec_n [intro!]: |
|
64 "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c \<rightarrow>^1 c'" |
|
65 by (cases c') simp |
|
66 |
|
67 |
|
68 subsection {* Concrete symbolic execution steps *} |
|
69 |
|
70 lemma exec_n_step: |
|
71 "n \<noteq> n' \<Longrightarrow> |
|
72 P \<turnstile> (n,stk,s) \<rightarrow>^k (n',stk',s') = |
|
73 (\<exists>c. P \<turnstile> (n,stk,s) \<rightarrow> c \<and> P \<turnstile> c \<rightarrow>^(k - 1) (n',stk',s') \<and> 0 < k)" |
|
74 by (cases k) auto |
|
75 |
|
76 lemma exec1_end: |
|
77 "size P <= fst c \<Longrightarrow> \<not> P \<turnstile> c \<rightarrow> c'" |
|
78 by auto |
|
79 |
|
80 lemma exec_n_end: |
|
81 "size P <= (n::int) \<Longrightarrow> |
|
82 P \<turnstile> (n,s,stk) \<rightarrow>^k (n',s',stk') = (n' = n \<and> stk'=stk \<and> s'=s \<and> k =0)" |
|
83 by (cases k) (auto simp: exec1_end) |
|
84 |
|
85 lemmas exec_n_simps = exec_n_step exec_n_end |
|
86 |
|
87 |
|
88 subsection {* Basic properties of @{term succs} *} |
|
89 |
|
90 lemma succs_simps [simp]: |
|
91 "succs [ADD] n = {n + 1}" |
|
92 "succs [LOADI v] n = {n + 1}" |
|
93 "succs [LOAD x] n = {n + 1}" |
|
94 "succs [STORE x] n = {n + 1}" |
|
95 "succs [JMP i] n = {n + 1 + i}" |
|
96 "succs [JMPGE i] n = {n + 1 + i, n + 1}" |
|
97 "succs [JMPLESS i] n = {n + 1 + i, n + 1}" |
|
98 by (auto simp: succs_def isuccs_def) |
|
99 |
|
100 lemma succs_empty [iff]: "succs [] n = {}" |
|
101 by (simp add: succs_def) |
|
102 |
|
103 lemma succs_Cons: |
|
104 "succs (x#xs) n = isuccs x n \<union> succs xs (1+n)" (is "_ = ?x \<union> ?xs") |
|
105 proof |
|
106 let ?isuccs = "\<lambda>p P n i::int. 0 \<le> i \<and> i < size P \<and> p \<in> isuccs (P!!i) (n+i)" |
|
107 { fix p assume "p \<in> succs (x#xs) n" |
|
108 then obtain i::int where isuccs: "?isuccs p (x#xs) n i" |
|
109 unfolding succs_def by auto |
|
110 have "p \<in> ?x \<union> ?xs" |
|
111 proof cases |
|
112 assume "i = 0" with isuccs show ?thesis by simp |
|
113 next |
|
114 assume "i \<noteq> 0" |
|
115 with isuccs |
|
116 have "?isuccs p xs (1+n) (i - 1)" by auto |
|
117 hence "p \<in> ?xs" unfolding succs_def by blast |
|
118 thus ?thesis .. |
|
119 qed |
|
120 } |
|
121 thus "succs (x#xs) n \<subseteq> ?x \<union> ?xs" .. |
|
122 |
|
123 { fix p assume "p \<in> ?x \<or> p \<in> ?xs" |
|
124 hence "p \<in> succs (x#xs) n" |
|
125 proof |
|
126 assume "p \<in> ?x" thus ?thesis by (fastforce simp: succs_def) |
|
127 next |
|
128 assume "p \<in> ?xs" |
|
129 then obtain i where "?isuccs p xs (1+n) i" |
|
130 unfolding succs_def by auto |
|
131 hence "?isuccs p (x#xs) n (1+i)" |
|
132 by (simp add: algebra_simps) |
|
133 thus ?thesis unfolding succs_def by blast |
|
134 qed |
|
135 } |
|
136 thus "?x \<union> ?xs \<subseteq> succs (x#xs) n" by blast |
|
137 qed |
|
138 |
|
139 lemma succs_iexec1: |
|
140 assumes "c' = iexec (P!!i) (i,s,stk)" "0 \<le> i" "i < size P" |
|
141 shows "fst c' \<in> succs P 0" |
|
142 using assms by (auto simp: succs_def isuccs_def split: instr.split) |
|
143 |
|
144 lemma succs_shift: |
|
145 "(p - n \<in> succs P 0) = (p \<in> succs P n)" |
|
146 by (fastforce simp: succs_def isuccs_def split: instr.split) |
|
147 |
|
148 lemma inj_op_plus [simp]: |
|
149 "inj (op + (i::int))" |
|
150 by (metis add_minus_cancel inj_on_inverseI) |
|
151 |
|
152 lemma succs_set_shift [simp]: |
|
153 "op + i ` succs xs 0 = succs xs i" |
|
154 by (force simp: succs_shift [where n=i, symmetric] intro: set_eqI) |
|
155 |
|
156 lemma succs_append [simp]: |
|
157 "succs (xs @ ys) n = succs xs n \<union> succs ys (n + size xs)" |
|
158 by (induct xs arbitrary: n) (auto simp: succs_Cons algebra_simps) |
|
159 |
|
160 |
|
161 lemma exits_append [simp]: |
|
162 "exits (xs @ ys) = exits xs \<union> (op + (size xs)) ` exits ys - |
|
163 {0..<size xs + size ys}" |
|
164 by (auto simp: exits_def image_set_diff) |
|
165 |
|
166 lemma exits_single: |
|
167 "exits [x] = isuccs x 0 - {0}" |
|
168 by (auto simp: exits_def succs_def) |
|
169 |
|
170 lemma exits_Cons: |
|
171 "exits (x # xs) = (isuccs x 0 - {0}) \<union> (op + 1) ` exits xs - |
|
172 {0..<1 + size xs}" |
|
173 using exits_append [of "[x]" xs] |
|
174 by (simp add: exits_single) |
|
175 |
|
176 lemma exits_empty [iff]: "exits [] = {}" by (simp add: exits_def) |
|
177 |
|
178 lemma exits_simps [simp]: |
|
179 "exits [ADD] = {1}" |
|
180 "exits [LOADI v] = {1}" |
|
181 "exits [LOAD x] = {1}" |
|
182 "exits [STORE x] = {1}" |
|
183 "i \<noteq> -1 \<Longrightarrow> exits [JMP i] = {1 + i}" |
|
184 "i \<noteq> -1 \<Longrightarrow> exits [JMPGE i] = {1 + i, 1}" |
|
185 "i \<noteq> -1 \<Longrightarrow> exits [JMPLESS i] = {1 + i, 1}" |
|
186 by (auto simp: exits_def) |
|
187 |
|
188 lemma acomp_succs [simp]: |
|
189 "succs (acomp a) n = {n + 1 .. n + size (acomp a)}" |
|
190 by (induct a arbitrary: n) auto |
|
191 |
|
192 lemma acomp_size: |
|
193 "(1::int) \<le> size (acomp a)" |
|
194 by (induct a) auto |
|
195 |
|
196 lemma acomp_exits [simp]: |
|
197 "exits (acomp a) = {size (acomp a)}" |
|
198 by (auto simp: exits_def acomp_size) |
|
199 |
|
200 lemma bcomp_succs: |
|
201 "0 \<le> i \<Longrightarrow> |
|
202 succs (bcomp b c i) n \<subseteq> {n .. n + size (bcomp b c i)} |
|
203 \<union> {n + i + size (bcomp b c i)}" |
|
204 proof (induction b arbitrary: c i n) |
|
205 case (And b1 b2) |
|
206 from And.prems |
|
207 show ?case |
|
208 by (cases c) |
|
209 (auto dest: And.IH(1) [THEN subsetD, rotated] |
|
210 And.IH(2) [THEN subsetD, rotated]) |
|
211 qed auto |
|
212 |
|
213 lemmas bcomp_succsD [dest!] = bcomp_succs [THEN subsetD, rotated] |
|
214 |
|
215 lemma bcomp_exits: |
|
216 fixes i :: int |
|
217 shows |
|
218 "0 \<le> i \<Longrightarrow> |
|
219 exits (bcomp b c i) \<subseteq> {size (bcomp b c i), i + size (bcomp b c i)}" |
|
220 by (auto simp: exits_def) |
|
221 |
|
222 lemma bcomp_exitsD [dest!]: |
|
223 "p \<in> exits (bcomp b c i) \<Longrightarrow> 0 \<le> i \<Longrightarrow> |
|
224 p = size (bcomp b c i) \<or> p = i + size (bcomp b c i)" |
|
225 using bcomp_exits by auto |
|
226 |
|
227 lemma ccomp_succs: |
|
228 "succs (ccomp c) n \<subseteq> {n..n + size (ccomp c)}" |
|
229 proof (induction c arbitrary: n) |
|
230 case SKIP thus ?case by simp |
|
231 next |
|
232 case Assign thus ?case by simp |
|
233 next |
|
234 case (Seq c1 c2) |
|
235 from Seq.prems |
|
236 show ?case |
|
237 by (fastforce dest: Seq.IH [THEN subsetD]) |
|
238 next |
|
239 case (If b c1 c2) |
|
240 from If.prems |
|
241 show ?case |
|
242 by (auto dest!: If.IH [THEN subsetD] simp: isuccs_def succs_Cons) |
|
243 next |
|
244 case (While b c) |
|
245 from While.prems |
|
246 show ?case by (auto dest!: While.IH [THEN subsetD]) |
|
247 qed |
|
248 |
|
249 lemma ccomp_exits: |
|
250 "exits (ccomp c) \<subseteq> {size (ccomp c)}" |
|
251 using ccomp_succs [of c 0] by (auto simp: exits_def) |
|
252 |
|
253 lemma ccomp_exitsD [dest!]: |
|
254 "p \<in> exits (ccomp c) \<Longrightarrow> p = size (ccomp c)" |
|
255 using ccomp_exits by auto |
|
256 |
|
257 |
|
258 subsection {* Splitting up machine executions *} |
|
259 |
|
260 lemma exec1_split: |
|
261 fixes i j :: int |
|
262 shows |
|
263 "P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow> (j,s') \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < size c \<Longrightarrow> |
|
264 c \<turnstile> (i,s) \<rightarrow> (j - size P, s')" |
|
265 by (auto split: instr.splits) |
|
266 |
|
267 lemma exec_n_split: |
|
268 fixes i j :: int |
|
269 assumes "P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow>^n (j, s')" |
|
270 "0 \<le> i" "i < size c" |
|
271 "j \<notin> {size P ..< size P + size c}" |
|
272 shows "\<exists>s'' (i'::int) k m. |
|
273 c \<turnstile> (i, s) \<rightarrow>^k (i', s'') \<and> |
|
274 i' \<in> exits c \<and> |
|
275 P @ c @ P' \<turnstile> (size P + i', s'') \<rightarrow>^m (j, s') \<and> |
|
276 n = k + m" |
|
277 using assms proof (induction n arbitrary: i j s) |
|
278 case 0 |
|
279 thus ?case by simp |
|
280 next |
|
281 case (Suc n) |
|
282 have i: "0 \<le> i" "i < size c" by fact+ |
|
283 from Suc.prems |
|
284 have j: "\<not> (size P \<le> j \<and> j < size P + size c)" by simp |
|
285 from Suc.prems |
|
286 obtain i0 s0 where |
|
287 step: "P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow> (i0,s0)" and |
|
288 rest: "P @ c @ P' \<turnstile> (i0,s0) \<rightarrow>^n (j, s')" |
|
289 by clarsimp |
|
290 |
|
291 from step i |
|
292 have c: "c \<turnstile> (i,s) \<rightarrow> (i0 - size P, s0)" by (rule exec1_split) |
|
293 |
|
294 have "i0 = size P + (i0 - size P) " by simp |
|
295 then obtain j0::int where j0: "i0 = size P + j0" .. |
|
296 |
|
297 note split_paired_Ex [simp del] |
|
298 |
|
299 { assume "j0 \<in> {0 ..< size c}" |
|
300 with j0 j rest c |
|
301 have ?case |
|
302 by (fastforce dest!: Suc.IH intro!: exec_Suc) |
|
303 } moreover { |
|
304 assume "j0 \<notin> {0 ..< size c}" |
|
305 moreover |
|
306 from c j0 have "j0 \<in> succs c 0" |
|
307 by (auto dest: succs_iexec1 simp del: iexec.simps) |
|
308 ultimately |
|
309 have "j0 \<in> exits c" by (simp add: exits_def) |
|
310 with c j0 rest |
|
311 have ?case by fastforce |
|
312 } |
|
313 ultimately |
|
314 show ?case by cases |
|
315 qed |
|
316 |
|
317 lemma exec_n_drop_right: |
|
318 fixes j :: int |
|
319 assumes "c @ P' \<turnstile> (0, s) \<rightarrow>^n (j, s')" "j \<notin> {0..<size c}" |
|
320 shows "\<exists>s'' i' k m. |
|
321 (if c = [] then s'' = s \<and> i' = 0 \<and> k = 0 |
|
322 else c \<turnstile> (0, s) \<rightarrow>^k (i', s'') \<and> |
|
323 i' \<in> exits c) \<and> |
|
324 c @ P' \<turnstile> (i', s'') \<rightarrow>^m (j, s') \<and> |
|
325 n = k + m" |
|
326 using assms |
|
327 by (cases "c = []") |
|
328 (auto dest: exec_n_split [where P="[]", simplified]) |
|
329 |
|
330 |
|
331 text {* |
|
332 Dropping the left context of a potentially incomplete execution of @{term c}. |
|
333 *} |
|
334 |
|
335 lemma exec1_drop_left: |
|
336 fixes i n :: int |
|
337 assumes "P1 @ P2 \<turnstile> (i, s, stk) \<rightarrow> (n, s', stk')" and "size P1 \<le> i" |
|
338 shows "P2 \<turnstile> (i - size P1, s, stk) \<rightarrow> (n - size P1, s', stk')" |
|
339 proof - |
|
340 have "i = size P1 + (i - size P1)" by simp |
|
341 then obtain i' :: int where "i = size P1 + i'" .. |
|
342 moreover |
|
343 have "n = size P1 + (n - size P1)" by simp |
|
344 then obtain n' :: int where "n = size P1 + n'" .. |
|
345 ultimately |
|
346 show ?thesis using assms by (clarsimp simp del: iexec.simps) |
|
347 qed |
|
348 |
|
349 lemma exec_n_drop_left: |
|
350 fixes i n :: int |
|
351 assumes "P @ P' \<turnstile> (i, s, stk) \<rightarrow>^k (n, s', stk')" |
|
352 "size P \<le> i" "exits P' \<subseteq> {0..}" |
|
353 shows "P' \<turnstile> (i - size P, s, stk) \<rightarrow>^k (n - size P, s', stk')" |
|
354 using assms proof (induction k arbitrary: i s stk) |
|
355 case 0 thus ?case by simp |
|
356 next |
|
357 case (Suc k) |
|
358 from Suc.prems |
|
359 obtain i' s'' stk'' where |
|
360 step: "P @ P' \<turnstile> (i, s, stk) \<rightarrow> (i', s'', stk'')" and |
|
361 rest: "P @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^k (n, s', stk')" |
|
362 by (auto simp del: exec1_def) |
|
363 from step `size P \<le> i` |
|
364 have "P' \<turnstile> (i - size P, s, stk) \<rightarrow> (i' - size P, s'', stk'')" |
|
365 by (rule exec1_drop_left) |
|
366 moreover |
|
367 then have "i' - size P \<in> succs P' 0" |
|
368 by (fastforce dest!: succs_iexec1 simp del: iexec.simps) |
|
369 with `exits P' \<subseteq> {0..}` |
|
370 have "size P \<le> i'" by (auto simp: exits_def) |
|
371 from rest this `exits P' \<subseteq> {0..}` |
|
372 have "P' \<turnstile> (i' - size P, s'', stk'') \<rightarrow>^k (n - size P, s', stk')" |
|
373 by (rule Suc.IH) |
|
374 ultimately |
|
375 show ?case by auto |
|
376 qed |
|
377 |
|
378 lemmas exec_n_drop_Cons = |
|
379 exec_n_drop_left [where P="[instr]", simplified] for instr |
|
380 |
|
381 definition |
|
382 "closed P \<longleftrightarrow> exits P \<subseteq> {size P}" |
|
383 |
|
384 lemma ccomp_closed [simp, intro!]: "closed (ccomp c)" |
|
385 using ccomp_exits by (auto simp: closed_def) |
|
386 |
|
387 lemma acomp_closed [simp, intro!]: "closed (acomp c)" |
|
388 by (simp add: closed_def) |
|
389 |
|
390 lemma exec_n_split_full: |
|
391 fixes j :: int |
|
392 assumes exec: "P @ P' \<turnstile> (0,s,stk) \<rightarrow>^k (j, s', stk')" |
|
393 assumes P: "size P \<le> j" |
|
394 assumes closed: "closed P" |
|
395 assumes exits: "exits P' \<subseteq> {0..}" |
|
396 shows "\<exists>k1 k2 s'' stk''. P \<turnstile> (0,s,stk) \<rightarrow>^k1 (size P, s'', stk'') \<and> |
|
397 P' \<turnstile> (0,s'',stk'') \<rightarrow>^k2 (j - size P, s', stk')" |
|
398 proof (cases "P") |
|
399 case Nil with exec |
|
400 show ?thesis by fastforce |
|
401 next |
|
402 case Cons |
|
403 hence "0 < size P" by simp |
|
404 with exec P closed |
|
405 obtain k1 k2 s'' stk'' where |
|
406 1: "P \<turnstile> (0,s,stk) \<rightarrow>^k1 (size P, s'', stk'')" and |
|
407 2: "P @ P' \<turnstile> (size P,s'',stk'') \<rightarrow>^k2 (j, s', stk')" |
|
408 by (auto dest!: exec_n_split [where P="[]" and i=0, simplified] |
|
409 simp: closed_def) |
|
410 moreover |
|
411 have "j = size P + (j - size P)" by simp |
|
412 then obtain j0 :: int where "j = size P + j0" .. |
|
413 ultimately |
|
414 show ?thesis using exits |
|
415 by (fastforce dest: exec_n_drop_left) |
|
416 qed |
|
417 |
|
418 |
|
419 subsection {* Correctness theorem *} |
|
420 |
|
421 lemma acomp_neq_Nil [simp]: |
|
422 "acomp a \<noteq> []" |
|
423 by (induct a) auto |
|
424 |
|
425 lemma acomp_exec_n [dest!]: |
|
426 "acomp a \<turnstile> (0,s,stk) \<rightarrow>^n (size (acomp a),s',stk') \<Longrightarrow> |
|
427 s' = s \<and> stk' = aval a s#stk" |
|
428 proof (induction a arbitrary: n s' stk stk') |
|
429 case (Plus a1 a2) |
|
430 let ?sz = "size (acomp a1) + (size (acomp a2) + 1)" |
|
431 from Plus.prems |
|
432 have "acomp a1 @ acomp a2 @ [ADD] \<turnstile> (0,s,stk) \<rightarrow>^n (?sz, s', stk')" |
|
433 by (simp add: algebra_simps) |
|
434 |
|
435 then obtain n1 s1 stk1 n2 s2 stk2 n3 where |
|
436 "acomp a1 \<turnstile> (0,s,stk) \<rightarrow>^n1 (size (acomp a1), s1, stk1)" |
|
437 "acomp a2 \<turnstile> (0,s1,stk1) \<rightarrow>^n2 (size (acomp a2), s2, stk2)" |
|
438 "[ADD] \<turnstile> (0,s2,stk2) \<rightarrow>^n3 (1, s', stk')" |
|
439 by (auto dest!: exec_n_split_full) |
|
440 |
|
441 thus ?case by (fastforce dest: Plus.IH simp: exec_n_simps) |
|
442 qed (auto simp: exec_n_simps) |
|
443 |
|
444 lemma bcomp_split: |
|
445 fixes i j :: int |
|
446 assumes "bcomp b c i @ P' \<turnstile> (0, s, stk) \<rightarrow>^n (j, s', stk')" |
|
447 "j \<notin> {0..<size (bcomp b c i)}" "0 \<le> i" |
|
448 shows "\<exists>s'' stk'' (i'::int) k m. |
|
449 bcomp b c i \<turnstile> (0, s, stk) \<rightarrow>^k (i', s'', stk'') \<and> |
|
450 (i' = size (bcomp b c i) \<or> i' = i + size (bcomp b c i)) \<and> |
|
451 bcomp b c i @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^m (j, s', stk') \<and> |
|
452 n = k + m" |
|
453 using assms by (cases "bcomp b c i = []") (fastforce dest!: exec_n_drop_right)+ |
|
454 |
|
455 lemma bcomp_exec_n [dest]: |
|
456 fixes i j :: int |
|
457 assumes "bcomp b c j \<turnstile> (0, s, stk) \<rightarrow>^n (i, s', stk')" |
|
458 "size (bcomp b c j) \<le> i" "0 \<le> j" |
|
459 shows "i = size(bcomp b c j) + (if c = bval b s then j else 0) \<and> |
|
460 s' = s \<and> stk' = stk" |
|
461 using assms proof (induction b arbitrary: c j i n s' stk') |
|
462 case Bc thus ?case |
|
463 by (simp split: split_if_asm add: exec_n_simps) |
|
464 next |
|
465 case (Not b) |
|
466 from Not.prems show ?case |
|
467 by (fastforce dest!: Not.IH) |
|
468 next |
|
469 case (And b1 b2) |
|
470 |
|
471 let ?b2 = "bcomp b2 c j" |
|
472 let ?m = "if c then size ?b2 else size ?b2 + j" |
|
473 let ?b1 = "bcomp b1 False ?m" |
|
474 |
|
475 have j: "size (bcomp (And b1 b2) c j) \<le> i" "0 \<le> j" by fact+ |
|
476 |
|
477 from And.prems |
|
478 obtain s'' stk'' and i'::int and k m where |
|
479 b1: "?b1 \<turnstile> (0, s, stk) \<rightarrow>^k (i', s'', stk'')" |
|
480 "i' = size ?b1 \<or> i' = ?m + size ?b1" and |
|
481 b2: "?b2 \<turnstile> (i' - size ?b1, s'', stk'') \<rightarrow>^m (i - size ?b1, s', stk')" |
|
482 by (auto dest!: bcomp_split dest: exec_n_drop_left) |
|
483 from b1 j |
|
484 have "i' = size ?b1 + (if \<not>bval b1 s then ?m else 0) \<and> s'' = s \<and> stk'' = stk" |
|
485 by (auto dest!: And.IH) |
|
486 with b2 j |
|
487 show ?case |
|
488 by (fastforce dest!: And.IH simp: exec_n_end split: split_if_asm) |
|
489 next |
|
490 case Less |
|
491 thus ?case by (auto dest!: exec_n_split_full simp: exec_n_simps) (* takes time *) |
|
492 qed |
|
493 |
|
494 lemma ccomp_empty [elim!]: |
|
495 "ccomp c = [] \<Longrightarrow> (c,s) \<Rightarrow> s" |
|
496 by (induct c) auto |
|
497 |
|
498 declare assign_simp [simp] |
|
499 |
|
500 lemma ccomp_exec_n: |
|
501 "ccomp c \<turnstile> (0,s,stk) \<rightarrow>^n (size(ccomp c),t,stk') |
|
502 \<Longrightarrow> (c,s) \<Rightarrow> t \<and> stk'=stk" |
|
503 proof (induction c arbitrary: s t stk stk' n) |
|
504 case SKIP |
|
505 thus ?case by auto |
|
506 next |
|
507 case (Assign x a) |
|
508 thus ?case |
|
509 by simp (fastforce dest!: exec_n_split_full simp: exec_n_simps) |
|
510 next |
|
511 case (Seq c1 c2) |
|
512 thus ?case by (fastforce dest!: exec_n_split_full) |
|
513 next |
|
514 case (If b c1 c2) |
|
515 note If.IH [dest!] |
|
516 |
|
517 let ?if = "IF b THEN c1 ELSE c2" |
|
518 let ?cs = "ccomp ?if" |
|
519 let ?bcomp = "bcomp b False (size (ccomp c1) + 1)" |
|
520 |
|
521 from `?cs \<turnstile> (0,s,stk) \<rightarrow>^n (size ?cs,t,stk')` |
|
522 obtain i' :: int and k m s'' stk'' where |
|
523 cs: "?cs \<turnstile> (i',s'',stk'') \<rightarrow>^m (size ?cs,t,stk')" and |
|
524 "?bcomp \<turnstile> (0,s,stk) \<rightarrow>^k (i', s'', stk'')" |
|
525 "i' = size ?bcomp \<or> i' = size ?bcomp + size (ccomp c1) + 1" |
|
526 by (auto dest!: bcomp_split) |
|
527 |
|
528 hence i': |
|
529 "s''=s" "stk'' = stk" |
|
530 "i' = (if bval b s then size ?bcomp else size ?bcomp+size(ccomp c1)+1)" |
|
531 by auto |
|
532 |
|
533 with cs have cs': |
|
534 "ccomp c1@JMP (size (ccomp c2))#ccomp c2 \<turnstile> |
|
535 (if bval b s then 0 else size (ccomp c1)+1, s, stk) \<rightarrow>^m |
|
536 (1 + size (ccomp c1) + size (ccomp c2), t, stk')" |
|
537 by (fastforce dest: exec_n_drop_left simp: exits_Cons isuccs_def algebra_simps) |
|
538 |
|
539 show ?case |
|
540 proof (cases "bval b s") |
|
541 case True with cs' |
|
542 show ?thesis |
|
543 by simp |
|
544 (fastforce dest: exec_n_drop_right |
|
545 split: split_if_asm simp: exec_n_simps) |
|
546 next |
|
547 case False with cs' |
|
548 show ?thesis |
|
549 by (auto dest!: exec_n_drop_Cons exec_n_drop_left |
|
550 simp: exits_Cons isuccs_def) |
|
551 qed |
|
552 next |
|
553 case (While b c) |
|
554 |
|
555 from While.prems |
|
556 show ?case |
|
557 proof (induction n arbitrary: s rule: nat_less_induct) |
|
558 case (1 n) |
|
559 |
|
560 { assume "\<not> bval b s" |
|
561 with "1.prems" |
|
562 have ?case |
|
563 by simp |
|
564 (fastforce dest!: bcomp_exec_n bcomp_split |
|
565 simp: exec_n_simps) |
|
566 } moreover { |
|
567 assume b: "bval b s" |
|
568 let ?c0 = "WHILE b DO c" |
|
569 let ?cs = "ccomp ?c0" |
|
570 let ?bs = "bcomp b False (size (ccomp c) + 1)" |
|
571 let ?jmp = "[JMP (-((size ?bs + size (ccomp c) + 1)))]" |
|
572 |
|
573 from "1.prems" b |
|
574 obtain k where |
|
575 cs: "?cs \<turnstile> (size ?bs, s, stk) \<rightarrow>^k (size ?cs, t, stk')" and |
|
576 k: "k \<le> n" |
|
577 by (fastforce dest!: bcomp_split) |
|
578 |
|
579 have ?case |
|
580 proof cases |
|
581 assume "ccomp c = []" |
|
582 with cs k |
|
583 obtain m where |
|
584 "?cs \<turnstile> (0,s,stk) \<rightarrow>^m (size (ccomp ?c0), t, stk')" |
|
585 "m < n" |
|
586 by (auto simp: exec_n_step [where k=k]) |
|
587 with "1.IH" |
|
588 show ?case by blast |
|
589 next |
|
590 assume "ccomp c \<noteq> []" |
|
591 with cs |
|
592 obtain m m' s'' stk'' where |
|
593 c: "ccomp c \<turnstile> (0, s, stk) \<rightarrow>^m' (size (ccomp c), s'', stk'')" and |
|
594 rest: "?cs \<turnstile> (size ?bs + size (ccomp c), s'', stk'') \<rightarrow>^m |
|
595 (size ?cs, t, stk')" and |
|
596 m: "k = m + m'" |
|
597 by (auto dest: exec_n_split [where i=0, simplified]) |
|
598 from c |
|
599 have "(c,s) \<Rightarrow> s''" and stk: "stk'' = stk" |
|
600 by (auto dest!: While.IH) |
|
601 moreover |
|
602 from rest m k stk |
|
603 obtain k' where |
|
604 "?cs \<turnstile> (0, s'', stk) \<rightarrow>^k' (size ?cs, t, stk')" |
|
605 "k' < n" |
|
606 by (auto simp: exec_n_step [where k=m]) |
|
607 with "1.IH" |
|
608 have "(?c0, s'') \<Rightarrow> t \<and> stk' = stk" by blast |
|
609 ultimately |
|
610 show ?case using b by blast |
|
611 qed |
|
612 } |
|
613 ultimately show ?case by cases |
|
614 qed |
|
615 qed |
|
616 |
|
617 theorem ccomp_exec: |
|
618 "ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk') \<Longrightarrow> (c,s) \<Rightarrow> t" |
|
619 by (auto dest: exec_exec_n ccomp_exec_n) |
|
620 |
|
621 corollary ccomp_sound: |
|
622 "ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk) \<longleftrightarrow> (c,s) \<Rightarrow> t" |
|
623 by (blast intro!: ccomp_exec ccomp_bigstep) |
|
624 |
|
625 end |