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