diff -r 860f05037c36 -r fe7a257bdff4 thys/uncomputable.thy
--- a/thys/uncomputable.thy	Wed Jan 30 02:29:47 2013 +0000
+++ b/thys/uncomputable.thy	Wed Jan 30 03:33:05 2013 +0000
@@ -895,16 +895,18 @@
 proof -
   have "{inv_begin1 x} tcopy_begin {inv_begin0 x}"
     by (metis assms begin_correct) 
-  moreover
-  have "{inv_loop1 x} tcopy_loop {inv_loop0 x}"
-    by (metis assms loop_correct) 
-  moreover
+  moreover 
   have "inv_begin0 x \<mapsto> inv_loop1 x"
     unfolding assert_imp_def
     unfolding inv_begin0.simps inv_loop1.simps
     unfolding inv_loop1_loop.simps inv_loop1_exit.simps
     apply(auto simp add: numeral Cons_eq_append_conv)
     by (rule_tac x = "Suc 0" in exI, auto)
+  ultimately have "{inv_begin1 x} tcopy_begin {inv_loop1 x}"
+    by (rule_tac Hoare_consequence) (auto)
+  moreover
+  have "{inv_loop1 x} tcopy_loop {inv_loop0 x}"
+    by (metis assms loop_correct) 
   ultimately 
   have "{inv_begin1 x} (tcopy_begin |+| tcopy_loop) {inv_loop0 x}"
     by (rule_tac Hoare_plus_halt) (auto)
@@ -912,7 +914,7 @@
   have "{inv_end1 x} tcopy_end {inv_end0 x}"
     by (metis assms end_correct) 
   moreover 
-  have "inv_loop0 x \<mapsto> inv_end1 x"
+  have "inv_loop0 x = inv_end1 x"
     by(auto simp: inv_end1.simps inv_loop1.simps assert_imp_def)
   ultimately 
   show "{inv_begin1 x} tcopy {inv_end0 x}"
@@ -955,10 +957,10 @@
 
 (* invariants of dither *)
 abbreviation (input)
-  "dither_halt_inv \<equiv> \<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <1::nat>))"
+  "dither_halt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"
 
 abbreviation (input)
-  "dither_unhalt_inv \<equiv> \<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <0::nat>))"
+  "dither_unhalt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"
 
 lemma dither_loops_aux: 
   "(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or> 
@@ -974,7 +976,6 @@
 apply(auto simp add: numeral tape_of_nat_abv)
 by (metis Suc_neq_Zero is_final_eq)
 
-
 lemma dither_halts_aux: 
   shows "steps0 (1, Bk \<up> m, [Oc, Oc]) dither 2 = (0, Bk \<up> m, [Oc, Oc])"
 unfolding dither_def
@@ -988,7 +989,6 @@
 by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases)
 
 
-
 section {* The diagnal argument below shows the undecidability of Halting problem *}
 
 text {*
@@ -998,7 +998,7 @@
 
 definition haltP :: "tprog0 \<Rightarrow> nat list \<Rightarrow> bool"
   where
-  "haltP p lm \<equiv> {(\<lambda>tp. tp = ([], <lm>))} p {(\<lambda>tp. (\<exists>k n. tp = (Bk \<up> k,  <n::nat>)))}"
+  "haltP p ns \<equiv> {(\<lambda>tp. tp = ([], <ns>))} p {(\<lambda>tp. (\<exists>k n. tp = (Bk \<up> k,  <n::nat>)))}"
 
 lemma [intro, simp]: "tm_wf0 tcopy"
 by (auto simp: tcopy_def)
@@ -1026,9 +1026,9 @@
   The following two assumptions specifies that @{text "H"} does solve the Halting problem.
   *}
   and h_case: 
-  "\<And> M lm. haltP M lm \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <code M#lm>))} H {(\<lambda>tp. \<exists>n. tp = (Bk \<up> n, <0::nat>))}"
+  "\<And> M ns. haltP M ns \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <code M#ns>))} H {(\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>))}"
   and nh_case: 
-  "\<And> M lm. \<not> haltP M lm \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <code M#lm>))} H {(\<lambda>tp. \<exists>n. tp = (Bk \<up> n, <1::nat>))}"
+  "\<And> M ns. \<not> haltP M ns \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <code M#ns>))} H {(\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>))}"
 begin
 
 (* invariants for H *)
@@ -1036,10 +1036,10 @@
   "pre_H_inv M n \<equiv> \<lambda>tp. tp = ([Bk], <[code M, n]>)"
 
 abbreviation
-  "post_H_halt_inv \<equiv> \<lambda>tp. \<exists>n. tp = (Bk \<up> n, <1::nat>)"
+  "post_H_halt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"
 
 abbreviation
-  "post_H_unhalt_inv \<equiv> \<lambda>tp. \<exists>n. tp = (Bk \<up> n, <0::nat>)"
+  "post_H_unhalt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"
 
 
 lemma H_halt_inv:
@@ -1067,7 +1067,7 @@
   (* invariants *)
   def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <[code_tcontra]>)"
   def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <[code_tcontra, code_tcontra]>)"
-  def P3 \<equiv> "\<lambda>tp. \<exists>n. tp = (Bk \<up> n, <1::nat>)"
+  def P3 \<equiv> "\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"
 
   (*
   {P1} tcopy {P2}  {P2} H {P3} 
@@ -1081,7 +1081,7 @@
 
   (* {P1} (tcopy |+| H) {P3} *)
   have first: "{P1} (tcopy |+| H) {P3}" 
-  proof (cases rule: Hoare_plus_halt_simple)
+  proof (cases rule: Hoare_plus_halt)
     case A_halt (* of tcopy *)
     show "{P1} tcopy {P2}" unfolding P1_def P2_def 
       by (rule tcopy_correct)
@@ -1099,7 +1099,7 @@
   (* {P1} tcontra {P3} *)
   have "{P1} tcontra {P3}" 
     unfolding tcontra_def
-    by (rule Hoare_plus_halt_simple[OF first second H_wf])
+    by (rule Hoare_plus_halt[OF first second H_wf])
 
   with assms show "False"
     unfolding P1_def P3_def
@@ -1120,7 +1120,7 @@
   (* invariants *)
   def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <[code_tcontra]>)"
   def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <[code_tcontra, code_tcontra]>)"
-  def Q3 \<equiv> "\<lambda>tp. \<exists>n. tp = (Bk \<up> n, <0::nat>)"
+  def Q3 \<equiv> "\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"
 
   (*
   {P1} tcopy {P2}  {P2} H {Q3} 
@@ -1134,7 +1134,7 @@
 
   (* {P1} (tcopy |+| H) {Q3} *)
   have first: "{P1} (tcopy |+| H) {Q3}" 
-  proof (cases rule: Hoare_plus_halt_simple)
+  proof (cases rule: Hoare_plus_halt)
     case A_halt (* of tcopy *)
     show "{P1} tcopy {P2}" unfolding P1_def P2_def
       by (rule tcopy_correct)
@@ -1152,7 +1152,7 @@
   (* {P1} tcontra loops *)
   have "{P1} tcontra \<up>" 
     unfolding tcontra_def
-    by (rule Hoare_plus_unhalt_simple[OF first second H_wf])
+    by (rule Hoare_plus_unhalt[OF first second H_wf])
 
   with assms show "False"
     unfolding P1_def