--- a/thys/uncomputable.thy	Wed Jan 23 08:01:35 2013 +0100
+++ b/thys/uncomputable.thy	Wed Jan 23 12:25:24 2013 +0100
@@ -1337,84 +1337,86 @@
     apply(erule_tac x = 0 in allE, simp)
     done
 qed
-  
 
 
-
+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 h_uh: 
   assumes "haltP (tcontra H, 0) [code (tcontra H)]"
   shows "\<not> haltP (tcontra H, 0) [code (tcontra H)]"
-proof(simp only: tcontra_def)
-  let ?tcontr = "(tcopy |+| H) |+| dither"
-  let ?cn = "Suc (code ?tcontr)"
-  let ?P1 = "\<lambda> (l, r). (l = [] \<and> (r::cell list) = Oc\<up>(?cn))"
-  let ?Q1 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)"
-  let ?P2 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)"
-  let ?Q2 = "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]"
-  let ?P3 = ?Q2
-  have "{?P1} ?tcontr \<up>"
-  proof(rule_tac Hoare_plus_unhalt, auto)
-    show "?Q2 \<mapsto> ?P3"
-      apply(simp add: assert_imp_def)
-      done
+proof - 
+  (* code of tcontra *)
+  def code_tcontra \<equiv> "(code (tcontra H))"
+
+  (* 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]"
+
+  (*
+  {P1} tcopy {P2}  {P2} H {P3} 
+  ----------------------------
+     {P1} (tcopy |+| H) {P3}     {P3} dither loops
+  ------------------------------------------------
+           {P1} (tcontra H) loops
+  *)
+
+  have tm1_wf: "tm_wf0 tcopy" by auto
+  have tm2_wf: "tm_wf0 (tcopy |+| H)" by auto
+
+  (* {P1} (tcopy |+| H) {P3} *)
+  have first: "{P1} (tcopy |+| H) {P3}" 
+  proof (induct rule: Hoare_plus_halt_simple)
+    case A_halt (* of tcopy *)
+    have "{inv_init1 (Suc code_tcontra)} tcopy {inv_end0 (Suc code_tcontra)}"
+      unfolding code_tcontra_def
+      by (rule tcopy_correct1) (simp)
+    moreover
+    have "P1 \<mapsto> inv_init1 (Suc code_tcontra)" unfolding P1_def
+      by (simp add: assert_imp_def tape_of_nl_abv)
+    moreover
+    have "inv_end0 (Suc code_tcontra) \<mapsto> P2" unfolding P2_def code_tcontra_def
+      by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv)
+    ultimately
+    show "{P1} tcopy {P2}" by (rule Hoare_weak)
   next
-    show "{?P1} (tcopy |+| H) {?Q2}"
-    proof(rule_tac Hoare_plus_halt, auto)
-      show "?Q1 \<mapsto> ?P2"
-        apply(simp add: assert_imp_def)
-        done
-    next
-      show "{?P1} tcopy {?Q1}"
-      proof -
-        have g: "{inv_init1 ?cn} tcopy {inv_end0 ?cn}"
-          by(rule_tac tcopy_correct1, simp)
-        thus "?thesis"
-        proof(rule_tac Hoare_weak)           
-          show "{inv_init1 ?cn} tcopy
-            {inv_end0 ?cn} " using g by simp
-        next
-          show "?P1 \<mapsto> inv_init1 (?cn)"
-            apply(simp add: inv_init1.simps assert_imp_def)
-            done
-        next
-          show "inv_end0 ?cn \<mapsto> ?Q1"
-            apply(simp add: assert_imp_def inv_end0.simps)
-            done
-        qed
-      qed
-    next
-      show "{?P2} H {?Q2}"
-        using Hoare_def h_newcase[of ?tcontr "[code ?tcontr]" 1] assms
-        unfolding tcontra_def
-        apply(auto)
-        apply(rule_tac x = na in exI)
-        apply(simp add: replicate_Suc tape_of_nl_abv)
-        done
-    qed
-  next
-    show "{?P3} dither \<up>"
-      using Hoare_unhalt_def
-    proof(auto)
-      fix nd n
-      assume "is_final (steps (Suc 0, Bk \<up> nd, [Oc]) (dither, 0) n)"
-      thus "False"
-        using dither_unhalt_rs[of nd n]
-        by simp
-    qed
-  qed    
-  thus "\<not> haltP ((tcopy |+| H) |+| dither, 0) [code ((tcopy |+| H) |+| dither)]"
+    case B_halt
+    show "{P2} H {P3}"
+      using Hoare_def h_newcase[of "tcontra H" "[code_tcontra]" 1] assms
+      unfolding tcontra_def P2_def P3_def code_tcontra_def        
+      apply(auto)
+      apply(rule_tac x = na in exI)
+      apply(simp add: replicate_Suc tape_of_nl_abv)
+      done
+  qed (simp add: tm1_wf)
+
+  (* {P3} dither loops *)
+  have second: "{P3} dither \<up>" unfolding P3_def 
+    by (rule dither_loops)
+  
+  (* {P1} tcontra loops *)
+  have "{P1} (tcontra H) \<up>" unfolding tcontra_def
+    by (rule Hoare_plus_unhalt_simple[OF first second tm2_wf])
+  
+  then show "\<not> haltP (tcontra H, 0) [code_tcontra]"
     using assms
-    unfolding tcontra_def
-    apply(auto simp: haltP_def Hoare_unhalt_def)
+    unfolding tcontra_def code_tcontra_def
+    apply(auto simp: haltP_def Hoare_unhalt_def P1_def)
     apply(erule_tac x = n in allE)
-    apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n")
-    apply(simp add: tape_of_nl_abv)
+    apply(case_tac "steps (Suc 0, [], <[code ((tcopy |+| H) |+| dither)]>) (tcontra H, 0) n")
+    apply(simp add: tape_of_nl_abv tcontra_def code_tcontra_def tape_of_nat_abv)
     done
 qed
-      
+
+
+
       
 text {*
-  @{text "False"} is finally derived.
+  @{text "False"} can finally derived.
 *}
 
 lemma false: "False"