diff -r 0349fa7f5595 -r 4a3cd7d70ec2 thys/uncomputable.thy
--- a/thys/uncomputable.thy	Wed Jan 23 15:06:32 2013 +0100
+++ b/thys/uncomputable.thy	Wed Jan 23 15:33:26 2013 +0100
@@ -1037,33 +1037,52 @@
   The {\em Dithering} TM, when the input is @{text "1"}, it will loop forever, otherwise, it will
   terminate.
 *}
+
 definition dither :: "instr list"
   where
   "dither \<equiv> [(W0, 1), (R, 2), (L, 1), (L, 0)] "
 
-lemma dither_halt_rs: 
-  "\<exists> stp. steps (Suc 0, Bk\<up>m, [Oc, Oc]) (dither, 0) stp = 
-                                 (0, Bk\<up>m, [Oc, Oc])"
-apply(rule_tac x = "Suc (Suc (Suc 0))" in exI)
-apply(simp add: dither_def steps.simps 
-                step.simps fetch.simps numeral)
-done
-
 lemma dither_unhalt_state: 
-  "(steps (Suc 0, Bk\<up>m, [Oc]) (dither, 0) stp = 
-   (Suc 0, Bk\<up>m, [Oc])) \<or> 
-   (steps (Suc 0, Bk\<up>m, [Oc]) (dither, 0) stp = (2, Oc # Bk\<up>m, []))"
-  apply(induct stp, simp add: steps.simps)
-  apply(simp add: step_red, auto)
+  "(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)
   done
 
 lemma dither_unhalt_rs: 
-  "\<not> is_final (steps (Suc 0, Bk\<up>m, [Oc]) (dither,0) stp)"
+  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 "{(\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc])} dither \<up>" 
+apply(rule Hoare_unhaltI)
+using dither_unhalt_rs
 apply(auto)
 done
 
+lemma dither_halt_rs: 
+  "\<exists>stp. steps0 (Suc 0, Bk \<up> m, [Oc, Oc]) dither stp = (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 
+
+definition
+  "dither_halt_inv \<equiv> (\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc])"
+
+lemma dither_halts:
+  shows "{dither_halt_inv} dither {dither_halt_inv}" 
+unfolding dither_halt_inv_def
+apply(rule HoareI)
+using dither_halt_rs
+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.
 *}
@@ -1250,29 +1269,15 @@
   qed
 qed
    
+(* TM that produces the contradiction *)
 definition tcontra :: "instr list \<Rightarrow> instr list"
   where
   "tcontra h \<equiv> (tcopy |+| h) |+| dither"
 
-declare replicate_Suc[simp del]
-
-lemma dither_loops:
-  shows "{(\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc])} dither \<up>" 
-apply(rule Hoare_unhaltI)
-apply(auto intro!: dither_unhalt_rs)
-done
-
-lemma dither_halts:
-  shows 
-  "{(\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc])} dither {(\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc])}" 
-apply(rule HoareI)
-using dither_halt_rs
-apply(auto)
-by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases)
 
 lemma uh_h: 
   assumes "\<not> haltP0 (tcontra H) [code (tcontra H)]"
-  shows "haltP0 (tcontra H) [code (tcontra H)]"
+  shows "False"
 proof -
    (* code of tcontra *)
   def code_tcontra \<equiv> "(code (tcontra H))"
@@ -1282,7 +1287,7 @@
   (* invariants *)
   def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)"
   def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)"
-  def P3 \<equiv> "\<lambda>(l::cell list, r::cell list). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]"
+  def P3 \<equiv> dither_halt_inv
 
   (*
   {P1} tcopy {P2}  {P2} H {P3} 
@@ -1316,11 +1321,11 @@
       using nh_newcase[of "tcontra H" "[code_tcontra]" 1, OF assms', folded code_tcontra_def]
       by (auto)
     then show "{P2} H {P3}"
-      unfolding P2_def P3_def
+      unfolding P2_def P3_def dither_halt_inv_def
       unfolding Hoare_def
       apply(auto)
       apply(rule_tac x = n in exI)
-      apply(simp add: replicate_Suc)
+      apply(simp)
       done
   qed (simp)
 
@@ -1332,8 +1337,8 @@
   have "{P1} (tcontra H) {P3}" unfolding tcontra_def
     by (rule Hoare_plus_halt_simple[OF first second H_wf])
 
-  with assms' have "False"
-    unfolding P1_def P3_def code_tcontra_def
+  with assms' show "False"
+    unfolding P1_def P3_def dither_halt_inv_def code_tcontra_def
     unfolding haltP_def
     unfolding Hoare_def 
     apply(auto)
@@ -1343,13 +1348,11 @@
     apply(erule_tac x = 2 in allE, erule_tac x = 0 in allE)
     apply(simp)
     by (smt replicate_0 replicate_Suc)
-  then show "haltP0 (tcontra H) [code (tcontra H)]"
-    by blast
 qed
 
 lemma h_uh: 
   assumes "haltP0 (tcontra H) [code (tcontra H)]"
-  shows "\<not> haltP0 (tcontra H) [code (tcontra H)]"
+  shows "False"
 proof - 
   (* code of tcontra *)
   def code_tcontra \<equiv> "(code (tcontra H))"
@@ -1397,7 +1400,7 @@
       unfolding Hoare_def
       apply(auto)
       apply(rule_tac x = n in exI)
-      apply(simp add: replicate_Suc)
+      apply(simp)
       done
   qed (simp)
 
@@ -1409,13 +1412,11 @@
   have "{P1} (tcontra H) \<up>" unfolding tcontra_def
     by (rule Hoare_plus_unhalt_simple[OF first second H_wf])
 
-  with assms have "False"
+  with assms show "False"
     unfolding haltP_def
     unfolding P1_def code_tcontra_def
     unfolding Hoare_unhalt_def
     by (auto, metis is_final_eq)  
-  then show "\<not> haltP0 (tcontra H) [code_tcontra]"
-    by blast
 qed
 
 
@@ -1426,10 +1427,12 @@
 *}
 
 lemma false: "False"
-using uh_h h_uh
-by auto
+using uh_h h_uh by auto
 
 end
 
+declare replicate_Suc[simp del]
+
+
 end