--- a/thys/uncomputable.thy	Thu Jan 24 18:59:49 2013 +0100
+++ b/thys/uncomputable.thy	Fri Jan 25 15:57:58 2013 +0100
@@ -1075,47 +1075,36 @@
 abbreviation
   "dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. l = Bk \<up> n) \<and> r = [Oc]"
 
-lemma dither_unhalt_state: 
+lemma dither_loops_aux: 
   "(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or> 
    (steps0 (1, Bk \<up> m, [Oc]) dither stp = (2, Oc # Bk \<up> m, []))"
   apply(induct stp)
-  apply(simp add: steps.simps)
-  apply(simp add: step_red)
-  apply(auto simp: step.simps fetch.simps dither_def numeral)
+  apply(auto simp: steps.simps step.simps dither_def numeral)
   done
 
-lemma dither_unhalt_rs: 
-  shows "\<not> is_final (steps0 (1, Bk \<up> m, [Oc]) dither stp)"
-using dither_unhalt_state[of m stp]
-by auto
-
 lemma dither_loops:
   shows "{dither_unhalt_inv} dither \<up>" 
 apply(rule Hoare_unhaltI)
-using dither_unhalt_rs
-apply(auto)
-done
+using dither_loops_aux
+apply(auto simp add: numeral)
+by (metis Suc_neq_Zero is_final_eq)
+
 
-lemma dither_halt_rs: 
-  "\<exists>stp. steps0 (1, Bk \<up> m, [Oc, Oc]) dither stp = (0, Bk \<up> m, [Oc, Oc])"
+lemma dither_halts_aux: 
+  shows "steps0 (1, Bk \<up> m, [Oc, Oc]) dither 3 = (0, Bk \<up> m, [Oc, Oc])"
 unfolding dither_def
-apply(rule_tac x = "3" in exI)
-apply(simp add: steps.simps step.simps fetch.simps numeral)
-done 
-
+by (simp add: steps.simps step.simps numeral)
 
 lemma dither_halts:
   shows "{dither_halt_inv} dither {dither_halt_inv}" 
 apply(rule Hoare_haltI)
-using dither_halt_rs
+using dither_halts_aux
 apply(auto)
 by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases)
 
 
 
-section {*
-  The final diagnal arguments to show the undecidability of Halting problem.
-*}
+section {* The diagnal argument below shows the undecidability of Halting problem *}
 
 text {*
   @{text "haltP tp x"} means TM @{text "tp"} terminates on input @{text "x"}
@@ -1124,8 +1113,7 @@
 
 definition haltP :: "tprog \<Rightarrow> nat list \<Rightarrow> bool"
   where
-  "haltP p lm = (\<exists>n a b c. steps (Suc 0, [], <lm>) p n = (0, Bk\<up>a,  Oc\<up>b @ Bk\<up>c))"
-
+  "haltP p lm \<equiv> \<exists>n a b c. steps (Suc 0, [], <lm>) p n = (0, Bk \<up> a,  Oc \<up> b @ Bk \<up> c)"
 
 abbreviation
   "haltP0 p lm \<equiv> haltP (p, 0) lm"