diff -r 6725c9c026f6 -r 2cb1e4499983 thys/turing_basic.thy
--- a/thys/turing_basic.thy	Fri Jan 18 23:59:33 2013 +0000
+++ b/thys/turing_basic.thy	Sat Jan 19 12:45:14 2013 +0000
@@ -209,7 +209,7 @@
 
 declare steps.simps[simp del]
 
-lemma before_final: 
+lemma before_final_old: 
   assumes "steps (1, tp) A n = (0, tp')"
   obtains n' where "\<not> is_final (steps (1, tp) A n')" 
         and "steps (1, tp) A (Suc n') = (0, tp')"
@@ -223,6 +223,12 @@
       \<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')"
     and h: " steps (1, tp) A (Suc n) = (0, tp')"
     from h show  "\<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')"
+      (*
+      apply(simp add: step_red del: steps.simps)
+      apply(case_tac "(steps (Suc 0, tp) A n)")
+      apply(case_tac "a = 0")
+      apply(simp)
+      *)
     proof(simp add: step_red del: steps.simps, 
                      case_tac "(steps (Suc 0, tp) A n)", case_tac "a = 0", simp)
       fix a b c
@@ -240,7 +246,8 @@
         "a \<noteq> 0"
       thus "\<exists>n'. \<not> is_final (steps (Suc 0, tp) A n') \<and> 
         step (steps (Suc 0, tp) A n') A = (0, tp')"
-        apply(rule_tac x = n in exI, simp)
+        apply(rule_tac x = n in exI)
+        apply(simp)
         done
     qed
   qed
@@ -249,6 +256,36 @@
     by auto
 qed
 
+lemma before_final: 
+  assumes "steps (1, tp) A n = (0, tp')"
+  shows "\<exists> n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')"
+using assms
+proof(induct n arbitrary: tp')
+  case (0 tp')
+  have asm: "steps (1, tp) A 0 = (0, tp')" by fact
+  then show "\<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')"
+    by (simp add: steps.simps)
+next
+  case (Suc n tp')
+  have ih: "\<And>tp'. steps (1, tp) A n = (0, tp') \<Longrightarrow>
+    \<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')" by fact
+  have asm: "steps (1, tp) A (Suc n) = (0, tp')" by fact
+  obtain s l r where cases: "steps (1, tp) A n = (s, l, r)"
+    by (auto intro: is_final.cases)
+  then show "\<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')"
+  proof (cases "s = 0")
+    case True (* in halting state *)
+    then have "steps (1, tp) A n = (0, tp')"
+      using asm cases by simp
+    then show ?thesis using ih by simp
+  next
+    case False (* not in halting state *)
+    then have "\<not> is_final (steps (1, tp) A n) \<and> steps (1, tp) A (Suc n) = (0, tp')"
+      using asm cases by simp
+    then show ?thesis by auto
+  qed
+qed
+
 declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del]
 
 lemma length_comp: