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

    10 begin

    11 

    12 text {*

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

    14 *}

    15 definition tcopy :: "tprog"

    16 where

    17 "tcopy \<equiv> [(W0, 0), (R, 2), (R, 3), (R, 2),

    18           (W1, 3), (L, 4), (L, 4), (L, 5), (R, 11), (R, 6), 

    19           (R, 7), (W0, 6), (R, 7), (R, 8), (W1, 9), (R, 8),

    20           (L, 10), (L, 9), (L, 10), (L, 5), (R, 12), (R, 12),

    21           (W1, 13), (L, 14), (R, 12), (R, 12), (L, 15), (W0, 14),

    22           (R, 0), (L, 15)]"

    23 

    24 text {*

    25   @{text "wipeLastBs tp"} removes all blanks at the end of tape @{text "tp"}.

    26 *}

    27 fun wipeLastBs :: "block list \<Rightarrow> block list"

    28   where 

    29   "wipeLastBs bl = rev (dropWhile (\<lambda>a. a = Bk) (rev bl))"

    30 

    31 fun isBk :: "block \<Rightarrow> bool"

    32   where

    33   "isBk b = (b = Bk)"

    34 

    35 text {*

    36   The following functions are used to expression invariants of {\em Copying} TM.

    37 *}

    38 fun tcopy_F0 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

    39   where

    40   "tcopy_F0 x tp = (let (ln, rn) = tp in 

    41            list_all isBk ln & rn = replicate x Oc 

    42                                    @ [Bk] @ replicate x Oc)"

    43 

    44 fun tcopy_F1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

    45   where

    46    "tcopy_F1 x (ln, rn) = (ln = [] & rn = replicate x Oc)"

    47 

    48 fun tcopy_F2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

    49   where

    50   "tcopy_F2 0 tp = False" |

    51   "tcopy_F2 (Suc x) (ln, rn) = (length ln > 0 & 

    52              ln @ rn = replicate (Suc x) Oc)"

    53 

    54 fun tcopy_F3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

    55   where

    56   "tcopy_F3 0 tp = False" |

    57   "tcopy_F3 (Suc x) (ln, rn) = 

    58             (ln = Bk # replicate (Suc x) Oc & length rn <= 1)"

    59 

    60 fun tcopy_F4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

    61   where

    62   "tcopy_F4 0 tp = False" | 

    63   "tcopy_F4 (Suc x) (ln, rn) = 

    64            ((ln = replicate x Oc & rn = [Oc, Bk, Oc])

    65            | (ln = replicate (Suc x) Oc & rn = [Bk, Oc])) "

    66 

    67 fun tcopy_F5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

    68   where

    69   "tcopy_F5 0 tp = False" |

    70   "tcopy_F5 (Suc x) (ln, rn) = 

    71         (if rn = [] then False 

    72          else if hd rn = Bk then (ln = [] & 

    73                    rn = Bk # (Oc # replicate (Suc x) Bk

    74                              @ replicate (Suc x) Oc))

    75          else if hd rn = Oc then 

    76            (\<exists>n. ln = replicate (x - n) Oc 

    77               & rn = Oc # (Oc # replicate n Bk @ replicate n Oc)

    78                & n > 0 & n <= x)

    79           else False)"

    80   

    81 

    82 fun tcopy_F6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

    83   where

    84   "tcopy_F6 0 tp = False" |

    85   "tcopy_F6 (Suc x) (ln, rn) = 

    86             (\<exists>n. ln = replicate (Suc x -n) Oc 

    87                      & tl rn = replicate n Bk @ replicate n Oc

    88              & n > 0 & n <= x)"

    89   

    90 fun tcopy_F7 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

    91   where

    92   "tcopy_F7 0 tp = False" |

    93   "tcopy_F7 (Suc x) (ln, rn) = 

    94             (let lrn = (rev ln) @ rn in 

    95             (\<exists>n. lrn = replicate ((Suc x) - n) Oc @

    96                         replicate (Suc n) Bk @ replicate n Oc

    97              & n > 0 & n <= x & 

    98                length rn >= n & length rn <= 2 * n ))"

    99                  

   100 fun tcopy_F8 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   101   where

   102   "tcopy_F8 0 tp = False" |

   103   "tcopy_F8 (Suc x) (ln, rn) = 

   104             (let lrn = (rev ln) @ rn in 

   105             (\<exists>n. lrn = replicate ((Suc x) - n) Oc @ 

   106                        replicate (Suc n) Bk @ replicate n Oc

   107                & n > 0 & n <= x & length rn < n)) "

   108 

   109 fun tcopy_F9 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   110   where

   111   "tcopy_F9 0 tp = False" | 

   112   "tcopy_F9 (Suc x) (ln, rn) =  

   113             (let lrn = (rev ln) @ rn in 

   114             (\<exists>n. lrn = replicate (Suc (Suc x) - n) Oc 

   115                             @ replicate n Bk @ replicate n Oc

   116              & n > Suc 0 & n <= Suc x & length rn > 0 

   117                     & length rn <= Suc n))"

   118 

   119 fun tcopy_F10 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   120   where

   121   "tcopy_F10 0 tp = False" |

   122   "tcopy_F10 (Suc x) (ln, rn) = 

   123            (let lrn = (rev ln) @ rn in 

   124              (\<exists>n. lrn = replicate (Suc (Suc x) - n) Oc

   125                    @ replicate n Bk @ replicate n Oc & n > Suc 0 

   126                 & n <= Suc x & length rn > Suc n & 

   127                   length rn <= 2*n + 1 ))"

   128 

   129 fun tcopy_F11 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   130   where

   131   "tcopy_F11 0 tp = False" |

   132   "tcopy_F11 (Suc x) (ln, rn) = 

   133             (ln = [Bk] & rn = Oc # replicate (Suc x) Bk 

   134                               @ replicate (Suc x) Oc)"

   135 

   136 fun tcopy_F12 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   137   where

   138   "tcopy_F12 0 tp = False" |

   139   "tcopy_F12 (Suc x) (ln, rn) =  

   140            (let lrn = ((rev ln) @ rn) in

   141            (\<exists>n. n > 0 & n <= Suc (Suc x) 

   142          & lrn = Bk # replicate n Oc @ replicate (Suc (Suc x) - n) Bk

   143                  @ replicate (Suc x) Oc 

   144          & length ln = Suc n))"

   145 

   146 fun tcopy_F13 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   147   where

   148   "tcopy_F13 0 tp = False" |

   149   "tcopy_F13 (Suc x) (ln, rn) =  

   150            (let lrn = ((rev ln) @ rn) in

   151            (\<exists>n. n > Suc 0 & n <= Suc (Suc x) 

   152          & lrn = Bk # replicate n Oc @ replicate (Suc (Suc x) - n) Bk

   153                  @ replicate (Suc x) Oc

   154          & length ln = n))"

   155           

   156 fun tcopy_F14 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   157   where

   158   "tcopy_F14 0 tp = False" |

   159   "tcopy_F14 (Suc x) (ln, rn) = 

   160              (ln = replicate (Suc x) Oc @ [Bk] & 

   161               tl rn = replicate (Suc x) Oc)"

   162 

   163 fun tcopy_F15 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   164   where

   165   "tcopy_F15 0 tp = False" |

   166   "tcopy_F15 (Suc x) (ln, rn) = 

   167             (let lrn = ((rev ln) @ rn) in

   168              lrn = Bk # replicate (Suc x) Oc @ [Bk] @ 

   169                    replicate (Suc x) Oc & length ln <= (Suc x))"

   170 

   171 text {*

   172   The following @{text "inv_tcopy"} is the invariant of the {\em Copying} TM.

   173 *}

   174 fun inv_tcopy :: "nat \<Rightarrow> t_conf \<Rightarrow> bool"

   175   where

   176   "inv_tcopy x c = (let (state, tp) = c in 

   177                     if state = 0 then tcopy_F0 x tp

   178                     else if state = 1 then tcopy_F1 x tp

   179                     else if state = 2 then tcopy_F2 x tp

   180                     else if state = 3 then tcopy_F3 x tp

   181                     else if state = 4 then tcopy_F4 x tp

   182                     else if state = 5 then tcopy_F5 x tp

   183                     else if state = 6 then tcopy_F6 x tp

   184                     else if state = 7 then tcopy_F7 x tp

   185                     else if state = 8 then tcopy_F8 x tp

   186                     else if state = 9 then tcopy_F9 x tp

   187                     else if state = 10 then tcopy_F10 x tp

   188                     else if state = 11 then tcopy_F11 x tp

   189                     else if state = 12 then tcopy_F12 x tp

   190                     else if state = 13 then tcopy_F13 x tp

   191                     else if state = 14 then tcopy_F14 x tp

   192                     else if state = 15 then tcopy_F15 x tp

   193                     else False)"

   194 declare tcopy_F0.simps [simp del]

   195         tcopy_F1.simps [simp del]

   196         tcopy_F2.simps [simp del]

   197         tcopy_F3.simps [simp del]

   198         tcopy_F4.simps [simp del]

   199         tcopy_F5.simps [simp del]

   200         tcopy_F6.simps [simp del]

   201         tcopy_F7.simps [simp del]

   202         tcopy_F8.simps [simp del]

   203         tcopy_F9.simps [simp del]

   204         tcopy_F10.simps [simp del]

   205         tcopy_F11.simps [simp del]

   206         tcopy_F12.simps [simp del]

   207         tcopy_F13.simps [simp del]

   208         tcopy_F14.simps [simp del]

   209         tcopy_F15.simps [simp del]

   210 

   211 lemma list_replicate_Bk[dest]: "list_all isBk list \<Longrightarrow> 

   212                             list = replicate (length list) Bk"

   213 apply(induct list)

   214 apply(simp+)

   215 done

   216 

   217 lemma [simp]: "dropWhile (\<lambda> a. a = b) (replicate x b @ ys) = 

   218                   dropWhile (\<lambda> a. a = b) ys"

   219 apply(induct x)

   220 apply(simp)

   221 apply(simp)

   222 done

   223 

   224 lemma [elim]: "\<lbrakk>tstep (0, a, b) tcopy = (s, l, r); s \<noteq> 0\<rbrakk> \<Longrightarrow> RR"

   225 apply(simp add: tstep.simps tcopy_def fetch.simps)

   226 done

   227 

   228 lemma [elim]: "\<lbrakk>tstep (Suc 0, a, b) tcopy = (s, l, r); s \<noteq> 0; s \<noteq> 2\<rbrakk>

   229                \<Longrightarrow> RR"

   230 apply(simp add: tstep.simps tcopy_def fetch.simps)

   231 apply(simp split: block.splits list.splits)

   232 done

   233 

   234 lemma [elim]: "\<lbrakk>tstep (2, a, b) tcopy = (s, l, r); s \<noteq> 2; s \<noteq> 3\<rbrakk>

   235                \<Longrightarrow> RR"

   236 apply(simp add: tstep.simps tcopy_def fetch.simps)

   237 apply(simp split: block.splits list.splits)

   238 done

   239 

   240 lemma [elim]: "\<lbrakk>tstep (3, a, b) tcopy = (s, l, r); s \<noteq> 3; s \<noteq> 4\<rbrakk> 

   241               \<Longrightarrow> RR"

   242 by(simp add: tstep.simps tcopy_def fetch.simps 

   243         split: block.splits list.splits)

   244 

   245 lemma [elim]: "\<lbrakk>tstep (4, a, b) tcopy = (s, l, r); s \<noteq> 4; s \<noteq> 5\<rbrakk> 

   246              \<Longrightarrow> RR"

   247 by(simp add: tstep.simps tcopy_def fetch.simps 

   248         split: block.splits list.splits)

   249 

   250 lemma [elim]: "\<lbrakk>tstep (5, a, b) tcopy = (s, l, r); s \<noteq> 6; s \<noteq> 11\<rbrakk> 

   251              \<Longrightarrow> RR"

   252 by(simp add: tstep.simps tcopy_def fetch.simps 

   253         split: block.splits list.splits)

   254 

   255 lemma [elim]: "\<lbrakk>tstep (6, a, b) tcopy = (s, l, r); s \<noteq> 6; s \<noteq> 7\<rbrakk> 

   256              \<Longrightarrow> RR"

   257 by(simp add: tstep.simps tcopy_def fetch.simps 

   258         split: block.splits list.splits)

   259 

   260 lemma [elim]: "\<lbrakk>tstep (7, a, b) tcopy = (s, l, r); s \<noteq> 7; s \<noteq> 8\<rbrakk> 

   261              \<Longrightarrow> RR"

   262 by(simp add: tstep.simps tcopy_def fetch.simps 

   263         split: block.splits list.splits)

   264 

   265 lemma [elim]: "\<lbrakk>tstep (8, a, b) tcopy = (s, l, r); s \<noteq> 8; s \<noteq> 9\<rbrakk> 

   266              \<Longrightarrow> RR"

   267 by(simp add: tstep.simps tcopy_def fetch.simps 

   268         split: block.splits list.splits)

   269 

   270 lemma [elim]: "\<lbrakk>tstep (9, a, b) tcopy = (s, l, r); s \<noteq> 9; s \<noteq> 10\<rbrakk> 

   271              \<Longrightarrow> RR"

   272 by(simp add: tstep.simps tcopy_def fetch.simps 

   273         split: block.splits list.splits)

   274 

   275 lemma [elim]: "\<lbrakk>tstep (10, a, b) tcopy = (s, l, r); s \<noteq> 10; s \<noteq> 5\<rbrakk> 

   276              \<Longrightarrow> RR"

   277 by(simp add: tstep.simps tcopy_def fetch.simps 

   278         split: block.splits list.splits)

   279 

   280 lemma [elim]: "\<lbrakk>tstep (11, a, b) tcopy = (s, l, r); s \<noteq> 12\<rbrakk> \<Longrightarrow> RR"

   281 by(simp add: tstep.simps tcopy_def fetch.simps 

   282         split: block.splits list.splits)

   283 

   284 lemma [elim]: "\<lbrakk>tstep (12, a, b) tcopy = (s, l, r); s \<noteq> 13; s \<noteq> 14\<rbrakk>

   285             \<Longrightarrow> RR"

   286 by(simp add: tstep.simps tcopy_def fetch.simps 

   287         split: block.splits list.splits)

   288 

   289 lemma [elim]: "\<lbrakk>tstep (13, a, b) tcopy = (s, l, r); s \<noteq> 12\<rbrakk> \<Longrightarrow> RR"

   290 by(simp add: tstep.simps tcopy_def fetch.simps 

   291         split: block.splits list.splits)

   292 

   293 lemma [elim]: "\<lbrakk>tstep (14, a, b) tcopy = (s, l, r); s \<noteq> 14; s \<noteq> 15\<rbrakk>  

   294             \<Longrightarrow> RR"

   295 by(simp add: tstep.simps tcopy_def fetch.simps 

   296         split: block.splits list.splits)

   297 

   298 lemma [elim]: "\<lbrakk>tstep (15, a, b) tcopy = (s, l, r); s \<noteq> 0; s \<noteq> 15\<rbrakk> 

   299             \<Longrightarrow> RR"

   300 by(simp add: tstep.simps tcopy_def fetch.simps 

   301         split: block.splits list.splits)

   302 

   303 lemma min_Suc4: "min (Suc (Suc x)) x = x"

   304 by auto

   305 

   306 lemma takeWhile2replicate: 

   307        "\<exists>n. takeWhile (\<lambda>a. a = b) list = replicate n b"

   308 apply(induct list)

   309 apply(rule_tac x = 0 in exI, simp)

   310 apply(auto)

   311 apply(rule_tac x = "Suc n" in exI, simp)

   312 done

   313 

   314 lemma rev_replicate_same: "rev (replicate x b) = replicate x b"

   315 by(simp)

   316 

   317 lemma rev_equal: "a = b \<Longrightarrow> rev a = rev b"

   318 by simp

   319 

   320 lemma rev_equal_rev: "rev a = rev b \<Longrightarrow> a = b"

   321 by simp

   322 

   323 lemma rep_suc_rev[simp]:"replicate n b @ [b] = replicate (Suc n) b"

   324 apply(rule rev_equal_rev)

   325 apply(simp only: rev_append rev_replicate_same)

   326 apply(auto)

   327 done

   328 

   329 lemma replicate_Cons_simp: "b # replicate n b @ xs = 

   330                                         replicate n b @ b # xs"

   331 apply(simp)

   332 done

   333 

   334 

   335 lemma [elim]: "\<lbrakk>tstep (14, b, c) tcopy = (15, ab, ba); 

   336                 tcopy_F14 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F15 x (ab, ba)"

   337 apply(case_tac x)

   338 apply(auto simp: tstep.simps tcopy_def 

   339           tcopy_F14.simps tcopy_F15.simps fetch.simps new_tape.simps 

   340            split: if_splits list.splits block.splits)

   341 done

   342 

   343 lemma dropWhile_drophd: "\<not> p a \<Longrightarrow> 

   344       (dropWhile p xs @ (a # as)) = (dropWhile p (xs @ [a]) @ as)"

   345 apply(induct xs)

   346 apply(auto)

   347 done

   348 

   349 lemma dropWhile_append3: "\<lbrakk>\<not> p a; 

   350   listall ((dropWhile p xs) @ [a]) isBk\<rbrakk> \<Longrightarrow> 

   351                listall (dropWhile p (xs @ [a])) isBk"

   352 apply(drule_tac p = p and xs = xs and a = a in dropWhile_drophd, simp)

   353 done

   354 

   355 lemma takeWhile_append3: "\<lbrakk>\<not>p a; (takeWhile p xs) = b\<rbrakk> 

   356                       \<Longrightarrow> takeWhile p (xs @ (a # as)) = b"

   357 apply(drule_tac P = p and xs = xs and x = a and l = as in 

   358       takeWhile_tail)

   359 apply(simp)

   360 done

   361 

   362 lemma listall_append: "list_all p (xs @ ys) = 

   363                         (list_all p xs \<and> list_all p ys)"

   364 apply(induct xs)

   365 apply(simp+)

   366 done

   367 

   368 lemma [elim]: "\<lbrakk>tstep (15, b, c) tcopy = (15, ab, ba); 

   369                 tcopy_F15 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F15 x (ab, ba)" 

   370 apply(case_tac x)

   371 apply(auto simp: tstep.simps tcopy_F15.simps

   372                  tcopy_def fetch.simps new_tape.simps

   373             split: if_splits list.splits block.splits)

   374 apply(case_tac b, simp+)

   375 done

   376 

   377 lemma [elim]: "\<lbrakk>tstep (14, b, c) tcopy = (14, ab, ba); 

   378                 tcopy_F14 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F14 x (ab, ba)"

   379 apply(case_tac x)

   380 apply(auto simp: tcopy_F14.simps tcopy_def tstep.simps 

   381                  tcopy_F14.simps fetch.simps new_tape.simps

   382            split: if_splits list.splits block.splits)

   383 done

   384 

   385 lemma [intro]: "list_all isBk (replicate x Bk)"

   386 apply(induct x, simp+)

   387 done

   388 

   389 lemma [elim]: "list_all isBk (dropWhile (\<lambda>a. a = Oc) b) \<Longrightarrow> 

   390                list_all isBk (dropWhile (\<lambda>a. a = Oc) (tl b))"

   391 apply(case_tac b, auto split: if_splits)

   392 apply(drule list_replicate_Bk)

   393 apply(case_tac "length list", auto)

   394 done

   395 

   396 lemma [elim]: "list_all (\<lambda> a. a = Oc) list \<Longrightarrow> 

   397                list = replicate (length list) Oc"

   398 apply(induct list)

   399 apply(simp+)

   400 done

   401 

   402 lemma append_length:  "\<lbrakk>as @ bs = cs @ ds; length bs = length ds\<rbrakk>

   403                     \<Longrightarrow> as = cs & bs = ds"

   404 apply(auto)

   405 done

   406 

   407 lemma Suc_elim: "Suc (Suc m) - n = Suc na \<Longrightarrow> Suc m - n = na"

   408 apply(simp)

   409 done

   410 

   411 lemma [elim]: "\<lbrakk>0 < n; n \<le> Suc (Suc na);

   412   rev b @ Oc # list = 

   413          Bk # replicate n Oc @ replicate (Suc (Suc na) - n) Bk @ 

   414          Oc # replicate na Oc;

   415   length b = Suc n; b \<noteq> []\<rbrakk>

   416        \<Longrightarrow> list_all isBk (dropWhile (\<lambda>a. a = Oc) (tl b))"

   417 apply(case_tac "rev b", auto)

   418 done

   419 

   420 lemma b_cons_same: "b#bs = replicate x a @ as \<Longrightarrow> a \<noteq> b \<longrightarrow> x = 0"

   421 apply(case_tac x, simp+)

   422 done

   423 

   424 lemma tcopy_tmp[elim]: 

   425   "\<lbrakk>0 < n; n \<le> Suc (Suc na); 

   426   rev b @ Oc # list = 

   427     Bk # replicate n Oc @ replicate (Suc (Suc na) - n) Bk 

   428     @ Oc # replicate na Oc; length b = Suc n; b \<noteq> []\<rbrakk>

   429    \<Longrightarrow> list = replicate na Oc"

   430 apply(case_tac "rev b", simp+)

   431 apply(auto)

   432 apply(frule b_cons_same, auto)

   433 done

   434 

   435 lemma [elim]: "\<lbrakk>tstep (12, b, c) tcopy = (14, ab, ba); 

   436                 tcopy_F12 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F14 x (ab, ba)" 

   437 apply(case_tac x)

   438 apply(auto simp:tcopy_F12.simps tcopy_F14.simps 

   439                 tcopy_def tstep.simps fetch.simps new_tape.simps 

   440            split: if_splits list.splits block.splits)

   441 apply(frule tcopy_tmp, simp+)

   442 apply(case_tac n, simp+)

   443 apply(case_tac nata, simp+)

   444 done

   445 

   446 lemma replicate_app_Cons: "replicate a b @ b # replicate c b 

   447                         = replicate (Suc (a + c)) b"

   448 apply(simp)

   449 apply(simp add: replicate_app_Cons_same)

   450 apply(simp only: replicate_add[THEN sym])

   451 done

   452 

   453 lemma replicate_same_exE_pref: "\<exists>x. bs @ (b # cs) = replicate x y

   454                             \<Longrightarrow> (\<exists>n. bs = replicate n y)"

   455 apply(induct bs)

   456 apply(rule_tac x = 0 in exI, simp)

   457 apply(drule impI)

   458 apply(erule impE)

   459 apply(erule exE, simp+)

   460 apply(case_tac x, auto)

   461 apply(case_tac x, auto)

   462 apply(rule_tac x = "Suc n" in exI, simp+)

   463 done

   464 

   465 lemma replicate_same_exE_inf: "\<exists>x. bs @ (b # cs) = replicate x y \<Longrightarrow> b = y"

   466 apply(induct bs, auto)

   467 apply(case_tac x, auto)

   468 apply(drule impI)

   469 apply(erule impE)

   470 apply(case_tac x, simp+)

   471 done

   472 

   473 lemma replicate_same_exE_suf: 

   474      "\<exists>x. bs @ (b # cs) = replicate x y \<Longrightarrow> \<exists>n. cs = replicate n y"

   475 apply(induct bs, auto)

   476 apply(case_tac x, simp+)

   477 apply(drule impI, erule impE)

   478 apply(case_tac x, simp+)

   479 done

   480 

   481 lemma replicate_same_exE: "\<exists>x. bs @ (b # cs) = replicate x y 

   482     \<Longrightarrow> (\<exists>n. bs = replicate n y) & (b = y) & (\<exists>m. cs = replicate m y)"

   483 apply(rule conjI)

   484 apply(drule  replicate_same_exE_pref, simp)

   485 apply(rule conjI)

   486 apply(drule replicate_same_exE_inf, simp)

   487 apply(drule replicate_same_exE_suf, simp)

   488 done

   489 

   490 lemma replicate_same: "bs @ (b # cs) = replicate x y

   491     \<Longrightarrow> (\<exists>n. bs = replicate n y) & (b = y) & (\<exists>m. cs = replicate m y)"

   492 apply(rule_tac replicate_same_exE)

   493 apply(rule_tac x = x in exI)

   494 apply(assumption)

   495 done

   496 

   497 lemma [elim]: "\<lbrakk> 0 < n; n \<le> Suc (Suc na);

   498     (rev ab @ Bk # list) = Bk # replicate n Oc 

   499    @ replicate (Suc (Suc na) - n) Bk @ Oc # replicate na Oc; ab \<noteq> []\<rbrakk>

   500     \<Longrightarrow> n \<le> Suc na"

   501 apply(rule contrapos_pp, simp+)

   502 apply(case_tac "rev ab", simp+)

   503 apply(auto)

   504 apply(simp only: replicate_app_Cons)

   505 apply(drule replicate_same)

   506 apply(auto)

   507 done

   508 

   509 

   510 lemma [elim]: "\<lbrakk>0 < n; n \<le> Suc (Suc na); 

   511    rev ab @ Bk # list = Bk # replicate n Oc @ 

   512     replicate (Suc (Suc na) - n) Bk @ Oc # replicate na Oc; 

   513    length ab = Suc n; ab \<noteq> []\<rbrakk>

   514     \<Longrightarrow> rev ab @ Oc # list = Bk # Oc # replicate n Oc @ 

   515                replicate (Suc na - n) Bk @ Oc # replicate na Oc"

   516 apply(case_tac "rev ab", simp+)

   517 apply(auto)

   518 apply(simp only: replicate_Cons_simp)

   519 apply(simp)

   520 apply(case_tac "Suc (Suc na) - n", simp+)

   521 done

   522 

   523 lemma [elim]: "\<lbrakk>tstep (12, b, c) tcopy = (13, ab, ba); 

   524                 tcopy_F12 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F13 x (ab, ba)"

   525 apply(case_tac x)

   526 apply(simp_all add:tcopy_F12.simps tcopy_F13.simps 

   527                    tcopy_def tstep.simps fetch.simps new_tape.simps)

   528 apply(simp split: if_splits list.splits block.splits)

   529 apply(auto)

   530 done

   531 

   532 

   533 lemma [elim]: "\<lbrakk>tstep (11, b, c) tcopy = (12, ab, ba); 

   534                 tcopy_F11 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F12 x (ab, ba)" 

   535 apply(case_tac x)

   536 apply(simp_all add:tcopy_F12.simps tcopy_F11.simps 

   537                    tcopy_def tstep.simps fetch.simps new_tape.simps)

   538 apply(auto)

   539 done

   540 

   541 lemma equal_length: "a = b \<Longrightarrow> length a = length b"

   542 by(simp)

   543 

   544 lemma [elim]: "\<lbrakk>tstep (13, b, c) tcopy = (12, ab, ba); 

   545                 tcopy_F13 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F12 x (ab, ba)"

   546 apply(case_tac x)

   547 apply(simp_all add:tcopy_F12.simps tcopy_F13.simps 

   548                    tcopy_def tstep.simps fetch.simps new_tape.simps)

   549 apply(simp split: if_splits list.splits block.splits)

   550 apply(auto)

   551 apply(drule equal_length, simp)

   552 done

   553 

   554 lemma [elim]: "\<lbrakk>tstep (5, b, c) tcopy = (11, ab, ba); 

   555                 tcopy_F5 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F11 x (ab, ba)" 

   556 apply(case_tac x)

   557 apply(simp_all add:tcopy_F11.simps tcopy_F5.simps tcopy_def 

   558                    tstep.simps fetch.simps new_tape.simps)

   559 apply(simp split: if_splits list.splits block.splits)

   560 done

   561 

   562 lemma less_equal: "\<lbrakk>length xs <= b; \<not> Suc (length xs) <= b\<rbrakk> \<Longrightarrow> 

   563                    length xs = b"

   564 apply(simp)

   565 done

   566 

   567 lemma length_cons_same: "\<lbrakk>xs @ b # ys = as @ bs; 

   568                  length ys = length bs\<rbrakk> \<Longrightarrow> xs @ [b] = as & ys = bs"

   569 apply(drule rev_equal)

   570 apply(simp)

   571 apply(auto)

   572 apply(drule rev_equal, simp)

   573 done

   574 

   575 lemma replicate_set_equal: "\<lbrakk> xs @ [a] = replicate n b; a \<noteq> b\<rbrakk> \<Longrightarrow> RR"

   576 apply(drule rev_equal, simp)

   577 apply(case_tac n, simp+)

   578 done

   579 

   580 lemma [elim]: "\<lbrakk>tstep (10, b, c) tcopy = (10, ab, ba); 

   581                 tcopy_F10 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F10 x (ab, ba)"

   582 apply(case_tac x)

   583 apply(auto simp:tcopy_F10.simps tcopy_def tstep.simps fetch.simps 

   584                 new_tape.simps

   585            split: if_splits list.splits block.splits)

   586 apply(rule_tac x = n in exI, auto)

   587 apply(case_tac b, simp+)

   588 apply(rule contrapos_pp, simp+)

   589 apply(frule less_equal, simp+)

   590 apply(drule length_cons_same, auto)

   591 apply(drule replicate_set_equal, simp+)

   592 done

   593 

   594 lemma less_equal2: "\<not> (n::nat) \<le> m \<Longrightarrow> \<exists>x. n = x + m & x > 0"

   595 apply(rule_tac x = "n - m" in exI)

   596 apply(auto)

   597 done

   598 

   599 lemma replicate_tail_length[dest]:

   600     "\<lbrakk>rev b @ Bk # list = xs @ replicate n Bk @ replicate n Oc\<rbrakk> 

   601  \<Longrightarrow> length list >= n"

   602 apply(rule contrapos_pp, simp+)

   603 apply(drule less_equal2, auto)

   604 apply(drule rev_equal)

   605 apply(simp add: replicate_add)

   606 apply(auto)

   607 apply(case_tac x, simp+)

   608 done

   609 

   610 

   611 lemma [elim]: "\<lbrakk>tstep (9, b, c) tcopy = (10, ab, ba); 

   612                 tcopy_F9 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F10 x (ab, ba)" 

   613 apply(case_tac x)

   614 apply(auto simp:tcopy_F10.simps tcopy_F9.simps tcopy_def

   615                 tstep.simps fetch.simps new_tape.simps 

   616            split: if_splits list.splits block.splits)

   617 apply(rule_tac x = n in exI, auto)

   618 apply(case_tac b, simp+)

   619 done

   620 

   621 lemma [elim]: "\<lbrakk>tstep (9, b, c) tcopy = (9, ab, ba); 

   622                 tcopy_F9 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F9 x (ab, ba)"

   623 apply(case_tac x)

   624 apply(simp_all add: tcopy_F9.simps tcopy_def 

   625                     tstep.simps fetch.simps new_tape.simps 

   626   split: if_splits list.splits block.splits)

   627 apply(rule_tac x = n in exI, auto)

   628 apply(case_tac b, simp+)

   629 apply(rule contrapos_pp, simp+)

   630 apply(drule less_equal, simp+)

   631 apply(drule rev_equal, auto)

   632 apply(case_tac "length list", simp+)

   633 done

   634 

   635 lemma app_cons_app_simp: "xs @ a # bs @ ys = (xs @ [a]) @ bs @ ys"

   636 apply(simp)

   637 done

   638 

   639 lemma [elim]: "\<lbrakk>tstep (8, b, c) tcopy = (9, ab, ba); 

   640                 tcopy_F8 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F9 x (ab, ba)" 

   641 apply(case_tac x)

   642 apply(auto simp:tcopy_F8.simps tcopy_F9.simps tcopy_def 

   643                 tstep.simps fetch.simps new_tape.simps

   644   split: if_splits list.splits block.splits)

   645 apply(rule_tac x = "Suc n" in exI, auto)

   646 apply(rule_tac x = "n" in exI, auto)

   647 apply(simp only: app_cons_app_simp)

   648 apply(frule replicate_tail_length, simp)

   649 done

   650 

   651 lemma [elim]: "\<lbrakk>tstep (8, b, c) tcopy = (8, ab, ba); 

   652                 tcopy_F8 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F8 x (ab, ba)"

   653 apply(case_tac x)

   654 apply(simp_all add:tcopy_F8.simps tcopy_def tstep.simps 

   655                    fetch.simps new_tape.simps)

   656 apply(simp split: if_splits list.splits block.splits)

   657 apply(rule_tac x = "n" in exI, auto)

   658 done

   659 

   660 lemma ex_less_more: "\<lbrakk>(x::nat) >= m ; x <= n\<rbrakk> \<Longrightarrow> 

   661                         \<exists>y. x = m + y & y <= n - m"

   662 by(rule_tac x = "x -m" in exI, auto)

   663 

   664 lemma replicate_split: "x <= n \<Longrightarrow> 

   665                       (\<exists>y. replicate n b = replicate (y + x) b)"

   666 apply(rule_tac x = "n - x" in exI)

   667 apply(simp)

   668 done

   669 

   670 lemma app_app_app_app_simp: "as @ bs @ cs @ ds = 

   671                              (as @ bs) @ (cs @ ds)"

   672 by simp

   673 

   674 lemma lengthtailsame_append_elim: 

   675      "\<lbrakk>as @ bs = cs @ ds; length bs = length ds\<rbrakk> \<Longrightarrow> bs = ds"

   676 apply(simp)

   677 done

   678 

   679 lemma rep_suc: "replicate (Suc n) x = replicate n x @ [x]" 

   680 by(induct n, auto)

   681 

   682 lemma length_append_diff_cons: 

   683  "\<lbrakk>b @ x # ba = xs @ replicate m y @ replicate n x; x \<noteq> y; 

   684    Suc (length ba) \<le> m + n\<rbrakk>

   685   \<Longrightarrow> length ba < n"

   686 apply(induct n arbitrary: ba, simp)

   687 apply(drule_tac b = y in replicate_split,

   688       simp add: replicate_add, erule exE, simp del: replicate.simps)

   689 proof -

   690   fix ba ya

   691   assume h1: 

   692      "b @ x # ba = xs @ y # replicate ya y @ replicate (length ba) y" 

   693     and h2: "x \<noteq> y"

   694   thus "False"  

   695     using append_eq_append_conv[of "b @ [x]" 

   696             "xs @ y # replicate ya y" "ba" "replicate (length ba) y"]

   697     apply(auto)

   698     apply(case_tac ya, simp, 

   699            simp add: rep_suc del: rep_suc_rev replicate.simps)

   700     done

   701 next

   702   fix n ba

   703   assume ind: "\<And>ba. \<lbrakk>b @ x # ba = xs @ replicate m y @ replicate n x;

   704                       x \<noteq> y; Suc (length ba) \<le> m + n\<rbrakk> 

   705                  \<Longrightarrow> length ba < n"

   706     and h1: "b @ x # ba = xs @ replicate m y @ replicate (Suc n) x" 

   707     and h2: "x \<noteq> y" and h3: "Suc (length ba) \<le> m + Suc n"

   708   show "length ba < Suc n"

   709   proof(cases "length ba")

   710     case 0 thus "?thesis" by simp

   711   next

   712     fix nat

   713     assume "length ba = Suc nat"

   714     hence "\<exists> ys a. ba = ys @ [a]"

   715       apply(rule_tac x = "butlast ba" in exI)

   716       apply(rule_tac x = "last ba" in exI)

   717       using append_butlast_last_id[of ba]

   718       apply(case_tac ba, auto)

   719       done

   720     from this obtain ys where "\<exists> a. ba = ys @ [a]" ..

   721     from this obtain a where "ba = ys @ [a]" ..

   722     thus "?thesis"

   723       using ind[of ys] h1 h2 h3

   724       apply(simp del: rep_suc_rev replicate.simps add: rep_suc)

   725       done

   726   qed

   727 qed

   728       

   729 lemma [elim]: 

   730   "\<lbrakk>b @ Oc # ba = xs @ Bk # replicate n Bk @ replicate n Oc;  

   731    Suc (length ba) \<le> 2 * n\<rbrakk>

   732   \<Longrightarrow> length ba < n"

   733   apply(rule_tac length_append_diff_cons[of b Oc ba xs "Suc n" Bk n])

   734   apply(simp, simp, simp)

   735   done

   736 

   737 lemma [elim]: "\<lbrakk>tstep (7, b, c) tcopy = (8, ab, ba); 

   738                 tcopy_F7 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F8 x (ab, ba)" 

   739 apply(case_tac x)

   740 apply(simp_all add:tcopy_F8.simps tcopy_F7.simps 

   741                    tcopy_def tstep.simps fetch.simps new_tape.simps)

   742 apply(simp split: if_splits list.splits block.splits)

   743 apply(rule_tac x = "n" in exI, auto)

   744 done

   745 

   746 lemma [elim]: "\<lbrakk>tstep (7, b, c) tcopy = (7, ab, ba); 

   747                 tcopy_F7 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F7 x (ab, ba)"

   748 apply(case_tac x)

   749 apply(auto simp:tcopy_F7.simps tcopy_def tstep.simps 

   750                 fetch.simps new_tape.simps

   751   split: if_splits list.splits block.splits)

   752 apply(rule_tac x = "n" in exI, auto)

   753 apply(simp only: app_cons_app_simp)

   754 apply(frule replicate_tail_length, simp)

   755 done

   756 

   757 lemma Suc_more: "n <= m \<Longrightarrow> Suc m - n = Suc (m - n)"

   758 by simp

   759 

   760 lemma [elim]: "\<lbrakk>tstep (6, b, c) tcopy = (7, ab, ba); 

   761                 tcopy_F6 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F7 x (ab, ba)" 

   762 apply(case_tac x)

   763 apply(auto simp:tcopy_F7.simps tcopy_F6.simps 

   764                 tcopy_def tstep.simps fetch.simps new_tape.simps

   765   split: if_splits list.splits block.splits)

   766 done

   767 

   768 lemma [elim]: "\<lbrakk>tstep (6, b, c) tcopy = (6, ab, ba); 

   769                 tcopy_F6 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F6 x (ab, ba)"

   770 apply(case_tac x)

   771 apply(auto simp:tcopy_F6.simps tcopy_def tstep.simps 

   772                 new_tape.simps fetch.simps

   773   split: if_splits list.splits block.splits)

   774 done

   775 

   776 lemma [elim]: "\<lbrakk>tstep (5, b, c) tcopy = (6, ab, ba); 

   777                 tcopy_F5 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F6 x (ab, ba)" 

   778 apply(case_tac x)

   779 apply(auto simp:tcopy_F5.simps tcopy_F6.simps tcopy_def 

   780                 tstep.simps fetch.simps new_tape.simps 

   781   split: if_splits list.splits block.splits)

   782 apply(rule_tac x = n in exI, simp)

   783 apply(rule_tac x = n in exI, simp)

   784 apply(drule Suc_more, simp)

   785 done

   786 

   787 lemma ex_less_more2: "\<lbrakk>(n::nat) < x ; x <= 2 * n\<rbrakk> \<Longrightarrow> 

   788                                \<exists>y. (x = n + y & y <= n)"

   789 apply(rule_tac x = "x - n" in exI)

   790 apply(auto)

   791 done

   792 

   793 lemma app_app_app_simp: "xs @ ys @ za = (xs @ ys) @ za"

   794 apply(simp)

   795 done

   796 

   797 lemma [elim]: "rev xs = replicate n b \<Longrightarrow> xs = replicate n b"

   798 using rev_replicate[of n b]

   799 thm rev_equal

   800 by(drule_tac rev_equal, simp)

   801 

   802 lemma app_cons_tail_same[dest]: 

   803   "\<lbrakk>rev b @ Oc # list = 

   804     replicate (Suc (Suc na) - n) Oc @ replicate n Bk @ replicate n Oc;

   805   Suc 0 < n; n \<le> Suc na; n < length list; length list \<le> 2 * n; b \<noteq> []\<rbrakk>

   806   \<Longrightarrow> list = replicate n Bk @ replicate n Oc 

   807            & b = replicate (Suc na - n) Oc"

   808 using length_append_diff_cons[of "rev b" Oc list 

   809                 "replicate (Suc (Suc na) - n) Oc" n Bk n]

   810 apply(case_tac "length list = 2*n", simp)

   811 using append_eq_append_conv[of "rev b @ [Oc]" "replicate 

   812       (Suc (Suc na) - n) Oc" "list" "replicate n Bk @ replicate n Oc"]

   813 apply(case_tac n, simp, simp add: Suc_more rep_suc 

   814                              del: rep_suc_rev replicate.simps, auto)

   815 done

   816 

   817 lemma hd_replicate_false1: "\<lbrakk>replicate x Oc \<noteq> [];

   818                              hd (replicate x Oc) = Bk\<rbrakk> \<Longrightarrow> RR"

   819 apply(case_tac x, auto)

   820 done

   821 

   822 lemma hd_replicate_false2: "\<lbrakk>replicate x Oc \<noteq> [];

   823                             hd (replicate x Oc) \<noteq> Oc\<rbrakk> \<Longrightarrow> RR"

   824 apply(case_tac x, auto)

   825 done

   826 

   827 lemma Suc_more_less: "\<lbrakk>n \<le> Suc m; n >= m\<rbrakk> \<Longrightarrow> n = m | n = Suc m"

   828 apply(auto)

   829 done

   830 

   831 lemma replicate_not_Nil: "replicate x a \<noteq> [] \<Longrightarrow> x > 0"

   832 apply(case_tac x, simp+)

   833 done

   834 

   835 lemma [elim]: "\<lbrakk>tstep (10, b, c) tcopy = (5, ab, ba); 

   836                 tcopy_F10 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F5 x (ab, ba)"

   837 apply(case_tac x)

   838 apply(auto simp:tcopy_F5.simps tcopy_F10.simps tcopy_def 

   839                 tstep.simps fetch.simps new_tape.simps

   840            split: if_splits list.splits block.splits)

   841 apply(frule app_cons_tail_same, simp+)

   842 apply(rule_tac x = n in exI, auto)

   843 done

   844 

   845 lemma [elim]: "\<lbrakk>tstep (4, b, c) tcopy = (5, ab, ba); 

   846                 tcopy_F4 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F5 x (ab, ba)" 

   847 apply(case_tac x)

   848 apply(auto simp:tcopy_F5.simps tcopy_F4.simps tcopy_def 

   849                 tstep.simps fetch.simps new_tape.simps

   850            split: if_splits list.splits block.splits)

   851 done

   852 

   853 lemma [elim]: "\<lbrakk>tstep (3, b, c) tcopy = (4, ab, ba); 

   854                 tcopy_F3 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F4 x (ab, ba)"

   855 apply(case_tac x)

   856 apply(auto simp:tcopy_F3.simps tcopy_F4.simps 

   857                 tcopy_def tstep.simps fetch.simps new_tape.simps

   858            split: if_splits list.splits block.splits)

   859 done

   860 

   861 lemma [elim]: "\<lbrakk>tstep (4, b, c) tcopy = (4, ab, ba);

   862                 tcopy_F4 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F4 x (ab, ba)" 

   863 apply(case_tac x)

   864 apply(auto simp:tcopy_F3.simps tcopy_F4.simps 

   865                 tcopy_def tstep.simps fetch.simps new_tape.simps

   866   split: if_splits list.splits block.splits)

   867 done

   868 

   869 lemma [elim]: "\<lbrakk>tstep (3, b, c) tcopy = (3, ab, ba); 

   870                 tcopy_F3 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F3 x (ab, ba)"

   871 apply(case_tac x)

   872 apply(auto simp:tcopy_F3.simps tcopy_F4.simps 

   873                 tcopy_def tstep.simps fetch.simps new_tape.simps 

   874   split: if_splits list.splits block.splits)

   875 done

   876 

   877 lemma replicate_cons_back: "y # replicate x y = replicate (Suc x) y"

   878 apply(simp)

   879 done

   880 

   881 lemma replicate_cons_same: "bs @ (b # cs) = y # replicate x y \<Longrightarrow> 

   882         (\<exists>n. bs = replicate n y) & (b = y) & (\<exists>m. cs = replicate m y)"

   883 apply(simp only: replicate_cons_back)

   884 apply(drule_tac replicate_same)

   885 apply(simp)

   886 done

   887 

   888 lemma [elim]: "\<lbrakk>tstep (2, b, c) tcopy = (3, ab, ba); 

   889                 tcopy_F2 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F3 x (ab, ba)" 

   890 apply(case_tac x)

   891 apply(auto simp:tcopy_F3.simps tcopy_F2.simps 

   892                 tcopy_def tstep.simps fetch.simps new_tape.simps

   893   split: if_splits list.splits block.splits)

   894 apply(drule replicate_cons_same, auto)+

   895 done

   896 

   897 lemma [elim]: "\<lbrakk>tstep (2, b, c) tcopy = (2, ab, ba); 

   898                 tcopy_F2 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F2 x (ab, ba)"

   899 apply(case_tac x)

   900 apply(auto simp:tcopy_F3.simps tcopy_F2.simps 

   901                 tcopy_def tstep.simps fetch.simps new_tape.simps

   902   split: if_splits list.splits block.splits)

   903 apply(frule replicate_cons_same, auto)

   904 apply(simp add: replicate_app_Cons_same)

   905 done

   906 

   907 lemma [elim]: "\<lbrakk>tstep (Suc 0, b, c) tcopy = (2, ab, ba); 

   908                 tcopy_F1 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F2 x (ab, ba)" 

   909 apply(case_tac x)

   910 apply(simp_all add:tcopy_F2.simps tcopy_F1.simps 

   911                    tcopy_def tstep.simps fetch.simps new_tape.simps)

   912 apply(auto)

   913 done

   914 

   915 lemma [elim]: "\<lbrakk>tstep (Suc 0, b, c) tcopy = (0, ab, ba); 

   916                 tcopy_F1 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F0 x (ab, ba)"

   917 apply(case_tac x)

   918 apply(simp_all add:tcopy_F0.simps tcopy_F1.simps 

   919                    tcopy_def tstep.simps fetch.simps new_tape.simps)

   920 done

   921 

   922 lemma ex_less: "Suc x <= y \<Longrightarrow> \<exists>z. y = x + z & z > 0"

   923 apply(rule_tac x = "y - x" in exI, auto)

   924 done

   925 

   926 lemma [elim]: "\<lbrakk>xs @ Bk # ba = 

   927   Bk # Oc # replicate n Oc @ Bk # Oc # replicate n Oc; 

   928   length xs \<le> Suc n; xs \<noteq> []\<rbrakk> \<Longrightarrow> RR"

   929 apply(case_tac xs, auto)

   930 apply(case_tac list, auto)

   931 apply(drule ex_less, auto)

   932 apply(simp add: replicate_add)

   933 apply(auto)

   934 apply(case_tac z, simp+)

   935 done

   936 

   937 lemma [elim]: "\<lbrakk>tstep (15, b, c) tcopy = (0, ab, ba); 

   938                 tcopy_F15 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F0 x (ab, ba)"

   939 apply(case_tac x)

   940 apply(auto simp: tcopy_F15.simps tcopy_F0.simps 

   941                  tcopy_def tstep.simps new_tape.simps fetch.simps

   942            split: if_splits list.splits block.splits)

   943 done

   944 

   945 lemma [elim]: "\<lbrakk>tstep (0, b, c) tcopy = (0, ab, ba); 

   946                 tcopy_F0 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F0 x (ab, ba)" 

   947 apply(case_tac x)

   948 apply(simp_all add: tcopy_F0.simps tcopy_def 

   949                     tstep.simps new_tape.simps fetch.simps)

   950 done

   951 

   952 declare tstep.simps[simp del]

   953 

   954 text {*

   955   Finally establishes the invariant of Copying TM, which is used to dervie 

   956   the parital correctness of Copying TM.

   957 *}

   958 lemma inv_tcopy_step:"inv_tcopy x c \<Longrightarrow> inv_tcopy x (tstep c tcopy)"

   959 apply(induct c)

   960 apply(auto split: if_splits block.splits list.splits taction.splits)

   961 apply(auto simp: tstep.simps tcopy_def fetch.simps new_tape.simps 

   962   split: if_splits list.splits block.splits taction.splits)

   963 done

   964 

   965 declare inv_tcopy.simps[simp del]

   966 

   967 text {*

   968   Invariant under mult-step execution.

   969   *}

   970 lemma inv_tcopy_steps: 

   971   "inv_tcopy x (steps (Suc 0, [], replicate x Oc) tcopy stp) "

   972 apply(induct stp)

   973 apply(simp add: tstep.simps tcopy_def steps.simps 

   974                 tcopy_F1.simps inv_tcopy.simps)

   975 apply(drule_tac inv_tcopy_step, simp add: tstep_red)

   976 done

   977   

   978 

   979 text {*

   980   The followng lemmas gives the parital correctness of Copying TM.

   981 *}

   982 theorem inv_tcopy_rs: 

   983   "steps (Suc 0, [], replicate x Oc) tcopy stp = (0, l, r)

   984   \<Longrightarrow> \<exists> n. l = replicate n Bk \<and> 

   985            r = replicate x Oc @ Bk # replicate x Oc"

   986 apply(insert inv_tcopy_steps[of x stp])

   987 apply(auto simp: inv_tcopy.simps tcopy_F0.simps isBk.simps)

   988 done

   989 

   990 

   991 

   992 

   993 (*----------halt problem of tcopy----------------------------------------*)

   994 

   995 section {*

   996   The following definitions are used to construct the measure function used to show

   997   the termnation of Copying TM.

   998 *}

   999 

  1000 definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set"

  1001   where

  1002   "lex_pair \<equiv> less_than <*lex*> less_than"

  1003 

  1004 definition lex_triple :: 

  1005  "((nat \<times> (nat \<times> nat)) \<times> (nat \<times> (nat \<times> nat))) set"

  1006   where

  1007 "lex_triple \<equiv> less_than <*lex*> lex_pair"

  1008 

  1009 definition lex_square :: 

  1010   "((nat \<times> nat \<times> nat \<times> nat) \<times> (nat \<times> nat \<times> nat \<times> nat)) set"

  1011   where

  1012 "lex_square \<equiv> less_than <*lex*> lex_triple"

  1013 

  1014 lemma wf_lex_triple: "wf lex_triple"

  1015   by (auto intro:wf_lex_prod simp:lex_triple_def lex_pair_def)

  1016 

  1017 lemma wf_lex_square: "wf lex_square"

  1018   by (auto intro:wf_lex_prod 

  1019            simp:lex_triple_def lex_square_def lex_pair_def)

  1020 

  1021 text {*

  1022   A measurement functions used to show the termination of copying machine:

  1023 *}

  1024 fun tcopy_phase :: "t_conf \<Rightarrow> nat"

  1025   where

  1026   "tcopy_phase c = (let (state, tp) = c in

  1027                     if state > 0 & state <= 4 then 5

  1028                     else if state >=5 & state <= 10 then 4

  1029                     else if state = 11 then 3

  1030                     else if state = 12 | state = 13 then 2

  1031                     else if state = 14 | state = 15 then 1

  1032                     else 0)" 

  1033 

  1034 fun tcopy_phase4_stage :: "tape \<Rightarrow> nat"

  1035   where

  1036   "tcopy_phase4_stage (ln, rn) = 

  1037                    (let lrn = (rev ln) @ rn 

  1038                     in length (takeWhile (\<lambda>a. a = Oc) lrn))"

  1039 

  1040 fun tcopy_stage :: "t_conf \<Rightarrow> nat"

  1041   where

  1042   "tcopy_stage c = (let (state, ln, rn) = c in 

  1043                     if tcopy_phase c = 5 then 0

  1044                     else if tcopy_phase c = 4 then 

  1045                                tcopy_phase4_stage (ln, rn)

  1046                     else if tcopy_phase c = 3 then 0

  1047                     else if tcopy_phase c = 2 then length rn

  1048                     else if tcopy_phase c = 1 then 0

  1049                     else 0)"

  1050 

  1051 fun tcopy_phase4_state :: "t_conf \<Rightarrow> nat"

  1052   where

  1053   "tcopy_phase4_state c = (let (state, ln, rn) = c in

  1054                            if state = 6 & hd rn = Oc then 0

  1055                            else if state = 5 then 1

  1056                            else 12 - state)"

  1057 

  1058 fun tcopy_state :: "t_conf \<Rightarrow> nat"

  1059   where

  1060   "tcopy_state c = (let (state, ln, rn) = c in

  1061                     if tcopy_phase c = 5 then 4 - state

  1062                     else if tcopy_phase c = 4 then 

  1063                          tcopy_phase4_state c

  1064                     else if tcopy_phase c = 3 then 0

  1065                     else if tcopy_phase c = 2 then 13 - state

  1066                     else if tcopy_phase c = 1 then 15 - state

  1067                     else 0)"

  1068 

  1069 fun tcopy_step2 :: "t_conf \<Rightarrow> nat"

  1070   where

  1071   "tcopy_step2 (s, l, r) = length r"

  1072 

  1073 fun tcopy_step3 :: "t_conf \<Rightarrow> nat"

  1074   where

  1075   "tcopy_step3 (s, l, r) = (if r = [] | r = [Bk] then Suc 0 else 0)"

  1076 

  1077 fun tcopy_step4 :: "t_conf \<Rightarrow> nat"

  1078   where

  1079   "tcopy_step4 (s, l, r) = length l"

  1080 

  1081 fun tcopy_step7 :: "t_conf \<Rightarrow> nat"

  1082   where

  1083   "tcopy_step7 (s, l, r) = length r"

  1084 

  1085 fun tcopy_step8 :: "t_conf \<Rightarrow> nat"

  1086   where

  1087   "tcopy_step8 (s, l, r) = length r"

  1088 

  1089 fun tcopy_step9 :: "t_conf \<Rightarrow> nat"

  1090   where

  1091   "tcopy_step9 (s, l, r) = length l"

  1092 

  1093 fun tcopy_step10 :: "t_conf \<Rightarrow> nat"

  1094   where

  1095   "tcopy_step10 (s, l, r) = length l"

  1096 

  1097 fun tcopy_step14 :: "t_conf \<Rightarrow> nat"

  1098   where

  1099   "tcopy_step14 (s, l, r) = (case hd r of 

  1100                             Oc \<Rightarrow> 1 |

  1101                             Bk    \<Rightarrow> 0)"

  1102 

  1103 fun tcopy_step15 :: "t_conf \<Rightarrow> nat"

  1104   where

  1105   "tcopy_step15 (s, l, r) = length l"

  1106 

  1107 fun tcopy_step :: "t_conf \<Rightarrow> nat"

  1108   where

  1109   "tcopy_step c = (let (state, ln, rn) = c in

  1110              if state = 0 | state = 1 | state = 11 | 

  1111                 state = 5 | state = 6 | state = 12 | state = 13 then 0

  1112                    else if state = 2 then tcopy_step2 c

  1113                    else if state = 3 then tcopy_step3 c

  1114                    else if state = 4 then tcopy_step4 c

  1115                    else if state = 7 then tcopy_step7 c

  1116                    else if state = 8 then tcopy_step8 c

  1117                    else if state = 9 then tcopy_step9 c

  1118                    else if state = 10 then tcopy_step10 c

  1119                    else if state = 14 then tcopy_step14 c

  1120                    else if state = 15 then tcopy_step15 c

  1121                    else 0)"

  1122 

  1123 text {*

  1124   The measure function used to show the termination of Copying TM.

  1125 *}

  1126 fun tcopy_measure :: "t_conf \<Rightarrow> (nat * nat * nat * nat)"

  1127   where

  1128   "tcopy_measure c = 

  1129    (tcopy_phase c, tcopy_stage c, tcopy_state c, tcopy_step c)"

  1130 

  1131 definition tcopy_LE :: "((nat \<times> block list \<times> block list) \<times> 

  1132                         (nat \<times> block list \<times> block list)) set"

  1133   where

  1134    "tcopy_LE \<equiv> (inv_image lex_square tcopy_measure)"

  1135