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

--- a/thys/Turing_Hoare.thy	Mon Feb 11 08:46:24 2013 +0000
+++ b/thys/Turing_Hoare.thy	Tue Feb 12 13:37:07 2013 +0000
@@ -1,3 +1,9 @@
+(* Title: thys/Turing_Hoare.thy
+   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
+*)
+
+header {* Hoare Rules for TMs *}
+
 theory Turing_Hoare
 imports Turing
 begin
@@ -37,7 +43,6 @@
 where
   "{P} p {Q} \<equiv> \<forall>tp. P tp \<longrightarrow> (\<exists>n. is_final (steps0 (1, tp) p n) \<and> Q holds_for (steps0 (1, tp) p n))"
 
-
 (* not halting case *)
 definition
   Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_)) \<up>" 50)
@@ -83,7 +88,7 @@
     by (metis is_final_eq surj_pair) 
   then obtain n2 
     where "steps0 (1, l, r) (A |+| B) n2 = (Suc (length A div 2), l', r')"
-    using A_wf by (rule_tac tm_comp_pre_halt_same) 
+    using A_wf by (rule_tac tm_comp_next) 
   moreover
   from a1 a2 have "Q (l', r')" by (simp)
   then obtain n3 l'' r''
@@ -93,7 +98,7 @@
     using B_halt unfolding Hoare_halt_def 
     by (metis is_final_eq surj_pair) 
   then have "steps0 (Suc (length A div 2), l', r')  (A |+| B) n3 = (0, l'', r'')"
-    using A_wf by (rule_tac tm_comp_second_halt_same) 
+    using A_wf by (rule_tac tm_comp_final) 
   ultimately show 
     "\<exists>n. is_final (steps0 (1, l, r) (A |+| B) n) \<and> S holds_for (steps0 (1, l, r) (A |+| B) n)"
     using b1 b2 by (rule_tac x = "n2 + n3" in exI) (simp)
@@ -120,7 +125,7 @@
     using A_halt unfolding Hoare_halt_def 
     by (metis is_final_eq surj_pair) 
   then obtain n2 where eq: "steps0 (1, l, r) (A |+| B) n2 = (Suc (length A div 2), l', r')"
-    using A_wf by (rule_tac tm_comp_pre_halt_same)
+    using A_wf by (rule_tac tm_comp_next)
   then show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)"
   proof(cases "n2 \<le> n")
     case True
@@ -132,7 +137,7 @@
       where "steps0 (1, l', r') B (n - n2) = (s'', l'', r'')" 
       and "\<not> is_final (s'', l'', r'')" by (metis surj_pair)
     then have "steps0 (Suc (length A div 2), l', r') (A |+| B) (n - n2) = (s''+ length A div 2, l'', r'')"
-      using A_wf by (auto dest: tm_comp_second_same simp del: tm_wf.simps)
+      using A_wf by (auto dest: tm_comp_second simp del: tm_wf.simps)
     then have "\<not> is_final (steps0 (1, l, r) (A |+| B) (n2 + (n  - n2)))"
       using A_wf by (simp only: steps_add eq) (simp add: tm_wf.simps)
     then show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" 

--- a/thys/Uncomputable.thy	Mon Feb 11 08:46:24 2013 +0000
+++ b/thys/Uncomputable.thy	Tue Feb 12 13:37:07 2013 +0000
@@ -1,9 +1,8 @@
-(* Title: Turing machine's definition and its charater
-   Author: XuJian <xujian817@hotmail.com>
-   Maintainer: Xujian
+(* Title: thys/Uncomputable.thy
+   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
 *)
 
-header {* Undeciablity of the {\em Halting problem} *}
+header {* Undeciablity of the Halting Problem *}
 
 theory Uncomputable
 imports Turing_Hoare
@@ -19,12 +18,10 @@
   and "7 = Suc 6"
   and "8 = Suc 7" 
   and "9 = Suc 8" 
-  and "10 = Suc 9" 
-  by arith+
+  and "10 = Suc 9"
+by simp_all
 
-text {*
-  The {\em Copying} TM, which duplicates its input. 
-*}
+text {* The Copying TM, which duplicates its input. *}
 
 definition 
   tcopy_begin :: "instr list"
@@ -88,7 +85,7 @@
   shows "inv_begin n (step0 cf tcopy_begin)"
 using assms
 unfolding tcopy_begin_def
-apply(case_tac cf)
+apply(cases cf)
 apply(auto simp: numeral split: if_splits)
 apply(case_tac "hd c")
 apply(auto)