diff -r a63c3f8d7234 -r 67063c5365e1 thys/uncomputable.thy
--- a/thys/uncomputable.thy	Thu Feb 07 06:39:06 2013 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1178 +0,0 @@
-(* 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_hoare
-begin
-
-lemma numeral:
-  shows "1 = Suc 0"
-  and "2 = Suc 1"
-  and "3 = Suc 2"
-  and "4 = Suc 3" 
-  and "5 = Suc 4" 
-  and "6 = Suc 5" 
-  and "7 = Suc 6"
-  and "8 = Suc 7" 
-  and "9 = Suc 8" 
-  and "10 = Suc 9" 
-  by arith+
-
-text {*
-  The {\em Copying} TM, which duplicates its input. 
-*}
-
-definition 
-  tcopy_begin :: "instr list"
-where
-  "tcopy_begin \<equiv> [(W0, 0), (R, 2), (R, 3), (R, 2),
-                 (W1, 3), (L, 4), (L, 4), (L, 0)]"
-
-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)]"
-
-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)]"
-
-definition 
-  tcopy :: "instr list"
-where
-  "tcopy \<equiv> (tcopy_begin |+| tcopy_loop) |+| tcopy_end"
-
-
-(* tcopy_begin *)
-
-fun 
-  inv_begin0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-  inv_begin1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-  inv_begin2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-  inv_begin3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-  inv_begin4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-where
-  "inv_begin0 n (l, r) = ((n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc])) \<or>   
-                          (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc])))"
-| "inv_begin1 n (l, r) = ((l, r) = ([], Oc \<up> n))"
-| "inv_begin2 n (l, r) = (\<exists> i j. i > 0 \<and> i + j = n \<and> (l, r) = (Oc \<up> i, Oc \<up> j))"
-| "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) = 
-        (if s = 0 then inv_begin0 n tp else
-         if s = 1 then inv_begin1 n tp else
-         if s = 2 then inv_begin2 n tp else
-         if s = 3 then inv_begin3 n tp else
-         if s = 4 then inv_begin4 n tp 
-         else False)"
-
-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"
-by (rule_tac x = "Suc i" in exI, simp)
-
-lemma inv_begin_step: 
-  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)
-apply(auto simp: numeral split: if_splits)
-apply(case_tac "hd c")
-apply(auto)
-apply(case_tac c)
-apply(simp_all)
-done
-
-lemma inv_begin_steps: 
-  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)
-apply(rule_tac inv_begin_step)
-apply(simp_all add: assms)
-done
-
-lemma begin_partial_correctness:
-  assumes "is_final (steps0 (1, [], Oc \<up> n) tcopy_begin stp)"
-  shows "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)"
-  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
-  "measure_begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)"
-
-fun measure_begin_step :: "config \<Rightarrow> nat"
-  where
-  "measure_begin_step (s, l, r) = 
-        (if s = 2 then length r else
-         if s = 3 then (if r = [] \<or> r = [Bk] then 1 else 0) else
-         if s = 4 then length l 
-         else 0)"
-
-definition
-  "measure_begin = measures [measure_begin_state, measure_begin_step]"
-
-lemma wf_measure_begin:
-  shows "wf measure_begin" 
-unfolding measure_begin_def 
-by auto
-
-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_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: 
-  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] 
-declare shift.simps[simp del]
-declare tm_wf.simps[simp del]
-declare step.simps[simp del]
-declare steps.simps[simp del]
-
-(* tcopy_loop *)
-
-fun 
-  inv_loop1_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-  inv_loop1_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-  inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-  inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-  inv_loop6_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-  inv_loop6_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-where
-  "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) = 
-     (\<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, 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, r) = (Oc\<up>i, Oc#Bk\<up>j @ Oc\<up>j))"
-
-fun 
-  inv_loop0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-  inv_loop1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-  inv_loop2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-  inv_loop3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-  inv_loop4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-  inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-  inv_loop6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-where
-  "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
-  "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"
-by (case_tac t, auto)
-
-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, [])"
-by (auto simp: inv_loop2.simps inv_loop3.simps)
-
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
-by (auto simp: inv_loop3.simps)
-
-
-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"
-by (auto simp: inv_loop4.simps inv_loop5.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, []); b \<noteq> []\<rbrakk> \<Longrightarrow> RR"
-by (auto simp: inv_loop4.simps inv_loop5.simps)
-
-lemma [elim]: "inv_loop6 x ([], []) \<Longrightarrow> RR"
-by (auto simp: inv_loop6.simps)
-
-lemma [elim]: "inv_loop6 x (b, []) \<Longrightarrow> RR" 
-by (auto simp: inv_loop6.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> b = []"
-by (auto simp: inv_loop1.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> list = Oc # Bk \<up> x @ Oc \<up> x"
-by (auto simp: inv_loop1.simps)
-
-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"
-by (case_tac j, simp_all)
-
-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)"
-by (auto simp: inv_loop4.simps inv_loop5.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
-by (auto simp: inv_loop6.simps inv_loop5.simps)
-
-lemma [simp]: "inv_loop5_loop x (b, Bk # list) = False"
-by (auto simp: inv_loop5.simps)
-
-lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
-by (auto simp: inv_loop6.simps)
-
-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"
-by (auto simp: inv_loop6_loop.simps)
-
-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)"
-by (simp)
-
-lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
-by (simp add: inv_loop6_exit.simps)
-
-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)"
-by (auto simp: inv_loop2.simps)
-
-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"
-by (auto simp: inv_loop5.simps inv_loop5_exit.simps inv_loop5_loop.simps)
-
-lemma [simp]: "inv_loop5_exit x (b, Oc # list) = False"
-by (auto simp: inv_loop5_exit.simps)
-
-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 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 measure_loop :: "(config \<times> config) set"
-  where
-   "measure_loop = measures [loop_stage, loop_state, loop_step]"
-
-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)
-
-lemma  [simp]: "inv_loop2 x (l', []) = False"
-by (auto simp: inv_loop2.simps)
-
-lemma [simp]: "inv_loop3 x (b, []) = False"
-by (auto simp: inv_loop3.simps)
-
-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> 
-  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))"
-by (auto simp: inv_loop4.simps)
-
-lemma takeWhile_replicate_append: 
-  "P a \<Longrightarrow> takeWhile P (a\<up>x @ ys) = a\<up>x @ takeWhile P ys"
-by (induct x, auto)
-
-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"
-by (auto simp: inv_loop1.simps)
-
-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_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:
-  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 < 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
-  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>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 "(steps0 (1, l, r) tcopy_loop stp)")
-    apply(simp add: inv_loop.simps)
-    done
-qed
-
-
-
-
-(* tcopy_end *)
-
-fun
-  inv_end5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
-  inv_end5_exit :: "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)"
-| "inv_end5_exit x (l, r) = (x > 0 \<and> l = [] \<and> r = Bk # Oc\<up>x @ Bk # Oc\<up>x)"
-
-fun 
-  inv_end0 :: "nat \<Rightarrow> tape \<Rightarrow>  bool" and
-  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_end5 :: "nat \<Rightarrow> tape \<Rightarrow> bool" 
-where
-  "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 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]
-        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"
-by (auto simp: inv_end1.simps)
-
-lemma [simp]: "inv_end2 x (b, []) = False"
-by (auto simp: inv_end2.simps)
-
-lemma [simp]: "inv_end3 x (b, []) = False"
-by (auto simp: inv_end3.simps)
-
-lemma [simp]: "inv_end4 x (b, []) = False"
-by (auto simp: inv_end4.simps)
-
-lemma [simp]: "inv_end5 x (b, []) = False"
-by (auto simp: inv_end5.simps)
-
-lemma [simp]: "inv_end1 x ([], list) = False"
-by (auto simp: inv_end1.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Bk # list); b \<noteq> []\<rbrakk>
-  \<Longrightarrow> inv_end0 x (tl b, hd b # Bk # list)"
-by (auto simp: inv_end1.simps inv_end0.simps)
-
-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)"
-by (auto simp: inv_end2.simps inv_end3.simps)
-  
-lemma [elim]: "\<lbrakk>0 < x; inv_end4 x ([], Bk # list)\<rbrakk> \<Longrightarrow> 
-  inv_end5 x ([], Bk # Bk # list)"
-by (auto simp: inv_end4.simps inv_end5.simps)
- 
-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)"
-by (auto simp: inv_end1.simps inv_end2.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_end2 x ([], Oc # list)\<rbrakk> \<Longrightarrow>
-               inv_end4 x ([], Bk # Oc # list)"
-by (auto simp: inv_end2.simps inv_end4.simps)
-
-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)"
-by (auto simp: inv_end2.simps inv_end3.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end4 x (b, Bk # list)"
-by (auto simp: inv_end2.simps inv_end4.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_end5 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_end5 x ([], Bk # Oc # list)"
-by (auto simp: inv_end2.simps inv_end5.simps)
-
-declare inv_end5_loop.simps[simp del]
-        inv_end5_exit.simps[simp del]
-
-lemma [simp]: "inv_end5_exit x (b, Oc # list) = False"
-by (auto simp: inv_end5_exit.simps)
-
-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 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)"
-
-definition end_LE :: "(config \<times> config) set"
-  where
-   "end_LE = measures [end_state, end_stage, end_step]"
-
-lemma wf_end_le: "wf end_LE"
-unfolding end_LE_def
-by (auto)
-
-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)"
-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 end_LE_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:
-  "n > 0 \<Longrightarrow> {inv_end1 n} tcopy_end {inv_end0 n}"
-proof(rule_tac Hoare_haltI)
-  fix 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 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>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)") 
-    apply(simp add: inv_end.simps)
-    done
-qed
-
-(* tcopy *)
-
-lemma [intro]: "tm_wf (tcopy_begin, 0)"
-by (auto simp: tm_wf.simps tcopy_begin_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 tcopy_correct1: 
-  assumes "0 < x"
-  shows "{inv_begin1 x} tcopy {inv_end0 x}"
-proof -
-  have "{inv_begin1 x} tcopy_begin {inv_begin0 x}"
-    by (metis assms begin_correct) 
-  moreover 
-  have "inv_begin0 x \<mapsto> inv_loop1 x"
-    unfolding assert_imp_def
-    unfolding inv_begin0.simps inv_loop1.simps
-    unfolding inv_loop1_loop.simps inv_loop1_exit.simps
-    apply(auto simp add: numeral Cons_eq_append_conv)
-    by (rule_tac x = "Suc 0" in exI, auto)
-  ultimately have "{inv_begin1 x} tcopy_begin {inv_loop1 x}"
-    by (rule_tac Hoare_consequence) (auto)
-  moreover
-  have "{inv_loop1 x} tcopy_loop {inv_loop0 x}"
-    by (metis assms loop_correct) 
-  ultimately 
-  have "{inv_begin1 x} (tcopy_begin |+| tcopy_loop) {inv_loop0 x}"
-    by (rule_tac Hoare_plus_halt) (auto)
-  moreover 
-  have "{inv_end1 x} tcopy_end {inv_end0 x}"
-    by (metis assms end_correct) 
-  moreover 
-  have "inv_loop0 x = inv_end1 x"
-    by(auto simp: inv_end1.simps inv_loop1.simps assert_imp_def)
-  ultimately 
-  show "{inv_begin1 x} tcopy {inv_end0 x}"
-    unfolding tcopy_def
-    by (rule_tac Hoare_plus_halt) (auto)
-qed
-
-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}"
-proof -
-  have "{inv_begin1 (Suc n)} tcopy {inv_end0 (Suc n)}"
-    by (rule tcopy_correct1) (simp)
-  moreover
-  have "pre_tcopy n = inv_begin1 (Suc n)" 
-    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_nat_pair)
-  ultimately
-  show "{pre_tcopy n} tcopy {post_tcopy n}" 
-    by simp
-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)] "
-
-(* invariants of dither *)
-abbreviation (input)
-  "dither_halt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"
-
-abbreviation (input)
-  "dither_unhalt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"
-
-lemma dither_loops_aux: 
-  "(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or> 
-   (steps0 (1, Bk \<up> m, [Oc]) dither stp = (2, Oc # Bk \<up> m, []))"
-  apply(induct stp)
-  apply(auto simp: steps.simps step.simps dither_def numeral tape_of_nat_abv)
-  done
-
-lemma dither_loops:
-  shows "{dither_unhalt_inv} dither \<up>" 
-apply(rule Hoare_unhaltI)
-using dither_loops_aux
-apply(auto simp add: numeral tape_of_nat_abv)
-by (metis Suc_neq_Zero is_final_eq)
-
-lemma dither_halts_aux: 
-  shows "steps0 (1, Bk \<up> m, [Oc, Oc]) dither 2 = (0, Bk \<up> m, [Oc, Oc])"
-unfolding dither_def
-by (simp add: steps.simps step.simps numeral)
-
-lemma dither_halts:
-  shows "{dither_halt_inv} dither {dither_halt_inv}" 
-apply(rule Hoare_haltI)
-using dither_halts_aux
-apply(auto simp add: tape_of_nat_abv)
-by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases)
-
-
-section {* The diagnal argument below shows the undecidability of Halting problem *}
-
-text {*
-  @{text "haltP tp x"} means TM @{text "tp"} terminates on input @{text "x"}
-  and the final configuration is standard.
-*}
-
-definition haltP :: "tprog0 \<Rightarrow> nat list \<Rightarrow> bool"
-  where
-  "haltP p ns \<equiv> {(\<lambda>tp. tp = ([], <ns>))} p {(\<lambda>tp. (\<exists>k n l. tp = (Bk \<up> k,  <n::nat> @ Bk \<up> l)))}"
-
-lemma [intro, simp]: "tm_wf0 tcopy"
-by (auto simp: tcopy_def)
-
-lemma [intro, simp]: "tm_wf0 dither"
-by (auto simp: tm_wf.simps dither_def)
-
-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_wf0 H"
-  -- {*
-  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 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>))}"
-begin
-
-(* invariants for H *)
-abbreviation (input)
-  "pre_H_inv M ns \<equiv> \<lambda>tp. tp = ([Bk], <(code M, ns::nat list)>)"
-
-abbreviation (input)
-  "post_H_halt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"
-
-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 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 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 *)
-
-definition
-  "tcontra \<equiv> (tcopy |+| H) |+| dither"
-abbreviation
-  "code_tcontra \<equiv> code tcontra"
-
-(* assume tcontra does not halt on its code *)
-lemma tcontra_unhalt: 
-  assumes "\<not> haltP tcontra [code tcontra]"
-  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 P3 \<equiv> "\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"
-
-  (*
-  {P1} tcopy {P2}  {P2} H {P3} 
-  ----------------------------
-     {P1} (tcopy |+| H) {P3}     {P3} dither {P3}
-  ------------------------------------------------
-                 {P1} tcontra {P3}
-  *)
-
-  have H_wf: "tm_wf0 (tcopy |+| H)" by auto
-
-  (* {P1} (tcopy |+| H) {P3} *)
-  have first: "{P1} (tcopy |+| H) {P3}" 
-  proof (cases rule: Hoare_plus_halt)
-    case A_halt (* of tcopy *)
-    show "{P1} tcopy {P2}" unfolding P1_def P2_def 
-      by (rule tcopy_correct)
-  next
-    case B_halt (* of H *)
-    show "{P2} H {P3}"
-      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} *)
-  have second: "{P3} dither {P3}" unfolding P3_def 
-    by (rule dither_halts)
-  
-  (* {P1} tcontra {P3} *)
-  have "{P1} tcontra {P3}" 
-    unfolding tcontra_def
-    by (rule Hoare_plus_halt[OF first second H_wf])
-
-  with assms show "False"
-    unfolding P1_def P3_def
-    unfolding haltP_def
-    unfolding Hoare_halt_def 
-    apply(auto)    
-    apply(drule_tac x = n in spec)
-    apply(case_tac "steps0 (Suc 0, [], <code tcontra>) tcontra n")
-    apply(auto simp add: tape_of_nl_abv)
-    by (metis append_Nil2 replicate_0)
-qed
-
-(* asumme tcontra halts on its code *)
-lemma tcontra_halt: 
-  assumes "haltP tcontra [code tcontra]"
-  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 Q3 \<equiv> "\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"
-
-  (*
-  {P1} tcopy {P2}  {P2} H {Q3} 
-  ----------------------------
-     {P1} (tcopy |+| H) {Q3}     {Q3} dither loops
-  ------------------------------------------------
-               {P1} tcontra loops
-  *)
-
-  have H_wf: "tm_wf0 (tcopy |+| H)" by auto
-
-  (* {P1} (tcopy |+| H) {Q3} *)
-  have first: "{P1} (tcopy |+| H) {Q3}" 
-  proof (cases rule: Hoare_plus_halt)
-    case A_halt (* of tcopy *)
-    show "{P1} tcopy {P2}" unfolding P1_def P2_def
-      by (rule tcopy_correct)
-  next
-    case B_halt (* of H *)
-    then show "{P2} H {Q3}"
-      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 *)
-  have second: "{Q3} dither \<up>" unfolding Q3_def 
-    by (rule dither_loops)
-  
-  (* {P1} tcontra loops *)
-  have "{P1} tcontra \<up>" 
-    unfolding tcontra_def
-    by (rule Hoare_plus_unhalt[OF first second H_wf])
-
-  with assms show "False"
-    unfolding P1_def
-    unfolding haltP_def
-    unfolding Hoare_halt_def Hoare_unhalt_def
-    by (auto simp add: tape_of_nl_abv)
-qed
-
-      
-text {*
-  @{text "False"} can finally derived.
-*}
-
-lemma false: "False"
-using tcontra_halt tcontra_unhalt 
-by auto
-
-end
-
-declare replicate_Suc[simp del]
-
-
-end
-