--- a/Paper/Paper.thy	Fri Jan 18 23:59:33 2013 +0000
+++ b/Paper/Paper.thy	Sat Jan 19 12:45:14 2013 +0000
@@ -72,7 +72,7 @@
 297]{Norrish11}.  Part of his formalisation is a clever infrastructure
 for reducing $\lambda$-terms. He also established the computational
 equivalence between the $\lambda$-calculus and recursive functions.
-Nevertheless he concluded that it would be ``appealing''
+Nevertheless he concluded that it would be appealing
  to have formalisations for more operational models of
 computations, such as Turing machines or register machines.  One
 reason is that many proofs in the literature use them.  He noted
@@ -232,7 +232,7 @@
   Note that by using lists each side of the tape is only finite. The
   potential infinity is achieved by adding an appropriate blank or occupied cell 
   whenever the head goes over the ``edge'' of the tape. To 
-  make this formal we define five possible \emph{actions} 
+  make this formal we define five possible \emph{actions}, @{text a} 
   the Turing machine can perform:
 
   \begin{center}

Binary file paper.pdf has changed

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