226 apply(auto simp: tm_comp_length nth_append) |
226 apply(auto simp: tm_comp_length nth_append) |
227 done |
227 done |
228 then show "step0 c (A |+| B) = step0 c A" by (simp add: eq) |
228 then show "step0 c (A |+| B) = step0 c A" by (simp add: eq) |
229 qed |
229 qed |
230 |
230 |
231 lemma tm_comp_pre_eq: |
231 lemma tm_comp_step: |
232 assumes "\<not> is_final (steps0 (1, tp) A n)" |
232 assumes "\<not> is_final (steps0 c A n)" |
233 shows "steps0 (1, tp) (A |+| B) n = steps0 (1, tp) A n" |
233 shows "steps0 c (A |+| B) n = steps0 c A n" |
234 using assms |
234 using assms |
235 proof(induct n) |
235 proof(induct n) |
236 case 0 |
236 case 0 |
237 then show "steps0 (1, tp) (A |+| B) 0 = steps0 (1, tp) A 0" by auto |
237 then show "steps0 c (A |+| B) 0 = steps0 c A 0" by auto |
238 next |
238 next |
239 case (Suc n) |
239 case (Suc n) |
240 have ih: "\<not> is_final (steps0 (1, tp) A n) \<Longrightarrow> steps0 (1, tp) (A |+| B) n = steps0 (1, tp) A n" by fact |
240 have ih: "\<not> is_final (steps0 c A n) \<Longrightarrow> steps0 c (A |+| B) n = steps0 c A n" by fact |
241 have fin: "\<not> is_final (steps0 (1, tp) A (Suc n))" by fact |
241 have fin: "\<not> is_final (steps0 c A (Suc n))" by fact |
242 then have fin1: "\<not> is_final (step0 (steps0 (1, tp) A n) A)" |
242 then have fin1: "\<not> is_final (step0 (steps0 c A n) A)" |
243 by (auto simp only: step_red) |
243 by (auto simp only: step_red) |
244 then have fin2: "\<not> is_final (steps0 (1, tp) A n)" |
244 then have fin2: "\<not> is_final (steps0 c A n)" |
245 by (metis is_final_eq step_0 surj_pair) |
245 by (metis is_final_eq step_0 surj_pair) |
246 |
246 |
247 have "steps0 (1, tp) (A |+| B) (Suc n) = step0 (steps0 (1, tp) (A |+| B) n) (A |+| B)" |
247 have "steps0 c (A |+| B) (Suc n) = step0 (steps0 c (A |+| B) n) (A |+| B)" |
248 by (simp only: step_red) |
248 by (simp only: step_red) |
249 also have "... = step0 (steps0 (1, tp) A n) (A |+| B)" by (simp only: ih[OF fin2]) |
249 also have "... = step0 (steps0 c A n) (A |+| B)" by (simp only: ih[OF fin2]) |
250 also have "... = step0 (steps0 (1, tp) A n) A" by (simp only: tm_comp_pre_eq_step[OF fin1]) |
250 also have "... = step0 (steps0 c A n) A" by (simp only: tm_comp_step_aux[OF fin1]) |
251 finally show "steps0 (1, tp) (A |+| B) (Suc n) = steps0 (1, tp) A (Suc n)" |
251 finally show "steps0 c (A |+| B) (Suc n) = steps0 c A (Suc n)" |
252 by (simp only: step_red) |
252 by (simp only: step_red) |
253 qed |
253 qed |
254 |
254 |
255 declare steps.simps[simp del] |
255 lemma tm_comp_fetch_in_A: |
256 declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del] |
256 assumes h1: "fetch A s x = (a, 0)" |
257 declare tm_wf.simps[simp del] step.simps[simp del] |
257 and h2: "s \<le> length A div 2" |
258 |
258 and h3: "s \<noteq> 0" |
259 lemma tmcomp_fetch_in_first2: |
259 shows "fetch (A |+| B) s x = (a, Suc (length A div 2))" |
260 assumes "fetch A a x = (ac, 0)" |
260 using h1 h2 h3 |
261 "tm_wf (A, 0)" |
261 apply(case_tac s) |
262 "a \<le> length A div 2" "a > 0" |
262 apply(case_tac [!] x) |
263 shows "fetch (A |+| B) a x = (ac, Suc (length A div 2))" |
263 apply(auto simp: tm_comp_length nth_append) |
264 using assms |
|
265 apply(case_tac a, case_tac [!] x, |
|
266 auto simp: tm_comp_length tm_comp.simps length_adjust nth_append) |
|
267 apply(simp_all add: adjust.simps) |
|
268 done |
264 done |
269 |
265 |
270 lemma tmcomp_exec_after_first: |
266 lemma tm_comp_exec_after_first: |
271 "\<lbrakk>0 < a; step (a, b, c) (A, 0) = (0, tp'); tm_wf (A, 0); |
267 assumes h1: "\<not> is_final c" |
272 a \<le> length A div 2\<rbrakk> |
268 and h2: "step0 c A = (0, tp)" |
273 \<Longrightarrow> step (a, b, c) (A |+| B, 0) = (Suc (length A div 2), tp')" |
269 and h3: "fst c \<le> length A div 2" |
274 apply(simp add: step.simps, auto) |
270 shows "step0 c (A |+| B) = (Suc (length A div 2), tp)" |
275 apply(case_tac "fetch A a Bk", simp add: tmcomp_fetch_in_first2) |
271 using h1 h2 h3 |
276 apply(case_tac "fetch A a (hd c)", simp add: tmcomp_fetch_in_first2) |
272 apply(case_tac c) |
|
273 apply(auto simp del: tm_comp.simps) |
|
274 apply(case_tac "fetch A a Bk") |
|
275 apply(simp del: tm_comp.simps) |
|
276 apply(subst tm_comp_fetch_in_A) |
|
277 apply(auto)[4] |
|
278 apply(case_tac "fetch A a (hd c)") |
|
279 apply(simp del: tm_comp.simps) |
|
280 apply(subst tm_comp_fetch_in_A) |
|
281 apply(auto)[4] |
277 done |
282 done |
278 |
283 |
279 lemma step_nothalt_pre: "\<lbrakk>step (aa, ba, ca) (A, 0) = (a, b, c); 0 < a\<rbrakk> \<Longrightarrow> 0 < aa" |
284 lemma step_in_range: |
280 apply(case_tac "aa = 0", simp add: step_0, simp) |
285 assumes h1: "\<not> is_final (step0 c A)" |
|
286 and h2: "tm_wf (A, 0)" |
|
287 shows "fst (step0 c A) \<le> length A div 2" |
|
288 using h1 h2 |
|
289 apply(case_tac c) |
|
290 apply(case_tac a) |
|
291 apply(auto simp add: prod_case_unfold Let_def) |
|
292 apply(case_tac "hd c") |
|
293 apply(auto simp add: prod_case_unfold) |
281 done |
294 done |
282 |
295 |
283 lemma nth_in_set: |
|
284 "\<lbrakk> A ! i = x; i < length A\<rbrakk> \<Longrightarrow> x \<in> set A" |
|
285 by auto |
|
286 |
|
287 lemma step_nothalt: |
|
288 "\<lbrakk>step (aa, ba, ca) (A, 0) = (a, b, c); 0 < a; tm_wf (A, 0)\<rbrakk> \<Longrightarrow> |
|
289 a \<le> length A div 2" |
|
290 apply(simp add: step.simps) |
|
291 apply(case_tac aa, case_tac [!] aa, auto split: if_splits simp: tm_wf.simps) |
|
292 apply(case_tac "A ! (2 * nat)", simp) |
|
293 apply(erule_tac x = "(aa, a)" in ballE, simp_all add: nth_in_set) |
|
294 apply(case_tac "hd ca", auto split: if_splits simp: tm_wf.simps) |
|
295 apply(case_tac "A ! (2 * nat)", simp) |
|
296 apply(erule_tac x = "(aa, a)" in ballE, simp_all add: nth_in_set) |
|
297 apply(case_tac "A ! (Suc (2 * nat))") |
|
298 apply(erule_tac x = "(aa,bb)" in ballE, simp_all add: nth_in_set) |
|
299 done |
|
300 |
|
301 lemma steps_in_range: |
296 lemma steps_in_range: |
302 " \<lbrakk>0 < a; steps (Suc 0, tp) (A, 0) stp = (a, b, c); tm_wf (A, 0)\<rbrakk> |
297 assumes h1: "\<not> is_final (steps0 (1, tp) A stp)" |
303 \<Longrightarrow> a \<le> length A div 2" |
298 and h2: "tm_wf (A, 0)" |
304 proof(induct stp arbitrary: a b c) |
299 shows "fst (steps0 (1, tp) A stp) \<le> length A div 2" |
305 fix a b c |
300 using h1 |
306 assume h: "0 < a" "steps (Suc 0, tp) (A, 0) 0 = (a, b, c)" |
301 proof(induct stp) |
307 "tm_wf (A, 0)" |
302 case 0 |
308 thus "a \<le> length A div 2" |
303 then show "fst (steps0 (1, tp) A 0) \<le> length A div 2" using h2 |
309 apply(simp add: steps.simps tm_wf.simps, auto) |
304 by (auto simp add: steps.simps tm_wf.simps) |
310 done |
|
311 next |
305 next |
312 fix stp a b c |
306 case (Suc stp) |
313 assume ind: "\<And>a b c. \<lbrakk>0 < a; steps (Suc 0, tp) (A, 0) stp = (a, b, c); |
307 have ih: "\<not> is_final (steps0 (1, tp) A stp) \<Longrightarrow> fst (steps0 (1, tp) A stp) \<le> length A div 2" by fact |
314 tm_wf (A, 0)\<rbrakk> \<Longrightarrow> a \<le> length A div 2" |
308 have h: "\<not> is_final (steps0 (1, tp) A (Suc stp))" by fact |
315 and h: "0 < a" "steps (Suc 0, tp) (A, 0) (Suc stp) = (a, b, c)" "tm_wf (A, 0)" |
309 from ih h h2 show "fst (steps0 (1, tp) A (Suc stp)) \<le> length A div 2" |
316 from h show "a \<le> length A div 2" |
310 by (metis step_in_range step_red) |
317 proof(simp add: step_red, case_tac "(steps (Suc 0, tp) (A, 0) stp)", simp) |
311 qed |
318 fix aa ba ca |
312 |
319 assume g: "step (aa, ba, ca) (A, 0) = (a, b, c)" |
313 lemma tm_comp_pre_halt_same: |
320 "steps (Suc 0, tp) (A, 0) stp = (aa, ba, ca)" |
314 assumes a_ht: "steps0 (1, tp) A n = (0, tp')" |
321 hence "aa \<le> length A div 2" |
|
322 apply(rule_tac ind, auto simp: h step_nothalt_pre) |
|
323 done |
|
324 thus "?thesis" |
|
325 using g h |
|
326 apply(rule_tac step_nothalt, auto) |
|
327 done |
|
328 qed |
|
329 qed |
|
330 |
|
331 lemma t_merge_pre_halt_same: |
|
332 assumes a_ht: "steps (1, tp) (A, 0) n = (0, tp')" |
|
333 and a_wf: "tm_wf (A, 0)" |
315 and a_wf: "tm_wf (A, 0)" |
334 obtains n' where "steps (1, tp) (A |+| B, 0) n' = (Suc (length A div 2), tp')" |
316 obtains n' where "steps0 (1, tp) (A |+| B) n' = (Suc (length A div 2), tp')" |
335 proof - |
317 proof - |
336 assume a: "\<And>n. steps (1, tp) (A |+| B, 0) n = (Suc (length A div 2), tp') \<Longrightarrow> thesis" |
318 assume a: "\<And>n. steps (1, tp) (A |+| B, 0) n = (Suc (length A div 2), tp') \<Longrightarrow> thesis" |
337 obtain stp' where "\<not> is_final (steps (1, tp) (A, 0) stp')" and |
319 obtain stp' where fin: "\<not> is_final (steps0 (1, tp) A stp')" and h: "steps0 (1, tp) A (Suc stp') = (0, tp')" |
338 "steps (1, tp) (A, 0) (Suc stp') = (0, tp')" |
320 using before_final[OF a_ht] by blast |
339 using a_ht before_final by blast |
321 from fin have h1:"steps0 (1, tp) (A |+| B) stp' = steps0 (1, tp) A stp'" |
340 then have "steps (1, tp) (A |+| B, 0) (Suc stp') = (Suc (length A div 2), tp')" |
322 by (rule tm_comp_step) |
341 proof(simp add: step_red) |
323 from h have h2: "step0 (steps0 (1, tp) A stp') A = (0, tp')" |
342 assume "\<not> is_final (steps (Suc 0, tp) (A, 0) stp')" |
324 by (simp only: step_red) |
343 " step (steps (Suc 0, tp) (A, 0) stp') (A, 0) = (0, tp')" |
325 |
344 moreover hence "(steps0 (1, tp) (A |+| B) stp') = (steps0 (1, tp) A stp')" |
326 have "steps0 (1, tp) (A |+| B) (Suc stp') = step0 (steps0 (1, tp) (A |+| B) stp') (A |+| B)" |
345 apply(rule_tac tm_comp_pre_eq) |
327 by (simp only: step_red) |
346 apply(simp_all add: a_ht) |
328 also have "... = step0 (steps0 (1, tp) A stp') (A |+| B)" using h1 by simp |
347 done |
329 also have "... = (Suc (length A div 2), tp')" |
348 ultimately show "step (steps (Suc 0, tp) (A |+| B, 0) stp') (A |+| B, 0) = (Suc (length A div 2), tp')" |
330 by (rule tm_comp_exec_after_first[OF fin h2 steps_in_range[OF fin a_wf]]) |
349 apply(case_tac " steps (Suc 0, tp) (A, 0) stp'", simp) |
331 finally show thesis using a by blast |
350 apply(rule tmcomp_exec_after_first, simp_all add: a_wf) |
332 qed |
351 apply(erule_tac steps_in_range, auto simp: a_wf) |
333 |
352 done |
334 |
353 qed |
|
354 with a show thesis by blast |
|
355 qed |
|
356 |
335 |
357 lemma tm_comp_fetch_second_zero: |
336 lemma tm_comp_fetch_second_zero: |
358 "\<lbrakk>fetch B sa' x = (a, 0); tm_wf (A, 0); tm_wf (B, 0); sa' > 0\<rbrakk> |
337 assumes h1: "fetch B s x = (a, 0)" |
359 \<Longrightarrow> fetch (A |+| B) (sa' + (length A div 2)) x = (a, 0)" |
338 and hs: "tm_wf (A, 0)" "s \<noteq> 0" |
|
339 shows "fetch (A |+| B) (s + (length A div 2)) x = (a, 0)" |
|
340 using h1 hs |
360 apply(case_tac x) |
341 apply(case_tac x) |
361 apply(case_tac [!] sa', |
342 apply(case_tac [!] s) |
362 auto simp: fetch.simps tm_comp_length length_adjust nth_append tm_comp.simps |
343 apply(auto simp: tm_comp_length nth_append) |
363 tm_wf.simps shift.simps split: if_splits) |
|
364 done |
344 done |
365 |
345 |
366 lemma tm_comp_fetch_second_inst: |
346 lemma tm_comp_fetch_second_inst: |
367 "\<lbrakk>sa > 0; s > 0; tm_wf (A, 0); tm_wf (B, 0); fetch B sa x = (a, s)\<rbrakk> |
347 assumes h1: "fetch B sa x = (a, s)" |
368 \<Longrightarrow> fetch (A |+| B) (sa + length A div 2) x = (a, s + length A div 2)" |
348 and hs: "tm_wf (A, 0)" "sa \<noteq> 0" "s \<noteq> 0" |
|
349 shows "fetch (A |+| B) (sa + length A div 2) x = (a, s + length A div 2)" |
|
350 using h1 hs |
369 apply(case_tac x) |
351 apply(case_tac x) |
370 apply(case_tac [!] sa, |
352 apply(case_tac [!] sa) |
371 auto simp: fetch.simps tm_comp_length length_adjust nth_append tm_comp.simps |
353 apply(auto simp: tm_comp_length nth_append) |
372 tm_wf.simps shift.simps split: if_splits) |
|
373 done |
354 done |
|
355 |
374 |
356 |
375 lemma t_merge_second_same: |
357 lemma t_merge_second_same: |
376 assumes a_wf: "tm_wf (A, 0)" |
358 assumes a_wf: "tm_wf (A, 0)" |
377 and b_wf: "tm_wf (B, 0)" |
359 and steps: "steps0 (1, l, r) B stp = (s', l', r')" |
378 and steps: "steps (Suc 0, l, r) (B, 0) stp = (s, l', r')" |
360 shows "steps0 (Suc (length A div 2), l, r) (A |+| B) stp |
379 shows "steps (Suc (length A div 2), l, r) (A |+| B, 0) stp |
361 = (if s' = 0 then 0 else s' + length A div 2, l', r')" |
380 = (if s = 0 then 0 |
362 using steps |
381 else s + length A div 2, l', r')" |
363 proof(induct stp arbitrary: s' l' r') |
382 using a_wf b_wf steps |
364 case 0 |
383 proof(induct stp arbitrary: s l' r', simp add: steps.simps, simp) |
365 then show ?case by (simp add: steps.simps) |
384 fix stpa sa l'a r'a |
366 next |
385 assume ind: "\<And>s l' r'. steps (Suc 0, l, r) (B, 0) stpa = (s, l', r') \<Longrightarrow> |
367 case (Suc stp s' l' r') |
386 steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa = |
368 obtain s'' l'' r'' where a: "steps0 (1, l, r) B stp = (s'', l'', r'')" |
387 (if s = 0 then 0 else s + length A div 2, l', r')" |
369 by (metis is_final.cases) |
388 and h: "step (steps (Suc 0, l, r) (B, 0) stpa) (B, 0) = (sa, l'a, r'a)" |
370 then have ih1: "s'' = 0 \<Longrightarrow> steps0 (Suc (length A div 2), l, r) (A |+| B) stp = (0, l'', r'')" |
389 obtain sa' l'' r'' where a: "(steps (Suc 0, l, r) (B, 0) stpa) = (sa', l'', r'')" |
371 and ih2: "s'' \<noteq> 0 \<Longrightarrow> steps0 (Suc (length A div 2), l, r) (A |+| B) stp = (s'' + length A div 2, l'', r'')" |
390 apply(case_tac "steps (Suc 0, l, r) (B, 0) stpa", auto) |
372 using Suc by (auto) |
|
373 have h: "steps0 (1, l, r) B (Suc stp) = (s', l', r')" by fact |
|
374 |
|
375 { assume "s'' = 0" |
|
376 then have ?case using a h ih1 by (simp del: steps.simps) |
|
377 } moreover |
|
378 { assume as: "s'' \<noteq> 0" "s' = 0" |
|
379 from as a h |
|
380 have "step0 (s'', l'', r'') B = (0, l', r')" by (simp del: steps.simps) |
|
381 with as have ?case |
|
382 apply(simp add: ih2[OF as(1)] step.simps del: tm_comp.simps steps.simps) |
|
383 apply(case_tac "fetch B s'' (read r'')") |
|
384 apply(auto simp add: tm_comp_fetch_second_zero[OF _ a_wf] simp del: tm_comp.simps) |
391 done |
385 done |
392 from this have b: "steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa = |
386 } moreover |
393 (if sa' = 0 then 0 else sa' + length A div 2, l'', r'')" |
387 { assume as: "s'' \<noteq> 0" "s' \<noteq> 0" |
394 apply(erule_tac ind) |
388 from as a h |
|
389 have "step0 (s'', l'', r'') B = (s', l', r')" by (simp del: steps.simps) |
|
390 with as have ?case |
|
391 apply(simp add: ih2[OF as(1)] step.simps del: tm_comp.simps steps.simps) |
|
392 apply(case_tac "fetch B s'' (read r'')") |
|
393 apply(auto simp add: tm_comp_fetch_second_inst[OF _ a_wf as] simp del: tm_comp.simps) |
395 done |
394 done |
396 from a b h show |
395 } |
397 "(sa = 0 \<longrightarrow> step (steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa) (A |+| B, 0) = (0, l'a, r'a)) \<and> |
396 ultimately show ?case by blast |
398 (0 < sa \<longrightarrow> step (steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa) (A |+| B, 0) = (sa + length A div 2, l'a, r'a))" |
|
399 proof(case_tac "sa' = 0", auto) |
|
400 assume "step (sa', l'', r'') (B, 0) = (0, l'a, r'a)" "0 < sa'" |
|
401 thus "step (sa' + length A div 2, l'', r'') (A |+| B, 0) = (0, l'a, r'a)" |
|
402 using a_wf b_wf |
|
403 apply(simp add: step.simps) |
|
404 apply(case_tac "fetch B sa' (read r'')", auto) |
|
405 apply(simp_all add: step.simps tm_comp_fetch_second_zero) |
|
406 done |
|
407 next |
|
408 assume "step (sa', l'', r'') (B, 0) = (sa, l'a, r'a)" "0 < sa'" "0 < sa" |
|
409 thus "step (sa' + length A div 2, l'', r'') (A |+| B, 0) = (sa + length A div 2, l'a, r'a)" |
|
410 using a_wf b_wf |
|
411 apply(simp add: step.simps) |
|
412 apply(case_tac "fetch B sa' (read r'')", auto) |
|
413 apply(simp_all add: step.simps tm_comp_fetch_second_inst) |
|
414 done |
|
415 qed |
|
416 qed |
397 qed |
417 |
398 |
418 lemma t_merge_second_halt_same: |
399 lemma t_merge_second_halt_same: |
419 "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0); |
400 assumes "tm_wf (A, 0)" |
420 steps (1, l, r) (B, 0) stp = (0, l', r')\<rbrakk> |
401 and "steps0 (1, l, r) B stp = (0, l', r')" |
421 \<Longrightarrow> steps (Suc (length A div 2), l, r) (A |+| B, 0) stp |
402 shows "steps0 (Suc (length A div 2), l, r) (A |+| B) stp = (0, l', r')" |
422 = (0, l', r')" |
403 using t_merge_second_same[OF assms] by (simp) |
423 using t_merge_second_same[where s = "0"] |
404 |
424 apply(auto) |
|
425 done |
|
426 |
|
427 |
|
428 end |
405 end |
429 |
406 |