12 ("_/ \<turnstile> (_ \<rightarrow>^_/ _)" [65,0,1000,55] 55) |
14 ("_/ \<turnstile> (_ \<rightarrow>^_/ _)" [65,0,1000,55] 55) |
13 where |
15 where |
14 "P \<turnstile> c \<rightarrow>^0 c' = (c'=c)" | |
16 "P \<turnstile> c \<rightarrow>^0 c' = (c'=c)" | |
15 "P \<turnstile> c \<rightarrow>^(Suc n) c'' = (\<exists>c'. (P \<turnstile> c \<rightarrow> c') \<and> P \<turnstile> c' \<rightarrow>^n c'')" |
17 "P \<turnstile> c \<rightarrow>^(Suc n) c'' = (\<exists>c'. (P \<turnstile> c \<rightarrow> c') \<and> P \<turnstile> c' \<rightarrow>^n c'')" |
16 |
18 |
17 text {* The possible successor pc's of an instruction at position @{term n} *} |
19 text {* The possible successor PCs of an instruction at position @{term n} *} |
18 definition |
20 definition |
19 "isuccs i n \<equiv> case i of |
21 "isuccs i n \<equiv> case i of |
20 JMP j \<Rightarrow> {n + 1 + j} |
22 JMP j \<Rightarrow> {n + 1 + j} |
21 | JMPLESS j \<Rightarrow> {n + 1 + j, n + 1} |
23 | JMPLESS j \<Rightarrow> {n + 1 + j, n + 1} |
22 | JMPGE j \<Rightarrow> {n + 1 + j, n + 1} |
24 | JMPGE j \<Rightarrow> {n + 1 + j, n + 1} |
23 | _ \<Rightarrow> {n +1}" |
25 | _ \<Rightarrow> {n +1}" |
24 |
26 |
25 text {* The possible successors pc's of an instruction list *} |
27 text {* The possible successors PCs of an instruction list *} |
26 definition |
28 definition |
27 "succs P n = {s. \<exists>i. 0 \<le> i \<and> i < isize P \<and> s \<in> isuccs (P!!i) (n+i)}" |
29 succs :: "instr list \<Rightarrow> int \<Rightarrow> int set" where |
28 |
30 "succs P n = {s. \<exists>i::int. 0 \<le> i \<and> i < size P \<and> s \<in> isuccs (P!!i) (n+i)}" |
29 text {* Possible exit pc's of a program *} |
31 |
|
32 text {* Possible exit PCs of a program *} |
30 definition |
33 definition |
31 "exits P = succs P 0 - {0..< isize P}" |
34 "exits P = succs P 0 - {0..< size P}" |
32 |
35 |
33 |
36 |
34 subsection {* Basic properties of @{term exec_n} *} |
37 subsection {* Basic properties of @{term exec_n} *} |
35 |
38 |
36 lemma exec_n_exec: |
39 lemma exec_n_exec: |
147 lemma succs_set_shift [simp]: |
150 lemma succs_set_shift [simp]: |
148 "op + i ` succs xs 0 = succs xs i" |
151 "op + i ` succs xs 0 = succs xs i" |
149 by (force simp: succs_shift [where n=i, symmetric] intro: set_eqI) |
152 by (force simp: succs_shift [where n=i, symmetric] intro: set_eqI) |
150 |
153 |
151 lemma succs_append [simp]: |
154 lemma succs_append [simp]: |
152 "succs (xs @ ys) n = succs xs n \<union> succs ys (n + isize xs)" |
155 "succs (xs @ ys) n = succs xs n \<union> succs ys (n + size xs)" |
153 by (induct xs arbitrary: n) (auto simp: succs_Cons algebra_simps) |
156 by (induct xs arbitrary: n) (auto simp: succs_Cons algebra_simps) |
154 |
157 |
155 |
158 |
156 lemma exits_append [simp]: |
159 lemma exits_append [simp]: |
157 "exits (xs @ ys) = exits xs \<union> (op + (isize xs)) ` exits ys - |
160 "exits (xs @ ys) = exits xs \<union> (op + (size xs)) ` exits ys - |
158 {0..<isize xs + isize ys}" |
161 {0..<size xs + size ys}" |
159 by (auto simp: exits_def image_set_diff) |
162 by (auto simp: exits_def image_set_diff) |
160 |
163 |
161 lemma exits_single: |
164 lemma exits_single: |
162 "exits [x] = isuccs x 0 - {0}" |
165 "exits [x] = isuccs x 0 - {0}" |
163 by (auto simp: exits_def succs_def) |
166 by (auto simp: exits_def succs_def) |
164 |
167 |
165 lemma exits_Cons: |
168 lemma exits_Cons: |
166 "exits (x # xs) = (isuccs x 0 - {0}) \<union> (op + 1) ` exits xs - |
169 "exits (x # xs) = (isuccs x 0 - {0}) \<union> (op + 1) ` exits xs - |
167 {0..<1 + isize xs}" |
170 {0..<1 + size xs}" |
168 using exits_append [of "[x]" xs] |
171 using exits_append [of "[x]" xs] |
169 by (simp add: exits_single) |
172 by (simp add: exits_single) |
170 |
173 |
171 lemma exits_empty [iff]: "exits [] = {}" by (simp add: exits_def) |
174 lemma exits_empty [iff]: "exits [] = {}" by (simp add: exits_def) |
172 |
175 |
238 from While.prems |
243 from While.prems |
239 show ?case by (auto dest!: While.IH [THEN subsetD]) |
244 show ?case by (auto dest!: While.IH [THEN subsetD]) |
240 qed |
245 qed |
241 |
246 |
242 lemma ccomp_exits: |
247 lemma ccomp_exits: |
243 "exits (ccomp c) \<subseteq> {isize (ccomp c)}" |
248 "exits (ccomp c) \<subseteq> {size (ccomp c)}" |
244 using ccomp_succs [of c 0] by (auto simp: exits_def) |
249 using ccomp_succs [of c 0] by (auto simp: exits_def) |
245 |
250 |
246 lemma ccomp_exitsD [dest!]: |
251 lemma ccomp_exitsD [dest!]: |
247 "p \<in> exits (ccomp c) \<Longrightarrow> p = isize (ccomp c)" |
252 "p \<in> exits (ccomp c) \<Longrightarrow> p = size (ccomp c)" |
248 using ccomp_exits by auto |
253 using ccomp_exits by auto |
249 |
254 |
250 |
255 |
251 subsection {* Splitting up machine executions *} |
256 subsection {* Splitting up machine executions *} |
252 |
257 |
253 lemma exec1_split: |
258 lemma exec1_split: |
254 "P @ c @ P' \<turnstile> (isize P + i, s) \<rightarrow> (j,s') \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < isize c \<Longrightarrow> |
259 fixes i j :: int |
255 c \<turnstile> (i,s) \<rightarrow> (j - isize P, s')" |
260 shows |
|
261 "P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow> (j,s') \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < size c \<Longrightarrow> |
|
262 c \<turnstile> (i,s) \<rightarrow> (j - size P, s')" |
256 by (auto split: instr.splits) |
263 by (auto split: instr.splits) |
257 |
264 |
258 lemma exec_n_split: |
265 lemma exec_n_split: |
259 assumes "P @ c @ P' \<turnstile> (isize P + i, s) \<rightarrow>^n (j, s')" |
266 fixes i j :: int |
260 "0 \<le> i" "i < isize c" |
267 assumes "P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow>^n (j, s')" |
261 "j \<notin> {isize P ..< isize P + isize c}" |
268 "0 \<le> i" "i < size c" |
262 shows "\<exists>s'' i' k m. |
269 "j \<notin> {size P ..< size P + size c}" |
|
270 shows "\<exists>s'' (i'::int) k m. |
263 c \<turnstile> (i, s) \<rightarrow>^k (i', s'') \<and> |
271 c \<turnstile> (i, s) \<rightarrow>^k (i', s'') \<and> |
264 i' \<in> exits c \<and> |
272 i' \<in> exits c \<and> |
265 P @ c @ P' \<turnstile> (isize P + i', s'') \<rightarrow>^m (j, s') \<and> |
273 P @ c @ P' \<turnstile> (size P + i', s'') \<rightarrow>^m (j, s') \<and> |
266 n = k + m" |
274 n = k + m" |
267 using assms proof (induction n arbitrary: i j s) |
275 using assms proof (induction n arbitrary: i j s) |
268 case 0 |
276 case 0 |
269 thus ?case by simp |
277 thus ?case by simp |
270 next |
278 next |
271 case (Suc n) |
279 case (Suc n) |
272 have i: "0 \<le> i" "i < isize c" by fact+ |
280 have i: "0 \<le> i" "i < size c" by fact+ |
273 from Suc.prems |
281 from Suc.prems |
274 have j: "\<not> (isize P \<le> j \<and> j < isize P + isize c)" by simp |
282 have j: "\<not> (size P \<le> j \<and> j < size P + size c)" by simp |
275 from Suc.prems |
283 from Suc.prems |
276 obtain i0 s0 where |
284 obtain i0 s0 where |
277 step: "P @ c @ P' \<turnstile> (isize P + i, s) \<rightarrow> (i0,s0)" and |
285 step: "P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow> (i0,s0)" and |
278 rest: "P @ c @ P' \<turnstile> (i0,s0) \<rightarrow>^n (j, s')" |
286 rest: "P @ c @ P' \<turnstile> (i0,s0) \<rightarrow>^n (j, s')" |
279 by clarsimp |
287 by clarsimp |
280 |
288 |
281 from step i |
289 from step i |
282 have c: "c \<turnstile> (i,s) \<rightarrow> (i0 - isize P, s0)" by (rule exec1_split) |
290 have c: "c \<turnstile> (i,s) \<rightarrow> (i0 - size P, s0)" by (rule exec1_split) |
283 |
291 |
284 have "i0 = isize P + (i0 - isize P) " by simp |
292 have "i0 = size P + (i0 - size P) " by simp |
285 then obtain j0 where j0: "i0 = isize P + j0" .. |
293 then obtain j0::int where j0: "i0 = size P + j0" .. |
286 |
294 |
287 note split_paired_Ex [simp del] |
295 note split_paired_Ex [simp del] |
288 |
296 |
289 { assume "j0 \<in> {0 ..< isize c}" |
297 { assume "j0 \<in> {0 ..< size c}" |
290 with j0 j rest c |
298 with j0 j rest c |
291 have ?case |
299 have ?case |
292 by (fastforce dest!: Suc.IH intro!: exec_Suc) |
300 by (fastforce dest!: Suc.IH intro!: exec_Suc) |
293 } moreover { |
301 } moreover { |
294 assume "j0 \<notin> {0 ..< isize c}" |
302 assume "j0 \<notin> {0 ..< size c}" |
295 moreover |
303 moreover |
296 from c j0 have "j0 \<in> succs c 0" |
304 from c j0 have "j0 \<in> succs c 0" |
297 by (auto dest: succs_iexec1 simp del: iexec.simps) |
305 by (auto dest: succs_iexec1 simp del: iexec.simps) |
298 ultimately |
306 ultimately |
299 have "j0 \<in> exits c" by (simp add: exits_def) |
307 have "j0 \<in> exits c" by (simp add: exits_def) |
320 text {* |
329 text {* |
321 Dropping the left context of a potentially incomplete execution of @{term c}. |
330 Dropping the left context of a potentially incomplete execution of @{term c}. |
322 *} |
331 *} |
323 |
332 |
324 lemma exec1_drop_left: |
333 lemma exec1_drop_left: |
325 assumes "P1 @ P2 \<turnstile> (i, s, stk) \<rightarrow> (n, s', stk')" and "isize P1 \<le> i" |
334 fixes i n :: int |
326 shows "P2 \<turnstile> (i - isize P1, s, stk) \<rightarrow> (n - isize P1, s', stk')" |
335 assumes "P1 @ P2 \<turnstile> (i, s, stk) \<rightarrow> (n, s', stk')" and "size P1 \<le> i" |
|
336 shows "P2 \<turnstile> (i - size P1, s, stk) \<rightarrow> (n - size P1, s', stk')" |
327 proof - |
337 proof - |
328 have "i = isize P1 + (i - isize P1)" by simp |
338 have "i = size P1 + (i - size P1)" by simp |
329 then obtain i' where "i = isize P1 + i'" .. |
339 then obtain i' :: int where "i = size P1 + i'" .. |
330 moreover |
340 moreover |
331 have "n = isize P1 + (n - isize P1)" by simp |
341 have "n = size P1 + (n - size P1)" by simp |
332 then obtain n' where "n = isize P1 + n'" .. |
342 then obtain n' :: int where "n = size P1 + n'" .. |
333 ultimately |
343 ultimately |
334 show ?thesis using assms by (clarsimp simp del: iexec.simps) |
344 show ?thesis using assms by (clarsimp simp del: iexec.simps) |
335 qed |
345 qed |
336 |
346 |
337 lemma exec_n_drop_left: |
347 lemma exec_n_drop_left: |
|
348 fixes i n :: int |
338 assumes "P @ P' \<turnstile> (i, s, stk) \<rightarrow>^k (n, s', stk')" |
349 assumes "P @ P' \<turnstile> (i, s, stk) \<rightarrow>^k (n, s', stk')" |
339 "isize P \<le> i" "exits P' \<subseteq> {0..}" |
350 "size P \<le> i" "exits P' \<subseteq> {0..}" |
340 shows "P' \<turnstile> (i - isize P, s, stk) \<rightarrow>^k (n - isize P, s', stk')" |
351 shows "P' \<turnstile> (i - size P, s, stk) \<rightarrow>^k (n - size P, s', stk')" |
341 using assms proof (induction k arbitrary: i s stk) |
352 using assms proof (induction k arbitrary: i s stk) |
342 case 0 thus ?case by simp |
353 case 0 thus ?case by simp |
343 next |
354 next |
344 case (Suc k) |
355 case (Suc k) |
345 from Suc.prems |
356 from Suc.prems |
346 obtain i' s'' stk'' where |
357 obtain i' s'' stk'' where |
347 step: "P @ P' \<turnstile> (i, s, stk) \<rightarrow> (i', s'', stk'')" and |
358 step: "P @ P' \<turnstile> (i, s, stk) \<rightarrow> (i', s'', stk'')" and |
348 rest: "P @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^k (n, s', stk')" |
359 rest: "P @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^k (n, s', stk')" |
349 by (auto simp del: exec1_def) |
360 by (auto simp del: exec1_def) |
350 from step `isize P \<le> i` |
361 from step `size P \<le> i` |
351 have "P' \<turnstile> (i - isize P, s, stk) \<rightarrow> (i' - isize P, s'', stk'')" |
362 have "P' \<turnstile> (i - size P, s, stk) \<rightarrow> (i' - size P, s'', stk'')" |
352 by (rule exec1_drop_left) |
363 by (rule exec1_drop_left) |
353 moreover |
364 moreover |
354 then have "i' - isize P \<in> succs P' 0" |
365 then have "i' - size P \<in> succs P' 0" |
355 by (fastforce dest!: succs_iexec1 simp del: iexec.simps) |
366 by (fastforce dest!: succs_iexec1 simp del: iexec.simps) |
356 with `exits P' \<subseteq> {0..}` |
367 with `exits P' \<subseteq> {0..}` |
357 have "isize P \<le> i'" by (auto simp: exits_def) |
368 have "size P \<le> i'" by (auto simp: exits_def) |
358 from rest this `exits P' \<subseteq> {0..}` |
369 from rest this `exits P' \<subseteq> {0..}` |
359 have "P' \<turnstile> (i' - isize P, s'', stk'') \<rightarrow>^k (n - isize P, s', stk')" |
370 have "P' \<turnstile> (i' - size P, s'', stk'') \<rightarrow>^k (n - size P, s', stk')" |
360 by (rule Suc.IH) |
371 by (rule Suc.IH) |
361 ultimately |
372 ultimately |
362 show ?case by auto |
373 show ?case by auto |
363 qed |
374 qed |
364 |
375 |
365 lemmas exec_n_drop_Cons = |
376 lemmas exec_n_drop_Cons = |
366 exec_n_drop_left [where P="[instr]", simplified] for instr |
377 exec_n_drop_left [where P="[instr]", simplified] for instr |
367 |
378 |
368 definition |
379 definition |
369 "closed P \<longleftrightarrow> exits P \<subseteq> {isize P}" |
380 "closed P \<longleftrightarrow> exits P \<subseteq> {size P}" |
370 |
381 |
371 lemma ccomp_closed [simp, intro!]: "closed (ccomp c)" |
382 lemma ccomp_closed [simp, intro!]: "closed (ccomp c)" |
372 using ccomp_exits by (auto simp: closed_def) |
383 using ccomp_exits by (auto simp: closed_def) |
373 |
384 |
374 lemma acomp_closed [simp, intro!]: "closed (acomp c)" |
385 lemma acomp_closed [simp, intro!]: "closed (acomp c)" |
375 by (simp add: closed_def) |
386 by (simp add: closed_def) |
376 |
387 |
377 lemma exec_n_split_full: |
388 lemma exec_n_split_full: |
|
389 fixes j :: int |
378 assumes exec: "P @ P' \<turnstile> (0,s,stk) \<rightarrow>^k (j, s', stk')" |
390 assumes exec: "P @ P' \<turnstile> (0,s,stk) \<rightarrow>^k (j, s', stk')" |
379 assumes P: "isize P \<le> j" |
391 assumes P: "size P \<le> j" |
380 assumes closed: "closed P" |
392 assumes closed: "closed P" |
381 assumes exits: "exits P' \<subseteq> {0..}" |
393 assumes exits: "exits P' \<subseteq> {0..}" |
382 shows "\<exists>k1 k2 s'' stk''. P \<turnstile> (0,s,stk) \<rightarrow>^k1 (isize P, s'', stk'') \<and> |
394 shows "\<exists>k1 k2 s'' stk''. P \<turnstile> (0,s,stk) \<rightarrow>^k1 (size P, s'', stk'') \<and> |
383 P' \<turnstile> (0,s'',stk'') \<rightarrow>^k2 (j - isize P, s', stk')" |
395 P' \<turnstile> (0,s'',stk'') \<rightarrow>^k2 (j - size P, s', stk')" |
384 proof (cases "P") |
396 proof (cases "P") |
385 case Nil with exec |
397 case Nil with exec |
386 show ?thesis by fastforce |
398 show ?thesis by fastforce |
387 next |
399 next |
388 case Cons |
400 case Cons |
389 hence "0 < isize P" by simp |
401 hence "0 < size P" by simp |
390 with exec P closed |
402 with exec P closed |
391 obtain k1 k2 s'' stk'' where |
403 obtain k1 k2 s'' stk'' where |
392 1: "P \<turnstile> (0,s,stk) \<rightarrow>^k1 (isize P, s'', stk'')" and |
404 1: "P \<turnstile> (0,s,stk) \<rightarrow>^k1 (size P, s'', stk'')" and |
393 2: "P @ P' \<turnstile> (isize P,s'',stk'') \<rightarrow>^k2 (j, s', stk')" |
405 2: "P @ P' \<turnstile> (size P,s'',stk'') \<rightarrow>^k2 (j, s', stk')" |
394 by (auto dest!: exec_n_split [where P="[]" and i=0, simplified] |
406 by (auto dest!: exec_n_split [where P="[]" and i=0, simplified] |
395 simp: closed_def) |
407 simp: closed_def) |
396 moreover |
408 moreover |
397 have "j = isize P + (j - isize P)" by simp |
409 have "j = size P + (j - size P)" by simp |
398 then obtain j0 where "j = isize P + j0" .. |
410 then obtain j0 :: int where "j = size P + j0" .. |
399 ultimately |
411 ultimately |
400 show ?thesis using exits |
412 show ?thesis using exits |
401 by (fastforce dest: exec_n_drop_left) |
413 by (fastforce dest: exec_n_drop_left) |
402 qed |
414 qed |
403 |
415 |
407 lemma acomp_neq_Nil [simp]: |
419 lemma acomp_neq_Nil [simp]: |
408 "acomp a \<noteq> []" |
420 "acomp a \<noteq> []" |
409 by (induct a) auto |
421 by (induct a) auto |
410 |
422 |
411 lemma acomp_exec_n [dest!]: |
423 lemma acomp_exec_n [dest!]: |
412 "acomp a \<turnstile> (0,s,stk) \<rightarrow>^n (isize (acomp a),s',stk') \<Longrightarrow> |
424 "acomp a \<turnstile> (0,s,stk) \<rightarrow>^n (size (acomp a),s',stk') \<Longrightarrow> |
413 s' = s \<and> stk' = aval a s#stk" |
425 s' = s \<and> stk' = aval a s#stk" |
414 proof (induction a arbitrary: n s' stk stk') |
426 proof (induction a arbitrary: n s' stk stk') |
415 case (Plus a1 a2) |
427 case (Plus a1 a2) |
416 let ?sz = "isize (acomp a1) + (isize (acomp a2) + 1)" |
428 let ?sz = "size (acomp a1) + (size (acomp a2) + 1)" |
417 from Plus.prems |
429 from Plus.prems |
418 have "acomp a1 @ acomp a2 @ [ADD] \<turnstile> (0,s,stk) \<rightarrow>^n (?sz, s', stk')" |
430 have "acomp a1 @ acomp a2 @ [ADD] \<turnstile> (0,s,stk) \<rightarrow>^n (?sz, s', stk')" |
419 by (simp add: algebra_simps) |
431 by (simp add: algebra_simps) |
420 |
432 |
421 then obtain n1 s1 stk1 n2 s2 stk2 n3 where |
433 then obtain n1 s1 stk1 n2 s2 stk2 n3 where |
422 "acomp a1 \<turnstile> (0,s,stk) \<rightarrow>^n1 (isize (acomp a1), s1, stk1)" |
434 "acomp a1 \<turnstile> (0,s,stk) \<rightarrow>^n1 (size (acomp a1), s1, stk1)" |
423 "acomp a2 \<turnstile> (0,s1,stk1) \<rightarrow>^n2 (isize (acomp a2), s2, stk2)" |
435 "acomp a2 \<turnstile> (0,s1,stk1) \<rightarrow>^n2 (size (acomp a2), s2, stk2)" |
424 "[ADD] \<turnstile> (0,s2,stk2) \<rightarrow>^n3 (1, s', stk')" |
436 "[ADD] \<turnstile> (0,s2,stk2) \<rightarrow>^n3 (1, s', stk')" |
425 by (auto dest!: exec_n_split_full) |
437 by (auto dest!: exec_n_split_full) |
426 |
438 |
427 thus ?case by (fastforce dest: Plus.IH simp: exec_n_simps) |
439 thus ?case by (fastforce dest: Plus.IH simp: exec_n_simps) |
428 qed (auto simp: exec_n_simps) |
440 qed (auto simp: exec_n_simps) |
429 |
441 |
430 lemma bcomp_split: |
442 lemma bcomp_split: |
|
443 fixes i j :: int |
431 assumes "bcomp b c i @ P' \<turnstile> (0, s, stk) \<rightarrow>^n (j, s', stk')" |
444 assumes "bcomp b c i @ P' \<turnstile> (0, s, stk) \<rightarrow>^n (j, s', stk')" |
432 "j \<notin> {0..<isize (bcomp b c i)}" "0 \<le> i" |
445 "j \<notin> {0..<size (bcomp b c i)}" "0 \<le> i" |
433 shows "\<exists>s'' stk'' i' k m. |
446 shows "\<exists>s'' stk'' (i'::int) k m. |
434 bcomp b c i \<turnstile> (0, s, stk) \<rightarrow>^k (i', s'', stk'') \<and> |
447 bcomp b c i \<turnstile> (0, s, stk) \<rightarrow>^k (i', s'', stk'') \<and> |
435 (i' = isize (bcomp b c i) \<or> i' = i + isize (bcomp b c i)) \<and> |
448 (i' = size (bcomp b c i) \<or> i' = i + size (bcomp b c i)) \<and> |
436 bcomp b c i @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^m (j, s', stk') \<and> |
449 bcomp b c i @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^m (j, s', stk') \<and> |
437 n = k + m" |
450 n = k + m" |
438 using assms by (cases "bcomp b c i = []") (fastforce dest!: exec_n_drop_right)+ |
451 using assms by (cases "bcomp b c i = []") (fastforce dest!: exec_n_drop_right)+ |
439 |
452 |
440 lemma bcomp_exec_n [dest]: |
453 lemma bcomp_exec_n [dest]: |
|
454 fixes i j :: int |
441 assumes "bcomp b c j \<turnstile> (0, s, stk) \<rightarrow>^n (i, s', stk')" |
455 assumes "bcomp b c j \<turnstile> (0, s, stk) \<rightarrow>^n (i, s', stk')" |
442 "isize (bcomp b c j) \<le> i" "0 \<le> j" |
456 "size (bcomp b c j) \<le> i" "0 \<le> j" |
443 shows "i = isize(bcomp b c j) + (if c = bval b s then j else 0) \<and> |
457 shows "i = size(bcomp b c j) + (if c = bval b s then j else 0) \<and> |
444 s' = s \<and> stk' = stk" |
458 s' = s \<and> stk' = stk" |
445 using assms proof (induction b arbitrary: c j i n s' stk') |
459 using assms proof (induction b arbitrary: c j i n s' stk') |
446 case Bc thus ?case |
460 case Bc thus ?case |
447 by (simp split: split_if_asm add: exec_n_simps) |
461 by (simp split: split_if_asm add: exec_n_simps) |
448 next |
462 next |
451 by (fastforce dest!: Not.IH) |
465 by (fastforce dest!: Not.IH) |
452 next |
466 next |
453 case (And b1 b2) |
467 case (And b1 b2) |
454 |
468 |
455 let ?b2 = "bcomp b2 c j" |
469 let ?b2 = "bcomp b2 c j" |
456 let ?m = "if c then isize ?b2 else isize ?b2 + j" |
470 let ?m = "if c then size ?b2 else size ?b2 + j" |
457 let ?b1 = "bcomp b1 False ?m" |
471 let ?b1 = "bcomp b1 False ?m" |
458 |
472 |
459 have j: "isize (bcomp (And b1 b2) c j) \<le> i" "0 \<le> j" by fact+ |
473 have j: "size (bcomp (And b1 b2) c j) \<le> i" "0 \<le> j" by fact+ |
460 |
474 |
461 from And.prems |
475 from And.prems |
462 obtain s'' stk'' i' k m where |
476 obtain s'' stk'' and i'::int and k m where |
463 b1: "?b1 \<turnstile> (0, s, stk) \<rightarrow>^k (i', s'', stk'')" |
477 b1: "?b1 \<turnstile> (0, s, stk) \<rightarrow>^k (i', s'', stk'')" |
464 "i' = isize ?b1 \<or> i' = ?m + isize ?b1" and |
478 "i' = size ?b1 \<or> i' = ?m + size ?b1" and |
465 b2: "?b2 \<turnstile> (i' - isize ?b1, s'', stk'') \<rightarrow>^m (i - isize ?b1, s', stk')" |
479 b2: "?b2 \<turnstile> (i' - size ?b1, s'', stk'') \<rightarrow>^m (i - size ?b1, s', stk')" |
466 by (auto dest!: bcomp_split dest: exec_n_drop_left) |
480 by (auto dest!: bcomp_split dest: exec_n_drop_left) |
467 from b1 j |
481 from b1 j |
468 have "i' = isize ?b1 + (if \<not>bval b1 s then ?m else 0) \<and> s'' = s \<and> stk'' = stk" |
482 have "i' = size ?b1 + (if \<not>bval b1 s then ?m else 0) \<and> s'' = s \<and> stk'' = stk" |
469 by (auto dest!: And.IH) |
483 by (auto dest!: And.IH) |
470 with b2 j |
484 with b2 j |
471 show ?case |
485 show ?case |
472 by (fastforce dest!: And.IH simp: exec_n_end split: split_if_asm) |
486 by (fastforce dest!: And.IH simp: exec_n_end split: split_if_asm) |
473 next |
487 next |
498 case (If b c1 c2) |
512 case (If b c1 c2) |
499 note If.IH [dest!] |
513 note If.IH [dest!] |
500 |
514 |
501 let ?if = "IF b THEN c1 ELSE c2" |
515 let ?if = "IF b THEN c1 ELSE c2" |
502 let ?cs = "ccomp ?if" |
516 let ?cs = "ccomp ?if" |
503 let ?bcomp = "bcomp b False (isize (ccomp c1) + 1)" |
517 let ?bcomp = "bcomp b False (size (ccomp c1) + 1)" |
504 |
518 |
505 from `?cs \<turnstile> (0,s,stk) \<rightarrow>^n (isize ?cs,t,stk')` |
519 from `?cs \<turnstile> (0,s,stk) \<rightarrow>^n (size ?cs,t,stk')` |
506 obtain i' k m s'' stk'' where |
520 obtain i' :: int and k m s'' stk'' where |
507 cs: "?cs \<turnstile> (i',s'',stk'') \<rightarrow>^m (isize ?cs,t,stk')" and |
521 cs: "?cs \<turnstile> (i',s'',stk'') \<rightarrow>^m (size ?cs,t,stk')" and |
508 "?bcomp \<turnstile> (0,s,stk) \<rightarrow>^k (i', s'', stk'')" |
522 "?bcomp \<turnstile> (0,s,stk) \<rightarrow>^k (i', s'', stk'')" |
509 "i' = isize ?bcomp \<or> i' = isize ?bcomp + isize (ccomp c1) + 1" |
523 "i' = size ?bcomp \<or> i' = size ?bcomp + size (ccomp c1) + 1" |
510 by (auto dest!: bcomp_split) |
524 by (auto dest!: bcomp_split) |
511 |
525 |
512 hence i': |
526 hence i': |
513 "s''=s" "stk'' = stk" |
527 "s''=s" "stk'' = stk" |
514 "i' = (if bval b s then isize ?bcomp else isize ?bcomp+isize(ccomp c1)+1)" |
528 "i' = (if bval b s then size ?bcomp else size ?bcomp+size(ccomp c1)+1)" |
515 by auto |
529 by auto |
516 |
530 |
517 with cs have cs': |
531 with cs have cs': |
518 "ccomp c1@JMP (isize (ccomp c2))#ccomp c2 \<turnstile> |
532 "ccomp c1@JMP (size (ccomp c2))#ccomp c2 \<turnstile> |
519 (if bval b s then 0 else isize (ccomp c1)+1, s, stk) \<rightarrow>^m |
533 (if bval b s then 0 else size (ccomp c1)+1, s, stk) \<rightarrow>^m |
520 (1 + isize (ccomp c1) + isize (ccomp c2), t, stk')" |
534 (1 + size (ccomp c1) + size (ccomp c2), t, stk')" |
521 by (fastforce dest: exec_n_drop_left simp: exits_Cons isuccs_def algebra_simps) |
535 by (fastforce dest: exec_n_drop_left simp: exits_Cons isuccs_def algebra_simps) |
522 |
536 |
523 show ?case |
537 show ?case |
524 proof (cases "bval b s") |
538 proof (cases "bval b s") |
525 case True with cs' |
539 case True with cs' |
549 simp: exec_n_simps) |
563 simp: exec_n_simps) |
550 } moreover { |
564 } moreover { |
551 assume b: "bval b s" |
565 assume b: "bval b s" |
552 let ?c0 = "WHILE b DO c" |
566 let ?c0 = "WHILE b DO c" |
553 let ?cs = "ccomp ?c0" |
567 let ?cs = "ccomp ?c0" |
554 let ?bs = "bcomp b False (isize (ccomp c) + 1)" |
568 let ?bs = "bcomp b False (size (ccomp c) + 1)" |
555 let ?jmp = "[JMP (-((isize ?bs + isize (ccomp c) + 1)))]" |
569 let ?jmp = "[JMP (-((size ?bs + size (ccomp c) + 1)))]" |
556 |
570 |
557 from "1.prems" b |
571 from "1.prems" b |
558 obtain k where |
572 obtain k where |
559 cs: "?cs \<turnstile> (isize ?bs, s, stk) \<rightarrow>^k (isize ?cs, t, stk')" and |
573 cs: "?cs \<turnstile> (size ?bs, s, stk) \<rightarrow>^k (size ?cs, t, stk')" and |
560 k: "k \<le> n" |
574 k: "k \<le> n" |
561 by (fastforce dest!: bcomp_split) |
575 by (fastforce dest!: bcomp_split) |
562 |
576 |
563 have ?case |
577 have ?case |
564 proof cases |
578 proof cases |
565 assume "ccomp c = []" |
579 assume "ccomp c = []" |
566 with cs k |
580 with cs k |
567 obtain m where |
581 obtain m where |
568 "?cs \<turnstile> (0,s,stk) \<rightarrow>^m (isize (ccomp ?c0), t, stk')" |
582 "?cs \<turnstile> (0,s,stk) \<rightarrow>^m (size (ccomp ?c0), t, stk')" |
569 "m < n" |
583 "m < n" |
570 by (auto simp: exec_n_step [where k=k]) |
584 by (auto simp: exec_n_step [where k=k]) |
571 with "1.IH" |
585 with "1.IH" |
572 show ?case by blast |
586 show ?case by blast |
573 next |
587 next |
574 assume "ccomp c \<noteq> []" |
588 assume "ccomp c \<noteq> []" |
575 with cs |
589 with cs |
576 obtain m m' s'' stk'' where |
590 obtain m m' s'' stk'' where |
577 c: "ccomp c \<turnstile> (0, s, stk) \<rightarrow>^m' (isize (ccomp c), s'', stk'')" and |
591 c: "ccomp c \<turnstile> (0, s, stk) \<rightarrow>^m' (size (ccomp c), s'', stk'')" and |
578 rest: "?cs \<turnstile> (isize ?bs + isize (ccomp c), s'', stk'') \<rightarrow>^m |
592 rest: "?cs \<turnstile> (size ?bs + size (ccomp c), s'', stk'') \<rightarrow>^m |
579 (isize ?cs, t, stk')" and |
593 (size ?cs, t, stk')" and |
580 m: "k = m + m'" |
594 m: "k = m + m'" |
581 by (auto dest: exec_n_split [where i=0, simplified]) |
595 by (auto dest: exec_n_split [where i=0, simplified]) |
582 from c |
596 from c |
583 have "(c,s) \<Rightarrow> s''" and stk: "stk'' = stk" |
597 have "(c,s) \<Rightarrow> s''" and stk: "stk'' = stk" |
584 by (auto dest!: While.IH) |
598 by (auto dest!: While.IH) |
585 moreover |
599 moreover |
586 from rest m k stk |
600 from rest m k stk |
587 obtain k' where |
601 obtain k' where |
588 "?cs \<turnstile> (0, s'', stk) \<rightarrow>^k' (isize ?cs, t, stk')" |
602 "?cs \<turnstile> (0, s'', stk) \<rightarrow>^k' (size ?cs, t, stk')" |
589 "k' < n" |
603 "k' < n" |
590 by (auto simp: exec_n_step [where k=m]) |
604 by (auto simp: exec_n_step [where k=m]) |
591 with "1.IH" |
605 with "1.IH" |
592 have "(?c0, s'') \<Rightarrow> t \<and> stk' = stk" by blast |
606 have "(?c0, s'') \<Rightarrow> t \<and> stk' = stk" by blast |
593 ultimately |
607 ultimately |