238 declare steps.simps[simp del] |
238 declare steps.simps[simp del] |
239 declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del] |
239 declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del] |
240 declare tm_wf.simps[simp del] step.simps[simp del] |
240 declare tm_wf.simps[simp del] step.simps[simp del] |
241 |
241 |
242 lemma t_merge_pre_eq: |
242 lemma t_merge_pre_eq: |
243 "\<lbrakk>steps0 (Suc 0, tp) A stp = cf; \<not> is_final cf; tm_wf (A, 0)\<rbrakk> |
243 assumes "steps0 (1, tp) A stp = cf" |
244 \<Longrightarrow> steps0 (Suc 0, tp) (A |+| B) stp = cf" |
244 and "\<not> is_final cf" |
245 proof(induct stp arbitrary: cf, simp add: steps.simps) |
245 and wf_A: "tm_wf (A, 0)" |
246 fix stp cf |
246 shows "steps0 (1, tp) (A |+| B) stp = cf" |
247 assume ind: "\<And>cf. \<lbrakk>steps (Suc 0, tp) (A, 0) stp = cf; \<not> is_final cf; tm_wf (A, 0)\<rbrakk> |
247 using assms(1) assms(2) |
248 \<Longrightarrow> steps (Suc 0, tp) (A |+| B, 0) stp = cf" |
248 proof(induct stp arbitrary: cf) |
249 and h: "steps (Suc 0, tp) (A, 0) (Suc stp) = cf" |
249 case (0 cf) |
250 "\<not> is_final cf" "tm_wf (A, 0)" |
250 then show "steps0 (1, tp) (A |+| B) 0 = cf" |
251 from h show "steps (Suc 0, tp) (A |+| B, 0) (Suc stp) = cf" |
251 by (auto simp: steps.simps) |
252 proof(simp add: step_red, case_tac "(steps (Suc 0, tp) (A, 0) stp)", simp) |
252 next |
253 fix a b c |
253 case (Suc stp cf) |
254 assume g: "steps (Suc 0, tp) (A, 0) stp = (a, b, c)" |
254 have ih: "\<And>cf. \<lbrakk>steps0 (1, tp) A stp = cf; \<not> is_final cf\<rbrakk> \<Longrightarrow> steps0 (1, tp) (A |+| B) stp = cf" by fact |
255 "step (a, b, c) (A, 0) = cf" |
255 then obtain s l r where eq: "steps0 (1, tp) A stp = (s, l, r)" |
256 have "(steps (Suc 0, tp) (A |+| B, 0) stp) = (a, b, c)" |
256 by (metis is_final.cases) |
257 proof(rule ind, simp_all add: h g) |
257 have fin: "\<not> is_final cf" by fact |
258 show "0 < a" |
258 |
259 using g h |
259 have "steps0 (1, tp) A (Suc stp) = cf" by fact |
260 apply(simp add: step_red) |
260 then have "step0 (steps0 (1, tp) A stp) A = cf" by simp |
261 apply(case_tac a, auto simp: step_0) |
261 then have h: "step0 (s, l, r) A = cf" using eq by simp |
262 apply(case_tac "steps (Suc 0, tp) (A, 0) stp", simp) |
262 then have "\<not> is_final (s, l, r)" using fin by (cases s) (auto) |
263 done |
263 then have eq2: "steps0 (1, tp) (A |+| B) stp = (s, l, r)" by (rule ih[OF eq]) |
264 qed |
264 |
265 thus "step (steps (Suc 0, tp) (A |+| B, 0) stp) (A |+| B, 0) = cf" |
265 have "steps0 (1, tp) (A |+| B) (Suc stp) = step0 (steps0 (Suc 0, tp) (A |+| B) stp) (A |+| B)" by simp |
266 apply(simp) |
266 also have "... = step0 (s, l, r) (A |+| B)" using eq2 by simp |
267 apply(rule_tac t_merge_pre_eq_step, simp_all add: g h) |
267 also have "... = cf" by (rule t_merge_pre_eq_step[OF h wf_A fin]) |
268 done |
268 finally show "steps0 (1, tp) (A |+| B) (Suc stp) = cf" . |
269 qed |
269 qed |
270 qed |
270 |
271 |
271 |
272 lemma tmcomp_fetch_in_first2: |
272 lemma tmcomp_fetch_in_first2: |
273 assumes "fetch A a x = (ac, 0)" |
273 assumes "fetch A a x = (ac, 0)" |
274 "tm_wf (A, 0)" |
274 "tm_wf (A, 0)" |
275 "a \<le> length A div 2" "a > 0" |
275 "a \<le> length A div 2" "a > 0" |
352 using a_ht before_final by blast |
352 using a_ht before_final by blast |
353 then have "steps (1, tp) (A |+| B, 0) (Suc stp') = (Suc (length A div 2), tp')" |
353 then have "steps (1, tp) (A |+| B, 0) (Suc stp') = (Suc (length A div 2), tp')" |
354 proof(simp add: step_red) |
354 proof(simp add: step_red) |
355 assume "\<not> is_final (steps (Suc 0, tp) (A, 0) stp')" |
355 assume "\<not> is_final (steps (Suc 0, tp) (A, 0) stp')" |
356 " step (steps (Suc 0, tp) (A, 0) stp') (A, 0) = (0, tp')" |
356 " step (steps (Suc 0, tp) (A, 0) stp') (A, 0) = (0, tp')" |
357 moreover hence "(steps (Suc 0, tp) (A |+| B, 0) stp') = (steps (Suc 0, tp) (A, 0) stp')" |
357 moreover hence "(steps0 (1, tp) (A |+| B) stp') = (steps0 (1, tp) A stp')" |
358 apply(rule_tac t_merge_pre_eq) |
358 apply(rule_tac t_merge_pre_eq) |
359 apply(simp_all add: a_wf a_ht) |
359 apply(simp_all add: a_wf a_ht) |
360 done |
360 done |
361 ultimately show "step (steps (Suc 0, tp) (A |+| B, 0) stp') (A |+| B, 0) = (Suc (length A div 2), tp')" |
361 ultimately show "step (steps (Suc 0, tp) (A |+| B, 0) stp') (A |+| B, 0) = (Suc (length A div 2), tp')" |
362 apply(case_tac " steps (Suc 0, tp) (A, 0) stp'", simp) |
362 apply(case_tac " steps (Suc 0, tp) (A, 0) stp'", simp) |