# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1358599514 0
# Node ID 2cb1e4499983ae14eb2bd25c87b1a49f8e585310
# Parent  6725c9c026f61d8f171fbc728834a38ab88ee3fe
updated before_final

diff -r 6725c9c026f6 -r 2cb1e4499983 Paper/Paper.thy
--- 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}
diff -r 6725c9c026f6 -r 2cb1e4499983 paper.pdf
Binary file paper.pdf has changed
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: