# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1359682477 0
# Node ID 2cae8a39803e5444c17dfff73274beaaf67d47f6
# Parent  01f688735b9b704288d3d7f6c2c1aeb519956d66
updated paper

diff -r 01f688735b9b -r 2cae8a39803e Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Jan 31 11:35:16 2013 +0000
+++ b/Paper/Paper.thy	Fri Feb 01 01:34:37 2013 +0000
@@ -22,16 +22,14 @@
   update2 ("update") and
   tm_wf0 ("wf") and
   (*is_even ("iseven") and*)
-  tcopy_begin ("copy\<^bsub>begin\<^esub>") and
-  tcopy_loop ("copy\<^bsub>loop\<^esub>") and
-  tcopy_end ("copy\<^bsub>end\<^esub>") and
+  tcopy_begin ("cbegin") and
+  tcopy_loop ("cloop") and
+  tcopy_end ("cend") and
   step0 ("step") and
-  uncomputable.tcontra ("C") and
+  uncomputable.tcontra ("tcontra") and
   steps0 ("steps") and
   exponent ("_\<^bsup>_\<^esup>") and
-(*  abc_lm_v ("lookup") and
-  abc_lm_s ("set") and*)
-  haltP ("stdhalt") and 
+  haltP ("halts") and 
   tcopy ("copy") and 
   tape_of ("\<langle>_\<rangle>") and 
   tm_comp ("_ \<oplus> _") and 
@@ -41,7 +39,12 @@
   inv_begin2 ("I\<^isub>2") and
   inv_begin3 ("I\<^isub>3") and
   inv_begin4 ("I\<^isub>4") and 
-  inv_begin ("I\<^bsub>begin\<^esub>")
+  inv_begin ("I\<^bsub>cbegin\<^esub>") and
+  inv_loop1 ("J\<^isub>1") and
+  inv_loop0 ("J\<^isub>0") and
+  inv_end1 ("K\<^isub>1") and
+  inv_end0 ("K\<^isub>0") and
+  measure_begin_step ("M\<^bsub>cbegin\<^esub>")
 
  
 lemma inv_begin_print:
@@ -71,6 +74,13 @@
 done
 
 
+lemma measure_begin_print:
+  shows "s = 2 \<Longrightarrow> measure_begin_step (s, l, r) = length r" and
+        "s = 3 \<Longrightarrow> measure_begin_step (s, l, r) = (if r = [] \<or> r = [Bk] then 1 else 0)" and
+        "s = 4 \<Longrightarrow> measure_begin_step (s, l, r) = length l" and 
+        "s \<notin> {2,3,4} \<Longrightarrow> measure_begin_step (s, l, r) = 0"
+by (simp_all)
+
 declare [[show_question_marks = false]]
 
 (* THEOREMS *)
@@ -900,20 +910,28 @@
 
   \begin{figure}[t]
   \begin{center}
-  \begin{tabular}{@ {}lcl@ {\hspace{-2cm}}l@ {}}
-  @{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\
-                                &             & @{thm (rhs) inv_begin02} \\
+  \begin{tabular}{@ {}lcl@ {\hspace{-0.5cm}}l@ {}}
+  \hline
   @{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\
   @{thm (lhs) inv_begin2.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin2.simps}\\
   @{thm (lhs) inv_begin3.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin3.simps}\\
   @{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps}\\
+  @{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\
+                                &             & @{thm (rhs) inv_begin02}\smallskip \\
+   \hline
   @{thm (lhs) inv_loop1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop1_loop.simps} @{text "\<or>"}\\
-                               &             & @{thm (rhs) inv_loop1_exit.simps}\\
-  @{thm (lhs) inv_loop0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop0.simps}\\
+                               &             & @{thm (rhs) inv_loop1_exit.simps} & (starting state)\\
+  @{thm (lhs) inv_loop0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop0.simps}& (halting state)\smallskip\\
+   \hline
+  @{thm (lhs) inv_end1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end1.simps} & (starting state)\\
+  @{thm (lhs) inv_end0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end0.simps} & (halting state)\smallskip\\
+  \hline
   \end{tabular}
   \end{center}
-  \caption{The invariants for each state of @{term tcopy_begin}. They depend on
-  the number @{term n} of @{term Oc}s with which this Turing machine is started.}\label{invbegin}
+  \caption{The invariants @{term inv_begin0},\ldots,@{term inv_begin4} for the states of 
+  @{term tcopy_begin}. Below, the invariants for the starting and halting states of
+  @{term tcopy_loop} and @{term tcopy_end}. In each invariant the parameter @{term n} stands for the number
+  of @{term Oc}s with which the Turing machine is started.}\label{invbegin}
   \end{figure}
 
   \begin{center}
@@ -932,41 +950,90 @@
   This invariant depends on @{term n} representing the number of
   @{term Oc}s (or encoded number) on the tape. It is not hard (26
   lines of automated proof script) to show that for @{term "n >
-  (0::nat)"} this invariant is preserved under computation rules
-  @{term step} and @{term steps}.
+  (0::nat)"} this invariant is preserved under the computation rules
+  @{term step} and @{term steps}. This gives us partial correctness
+  for @{term "tcopy_begin"}. 
 
-  measure for the copying TM, which we however omit.
+  We next need to show that @{term "tcopy_begin"} terminates. For this
+  we introduce lexicographically ordered pairs @{term "(n, m)"}
+  derived from configurations @{text "(s, (l, r))"}: @{text n} stands
+  for the state ordered according to how @{term tcopy_begin} executes
+  them, that is @{text "1 > 2 > 3 > 4 > 0"}; @{term m} is calculated
+  according to the measure function:
 
-  
   \begin{center}
-  @{thm begin_correct}\\
-  @{thm loop_correct}\\
-  @{thm end_correct}
+  \begin{tabular}{rcl}
+  @{term measure_begin_step}@{text "(s, (l, r))"} & @{text "\<equiv>"} & 
+  @{text "if"} @{thm (prem 1) measure_begin_print(1)} @{text then} @{thm (rhs) measure_begin_print(1)}\\
+  & & @{text else} @{text "if"} @{thm (prem 1) measure_begin_print(2)} @{text then} @{thm (rhs) measure_begin_print(2)} \\
+ & & @{text else} @{text "if"} @{thm (prem 1) measure_begin_print(3)} @{text then} @{thm (rhs) measure_begin_print(3)}\\
+  & & @{text else} @{thm (rhs) measure_begin_print(4)}\\
+  \end{tabular}
+  \end{center}
+  
+  \noindent
+  With this in place, we can show that for every starting tape of the
+  form @{term "([], Oc \<up> n)"} with @{term "n > (0::nat)"}, the Turing
+  machine @{term "tcopy_begin"} will halt. Taking this and the partial
+  correctness proof together we obtain for @{term tcopy_begin} (similar 
+  resoning is needed for @{term tcopy_loop} and @{term tcopy_end}):
+   
+
+  \begin{center}
+  @{thm (concl) begin_correct}\hspace{6mm}
+  @{thm (concl) loop_correct}\hspace{6mm}
+  @{thm (concl) end_correct}
   \end{center}
 
+  \noindent 
+  where we assume @{text "0 < n"}. Since @{term "inv_begin0 n \<mapsto> inv_loop1 n"} holds
+  and @{term "inv_loop0 n = inv_end1 n"}, we can derive using our Hoare-rules
+  the correctness of @{term tcopy}
 
+  \begin{center}
+  @{thm tcopy_correct}
+  \end{center}
+
+  Finally, we are in the position to prove the undecidability of the halting problem.
+  A program @{term p} started with a standard tape containing the (encoded) numbers
+  @{term ns} will \emph{halt} with a standard tape containging a single (encoded) 
+  number is defined as
 
   \begin{center}
   @{thm haltP_def}
   \end{center}
 
-
-  Undecidability of the halting problem.
-
-  We assume a coding function from Turing machine programs to natural numbers.
-  
+  \noindent
+  This means we considering only Turing machine programs representing functions that take 
+  some numbers as input and produce a single number as output. There is no Turing
+  machine that can decide the halting problem (answer @{text 0} for halting and 
+  @{text 1} for looping). Given our correctness proofs for @{term dither} and @{term tcopy} 
+  this non-existence is relatively straightforward to establish. We first assume there is a coding 
+  function, written @{term code}, from Turing machine programs to natural numbers.
+  Suppose a Turing machine @{term H} exists such that if started with the standard 
+  tape @{term "([Bk], <(code M, ns)>)"} returns @{text 0} or @{text 1} depending
+  on whether @{text M} halts when started with the input tape containing @{term "<ns>"}.
+  This is formalised as follows
+ 
+  \begin{center}
+  \begin{tabular}{r}
   @{thm (prem 2) uncomputable.h_case} implies
-  @{thm (concl) uncomputable.h_case}
+  @{thm (concl) uncomputable.h_case}\\
   
   @{thm (prem 2) uncomputable.nh_case} implies
   @{thm (concl) uncomputable.nh_case}
+  \end{tabular}
+  \end{center}
 
-  Then contradiction
+  \noindent
+  The contradiction can be derived using the following Turing machine
 
   \begin{center}
   @{term "tcontra"} @{text "\<equiv>"} @{term "(tcopy |+| H) |+| dither"}
   \end{center}
 
+  \noindent
+  Let us assume @{thm (prem 2) "uncomputable.tcontra_halt"}
   Proof
 
   \begin{center}
diff -r 01f688735b9b -r 2cae8a39803e paper.pdf
Binary file paper.pdf has changed
diff -r 01f688735b9b -r 2cae8a39803e thys/uncomputable.thy
--- a/thys/uncomputable.thy	Thu Jan 31 11:35:16 2013 +0000
+++ b/thys/uncomputable.thy	Fri Feb 01 01:34:37 2013 +0000
@@ -63,8 +63,6 @@
 | "inv_begin3 n (l, r) = (n > 0 \<and> (l, tl r) = (Bk # Oc \<up> n, []))"
 | "inv_begin4 n (l, r) = (n > 0 \<and> (l, r) = (Oc \<up> n, [Bk, Oc]) \<or> (l, r) = (Oc \<up> (n - 1), [Oc, Bk, Oc]))"
 
-
-
 fun inv_begin :: "nat \<Rightarrow> config \<Rightarrow> bool"
   where
   "inv_begin n (s, tp) = 
@@ -80,9 +78,9 @@
 by (rule_tac x = "Suc i" in exI, simp)
 
 lemma inv_begin_step: 
-  assumes "inv_begin x cf"
-  and "x > 0"
-  shows "inv_begin x (step0 cf tcopy_begin)"
+  assumes "inv_begin n cf"
+  and "n > 0"
+  shows "inv_begin n (step0 cf tcopy_begin)"
 using assms
 unfolding tcopy_begin_def
 apply(case_tac cf)
@@ -94,9 +92,9 @@
 done
 
 lemma inv_begin_steps: 
-  assumes "inv_begin x cf"
-  and "x > 0"
-  shows "inv_begin x (steps0 cf tcopy_begin stp)"
+  assumes "inv_begin n cf"
+  and "n > 0"
+  shows "inv_begin n (steps0 cf tcopy_begin stp)"
 apply(induct stp)
 apply(simp add: assms)
 apply(auto simp del: steps.simps)
@@ -104,23 +102,22 @@
 apply(simp_all add: assms)
 done
 
-(*
 lemma begin_partial_correctness:
-  assumes "\<exists>stp. is_final (steps0 (1, [], Oc \<up> n) tcopy_begin stp)"
+  assumes "is_final (steps0 (1, [], Oc \<up> n) tcopy_begin stp)"
   shows "0 < n \<Longrightarrow> {inv_begin1 n} tcopy_begin {inv_begin0 n}"
-using assms 
-apply(auto simp add: Hoare_halt_def)
-apply(rule_tac x="stp" in exI)
-apply(simp)
-apply(case_tac "steps0 (Suc 0, [], Oc \<up> n) tcopy_begin stp")
-apply(simp)
-apply(case_tac n)
-apply(simp)
-apply(simp)
-apply(case_tac nat)
-apply(simp)
-apply(simp)
-*)
+proof(rule_tac Hoare_haltI)
+  fix l r
+  assume h: "0 < n" "inv_begin1 n (l, r)"
+  have "inv_begin n (steps0 (1, [], Oc \<up> n) tcopy_begin stp)"
+    using h by (rule_tac inv_begin_steps) (simp_all add: inv_begin.simps)
+  then show
+    "\<exists>stp. is_final (steps0 (1, l, r) tcopy_begin stp) \<and> 
+    inv_begin0 n holds_for steps (1, l, r) (tcopy_begin, 0) stp"
+    using h assms
+    apply(rule_tac x = stp in exI)
+    apply(case_tac "(steps0 (1, [], Oc \<up> n) tcopy_begin stp)", simp add: inv_begin.simps)
+    done
+qed
 
 fun measure_begin_state :: "config \<Rightarrow> nat"
   where
@@ -135,69 +132,44 @@
          else 0)"
 
 definition
-  "begin_LE = measures [measure_begin_state, measure_begin_step]"
+  "measure_begin = measures [measure_begin_state, measure_begin_step]"
 
-lemma [simp]: "\<lbrakk>tl r = []; r \<noteq> []; r \<noteq> [Bk]\<rbrakk> \<Longrightarrow> r = [Oc]"
-by (case_tac r, auto, case_tac a, auto)
+lemma wf_measure_begin:
+  shows "wf measure_begin" 
+unfolding measure_begin_def 
+by auto
 
-
-lemma halt_lemma: 
-  "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
+lemma measure_begin_induct [case_names Step]: 
+  "\<lbrakk>\<And>n. \<not> P (f n) \<Longrightarrow> (f (Suc n), (f n)) \<in> measure_begin\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
+using wf_measure_begin
 by (metis wf_iff_no_infinite_down_chain)
 
-lemma begin_halt: 
-  "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (1, [], Oc \<up> x) tcopy_begin stp)"
-proof(rule_tac LE = begin_LE in halt_lemma) 
-  show "wf begin_LE" unfolding begin_LE_def by (auto) 
-next
-  assume h: "0 < x"
-  show "\<forall>n. \<not> is_final (steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow>
-        (steps (1, [], Oc \<up> x) (tcopy_begin, 0) (Suc n), 
-            steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE"
-  proof(rule_tac allI, rule_tac impI)
-    fix n
-    assume a: "\<not> is_final (steps (1, [], Oc \<up> x) (tcopy_begin, 0) n)"
-    have b: "inv_begin x (steps (1, [], Oc \<up> x) (tcopy_begin, 0) n)"
-      apply(rule_tac inv_begin_steps)
-      apply(simp_all add: inv_begin.simps h)
-      done 
-    obtain s l r where c: "(steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) = (s, l, r)"
-      apply(case_tac "steps (1, [], Oc \<up> x) (tcopy_begin, 0) n", auto)
-      done
-    moreover hence "inv_begin x (s, l, r)" 
-      using c b by simp
-    ultimately show "(steps (1, [], Oc \<up> x) (tcopy_begin, 0) (Suc n), 
-      steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE"
-      using a 
-    proof(simp del: inv_begin.simps step.simps steps.simps)
-      assume "inv_begin x (s, l, r)" "0 < s"
-      thus "(step (s, l, r) (tcopy_begin, 0), s, l, r) \<in> begin_LE"
-        apply(auto simp: begin_LE_def step.simps tcopy_begin_def numeral split: if_splits)
-        apply(case_tac r, auto, case_tac a, auto)
-        done
-    qed
-  qed
+lemma begin_halts: 
+  assumes h: "x > 0"
+  shows "\<exists> stp. is_final (steps0 (1, [], Oc \<up> x) tcopy_begin stp)"
+proof (induct rule: measure_begin_induct) 
+  case (Step n)
+  have "\<not> is_final (steps0 (1, [], Oc \<up> x) tcopy_begin n)" by fact
+  moreover
+  have "inv_begin x (steps0 (1, [], Oc \<up> x) tcopy_begin n)"
+    by (rule_tac inv_begin_steps) (simp_all add: inv_begin.simps h)
+  moreover
+  obtain s l r where eq: "(steps0 (1, [], Oc \<up> x) tcopy_begin n) = (s, l, r)"
+    by (metis measure_begin_state.cases)
+  ultimately 
+  have "(step0 (s, l, r) tcopy_begin, s, l, r) \<in> measure_begin"
+    apply(auto simp: measure_begin_def tcopy_begin_def numeral split: if_splits)
+    apply(subgoal_tac "r = [Oc]")
+    apply(auto)
+    by (metis cell.exhaust list.exhaust tl.simps(2))
+  then 
+  show "(steps0 (1, [], Oc \<up> x) tcopy_begin (Suc n), steps0 (1, [], Oc \<up> x) tcopy_begin n) \<in> measure_begin"
+    using eq by (simp only: step_red)
 qed
-    
+
 lemma begin_correct: 
-  "0 < n \<Longrightarrow> {inv_begin1 n} tcopy_begin {inv_begin0 n}"
-proof(rule_tac Hoare_haltI)
-  fix l r
-  assume h: "0 < n" "inv_begin1 n (l, r)"
-  then have "\<exists> stp. is_final (steps0 (1, [], Oc \<up> n) tcopy_begin stp)"
-    by (rule_tac begin_halt)    
-  then obtain stp where "is_final (steps0 (1, [], Oc \<up> n) tcopy_begin stp)" ..
-  moreover have "inv_begin n (steps0 (1, [], Oc \<up> n) tcopy_begin stp)"
-    apply(rule_tac inv_begin_steps)
-    using h by(simp_all add: inv_begin.simps)
-  ultimately show
-    "\<exists>stp. is_final (steps0 (1, l, r) tcopy_begin stp) \<and> 
-    inv_begin0 n holds_for steps (1, l, r) (tcopy_begin, 0) stp"
-    using h
-    apply(rule_tac x = stp in exI)
-    apply(case_tac "(steps0 (1, [], Oc \<up> n) tcopy_begin stp)", simp add: inv_begin.simps)
-    done
-qed
+  shows "0 < n \<Longrightarrow> {inv_begin1 n} tcopy_begin {inv_begin0 n}"
+using begin_partial_correctness begin_halts by blast
 
 declare tm_comp.simps [simp del] 
 declare adjust.simps[simp del] 
@@ -206,7 +178,6 @@
 declare step.simps[simp del]
 declare steps.simps[simp del]
 
-
 (* tcopy_loop *)
 
 fun 
@@ -217,8 +188,8 @@
   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, 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_loop1_loop n (l, r) = (\<exists> i j. i + j + 1 = n \<and> (l, r) = (Oc\<up>i, Oc#Oc#Bk\<up>j @ Oc\<up>j) \<and> j > 0)"
+| "inv_loop1_exit n (l, r) = (0 < n \<and> (l, r) = ([], Bk#Oc#Bk\<up>n @ Oc\<up>n))"
 | "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, r) = (Oc\<up>k@Bk\<up>j@Oc\<up>i, Oc\<up>t))"
 | "inv_loop5_exit x (l, r) = 
@@ -237,15 +208,15 @@
   inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
   inv_loop6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 where
-  "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, 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, 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, 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))"
+  "inv_loop0 n (l, r) =  (0 < n \<and> (l, r) = ([Bk], Oc # Bk\<up>n @ Oc\<up>n))"
+| "inv_loop1 n (l, r) = (inv_loop1_loop n (l, r) \<or> inv_loop1_exit n (l, r))"
+| "inv_loop2 n (l, r) = (\<exists> i j any. i + j = n \<and> n > 0 \<and> i > 0 \<and> j > 0 \<and> (l, r) = (Oc\<up>i, any#Bk\<up>j@Oc\<up>j))"
+| "inv_loop3 n (l, r) = 
+     (\<exists> i j k t. i + j = n \<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 n (l, r) = 
+     (\<exists> i j k t. i + j = n \<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 n (l, r) = (inv_loop5_loop n (l, r) \<or> inv_loop5_exit n (l, r))"
+| "inv_loop6 n (l, r) = (inv_loop6_loop n (l, r) \<or> inv_loop6_exit n (l, r))"
 
 fun inv_loop :: "nat \<Rightarrow> config \<Rightarrow> bool"
   where
@@ -464,8 +435,7 @@
 done
 
 lemma inv_loop_steps:
-  "\<lbrakk>inv_loop x cf; x > 0\<rbrakk>
-  \<Longrightarrow> inv_loop x (steps cf (tcopy_loop, 0) stp)"
+  "\<lbrakk>inv_loop x cf; x > 0\<rbrakk> \<Longrightarrow> inv_loop x (steps cf (tcopy_loop, 0) stp)"
 apply(induct stp, simp add: steps.simps, simp)
 apply(erule_tac inv_loop_step, simp)
 done
@@ -489,14 +459,21 @@
                           else if s = 6 then length l
                           else 0)"
 
-definition loop_LE :: "(config \<times> config) set"
+definition measure_loop :: "(config \<times> config) set"
   where
-   "loop_LE = measures [loop_stage, loop_state, loop_step]"
+   "measure_loop = measures [loop_stage, loop_state, loop_step]"
 
-lemma wf_loop_le: "wf loop_LE"
-unfolding loop_LE_def
+lemma wf_measure_loop: "wf measure_loop"
+unfolding measure_loop_def
 by (auto)
 
+lemma measure_loop_induct [case_names Step]: 
+  "\<lbrakk>\<And>n. \<not> P (f n) \<Longrightarrow> (f (Suc n), (f n)) \<in> measure_loop\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
+using wf_measure_loop
+by (metis wf_iff_no_infinite_down_chain)
+
+
+
 lemma [simp]: "inv_loop2 x ([], b) = False"
 by (auto simp: inv_loop2.simps)
 
@@ -509,6 +486,7 @@
 lemma [simp]: "inv_loop4 x ([], b) = False"
 by (auto simp: inv_loop4.simps)
 
+
 lemma [elim]: 
   "\<lbrakk>inv_loop4 x (l', []); l' \<noteq> []; x > 0;
   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ [Oc])) \<noteq> 
@@ -581,7 +559,6 @@
 apply(case_tac l', auto)
 done
 
-
 lemma[elim]: 
   "\<lbrakk>inv_loop6 x (l', Oc # list); l' \<noteq> []; 0 < x;
   length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list))
@@ -592,63 +569,58 @@
 apply(auto simp: inv_loop6.simps)
 done
 
-lemma loop_halt: 
-  "\<lbrakk>x > 0; inv_loop x (Suc 0, l, r)\<rbrakk> \<Longrightarrow> 
-      \<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_loop, 0) stp)"
-proof(rule_tac LE = loop_LE in halt_lemma)
-  show "wf loop_LE" by(intro wf_loop_le)
-next
-  assume h: "0 < x"  and g: "inv_loop x (Suc 0, l, r)"
-  show "\<forall>n. \<not> is_final (steps (Suc 0, l, r) (tcopy_loop, 0) n) \<longrightarrow> 
-        (steps (Suc 0, l, r) (tcopy_loop, 0) (Suc n), steps (Suc 0, l, r) (tcopy_loop, 0) n) \<in> loop_LE"
-  proof(rule_tac allI, rule_tac impI)
-    fix n
-    assume a: "\<not> is_final (steps (Suc 0, l, r) (tcopy_loop, 0) n)"
-    obtain s' l' r' where d: "(steps (Suc 0, l, r) (tcopy_loop, 0) n) = (s', l', r')"
-      by(case_tac "(steps (Suc 0, l, r) (tcopy_loop, 0) n)", auto)
-    hence "inv_loop x (s', l', r') \<and> s' \<noteq> 0"
-      using h g
-      apply(drule_tac stp = n in inv_loop_steps, auto)
-      using a
-      apply(simp)
-      done
-    hence "(step(s', l', r') (tcopy_loop, 0), s', l', r') \<in> loop_LE"
-      using h 
-      apply(case_tac r', case_tac [2] a)
-      apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral loop_LE_def split: if_splits)
-      done
-    thus "(steps (Suc 0, l, r) (tcopy_loop, 0) (Suc n), 
-          steps (Suc 0, l, r) (tcopy_loop, 0) n) \<in> loop_LE"
-      using d
-      apply(simp add: step_red)
-      done
-  qed
+lemma loop_halts: 
+  assumes h: "n > 0" "inv_loop n (1, l, r)"
+  shows "\<exists> stp. is_final (steps0 (1, l, r) tcopy_loop stp)"
+proof (induct rule: measure_loop_induct) 
+  case (Step stp)
+  have "\<not> is_final (steps0 (1, l, r) tcopy_loop stp)" by fact
+  moreover
+  have "inv_loop n (steps0 (1, l, r) tcopy_loop stp)"
+    by (rule_tac inv_loop_steps) (simp_all only: h)
+  moreover
+  obtain s l' r' where eq: "(steps0 (1, l, r) tcopy_loop stp) = (s, l', r')"
+    by (metis measure_begin_state.cases)
+  ultimately 
+  have "(step0 (s, l', r') tcopy_loop, s, l', r') \<in> measure_loop"
+    using h(1)
+    apply(case_tac r')
+    apply(case_tac [2] a)
+    apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral measure_loop_def split: if_splits)
+    done
+  then 
+  show "(steps0 (1, l, r) tcopy_loop (Suc stp), steps0 (1, l, r) tcopy_loop stp) \<in> measure_loop"
+    using eq by (simp only: step_red)
 qed
 
 lemma loop_correct:
-  "x > 0 \<Longrightarrow> {inv_loop1 x} tcopy_loop {inv_loop0 x}"
+  shows "0 < n \<Longrightarrow> {inv_loop1 n} tcopy_loop {inv_loop0 n}"
+  using assms
 proof(rule_tac Hoare_haltI)
   fix l r
-  assume h: "0 < x"
-    "inv_loop1 x (l, r)"
-  hence "\<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_loop, 0) stp)"
-    apply(rule_tac loop_halt, simp_all add: inv_loop.simps)
+  assume h: "0 < n" "inv_loop1 n (l, r)"
+  then obtain stp where k: "is_final (steps0 (1, l, r) tcopy_loop stp)" 
+    using loop_halts
+    apply(simp add: inv_loop.simps)
+    apply(blast)
     done
-  then obtain stp where "is_final (steps (Suc 0, l, r) (tcopy_loop, 0) stp)" ..
-  moreover have "inv_loop x (steps (Suc 0, l, r) (tcopy_loop, 0) stp)"
-    apply(rule_tac inv_loop_steps)
-    using h by(simp_all add: inv_loop.simps)
+  moreover
+  have "inv_loop n (steps0 (1, l, r) tcopy_loop stp)"
+    using h 
+    by (rule_tac inv_loop_steps) (simp_all add: inv_loop.simps)
   ultimately show
-    "\<exists>n. is_final (steps (1, l, r) (tcopy_loop, 0) n) \<and> 
-    inv_loop0 x holds_for steps (1, l, r) (tcopy_loop, 0) n"    
-    using h
+    "\<exists>stp. is_final (steps0 (1, l, r) tcopy_loop stp) \<and> 
+    inv_loop0 n holds_for steps0 (1, l, r) tcopy_loop stp"
+    using h(1) 
     apply(rule_tac x = stp in exI)
-    apply(case_tac "(steps (Suc 0, l, r) (tcopy_loop, 0) stp)", 
-      simp add: inv_begin.simps inv_loop.simps)
+    apply(case_tac "(steps0 (1, l, r) tcopy_loop stp)")
+    apply(simp add: inv_loop.simps)
     done
 qed
 
 
+
+
 (* tcopy_end *)
 
 fun
@@ -664,27 +636,26 @@
   inv_end1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
   inv_end2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
   inv_end3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-  inv_end4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
- 
+  inv_end4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and 
   inv_end5 :: "nat \<Rightarrow> tape \<Rightarrow> bool" 
 where
-  "inv_end0 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc\<up>x @ Bk # Oc\<up>x)"
-| "inv_end1 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x)"
-| "inv_end2 x (l, r) = (\<exists> i j. i + j = Suc x \<and> x > 0 \<and> l = Oc\<up>i @ [Bk] \<and> r = Bk\<up>j @ Oc\<up>x)"
-| "inv_end3 x (l, r) =
-     (\<exists> i j. x > 0 \<and> i + j = x \<and> l = Oc\<up>i @ [Bk] \<and> r = Oc # Bk\<up>j@ Oc\<up>x)"
-| "inv_end4 x (l, r) = (\<exists> any. x > 0 \<and> l = Oc\<up>x @ [Bk] \<and> r = any#Oc\<up>x)"
-| "inv_end5 x (l, r) = (inv_end5_loop x (l, r) \<or> inv_end5_exit x (l, r))"
+  "inv_end0 n (l, r) = (n > 0 \<and> (l, r) = ([Bk], Oc\<up>n @ Bk # Oc\<up>n))"
+| "inv_end1 n (l, r) = (n > 0 \<and> (l, r) = ([Bk], Oc # Bk\<up>n @ Oc\<up>n))"
+| "inv_end2 n (l, r) = (\<exists> i j. i + j = Suc n \<and> n > 0 \<and> l = Oc\<up>i @ [Bk] \<and> r = Bk\<up>j @ Oc\<up>n)"
+| "inv_end3 n (l, r) =
+     (\<exists> i j. n > 0 \<and> i + j = n \<and> l = Oc\<up>i @ [Bk] \<and> r = Oc # Bk\<up>j@ Oc\<up>n)"
+| "inv_end4 n (l, r) = (\<exists> any. n > 0 \<and> l = Oc\<up>n @ [Bk] \<and> r = any#Oc\<up>n)"
+| "inv_end5 n (l, r) = (inv_end5_loop n (l, r) \<or> inv_end5_exit n (l, r))"
 
 fun 
   inv_end :: "nat \<Rightarrow> config \<Rightarrow> bool"
 where
-  "inv_end x (s, l, r) = (if s = 0 then inv_end0 x (l, r)
-                          else if s = 1 then inv_end1 x (l, r)
-                          else if s = 2 then inv_end2 x (l, r)
-                          else if s = 3 then inv_end3 x (l, r)
-                          else if s = 4 then inv_end4 x (l, r)
-                          else if s = 5 then inv_end5 x (l, r)
+  "inv_end n (s, l, r) = (if s = 0 then inv_end0 n (l, r)
+                          else if s = 1 then inv_end1 n (l, r)
+                          else if s = 2 then inv_end2 n (l, r)
+                          else if s = 3 then inv_end3 n (l, r)
+                          else if s = 4 then inv_end4 n (l, r)
+                          else if s = 5 then inv_end5 n (l, r)
                           else False)"
 
 declare inv_end.simps[simp del] inv_end1.simps[simp del]
@@ -843,6 +814,10 @@
 lemma [simp]: "inv_end5 x ([], Oc # list) = False"
 by (auto simp: inv_end5.simps inv_end5_loop.simps)
 
+lemma halt_lemma: 
+  "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
+by (metis wf_iff_no_infinite_down_chain)
+
 lemma end_halt: 
   "\<lbrakk>x > 0; inv_end x (Suc 0, l, r)\<rbrakk> \<Longrightarrow> 
       \<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_end, 0) stp)"
@@ -875,20 +850,20 @@
 qed
 
 lemma end_correct:
-  "x > 0 \<Longrightarrow> {inv_end1 x} tcopy_end {inv_end0 x}"
+  "n > 0 \<Longrightarrow> {inv_end1 n} tcopy_end {inv_end0 n}"
 proof(rule_tac Hoare_haltI)
   fix l r
-  assume h: "0 < x"
-    "inv_end1 x (l, r)"
+  assume h: "0 < n"
+    "inv_end1 n (l, r)"
   then have "\<exists> stp. is_final (steps0 (1, l, r) tcopy_end stp)"
     by (simp add: end_halt inv_end.simps)
   then obtain stp where "is_final (steps0 (1, l, r) tcopy_end stp)" ..
-  moreover have "inv_end x (steps0 (1, l, r) tcopy_end stp)"
+  moreover have "inv_end n (steps0 (1, l, r) tcopy_end stp)"
     apply(rule_tac inv_end_steps)
     using h by(simp_all add: inv_end.simps)
   ultimately show
-    "\<exists>n. is_final (steps (1, l, r) (tcopy_end, 0) n) \<and> 
-    inv_end0 x holds_for steps (1, l, r) (tcopy_end, 0) n"        
+    "\<exists>stp. is_final (steps (1, l, r) (tcopy_end, 0) stp) \<and> 
+    inv_end0 n holds_for steps (1, l, r) (tcopy_end, 0) stp"        
     using h
     apply(rule_tac x = stp in exI)
     apply(case_tac "(steps0 (1, l, r) tcopy_end stp)") 
@@ -940,10 +915,10 @@
     by (rule_tac Hoare_plus_halt) (auto)
 qed
 
-abbreviation
-  "pre_tcopy n \<equiv> \<lambda>tp. tp = ([]::cell list, <[n::nat]>)"
-abbreviation
-  "post_tcopy n \<equiv> \<lambda>tp. tp= ([Bk], <[n, n::nat]>)"
+abbreviation (input)
+  "pre_tcopy n \<equiv> \<lambda>tp. tp = ([]::cell list, <(n::nat)>)"
+abbreviation (input)
+  "post_tcopy n \<equiv> \<lambda>tp. tp= ([Bk], <(n, n::nat)>)"
 
 lemma tcopy_correct:
   shows "{pre_tcopy n} tcopy {post_tcopy n}"
@@ -955,7 +930,7 @@
     by (auto simp add: tape_of_nl_abv tape_of_nat_abv)
   moreover
   have "inv_end0 (Suc n) = post_tcopy n" 
-    by (auto simp add: inv_end0.simps tape_of_nat_abv tape_of_nl_abv)
+    by (auto simp add: inv_end0.simps tape_of_nat_abv tape_of_nat_pair)
   ultimately
   show "{pre_tcopy n} tcopy {post_tcopy n}" 
     by simp
@@ -1044,30 +1019,30 @@
   The following two assumptions specifies that @{text "H"} does solve the Halting problem.
   *}
   and h_case: 
-  "\<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> 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 ns. \<not> haltP M ns \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <code M#ns>))} H {(\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <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 *)
-abbreviation
-  "pre_H_inv M n \<equiv> \<lambda>tp. tp = ([Bk], <[code M, n]>)"
+abbreviation (input)
+  "pre_H_inv M ns \<equiv> \<lambda>tp. tp = ([Bk], <(code M, ns::nat list)>)"
 
-abbreviation
+abbreviation (input)
   "post_H_halt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"
 
-abbreviation
+abbreviation (input)
   "post_H_unhalt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"
 
 
 lemma H_halt_inv:
-  assumes "\<not> haltP M [n]" 
-  shows "{pre_H_inv M n} H {post_H_halt_inv}"
+  assumes "\<not> haltP M ns" 
+  shows "{pre_H_inv M ns} H {post_H_halt_inv}"
 using assms nh_case by auto
 
 lemma H_unhalt_inv:
-  assumes "haltP M [n]" 
-  shows "{pre_H_inv M n} H {post_H_unhalt_inv}"
+  assumes "haltP M ns" 
+  shows "{pre_H_inv M ns} H {post_H_unhalt_inv}"
 using assms h_case by auto
    
 (* TM that produces the contradiction and its code *)
@@ -1083,8 +1058,8 @@
   shows "False"
 proof -
   (* invariants *)
-  def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <[code_tcontra]>)"
-  def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <[code_tcontra, code_tcontra]>)"
+  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>k. tp = (Bk \<up> k, <1::nat>)"
 
   (*
@@ -1106,8 +1081,9 @@
   next
     case B_halt (* of H *)
     show "{P2} H {P3}"
-      unfolding P2_def P3_def
-      by (rule H_halt_inv[OF assms])
+      unfolding P2_def P3_def 
+      using H_halt_inv[OF assms]
+      by (simp add: tape_of_nat_pair tape_of_nl_abv)
   qed (simp)
 
   (* {P3} dither {P3} *)
@@ -1123,10 +1099,10 @@
     unfolding P1_def P3_def
     unfolding haltP_def
     unfolding Hoare_halt_def 
-    apply(auto)
+    apply(auto)    
     apply(drule_tac x = n in spec)
-    apply(case_tac "steps0 (Suc 0, [], <[code tcontra]>) tcontra n")
-    apply(auto)
+    apply(case_tac "steps0 (Suc 0, [], <code tcontra>) tcontra n")
+    apply(auto simp add: tape_of_nl_abv)
     done
 qed
 
@@ -1136,8 +1112,8 @@
   shows "False"
 proof - 
   (* invariants *)
-  def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <[code_tcontra]>)"
-  def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <[code_tcontra, code_tcontra]>)"
+  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>k. tp = (Bk \<up> k, <0::nat>)"
 
   (*
@@ -1159,8 +1135,8 @@
   next
     case B_halt (* of H *)
     then show "{P2} H {Q3}"
-      unfolding P2_def Q3_def
-      by (rule H_unhalt_inv[OF assms])
+      unfolding P2_def Q3_def using H_unhalt_inv[OF assms]
+      by(simp add: tape_of_nat_pair tape_of_nl_abv)
   qed (simp)
 
   (* {P3} dither loops *)
@@ -1176,7 +1152,7 @@
     unfolding P1_def
     unfolding haltP_def
     unfolding Hoare_halt_def Hoare_unhalt_def
-    by auto
+    by (auto simp add: tape_of_nl_abv)
 qed
       
 text {*