1 (* Title: Turing machine's definition and its charater

     2    Author: XuJian <xujian817@hotmail.com>

     3    Maintainer: Xujian

     4 *)

     5 

     6 header {* Undeciablity of the {\em Halting problem} *}

     7 

     8 theory Uncomputable

     9 imports Turing_Hoare

    10 begin

    11 

    12 lemma numeral:

    13   shows "1 = Suc 0"

    14   and "2 = Suc 1"

    15   and "3 = Suc 2"

    16   and "4 = Suc 3" 

    17   and "5 = Suc 4" 

    18   and "6 = Suc 5" 

    19   and "7 = Suc 6"

    20   and "8 = Suc 7" 

    21   and "9 = Suc 8" 

    22   and "10 = Suc 9" 

    23   by arith+

    24 

    25 text {*

    26   The {\em Copying} TM, which duplicates its input. 

    27 *}

    28 

    29 definition 

    30   tcopy_begin :: "instr list"

    31 where

    32   "tcopy_begin \<equiv> [(W0, 0), (R, 2), (R, 3), (R, 2),

    33                  (W1, 3), (L, 4), (L, 4), (L, 0)]"

    34 

    35 definition 

    36   tcopy_loop :: "instr list"

    37 where

    38   "tcopy_loop \<equiv> [(R, 0), (R, 2),  (R, 3), (W0, 2),

    39                  (R, 3), (R, 4), (W1, 5), (R, 4),

    40                  (L, 6), (L, 5), (L, 6), (L, 1)]"

    41 

    42 definition 

    43   tcopy_end :: "instr list"

    44 where

    45   "tcopy_end \<equiv> [(L, 0), (R, 2), (W1, 3), (L, 4),

    46                 (R, 2), (R, 2), (L, 5), (W0, 4),

    47                 (R, 0), (L, 5)]"

    48 

    49 definition 

    50   tcopy :: "instr list"

    51 where

    52   "tcopy \<equiv> (tcopy_begin |+| tcopy_loop) |+| tcopy_end"

    53 

    54 

    55 (* tcopy_begin *)

    56 

    57 fun 

    58   inv_begin0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

    59   inv_begin1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

    60   inv_begin2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

    61   inv_begin3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

    62   inv_begin4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

    63 where

    64   "inv_begin0 n (l, r) = ((n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc])) \<or>   

    65                           (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc])))"

    66 | "inv_begin1 n (l, r) = ((l, r) = ([], Oc \<up> n))"

    67 | "inv_begin2 n (l, r) = (\<exists> i j. i > 0 \<and> i + j = n \<and> (l, r) = (Oc \<up> i, Oc \<up> j))"

    68 | "inv_begin3 n (l, r) = (n > 0 \<and> (l, tl r) = (Bk # Oc \<up> n, []))"

    69 | "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]))"

    70 

    71 fun inv_begin :: "nat \<Rightarrow> config \<Rightarrow> bool"

    72   where

    73   "inv_begin n (s, tp) = 

    74         (if s = 0 then inv_begin0 n tp else

    75          if s = 1 then inv_begin1 n tp else

    76          if s = 2 then inv_begin2 n tp else

    77          if s = 3 then inv_begin3 n tp else

    78          if s = 4 then inv_begin4 n tp 

    79          else False)"

    80 

    81 lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> 

    82   \<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia"

    83 by (rule_tac x = "Suc i" in exI, simp)

    84 

    85 lemma inv_begin_step: 

    86   assumes "inv_begin n cf"

    87   and "n > 0"

    88   shows "inv_begin n (step0 cf tcopy_begin)"

    89 using assms

    90 unfolding tcopy_begin_def

    91 apply(case_tac cf)

    92 apply(auto simp: numeral split: if_splits)

    93 apply(case_tac "hd c")

    94 apply(auto)

    95 apply(case_tac c)

    96 apply(simp_all)

    97 done

    98 

    99 lemma inv_begin_steps: 

   100   assumes "inv_begin n cf"

   101   and "n > 0"

   102   shows "inv_begin n (steps0 cf tcopy_begin stp)"

   103 apply(induct stp)

   104 apply(simp add: assms)

   105 apply(auto simp del: steps.simps)

   106 apply(rule_tac inv_begin_step)

   107 apply(simp_all add: assms)

   108 done

   109 

   110 lemma begin_partial_correctness:

   111   assumes "is_final (steps0 (1, [], Oc \<up> n) tcopy_begin stp)"

   112   shows "0 < n \<Longrightarrow> {inv_begin1 n} tcopy_begin {inv_begin0 n}"

   113 proof(rule_tac Hoare_haltI)

   114   fix l r

   115   assume h: "0 < n" "inv_begin1 n (l, r)"

   116   have "inv_begin n (steps0 (1, [], Oc \<up> n) tcopy_begin stp)"

   117     using h by (rule_tac inv_begin_steps) (simp_all add: inv_begin.simps)

   118   then show

   119     "\<exists>stp. is_final (steps0 (1, l, r) tcopy_begin stp) \<and> 

   120     inv_begin0 n holds_for steps (1, l, r) (tcopy_begin, 0) stp"

   121     using h assms

   122     apply(rule_tac x = stp in exI)

   123     apply(case_tac "(steps0 (1, [], Oc \<up> n) tcopy_begin stp)", simp add: inv_begin.simps)

   124     done

   125 qed

   126 

   127 fun measure_begin_state :: "config \<Rightarrow> nat"

   128   where

   129   "measure_begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)"

   130 

   131 fun measure_begin_step :: "config \<Rightarrow> nat"

   132   where

   133   "measure_begin_step (s, l, r) = 

   134         (if s = 2 then length r else

   135          if s = 3 then (if r = [] \<or> r = [Bk] then 1 else 0) else

   136          if s = 4 then length l 

   137          else 0)"

   138 

   139 definition

   140   "measure_begin = measures [measure_begin_state, measure_begin_step]"

   141 

   142 lemma wf_measure_begin:

   143   shows "wf measure_begin" 

   144 unfolding measure_begin_def 

   145 by auto

   146 

   147 lemma measure_begin_induct [case_names Step]: 

   148   "\<lbrakk>\<And>n. \<not> P (f n) \<Longrightarrow> (f (Suc n), (f n)) \<in> measure_begin\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"

   149 using wf_measure_begin

   150 by (metis wf_iff_no_infinite_down_chain)

   151 

   152 lemma begin_halts: 

   153   assumes h: "x > 0"

   154   shows "\<exists> stp. is_final (steps0 (1, [], Oc \<up> x) tcopy_begin stp)"

   155 proof (induct rule: measure_begin_induct) 

   156   case (Step n)

   157   have "\<not> is_final (steps0 (1, [], Oc \<up> x) tcopy_begin n)" by fact

   158   moreover

   159   have "inv_begin x (steps0 (1, [], Oc \<up> x) tcopy_begin n)"

   160     by (rule_tac inv_begin_steps) (simp_all add: inv_begin.simps h)

   161   moreover

   162   obtain s l r where eq: "(steps0 (1, [], Oc \<up> x) tcopy_begin n) = (s, l, r)"

   163     by (metis measure_begin_state.cases)

   164   ultimately 

   165   have "(step0 (s, l, r) tcopy_begin, s, l, r) \<in> measure_begin"

   166     apply(auto simp: measure_begin_def tcopy_begin_def numeral split: if_splits)

   167     apply(subgoal_tac "r = [Oc]")

   168     apply(auto)

   169     by (metis cell.exhaust list.exhaust tl.simps(2))

   170   then 

   171   show "(steps0 (1, [], Oc \<up> x) tcopy_begin (Suc n), steps0 (1, [], Oc \<up> x) tcopy_begin n) \<in> measure_begin"

   172     using eq by (simp only: step_red)

   173 qed

   174 

   175 lemma begin_correct: 

   176   shows "0 < n \<Longrightarrow> {inv_begin1 n} tcopy_begin {inv_begin0 n}"

   177 using begin_partial_correctness begin_halts by blast

   178 

   179 declare tm_comp.simps [simp del] 

   180 declare adjust.simps[simp del] 

   181 declare shift.simps[simp del]

   182 declare tm_wf.simps[simp del]

   183 declare step.simps[simp del]

   184 declare steps.simps[simp del]

   185 

   186 (* tcopy_loop *)

   187 

   188 fun 

   189   inv_loop1_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

   190   inv_loop1_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

   191   inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

   192   inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

   193   inv_loop6_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

   194   inv_loop6_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   195 where

   196   "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)"

   197 | "inv_loop1_exit n (l, r) = (0 < n \<and> (l, r) = ([], Bk#Oc#Bk\<up>n @ Oc\<up>n))"

   198 | "inv_loop5_loop x (l, r) = 

   199      (\<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))"

   200 | "inv_loop5_exit x (l, r) = 

   201      (\<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))"

   202 | "inv_loop6_loop x (l, r) = 

   203      (\<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))"

   204 | "inv_loop6_exit x (l, r) = 

   205      (\<exists> i j. i + j = x \<and> j > 0 \<and> (l, r) = (Oc\<up>i, Oc#Bk\<up>j @ Oc\<up>j))"

   206 

   207 fun 

   208   inv_loop0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

   209   inv_loop1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

   210   inv_loop2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

   211   inv_loop3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

   212   inv_loop4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

   213   inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

   214   inv_loop6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   215 where

   216   "inv_loop0 n (l, r) =  (0 < n \<and> (l, r) = ([Bk], Oc # Bk\<up>n @ Oc\<up>n))"

   217 | "inv_loop1 n (l, r) = (inv_loop1_loop n (l, r) \<or> inv_loop1_exit n (l, r))"

   218 | "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))"

   219 | "inv_loop3 n (l, r) = 

   220      (\<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))"

   221 | "inv_loop4 n (l, r) = 

   222      (\<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))"

   223 | "inv_loop5 n (l, r) = (inv_loop5_loop n (l, r) \<or> inv_loop5_exit n (l, r))"

   224 | "inv_loop6 n (l, r) = (inv_loop6_loop n (l, r) \<or> inv_loop6_exit n (l, r))"

   225 

   226 fun inv_loop :: "nat \<Rightarrow> config \<Rightarrow> bool"

   227   where

   228   "inv_loop x (s, l, r) = 

   229          (if s = 0 then inv_loop0 x (l, r)

   230           else if s = 1 then inv_loop1 x (l, r)

   231           else if s = 2 then inv_loop2 x (l, r)

   232           else if s = 3 then inv_loop3 x (l, r)

   233           else if s = 4 then inv_loop4 x (l, r)

   234           else if s = 5 then inv_loop5 x (l, r)

   235           else if s = 6 then inv_loop6 x (l, r)

   236           else False)"

   237        

   238 declare inv_loop.simps[simp del] inv_loop1.simps[simp del]

   239         inv_loop2.simps[simp del] inv_loop3.simps[simp del] 

   240         inv_loop4.simps[simp del] inv_loop5.simps[simp del] 

   241         inv_loop6.simps[simp del]

   242 

   243 lemma [elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR"

   244 by (case_tac t, auto)

   245 

   246 lemma [simp]: "inv_loop1 x (b, []) = False"

   247 by (simp add: inv_loop1.simps)

   248 

   249 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"

   250 by (auto simp: inv_loop2.simps inv_loop3.simps)

   251 

   252 

   253 lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"

   254 by (auto simp: inv_loop3.simps)

   255 

   256 

   257 lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop5 x (b, [Oc])"

   258 apply(auto simp: inv_loop4.simps inv_loop5.simps)

   259 apply(rule_tac [!] x = i in exI, 

   260       rule_tac [!] x  = "Suc j" in exI, simp_all)

   261 done

   262 

   263 lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], [])\<rbrakk> \<Longrightarrow> RR"

   264 by (auto simp: inv_loop4.simps inv_loop5.simps)

   265 

   266 lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, []); b \<noteq> []\<rbrakk> \<Longrightarrow> RR"

   267 by (auto simp: inv_loop4.simps inv_loop5.simps)

   268 

   269 lemma [elim]: "inv_loop6 x ([], []) \<Longrightarrow> RR"

   270 by (auto simp: inv_loop6.simps)

   271 

   272 lemma [elim]: "inv_loop6 x (b, []) \<Longrightarrow> RR" 

   273 by (auto simp: inv_loop6.simps)

   274 

   275 lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> b = []"

   276 by (auto simp: inv_loop1.simps)

   277 

   278 lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> list = Oc # Bk \<up> x @ Oc \<up> x"

   279 by (auto simp: inv_loop1.simps)

   280 

   281 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"

   282 apply(auto simp: inv_loop2.simps inv_loop3.simps)

   283 apply(rule_tac [!] x = i  in exI, rule_tac [!] x = j in exI, simp_all)

   284 done

   285 

   286 lemma [elim]: "Bk # list = Oc \<up> j \<Longrightarrow> RR"

   287 by (case_tac j, simp_all)

   288 

   289 lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"

   290 apply(auto simp: inv_loop3.simps)

   291 apply(rule_tac [!] x = i in exI, 

   292       rule_tac [!] x = j in exI, simp_all)

   293 apply(case_tac [!] t, auto)

   294 done

   295 

   296 lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop5 x (b, Oc # list)"

   297 by (auto simp: inv_loop4.simps inv_loop5.simps)

   298 

   299 lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"

   300 by (auto simp: inv_loop6.simps inv_loop5.simps)

   301 

   302 lemma [simp]: "inv_loop5_loop x (b, Bk # list) = False"

   303 by (auto simp: inv_loop5.simps)

   304 

   305 lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"

   306 by (auto simp: inv_loop6.simps)

   307 

   308 declare inv_loop5_loop.simps[simp del]  inv_loop5_exit.simps[simp del]

   309        inv_loop6_loop.simps[simp del]  inv_loop6_exit.simps[simp del]

   310 

   311 lemma [elim]:"\<lbrakk>0 < x; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk> 

   312           \<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"

   313 apply(simp only: inv_loop5_exit.simps inv_loop6_loop.simps )

   314 apply(erule_tac exE)+

   315 apply(rule_tac x = i in exI, 

   316       rule_tac x = j in exI,

   317       rule_tac x = "j - Suc (Suc 0)" in exI, 

   318       rule_tac x = "Suc 0" in exI, auto)

   319 apply(case_tac [!] j, simp_all)

   320 apply(case_tac [!] nat, simp_all)

   321 done

   322 

   323 lemma [simp]: "inv_loop6_loop x (b, Oc # Bk # list) = False"

   324 by (auto simp: inv_loop6_loop.simps)

   325 

   326 lemma [elim]: "\<lbrakk>x > 0; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow> 

   327   inv_loop6_exit x (tl b, Oc # Bk # list)"

   328 apply(simp only: inv_loop5_exit.simps inv_loop6_exit.simps)

   329 apply(erule_tac exE)+

   330 apply(rule_tac x = "x - 1" in exI, rule_tac x = 1 in exI, simp)

   331 apply(case_tac j, auto)

   332 apply(case_tac [!] nat, auto)

   333 done

   334 

   335 lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"

   336 apply(simp add: inv_loop5.simps inv_loop6.simps)

   337 apply(case_tac "hd b", simp_all, auto)

   338 done

   339 

   340 lemma  [simp]: "inv_loop6 x ([], Bk # xs) = False"

   341 apply(simp add: inv_loop6.simps inv_loop6_loop.simps

   342                 inv_loop6_exit.simps)

   343 apply(auto)

   344 done

   345 

   346 lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"

   347 by (simp)

   348 

   349 lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"

   350 by (simp add: inv_loop6_exit.simps)

   351 

   352 lemma [elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk>

   353               \<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"

   354 apply(simp only: inv_loop6_loop.simps)

   355 apply(erule_tac exE)+

   356 apply(rule_tac x = i in exI, rule_tac x = j in exI, 

   357       rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, auto)

   358 apply(case_tac [!] k, auto)

   359 done

   360 

   361 lemma [elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> 

   362         \<Longrightarrow> inv_loop6_exit x (tl b, Oc # Bk # list)"

   363 apply(simp only: inv_loop6_loop.simps inv_loop6_exit.simps)

   364 apply(erule_tac exE)+

   365 apply(rule_tac x = "i - 1" in exI, rule_tac x = j in exI, auto)

   366 apply(case_tac [!] k, auto)

   367 done

   368 

   369 lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"

   370 apply(simp add: inv_loop6.simps)

   371 apply(case_tac "hd b", simp_all, auto)

   372 done

   373 

   374 lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (Oc # b, list)"

   375 apply(auto simp: inv_loop1.simps inv_loop2.simps)

   376 apply(rule_tac x = "Suc i" in exI, auto)

   377 done

   378 

   379 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (b, Bk # list)"

   380 by (auto simp: inv_loop2.simps)

   381 

   382 lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"

   383 apply(auto simp: inv_loop3.simps inv_loop4.simps)

   384 apply(rule_tac [!] x = i in exI, auto)

   385 apply(rule_tac [!] x = "Suc 0" in exI, rule_tac [!] x = "j - 1" in exI, auto)

   386 apply(case_tac [!] t, auto)

   387 apply(case_tac [!] j, auto)

   388 done

   389 

   390 lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"

   391 apply(auto simp: inv_loop4.simps)

   392 apply(rule_tac [!] x = "i" in exI, auto)

   393 apply(rule_tac [!] x = "Suc k" in exI, rule_tac [!] x = "t - 1" in exI, auto)

   394 apply(case_tac [!] t, simp_all)

   395 done

   396 

   397 lemma [simp]: "inv_loop5 x ([], list) = False"

   398 by (auto simp: inv_loop5.simps inv_loop5_exit.simps inv_loop5_loop.simps)

   399 

   400 lemma [simp]: "inv_loop5_exit x (b, Oc # list) = False"

   401 by (auto simp: inv_loop5_exit.simps)

   402 

   403 lemma [elim]: " \<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk>

   404   \<Longrightarrow> inv_loop5_exit x (tl b, Bk # Oc # list)"

   405 apply(simp only: inv_loop5_loop.simps inv_loop5_exit.simps)

   406 apply(erule_tac exE)+

   407 apply(rule_tac x = i in exI, auto)

   408 apply(case_tac [!] k, auto)

   409 done

   410 

   411 lemma [elim]: "\<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk> 

   412            \<Longrightarrow> inv_loop5_loop x (tl b, Oc # Oc # list)"

   413 apply(simp only:  inv_loop5_loop.simps)

   414 apply(erule_tac exE)+

   415 apply(rule_tac x = i in exI, rule_tac x = j in exI)

   416 apply(rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, auto)

   417 apply(case_tac [!] k, auto)

   418 done

   419 

   420 lemma [elim]: "\<lbrakk>inv_loop5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop5 x (tl b, hd b # Oc # list)"

   421 apply(simp add: inv_loop5.simps)

   422 apply(case_tac "hd b", simp_all, auto)

   423 done

   424 

   425 lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_loop1 x ([], Bk # Oc # list)"

   426 apply(auto simp: inv_loop6.simps inv_loop1.simps 

   427   inv_loop6_loop.simps inv_loop6_exit.simps)

   428 done

   429 

   430 lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Oc # list); b \<noteq> []\<rbrakk> 

   431            \<Longrightarrow> inv_loop1 x (tl b, hd b # Oc # list)"

   432 apply(auto simp: inv_loop6.simps inv_loop1.simps 

   433   inv_loop6_loop.simps inv_loop6_exit.simps)

   434 done

   435 

   436 lemma inv_loop_step: 

   437   "\<lbrakk>inv_loop x cf; x > 0\<rbrakk> \<Longrightarrow> inv_loop x (step cf (tcopy_loop, 0))"

   438 apply(case_tac cf, case_tac c, case_tac [2] aa)

   439 apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral split: if_splits)

   440 done

   441 

   442 lemma inv_loop_steps:

   443   "\<lbrakk>inv_loop x cf; x > 0\<rbrakk> \<Longrightarrow> inv_loop x (steps cf (tcopy_loop, 0) stp)"

   444 apply(induct stp, simp add: steps.simps, simp)

   445 apply(erule_tac inv_loop_step, simp)

   446 done

   447 

   448 fun loop_stage :: "config \<Rightarrow> nat"

   449   where

   450   "loop_stage (s, l, r) = (if s = 0 then 0

   451                            else (Suc (length (takeWhile (\<lambda>a. a = Oc) (rev l @ r)))))"

   452 

   453 fun loop_state :: "config \<Rightarrow> nat"

   454   where

   455   "loop_state (s, l, r) = (if s = 2 \<and> hd r = Oc then 0

   456                            else if s = 1 then 1

   457                            else 10 - s)"

   458 

   459 fun loop_step :: "config \<Rightarrow> nat"

   460   where

   461   "loop_step (s, l, r) = (if s = 3 then length r

   462                           else if s = 4 then length r

   463                           else if s = 5 then length l 

   464                           else if s = 6 then length l

   465                           else 0)"

   466 

   467 definition measure_loop :: "(config \<times> config) set"

   468   where

   469    "measure_loop = measures [loop_stage, loop_state, loop_step]"

   470 

   471 lemma wf_measure_loop: "wf measure_loop"

   472 unfolding measure_loop_def

   473 by (auto)

   474 

   475 lemma measure_loop_induct [case_names Step]: 

   476   "\<lbrakk>\<And>n. \<not> P (f n) \<Longrightarrow> (f (Suc n), (f n)) \<in> measure_loop\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"

   477 using wf_measure_loop

   478 by (metis wf_iff_no_infinite_down_chain)

   479 

   480 

   481 

   482 lemma [simp]: "inv_loop2 x ([], b) = False"

   483 by (auto simp: inv_loop2.simps)

   484 

   485 lemma  [simp]: "inv_loop2 x (l', []) = False"

   486 by (auto simp: inv_loop2.simps)

   487 

   488 lemma [simp]: "inv_loop3 x (b, []) = False"

   489 by (auto simp: inv_loop3.simps)

   490 

   491 lemma [simp]: "inv_loop4 x ([], b) = False"

   492 by (auto simp: inv_loop4.simps)

   493 

   494 

   495 lemma [elim]: 

   496   "\<lbrakk>inv_loop4 x (l', []); l' \<noteq> []; x > 0;

   497   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ [Oc])) \<noteq> 

   498   length (takeWhile (\<lambda>a. a = Oc) (rev l'))\<rbrakk>

   499   \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ [Oc])) < length (takeWhile (\<lambda>a. a = Oc) (rev l'))"

   500 apply(auto simp: inv_loop4.simps)

   501 apply(case_tac [!] j, simp_all add: List.takeWhile_tail)

   502 done

   503 

   504 

   505 lemma [elim]: 

   506   "\<lbrakk>inv_loop4 x (l', Bk # list); l' \<noteq> []; 0 < x;

   507    length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) \<noteq> 

   508     length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>

   509     \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) < 

   510     length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"

   511 by (auto simp: inv_loop4.simps)

   512 

   513 lemma takeWhile_replicate_append: 

   514   "P a \<Longrightarrow> takeWhile P (a\<up>x @ ys) = a\<up>x @ takeWhile P ys"

   515 by (induct x, auto)

   516 

   517 lemma takeWhile_replicate: 

   518   "P a \<Longrightarrow> takeWhile P (a\<up>x) = a\<up>x"

   519 by (induct x, auto)

   520 

   521 lemma [elim]: 

   522    "\<lbrakk>inv_loop5 x (l', Bk # list); l' \<noteq> []; 0 < x;

   523    length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq>

   524    length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>

   525    \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) < 

   526    length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"

   527 apply(auto simp: inv_loop5.simps inv_loop5_exit.simps)

   528 apply(case_tac [!] j, simp_all)

   529 apply(case_tac [!] "nat", simp_all)

   530 apply(case_tac  nata, simp_all add: List.takeWhile_tail)

   531 apply(simp add: takeWhile_replicate_append takeWhile_replicate)

   532 apply(case_tac  nata, simp_all add: List.takeWhile_tail)

   533 done

   534 

   535 lemma [elim]: "\<lbrakk>inv_loop1 x (l', Oc # list)\<rbrakk> \<Longrightarrow> hd list = Oc"

   536 by (auto simp: inv_loop1.simps)

   537 

   538 lemma [elim]: 

   539   "\<lbrakk>inv_loop6 x (l', Bk # list); l' \<noteq> []; 0 < x;

   540   length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq> 

   541   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>

   542   \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) < 

   543   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"

   544 apply(auto simp: inv_loop6.simps)

   545 apply(case_tac l', simp_all)

   546 done

   547 

   548 lemma [elim]:

   549   "\<lbrakk>inv_loop2 x (l', Oc # list); l' \<noteq> []; 0 < x\<rbrakk> \<Longrightarrow> 

   550   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list)) <

   551   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"

   552 apply(auto simp: inv_loop2.simps)

   553 apply(simp_all add: takeWhile_tail takeWhile_replicate_append

   554                 takeWhile_replicate)

   555 done

   556 

   557 lemma [elim]: 

   558   "\<lbrakk>inv_loop5 x (l', Oc # list); l' \<noteq> []; 0 < x;

   559   length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) \<noteq> 

   560   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))\<rbrakk>

   561   \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) < 

   562   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"

   563 apply(auto simp: inv_loop5.simps)

   564 apply(case_tac l', auto)

   565 done

   566 

   567 lemma[elim]: 

   568   "\<lbrakk>inv_loop6 x (l', Oc # list); l' \<noteq> []; 0 < x;

   569   length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list))

   570   \<noteq> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))\<rbrakk>

   571   \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) < 

   572       length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"

   573 apply(case_tac l')

   574 apply(auto simp: inv_loop6.simps)

   575 done

   576 

   577 lemma loop_halts: 

   578   assumes h: "n > 0" "inv_loop n (1, l, r)"

   579   shows "\<exists> stp. is_final (steps0 (1, l, r) tcopy_loop stp)"

   580 proof (induct rule: measure_loop_induct) 

   581   case (Step stp)

   582   have "\<not> is_final (steps0 (1, l, r) tcopy_loop stp)" by fact

   583   moreover

   584   have "inv_loop n (steps0 (1, l, r) tcopy_loop stp)"

   585     by (rule_tac inv_loop_steps) (simp_all only: h)

   586   moreover

   587   obtain s l' r' where eq: "(steps0 (1, l, r) tcopy_loop stp) = (s, l', r')"

   588     by (metis measure_begin_state.cases)

   589   ultimately 

   590   have "(step0 (s, l', r') tcopy_loop, s, l', r') \<in> measure_loop"

   591     using h(1)

   592     apply(case_tac r')

   593     apply(case_tac [2] a)

   594     apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral measure_loop_def split: if_splits)

   595     done

   596   then 

   597   show "(steps0 (1, l, r) tcopy_loop (Suc stp), steps0 (1, l, r) tcopy_loop stp) \<in> measure_loop"

   598     using eq by (simp only: step_red)

   599 qed

   600 

   601 lemma loop_correct:

   602   shows "0 < n \<Longrightarrow> {inv_loop1 n} tcopy_loop {inv_loop0 n}"

   603   using assms

   604 proof(rule_tac Hoare_haltI)

   605   fix l r

   606   assume h: "0 < n" "inv_loop1 n (l, r)"

   607   then obtain stp where k: "is_final (steps0 (1, l, r) tcopy_loop stp)" 

   608     using loop_halts

   609     apply(simp add: inv_loop.simps)

   610     apply(blast)

   611     done

   612   moreover

   613   have "inv_loop n (steps0 (1, l, r) tcopy_loop stp)"

   614     using h 

   615     by (rule_tac inv_loop_steps) (simp_all add: inv_loop.simps)

   616   ultimately show

   617     "\<exists>stp. is_final (steps0 (1, l, r) tcopy_loop stp) \<and> 

   618     inv_loop0 n holds_for steps0 (1, l, r) tcopy_loop stp"

   619     using h(1) 

   620     apply(rule_tac x = stp in exI)

   621     apply(case_tac "(steps0 (1, l, r) tcopy_loop stp)")

   622     apply(simp add: inv_loop.simps)

   623     done

   624 qed

   625 

   626 

   627 

   628 

   629 (* tcopy_end *)

   630 

   631 fun

   632   inv_end5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

   633   inv_end5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" 

   634 where  

   635   "inv_end5_loop x (l, r) = 

   636      (\<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)"

   637 | "inv_end5_exit x (l, r) = (x > 0 \<and> l = [] \<and> r = Bk # Oc\<up>x @ Bk # Oc\<up>x)"

   638 

   639 fun 

   640   inv_end0 :: "nat \<Rightarrow> tape \<Rightarrow>  bool" and

   641   inv_end1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

   642   inv_end2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

   643   inv_end3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

   644   inv_end4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and 

   645   inv_end5 :: "nat \<Rightarrow> tape \<Rightarrow> bool" 

   646 where

   647   "inv_end0 n (l, r) = (n > 0 \<and> (l, r) = ([Bk], Oc\<up>n @ Bk # Oc\<up>n))"

   648 | "inv_end1 n (l, r) = (n > 0 \<and> (l, r) = ([Bk], Oc # Bk\<up>n @ Oc\<up>n))"

   649 | "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)"

   650 | "inv_end3 n (l, r) =

   651      (\<exists> i j. n > 0 \<and> i + j = n \<and> l = Oc\<up>i @ [Bk] \<and> r = Oc # Bk\<up>j@ Oc\<up>n)"

   652 | "inv_end4 n (l, r) = (\<exists> any. n > 0 \<and> l = Oc\<up>n @ [Bk] \<and> r = any#Oc\<up>n)"

   653 | "inv_end5 n (l, r) = (inv_end5_loop n (l, r) \<or> inv_end5_exit n (l, r))"

   654 

   655 fun 

   656   inv_end :: "nat \<Rightarrow> config \<Rightarrow> bool"

   657 where

   658   "inv_end n (s, l, r) = (if s = 0 then inv_end0 n (l, r)

   659                           else if s = 1 then inv_end1 n (l, r)

   660                           else if s = 2 then inv_end2 n (l, r)

   661                           else if s = 3 then inv_end3 n (l, r)

   662                           else if s = 4 then inv_end4 n (l, r)

   663                           else if s = 5 then inv_end5 n (l, r)

   664                           else False)"

   665 

   666 declare inv_end.simps[simp del] inv_end1.simps[simp del]

   667         inv_end0.simps[simp del] inv_end2.simps[simp del]

   668         inv_end3.simps[simp del] inv_end4.simps[simp del]

   669         inv_end5.simps[simp del]

   670 

   671 lemma [simp]:  "inv_end1 x (b, []) = False"

   672 by (auto simp: inv_end1.simps)

   673 

   674 lemma [simp]: "inv_end2 x (b, []) = False"

   675 by (auto simp: inv_end2.simps)

   676 

   677 lemma [simp]: "inv_end3 x (b, []) = False"

   678 by (auto simp: inv_end3.simps)

   679 

   680 lemma [simp]: "inv_end4 x (b, []) = False"

   681 by (auto simp: inv_end4.simps)

   682 

   683 lemma [simp]: "inv_end5 x (b, []) = False"

   684 by (auto simp: inv_end5.simps)

   685 

   686 lemma [simp]: "inv_end1 x ([], list) = False"

   687 by (auto simp: inv_end1.simps)

   688 

   689 lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Bk # list); b \<noteq> []\<rbrakk>

   690   \<Longrightarrow> inv_end0 x (tl b, hd b # Bk # list)"

   691 by (auto simp: inv_end1.simps inv_end0.simps)

   692 

   693 lemma [elim]: "\<lbrakk>0 < x; inv_end2 x (b, Bk # list)\<rbrakk> 

   694   \<Longrightarrow> inv_end3 x (b, Oc # list)"

   695 apply(auto simp: inv_end2.simps inv_end3.simps)

   696 apply(rule_tac x = "j - 1" in exI)

   697 apply(case_tac j, simp_all)

   698 apply(case_tac x, simp_all)

   699 done

   700 

   701 lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Bk # b, list)"

   702 by (auto simp: inv_end2.simps inv_end3.simps)

   703   

   704 lemma [elim]: "\<lbrakk>0 < x; inv_end4 x ([], Bk # list)\<rbrakk> \<Longrightarrow> 

   705   inv_end5 x ([], Bk # Bk # list)"

   706 by (auto simp: inv_end4.simps inv_end5.simps)

   707  

   708 lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> 

   709   inv_end5 x (tl b, hd b # Bk # list)"

   710 apply(auto simp: inv_end4.simps inv_end5.simps)

   711 apply(rule_tac x = 1 in exI, simp)

   712 done

   713 

   714 lemma [elim]: "\<lbrakk>0 < x; inv_end5 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end0 x (Bk # b, list)"

   715 apply(auto simp: inv_end5.simps inv_end0.simps)

   716 apply(case_tac [!] j, simp_all)

   717 done

   718 

   719 lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"

   720 by (auto simp: inv_end1.simps inv_end2.simps)

   721 

   722 lemma [elim]: "\<lbrakk>0 < x; inv_end2 x ([], Oc # list)\<rbrakk> \<Longrightarrow>

   723                inv_end4 x ([], Bk # Oc # list)"

   724 by (auto simp: inv_end2.simps inv_end4.simps)

   725 

   726 lemma [elim]:  "\<lbrakk>0 < x; inv_end2 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>

   727   inv_end4 x (tl b, hd b # Oc # list)"

   728 apply(auto simp: inv_end2.simps inv_end4.simps)

   729 apply(case_tac [!] j, simp_all)

   730 done

   731 

   732 lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"

   733 by (auto simp: inv_end2.simps inv_end3.simps)

   734 

   735 lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end4 x (b, Bk # list)"

   736 by (auto simp: inv_end2.simps inv_end4.simps)

   737 

   738 lemma [elim]: "\<lbrakk>0 < x; inv_end5 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_end5 x ([], Bk # Oc # list)"

   739 by (auto simp: inv_end2.simps inv_end5.simps)

   740 

   741 declare inv_end5_loop.simps[simp del]

   742         inv_end5_exit.simps[simp del]

   743 

   744 lemma [simp]: "inv_end5_exit x (b, Oc # list) = False"

   745 by (auto simp: inv_end5_exit.simps)

   746 

   747 lemma [simp]: "inv_end5_loop x (tl b, Bk # Oc # list) = False"

   748 apply(auto simp: inv_end5_loop.simps)

   749 apply(case_tac [!] j, simp_all)

   750 done

   751 

   752 lemma [elim]:

   753   "\<lbrakk>0 < x; inv_end5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk> \<Longrightarrow>

   754   inv_end5_exit x (tl b, Bk # Oc # list)"

   755 apply(auto simp: inv_end5_loop.simps inv_end5_exit.simps)

   756 apply(case_tac [!] i, simp_all)

   757 done

   758 

   759 lemma [elim]: 

   760   "\<lbrakk>0 < x; inv_end5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow>

   761   inv_end5_loop x (tl b, Oc # Oc # list)"

   762 apply(simp only: inv_end5_loop.simps inv_end5_exit.simps)

   763 apply(erule_tac exE)+

   764 apply(rule_tac x = "i - 1" in exI, 

   765       rule_tac x = "Suc j" in exI, auto)

   766 apply(case_tac [!] i, simp_all)

   767 done

   768 

   769 lemma [elim]: "\<lbrakk>0 < x; inv_end5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow> 

   770   inv_end5 x (tl b, hd b # Oc # list)"

   771 apply(simp add: inv_end2.simps inv_end5.simps)

   772 apply(case_tac "hd b", simp_all, auto)

   773 done

   774 

   775 lemma inv_end_step:

   776   "\<lbrakk>x > 0; inv_end x cf\<rbrakk> \<Longrightarrow> inv_end x (step cf (tcopy_end, 0))"

   777 apply(case_tac cf, case_tac c, case_tac [2] aa)

   778 apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral split: if_splits)

   779 done

   780 

   781 lemma inv_end_steps:

   782   "\<lbrakk>x > 0; inv_end x cf\<rbrakk> \<Longrightarrow> inv_end x (steps cf (tcopy_end, 0) stp)"

   783 apply(induct stp, simp add:steps.simps, simp)

   784 apply(erule_tac inv_end_step, simp)

   785 done

   786 

   787 fun end_state :: "config \<Rightarrow> nat"

   788   where

   789   "end_state (s, l, r) = 

   790        (if s = 0 then 0

   791         else if s = 1 then 5

   792         else if s = 2 \<or> s = 3 then 4

   793         else if s = 4 then 3 

   794         else if s = 5 then 2

   795         else 0)"

   796 

   797 fun end_stage :: "config \<Rightarrow> nat"

   798   where

   799   "end_stage (s, l, r) = 

   800           (if s = 2 \<or> s = 3 then (length r) else 0)"

   801 

   802 fun end_step :: "config \<Rightarrow> nat"

   803   where

   804   "end_step (s, l, r) = 

   805          (if s = 4 then (if hd r = Oc then 1 else 0)

   806           else if s = 5 then length l

   807           else if s = 2 then 1

   808           else if s = 3 then 0

   809           else 0)"

   810 

   811 definition end_LE :: "(config \<times> config) set"

   812   where

   813    "end_LE = measures [end_state, end_stage, end_step]"

   814 

   815 lemma wf_end_le: "wf end_LE"

   816 unfolding end_LE_def

   817 by (auto)

   818 

   819 lemma [simp]: "inv_end5 x ([], Oc # list) = False"

   820 by (auto simp: inv_end5.simps inv_end5_loop.simps)

   821 

   822 lemma halt_lemma: 

   823   "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"

   824 by (metis wf_iff_no_infinite_down_chain)

   825 

   826 lemma end_halt: 

   827   "\<lbrakk>x > 0; inv_end x (Suc 0, l, r)\<rbrakk> \<Longrightarrow> 

   828       \<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_end, 0) stp)"

   829 proof(rule_tac LE = end_LE in halt_lemma)

   830   show "wf end_LE" by(intro wf_end_le)

   831 next

   832   assume great: "0 < x"

   833     and inv_start: "inv_end x (Suc 0, l, r)"

   834   show "\<forall>n. \<not> is_final (steps (Suc 0, l, r) (tcopy_end, 0) n) \<longrightarrow> 

   835     (steps (Suc 0, l, r) (tcopy_end, 0) (Suc n), steps (Suc 0, l, r) (tcopy_end, 0) n) \<in> end_LE"

   836   proof(rule_tac allI, rule_tac impI)

   837     fix n

   838     assume notfinal: "\<not> is_final (steps (Suc 0, l, r) (tcopy_end, 0) n)"

   839     obtain s' l' r' where d: "steps (Suc 0, l, r) (tcopy_end, 0) n = (s', l', r')"

   840       apply(case_tac "steps (Suc 0, l, r) (tcopy_end, 0) n", auto)

   841       done

   842     hence "inv_end x (s', l', r') \<and> s' \<noteq> 0"

   843       using great inv_start notfinal

   844       apply(drule_tac stp = n in inv_end_steps, auto)

   845       done

   846     hence "(step (s', l', r') (tcopy_end, 0), s', l', r') \<in> end_LE"

   847       apply(case_tac r', case_tac [2] a)

   848       apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral end_LE_def split: if_splits)

   849       done

   850     thus "(steps (Suc 0, l, r) (tcopy_end, 0) (Suc n), 

   851       steps (Suc 0, l, r) (tcopy_end, 0) n) \<in> end_LE"

   852       using d

   853       by simp

   854   qed

   855 qed

   856 

   857 lemma end_correct:

   858   "n > 0 \<Longrightarrow> {inv_end1 n} tcopy_end {inv_end0 n}"

   859 proof(rule_tac Hoare_haltI)

   860   fix l r

   861   assume h: "0 < n"

   862     "inv_end1 n (l, r)"

   863   then have "\<exists> stp. is_final (steps0 (1, l, r) tcopy_end stp)"

   864     by (simp add: end_halt inv_end.simps)

   865   then obtain stp where "is_final (steps0 (1, l, r) tcopy_end stp)" ..

   866   moreover have "inv_end n (steps0 (1, l, r) tcopy_end stp)"

   867     apply(rule_tac inv_end_steps)

   868     using h by(simp_all add: inv_end.simps)

   869   ultimately show

   870     "\<exists>stp. is_final (steps (1, l, r) (tcopy_end, 0) stp) \<and> 

   871     inv_end0 n holds_for steps (1, l, r) (tcopy_end, 0) stp"        

   872     using h

   873     apply(rule_tac x = stp in exI)

   874     apply(case_tac "(steps0 (1, l, r) tcopy_end stp)") 

   875     apply(simp add: inv_end.simps)

   876     done

   877 qed

   878 

   879 (* tcopy *)

   880 

   881 lemma [intro]: "tm_wf (tcopy_begin, 0)"

   882 by (auto simp: tm_wf.simps tcopy_begin_def)

   883 

   884 lemma [intro]: "tm_wf (tcopy_loop, 0)"

   885 by (auto simp: tm_wf.simps tcopy_loop_def)

   886 

   887 lemma [intro]: "tm_wf (tcopy_end, 0)"

   888 by (auto simp: tm_wf.simps tcopy_end_def)

   889 

   890 lemma tcopy_correct1: 

   891   assumes "0 < x"

   892   shows "{inv_begin1 x} tcopy {inv_end0 x}"

   893 proof -

   894   have "{inv_begin1 x} tcopy_begin {inv_begin0 x}"

   895     by (metis assms begin_correct) 

   896   moreover 

   897   have "inv_begin0 x \<mapsto> inv_loop1 x"

   898     unfolding assert_imp_def

   899     unfolding inv_begin0.simps inv_loop1.simps

   900     unfolding inv_loop1_loop.simps inv_loop1_exit.simps

   901     apply(auto simp add: numeral Cons_eq_append_conv)

   902     by (rule_tac x = "Suc 0" in exI, auto)

   903   ultimately have "{inv_begin1 x} tcopy_begin {inv_loop1 x}"

   904     by (rule_tac Hoare_consequence) (auto)

   905   moreover

   906   have "{inv_loop1 x} tcopy_loop {inv_loop0 x}"

   907     by (metis assms loop_correct) 

   908   ultimately 

   909   have "{inv_begin1 x} (tcopy_begin |+| tcopy_loop) {inv_loop0 x}"

   910     by (rule_tac Hoare_plus_halt) (auto)

   911   moreover 

   912   have "{inv_end1 x} tcopy_end {inv_end0 x}"

   913     by (metis assms end_correct) 

   914   moreover 

   915   have "inv_loop0 x = inv_end1 x"

   916     by(auto simp: inv_end1.simps inv_loop1.simps assert_imp_def)

   917   ultimately 

   918   show "{inv_begin1 x} tcopy {inv_end0 x}"

   919     unfolding tcopy_def

   920     by (rule_tac Hoare_plus_halt) (auto)

   921 qed

   922 

   923 abbreviation (input)

   924   "pre_tcopy n \<equiv> \<lambda>tp. tp = ([]::cell list, <(n::nat)>)"

   925 abbreviation (input)

   926   "post_tcopy n \<equiv> \<lambda>tp. tp= ([Bk], <(n, n::nat)>)"

   927 

   928 lemma tcopy_correct:

   929   shows "{pre_tcopy n} tcopy {post_tcopy n}"

   930 proof -

   931   have "{inv_begin1 (Suc n)} tcopy {inv_end0 (Suc n)}"

   932     by (rule tcopy_correct1) (simp)

   933   moreover

   934   have "pre_tcopy n = inv_begin1 (Suc n)" 

   935     by (auto simp add: tape_of_nl_abv tape_of_nat_abv)

   936   moreover

   937   have "inv_end0 (Suc n) = post_tcopy n" 

   938     by (auto simp add: inv_end0.simps tape_of_nat_abv tape_of_nat_pair)

   939   ultimately

   940   show "{pre_tcopy n} tcopy {post_tcopy n}" 

   941     by simp

   942 qed

   943 

   944 

   945 section {* The {\em Dithering} Turing Machine *}

   946 

   947 text {*

   948   The {\em Dithering} TM, when the input is @{text "1"}, it will loop forever, otherwise, it will

   949   terminate.

   950 *}

   951 

   952 definition dither :: "instr list"

   953   where

   954   "dither \<equiv> [(W0, 1), (R, 2), (L, 1), (L, 0)] "

   955 

   956 (* invariants of dither *)

   957 abbreviation (input)

   958   "dither_halt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"

   959 

   960 abbreviation (input)

   961   "dither_unhalt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"

   962 

   963 lemma dither_loops_aux: 

   964   "(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or> 

   965    (steps0 (1, Bk \<up> m, [Oc]) dither stp = (2, Oc # Bk \<up> m, []))"

   966   apply(induct stp)

   967   apply(auto simp: steps.simps step.simps dither_def numeral tape_of_nat_abv)

   968   done

   969 

   970 lemma dither_loops:

   971   shows "{dither_unhalt_inv} dither \<up>" 

   972 apply(rule Hoare_unhaltI)

   973 using dither_loops_aux

   974 apply(auto simp add: numeral tape_of_nat_abv)

   975 by (metis Suc_neq_Zero is_final_eq)

   976 

   977 lemma dither_halts_aux: 

   978   shows "steps0 (1, Bk \<up> m, [Oc, Oc]) dither 2 = (0, Bk \<up> m, [Oc, Oc])"

   979 unfolding dither_def

   980 by (simp add: steps.simps step.simps numeral)

   981 

   982 lemma dither_halts:

   983   shows "{dither_halt_inv} dither {dither_halt_inv}" 

   984 apply(rule Hoare_haltI)

   985 using dither_halts_aux

   986 apply(auto simp add: tape_of_nat_abv)

   987 by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases)

   988 

   989 

   990 section {* The diagnal argument below shows the undecidability of Halting problem *}

   991 

   992 text {*

   993   @{text "haltP tp x"} means TM @{text "tp"} terminates on input @{text "x"}

   994   and the final configuration is standard.

   995 *}

   996 

   997 definition haltP :: "tprog0 \<Rightarrow> nat list \<Rightarrow> bool"

   998   where

   999   "haltP p ns \<equiv> {(\<lambda>tp. tp = ([], <ns>))} p {(\<lambda>tp. (\<exists>k n l. tp = (Bk \<up> k,  <n::nat> @ Bk \<up> l)))}"

  1000 

  1001 lemma [intro, simp]: "tm_wf0 tcopy"

  1002 by (auto simp: tcopy_def)

  1003 

  1004 lemma [intro, simp]: "tm_wf0 dither"

  1005 by (auto simp: tm_wf.simps dither_def)

  1006 

  1007 text {*

  1008   The following locale specifies that TM @{text "H"} can be used to solve 

  1009   the {\em Halting Problem} and @{text "False"} is going to be derived 

  1010   under this locale. Therefore, the undecidability of {\em Halting Problem}

  1011   is established. 

  1012 *}

  1013 

  1014 locale uncomputable = 

  1015   -- {* The coding function of TM, interestingly, the detailed definition of this 

  1016   funciton @{text "code"} does not affect the final result. *}

  1017   fixes code :: "instr list \<Rightarrow> nat" 

  1018   -- {* 

  1019   The TM @{text "H"} is the one which is assummed being able to solve the Halting problem.

  1020   *}

  1021   and H :: "instr list"

  1022   assumes h_wf[intro]: "tm_wf0 H"

  1023   -- {*

  1024   The following two assumptions specifies that @{text "H"} does solve the Halting problem.

  1025   *}

  1026   and h_case: 

  1027   "\<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>))}"

  1028   and nh_case: 

  1029   "\<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>))}"

  1030 begin

  1031 

  1032 (* invariants for H *)

  1033 abbreviation (input)

  1034   "pre_H_inv M ns \<equiv> \<lambda>tp. tp = ([Bk], <(code M, ns::nat list)>)"

  1035 

  1036 abbreviation (input)

  1037   "post_H_halt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"

  1038 

  1039 abbreviation (input)

  1040   "post_H_unhalt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"

  1041 

  1042 

  1043 lemma H_halt_inv:

  1044   assumes "\<not> haltP M ns" 

  1045   shows "{pre_H_inv M ns} H {post_H_halt_inv}"

  1046 using assms nh_case by auto

  1047 

  1048 lemma H_unhalt_inv:

  1049   assumes "haltP M ns" 

  1050   shows "{pre_H_inv M ns} H {post_H_unhalt_inv}"

  1051 using assms h_case by auto

  1052    

  1053 (* TM that produces the contradiction and its code *)

  1054 

  1055 definition

  1056   "tcontra \<equiv> (tcopy |+| H) |+| dither"

  1057 abbreviation

  1058   "code_tcontra \<equiv> code tcontra"

  1059 

  1060 (* assume tcontra does not halt on its code *)

  1061 lemma tcontra_unhalt: 

  1062   assumes "\<not> haltP tcontra [code tcontra]"

  1063   shows "False"

  1064 proof -

  1065   (* invariants *)

  1066   def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <code_tcontra>)"

  1067   def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"

  1068   def P3 \<equiv> "\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"

  1069 

  1070   (*

  1071   {P1} tcopy {P2}  {P2} H {P3} 

  1072   ----------------------------

  1073      {P1} (tcopy |+| H) {P3}     {P3} dither {P3}

  1074   ------------------------------------------------

  1075                  {P1} tcontra {P3}

  1076   *)

  1077 

  1078   have H_wf: "tm_wf0 (tcopy |+| H)" by auto

  1079 

  1080   (* {P1} (tcopy |+| H) {P3} *)

  1081   have first: "{P1} (tcopy |+| H) {P3}" 

  1082   proof (cases rule: Hoare_plus_halt)

  1083     case A_halt (* of tcopy *)

  1084     show "{P1} tcopy {P2}" unfolding P1_def P2_def 

  1085       by (rule tcopy_correct)

  1086   next

  1087     case B_halt (* of H *)

  1088     show "{P2} H {P3}"

  1089       unfolding P2_def P3_def 

  1090       using H_halt_inv[OF assms]

  1091       by (simp add: tape_of_nat_pair tape_of_nl_abv)

  1092   qed (simp)

  1093 

  1094   (* {P3} dither {P3} *)

  1095   have second: "{P3} dither {P3}" unfolding P3_def 

  1096     by (rule dither_halts)

  1097   

  1098   (* {P1} tcontra {P3} *)

  1099   have "{P1} tcontra {P3}" 

  1100     unfolding tcontra_def

  1101     by (rule Hoare_plus_halt[OF first second H_wf])

  1102 

  1103   with assms show "False"

  1104     unfolding P1_def P3_def

  1105     unfolding haltP_def

  1106     unfolding Hoare_halt_def 

  1107     apply(auto)    

  1108     apply(drule_tac x = n in spec)

  1109     apply(case_tac "steps0 (Suc 0, [], <code tcontra>) tcontra n")

  1110     apply(auto simp add: tape_of_nl_abv)

  1111     by (metis append_Nil2 replicate_0)

  1112 qed

  1113 

  1114 (* asumme tcontra halts on its code *)

  1115 lemma tcontra_halt: 

  1116   assumes "haltP tcontra [code tcontra]"

  1117   shows "False"

  1118 proof - 

  1119   (* invariants *)

  1120   def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <code_tcontra>)"

  1121   def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"

  1122   def Q3 \<equiv> "\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"

  1123 

  1124   (*

  1125   {P1} tcopy {P2}  {P2} H {Q3} 

  1126   ----------------------------

  1127      {P1} (tcopy |+| H) {Q3}     {Q3} dither loops

  1128   ------------------------------------------------

  1129                {P1} tcontra loops

  1130   *)

  1131 

  1132   have H_wf: "tm_wf0 (tcopy |+| H)" by auto

  1133 

  1134   (* {P1} (tcopy |+| H) {Q3} *)