diff -r 641512ab0f6c -r d7570dbf9f06 thys/Turing.thy
--- a/thys/Turing.thy	Mon Feb 11 08:46:24 2013 +0000
+++ b/thys/Turing.thy	Tue Feb 12 13:37:07 2013 +0000
@@ -1,8 +1,9 @@
-(* Title: Turing machines
-   Author: Xu Jian <xujian817@hotmail.com>
-   Maintainer: Xu Jian
+(* Title: thys/Turing.thy
+   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
 *)
 
+header {* Turing Machines *}
+
 theory Turing
 imports Main
 begin
@@ -26,8 +27,7 @@
 type_synonym config = "state \<times> tape"
 
 fun nth_of where
-  "nth_of xs i = (if i \<ge> length xs then None
-                  else Some (xs ! i))"
+  "nth_of xs i = (if i \<ge> length xs then None else Some (xs ! i))"
 
 lemma nth_of_map [simp]:
   shows "nth_of (map f p) n = (case (nth_of p n) of None \<Rightarrow> None | Some x \<Rightarrow> Some (f x))"
@@ -75,15 +75,14 @@
   "step (s, l, r) (p, off) = 
      (let (a, s') = fetch p (s - off) (read r) in (s', update a (l, r)))"
 
+abbreviation
+  "step0 c p \<equiv> step c (p, 0)"
+
 fun steps :: "config \<Rightarrow> tprog \<Rightarrow> nat \<Rightarrow> config"
   where
   "steps c p 0 = c" |
   "steps c p (Suc n) = steps (step c p) p n"
 
-
-abbreviation
-  "step0 c p \<equiv> step c (p, 0)"
-
 abbreviation
   "steps0 c p n \<equiv> steps c (p, 0) n"
 
@@ -103,8 +102,6 @@
   shows "steps (0, (l, r)) p n = (0, (l, r))"
 by (induct n) (simp_all)
 
-
-
 fun
   is_final :: "config \<Rightarrow> bool"
 where
@@ -233,8 +230,7 @@
 
 lemma tm_comp_wf[intro]: 
   "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)"
-by (auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length tm_comp.simps)
-
+by (auto)
 
 lemma tm_comp_step: 
   assumes unfinal: "\<not> is_final (step0 c A)"
@@ -334,7 +330,8 @@
     by (metis step_in_range step_red)
 qed
 
-lemma tm_comp_pre_halt_same: 
+(* if A goes into the final state, then A |+| B will go into the first state of B *)
+lemma tm_comp_next: 
   assumes a_ht: "steps0 (1, tp) A n = (0, tp')"
   and a_wf: "tm_wf (A, 0)"
   obtains n' where "steps0 (1, tp) (A |+| B) n' = (Suc (length A div 2), tp')"
@@ -376,7 +373,7 @@
 done 
 
 
-lemma tm_comp_second_same:
+lemma tm_comp_second:
   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 
@@ -418,11 +415,12 @@
   ultimately show ?case by blast
 qed
 
-lemma tm_comp_second_halt_same:
+
+lemma tm_comp_final:
   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 tm_comp_second_same[OF assms] by (simp)
+using tm_comp_second[OF assms] by (simp)
 
 end