--- a/thys/Turing.thy	Thu May 02 13:19:50 2013 +0100
+++ b/thys/Turing.thy	Thu May 09 18:16:36 2013 +0100
@@ -111,6 +111,10 @@
   shows "is_final (s, tp) = (s = 0)"
 by (case_tac tp) (auto)
 
+lemma is_finalI [intro]:
+  shows "is_final (0, tp)"
+by (simp add: is_final_eq)
+
 lemma after_is_final:
   assumes "is_final c"
   shows "is_final (steps c p n)"
@@ -120,6 +124,16 @@
 apply(auto)
 done
 
+lemma is_final:
+  assumes a: "is_final (steps c p n1)"
+  and b: "n1 \<le> n2"
+  shows "is_final (steps c p n2)"
+proof - 
+  obtain n3 where eq: "n2 = n1 + n3" using b by (metis le_iff_add)
+  from a show "is_final (steps c p n2)" unfolding eq
+    by (simp add: after_is_final)
+qed
+
 lemma not_is_final:
   assumes a: "\<not> is_final (steps c p n1)"
   and b: "n2 \<le> n1"
@@ -164,6 +178,29 @@
   qed
 qed
 
+lemma least_steps: 
+  assumes "steps0 (1, tp) A n = (0, tp')"
+  shows "\<exists> n'. (\<forall>n'' < n'. \<not> is_final (steps0 (1, tp) A n'')) \<and> 
+               (\<forall>n'' \<ge> n'. is_final (steps0 (1, tp) A n''))"
+proof -
+  from before_final[OF assms] 
+  obtain n' where
+    before: "\<not> is_final (steps0 (1, tp) A n')" and
+    final: "steps0 (1, tp) A (Suc n') = (0, tp')" by auto
+  from before
+    have "\<forall>n'' < Suc n'. \<not> is_final (steps0 (1, tp) A n'')"
+      using not_is_final by auto
+  moreover
+  from final 
+    have "\<forall>n'' \<ge> Suc n'. is_final (steps0 (1, tp) A n'')" 
+      using is_final[of _ _ "Suc n'"] by (auto simp add: is_final_eq)
+  ultimately
+  show "\<exists> n'. (\<forall>n'' < n'. \<not> is_final (steps0 (1, tp) A n'')) \<and> (\<forall>n'' \<ge> n'. is_final (steps0 (1, tp) A n''))"
+    by blast
+qed
+
+
+
 (* well-formedness of Turing machine programs *)
 abbreviation "is_even n \<equiv> (n::nat) mod 2 = 0"