diff -r c8ff97d9f8da -r 7edbd5657702 thys/turing_basic.thy
--- a/thys/turing_basic.thy	Sun Jan 20 16:01:16 2013 +0000
+++ b/thys/turing_basic.thy	Tue Jan 22 14:38:56 2013 +0000
@@ -114,12 +114,26 @@
   shows "is_final (s, tp) = (s = 0)"
 by (case_tac tp) (auto)
 
-lemma is_final_steps:
-  assumes "is_final (s, l, r)"
-  shows "is_final (steps (s, l, r) (p, off) n)"
+lemma after_is_final:
+  assumes "is_final c"
+  shows "is_final (steps c p n)"
 using assms 
-by (induct n) (auto)
+apply(induct n) 
+apply(case_tac [!] c)
+apply(auto)
+done
 
+lemma not_is_final:
+  assumes a: "\<not> is_final (steps c p n1)"
+  and b: "n2 \<le> n1"
+  shows "\<not> is_final (steps c p n2)"
+proof (rule notI)
+  obtain n3 where eq: "n1 = n2 + n3" using b by (metis le_iff_add)
+  assume "is_final (steps c p n2)"
+  then have "is_final (steps c p n1)" unfolding eq
+    by (simp add: after_is_final)
+  with a show "False" by simp
+qed
 
 (* if the machine is in the halting state, there must have 
    been a state just before the halting state *)
@@ -212,7 +226,7 @@
   shows "length (A |+| B) = length A + length B"
 by auto
 
-lemma tm_comp_step_aux: 
+lemma tm_comp_step: 
   assumes unfinal: "\<not> is_final (step0 c A)"
   shows "step0 c (A |+| B) = step0 c A"
 proof -
@@ -228,7 +242,7 @@
   then show "step0 c (A |+| B) = step0 c A" by (simp add: eq) 
 qed
 
-lemma tm_comp_step:  
+lemma tm_comp_steps:  
   assumes "\<not> is_final (steps0 c A n)" 
   shows "steps0 c (A |+| B) n = steps0 c A n"
 using assms
@@ -247,7 +261,7 @@
   have "steps0 c (A |+| B) (Suc n) = step0 (steps0 c (A |+| B) n) (A |+| B)" 
     by (simp only: step_red)
   also have "... = step0 (steps0 c A n) (A |+| B)" by (simp only: ih[OF fin2])
-  also have "... = step0 (steps0 c A n) A" by (simp only: tm_comp_step_aux[OF fin1])
+  also have "... = step0 (steps0 c A n) A" by (simp only: tm_comp_step[OF fin1])
   finally show "steps0 c (A |+| B) (Suc n) = steps0 c A (Suc n)"
     by (simp only: step_red)
 qed
@@ -319,7 +333,7 @@
   obtain stp' where fin: "\<not> is_final (steps0 (1, tp) A stp')" and h: "steps0 (1, tp) A (Suc stp') = (0, tp')"
   using before_final[OF a_ht] by blast
   from fin have h1:"steps0 (1, tp) (A |+| B) stp' = steps0 (1, tp) A stp'"
-    by (rule tm_comp_step)
+    by (rule tm_comp_steps)
   from h have h2: "step0 (steps0 (1, tp) A stp') A = (0, tp')"
     by (simp only: step_red)