# HG changeset patch # User Christian Urban # Date 1358629435 0 # Node ID fbd346f5af86e1c1ee88e28931bb256975936888 # Parent be5187b73ab9366aeaea538c6f84f720c9fbdc29 more proofs polished diff -r be5187b73ab9 -r fbd346f5af86 paper.pdf Binary file paper.pdf has changed diff -r be5187b73ab9 -r fbd346f5af86 thys/turing_basic.thy --- a/thys/turing_basic.thy Sat Jan 19 19:23:42 2013 +0000 +++ b/thys/turing_basic.thy Sat Jan 19 21:03:55 2013 +0000 @@ -212,63 +212,50 @@ shows "length (A |+| B) = length A + length B" by auto -lemma tm_comp_fetch_in_first: - assumes "case (fetch A a x) of (ac, ns) \ ns \ 0" - shows "fetch (A |+| B) a x = fetch A a x" -using assms -apply(case_tac a) -apply(case_tac [!] x) -apply(auto simp: tm_comp_length nth_append) -done +lemma tm_comp_pre_eq_step: + assumes unfinal: "\ is_final (step0 c A)" + shows "step0 c (A |+| B) = step0 c A" +proof - + obtain s l r where eq: "c = (s, l, r)" by (metis is_final.cases) + have "\ is_final (step0 (s, l, r) A)" using unfinal eq by simp + then have "case (fetch A s (read r)) of (a, s) \ s \ 0" + by (auto simp add: is_final_eq) + then have "fetch (A |+| B) s (read r) = fetch A s (read r)" + apply(case_tac [!] "read r") + apply(case_tac [!] s) + apply(auto simp: tm_comp_length nth_append) + done + then show "step0 c (A |+| B) = step0 c A" by (simp add: eq) +qed -lemma t_merge_pre_eq_step: - assumes step: "step0 (s, l, r) A = cf" - and tm_wf: "tm_wf (A, 0)" - and unfinal: "\ is_final cf" - shows "step0 (s, l, r) (A |+| B) = cf" -proof - - from step unfinal - have "\ is_final (step0 (s, l, r) A)" by simp - then have "fetch (A |+| B) s (read r) = fetch A s (read r)" - by (rule_tac tm_comp_fetch_in_first) (auto simp add: is_final_eq) - then show ?thesis - using step by auto +lemma tm_comp_pre_eq: + assumes "\ is_final (steps0 (1, tp) A n)" + shows "steps0 (1, tp) (A |+| B) n = steps0 (1, tp) A n" +using assms +proof(induct n) + case 0 + then show "steps0 (1, tp) (A |+| B) 0 = steps0 (1, tp) A 0" by auto +next + case (Suc n) + have ih: "\ is_final (steps0 (1, tp) A n) \ steps0 (1, tp) (A |+| B) n = steps0 (1, tp) A n" by fact + have fin: "\ is_final (steps0 (1, tp) A (Suc n))" by fact + then have fin1: "\ is_final (step0 (steps0 (1, tp) A n) A)" + by (auto simp only: step_red) + then have fin2: "\ is_final (steps0 (1, tp) A n)" + by (metis is_final_eq step_0 surj_pair) + + have "steps0 (1, tp) (A |+| B) (Suc n) = step0 (steps0 (1, tp) (A |+| B) n) (A |+| B)" + by (simp only: step_red) + also have "... = step0 (steps0 (1, tp) A n) (A |+| B)" by (simp only: ih[OF fin2]) + also have "... = step0 (steps0 (1, tp) A n) A" by (simp only: tm_comp_pre_eq_step[OF fin1]) + finally show "steps0 (1, tp) (A |+| B) (Suc n) = steps0 (1, tp) A (Suc n)" + by (simp only: step_red) qed declare steps.simps[simp del] declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del] declare tm_wf.simps[simp del] step.simps[simp del] -lemma t_merge_pre_eq: - assumes "steps0 (1, tp) A stp = cf" - and "\ is_final cf" - and wf_A: "tm_wf (A, 0)" - shows "steps0 (1, tp) (A |+| B) stp = cf" -using assms(1) assms(2) -proof(induct stp arbitrary: cf) - case (0 cf) - then show "steps0 (1, tp) (A |+| B) 0 = cf" - by (auto simp: steps.simps) -next - case (Suc stp cf) - have ih: "\cf. \steps0 (1, tp) A stp = cf; \ is_final cf\ \ steps0 (1, tp) (A |+| B) stp = cf" by fact - then obtain s l r where eq: "steps0 (1, tp) A stp = (s, l, r)" - by (metis is_final.cases) - have fin: "\ is_final cf" by fact - - have "steps0 (1, tp) A (Suc stp) = cf" by fact - then have "step0 (steps0 (1, tp) A stp) A = cf" by simp - then have h: "step0 (s, l, r) A = cf" using eq by simp - then have "\ is_final (s, l, r)" using fin by (cases s) (auto) - then have eq2: "steps0 (1, tp) (A |+| B) stp = (s, l, r)" by (rule ih[OF eq]) - - have "steps0 (1, tp) (A |+| B) (Suc stp) = step0 (steps0 (Suc 0, tp) (A |+| B) stp) (A |+| B)" by simp - also have "... = step0 (s, l, r) (A |+| B)" using eq2 by simp - also have "... = cf" by (rule t_merge_pre_eq_step[OF h wf_A fin]) - finally show "steps0 (1, tp) (A |+| B) (Suc stp) = cf" . -qed - - lemma tmcomp_fetch_in_first2: assumes "fetch A a x = (ac, 0)" "tm_wf (A, 0)" @@ -355,8 +342,8 @@ assume "\ is_final (steps (Suc 0, tp) (A, 0) stp')" " step (steps (Suc 0, tp) (A, 0) stp') (A, 0) = (0, tp')" moreover hence "(steps0 (1, tp) (A |+| B) stp') = (steps0 (1, tp) A stp')" - apply(rule_tac t_merge_pre_eq) - apply(simp_all add: a_wf a_ht) + apply(rule_tac tm_comp_pre_eq) + apply(simp_all add: a_ht) done ultimately show "step (steps (Suc 0, tp) (A |+| B, 0) stp') (A |+| B, 0) = (Suc (length A div 2), tp')" apply(case_tac " steps (Suc 0, tp) (A, 0) stp'", simp)