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 (l, r) = (\<exists> i. l = Bk\<^bsup>i\<^esup> \<and> r = Oc\<^bsup>x\<^esup> @ Bk # Oc\<^bsup>x\<^esup>)"

    41 

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

    43   where

    44    "tcopy_F1 x (l, r) = (l = [] \<and> r = Oc\<^bsup>x\<^esup>)"

    45 

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

    47   where 

    48   "tcopy_F2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc\<^bsup>i\<^esup> \<and> r = Oc\<^bsup>j\<^esup>)"

    49 

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

    51   where

    52   "tcopy_F3 x (l, r) = (x > 0 \<and> l = Bk # Oc\<^bsup>x\<^esup> \<and> tl r = [])"

    53 

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

    55   where

    56   "tcopy_F4 x (l, r) = (x > 0 \<and> ((l = Oc\<^bsup>x\<^esup> \<and> r = [Bk, Oc]) \<or> (l = Oc\<^bsup>x - 1\<^esup> \<and> r = [Oc, Bk, Oc])))"

    57 

    58 fun tcopy_F5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"

    59   where

    60   "tcopy_F5_loop x (l, r) = 

    61        (\<exists> i j. i + j + 1 = x \<and> l = Oc\<^bsup>i\<^esup> \<and> r = Oc # Oc # Bk\<^bsup>j\<^esup> @ Oc\<^bsup>j\<^esup> \<and> j > 0)"

    62 

    63 fun tcopy_F5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"

    64   where

    65   "tcopy_F5_exit x (l, r) = 

    66       (l = [] \<and> r = Bk # Oc # Bk\<^bsup>x\<^esup> @ Oc\<^bsup>x\<^esup> \<and> x > 0 )"

    67 

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

    69   where

    70   "tcopy_F5 x (l, r) = (tcopy_F5_loop x (l, r) \<or> tcopy_F5_exit x (l, r))"

    71 

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

    73   where

    74   "tcopy_F6 x (l, r) = 

    75        (\<exists> i j any. i + j = x \<and> x > 0 \<and> i > 0 \<and> j > 0 \<and> l = Oc\<^bsup>i\<^esup> \<and> r = any#Bk\<^bsup>j\<^esup> @ Oc\<^bsup>j\<^esup>)"

    76 

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

    78   where

    79   "tcopy_F7 x (l, r) = 

    80          (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = Suc j \<and> l = Bk\<^bsup>k\<^esup> @ Oc\<^bsup>i\<^esup> \<and> r = Bk\<^bsup>t\<^esup> @ Oc\<^bsup>j\<^esup>)"

    81 

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

    83   where

    84   "tcopy_F8 x (l, r) = 

    85            (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = j \<and> l = Oc\<^bsup>k\<^esup> @ Bk\<^bsup>Suc j\<^esup> @ Oc\<^bsup>i\<^esup> \<and> r = Oc\<^bsup>t\<^esup>)"

    86 

    87 fun tcopy_F9_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"

    88 where

    89   "tcopy_F9_loop x (l, r) = 

    90           (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> t > 0\<and> l = Oc\<^bsup>k\<^esup> @ Bk\<^bsup>j\<^esup> @ Oc\<^bsup>i\<^esup> \<and> r = Oc\<^bsup>t\<^esup>)"

    91 

    92 fun tcopy_F9_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"

    93   where

    94   "tcopy_F9_exit x (l, r) = (\<exists> i j. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and>  l = Bk\<^bsup>j - 1\<^esup> @ Oc\<^bsup>i\<^esup> \<and> r = Bk # Oc\<^bsup>j\<^esup>)"

    95 

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

    97   where

    98   "tcopy_F9 x (l, r) = (tcopy_F9_loop x (l, r) \<or> 

    99                         tcopy_F9_exit x (l, r))"

   100 

   101 fun tcopy_F10_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   102   where

   103   "tcopy_F10_loop x (l, r) = 

   104      (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> k + t + 1 = j \<and> l = Bk\<^bsup>k\<^esup> @ Oc\<^bsup>i\<^esup> \<and> r = Bk\<^bsup>Suc t\<^esup> @ Oc\<^bsup>j\<^esup>)"

   105 

   106 fun tcopy_F10_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   107   where

   108   "tcopy_F10_exit x (l, r) = 

   109      (\<exists> i j. i + j = x \<and> j > 0 \<and> l =  Oc\<^bsup>i\<^esup> \<and> r = Oc # Bk\<^bsup>j\<^esup> @ Oc\<^bsup>j\<^esup>)"

   110 

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

   112   where

   113   "tcopy_F10 x (l, r) = (tcopy_F10_loop x (l, r) \<or> tcopy_F10_exit x (l, r))"

   114 

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

   116   where

   117   "tcopy_F11 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc # Bk\<^bsup>x\<^esup> @ Oc\<^bsup>x\<^esup>)"

   118 

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

   120   where

   121   "tcopy_F12 x (l, r) = (\<exists> i j. i + j = Suc x \<and> x > 0 \<and> l = Oc\<^bsup>i\<^esup> @ [Bk] \<and> r = Bk\<^bsup>j\<^esup> @ Oc\<^bsup>x\<^esup>)"

   122 

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

   124   where

   125   "tcopy_F13 x (l, r) =

   126         (\<exists> i j. x > 0 \<and> i + j = x \<and> l = Oc\<^bsup>i\<^esup> @ [Bk] \<and> r = Oc # Bk\<^bsup>j\<^esup> @ Oc\<^bsup>x\<^esup> )"

   127 

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

   129   where

   130   "tcopy_F14 x (l, r) = (\<exists> any. x > 0 \<and> l = Oc\<^bsup>x\<^esup> @ [Bk] \<and> r = any#Oc\<^bsup>x\<^esup>)"

   131 

   132 fun tcopy_F15_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   133   where

   134   "tcopy_F15_loop x (l, r) = 

   135          (\<exists> i j. i + j = x \<and> x > 0 \<and> j > 0 \<and> l = Oc\<^bsup>i\<^esup> @ [Bk] \<and> r = Oc\<^bsup>j\<^esup> @ Bk # Oc\<^bsup>x\<^esup>)"

   136 

   137 fun tcopy_F15_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   138   where

   139   "tcopy_F15_exit x (l, r) = (x > 0 \<and> l = [] \<and> r = Bk # Oc\<^bsup>x\<^esup> @ Bk # Oc\<^bsup>x\<^esup>)"

   140 

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

   142   where

   143   "tcopy_F15 x (l, r) = (tcopy_F15_loop x (l, r) \<or>  tcopy_F15_exit x (l, r))"

   144 

   145 text {*

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

   147 *}

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

   149   where

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

   151                     if state = 0 then tcopy_F0 x tp

   152                     else if state = 1 then tcopy_F1 x tp

   153                     else if state = 2 then tcopy_F2 x tp

   154                     else if state = 3 then tcopy_F3 x tp

   155                     else if state = 4 then tcopy_F4 x tp

   156                     else if state = 5 then tcopy_F5 x tp

   157                     else if state = 6 then tcopy_F6 x tp

   158                     else if state = 7 then tcopy_F7 x tp

   159                     else if state = 8 then tcopy_F8 x tp

   160                     else if state = 9 then tcopy_F9 x tp

   161                     else if state = 10 then tcopy_F10 x tp

   162                     else if state = 11 then tcopy_F11 x tp

   163                     else if state = 12 then tcopy_F12 x tp

   164                     else if state = 13 then tcopy_F13 x tp

   165                     else if state = 14 then tcopy_F14 x tp

   166                     else if state = 15 then tcopy_F15 x tp

   167                     else False)"

   168 declare tcopy_F0.simps [simp del]

   169         tcopy_F1.simps [simp del]

   170         tcopy_F2.simps [simp del]

   171         tcopy_F3.simps [simp del]

   172         tcopy_F4.simps [simp del]

   173         tcopy_F5.simps [simp del]

   174         tcopy_F6.simps [simp del]

   175         tcopy_F7.simps [simp del]

   176         tcopy_F8.simps [simp del]

   177         tcopy_F9.simps [simp del]

   178         tcopy_F10.simps [simp del]

   179         tcopy_F11.simps [simp del]

   180         tcopy_F12.simps [simp del]

   181         tcopy_F13.simps [simp del]

   182         tcopy_F14.simps [simp del]

   183         tcopy_F15.simps [simp del]

   184 

   185 lemma exp_zero_simp: "(a\<^bsup>b\<^esup> = []) = (b = 0)"

   186 apply(auto simp: exponent_def)

   187 done

   188 

   189 lemma exp_zero_simp2: "([] = a\<^bsup>b\<^esup> ) = (b = 0)"

   190 apply(auto simp: exponent_def)

   191 done

   192 

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

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

   195 done

   196 

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

   198                \<Longrightarrow> RR"

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

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

   201 done

   202 

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

   204                \<Longrightarrow> RR"

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

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

   207 done

   208 

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

   210               \<Longrightarrow> RR"

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

   212         split: block.splits list.splits)

   213 

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

   215              \<Longrightarrow> RR"

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

   217         split: block.splits list.splits)

   218 

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

   220              \<Longrightarrow> RR"

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

   222         split: block.splits list.splits)

   223 

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

   225              \<Longrightarrow> RR"

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

   227         split: block.splits list.splits)

   228 

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

   230              \<Longrightarrow> RR"

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

   232         split: block.splits list.splits)

   233 

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

   235              \<Longrightarrow> RR"

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

   237         split: block.splits list.splits)

   238 

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

   240              \<Longrightarrow> RR"

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

   242         split: block.splits list.splits)

   243 

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

   245              \<Longrightarrow> RR"

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

   247         split: block.splits list.splits)

   248 

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

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

   251         split: block.splits list.splits)

   252 

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

   254             \<Longrightarrow> RR"

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

   256         split: block.splits list.splits)

   257 

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

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

   260         split: block.splits list.splits)

   261 

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

   263             \<Longrightarrow> RR"

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

   265         split: block.splits list.splits)

   266 

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

   268             \<Longrightarrow> RR"

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

   270         split: block.splits list.splits)

   271 

   272 (*

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

   274 by auto

   275 

   276 lemma takeWhile2replicate: 

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

   278 apply(induct list)

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

   280 apply(auto)

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

   282 done

   283 

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

   285 by(simp)

   286 

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

   288 by simp

   289 

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

   291 by simp

   292 

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

   294 apply(rule rev_equal_rev)

   295 apply(simp only: rev_append rev_replicate_same)

   296 apply(auto)

   297 done

   298 

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

   300                                         replicate n b @ b # xs"

   301 apply(simp)

   302 done

   303 *)

   304 

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

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

   307 apply(auto simp: tstep.simps tcopy_def 

   308           tcopy_F14.simps tcopy_F15.simps fetch.simps new_tape.simps 

   309            split: if_splits list.splits block.splits)

   310 apply(erule_tac [!] x = "x - 1" in allE)

   311 apply(case_tac [!] x, simp_all add: exp_ind_def exp_zero)

   312 apply(erule_tac [!] x = "Suc 0" in allE, simp_all)

   313 done

   314 

   315 (*

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

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

   318 apply(induct xs)

   319 apply(auto)

   320 done

   321 *)

   322 (*

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

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

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

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

   327 done

   328 

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

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

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

   332       takeWhile_tail)

   333 apply(simp)

   334 done

   335 

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

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

   338 apply(induct xs)

   339 apply(simp+)

   340 done

   341 *)

   342 lemma false_case1:

   343   "\<lbrakk>Oc\<^bsup>j\<^esup> @ Bk # Oc\<^bsup>i + j\<^esup> = Oc # list;

   344   0 < i; 

   345   \<forall>ia. tl (Oc\<^bsup>i\<^esup> @ [Bk]) = Oc\<^bsup>ia\<^esup> @ [Bk] \<longrightarrow> (\<forall>ja. ia + ja = i + j 

   346   \<longrightarrow> hd (Oc\<^bsup>i\<^esup> @ [Bk]) # Oc # list \<noteq> Oc\<^bsup>ja\<^esup> @ Bk # Oc\<^bsup>i + j\<^esup>)\<rbrakk>

   347   \<Longrightarrow> RR"

   348 apply(case_tac i, auto simp: exp_ind_def)

   349 apply(erule_tac x = nat in allE, simp add:exp_ind_def)

   350 apply(erule_tac x = "Suc j" in allE, simp)

   351 done

   352 

   353 lemma false_case3:"\<forall>ja. ja \<noteq> i \<Longrightarrow> RR"

   354 by auto

   355 

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

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

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

   359                  tcopy_def fetch.simps new_tape.simps

   360             split: if_splits list.splits block.splits elim: false_case1)

   361 apply(case_tac [!] i, simp_all add: exp_zero exp_ind_def)

   362 apply(erule_tac [!] x = nat in allE, simp_all add: exp_ind_def)

   363 apply(auto elim: false_case3)

   364 done

   365 

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

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

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

   369                  tcopy_F14.simps fetch.simps new_tape.simps

   370            split: if_splits list.splits block.splits)

   371 done

   372 

   373 

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

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

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

   377                 tcopy_def tstep.simps fetch.simps new_tape.simps 

   378            split: if_splits list.splits block.splits)

   379 apply(case_tac [!] j, simp_all add: exp_zero exp_ind_def)

   380 done

   381 

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

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

   384 apply(auto simp:tcopy_F12.simps tcopy_F13.simps 

   385                    tcopy_def tstep.simps fetch.simps new_tape.simps

   386   split: if_splits list.splits block.splits)

   387 apply(case_tac x, simp_all add: exp_ind_def exp_zero)

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

   389 apply(rule_tac [!] x = "j - 1" in exI)

   390 apply(case_tac [!] j, simp_all add: exp_ind_def exp_zero)

   391 apply(case_tac x, simp_all add: exp_ind_def exp_zero)

   392 done

   393 

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

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

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

   397                    tcopy_def tstep.simps fetch.simps new_tape.simps)

   398 apply(auto)

   399 apply(rule_tac x = "Suc 0" in exI, 

   400   rule_tac x = x in exI, simp add: exp_ind_def exp_zero)

   401 done

   402 

   403 

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

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

   406 apply(auto simp:tcopy_F12.simps tcopy_F13.simps 

   407                    tcopy_def tstep.simps fetch.simps new_tape.simps

   408   split: if_splits list.splits block.splits)

   409 apply(rule_tac [!] x = "Suc i" in exI, simp_all add: exp_ind_def)

   410 done

   411 

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

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

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

   415                    tstep.simps fetch.simps new_tape.simps)

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

   417 done

   418 

   419 lemma F10_false: "tcopy_F10 x (b, []) = False"

   420 apply(auto simp: tcopy_F10.simps exp_ind_def)

   421 done

   422 

   423 lemma F10_false2: "tcopy_F10 x ([], Bk # list) = False"

   424 apply(auto simp:tcopy_F10.simps)

   425 apply(case_tac i, simp_all add: exp_ind_def exp_zero)

   426 done

   427  

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

   429 apply(auto simp: tcopy_F10.simps)

   430 done

   431 

   432 declare tcopy_F10_loop.simps[simp del]  tcopy_F10_exit.simps[simp del]

   433 

   434 lemma [simp]: "tcopy_F10_loop x (b, [Bk]) = False"

   435 apply(auto simp: tcopy_F10_loop.simps)

   436 apply(simp add: exp_ind_def)

   437 done

   438 

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

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

   441 apply(simp add: tcopy_def tstep.simps fetch.simps 

   442                 new_tape.simps exp_ind_def exp_zero_simp exp_zero_simp2 F10_false F10_false2

   443            split: if_splits list.splits block.splits)

   444 apply(simp add: tcopy_F10.simps del: tcopy_F10_loop.simps  tcopy_F10_exit.simps)

   445 apply(case_tac b, simp, case_tac aa)

   446 apply(rule_tac disjI1)

   447 apply(simp only: tcopy_F10_loop.simps)

   448 apply(erule_tac exE)+

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

   450       rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, simp)

   451 apply(case_tac k, simp_all add: exp_ind_def exp_zero)

   452 apply(case_tac i, simp_all add: exp_ind_def exp_zero)

   453 apply(rule_tac disjI2)

   454 apply(simp only: tcopy_F10_loop.simps tcopy_F10_exit.simps)

   455 apply(erule_tac exE)+

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

   457 apply(case_tac k, simp_all add: exp_ind_def exp_zero)

   458 apply(case_tac i, simp_all add: exp_ind_def exp_zero)

   459 apply(auto)

   460 apply(simp add: exp_ind_def)

   461 done

   462 

   463 (*

   464 lemma false_case4: "\<lbrakk>i + (k + t) = Suc x; 

   465         0 < i;

   466         Bk # list = Oc\<^bsup>t\<^esup>;

   467         \<forall>ia j. ia + j = Suc x \<longrightarrow> ia = 0 \<or> (\<forall>ka. tl (Oc\<^bsup>k\<^esup>) @ Bk\<^bsup>k + t\<^esup> @ Oc\<^bsup>i\<^esup> = Bk\<^bsup>ka\<^esup> @ Oc\<^bsup>ia\<^esup> \<longrightarrow> (\<forall>ta. Suc (ka + ta) = j \<longrightarrow> Oc # Oc\<^bsup>t\<^esup> \<noteq> Bk\<^bsup>Suc ta\<^esup> @ Oc\<^bsup>j\<^esup>));

   468         0 < k\<rbrakk>

   469        \<Longrightarrow> RR"

   470 apply(case_tac t, simp_all add: exp_ind_def exp_zero)

   471 done

   472 

   473 lemma false_case5: "

   474   \<lbrakk>Suc (i + nata) = x;

   475    0 < i;

   476    \<forall>ia j. ia + j = Suc x \<longrightarrow> ia = 0 \<or> (\<forall>k. Bk\<^bsup>nata\<^esup> @ Oc\<^bsup>i\<^esup> = Bk\<^bsup>k\<^esup> @ Oc\<^bsup>ia\<^esup> \<longrightarrow> (\<forall>t. Suc (k + t) = j \<longrightarrow> Bk # Oc # Oc # Oc\<^bsup>nata\<^esup> \<noteq> Bk\<^bsup>t\<^esup> @ Oc\<^bsup>j\<^esup>))\<rbrakk>

   477        \<Longrightarrow> False"

   478 apply(erule_tac x = i in allE, simp)

   479 apply(erule_tac x = "Suc (Suc nata)" in allE, simp)

   480 apply(erule_tac x = nata in allE, simp, simp add: exp_ind_def exp_zero)

   481 done

   482 

   483 lemma false_case6: "\<lbrakk>0 < x; \<forall>i. tl (Oc\<^bsup>x\<^esup>) = Oc\<^bsup>i\<^esup> \<longrightarrow> (\<forall>j. i + j = x \<longrightarrow> j = 0 \<or> [Bk, Oc] \<noteq> Bk\<^bsup>j\<^esup> @ Oc\<^bsup>j\<^esup>)\<rbrakk>

   484   \<Longrightarrow> False"

   485 apply(erule_tac x = "x - 1" in allE)

   486 apply(case_tac x, simp_all add: exp_ind_def exp_zero)

   487 apply(erule_tac x = "Suc 0" in allE, simp)

   488 done

   489 *)

   490 

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

   492 apply(auto simp: tcopy_F9.simps)

   493 apply(case_tac [!] i, simp_all add: exp_ind_def exp_zero)

   494 done

   495 

   496 lemma [simp]: "tcopy_F9 x (b, []) = False"

   497 apply(auto simp: tcopy_F9.simps)

   498 apply(case_tac [!] t, simp_all add: exp_ind_def exp_zero)

   499 done

   500 

   501 declare tcopy_F9_loop.simps[simp del] tcopy_F9_exit.simps[simp del]

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

   503 apply(auto simp: tcopy_F9_loop.simps)

   504 apply(case_tac [!] t, simp_all add: exp_ind_def exp_zero)

   505 done

   506 

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

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

   509 apply(auto simp:tcopy_def

   510                 tstep.simps fetch.simps new_tape.simps exp_zero_simp

   511                 exp_zero_simp2 

   512            split: if_splits list.splits block.splits)

   513 apply(case_tac "hd b", simp add:tcopy_F9.simps tcopy_F10.simps )

   514 apply(simp only: tcopy_F9_exit.simps tcopy_F10_loop.simps)

   515 apply(erule_tac exE)+

   516 apply(rule_tac x = i in exI, rule_tac x = j in exI, simp)

   517 apply(rule_tac x = "j - 2" in exI, simp add: exp_ind_def)

   518 apply(case_tac j, simp, simp)

   519 apply(case_tac nat, simp_all add: exp_zero exp_ind_def)

   520 apply(case_tac x, simp_all add: exp_ind_def exp_zero)

   521 apply(simp add: tcopy_F9.simps tcopy_F10.simps)

   522 apply(rule_tac disjI2)

   523 apply(simp only: tcopy_F10_exit.simps tcopy_F9_exit.simps)

   524 apply(erule_tac exE)+

   525 apply(simp)

   526 apply(case_tac j, simp_all, case_tac nat, simp_all add: exp_ind_def exp_zero)

   527 apply(case_tac x, simp_all add: exp_ind_def exp_zero)

   528 apply(rule_tac x = nata in exI, rule_tac x = 1 in exI, simp add: exp_ind_def exp_zero)

   529 done

   530 

   531 lemma false_case7:

   532   "\<lbrakk>i + (n + t) = x; 0 < i; 0 < t; Oc # list = Oc\<^bsup>t\<^esup>; k = Suc n;

   533         \<forall>j. i + j = Suc x \<longrightarrow> (\<forall>k. Oc\<^bsup>n\<^esup> @ Bk # Bk\<^bsup>n + t\<^esup> = Oc\<^bsup>k\<^esup> @ Bk\<^bsup>j\<^esup> \<longrightarrow>

   534          (\<forall>ta. k + ta = j \<longrightarrow> ta = 0 \<or> Oc # Oc\<^bsup>t\<^esup> \<noteq> Oc\<^bsup>ta\<^esup>))\<rbrakk>

   535        \<Longrightarrow> RR"

   536 apply(erule_tac x = "k + t" in allE, simp)

   537 apply(erule_tac x = n in allE, simp add: exp_ind_def)

   538 apply(erule_tac x = "Suc t" in allE, simp)

   539 done

   540 

   541 lemma false_case8: 

   542   "\<lbrakk>i + t = Suc x;

   543    0 < i;

   544     0 < t; 

   545     \<forall>ia j. tl (Bk\<^bsup>t\<^esup> @ Oc\<^bsup>i\<^esup>) = Bk\<^bsup>j - Suc 0\<^esup> @ Oc\<^bsup>ia\<^esup> \<longrightarrow> 

   546     ia + j = Suc x \<longrightarrow> ia = 0 \<or> j = 0 \<or> Oc\<^bsup>t\<^esup> \<noteq> Oc\<^bsup>j\<^esup>\<rbrakk> \<Longrightarrow> 

   547   RR"

   548 apply(erule_tac x = i in allE, simp)

   549 apply(erule_tac x = t in allE, simp)

   550 apply(case_tac t, simp_all add: exp_ind_def exp_zero)

   551 done

   552 

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

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

   555 apply(auto simp: tcopy_F9.simps tcopy_def 

   556                     tstep.simps fetch.simps new_tape.simps exp_zero_simp exp_zero_simp2

   557                     tcopy_F9_exit.simps tcopy_F9_loop.simps

   558   split: if_splits list.splits block.splits)

   559 apply(case_tac [!] k, simp_all add: exp_ind_def exp_zero)

   560 apply(erule_tac [!] x = i in allE, simp)

   561 apply(erule_tac false_case7, simp_all)+

   562 apply(case_tac t, simp_all add: exp_zero exp_ind_def)

   563 apply(erule_tac false_case7, simp_all)+

   564 apply(erule_tac false_case8, simp_all)

   565 apply(erule_tac false_case7, simp_all)+

   566 apply(case_tac t, simp_all add: exp_ind_def exp_zero)

   567 apply(erule_tac false_case7, simp_all)

   568 apply(erule_tac false_case8, simp_all)

   569 apply(erule_tac false_case7, simp_all)

   570 done

   571  

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

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

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

   575                 tstep.simps fetch.simps new_tape.simps tcopy_F9_loop.simps

   576                 tcopy_F9_exit.simps

   577   split: if_splits list.splits block.splits)

   578 apply(case_tac [!] t, simp_all add: exp_ind_def exp_zero)

   579 apply(rule_tac x = i in exI)

   580 apply(rule_tac x = "Suc k" in exI, simp)

   581 apply(rule_tac x = "k" in exI, simp add: exp_ind_def exp_zero)

   582 done

   583 

   584 

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

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

   587 apply(auto simp:tcopy_F8.simps tcopy_def tstep.simps 

   588                    fetch.simps new_tape.simps exp_zero_simp exp_zero split: if_splits list.splits 

   589                    

   590          block.splits)

   591 apply(rule_tac x = i in exI, rule_tac x = "k + t" in exI, simp)

   592 apply(rule_tac x = "Suc k" in exI, simp)

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

   594 apply(case_tac t, simp_all add: exp_zero exp_ind_def)

   595 done

   596 

   597 

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

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

   600 apply(auto simp:tcopy_F7.simps tcopy_def tstep.simps fetch.simps 

   601                 new_tape.simps exp_ind_def exp_zero_simp

   602            split: if_splits list.splits block.splits)

   603 apply(rule_tac x = i in exI)

   604 apply(rule_tac x = j in exI, simp)

   605 apply(rule_tac x = "Suc k" in exI, simp)

   606 apply(rule_tac x = "t - 1" in exI)

   607 apply(case_tac t, simp_all add: exp_zero exp_ind_def)

   608 apply(case_tac j, simp_all add: exp_zero exp_ind_def)

   609 done

   610 

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

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

   613 apply(auto simp:tcopy_F7.simps tcopy_def tstep.simps tcopy_F8.simps

   614                 fetch.simps new_tape.simps exp_zero_simp

   615   split: if_splits list.splits block.splits)

   616 apply(rule_tac x = i in exI, simp)

   617 apply(rule_tac x =  "Suc 0" in exI, simp add: exp_ind_def exp_zero)

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

   619 apply(case_tac t, simp_all add: exp_ind_def )

   620 apply(case_tac j, simp_all add: exp_ind_def exp_zero)

   621 done

   622 

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

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

   625 apply(case_tac x)

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

   627                 tcopy_def tstep.simps fetch.simps new_tape.simps exp_zero_simp

   628   split: if_splits list.splits block.splits)

   629 apply(case_tac i, simp_all add: exp_ind_def exp_zero)

   630 apply(rule_tac x = i in exI, simp)

   631 apply(rule_tac x = j in exI, simp)

   632 apply(rule_tac x = "Suc 0" in exI, simp add: exp_ind_def exp_zero)

   633 done

   634 

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

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

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

   638                 new_tape.simps fetch.simps

   639   split: if_splits list.splits block.splits)

   640 done

   641 

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

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

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

   645                 tstep.simps fetch.simps new_tape.simps exp_zero_simp2

   646   split: if_splits list.splits block.splits)

   647 apply(rule_tac x = "Suc 0" in exI, simp add: exp_ind_def exp_zero)

   648 apply(rule_tac x = "Suc i" in exI, simp add: exp_ind_def)

   649 done

   650 

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

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

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

   654                 tstep.simps fetch.simps new_tape.simps exp_zero_simp exp_zero_simp2

   655                 exp_ind_def tcopy_F10.simps tcopy_F10_loop.simps tcopy_F10_exit.simps

   656            split: if_splits list.splits block.splits )

   657 apply(erule_tac [!] x = "i - 1" in allE)

   658 apply(erule_tac [!] x = j in allE, simp_all)

   659 apply(case_tac [!] i, simp_all add: exp_ind_def)

   660 done

   661 

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

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

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

   665                 tstep.simps fetch.simps new_tape.simps exp_zero_simp exp_zero_simp2

   666            split: if_splits list.splits block.splits)

   667 apply(case_tac x, simp, simp add: exp_ind_def exp_zero)

   668 apply(erule_tac [!] x = "x - 2" in allE)

   669 apply(erule_tac [!] x = "Suc 0" in allE)

   670 apply(case_tac [!] x, simp_all add: exp_ind_def exp_zero)

   671 apply(case_tac [!] nat, simp_all add: exp_ind_def exp_zero)

   672 done

   673 

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

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

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

   677                 tcopy_def tstep.simps fetch.simps new_tape.simps

   678            split: if_splits list.splits block.splits)

   679 done

   680 

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

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

   683 apply(case_tac x)

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

   685                 tcopy_def tstep.simps fetch.simps new_tape.simps exp_zero_simp exp_zero_simp2 exp_ind_def

   686   split: if_splits list.splits block.splits)

   687 done

   688 

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

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

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

   692                 tcopy_def tstep.simps fetch.simps new_tape.simps 

   693   split: if_splits list.splits block.splits)

   694 done

   695 

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

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

   698 apply(case_tac x)

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

   700                 tcopy_def tstep.simps fetch.simps new_tape.simps

   701                 exp_zero_simp exp_zero_simp2 exp_zero

   702   split: if_splits list.splits block.splits)

   703 apply(case_tac [!] j, simp_all add: exp_zero exp_ind_def)

   704 done

   705 

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

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

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

   709                 tcopy_def tstep.simps fetch.simps new_tape.simps 

   710                 exp_zero_simp exp_zero_simp2 exp_zero

   711   split: if_splits list.splits block.splits)

   712 apply(rule_tac x = "Suc i" in exI, simp add: exp_ind_def exp_zero)

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

   714 apply(case_tac j, simp_all add: exp_ind_def exp_zero)

   715 done

   716 

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

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

   719 apply(auto simp:tcopy_F1.simps tcopy_F2.simps 

   720                 tcopy_def tstep.simps fetch.simps new_tape.simps 

   721                 exp_zero_simp exp_zero_simp2 exp_zero

   722              split: if_splits list.splits block.splits)

   723 apply(rule_tac x = "Suc 0" in exI, simp)

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

   725 apply(case_tac x, simp_all add: exp_ind_def exp_zero)

   726 done

   727 

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

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

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

   731                    tcopy_def tstep.simps fetch.simps new_tape.simps

   732                    exp_zero_simp exp_zero_simp2 exp_zero

   733          split: if_splits list.splits block.splits )

   734 apply(case_tac x, simp_all add: exp_ind_def exp_zero, auto)

   735 done

   736 

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

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

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

   740                  tcopy_def tstep.simps new_tape.simps fetch.simps

   741            split: if_splits list.splits block.splits)

   742 apply(rule_tac x = "Suc 0" in exI, simp add: exp_ind_def exp_zero)

   743 apply(case_tac [!] j, simp_all add: exp_ind_def exp_zero)

   744 done

   745 

   746 

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

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

   749 apply(case_tac x)

   750 apply(simp_all add: tcopy_F0.simps tcopy_def 

   751                     tstep.simps new_tape.simps fetch.simps)

   752 done

   753 

   754 declare tstep.simps[simp del]

   755 

   756 text {*

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

   758   the parital correctness of Copying TM.

   759 *}

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

   761 apply(induct c)

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

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

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

   765 done

   766 

   767 declare inv_tcopy.simps[simp del]

   768 

   769 text {*

   770   Invariant under mult-step execution.

   771   *}

   772 lemma inv_tcopy_steps: 

   773   "inv_tcopy x (steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy stp) "

   774 apply(induct stp)

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

   776                 tcopy_F1.simps inv_tcopy.simps)

   777 apply(drule_tac inv_tcopy_step, simp add: tstep_red)

   778 done

   779   

   780 

   781 

   782 

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

   784 

   785 section {*

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

   787   the termnation of Copying TM.

   788 *}

   789 

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

   791   where

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

   793 

   794 definition lex_triple :: 

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

   796   where

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

   798 

   799 definition lex_square :: 

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

   801   where

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

   803 

   804 lemma wf_lex_triple: "wf lex_triple"

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

   806 

   807 lemma wf_lex_square: "wf lex_square"

   808   by (auto intro:wf_lex_prod 

   809            simp:lex_triple_def lex_square_def lex_pair_def)

   810 

   811 text {*

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

   813 *}

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

   815   where

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

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

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

   819                     else if state = 11 then 3

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

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

   822                     else 0)" 

   823 

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

   825   where

   826   "tcopy_phase4_stage (ln, rn) = 

   827                    (let lrn = (rev ln) @ rn 

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

   829 

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

   831   where

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

   833                     if tcopy_phase c = 5 then 0

   834                     else if tcopy_phase c = 4 then 

   835                                tcopy_phase4_stage (ln, rn)

   836                     else if tcopy_phase c = 3 then 0

   837                     else if tcopy_phase c = 2 then length rn

   838                     else if tcopy_phase c = 1 then 0

   839                     else 0)"

   840 

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

   842   where

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

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

   845                            else if state = 5 then 1

   846                            else 12 - state)"

   847 

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

   849   where

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

   851                     if tcopy_phase c = 5 then 4 - state

   852                     else if tcopy_phase c = 4 then 

   853                          tcopy_phase4_state c

   854                     else if tcopy_phase c = 3 then 0

   855                     else if tcopy_phase c = 2 then 13 - state

   856                     else if tcopy_phase c = 1 then 15 - state

   857                     else 0)"

   858 

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

   860   where

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

   862 

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

   864   where

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

   866 

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

   868   where

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

   870 

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

   872   where

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

   874 

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

   876   where

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

   878 

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

   880   where

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

   882 

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

   884   where

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

   886 

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

   888   where

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

   890                             Oc \<Rightarrow> 1 |

   891                             Bk    \<Rightarrow> 0)"

   892 

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

   894   where

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

   896 

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

   898   where

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

   900              if state = 0 | state = 1 | state = 11 | 

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

   902                    else if state = 2 then tcopy_step2 c

   903                    else if state = 3 then tcopy_step3 c

   904                    else if state = 4 then tcopy_step4 c

   905                    else if state = 7 then tcopy_step7 c

   906                    else if state = 8 then tcopy_step8 c

   907                    else if state = 9 then tcopy_step9 c

   908                    else if state = 10 then tcopy_step10 c

   909                    else if state = 14 then tcopy_step14 c

   910                    else if state = 15 then tcopy_step15 c

   911                    else 0)"

   912 

   913 text {*

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

   915 *}

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

   917   where

   918   "tcopy_measure c = 

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

   920 

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

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

   923   where

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

   925 

   926 lemma wf_tcopy_le: "wf tcopy_LE"

   927 by(auto intro:wf_inv_image wf_lex_square simp:tcopy_LE_def)

   928 

   929 

   930 declare steps.simps[simp del] 

   931 

   932 declare tcopy_phase.simps[simp del] tcopy_stage.simps[simp del] 

   933         tcopy_state.simps[simp del] tcopy_step.simps[simp del] 

   934         inv_tcopy.simps[simp del]

   935 declare tcopy_F0.simps [simp]

   936         tcopy_F1.simps [simp]

   937         tcopy_F2.simps [simp]

   938         tcopy_F3.simps [simp]

   939         tcopy_F4.simps [simp]

   940         tcopy_F5.simps [simp]

   941         tcopy_F6.simps [simp]

   942         tcopy_F7.simps [simp]

   943         tcopy_F8.simps [simp]

   944         tcopy_F9.simps [simp]

   945         tcopy_F10.simps [simp]

   946         tcopy_F11.simps [simp]

   947         tcopy_F12.simps [simp]

   948         tcopy_F13.simps [simp]

   949         tcopy_F14.simps [simp]

   950         tcopy_F15.simps [simp]

   951         fetch.simps[simp]

   952         new_tape.simps[simp]

   953 lemma [elim]: "tcopy_F1 x (b, c) \<Longrightarrow> 

   954               (tstep (Suc 0, b, c) tcopy, Suc 0, b, c) \<in> tcopy_LE"

   955 apply(simp add: tcopy_F1.simps tstep.simps tcopy_def tcopy_LE_def 

   956   lex_square_def lex_triple_def lex_pair_def tcopy_phase.simps 

   957   tcopy_stage.simps tcopy_state.simps tcopy_step.simps)

   958 apply(simp split: if_splits list.splits block.splits taction.splits)

   959 done

   960 

   961 lemma [elim]: "tcopy_F2 x (b, c) \<Longrightarrow> 

   962               (tstep (2, b, c) tcopy, 2, b, c) \<in> tcopy_LE"

   963 apply(simp add:tstep.simps tcopy_def tcopy_LE_def lex_square_def 

   964   lex_triple_def lex_pair_def tcopy_phase.simps tcopy_stage.simps 

   965   tcopy_state.simps tcopy_step.simps)

   966 apply(simp split: if_splits list.splits block.splits taction.splits)

   967 done

   968 

   969 lemma [elim]: "tcopy_F3 x (b, c) \<Longrightarrow> 

   970              (tstep (3, b, c) tcopy, 3, b, c) \<in> tcopy_LE"

   971 apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def 

   972  lex_triple_def lex_pair_def tcopy_phase.simps tcopy_stage.simps 

   973  tcopy_state.simps tcopy_step.simps)

   974 apply(simp split: if_splits list.splits block.splits taction.splits)

   975 apply(auto)

   976 done

   977 

   978 lemma [elim]: "tcopy_F4 x (b, c) \<Longrightarrow> 

   979             (tstep (4, b, c) tcopy, 4, b, c) \<in> tcopy_LE"

   980 apply(case_tac x, simp)

   981 apply(simp add: tcopy_F4.simps tstep.simps tcopy_def tcopy_LE_def 

   982  lex_square_def lex_triple_def lex_pair_def tcopy_phase.simps 

   983  tcopy_stage.simps tcopy_state.simps tcopy_step.simps)

   984 apply(simp split: if_splits list.splits block.splits taction.splits)

   985 apply(auto simp: exp_ind_def)

   986 done

   987 

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

   989              replicate x b @ (takeWhile (\<lambda>a. a = b) ys)"

   990 apply(induct x)

   991 apply(simp+)

   992 done

   993 

   994 lemma [elim]: "tcopy_F5 x (b, c) \<Longrightarrow> 

   995               (tstep (5, b, c) tcopy, 5, b, c) \<in> tcopy_LE"

   996 apply(case_tac x, simp)

   997 apply(simp add: tstep.simps tcopy_def tcopy_LE_def 

   998         lex_square_def lex_triple_def lex_pair_def tcopy_phase.simps)

   999 apply(simp split: if_splits list.splits block.splits taction.splits)

  1000 apply(auto)

  1001 apply(simp_all add: tcopy_phase.simps 

  1002                     tcopy_stage.simps tcopy_state.simps)

  1003 done

  1004 

  1005 lemma [elim]: "\<lbrakk>replicate n x = []; n > 0\<rbrakk> \<Longrightarrow> RR"

  1006 apply(case_tac n, simp+)

  1007 done

  1008 

  1009 lemma [elim]: "tcopy_F6 x (b, c) \<Longrightarrow> 

  1010               (tstep (6, b, c) tcopy, 6, b, c) \<in> tcopy_LE"

  1011 apply(case_tac x, simp)

  1012 apply(simp add: tstep.simps tcopy_def tcopy_LE_def 

  1013                 lex_square_def lex_triple_def lex_pair_def 

  1014                 tcopy_phase.simps)

  1015 apply(simp split: if_splits list.splits block.splits taction.splits)

  1016 apply(auto)

  1017 apply(simp_all add: tcopy_phase.simps tcopy_stage.simps 

  1018                     tcopy_state.simps tcopy_step.simps exponent_def)

  1019 done

  1020 

  1021 lemma [elim]: "tcopy_F7 x (b, c) \<Longrightarrow> 

  1022              (tstep (7, b, c) tcopy, 7, b, c) \<in> tcopy_LE"

  1023 apply(case_tac x, simp)

  1024 apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def 

  1025                 lex_triple_def lex_pair_def tcopy_phase.simps)

  1026 apply(simp split: if_splits list.splits block.splits taction.splits)

  1027 apply(auto simp: exp_zero_simp)

  1028 apply(simp_all add: tcopy_phase.simps tcopy_stage.simps 

  1029                     tcopy_state.simps tcopy_step.simps)

  1030 done

  1031 

  1032 lemma [elim]: "tcopy_F8 x (b, c) \<Longrightarrow> 

  1033               (tstep (8, b, c) tcopy, 8, b, c) \<in> tcopy_LE"

  1034 apply(case_tac x, simp)

  1035 apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def 

  1036                 lex_triple_def lex_pair_def tcopy_phase.simps)

  1037 apply(simp split: if_splits list.splits block.splits taction.splits)

  1038 apply(auto simp: exp_zero_simp)

  1039 apply(simp_all add: tcopy_phase.simps tcopy_stage.simps 

  1040                     tcopy_state.simps tcopy_step.simps exponent_def)

  1041 done

  1042 

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

  1044 by simp

  1045 

  1046 lemma app_app_app_equal: "xs @ ys @ zs = (xs @ ys) @ zs"

  1047 by simp

  1048 

  1049 lemma append_cons_assoc: "as @ b # bs = (as @ [b]) @ bs"

  1050 apply(rule rev_equal_rev)

  1051 apply(simp)

  1052 done

  1053 

  1054 lemma rev_tl_hd_merge: "bs \<noteq> [] \<Longrightarrow> 

  1055                         rev (tl bs) @ hd bs # as = rev bs @ as"

  1056 apply(rule rev_equal_rev)

  1057 apply(simp)

  1058 done

  1059 

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

  1061              replicate x b @ (takeWhile (\<lambda>a. a = b) ys)"

  1062 apply(induct x)

  1063 apply(simp+)

  1064 done

  1065 

  1066 lemma [elim]: "tcopy_F9 x (b, c) \<Longrightarrow> 

  1067                       (tstep (9, b, c) tcopy, 9, b, c) \<in> tcopy_LE"

  1068 apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def 

  1069                 lex_triple_def lex_pair_def tcopy_phase.simps tcopy_F9.simps

  1070                 tcopy_F9_loop.simps tcopy_F9_exit.simps)

  1071 apply(simp split: if_splits list.splits block.splits taction.splits)

  1072 apply(auto)

  1073 apply(simp_all add: tcopy_phase.simps tcopy_stage.simps  tcopy_F9_loop.simps

  1074                     tcopy_state.simps tcopy_step.simps tstep.simps exp_zero_simp

  1075                     exponent_def)

  1076 apply(case_tac [1-2] t, simp_all add: rev_tl_hd_merge)

  1077 apply(case_tac j, simp, simp)

  1078 apply(case_tac nat, simp_all)

  1079 apply(case_tac nata, simp_all)

  1080 done

  1081 

  1082 lemma [elim]: "tcopy_F10 x (b, c) \<Longrightarrow> 

  1083               (tstep (10, b, c) tcopy, 10, b, c) \<in> tcopy_LE"

  1084 apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def 

  1085                 lex_triple_def lex_pair_def tcopy_phase.simps tcopy_F10_loop.simps

  1086                 tcopy_F10_exit.simps exp_zero_simp)

  1087 apply(simp split: if_splits list.splits block.splits taction.splits)

  1088 apply(auto simp: exp_zero_simp)

  1089 apply(simp_all add: tcopy_phase.simps tcopy_stage.simps 

  1090                     tcopy_state.simps tcopy_step.simps exponent_def

  1091                     rev_tl_hd_merge)

  1092 apply(case_tac k, simp_all)

  1093 apply(case_tac nat, simp_all)

  1094 done

  1095 

  1096 lemma [elim]: "tcopy_F11 x (b, c) \<Longrightarrow> 

  1097               (tstep (11, b, c) tcopy, 11, b, c) \<in> tcopy_LE"

  1098 apply(case_tac x, simp)

  1099 apply(simp add: tstep.simps tcopy_def tcopy_LE_def 

  1100                 lex_square_def lex_triple_def lex_pair_def 

  1101                 tcopy_phase.simps)

  1102 done

  1103 

  1104 lemma [elim]: "tcopy_F12 x (b, c) \<Longrightarrow> 

  1105               (tstep (12, b, c) tcopy, 12, b, c) \<in> tcopy_LE"

  1106 apply(case_tac x, simp)

  1107 apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def 

  1108                 lex_triple_def lex_pair_def tcopy_phase.simps)

  1109 apply(simp split: if_splits list.splits block.splits taction.splits)

  1110 apply(auto)

  1111 apply(simp_all add: tcopy_phase.simps tcopy_stage.simps 

  1112                     tcopy_state.simps tcopy_step.simps)

  1113 apply(simp_all add: exp_ind_def)

  1114 done

  1115 

  1116 lemma [elim]: "tcopy_F13 x (b, c) \<Longrightarrow> 

  1117               (tstep (13, b, c) tcopy, 13, b, c) \<in> tcopy_LE"

  1118 apply(case_tac x, simp)

  1119 apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def 

  1120                 lex_triple_def lex_pair_def tcopy_phase.simps)

  1121 apply(simp split: if_splits list.splits block.splits taction.splits)

  1122 apply(auto)

  1123 apply(simp_all add: tcopy_phase.simps tcopy_stage.simps 

  1124                     tcopy_state.simps tcopy_step.simps)

  1125 done

  1126 

  1127 lemma [elim]: "tcopy_F14 x (b, c) \<Longrightarrow> 

  1128              (tstep (14, b, c) tcopy, 14, b, c) \<in> tcopy_LE"

  1129 apply(case_tac x, simp)

  1130 apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def 

  1131                 lex_triple_def lex_pair_def tcopy_phase.simps)

  1132 apply(simp split: if_splits list.splits block.splits taction.splits)

  1133 apply(auto)

  1134 apply(simp_all add: tcopy_phase.simps tcopy_stage.simps 

  1135                     tcopy_state.simps tcopy_step.simps)