--- 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)