diff -r 8dc659af1bd2 -r 4c8325c64dab thys/uncomputable.thy
--- a/thys/uncomputable.thy	Fri Jan 25 22:12:01 2013 +0000
+++ b/thys/uncomputable.thy	Sat Jan 26 01:36:48 2013 +0000
@@ -204,16 +204,16 @@
   inv_loop6_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
   inv_loop6_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 where
-  "inv_loop1_loop x (l, r) = (\<exists> i j. i + j + 1 = x \<and> l = Oc\<up>i \<and> r = Oc # Oc # Bk\<up>j @ Oc\<up>j \<and> j > 0)"
-| "inv_loop1_exit x (l, r) = (l = [] \<and> r = Bk # Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0)"
+  "inv_loop1_loop x (l, r) = (\<exists> i j. i + j + 1 = x \<and> (l, r) = (Oc\<up>i, Oc#Oc#Bk\<up>j @ Oc\<up>j) \<and> j > 0)"
+| "inv_loop1_exit x (l, r) = ((l, r) = ([], Bk#Oc#Bk\<up>x @ Oc\<up>x) \<and> x > 0)"
 | "inv_loop5_loop x (l, r) = 
-     (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> t > 0 \<and> l = Oc\<up>k@Bk\<up>j@Oc\<up>i \<and> r = Oc\<up>t)"
+     (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> t > 0 \<and> (l, r) = (Oc\<up>k@Bk\<up>j@Oc\<up>i, Oc\<up>t))"
 | "inv_loop5_exit x (l, r) = 
-     (\<exists> i j. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and>  l = Bk\<up>(j - 1)@Oc\<up>i \<and> r = Bk # Oc\<up>j)"
+     (\<exists> i j. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> (l, r) = (Bk\<up>(j - 1)@Oc\<up>i, Bk # Oc\<up>j))"
 | "inv_loop6_loop x (l, r) = 
-     (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> k + t + 1 = j \<and> l = Bk\<up>k @ Oc\<up>i \<and> r = Bk\<up>(Suc t) @ Oc\<up>j)"
+     (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> k + t + 1 = j \<and> (l, r) = (Bk\<up>k @ Oc\<up>i, Bk\<up>(Suc t) @ Oc\<up>j))"
 | "inv_loop6_exit x (l, r) = 
-     (\<exists> i j. i + j = x \<and> j > 0 \<and> l = Oc\<up>i \<and> r = Oc # Bk\<up>j @ Oc\<up>j)"
+     (\<exists> i j. i + j = x \<and> j > 0 \<and> (l, r) = (Oc\<up>i, Oc#Bk\<up>j @ Oc\<up>j))"
 
 fun 
   inv_loop0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
@@ -224,13 +224,13 @@
   inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
   inv_loop6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 where
-  "inv_loop0 x (l, r) =  (l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0 )"
+  "inv_loop0 x (l, r) =  ((l, r) = ([Bk], Oc # Bk\<up>x @ Oc\<up>x) \<and> x > 0)"
 | "inv_loop1 x (l, r) = (inv_loop1_loop x (l, r) \<or> inv_loop1_exit x (l, r))"
-| "inv_loop2 x (l, r) = (\<exists> i j any. i + j = x \<and> x > 0 \<and> i > 0 \<and> j > 0 \<and> l = Oc\<up>i \<and> r = any#Bk\<up>j@Oc\<up>j)"
+| "inv_loop2 x (l, r) = (\<exists> i j any. i + j = x \<and> x > 0 \<and> i > 0 \<and> j > 0 \<and> (l, r) = (Oc\<up>i, any#Bk\<up>j@Oc\<up>j))"
 | "inv_loop3 x (l, r) = 
-     (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = Suc j \<and> l = Bk\<up>k@Oc\<up>i \<and> r = Bk\<up>t@Oc\<up>j)"
+     (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = Suc j \<and> (l, r) = (Bk\<up>k@Oc\<up>i, Bk\<up>t@Oc\<up>j))"
 | "inv_loop4 x (l, r) = 
-     (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = j \<and> l = Oc\<up>k @ Bk\<up>(Suc j)@Oc\<up>i \<and> r = Oc\<up>t)"
+     (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = j \<and> (l, r) = (Oc\<up>k @ Bk\<up>(Suc j)@Oc\<up>i, Oc\<up>t))"
 | "inv_loop5 x (l, r) = (inv_loop5_loop x (l, r) \<or> inv_loop5_exit x (l, r))"
 | "inv_loop6 x (l, r) = (inv_loop6_loop x (l, r) \<or> inv_loop6_exit x (l, r))"
 
@@ -1026,7 +1026,7 @@
 
 definition haltP :: "tprog \<Rightarrow> nat list \<Rightarrow> bool"
   where
-  "haltP p lm \<equiv> \<exists>n a b c. steps (1, [], <lm>) p n = (0, Bk \<up> a,  Oc \<up> b @ Bk \<up> c)"
+  "haltP p lm \<equiv> \<exists>n a m. steps (1, [], <lm>) p n = (0, Bk \<up> a,  <m::nat>)"
 
 abbreviation
   "haltP0 p lm \<equiv> haltP (p, 0) lm" 
@@ -1057,9 +1057,9 @@
   The following two assumptions specifies that @{text "H"} does solve the Halting problem.
   *}
   and h_case: 
-  "\<And> M lm. (haltP0 M lm) \<Longrightarrow> \<exists> na nb. (steps0 (1, [Bk], <code M # lm>) H na = (0, Bk \<up> nb, [Oc]))"
+  "\<And> M lm. (haltP0 M lm) \<Longrightarrow> \<exists>stp n. (steps0 (1, [Bk], <code M#lm>) H stp = (0, Bk \<up> n, [Oc]))"
   and nh_case: 
-  "\<And> M lm. (\<not> haltP0 M lm) \<Longrightarrow> \<exists> na nb. (steps0 (1, [Bk], <code M # lm>) H na = (0, Bk \<up> nb, [Oc, Oc]))"
+  "\<And> M lm. (\<not> haltP0 M lm) \<Longrightarrow> \<exists>stp n. (steps0 (1, [Bk], <code M#lm>) H stp = (0, Bk \<up> n, [Oc, Oc]))"
 begin
 
 (* invariants for H *)
@@ -1079,7 +1079,7 @@
 proof -
   obtain stp i
     where "steps0 (1, [Bk], <[code M, n]>) H stp = (0, Bk \<up> i, [Oc, Oc])"
-    using nh_case[of "M" "[n]", OF assms] by auto
+    using nh_case assms by blast
   then show "{pre_H_inv M n} H {post_H_halt_inv}"
     unfolding Hoare_halt_def
     apply(auto)
@@ -1094,7 +1094,7 @@
 proof -
   obtain stp i
     where "steps0 (1, [Bk], <[code M, n]>) H stp = (0, Bk \<up> i, [Oc])"
-    using h_case[of "M" "[n]", OF assms] by auto 
+    using h_case assms by blast
   then show "{pre_H_inv M n} H {post_H_unhalt_inv}"
     unfolding Hoare_halt_def
     apply(auto)
@@ -1156,11 +1156,11 @@
     unfolding haltP_def
     unfolding Hoare_halt_def 
     apply(auto)
-    apply(erule_tac x = n in allE)
+    apply(drule_tac x = n in spec)
     apply(case_tac "steps0 (Suc 0, [], <[code tcontra]>) tcontra n")
-    apply(simp, auto)
-    apply(erule_tac x = 2 in allE, erule_tac x = 0 in allE)
-    apply(simp add: numeral)
+    apply(auto)
+    apply(drule_tac x = 1 in spec)
+    apply(simp add: numeral tape_of_nat_abv)
     done
 qed