diff -r a8785fa80278 -r 2f765afc1f7e thys/uncomputable.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/uncomputable.thy	Wed Jan 16 10:12:43 2013 +0000
@@ -0,0 +1,1451 @@
+(* Title: Turing machine's definition and its charater
+   Author: XuJian <xujian817@hotmail.com>
+   Maintainer: Xujian
+*)
+
+header {* Undeciablity of the {\em Halting problem} *}
+
+theory uncomputable
+imports Main turing_basic
+begin
+
+text {*
+  The {\em Copying} TM, which duplicates its input. 
+*}
+
+definition tcopy_init :: "instr list"
+where
+"tcopy_init \<equiv> [(W0, 0), (R, 2), (R, 3), (R, 2),
+               (W1, 3), (L, 4), (L, 4), (L, 0)]"
+
+fun inv_init1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+   "inv_init1 x (l, r) = (l = [] \<and> r = Oc\<up>x )"
+
+fun inv_init2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where 
+  "inv_init2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc\<up>i \<and> r = Oc\<up>j)"
+
+fun inv_init3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "inv_init3 x (l, r) = (x > 0 \<and> l = Bk # Oc\<up>x \<and> tl r = [])"
+
+fun inv_init4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "inv_init4 x (l, r) = (x > 0 \<and> ((l = Oc\<up>x \<and> r = [Bk, Oc]) \<or> (l = Oc\<up>(x - 1) \<and> r = [Oc, Bk, Oc])))"
+
+fun inv_init0 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "inv_init0 x (l, r) = ((x >  Suc 0 \<and> l = Oc\<up>(x - 2) \<and> r = [Oc, Oc, Bk, Oc]) \<or>   
+                        (x = 1 \<and> l = [] \<and> r = [Bk, Oc, Bk, Oc]))"
+
+fun inv_init :: "nat \<Rightarrow> config \<Rightarrow> bool"
+  where
+  "inv_init x (s, l, r) = (
+         if s = 0 then inv_init0 x (l, r) 
+         else if s = Suc 0 then inv_init1 x (l, r)
+         else if s = 2 then inv_init2 x (l, r)
+         else if s = 3 then inv_init3 x (l, r)
+         else if s = 4 then inv_init4 x (l, r)
+         else False)"
+
+declare inv_init.simps[simp del]
+
+lemma numeral_4_eq_4: "4 = Suc 3"
+by arith
+
+lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> 
+  \<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia"
+apply(rule_tac x = "Suc i" in exI, simp)
+done
+
+lemma inv_init_step: 
+  "\<lbrakk>inv_init x cf; x > 0\<rbrakk>
+ \<Longrightarrow> inv_init x (step cf (tcopy_init, 0))"
+apply(case_tac cf)
+apply(auto simp: inv_init.simps step.simps tcopy_init_def numeral_2_eq_2 
+  numeral_3_eq_3 numeral_4_eq_4 split: if_splits)
+apply(case_tac "hd c", auto simp: inv_init.simps)
+apply(case_tac c, simp_all)
+done
+
+lemma inv_init_steps: 
+  "\<lbrakk>inv_init x (s, l, r); x > 0\<rbrakk>
+ \<Longrightarrow> inv_init x (steps (s, l, r) (tcopy_init, 0) stp)"
+apply(induct stp, simp add: steps.simps)
+apply(auto simp: step_red)
+apply(rule_tac inv_init_step, simp_all)
+done
+
+fun init_state :: "config \<Rightarrow> nat"
+  where
+  "init_state (s, l, r) = (if s = 0 then 0
+                             else 5 - s)"
+
+fun init_step :: "config \<Rightarrow> nat"
+  where
+  "init_step (s, l, r) = (if s = 2 then length r
+                            else if s = 3 then if r = [] \<or> r = [Bk] then Suc 0 else 0
+                            else if s = 4 then length l
+                            else 0)"
+
+fun init_measure :: "config \<Rightarrow> nat \<times> nat"
+  where
+  "init_measure c = 
+   (init_state c, init_step c)"
+
+
+definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set"
+  where
+  "lex_pair \<equiv> less_than <*lex*> less_than"
+
+definition init_LE :: "(config \<times> config) set"
+  where
+   "init_LE \<equiv> (inv_image lex_pair init_measure)"
+
+lemma [simp]: "\<lbrakk>tl r = []; r \<noteq> []; r \<noteq> [Bk]\<rbrakk> \<Longrightarrow> r = [Oc]"
+apply(case_tac r, auto, case_tac a, auto)
+done
+
+lemma wf_init_le: "wf init_LE"
+by(auto intro:wf_inv_image simp:init_LE_def lex_pair_def)
+
+lemma init_halt: 
+  "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_init, 0) stp)"
+proof(rule_tac LE = init_LE in halt_lemma)
+  show "wf init_LE" by(simp add: wf_init_le)
+next
+  assume h: "0 < x"
+  show "\<forall>n. \<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) \<longrightarrow>
+        (steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) (Suc n), 
+            steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) \<in> init_LE"
+  proof(rule_tac allI, rule_tac impI)
+    fix n
+    assume a: "\<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n)"
+    have b: "inv_init x (steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n)"
+      apply(rule_tac inv_init_steps)
+      apply(simp_all add: inv_init.simps h)
+      done 
+    obtain s l r where c: "(steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) = (s, l, r)"
+      apply(case_tac "steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n", auto)
+      done
+    moreover hence "inv_init x (s, l, r)" 
+      using c b by simp
+    ultimately show "(steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) (Suc n), 
+      steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) \<in> init_LE"
+      using a 
+    proof(simp)
+      assume "inv_init x (s, l, r)" "0 < s"
+      thus "(step (s, l, r) (tcopy_init, 0), s, l, r) \<in> init_LE"
+        apply(auto simp: inv_init.simps init_LE_def lex_pair_def step.simps tcopy_init_def numeral_2_eq_2
+          numeral_3_eq_3 numeral_4_eq_4 split: if_splits)
+        apply(case_tac r, auto, case_tac a, auto)
+        done
+    qed
+  qed
+qed
+    
+lemma init_correct: 
+  "x > 0 \<Longrightarrow> 
+  {inv_init1 x} (tcopy_init, 0) {inv_init0 x}"
+proof(rule_tac HoareI)
+  fix l r
+  assume h: "0 < x"
+    "inv_init1 x (l, r)"
+  hence "\<exists> stp. is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_init, 0) stp)"
+    by(erule_tac init_halt)    
+  then obtain stp where "is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_init, 0) stp)" ..
+  moreover have "inv_init x (steps (Suc 0, [], Oc\<up>x) (tcopy_init, 0) stp)"
+    apply(rule_tac inv_init_steps)
+    using h by(simp_all add: inv_init.simps)
+  ultimately show
+    "\<exists>n. is_final (steps (1, l, r) (tcopy_init, 0) n) \<and> 
+    inv_init0 x holds_for steps (1, l, r) (tcopy_init, 0) n"
+    using h
+    apply(rule_tac x = stp in exI)
+    apply(case_tac "(steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) stp)", simp add: inv_init.simps)
+    done
+qed
+
+definition tcopy_loop :: "instr list"
+where
+"tcopy_loop \<equiv> [(R, 0), (R, 2),  (R, 3), (W0, 2),
+                (R, 3), (R, 4), (W1, 5), (R, 4),
+                 (L, 6), (L, 5), (L, 6), (L, 1)]"
+
+fun inv_loop1_loop :: "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)"
+
+fun inv_loop1_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "inv_loop1_exit x (l, r) = 
+      (l = [] \<and> r = Bk # Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0 )"
+
+fun inv_loop1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "inv_loop1 x (l, r) = (inv_loop1_loop x (l, r) \<or> inv_loop1_exit x (l, r))"
+
+fun inv_loop2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "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)"
+
+fun inv_loop3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "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)"
+
+fun inv_loop4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "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)"
+
+fun inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+where
+  "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)"
+
+fun inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "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)"
+
+fun inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "inv_loop5 x (l, r) = (inv_loop5_loop x (l, r) \<or> 
+                         inv_loop5_exit x (l, r))"
+
+fun inv_loop6_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "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)"
+
+fun inv_loop6_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "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)"
+
+fun inv_loop6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "inv_loop6 x (l, r) = (inv_loop6_loop x (l, r) \<or> inv_loop6_exit x (l, r))"
+
+fun inv_loop0 :: "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 )"
+
+fun inv_loop :: "nat \<Rightarrow> config \<Rightarrow> bool"
+  where
+  "inv_loop x (s, l, r) = 
+         (if s = 0 then inv_loop0 x (l, r)
+          else if s = 1 then inv_loop1 x (l, r)
+          else if s = 2 then inv_loop2 x (l, r)
+          else if s = 3 then inv_loop3 x (l, r)
+          else if s = 4 then inv_loop4 x (l, r)
+          else if s = 5 then inv_loop5 x (l, r)
+          else if s = 6 then inv_loop6 x (l, r)
+          else False)"
+       
+declare inv_loop.simps[simp del] inv_loop1.simps[simp del]
+        inv_loop2.simps[simp del] inv_loop3.simps[simp del] 
+        inv_loop4.simps[simp del] inv_loop5.simps[simp del] 
+        inv_loop6.simps[simp del]
+lemma [elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR"
+apply(case_tac t, auto)
+done
+
+lemma numeral_5_eq_5: "5 = Suc 4" by arith
+
+lemma numeral_6_eq_6: "6 = Suc (Suc 4)" by arith
+
+lemma [simp]: "inv_loop1 x (b, []) = False"
+by(simp add: inv_loop1.simps)
+
+lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
+apply(auto simp: inv_loop2.simps inv_loop3.simps)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
+apply(auto simp: inv_loop3.simps)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop5 x (b, [Oc])"
+apply(auto simp: inv_loop4.simps inv_loop5.simps)
+apply(rule_tac [!] x = i in exI, 
+      rule_tac [!] x  = "Suc j" in exI, simp_all)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], [])\<rbrakk> \<Longrightarrow> RR"
+apply(auto simp: inv_loop4.simps inv_loop5.simps)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, []); b \<noteq> []\<rbrakk> \<Longrightarrow> RR"
+apply(auto simp: inv_loop4.simps inv_loop5.simps)
+done
+
+lemma [elim]: "inv_loop6 x ([], []) \<Longrightarrow> RR"
+apply(auto simp: inv_loop6.simps)
+done
+
+thm inv_loop6_exit.simps
+lemma [elim]: "inv_loop6 x (b, []) \<Longrightarrow> RR" 
+apply(auto simp: inv_loop6.simps)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> b = []"
+apply(auto simp: inv_loop1.simps)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> list = Oc # Bk \<up> x @ Oc \<up> x"
+apply(auto simp: inv_loop1.simps)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
+apply(auto simp: inv_loop2.simps inv_loop3.simps)
+apply(rule_tac [!] x = i  in exI, rule_tac [!] x = j in exI, simp_all)
+done
+
+lemma [elim]: "Bk # list = Oc \<up> j \<Longrightarrow> RR"
+apply(case_tac j, simp_all)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
+apply(auto simp: inv_loop3.simps)
+apply(rule_tac [!] x = i in exI, 
+      rule_tac [!] x = j in exI, simp_all)
+apply(case_tac [!] t, auto)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop5 x (b, Oc # list)"
+apply(auto simp: inv_loop4.simps inv_loop5.simps)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
+apply(auto simp: inv_loop6.simps inv_loop5.simps)
+done
+
+lemma [simp]: "inv_loop5_loop x (b, Bk # list) = False"
+apply(auto simp: inv_loop5_loop.simps)
+done
+
+lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
+apply(auto simp: inv_loop6.simps)
+done
+
+declare inv_loop5_loop.simps[simp del]  inv_loop5_exit.simps[simp del]
+       inv_loop6_loop.simps[simp del]  inv_loop6_exit.simps[simp del]
+
+lemma [elim]:"\<lbrakk>0 < x; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk> 
+          \<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"
+apply(simp only: inv_loop5_exit.simps inv_loop6_loop.simps )
+apply(erule_tac exE)+
+apply(rule_tac x = i in exI, 
+      rule_tac x = j in exI,
+      rule_tac x = "j - Suc (Suc 0)" in exI, 
+      rule_tac x = "Suc 0" in exI, auto)
+apply(case_tac [!] j, simp_all)
+apply(case_tac [!] nat, simp_all)
+done
+
+lemma [simp]: "inv_loop6_loop x (b, Oc # Bk # list) = False"
+apply(auto simp: inv_loop6_loop.simps)
+done
+
+lemma [elim]: "\<lbrakk>x > 0; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow> 
+  inv_loop6_exit x (tl b, Oc # Bk # list)"
+apply(simp only: inv_loop5_exit.simps inv_loop6_exit.simps)
+apply(erule_tac exE)+
+apply(rule_tac x = "x - 1" in exI, rule_tac x = 1 in exI, simp)
+apply(case_tac j, auto)
+apply(case_tac [!] nat, auto)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"
+apply(simp add: inv_loop5.simps inv_loop6.simps)
+apply(case_tac "hd b", simp_all, auto)
+done
+
+lemma  [simp]: "inv_loop6 x ([], Bk # xs) = False"
+apply(simp add: inv_loop6.simps inv_loop6_loop.simps
+                inv_loop6_exit.simps)
+apply(auto)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
+apply(simp)
+done
+
+lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
+apply(simp add: inv_loop6_exit.simps)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk>
+              \<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"
+apply(simp only: inv_loop6_loop.simps)
+apply(erule_tac exE)+
+apply(rule_tac x = i in exI, rule_tac x = j in exI, 
+      rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, auto)
+apply(case_tac [!] k, auto)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> 
+        \<Longrightarrow> inv_loop6_exit x (tl b, Oc # Bk # list)"
+apply(simp only: inv_loop6_loop.simps inv_loop6_exit.simps)
+apply(erule_tac exE)+
+apply(rule_tac x = "i - 1" in exI, rule_tac x = j in exI, auto)
+apply(case_tac [!] k, auto)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"
+apply(simp add: inv_loop6.simps)
+apply(case_tac "hd b", simp_all, auto)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (Oc # b, list)"
+apply(auto simp: inv_loop1.simps inv_loop2.simps)
+apply(rule_tac x = "Suc i" in exI, auto)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (b, Bk # list)"
+apply(auto simp: inv_loop2.simps)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
+apply(auto simp: inv_loop3.simps inv_loop4.simps)
+apply(rule_tac [!] x = i in exI, auto)
+apply(rule_tac [!] x = "Suc 0" in exI, rule_tac [!] x = "j - 1" in exI, auto)
+apply(case_tac [!] t, auto)
+apply(case_tac [!] j, auto)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
+apply(auto simp: inv_loop4.simps)
+apply(rule_tac [!] x = "i" in exI, auto)
+apply(rule_tac [!] x = "Suc k" in exI, rule_tac [!] x = "t - 1" in exI, auto)
+apply(case_tac [!] t, simp_all)
+done
+
+lemma [simp]: "inv_loop5 x ([], list) = False"
+apply(auto simp: inv_loop5.simps inv_loop5_exit.simps inv_loop5_loop.simps)
+done
+
+lemma [simp]: "inv_loop5_exit x (b, Oc # list) = False"
+apply(auto simp: inv_loop5_exit.simps)
+done
+
+lemma [elim]: " \<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk>
+  \<Longrightarrow> inv_loop5_exit x (tl b, Bk # Oc # list)"
+apply(simp only: inv_loop5_loop.simps inv_loop5_exit.simps)
+apply(erule_tac exE)+
+apply(rule_tac x = i in exI, auto)
+apply(case_tac [!] k, auto)
+done
+
+lemma [elim]: "\<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk> 
+           \<Longrightarrow> inv_loop5_loop x (tl b, Oc # Oc # list)"
+apply(simp only:  inv_loop5_loop.simps)
+apply(erule_tac exE)+
+apply(rule_tac x = i in exI, rule_tac x = j in exI)
+apply(rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, auto)
+apply(case_tac [!] k, auto)
+done
+
+lemma [elim]: "\<lbrakk>inv_loop5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow> 
+  inv_loop5 x (tl b, hd b # Oc # list)"
+apply(simp add: inv_loop5.simps)
+apply(case_tac "hd b", simp_all, auto)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Oc # list)\<rbrakk> \<Longrightarrow> 
+               inv_loop1 x ([], Bk # Oc # list)"
+apply(auto simp: inv_loop6.simps inv_loop1.simps 
+  inv_loop6_loop.simps inv_loop6_exit.simps)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Oc # list); b \<noteq> []\<rbrakk> 
+           \<Longrightarrow> inv_loop1 x (tl b, hd b # Oc # list)"
+apply(auto simp: inv_loop6.simps inv_loop1.simps 
+  inv_loop6_loop.simps inv_loop6_exit.simps)
+done
+
+lemma inv_loop_step: 
+  "\<lbrakk>inv_loop x cf; x > 0\<rbrakk>
+ \<Longrightarrow> inv_loop x (step cf (tcopy_loop, 0))"
+apply(case_tac cf, case_tac c, case_tac [2] aa)
+apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral_2_eq_2  
+  numeral_3_eq_3 numeral_4_eq_4 numeral_5_eq_5 numeral_6_eq_6 split: if_splits)
+done
+
+lemma inv_loop_steps:
+  "\<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
+
+fun loop_stage :: "config \<Rightarrow> nat"
+  where
+  "loop_stage (s, l, r) = (if s = 0 then 0
+                           else (Suc (length (takeWhile (\<lambda>a. a = Oc) (rev l @ r)))))"
+
+fun loop_state :: "config \<Rightarrow> nat"
+  where
+  "loop_state (s, l, r) = (if s = 2 \<and> hd r = Oc then 0
+                           else if s = 1 then 1
+                           else 10 - s)"
+
+fun loop_step :: "config \<Rightarrow> nat"
+  where
+  "loop_step (s, l, r) = (if s = 3 then length r
+                          else if s = 4 then length r
+                          else if s = 5 then length l 
+                          else if s = 6 then length l
+                          else 0)"
+
+definition lex_triple :: 
+ "((nat \<times> (nat \<times> nat)) \<times> (nat \<times> (nat \<times> nat))) set"
+  where
+  "lex_triple \<equiv> less_than <*lex*> lex_pair"
+
+lemma wf_lex_triple: "wf lex_triple"
+  by (auto intro:wf_lex_prod simp:lex_triple_def lex_pair_def)
+
+fun loop_measure :: "config \<Rightarrow> nat \<times> nat \<times> nat"
+  where
+  "loop_measure c = 
+   (loop_stage c, loop_state c, loop_step c)"
+
+definition loop_LE :: "(config \<times> config) set"
+  where
+   "loop_LE \<equiv> (inv_image lex_triple loop_measure)"
+
+lemma wf_loop_le: "wf loop_LE"
+by(auto intro:wf_inv_image simp: loop_LE_def wf_lex_triple)
+
+lemma [simp]: "inv_loop2 x ([], b) = False"
+apply(auto simp: inv_loop2.simps)
+done
+
+lemma  [simp]: "inv_loop2 x (l', []) = False"
+apply(auto simp: inv_loop2.simps)
+done
+
+lemma [simp]: "inv_loop3 x (b, []) = False"
+apply(auto simp: inv_loop3.simps)
+done
+
+lemma [simp]: "inv_loop4 x ([], b) = False"
+apply(auto simp: inv_loop4.simps)
+done
+
+lemma [elim]: 
+  "\<lbrakk>inv_loop4 x (l', []); l' \<noteq> []; x > 0;
+  length (takeWhile (\<lambda>a. a = Oc) (rev l' @ [Oc])) \<noteq> 
+  length (takeWhile (\<lambda>a. a = Oc) (rev l'))\<rbrakk>
+  \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ [Oc])) < length (takeWhile (\<lambda>a. a = Oc) (rev l'))"
+apply(auto simp: inv_loop4.simps)
+apply(case_tac [!] j, simp_all add: List.takeWhile_tail)
+done
+
+
+lemma [elim]: 
+  "\<lbrakk>inv_loop4 x (l', Bk # list); l' \<noteq> []; 0 < x;
+   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) \<noteq> 
+    length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
+    \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) < 
+    length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
+apply(auto simp: inv_loop4.simps)
+done
+
+lemma takeWhile_replicate_append: 
+  "P a \<Longrightarrow> takeWhile P (a\<up>x @ ys) = a\<up>x @ takeWhile P ys"
+apply(induct x, auto)
+done
+
+lemma takeWhile_replicate: 
+  "P a \<Longrightarrow> takeWhile P (a\<up>x) = a\<up>x"
+by(induct x, auto)
+
+lemma [elim]: 
+   "\<lbrakk>inv_loop5 x (l', Bk # list); l' \<noteq> []; 0 < x;
+   length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq>
+   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
+   \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) < 
+   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
+apply(auto simp: inv_loop5.simps inv_loop5_exit.simps)
+apply(case_tac [!] j, simp_all)
+apply(case_tac [!] "nat", simp_all)
+apply(case_tac  nata, simp_all add: List.takeWhile_tail)
+apply(simp add: takeWhile_replicate_append takeWhile_replicate)
+apply(case_tac  nata, simp_all add: List.takeWhile_tail)
+done
+
+lemma [elim]: "\<lbrakk>inv_loop1 x (l', Oc # list)\<rbrakk> \<Longrightarrow> hd list = Oc"
+apply(auto simp: inv_loop1.simps)
+done
+
+lemma [elim]: 
+  "\<lbrakk>inv_loop6 x (l', Bk # list); l' \<noteq> []; 0 < x;
+  length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq> 
+  length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
+  \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) < 
+  length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
+apply(auto simp: inv_loop6.simps)
+apply(case_tac l', simp_all)
+done
+
+lemma [elim]:
+  "\<lbrakk>inv_loop2 x (l', Oc # list); l' \<noteq> []; 0 < x\<rbrakk> \<Longrightarrow> 
+  length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list)) <
+  length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"
+apply(auto simp: inv_loop2.simps)
+apply(simp_all add: takeWhile_tail takeWhile_replicate_append
+                takeWhile_replicate)
+done
+
+lemma [elim]: 
+  "\<lbrakk>inv_loop5 x (l', Oc # list); l' \<noteq> []; 0 < x;
+  length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) \<noteq> 
+  length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))\<rbrakk>
+  \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) < 
+  length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"
+apply(auto simp: inv_loop5.simps)
+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))
+  \<noteq> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))\<rbrakk>
+  \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) < 
+      length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"
+apply(case_tac l')
+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_2_eq_2 numeral_3_eq_3 numeral_4_eq_4
+                       numeral_5_eq_5 numeral_6_eq_6 loop_LE_def lex_triple_def lex_pair_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
+qed
+
+lemma loop_correct:
+  "x > 0 \<Longrightarrow> 
+      {inv_loop1 x} (tcopy_loop, 0) {inv_loop0 x}"
+proof(rule_tac HoareI)
+  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)
+    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)
+  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
+    apply(rule_tac x = stp in exI)
+    apply(case_tac "(steps (Suc 0, l, r) (tcopy_loop, 0) stp)", 
+      simp add: inv_init.simps inv_loop.simps)
+    done
+qed
+  
+definition tcopy_end :: "instr list"
+  where
+  "tcopy_end \<equiv> [(L, 0), (R, 2), (W1, 3), (L, 4),
+                (R, 2), (R, 2), (L, 5), (W0, 4),
+                (R, 0), (L, 5)]"
+
+fun inv_end1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "inv_end1 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x)"
+
+fun inv_end2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "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>)"
+
+fun inv_end3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "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 )"
+
+fun inv_end4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "inv_end4 x (l, r) = (\<exists> any. x > 0 \<and> l = Oc\<up>x @ [Bk] \<and> r = any#Oc\<up>x)"
+
+fun inv_end5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "inv_end5_loop x (l, r) = 
+         (\<exists> i j. i + j = x \<and> x > 0 \<and> j > 0 \<and> l = Oc\<up>i @ [Bk] \<and> r = Oc\<up>j @ Bk # Oc\<up>x)"
+
+fun inv_end5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "inv_end5_exit x (l, r) = (x > 0 \<and> l = [] \<and> r = Bk # Oc\<up>x @ Bk # Oc\<up>x)"
+
+fun inv_end5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+  where
+  "inv_end5 x (l, r) = (inv_end5_loop x (l, r) \<or> inv_end5_exit x (l, r))"
+
+fun inv_end0 :: "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)"
+
+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)
+                          else False)"
+
+declare inv_end.simps[simp del] inv_end1.simps[simp del]
+        inv_end0.simps[simp del] inv_end2.simps[simp del]
+        inv_end3.simps[simp del] inv_end4.simps[simp del]
+        inv_end5.simps[simp del]
+
+lemma [simp]:  "inv_end1 x (b, []) = False"
+apply(auto simp: inv_end1.simps)
+done
+
+lemma [simp]: "inv_end2 x (b, []) = False"
+apply(auto simp: inv_end2.simps)
+done
+
+lemma [simp]: "inv_end3 x (b, []) = False"
+apply(auto simp: inv_end3.simps)
+done
+
+thm inv_end4.simps
+lemma [simp]: "inv_end4 x (b, []) = False"
+apply(auto simp: inv_end4.simps)
+done
+
+lemma [simp]: "inv_end5 x (b, []) = False"
+apply(auto simp: inv_end5.simps)
+done
+
+lemma [simp]: "inv_end1 x ([], list) = False"
+apply(auto simp: inv_end1.simps)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Bk # list); b \<noteq> []\<rbrakk>
+  \<Longrightarrow> inv_end0 x (tl b, hd b # Bk # list)"
+apply(auto simp: inv_end1.simps inv_end0.simps)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_end2 x (b, Bk # list)\<rbrakk> 
+  \<Longrightarrow> inv_end3 x (b, Oc # list)"
+apply(auto simp: inv_end2.simps inv_end3.simps)
+apply(rule_tac x = "j - 1" in exI)
+apply(case_tac j, simp_all)
+apply(case_tac x, simp_all)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Bk # b, list)"
+apply(auto simp: inv_end2.simps inv_end3.simps)
+done
+  
+lemma [elim]: "\<lbrakk>0 < x; inv_end4 x ([], Bk # list)\<rbrakk> \<Longrightarrow> 
+  inv_end5 x ([], Bk # Bk # list)"
+apply(auto simp: inv_end4.simps inv_end5.simps)
+done
+ 
+lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> 
+  inv_end5 x (tl b, hd b # Bk # list)"
+apply(auto simp: inv_end4.simps inv_end5.simps)
+apply(rule_tac x = 1 in exI, simp)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_end5 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end0 x (Bk # b, list)"
+apply(auto simp: inv_end5.simps inv_end0.simps)
+apply(case_tac [!] j, simp_all)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
+apply(auto simp: inv_end1.simps inv_end2.simps)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_end2 x ([], Oc # list)\<rbrakk> \<Longrightarrow>
+               inv_end4 x ([], Bk # Oc # list)"
+apply(auto simp: inv_end2.simps inv_end4.simps)
+done
+
+lemma [elim]:  "\<lbrakk>0 < x; inv_end2 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
+  inv_end4 x (tl b, hd b # Oc # list)"
+apply(auto simp: inv_end2.simps inv_end4.simps)
+apply(case_tac [!] j, simp_all)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
+apply(auto simp: inv_end2.simps inv_end3.simps)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end4 x (b, Bk # list)"
+apply(auto simp: inv_end2.simps inv_end4.simps)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_end5 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_end5 x ([], Bk # Oc # list)"
+apply(auto simp: inv_end2.simps inv_end5.simps)
+done
+
+declare inv_end5_loop.simps[simp del]
+        inv_end5_exit.simps[simp del]
+
+lemma [simp]: "inv_end5_exit x (b, Oc # list) = False"
+apply(auto simp: inv_end5_exit.simps)
+done
+
+lemma [simp]: "inv_end5_loop x (tl b, Bk # Oc # list) = False"
+apply(auto simp: inv_end5_loop.simps)
+apply(case_tac [!] j, simp_all)
+done
+
+lemma [elim]:
+  "\<lbrakk>0 < x; inv_end5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk> \<Longrightarrow>
+  inv_end5_exit x (tl b, Bk # Oc # list)"
+apply(auto simp: inv_end5_loop.simps inv_end5_exit.simps)
+apply(case_tac [!] i, simp_all)
+done
+
+lemma [elim]: 
+  "\<lbrakk>0 < x; inv_end5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow>
+  inv_end5_loop x (tl b, Oc # Oc # list)"
+apply(simp only: inv_end5_loop.simps inv_end5_exit.simps)
+apply(erule_tac exE)+
+apply(rule_tac x = "i - 1" in exI, 
+      rule_tac x = "Suc j" in exI, auto)
+apply(case_tac [!] i, simp_all)
+done
+
+lemma [elim]: "\<lbrakk>0 < x; inv_end5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow> 
+  inv_end5 x (tl b, hd b # Oc # list)"
+apply(simp add: inv_end2.simps inv_end5.simps)
+apply(case_tac "hd b", simp_all, auto)
+done
+
+lemma inv_end_step:
+  "\<lbrakk>x > 0;
+ inv_end x cf\<rbrakk>
+ \<Longrightarrow> inv_end x (step cf (tcopy_end, 0))"
+apply(case_tac cf, case_tac c, case_tac [2] aa)
+apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral_2_eq_2 
+  numeral_3_eq_3 numeral_4_eq_4 numeral_5_eq_5 split: if_splits)
+done
+
+lemma inv_end_steps:
+  "\<lbrakk>x > 0; inv_end x cf\<rbrakk>
+\<Longrightarrow> inv_end x (steps cf (tcopy_end, 0) stp)"
+apply(induct stp, simp add:steps.simps, simp)
+apply(erule_tac inv_end_step, simp)
+done
+
+fun end_state :: "config \<Rightarrow> nat"
+  where
+  "end_state (s, l, r) = 
+       (if s = 0 then 0
+        else if s = 1 then 5
+        else if s = 2 \<or> s = 3 then 4
+        else if s = 4 then 3 
+        else if s = 5 then 2
+        else 0)"
+
+fun end_stage :: "config \<Rightarrow> nat"
+  where
+  "end_stage (s, l, r) = 
+          (if s = 2 \<or> s = 3 then (length r)
+           else 0)"
+
+fun end_step :: "config \<Rightarrow> nat"
+  where
+  "end_step (s, l, r) = 
+         (if s = 4 then (if hd r = Oc then 1 else 0)
+          else if s = 5 then length l
+          else if s = 2 then 1
+          else if s = 3 then 0
+          else 0)"
+
+fun end_measure :: "config \<Rightarrow> nat \<times> nat \<times> nat"
+  where
+  "end_measure c = 
+   (end_state c, end_stage c, end_step c)"
+
+definition end_LE :: "(config \<times> config) set"
+  where
+   "end_LE \<equiv> (inv_image lex_triple end_measure)"
+
+lemma wf_end_le: "wf end_LE"
+by(auto intro:wf_inv_image simp: end_LE_def wf_lex_triple)
+
+lemma [simp]: "inv_end5 x ([], Oc # list) = False"
+apply(auto simp: inv_end5.simps inv_end5_loop.simps)
+done
+
+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)"
+proof(rule_tac LE = end_LE in halt_lemma)
+  show "wf end_LE" by(intro wf_end_le)
+next
+  assume great: "0 < x"
+    and inv_start: "inv_end x (Suc 0, l, r)"
+  show "\<forall>n. \<not> is_final (steps (Suc 0, l, r) (tcopy_end, 0) n) \<longrightarrow> 
+    (steps (Suc 0, l, r) (tcopy_end, 0) (Suc n), steps (Suc 0, l, r) (tcopy_end, 0) n) \<in> end_LE"
+  proof(rule_tac allI, rule_tac impI)
+    fix n
+    assume notfinal: "\<not> is_final (steps (Suc 0, l, r) (tcopy_end, 0) n)"
+    obtain s' l' r' where d: "steps (Suc 0, l, r) (tcopy_end, 0) n = (s', l', r')"
+      apply(case_tac "steps (Suc 0, l, r) (tcopy_end, 0) n", auto)
+      done
+    hence "inv_end x (s', l', r') \<and> s' \<noteq> 0"
+      using great inv_start notfinal
+      apply(drule_tac stp = n in inv_end_steps, auto)
+      done
+    hence "(step (s', l', r') (tcopy_end, 0), s', l', r') \<in> end_LE"
+      apply(case_tac r', case_tac [2] a)
+      apply(auto simp: inv_end.simps step.simps tcopy_end_def 
+                       numeral_2_eq_2 numeral_3_eq_3 numeral_4_eq_4 
+                       numeral_5_eq_5 numeral_6_eq_6 end_LE_def lex_triple_def lex_pair_def split: if_splits)
+      done
+    thus "(steps (Suc 0, l, r) (tcopy_end, 0) (Suc n), 
+      steps (Suc 0, l, r) (tcopy_end, 0) n) \<in> end_LE"
+      using d
+      by simp
+  qed
+qed
+
+lemma end_correct:
+  "x > 0 \<Longrightarrow> 
+      {inv_end1 x} (tcopy_end, 0) {inv_end0 x}"
+proof(rule_tac HoareI)
+  fix l r
+  assume h: "0 < x"
+    "inv_end1 x (l, r)"
+  hence "\<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_end, 0) stp)"
+    apply(rule_tac end_halt, simp_all add: inv_end.simps)
+    done
+  then obtain stp where "is_final (steps (Suc 0, l, r) (tcopy_end, 0) stp)" ..
+  moreover have "inv_end x (steps (Suc 0, l, r) (tcopy_end, 0) 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"        
+    using h
+    apply(rule_tac x = stp in exI)
+    apply(case_tac "(steps (Suc 0, l, r) (tcopy_end, 0) stp)", 
+      simp add:  inv_end.simps)
+    done
+qed
+
+definition tcopy :: "instr list"
+  where
+  "tcopy = ((tcopy_init |+| tcopy_loop) |+| tcopy_end)"
+
+lemma [intro]: "tm_wf (tcopy_init, 0)"
+by(auto simp: tm_wf.simps tcopy_init_def)
+
+lemma [intro]: "tm_wf (tcopy_loop, 0)"
+by(auto simp: tm_wf.simps tcopy_loop_def)
+
+lemma [intro]: "tm_wf (tcopy_end, 0)"
+by(auto simp: tm_wf.simps tcopy_end_def)
+
+lemma [intro]: "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)"
+apply(auto simp: tm_wf.simps shift.simps adjust.simps length_comp
+                 tm_comp.simps)
+done
+
+lemma tcopy_correct1: 
+  "\<lbrakk>x > 0\<rbrakk> \<Longrightarrow> {inv_init1 x} (tcopy, 0) {inv_end0 x}"
+proof(simp add: tcopy_def, rule_tac Hoare_plus_halt)
+  show "inv_loop0 x \<mapsto> inv_end1 x"
+    by(auto simp: inv_end1.simps inv_loop1.simps assert_imp_def)
+next
+  show "tm_wf (tcopy_init |+| tcopy_loop, 0)" by auto
+next
+  show "tm_wf (tcopy_end, 0)" by auto
+next
+  assume "0 < x"
+  thus "{inv_init1 x} (tcopy_init |+| tcopy_loop, 0) {inv_loop0 x}"
+  proof(rule_tac Hoare_plus_halt)
+    show "inv_init0 x \<mapsto> inv_loop1 x"
+      apply(auto simp: inv_init0.simps inv_loop1.simps assert_imp_def)
+      apply(rule_tac x = "Suc 0" in exI, auto)
+      done
+  next
+    show "tm_wf (tcopy_init, 0)" by auto
+  next
+    show "tm_wf (tcopy_loop, 0)" by auto
+  next
+    assume "0 < x"
+    thus "{inv_init1 x} (tcopy_init, 0) {inv_init0 x}"
+      by(erule_tac init_correct)
+  next
+    assume "0 < x"
+    thus "{inv_loop1 x} (tcopy_loop, 0) {inv_loop0 x}"
+      by(erule_tac loop_correct)
+  qed
+next
+  assume "0 < x"
+  thus "{inv_end1 x} (tcopy_end, 0) {inv_end0 x}"
+    by(erule_tac end_correct)
+qed
+
+section {*
+  The {\em Dithering} Turing Machine 
+*}
+
+text {*
+  The {\em Dithering} TM, when the input is @{text "1"}, it will loop forever, otherwise, it will
+  terminate.
+*}
+definition dither :: "instr list"
+  where
+  "dither \<equiv> [(W0, 1), (R, 2), (L, 1), (L, 0)] "
+
+lemma dither_halt_rs: 
+  "\<exists> stp. steps (Suc 0, Bk\<up>m, [Oc, Oc]) (dither, 0) stp = 
+                                 (0, Bk\<up>m, [Oc, Oc])"
+apply(rule_tac x = "Suc (Suc (Suc 0))" in exI)
+apply(simp add: dither_def steps.simps 
+                step.simps fetch.simps numeral_2_eq_2)
+done
+
+lemma dither_unhalt_state: 
+  "(steps (Suc 0, Bk\<up>m, [Oc]) (dither, 0) stp = 
+   (Suc 0, Bk\<up>m, [Oc])) \<or> 
+   (steps (Suc 0, Bk\<up>m, [Oc]) (dither, 0) stp = (2, Oc # Bk\<up>m, []))"
+  apply(induct stp, simp add: steps.simps)
+  apply(simp add: step_red, auto)
+  apply(auto simp: step.simps fetch.simps dither_def numeral_2_eq_2)
+  done
+
+lemma dither_unhalt_rs: 
+  "\<not> is_final (steps (Suc 0, Bk\<up>m, [Oc]) (dither,0) stp)"
+using dither_unhalt_state[of m stp]
+apply(auto)
+done
+
+section {*
+  The final diagnal arguments to show the undecidability of Halting problem.
+*}
+
+text {*
+  @{text "haltP tp x"} means TM @{text "tp"} terminates on input @{text "x"}
+  and the final configuration is standard.
+*}
+
+
+fun tape_of_nat_list :: "nat list \<Rightarrow> cell list" ("< _ >" [0] 100)
+  where 
+  "tape_of_nat_list [] = []" |
+  "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)"
+
+definition haltP :: "tprog \<Rightarrow> nat list \<Rightarrow> bool"
+  where
+  "haltP t lm = (\<exists>n a b c. steps (Suc 0, [], <lm>) t n = (0, Bk\<up>a,  Oc\<up>b @ Bk\<up>c))"
+
+lemma [intro]: "tm_wf (tcopy, 0)"
+by(auto simp: tcopy_def)
+
+lemma [intro]: "tm_wf (dither, 0)"
+apply(auto simp: tm_wf.simps dither_def)
+done
+
+text {*
+  The following lemma shows the meaning of @{text "tinres"} with respect to 
+  one step execution.
+  *}
+lemma tinres_step: 
+  "\<lbrakk>tinres l l'; step (ss, l, r) (t, 0) = (sa, la, ra); 
+                 step (ss, l', r) (t, 0) = (sb, lb, rb)\<rbrakk>
+    \<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb"
+apply(case_tac ss, case_tac [!]r, case_tac [!] "a::cell")
+apply(auto simp: step.simps fetch.simps
+        split: if_splits )
+apply(case_tac [!] "t ! (2 * nat)", 
+     auto simp: tinres_def split: if_splits)
+apply(case_tac [1-8] a, auto split: if_splits)
+apply(case_tac [!] "t ! (2 * nat)", 
+     auto simp: tinres_def split: if_splits)
+apply(case_tac [1-4] a, auto split: if_splits)
+apply(case_tac [!] "t ! Suc (2 * nat)", 
+     auto simp: if_splits)
+apply(case_tac [!] aa, auto split: if_splits)
+done
+
+text {*
+  The following lemma shows the meaning of @{text "tinres"} with respect to 
+  many step execution.
+  *}
+
+lemma tinres_steps: 
+  "\<lbrakk>tinres l l'; steps (ss, l, r) (t, 0) stp = (sa, la, ra); 
+                 steps (ss, l', r) (t, 0) stp = (sb, lb, rb)\<rbrakk>
+    \<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb"
+apply(induct stp arbitrary: sa la ra sb lb rb, simp add: steps.simps)
+apply(simp add: step_red)
+apply(case_tac "(steps (ss, l, r) (t, 0) stp)")
+apply(case_tac "(steps (ss, l', r) (t, 0) stp)")
+proof -
+  fix stp sa la ra sb lb rb a b c aa ba ca
+  assume ind: "\<And>sa la ra sb lb rb. \<lbrakk>steps (ss, l, r) (t, 0) stp = (sa, (la::cell list), ra); 
+          steps (ss, l', r) (t, 0) stp = (sb, lb, rb)\<rbrakk> \<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb"
+  and h: " tinres l l'" "step (steps (ss, l, r) (t, 0) stp) (t, 0) = (sa, la, ra)"
+         "step (steps (ss, l', r) (t, 0) stp) (t, 0) = (sb, lb, rb)" "steps (ss, l, r) (t, 0) stp = (a, b, c)" 
+         "steps (ss, l', r) (t, 0) stp = (aa, ba, ca)"
+  have "tinres b ba \<and> c = ca \<and> a = aa"
+    apply(rule_tac ind, simp_all add: h)
+    done
+  thus "tinres la lb \<and> ra = rb \<and> sa = sb"
+    apply(rule_tac l = b and l' = ba and r = c  and ss = a   
+            and t = t in tinres_step)
+    using h
+    apply(simp, simp, simp)
+    done
+qed
+
+lemma length_eq: "xs = ys \<Longrightarrow> length xs = length ys"
+by auto
+
+lemma tinres_ex1: "tinres (Bk \<up> nb) b \<Longrightarrow> \<exists>nb. b = Bk \<up> nb"
+apply(auto simp: tinres_def replicate_add[THEN sym])
+apply(case_tac "nb \<ge> n")
+apply(subgoal_tac "\<exists> d. nb = d + n", auto simp: replicate_add)
+apply arith
+apply(drule_tac length_eq, simp)
+done
+
+lemma Hoare_weak:
+  "\<lbrakk>{P} (p, off) {Q}; P'\<mapsto>P; Q\<mapsto>Q'\<rbrakk> \<Longrightarrow> {P'} (p, off) {Q'}"
+using Hoare_def
+proof(auto simp: assert_imp_def)
+  fix l r
+  assume 
+    ho1: "\<forall>l r. P (l, r) \<longrightarrow> (\<exists>n. is_final (steps (Suc 0, l, r) (p, off) n) 
+    \<and> Q holds_for steps (Suc 0, l, r) (p, off) n)"
+    and imp1: "\<forall>l r. P' (l, r) \<longrightarrow> P (l, r)"
+    and imp2: "\<forall>l r. Q (l, r) \<longrightarrow> Q' (l, r)"
+    and cond: "P' (l, r)"
+    and ho2: "\<And>P a b Q. {P} (a, b) {Q} \<equiv> \<forall>l r. P (l, r) \<longrightarrow>
+    (\<exists>n. is_final (steps (Suc 0, l, r) (a, b) n) \<and> Q holds_for steps (Suc 0, l, r) (a, b) n)"
+  have "P (l, r)"
+    using cond imp1 by auto
+  hence "(\<exists>n. is_final (steps (Suc 0, l, r) (p, off) n) 
+    \<and> Q holds_for steps (Suc 0, l, r) (p, off) n)"
+    using ho1 by auto
+  from this obtain n where "is_final (steps (Suc 0, l, r) (p, off) n) 
+    \<and> Q holds_for steps (Suc 0, l, r) (p, off) n" ..
+  thus "\<exists>n. is_final (steps (Suc 0, l, r) (p, off) n) \<and> 
+    Q' holds_for steps (Suc 0, l, r) (p, off) n"
+    apply(rule_tac x = n in exI, auto)
+    apply(case_tac "steps (Suc 0, l, r) (p, off) n", simp)
+    using imp2
+    by simp
+qed
+
+text {*
+  The following locale specifies that TM @{text "H"} can be used to solve 
+  the {\em Halting Problem} and @{text "False"} is going to be derived 
+  under this locale. Therefore, the undecidability of {\em Halting Problem}
+  is established. 
+*}
+
+locale uncomputable = 
+  -- {* The coding function of TM, interestingly, the detailed definition of this 
+  funciton @{text "code"} does not affect the final result. *}
+  fixes code :: "instr list \<Rightarrow> nat" 
+  -- {* 
+  The TM @{text "H"} is the one which is assummed being able to solve the Halting problem.
+  *}
+  and H :: "instr list"
+  assumes h_wf[intro]: "tm_wf (H, 0)"
+  -- {*
+  The following two assumptions specifies that @{text "H"} does solve the Halting problem.
+  *}
+  and h_case: 
+  "\<And> M n. \<lbrakk>(haltP (M, 0) lm)\<rbrakk> \<Longrightarrow> 
+             \<exists> na nb. (steps (Suc 0, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc]))"
+  and nh_case: 
+  "\<And> M n. \<lbrakk>(\<not> haltP (M, 0) lm)\<rbrakk> \<Longrightarrow>
+             \<exists> na nb. (steps (Suc 0, [],  <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
+begin
+
+lemma h_newcase: 
+  "\<And> M n. haltP (M, 0) lm \<Longrightarrow> 
+  \<exists> na nb. (steps (Suc 0, Bk\<up>x , <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc]))"
+proof -
+  fix M n
+  assume "haltP (M, 0) lm"
+  hence "\<exists> na nb. (steps (Suc 0, [], <code M # lm>) (H, 0) na
+            = (0, Bk\<up>nb, [Oc]))"
+    apply(erule_tac h_case)
+    done
+  from this obtain na nb where 
+    cond1:"(steps (Suc 0, [], <code M # lm>) (H, 0) na
+            = (0, Bk\<up>nb, [Oc]))" by blast
+  thus "\<exists> na nb. (steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc]))"
+  proof(rule_tac x = na in exI, case_tac "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na", simp)
+    fix a b c
+    assume cond2: "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
+    have "tinres (Bk\<up>nb) b \<and> [Oc] = c \<and> 0 = a"
+    proof(rule_tac tinres_steps)
+      show "tinres [] (Bk\<up>x)"
+        apply(simp add: tinres_def)
+        apply(auto)
+        done
+    next
+      show "(steps (Suc 0, [], <code M # lm>) (H, 0) na
+            = (0, Bk\<up>nb, [Oc]))"
+        by(simp add: cond1)
+    next
+      show "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
+        by(simp add: cond2)
+    qed
+    thus "a = 0 \<and> (\<exists>nb. b = (Bk\<up>nb)) \<and> c = [Oc]"
+      by(auto elim: tinres_ex1)
+  qed
+qed
+
+lemma nh_newcase: "\<And> M n. \<lbrakk>\<not> (haltP (M, 0) lm)\<rbrakk> \<Longrightarrow> 
+             \<exists> na nb. (steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
+proof -
+  fix M n
+  assume "\<not> haltP (M, 0) lm"
+  hence "\<exists> na nb. (steps (Suc 0, [], <code M # lm>) (H, 0) na
+            = (0, Bk\<up>nb, [Oc, Oc]))"
+    apply(erule_tac nh_case)
+    done
+  from this obtain na nb where 
+    cond1: "(steps (Suc 0, [], <code M # lm>) (H, 0) na
+            = (0, Bk\<up>nb, [Oc, Oc]))" by blast
+  thus "\<exists> na nb. (steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
+  proof(rule_tac x = na in exI, case_tac "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na", simp)
+    fix a b c
+    assume cond2: "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
+    have "tinres (Bk\<up>nb) b \<and> [Oc, Oc] = c \<and> 0 = a"
+    proof(rule_tac tinres_steps)
+      show "tinres [] (Bk\<up>x)"
+        apply(auto simp: tinres_def)
+        done
+    next
+      show "(steps (Suc 0, [], <code M # lm>) (H, 0) na
+            = (0, Bk\<up>nb, [Oc, Oc]))"
+        by(simp add: cond1)
+    next
+      show "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
+        by(simp add: cond2)
+    qed
+    thus "a = 0 \<and> (\<exists>nb. b =  Bk\<up>nb) \<and> c = [Oc, Oc]"
+      by(auto elim: tinres_ex1)
+  qed
+qed
+   
+(*  
+lemma haltP_weaking: 
+  "haltP (tcontra H) (code (tcontra H)) \<Longrightarrow> 
+    \<exists>stp. isS0 (steps (Suc 0, [], Oc\<^bsup>code (tcontra H)\<^esup>) 
+          ((tcopy |+| H) |+| dither) stp)"
+  apply(simp add: haltP_def, auto)
+  apply(rule_tac x = n in exI, simp add: isS0_def tcontra_def)
+  done
+*)
+
+definition tcontra :: "instr list \<Rightarrow> instr list"
+  where
+  "tcontra h \<equiv> ((tcopy |+| h) |+| dither)"
+
+declare replicate_Suc[simp del]
+
+lemma uh_h: "\<not> haltP (tcontra H, 0) [code (tcontra H)]
+       \<Longrightarrow> 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, Oc]"
+  let ?P3 = ?Q2
+  let ?Q3 = ?P3
+  assume h: "\<not> haltP (?tcontr, 0) [code ?tcontr]"
+  have "{?P1} (?tcontr, 0) {?Q3}"
+  proof(rule_tac Hoare_plus_halt, auto)
+    show "?Q2 \<mapsto> ?P3"
+      apply(simp add: assert_imp_def)
+      done
+  next
+    show "{?P1} (tcopy|+|H, 0) {?Q2}"
+    proof(rule_tac Hoare_plus_halt, auto)
+      show "?Q1 \<mapsto> ?P2"
+        apply(simp add: assert_imp_def)
+        done
+    next
+      show "{?P1} (tcopy, 0) {?Q1}"
+      proof -
+        have g: "{inv_init1 ?cn} (tcopy, 0) {inv_end0 ?cn}"
+          by(rule_tac tcopy_correct1, simp)
+        thus "?thesis"
+        proof(rule_tac Hoare_weak)           
+          show "{inv_init1 ?cn} (tcopy, 0)
+            {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, 0) {?Q2}"
+        using Hoare_def nh_newcase[of ?tcontr "[code ?tcontr]" 1] h
+        apply(auto)
+        apply(rule_tac x = na in exI)
+        apply(simp add: replicate_Suc)
+        done
+    qed
+  next
+    show "{?P3}(dither, 0){?Q3}"
+      using Hoare_def
+    proof(auto)
+      fix nd
+      show "\<exists>n. is_final (steps (Suc 0, Bk \<up> nd, [Oc, Oc]) (dither, 0) n) \<and>
+        (\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc])
+        holds_for steps (Suc 0, Bk \<up> nd, [Oc, Oc]) (dither, 0) n"
+        using dither_halt_rs[of nd]
+        apply(auto)
+        apply(rule_tac x = stp in exI, simp)
+        done
+    qed
+  qed    
+  thus "False"
+    using h
+    apply(auto simp: haltP_def Hoare_def)
+    apply(erule_tac x = n in allE)
+    apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n")
+    apply(simp, auto)
+    apply(erule_tac x = 2 in allE, erule_tac x = 0 in allE)
+    apply(simp add: numeral_2_eq_2 replicate_Suc)
+    done
+qed
+  
+
+lemma h_uh: "haltP (tcontra H, 0) [code (tcontra H)]
+       \<Longrightarrow> \<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
+  assume h: "haltP (?tcontr, 0) [code ?tcontr]"
+  have "{?P1} (?tcontr, 0)"
+  proof(rule_tac Hoare_plus_unhalt, auto)
+    show "?Q2 \<mapsto> ?P3"
+      apply(simp add: assert_imp_def)
+      done
+  next
+    show "{?P1} (tcopy|+|H, 0) {?Q2}"
+    proof(rule_tac Hoare_plus_halt, auto)
+      show "?Q1 \<mapsto> ?P2"
+        apply(simp add: assert_imp_def)
+        done
+    next
+      show "{?P1} (tcopy, 0) {?Q1}"
+      proof -
+        have g: "{inv_init1 ?cn} (tcopy, 0) {inv_end0 ?cn}"
+          by(rule_tac tcopy_correct1, simp)
+        thus "?thesis"
+        proof(rule_tac Hoare_weak)           
+          show "{inv_init1 ?cn} (tcopy, 0)
+            {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, 0) {?Q2}"
+        using Hoare_def h_newcase[of ?tcontr "[code ?tcontr]" 1] h
+        apply(auto)
+        apply(rule_tac x = na in exI)
+        apply(simp add: replicate_Suc)
+        done
+    qed
+  next
+    show "{?P3}(dither, 0)"
+      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> True"
+    using h
+    apply(auto simp: haltP_def Hoare_unhalt_def)
+    apply(erule_tac x = n in allE)
+    apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n", simp)
+    done
+qed
+      
+text {*
+  @{text "False"} is finally derived.
+*}
+
+lemma false: "False"
+using uh_h h_uh
+by auto
+end
+
+end
+