--- a/thys/turing_hoare.thy	Wed Jan 23 08:01:35 2013 +0100
+++ b/thys/turing_hoare.thy	Wed Jan 23 12:25:24 2013 +0100
@@ -35,7 +35,7 @@
 unfolding Hoare_def 
 using assms by auto
 
-lemma Hoare_unhalt_I:
+lemma Hoare_unhaltI:
   assumes "\<And>l r n. P (l, r) \<Longrightarrow> \<not> is_final (steps0 (1, (l, r)) p n)"
   shows "{P} p \<up>"
 unfolding Hoare_unhalt_def 
@@ -92,6 +92,15 @@
     using b1 b2 by (rule_tac x = "n2 + n3" in exI) (simp)
 qed
 
+lemma Hoare_plus_halt_simple [case_names A_halt B_halt A_wf]: 
+  assumes A_halt : "{P1} A {P2}"
+  and B_halt : "{P2} B {P3}"
+  and A_wf : "tm_wf (A, 0)"
+  shows "{P1} A |+| B {P3}"
+by (rule Hoare_plus_halt[OF A_halt B_halt _ A_wf])
+   (simp add: assert_imp_def)
+
+
 
 text {*
   {P1} A {Q1}   {P2} B loops    Q1 \<mapsto> P2   A well-formed
@@ -99,16 +108,13 @@
           {P1} A |+| B  loops
 *}
 
-
-
-
 lemma Hoare_plus_unhalt:
   assumes A_halt: "{P1} A {Q1}"
   and B_uhalt: "{P2} B \<up>"
   and a_imp: "Q1 \<mapsto> P2"
   and A_wf : "tm_wf (A, 0)"
   shows "{P1} (A |+| B) \<up>"
-proof(rule_tac Hoare_unhalt_I)
+proof(rule_tac Hoare_unhaltI)
   fix n l r 
   assume h: "P1 (l, r)"
   then obtain n1 l' r'
@@ -145,6 +151,15 @@
   qed
 qed
 
+lemma Hoare_plus_unhalt_simple [case_names A_halt B_unhalt A_wf]: 
+ assumes A_halt: "{P1} A {P2}"
+  and B_uhalt: "{P2} B \<up>"
+  and A_wf : "tm_wf (A, 0)"
+  shows "{P1} (A |+| B) \<up>"
+by (rule Hoare_plus_unhalt[OF A_halt B_uhalt _ A_wf])
+   (simp add: assert_imp_def)
+
+
 lemma Hoare_weak:
   assumes a: "{P} p {Q}"
   and b: "P' \<mapsto> P" 

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