--- a/thys/turing_basic.thy	Wed Jan 23 20:18:40 2013 +0100
+++ b/thys/turing_basic.thy	Thu Jan 24 00:20:26 2013 +0100
@@ -168,16 +168,17 @@
 qed
 
 (* well-formedness of Turing machine programs *)
+abbreviation "is_even n \<equiv> (n::nat) mod 2 = 0"
+
 fun 
   tm_wf :: "tprog \<Rightarrow> bool"
 where
-  "tm_wf (p, off) = (length p \<ge> 2 \<and> length p mod 2 = 0 \<and> 
+  "tm_wf (p, off) = (length p \<ge> 2 \<and> is_even (length p) \<and> 
                     (\<forall>(a, s) \<in> set p. s \<le> length p div 2 + off \<and> s \<ge> off))"
 
 abbreviation
   "tm_wf0 p \<equiv> tm_wf (p, 0)"
 
-
 lemma halt_lemma: 
   "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
 by (metis wf_iff_no_infinite_down_chain)
@@ -349,8 +350,6 @@
   finally show thesis using a by blast
 qed
 
-
-
 lemma tm_comp_fetch_second_zero:
   assumes h1: "fetch B s x = (a, 0)"
   and hs: "tm_wf (A, 0)" "s \<noteq> 0"
@@ -372,7 +371,7 @@
 done 
 
 
-lemma t_merge_second_same:
+lemma tm_comp_second_same:
   assumes a_wf: "tm_wf (A, 0)"
   and steps: "steps0 (1, l, r) B stp = (s', l', r')"
   shows "steps0 (Suc (length A div 2), l, r)  (A |+| B) stp 
@@ -414,11 +413,11 @@
   ultimately show ?case by blast
 qed
 
-lemma t_merge_second_halt_same:
+lemma tm_comp_second_halt_same:
   assumes "tm_wf (A, 0)"  
   and "steps0 (1, l, r) B stp = (0, l', r')"
   shows "steps0 (Suc (length A div 2), l, r)  (A |+| B) stp = (0, l', r')"
-using t_merge_second_same[OF assms] by (simp)
+using tm_comp_second_same[OF assms] by (simp)
 
 end