--- a/Paper/Paper.thy	Fri Jan 25 22:12:01 2013 +0000
+++ b/Paper/Paper.thy	Sat Jan 26 01:36:48 2013 +0000
@@ -531,16 +531,19 @@
   We often need to restrict tapes to be in \emph{standard form}, which means 
   the left list of the tape is either empty or only contains @{text "Bk"}s, and 
   the right list contains some ``clusters'' of @{text "Oc"}s separted by single 
-  blanks and can be followed by some blanks. To make this formal we define the 
-  following function
+  blanks. To make this formal we define the following function
   
   \begin{center}
-  foo
+  \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+  @{thm (lhs) tape_of_nat_list.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list.simps(1)}\\
+  @{thm (lhs) tape_of_nat_list.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list.simps(2)}\\
+  @{thm (lhs) tape_of_nat_list.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list.simps(3)}
+  \end{tabular}
   \end{center}
 
   \noindent
-  A standard tape is then of the form @{text "(Bk\<^isup>k,\<langle>n\<^isub>1,...,n\<^isub>m\<rangle> @ Bk\<^isup>l)"} for some @{text k},
-  @{text l} and @{text "n\<^isub>i"}. Note that the head in a standard tape ``points'' to the 
+  A standard tape is then of the form @{text "(Bk\<^isup>l,\<langle>n\<^isub>1,...,n\<^isub>m\<rangle>)"} for some @{text l} 
+  and @{text "n\<^isub>i"}. Note that the head in a standard tape ``points'' to the 
   leftmost @{term "Oc"} on the tape.
 
 

Binary file paper.pdf has changed

--- a/thys/turing_basic.thy	Fri Jan 25 22:12:01 2013 +0000
+++ b/thys/turing_basic.thy	Sat Jan 26 01:36:48 2013 +0000
@@ -194,13 +194,15 @@
   "tape_of_nat_list [n] = Oc\<up>(Suc n)" |
   "tape_of_nat_list (n#ns) = Oc\<up>(Suc n) @ Bk # (tape_of_nat_list ns)"
 
-defs (overloaded)
-  tape_of_nl_abv: "<am> \<equiv> tape_of_nat_list am"
-  tape_of_nat_abv : "<(n::nat)> \<equiv> Oc\<up>(Suc n)"
+fun tape_of_nat_pair :: "nat \<times> nat \<Rightarrow> cell list" 
+  where 
+  "tape_of_nat_pair (n, m) = Oc\<up>(Suc n) @ [Bk] @ Oc\<up>(Suc m)" 
+
 
-definition tinres :: "cell list \<Rightarrow> cell list \<Rightarrow> bool"
-  where
-  "tinres xs ys = (\<exists>n. xs = ys @ Bk \<up> n \<or> ys = xs @ Bk \<up> n)"
+defs (overloaded)
+  tape_of_nl_abv: "<ns> \<equiv> tape_of_nat_list ns"
+  tape_of_nat_abv: "<(n::nat)> \<equiv> Oc\<up>(Suc n)"
+  tape_of_nat_pair: "<p> \<equiv> tape_of_nat_pair p"
 
 fun 
   shift :: "instr list \<Rightarrow> nat \<Rightarrow> instr list"

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