210 |
210 |
211 lemma tm_comp_length: |
211 lemma tm_comp_length: |
212 shows "length (A |+| B) = length A + length B" |
212 shows "length (A |+| B) = length A + length B" |
213 by auto |
213 by auto |
214 |
214 |
215 lemma tm_comp_fetch_in_first: |
215 lemma tm_comp_pre_eq_step: |
216 assumes "case (fetch A a x) of (ac, ns) \<Rightarrow> ns \<noteq> 0" |
216 assumes unfinal: "\<not> is_final (step0 c A)" |
217 shows "fetch (A |+| B) a x = fetch A a x" |
217 shows "step0 c (A |+| B) = step0 c A" |
|
218 proof - |
|
219 obtain s l r where eq: "c = (s, l, r)" by (metis is_final.cases) |
|
220 have "\<not> is_final (step0 (s, l, r) A)" using unfinal eq by simp |
|
221 then have "case (fetch A s (read r)) of (a, s) \<Rightarrow> s \<noteq> 0" |
|
222 by (auto simp add: is_final_eq) |
|
223 then have "fetch (A |+| B) s (read r) = fetch A s (read r)" |
|
224 apply(case_tac [!] "read r") |
|
225 apply(case_tac [!] s) |
|
226 apply(auto simp: tm_comp_length nth_append) |
|
227 done |
|
228 then show "step0 c (A |+| B) = step0 c A" by (simp add: eq) |
|
229 qed |
|
230 |
|
231 lemma tm_comp_pre_eq: |
|
232 assumes "\<not> is_final (steps0 (1, tp) A n)" |
|
233 shows "steps0 (1, tp) (A |+| B) n = steps0 (1, tp) A n" |
218 using assms |
234 using assms |
219 apply(case_tac a) |
235 proof(induct n) |
220 apply(case_tac [!] x) |
236 case 0 |
221 apply(auto simp: tm_comp_length nth_append) |
237 then show "steps0 (1, tp) (A |+| B) 0 = steps0 (1, tp) A 0" by auto |
222 done |
238 next |
223 |
239 case (Suc n) |
224 lemma t_merge_pre_eq_step: |
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 |
225 assumes step: "step0 (s, l, r) A = cf" |
241 have fin: "\<not> is_final (steps0 (1, tp) A (Suc n))" by fact |
226 and tm_wf: "tm_wf (A, 0)" |
242 then have fin1: "\<not> is_final (step0 (steps0 (1, tp) A n) A)" |
227 and unfinal: "\<not> is_final cf" |
243 by (auto simp only: step_red) |
228 shows "step0 (s, l, r) (A |+| B) = cf" |
244 then have fin2: "\<not> is_final (steps0 (1, tp) A n)" |
229 proof - |
245 by (metis is_final_eq step_0 surj_pair) |
230 from step unfinal |
246 |
231 have "\<not> is_final (step0 (s, l, r) A)" by simp |
247 have "steps0 (1, tp) (A |+| B) (Suc n) = step0 (steps0 (1, tp) (A |+| B) n) (A |+| B)" |
232 then have "fetch (A |+| B) s (read r) = fetch A s (read r)" |
248 by (simp only: step_red) |
233 by (rule_tac tm_comp_fetch_in_first) (auto simp add: is_final_eq) |
249 also have "... = step0 (steps0 (1, tp) A n) (A |+| B)" by (simp only: ih[OF fin2]) |
234 then show ?thesis |
250 also have "... = step0 (steps0 (1, tp) A n) A" by (simp only: tm_comp_pre_eq_step[OF fin1]) |
235 using step by auto |
251 finally show "steps0 (1, tp) (A |+| B) (Suc n) = steps0 (1, tp) A (Suc n)" |
|
252 by (simp only: step_red) |
236 qed |
253 qed |
237 |
254 |
238 declare steps.simps[simp del] |
255 declare steps.simps[simp del] |
239 declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del] |
256 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] |
257 declare tm_wf.simps[simp del] step.simps[simp del] |
241 |
|
242 lemma t_merge_pre_eq: |
|
243 assumes "steps0 (1, tp) A stp = cf" |
|
244 and "\<not> is_final cf" |
|
245 and wf_A: "tm_wf (A, 0)" |
|
246 shows "steps0 (1, tp) (A |+| B) stp = cf" |
|
247 using assms(1) assms(2) |
|
248 proof(induct stp arbitrary: cf) |
|
249 case (0 cf) |
|
250 then show "steps0 (1, tp) (A |+| B) 0 = cf" |
|
251 by (auto simp: steps.simps) |
|
252 next |
|
253 case (Suc stp cf) |
|
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 then obtain s l r where eq: "steps0 (1, tp) A stp = (s, l, r)" |
|
256 by (metis is_final.cases) |
|
257 have fin: "\<not> is_final cf" by fact |
|
258 |
|
259 have "steps0 (1, tp) A (Suc stp) = cf" by fact |
|
260 then have "step0 (steps0 (1, tp) A stp) A = cf" by simp |
|
261 then have h: "step0 (s, l, r) A = cf" using eq by simp |
|
262 then have "\<not> is_final (s, l, r)" using fin by (cases s) (auto) |
|
263 then have eq2: "steps0 (1, tp) (A |+| B) stp = (s, l, r)" by (rule ih[OF eq]) |
|
264 |
|
265 have "steps0 (1, tp) (A |+| B) (Suc stp) = step0 (steps0 (Suc 0, tp) (A |+| B) stp) (A |+| B)" by simp |
|
266 also have "... = step0 (s, l, r) (A |+| B)" using eq2 by simp |
|
267 also have "... = cf" by (rule t_merge_pre_eq_step[OF h wf_A fin]) |
|
268 finally show "steps0 (1, tp) (A |+| B) (Suc stp) = cf" . |
|
269 qed |
|
270 |
|
271 |
258 |
272 lemma tmcomp_fetch_in_first2: |
259 lemma tmcomp_fetch_in_first2: |
273 assumes "fetch A a x = (ac, 0)" |
260 assumes "fetch A a x = (ac, 0)" |
274 "tm_wf (A, 0)" |
261 "tm_wf (A, 0)" |
275 "a \<le> length A div 2" "a > 0" |
262 "a \<le> length A div 2" "a > 0" |
353 then have "steps (1, tp) (A |+| B, 0) (Suc stp') = (Suc (length A div 2), tp')" |
340 then have "steps (1, tp) (A |+| B, 0) (Suc stp') = (Suc (length A div 2), tp')" |
354 proof(simp add: step_red) |
341 proof(simp add: step_red) |
355 assume "\<not> is_final (steps (Suc 0, tp) (A, 0) stp')" |
342 assume "\<not> is_final (steps (Suc 0, tp) (A, 0) stp')" |
356 " step (steps (Suc 0, tp) (A, 0) stp') (A, 0) = (0, tp')" |
343 " step (steps (Suc 0, tp) (A, 0) stp') (A, 0) = (0, tp')" |
357 moreover hence "(steps0 (1, tp) (A |+| B) stp') = (steps0 (1, tp) A stp')" |
344 moreover hence "(steps0 (1, tp) (A |+| B) stp') = (steps0 (1, tp) A stp')" |
358 apply(rule_tac t_merge_pre_eq) |
345 apply(rule_tac tm_comp_pre_eq) |
359 apply(simp_all add: a_wf a_ht) |
346 apply(simp_all add: a_ht) |
360 done |
347 done |
361 ultimately show "step (steps (Suc 0, tp) (A |+| B, 0) stp') (A |+| B, 0) = (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')" |
362 apply(case_tac " steps (Suc 0, tp) (A, 0) stp'", simp) |
349 apply(case_tac " steps (Suc 0, tp) (A, 0) stp'", simp) |
363 apply(rule tmcomp_exec_after_first, simp_all add: a_wf) |
350 apply(rule tmcomp_exec_after_first, simp_all add: a_wf) |
364 apply(erule_tac steps_in_range, auto simp: a_wf) |
351 apply(erule_tac steps_in_range, auto simp: a_wf) |