--- 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) \<Rightarrow> ns \<noteq> 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: "\<not> 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 "\<not> is_final (step0 (s, l, r) A)" using unfinal eq by simp
+ then have "case (fetch A s (read r)) of (a, s) \<Rightarrow> s \<noteq> 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: "\<not> is_final cf"
- shows "step0 (s, l, r) (A |+| B) = cf"
-proof -
- from step unfinal
- have "\<not> 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 "\<not> 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: "\<not> is_final (steps0 (1, tp) A n) \<Longrightarrow> steps0 (1, tp) (A |+| B) n = steps0 (1, tp) A n" by fact
+ have fin: "\<not> is_final (steps0 (1, tp) A (Suc n))" by fact
+ then have fin1: "\<not> is_final (step0 (steps0 (1, tp) A n) A)"
+ by (auto simp only: step_red)
+ then have fin2: "\<not> 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 "\<not> 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: "\<And>cf. \<lbrakk>steps0 (1, tp) A stp = cf; \<not> is_final cf\<rbrakk> \<Longrightarrow> 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: "\<not> 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 "\<not> 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 "\<not> 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)