1 theory UTM

     2 imports Main uncomputable recursive abacus UF GCD 

     3 begin

     4 

     5 section {* Wang coding of input arguments *}

     6 

     7 text {*

     8   The direct compilation of the universal function @{text "rec_F"} can not give us UTM, because @{text "rec_F"} is of arity 2,

     9   where the first argument represents the Godel coding of the TM being simulated and the second argument represents the right number (in Wang's coding) of the TM tape. 

    10   (Notice, left number is always @{text "0"} at the very beginning). However, UTM needs to simulate the execution of any TM which may

    11   very well take many input arguments. Therefore, a initialization TM needs to run before the TM compiled from @{text "rec_F"}, and the sequential 

    12   composition of these two TMs will give rise to the UTM we are seeking. The purpose of this initialization TM is to transform the multiple 

    13   input arguments of the TM being simulated into Wang's coding, so that it can be consumed by the TM compiled from @{text "rec_F"} as the second

    14   argument. 

    15 

    16   However, this initialization TM (named @{text "t_wcode"}) can not be constructed by compiling from any resurve function, because every recursive 

    17   function takes a fixed number of input arguments, while @{text "t_wcode"} needs to take varying number of arguments and tranform them into 

    18   Wang's coding. Therefore, this section give a direct construction of @{text "t_wcode"} with just some parts being obtained from recursive functions.

    19 *}

    20 

    21 definition rec_twice :: "recf"

    22   where

    23   "rec_twice = Cn 1 rec_mult [id 1 0, constn 2]"

    24 

    25 definition rec_fourtimes  :: "recf"

    26   where

    27   "rec_fourtimes = Cn 1 rec_mult [id 1 0, constn 4]"

    28 

    29 definition abc_twice :: "abc_prog"

    30   where

    31   "abc_twice = (let (aprog, ary, fp) = rec_ci rec_twice in 

    32                        aprog [+] dummy_abc ((Suc 0)))"

    33 

    34 definition abc_fourtimes :: "abc_prog"

    35   where

    36   "abc_fourtimes = (let (aprog, ary, fp) = rec_ci rec_fourtimes in 

    37                        aprog [+] dummy_abc ((Suc 0)))"

    38 

    39 definition twice_ly :: "nat list"

    40   where

    41   "twice_ly = layout_of abc_twice"

    42 

    43 definition fourtimes_ly :: "nat list"

    44   where

    45   "fourtimes_ly = layout_of abc_fourtimes"

    46 

    47 definition t_twice :: "tprog"

    48   where

    49   "t_twice = change_termi_state (tm_of (abc_twice) @ (tMp 1 (start_of twice_ly (length abc_twice) - Suc 0)))"

    50 

    51 definition t_fourtimes :: "tprog"

    52   where

    53   "t_fourtimes = change_termi_state (tm_of (abc_fourtimes) @ 

    54              (tMp 1 (start_of fourtimes_ly (length abc_fourtimes) - Suc 0)))"

    55 

    56 

    57 definition t_twice_len :: "nat"

    58   where

    59   "t_twice_len = length t_twice div 2"

    60 

    61 definition t_wcode_main_first_part:: "tprog"

    62   where

    63   "t_wcode_main_first_part \<equiv> 

    64                    [(L, 1), (L, 2), (L, 7), (R, 3),

    65                     (R, 4), (W0, 3), (R, 4), (R, 5),

    66                     (W1, 6), (R, 5), (R, 13), (L, 6),

    67                     (R, 0), (R, 8), (R, 9), (Nop, 8),

    68                     (R, 10), (W0, 9), (R, 10), (R, 11), 

    69                     (W1, 12), (R, 11), (R, t_twice_len + 14), (L, 12)]"

    70 

    71 definition t_wcode_main :: "tprog"

    72   where

    73   "t_wcode_main = (t_wcode_main_first_part @ tshift t_twice 12 @ [(L, 1), (L, 1)]

    74                     @ tshift t_fourtimes (t_twice_len + 13) @ [(L, 1), (L, 1)])"

    75 

    76 fun bl_bin :: "block list \<Rightarrow> nat"

    77   where

    78   "bl_bin [] = 0" 

    79 | "bl_bin (Bk # xs) = 2 * bl_bin xs"

    80 | "bl_bin (Oc # xs) = Suc (2 * bl_bin xs)"

    81 

    82 declare bl_bin.simps[simp del]

    83 

    84 type_synonym bin_inv_t = "block list \<Rightarrow> nat \<Rightarrow> tape \<Rightarrow> bool"

    85 

    86 fun wcode_before_double :: "bin_inv_t"

    87   where

    88   "wcode_before_double ires rs (l, r) =

    89      (\<exists> ln rn. l = Bk # Bk # Bk\<^bsup>ln\<^esup> @ Oc # ires \<and> 

    90                r = Oc\<^bsup>(Suc (Suc rs))\<^esup> @ Bk\<^bsup>rn \<^esup>)"

    91 

    92 declare wcode_before_double.simps[simp del]

    93 

    94 fun wcode_after_double :: "bin_inv_t"

    95   where

    96   "wcode_after_double ires rs (l, r) = 

    97      (\<exists> ln rn. l = Bk # Bk # Bk\<^bsup>ln\<^esup> @ Oc # ires \<and>

    98          r = Oc\<^bsup>Suc (Suc (Suc 2*rs))\<^esup> @ Bk\<^bsup>rn\<^esup>)"

    99 

   100 declare wcode_after_double.simps[simp del]

   101 

   102 fun wcode_on_left_moving_1_B :: "bin_inv_t"

   103   where

   104   "wcode_on_left_moving_1_B ires rs (l, r) = 

   105      (\<exists> ml mr rn. l = Bk\<^bsup>ml\<^esup> @ Oc # Oc # ires \<and> 

   106                r = Bk\<^bsup>mr\<^esup> @ Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>rn\<^esup> \<and>

   107                ml + mr > Suc 0 \<and> mr > 0)"

   108 

   109 declare wcode_on_left_moving_1_B.simps[simp del]

   110 

   111 fun wcode_on_left_moving_1_O :: "bin_inv_t"

   112   where

   113   "wcode_on_left_moving_1_O ires rs (l, r) = 

   114      (\<exists> ln rn.

   115                l = Oc # ires \<and> 

   116                r = Oc # Bk\<^bsup>ln\<^esup> @ Bk # Bk # Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>rn\<^esup>)"

   117 

   118 declare wcode_on_left_moving_1_O.simps[simp del]

   119 

   120 fun wcode_on_left_moving_1 :: "bin_inv_t"

   121   where

   122   "wcode_on_left_moving_1 ires rs (l, r) = 

   123           (wcode_on_left_moving_1_B ires rs (l, r) \<or> wcode_on_left_moving_1_O ires rs (l, r))"

   124 

   125 declare wcode_on_left_moving_1.simps[simp del]

   126 

   127 fun wcode_on_checking_1 :: "bin_inv_t"

   128   where

   129    "wcode_on_checking_1 ires rs (l, r) = 

   130     (\<exists> ln rn. l = ires \<and>

   131               r = Oc # Oc # Bk\<^bsup>ln\<^esup> @ Bk # Bk # Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>rn\<^esup>)"

   132 

   133 fun wcode_erase1 :: "bin_inv_t"

   134   where

   135 "wcode_erase1 ires rs (l, r) = 

   136        (\<exists> ln rn. l = Oc # ires \<and> 

   137                  tl r = Bk\<^bsup>ln\<^esup> @ Bk # Bk # Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>rn\<^esup>)"

   138 

   139 declare wcode_erase1.simps [simp del]

   140 

   141 fun wcode_on_right_moving_1 :: "bin_inv_t"

   142   where

   143   "wcode_on_right_moving_1 ires rs (l, r) = 

   144        (\<exists> ml mr rn.        

   145              l = Bk\<^bsup>ml\<^esup> @ Oc # ires \<and> 

   146              r = Bk\<^bsup>mr\<^esup> @ Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>rn\<^esup> \<and>

   147              ml + mr > Suc 0)"

   148 

   149 declare wcode_on_right_moving_1.simps [simp del] 

   150 

   151 declare wcode_on_right_moving_1.simps[simp del]

   152 

   153 fun wcode_goon_right_moving_1 :: "bin_inv_t"

   154   where

   155   "wcode_goon_right_moving_1 ires rs (l, r) = 

   156       (\<exists> ml mr ln rn. 

   157             l = Oc\<^bsup>ml\<^esup> @ Bk # Bk # Bk\<^bsup>ln\<^esup> @ Oc # ires \<and> 

   158             r = Oc\<^bsup>mr\<^esup> @ Bk\<^bsup>rn\<^esup> \<and>

   159             ml + mr = Suc rs)"

   160 

   161 declare wcode_goon_right_moving_1.simps[simp del]

   162 

   163 fun wcode_backto_standard_pos_B :: "bin_inv_t"

   164   where

   165   "wcode_backto_standard_pos_B ires rs (l, r) = 

   166           (\<exists> ln rn. l =  Bk # Bk\<^bsup>ln\<^esup> @ Oc # ires \<and> 

   167                r =  Bk # Oc\<^bsup>(Suc (Suc rs))\<^esup> @ Bk\<^bsup>rn \<^esup>)"

   168 

   169 declare wcode_backto_standard_pos_B.simps[simp del]

   170 

   171 fun wcode_backto_standard_pos_O :: "bin_inv_t"

   172   where

   173    "wcode_backto_standard_pos_O ires rs (l, r) = 

   174         (\<exists> ml mr ln rn. 

   175             l = Oc\<^bsup>ml\<^esup> @ Bk # Bk # Bk\<^bsup>ln\<^esup> @ Oc # ires \<and>

   176             r = Oc\<^bsup>mr\<^esup> @ Bk\<^bsup>rn\<^esup> \<and>

   177             ml + mr = Suc (Suc rs) \<and> mr > 0)"

   178 

   179 declare wcode_backto_standard_pos_O.simps[simp del]

   180 

   181 fun wcode_backto_standard_pos :: "bin_inv_t"

   182   where

   183   "wcode_backto_standard_pos ires rs (l, r) = (wcode_backto_standard_pos_B ires rs (l, r) \<or>

   184                                             wcode_backto_standard_pos_O ires rs (l, r))"

   185 

   186 declare wcode_backto_standard_pos.simps[simp del]

   187 

   188 lemma [simp]: "<0::nat> = [Oc]"

   189 apply(simp add: tape_of_nat_abv exponent_def tape_of_nat_list.simps)

   190 done

   191 

   192 lemma tape_of_Suc_nat: "<Suc (a ::nat)> = replicate a Oc @ [Oc, Oc]"

   193 apply(simp add: tape_of_nat_abv exp_ind tape_of_nat_list.simps)

   194 apply(simp only: exp_ind_def[THEN sym])

   195 apply(simp only: exp_ind, simp, simp add: exponent_def)

   196 done

   197 

   198 lemma [simp]: "length (<a::nat>) = Suc a"

   199 apply(simp add: tape_of_nat_abv tape_of_nat_list.simps)

   200 done

   201 

   202 lemma [simp]: "<[a::nat]> = <a>"

   203 apply(simp add: tape_of_nat_abv tape_of_nl_abv exponent_def

   204                 tape_of_nat_list.simps)

   205 done

   206 

   207 lemma bin_wc_eq: "bl_bin xs = bl2wc xs"

   208 proof(induct xs)

   209   show " bl_bin [] = bl2wc []" 

   210     apply(simp add: bl_bin.simps)

   211     done

   212 next

   213   fix a xs

   214   assume "bl_bin xs = bl2wc xs"

   215   thus " bl_bin (a # xs) = bl2wc (a # xs)"

   216     apply(case_tac a, simp_all add: bl_bin.simps bl2wc.simps)

   217     apply(simp_all add: bl2nat.simps bl2nat_double)

   218     done

   219 qed

   220 

   221 declare exp_def[simp del]

   222 

   223 lemma bl_bin_nat_Suc:  

   224   "bl_bin (<Suc a>) = bl_bin (<a>) + 2^(Suc a)"

   225 apply(simp add: tape_of_nat_abv bin_wc_eq)

   226 apply(simp add: bl2wc.simps)

   227 done

   228 lemma [simp]: " rev (a\<^bsup>aa\<^esup>) = a\<^bsup>aa\<^esup>"

   229 apply(simp add: exponent_def)

   230 done

   231  

   232 declare tape_of_nl_abv_cons[simp del]

   233 

   234 lemma tape_of_nl_rev: "rev (<lm::nat list>) = (<rev lm>)"

   235 apply(induct lm rule: list_tl_induct, simp)

   236 apply(case_tac "list = []", simp add: tape_of_nl_abv tape_of_nat_list.simps)

   237 apply(simp add: tape_of_nat_list_butlast_last tape_of_nl_abv_cons)

   238 done

   239 lemma [simp]: "a\<^bsup>Suc 0\<^esup> = [a]" 

   240 by(simp add: exp_def)

   241 lemma tape_of_nl_cons_app1: "(<a # xs @ [b]>) = (Oc\<^bsup>Suc a\<^esup> @ Bk # (<xs@ [b]>))"

   242 apply(case_tac xs, simp add: tape_of_nl_abv tape_of_nat_list.simps)

   243 apply(simp add: tape_of_nl_abv  tape_of_nat_list.simps)

   244 done

   245 

   246 lemma bl_bin_bk_oc[simp]:

   247   "bl_bin (xs @ [Bk, Oc]) = 

   248   bl_bin xs + 2*2^(length xs)"

   249 apply(simp add: bin_wc_eq)

   250 using bl2nat_cons_oc[of "xs @ [Bk]"]

   251 apply(simp add: bl2nat_cons_bk bl2wc.simps)

   252 done

   253 

   254 lemma tape_of_nat[simp]: "(<a::nat>) = Oc\<^bsup>Suc a\<^esup>"

   255 apply(simp add: tape_of_nat_abv)

   256 done

   257 lemma tape_of_nl_cons_app2: "(<c # xs @ [b]>) = (<c # xs> @ Bk # Oc\<^bsup>Suc b\<^esup>)"

   258 proof(induct "length xs" arbitrary: xs c,

   259   simp add: tape_of_nl_abv  tape_of_nat_list.simps)

   260   fix x xs c

   261   assume ind: "\<And>xs c. x = length xs \<Longrightarrow> <c # xs @ [b]> = 

   262     <c # xs> @ Bk # Oc\<^bsup>Suc b\<^esup>"

   263     and h: "Suc x = length (xs::nat list)" 

   264   show "<c # xs @ [b]> = <c # xs> @ Bk # Oc\<^bsup>Suc b\<^esup>"

   265   proof(case_tac xs, simp add: tape_of_nl_abv  tape_of_nat_list.simps)

   266     fix a list

   267     assume g: "xs = a # list"

   268     hence k: "<a # list @ [b]> =  <a # list> @ Bk # Oc\<^bsup>Suc b\<^esup>"

   269       apply(rule_tac ind)

   270       using h

   271       apply(simp)

   272       done

   273     from g and k show "<c # xs @ [b]> = <c # xs> @ Bk # Oc\<^bsup>Suc b\<^esup>"

   274       apply(simp add: tape_of_nl_abv tape_of_nat_list.simps)

   275       done

   276   qed

   277 qed

   278 

   279 lemma [simp]: "length (<aa # a # list>) = Suc (Suc aa) + length (<a # list>)"

   280 apply(simp add: tape_of_nl_abv tape_of_nat_list.simps)

   281 done

   282 

   283 lemma [simp]: "bl_bin (Oc\<^bsup>Suc aa\<^esup> @ Bk # tape_of_nat_list (a # lista) @ [Bk, Oc]) =

   284               bl_bin (Oc\<^bsup>Suc aa\<^esup> @ Bk # tape_of_nat_list (a # lista)) + 

   285               2* 2^(length (Oc\<^bsup>Suc aa\<^esup> @ Bk # tape_of_nat_list (a # lista)))"

   286 using bl_bin_bk_oc[of "Oc\<^bsup>Suc aa\<^esup> @ Bk # tape_of_nat_list (a # lista)"]

   287 apply(simp)

   288 done

   289 

   290 lemma [simp]: 

   291   "bl_bin (<aa # list>) + (4 * rs + 4) * 2 ^ (length (<aa # list>) - Suc 0)

   292   = bl_bin (Oc\<^bsup>Suc aa\<^esup> @ Bk # <list @ [0]>) + rs * (2 * 2 ^ (aa + length (<list @ [0]>)))"

   293 apply(case_tac "list", simp add: add_mult_distrib, simp)

   294 apply(simp add: tape_of_nl_cons_app2 add_mult_distrib)

   295 apply(simp add: tape_of_nl_abv tape_of_nat_list.simps)

   296 done

   297   

   298 lemma tape_of_nl_app_Suc: "((<list @ [Suc ab]>)) = (<list @ [ab]>) @ [Oc]"

   299 apply(induct list)

   300 apply(simp add: tape_of_nl_abv tape_of_nat_list.simps exp_ind)

   301 apply(case_tac list)

   302 apply(simp_all add:tape_of_nl_abv tape_of_nat_list.simps exp_ind)

   303 done

   304 

   305 lemma [simp]: "bl_bin (Oc # Oc\<^bsup>aa\<^esup> @ Bk # <list @ [ab]> @ [Oc])

   306               = bl_bin (Oc # Oc\<^bsup>aa\<^esup> @ Bk # <list @ [ab]>) +

   307               2^(length (Oc # Oc\<^bsup>aa\<^esup> @ Bk # <list @ [ab]>))"

   308 apply(simp add: bin_wc_eq)

   309 apply(simp add: bl2nat_cons_oc bl2wc.simps)

   310 using bl2nat_cons_oc[of "Oc # Oc\<^bsup>aa\<^esup> @ Bk # <list @ [ab]>"]

   311 apply(simp)

   312 done

   313 lemma [simp]: "bl_bin (Oc # Oc\<^bsup>aa\<^esup> @ Bk # <list @ [ab]>) + (4 * 2 ^ (aa + length (<list @ [ab]>)) +

   314          4 * (rs * 2 ^ (aa + length (<list @ [ab]>)))) =

   315        bl_bin (Oc # Oc\<^bsup>aa\<^esup> @ Bk # <list @ [Suc ab]>) +

   316          rs * (2 * 2 ^ (aa + length (<list @ [Suc ab]>)))"

   317 apply(simp add: tape_of_nl_app_Suc)

   318 done

   319 

   320 declare tape_of_nat[simp del]

   321 

   322 text{* double case*}

   323 fun wcode_double_case_inv :: "nat \<Rightarrow> bin_inv_t"

   324   where

   325   "wcode_double_case_inv st ires rs (l, r) = 

   326           (if st = Suc 0 then wcode_on_left_moving_1 ires rs (l, r)

   327           else if st = Suc (Suc 0) then wcode_on_checking_1 ires rs (l, r)

   328           else if st = 3 then wcode_erase1 ires rs (l, r)

   329           else if st = 4 then wcode_on_right_moving_1 ires rs (l, r)

   330           else if st = 5 then wcode_goon_right_moving_1 ires rs (l, r)

   331           else if st = 6 then wcode_backto_standard_pos ires rs (l, r)

   332           else if st = 13 then wcode_before_double ires rs (l, r)

   333           else False)"

   334 

   335 declare wcode_double_case_inv.simps[simp del]

   336 

   337 fun wcode_double_case_state :: "t_conf \<Rightarrow> nat"

   338   where

   339   "wcode_double_case_state (st, l, r) = 

   340    13 - st"

   341 

   342 fun wcode_double_case_step :: "t_conf \<Rightarrow> nat"

   343   where

   344   "wcode_double_case_step (st, l, r) = 

   345       (if st = Suc 0 then (length l)

   346       else if st = Suc (Suc 0) then (length r)

   347       else if st = 3 then 

   348                  if hd r = Oc then 1 else 0

   349       else if st = 4 then (length r)

   350       else if st = 5 then (length r)

   351       else if st = 6 then (length l)

   352       else 0)"

   353 

   354 fun wcode_double_case_measure :: "t_conf \<Rightarrow> nat \<times> nat"

   355   where

   356   "wcode_double_case_measure (st, l, r) = 

   357      (wcode_double_case_state (st, l, r), 

   358       wcode_double_case_step (st, l, r))"

   359 

   360 definition wcode_double_case_le :: "(t_conf \<times> t_conf) set"

   361   where "wcode_double_case_le \<equiv> (inv_image lex_pair wcode_double_case_measure)"

   362 

   363 lemma [intro]: "wf lex_pair"

   364 by(auto intro:wf_lex_prod simp:lex_pair_def)

   365 

   366 lemma wf_wcode_double_case_le[intro]: "wf wcode_double_case_le"

   367 by(auto intro:wf_inv_image simp: wcode_double_case_le_def )

   368 term fetch

   369 

   370 lemma [simp]: "fetch t_wcode_main (Suc 0) Bk = (L, Suc 0)"

   371 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

   372                 fetch.simps nth_of.simps)

   373 done

   374 

   375 lemma [simp]: "fetch t_wcode_main (Suc 0) Oc = (L, Suc (Suc 0))"

   376 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

   377                 fetch.simps nth_of.simps)

   378 done

   379 

   380 lemma [simp]: "fetch t_wcode_main (Suc (Suc 0)) Oc = (R, 3)"

   381 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

   382                 fetch.simps nth_of.simps)

   383 done

   384 

   385 lemma [simp]: "fetch t_wcode_main (Suc (Suc (Suc 0))) Bk = (R, 4)"

   386 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

   387                 fetch.simps nth_of.simps)

   388 done 

   389 

   390 lemma [simp]: "fetch t_wcode_main (Suc (Suc (Suc 0))) Oc = (W0, 3)"

   391 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

   392                 fetch.simps nth_of.simps)

   393 done

   394 

   395 lemma [simp]: "fetch t_wcode_main 4 Bk = (R, 4)"

   396 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

   397                 fetch.simps nth_of.simps)

   398 done

   399 

   400 lemma [simp]: "fetch t_wcode_main 4 Oc = (R, 5)"

   401 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

   402                 fetch.simps nth_of.simps)

   403 done

   404 

   405 lemma [simp]: "fetch t_wcode_main 5 Oc = (R, 5)"

   406 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

   407                 fetch.simps nth_of.simps)

   408 done

   409 

   410 lemma [simp]: "fetch t_wcode_main 5 Bk = (W1, 6)"

   411 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

   412                 fetch.simps nth_of.simps)

   413 done

   414 

   415 lemma [simp]: "fetch t_wcode_main 6 Bk = (R, 13)"

   416 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

   417                 fetch.simps nth_of.simps)

   418 done

   419 

   420 lemma [simp]: "fetch t_wcode_main 6 Oc = (L, 6)"

   421 apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

   422                 fetch.simps nth_of.simps)

   423 done

   424 lemma [elim]: "Bk\<^bsup>mr\<^esup> = [] \<Longrightarrow> mr = 0"

   425 apply(case_tac mr, auto simp: exponent_def)

   426 done

   427 

   428 lemma [simp]: "wcode_on_left_moving_1 ires rs (b, []) = False"

   429 apply(simp add: wcode_on_left_moving_1.simps wcode_on_left_moving_1_B.simps

   430                 wcode_on_left_moving_1_O.simps, auto)

   431 done

   432 

   433 

   434 declare wcode_on_checking_1.simps[simp del]

   435 

   436 lemmas wcode_double_case_inv_simps = 

   437   wcode_on_left_moving_1.simps wcode_on_left_moving_1_O.simps

   438   wcode_on_left_moving_1_B.simps wcode_on_checking_1.simps

   439   wcode_erase1.simps wcode_on_right_moving_1.simps

   440   wcode_goon_right_moving_1.simps wcode_backto_standard_pos.simps

   441 

   442 

   443 lemma [simp]: "wcode_on_left_moving_1 ires rs (b, r) \<Longrightarrow> b \<noteq> []"

   444 apply(simp add: wcode_double_case_inv_simps, auto)

   445 done

   446 

   447 

   448 lemma [elim]: "\<lbrakk>wcode_on_left_moving_1 ires rs (b, Bk # list);

   449                 tl b = aa \<and> hd b # Bk # list = ba\<rbrakk> \<Longrightarrow> 

   450                wcode_on_left_moving_1 ires rs (aa, ba)"

   451 apply(simp only: wcode_on_left_moving_1.simps wcode_on_left_moving_1_O.simps

   452                 wcode_on_left_moving_1_B.simps)

   453 apply(erule_tac disjE)

   454 apply(erule_tac exE)+

   455 apply(case_tac ml, simp)

   456 apply(rule_tac x = "mr - Suc (Suc 0)" in exI, rule_tac x = rn in exI)

   457 apply(case_tac mr, simp, case_tac nat, simp, simp add: exp_ind)

   458 apply(rule_tac disjI1)

   459 apply(rule_tac x = nat in exI, rule_tac x = "Suc mr" in exI, rule_tac x = rn in exI, 

   460       simp add: exp_ind_def)

   461 apply(erule_tac exE)+

   462 apply(simp)

   463 done

   464 

   465 

   466 lemma [elim]: 

   467   "\<lbrakk>wcode_on_left_moving_1 ires rs (b, Oc # list); tl b = aa \<and> hd b # Oc # list = ba\<rbrakk> 

   468     \<Longrightarrow> wcode_on_checking_1 ires rs (aa, ba)"

   469 apply(simp only: wcode_double_case_inv_simps)

   470 apply(erule_tac disjE)

   471 apply(erule_tac [!] exE)+

   472 apply(case_tac mr, simp, simp add: exp_ind_def)

   473 apply(rule_tac x = ln in exI, rule_tac x = rn in exI, simp)

   474 done

   475 

   476 

   477 lemma [simp]: "wcode_on_checking_1 ires rs (b, []) = False" 

   478 apply(auto simp: wcode_double_case_inv_simps)

   479 done         

   480  

   481 lemma [simp]: "wcode_on_checking_1 ires rs (b, Bk # list) = False"

   482 apply(auto simp: wcode_double_case_inv_simps)

   483 done         

   484   

   485 lemma [elim]: "\<lbrakk>wcode_on_checking_1 ires rs (b, Oc # ba);Oc # b = aa \<and> list = ba\<rbrakk>

   486   \<Longrightarrow> wcode_erase1 ires rs (aa, ba)"

   487 apply(simp only: wcode_double_case_inv_simps)

   488 apply(erule_tac exE)+

   489 apply(rule_tac x = ln in exI, rule_tac x = rn in exI, simp)

   490 done

   491 

   492 

   493 lemma [simp]: "wcode_on_checking_1 ires rs (b, []) = False"

   494 apply(simp add: wcode_double_case_inv_simps)

   495 done

   496 

   497 lemma [simp]: "wcode_on_checking_1 ires rs ([], Bk # list) = False"

   498 apply(simp add: wcode_double_case_inv_simps)

   499 done

   500 

   501 lemma [simp]: "wcode_erase1 ires rs (b, []) = False"

   502 apply(simp add: wcode_double_case_inv_simps)

   503 done

   504 

   505 lemma [simp]: "wcode_on_right_moving_1 ires rs (b, []) = False"

   506 apply(simp add: wcode_double_case_inv_simps exp_ind_def)

   507 done

   508 

   509 lemma [simp]: "wcode_on_right_moving_1 ires rs (b, []) = False"

   510 apply(simp add: wcode_double_case_inv_simps exp_ind_def)

   511 done

   512 

   513 lemma [elim]: "\<lbrakk>wcode_on_right_moving_1 ires rs (b, Bk # ba);  Bk # b = aa \<and> list = b\<rbrakk> \<Longrightarrow> 

   514   wcode_on_right_moving_1 ires rs (aa, ba)"

   515 apply(simp only: wcode_double_case_inv_simps)

   516 apply(erule_tac exE)+

   517 apply(rule_tac x = "Suc ml" in exI, rule_tac x = "mr - Suc 0" in exI,

   518       rule_tac x = rn in exI)

   519 apply(simp add: exp_ind_def)

   520 apply(case_tac mr, simp, simp add: exp_ind_def)

   521 done

   522 

   523 lemma [elim]: 

   524   "\<lbrakk>wcode_on_right_moving_1 ires rs (b, Oc # ba); Oc # b = aa \<and> list = ba\<rbrakk> 

   525   \<Longrightarrow> wcode_goon_right_moving_1 ires rs (aa, ba)"

   526 apply(simp only: wcode_double_case_inv_simps)

   527 apply(erule_tac exE)+

   528 apply(rule_tac x = "Suc 0" in exI, rule_tac x = "rs" in exI,

   529       rule_tac x = "ml - Suc (Suc 0)" in exI, rule_tac x = rn in exI)

   530 apply(case_tac mr, simp_all add: exp_ind_def)

   531 apply(case_tac ml, simp, case_tac nat, simp, simp)

   532 apply(simp add: exp_ind_def)

   533 done

   534 

   535 lemma [simp]: 

   536   "wcode_on_right_moving_1 ires rs (b, []) \<Longrightarrow> False"

   537 apply(simp add: wcode_double_case_inv_simps exponent_def)

   538 done

   539 

   540 lemma [elim]: "\<lbrakk>wcode_erase1 ires rs (b, Bk # ba); Bk # b = aa \<and> list = ba; c = Bk # ba\<rbrakk> 

   541   \<Longrightarrow> wcode_on_right_moving_1 ires rs (aa, ba)"

   542 apply(simp only: wcode_double_case_inv_simps)

   543 apply(erule_tac exE)+

   544 apply(rule_tac x = "Suc 0" in exI, rule_tac x = "Suc (Suc ln)" in exI, 

   545       rule_tac x = rn in exI, simp add: exp_ind)

   546 done

   547 

   548 lemma [elim]: "\<lbrakk>wcode_erase1 ires rs (aa, Oc # list);  b = aa \<and> Bk # list = ba\<rbrakk> \<Longrightarrow> 

   549   wcode_erase1 ires rs (aa, ba)"

   550 apply(simp only: wcode_double_case_inv_simps)

   551 apply(erule_tac exE)+

   552 apply(rule_tac x = ln in exI, rule_tac x = rn in exI, auto)

   553 done

   554 

   555 lemma [elim]: "\<lbrakk>wcode_goon_right_moving_1 ires rs (aa, []); b = aa \<and> [Oc] = ba\<rbrakk> 

   556               \<Longrightarrow> wcode_backto_standard_pos ires rs (aa, ba)"

   557 apply(simp only: wcode_double_case_inv_simps)

   558 apply(erule_tac exE)+

   559 apply(rule_tac disjI2)

   560 apply(simp only:wcode_backto_standard_pos_O.simps)

   561 apply(rule_tac x = ml in exI, rule_tac x = "Suc 0" in exI, rule_tac x = ln in exI,

   562       rule_tac x = rn in exI, simp)

   563 apply(case_tac mr, simp_all add: exponent_def)

   564 done

   565 

   566 lemma [elim]: 

   567   "\<lbrakk>wcode_goon_right_moving_1 ires rs (aa, Bk # list);  b = aa \<and> Oc # list = ba\<rbrakk>

   568   \<Longrightarrow> wcode_backto_standard_pos ires rs (aa, ba)"

   569 apply(simp only: wcode_double_case_inv_simps)

   570 apply(erule_tac exE)+

   571 apply(rule_tac disjI2)

   572 apply(simp only:wcode_backto_standard_pos_O.simps)

   573 apply(rule_tac x = ml in exI, rule_tac x = "Suc 0" in exI, rule_tac x = ln in exI,

   574       rule_tac x = "rn - Suc 0" in exI, simp)

   575 apply(case_tac mr, simp, case_tac rn, simp, simp_all add: exp_ind_def)

   576 done

   577 

   578 lemma [elim]: "\<lbrakk>wcode_goon_right_moving_1 ires rs (b, Oc # ba);  Oc # b = aa \<and> list = ba\<rbrakk> 

   579   \<Longrightarrow> wcode_goon_right_moving_1 ires rs (aa, ba)"

   580 apply(simp only: wcode_double_case_inv_simps)

   581 apply(erule_tac exE)+

   582 apply(rule_tac x = "Suc ml" in exI, rule_tac x = "mr - Suc 0" in exI, 

   583       rule_tac x = ln in exI, rule_tac x = rn in exI)

   584 apply(simp add: exp_ind_def)

   585 apply(case_tac mr, simp, case_tac rn, simp_all add: exp_ind_def)

   586 done

   587 

   588 lemma [elim]: "\<lbrakk>wcode_backto_standard_pos ires rs (b, []);  Bk # b = aa\<rbrakk> \<Longrightarrow> False"

   589 apply(auto simp: wcode_double_case_inv_simps wcode_backto_standard_pos_O.simps

   590                  wcode_backto_standard_pos_B.simps)

   591 apply(case_tac mr, simp_all add: exp_ind_def)

   592 done

   593 

   594 lemma [elim]: "\<lbrakk>wcode_backto_standard_pos ires rs (b, Bk # ba); Bk # b = aa \<and> list = ba\<rbrakk> 

   595   \<Longrightarrow> wcode_before_double ires rs (aa, ba)"

   596 apply(simp only: wcode_double_case_inv_simps wcode_backto_standard_pos_B.simps

   597                  wcode_backto_standard_pos_O.simps wcode_before_double.simps)

   598 apply(erule_tac disjE)

   599 apply(erule_tac exE)+

   600 apply(rule_tac x = ln in exI, rule_tac x = rn in exI, simp)

   601 apply(auto)

   602 apply(case_tac [!] mr, simp_all add: exp_ind_def)

   603 done

   604 

   605 lemma [simp]: "wcode_backto_standard_pos ires rs ([], Oc # list) = False"

   606 apply(auto simp: wcode_backto_standard_pos.simps wcode_backto_standard_pos_B.simps

   607                  wcode_backto_standard_pos_O.simps)

   608 done

   609 

   610 lemma [simp]: "wcode_backto_standard_pos ires rs (b, []) = False"

   611 apply(auto simp: wcode_backto_standard_pos.simps wcode_backto_standard_pos_B.simps

   612                  wcode_backto_standard_pos_O.simps)

   613 apply(case_tac mr, simp, simp add: exp_ind_def)

   614 done

   615 

   616 lemma [elim]: "\<lbrakk>wcode_backto_standard_pos ires rs (b, Oc # list); tl b = aa; hd b # Oc # list =  ba\<rbrakk>

   617        \<Longrightarrow> wcode_backto_standard_pos ires rs (aa, ba)"

   618 apply(simp only:  wcode_backto_standard_pos.simps wcode_backto_standard_pos_B.simps

   619                  wcode_backto_standard_pos_O.simps)

   620 apply(erule_tac disjE)

   621 apply(simp)

   622 apply(erule_tac exE)+

   623 apply(case_tac ml, simp)

   624 apply(rule_tac disjI1, rule_tac conjI)

   625 apply(rule_tac x = ln  in exI, simp, rule_tac x = rn in exI, simp)

   626 apply(rule_tac disjI2)

   627 apply(rule_tac x = nat in exI, rule_tac x = "Suc mr" in exI, rule_tac x = ln in exI, 

   628       rule_tac x = rn in exI, simp)

   629 apply(simp add: exp_ind_def)

   630 done

   631 

   632 declare new_tape.simps[simp del] nth_of.simps[simp del] fetch.simps[simp del]

   633 lemma wcode_double_case_first_correctness:

   634   "let P = (\<lambda> (st, l, r). st = 13) in 

   635        let Q = (\<lambda> (st, l, r). wcode_double_case_inv st ires rs (l, r)) in 

   636        let f = (\<lambda> stp. steps (Suc 0, Bk # Bk\<^bsup>m\<^esup> @ Oc # Oc # ires, Bk # Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>n\<^esup>) t_wcode_main stp) in

   637        \<exists> n .P (f n) \<and> Q (f (n::nat))"

   638 proof -

   639   let ?P = "(\<lambda> (st, l, r). st = 13)"

   640   let ?Q = "(\<lambda> (st, l, r). wcode_double_case_inv st ires rs (l, r))"

   641   let ?f = "(\<lambda> stp. steps (Suc 0, Bk # Bk\<^bsup>m\<^esup> @ Oc # Oc # ires, Bk # Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>n\<^esup>) t_wcode_main stp)"

   642   have "\<exists> n. ?P (?f n) \<and> ?Q (?f (n::nat))"

   643   proof(rule_tac halt_lemma2)

   644     show "wf wcode_double_case_le"

   645       by auto

   646   next

   647     show "\<forall> na. \<not> ?P (?f na) \<and> ?Q (?f na) \<longrightarrow>

   648                    ?Q (?f (Suc na)) \<and> (?f (Suc na), ?f na) \<in> wcode_double_case_le"

   649     proof(rule_tac allI, case_tac "?f na", simp add: tstep_red)

   650       fix na a b c

   651       show "a \<noteq> 13 \<and> wcode_double_case_inv a ires rs (b, c) \<longrightarrow>

   652                (case tstep (a, b, c) t_wcode_main of (st, x) \<Rightarrow> 

   653                    wcode_double_case_inv st ires rs x) \<and> 

   654                 (tstep (a, b, c) t_wcode_main, a, b, c) \<in> wcode_double_case_le"

   655         apply(rule_tac impI, simp add: wcode_double_case_inv.simps)

   656         apply(auto split: if_splits simp: tstep.simps, 

   657               case_tac [!] c, simp_all, case_tac [!] "(c::block list)!0")

   658         apply(simp_all add: new_tape.simps wcode_double_case_inv.simps wcode_double_case_le_def

   659                                         lex_pair_def)

   660         apply(auto split: if_splits)

   661         done

   662     qed

   663   next

   664     show "?Q (?f 0)"

   665       apply(simp add: steps.simps wcode_double_case_inv.simps 

   666                                   wcode_on_left_moving_1.simps

   667                                   wcode_on_left_moving_1_B.simps)

   668       apply(rule_tac disjI1)

   669       apply(rule_tac x = "Suc m" in exI, simp add: exp_ind_def)

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

   671       apply(auto)

   672       done

   673   next

   674     show "\<not> ?P (?f 0)"

   675       apply(simp add: steps.simps)

   676       done

   677   qed

   678   thus "let P = \<lambda>(st, l, r). st = 13;

   679     Q = \<lambda>(st, l, r). wcode_double_case_inv st ires rs (l, r);

   680     f = steps (Suc 0, Bk # Bk\<^bsup>m\<^esup> @ Oc # Oc # ires, Bk # Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>n\<^esup>) t_wcode_main

   681     in \<exists>n. P (f n) \<and> Q (f n)"

   682     apply(simp add: Let_def)

   683     done

   684 qed

   685     

   686 lemma [elim]: "t_ncorrect tp

   687     \<Longrightarrow> t_ncorrect (abacus.tshift tp a)"

   688 apply(simp add: t_ncorrect.simps shift_length)

   689 done

   690 

   691 lemma tshift_fetch: "\<lbrakk> fetch tp a b = (aa, st'); 0 < st'\<rbrakk>

   692        \<Longrightarrow> fetch (abacus.tshift tp (length tp1 div 2)) a b 

   693           = (aa, st' + length tp1 div 2)"

   694 apply(subgoal_tac "a > 0")

   695 apply(auto simp: fetch.simps nth_of.simps shift_length nth_map

   696                  tshift.simps split: block.splits if_splits)

   697 done

   698 

   699 lemma t_steps_steps_eq: "\<lbrakk>steps (st, l, r) tp stp = (st', l', r');

   700          0 < st';  

   701          0 < st \<and> st \<le> length tp div 2; 

   702          t_ncorrect tp1;

   703           t_ncorrect tp\<rbrakk>

   704     \<Longrightarrow> t_steps (st + length tp1 div 2, l, r) (tshift tp (length tp1 div 2), 

   705                                                       length tp1 div 2) stp

   706        = (st' + length tp1 div 2, l', r')"

   707 apply(induct stp arbitrary: st' l' r', simp add: steps.simps t_steps.simps,

   708       simp add: tstep_red stepn)

   709 apply(case_tac "(steps (st, l, r) tp stp)", simp)

   710 proof -

   711   fix stp st' l' r' a b c

   712   assume ind: "\<And>st' l' r'.

   713     \<lbrakk>a = st' \<and> b = l' \<and> c = r'; 0 < st'\<rbrakk>

   714     \<Longrightarrow> t_steps (st + length tp1 div 2, l, r) 

   715     (abacus.tshift tp (length tp1 div 2), length tp1 div 2) stp = 

   716      (st' + length tp1 div 2, l', r')"

   717   and h: "tstep (a, b, c) tp = (st', l', r')" "0 < st'" "t_ncorrect tp1"  "t_ncorrect tp"

   718   have k: "t_steps (st + length tp1 div 2, l, r) (abacus.tshift tp (length tp1 div 2),

   719          length tp1 div 2) stp = (a + length tp1 div 2, b, c)"

   720     apply(rule_tac ind, simp)

   721     using h

   722     apply(case_tac a, simp_all add: tstep.simps fetch.simps)

   723     done

   724   from h and this show "t_step (t_steps (st + length tp1 div 2, l, r) (abacus.tshift tp (length tp1 div 2), length tp1 div 2) stp)

   725            (abacus.tshift tp (length tp1 div 2), length tp1 div 2) =

   726           (st' + length tp1 div 2, l', r')"

   727     apply(simp add: k)

   728     apply(simp add: tstep.simps t_step.simps)

   729     apply(case_tac "fetch tp a (case c of [] \<Rightarrow> Bk | x # xs \<Rightarrow> x)", simp)

   730     apply(subgoal_tac "fetch (abacus.tshift tp (length tp1 div 2)) a

   731                        (case c of [] \<Rightarrow> Bk | x # xs \<Rightarrow> x) = (aa, st' + length tp1 div 2)", simp)

   732     apply(simp add: tshift_fetch)

   733     done

   734 qed 

   735 

   736 lemma t_tshift_lemma: "\<lbrakk> steps (st, l, r) tp stp = (st', l', r'); 

   737                          st' \<noteq> 0; 

   738                          stp > 0;

   739                          0 < st \<and> st \<le> length tp div 2;

   740                          t_ncorrect tp1;

   741                          t_ncorrect tp;

   742                          t_ncorrect tp2

   743                          \<rbrakk>

   744          \<Longrightarrow> \<exists> stp>0. steps (st + length tp1 div 2, l, r) (tp1 @ tshift tp (length tp1 div 2) @ tp2) stp 

   745                   = (st' + length tp1 div 2, l', r')"

   746 proof -

   747   assume h: "steps (st, l, r) tp stp = (st', l', r')"

   748     "st' \<noteq> 0" "stp > 0"

   749     "0 < st \<and> st \<le> length tp div 2"

   750     "t_ncorrect tp1"

   751     "t_ncorrect tp"

   752     "t_ncorrect tp2"

   753   from h have 

   754     "\<exists>stp>0. t_steps (st + length tp1 div 2, l, r) (tp1 @ abacus.tshift tp (length tp1 div 2) @ tp2, 0) stp = 

   755                             (st' + length tp1 div 2, l', r')"

   756     apply(rule_tac stp = stp in turing_shift, simp_all add: shift_length)

   757     apply(simp add: t_steps_steps_eq)

   758     apply(simp add: t_ncorrect.simps shift_length)

   759     done

   760   thus "\<exists> stp>0. steps (st + length tp1 div 2, l, r) (tp1 @ tshift tp (length tp1 div 2) @ tp2) stp 

   761                   = (st' + length tp1 div 2, l', r')"

   762     apply(erule_tac exE)

   763     apply(rule_tac x = stp in exI, simp)

   764     apply(subgoal_tac "length (tp1 @ abacus.tshift tp (length tp1 div 2) @ tp2) mod 2 = 0")

   765     apply(simp only: steps_eq)

   766     using h

   767     apply(auto simp: t_ncorrect.simps shift_length)

   768     apply arith

   769     done

   770 qed  

   771   

   772 

   773 lemma t_twice_len_ge: "Suc 0 \<le> length t_twice div 2"

   774 apply(simp add: t_twice_def tMp.simps shift_length)

   775 done

   776 

   777 lemma [intro]: "rec_calc_rel (recf.id (Suc 0) 0) [rs] rs"

   778   apply(rule_tac calc_id, simp_all)

   779   done

   780   

   781 lemma [intro]: "rec_calc_rel (constn 2) [rs] 2"

   782 using prime_rel_exec_eq[of "constn 2" "[rs]" 2]

   783 apply(subgoal_tac "primerec (constn 2) 1", auto)

   784 done

   785 

   786 lemma  [intro]: "rec_calc_rel rec_mult [rs, 2] (2 * rs)"

   787 using prime_rel_exec_eq[of "rec_mult" "[rs, 2]"  "2*rs"]

   788 apply(subgoal_tac "primerec rec_mult (Suc (Suc 0))", auto)

   789 done

   790 lemma t_twice_correct: "\<exists>stp ln rn. steps (Suc 0, Bk # Bk # ires, Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>n\<^esup>) 

   791             (tm_of abc_twice @ tMp (Suc 0) (start_of twice_ly (length abc_twice) - Suc 0)) stp =

   792        (0, Bk\<^bsup>ln\<^esup> @ Bk # Bk # ires, Oc\<^bsup>Suc (2 * rs)\<^esup> @ Bk\<^bsup>rn\<^esup>)"

   793 proof(case_tac "rec_ci rec_twice")

   794   fix a b c

   795   assume h: "rec_ci rec_twice = (a, b, c)"

   796   have "\<exists>stp m l. steps (Suc 0, Bk # Bk # ires, <[rs]> @ Bk\<^bsup>n\<^esup>) (tm_of abc_twice @ tMp (Suc 0) 

   797     (start_of twice_ly (length abc_twice) - 1)) stp = (0, Bk\<^bsup>m\<^esup> @ Bk # Bk # ires, Oc\<^bsup>Suc (2*rs)\<^esup> @ Bk\<^bsup>l\<^esup>)"

   798   proof(rule_tac t_compiled_by_rec)

   799     show "rec_ci rec_twice = (a, b, c)" by (simp add: h)

   800   next

   801     show "rec_calc_rel rec_twice [rs] (2 * rs)"

   802       apply(simp add: rec_twice_def)

   803       apply(rule_tac rs =  "[rs, 2]" in calc_cn, simp_all)

   804       apply(rule_tac allI, case_tac k, auto)

   805       done

   806   next

   807     show "length [rs] = Suc 0" by simp

   808   next

   809     show "layout_of (a [+] dummy_abc (Suc 0)) = layout_of (a [+] dummy_abc (Suc 0))"

   810       by simp

   811   next

   812     show "start_of twice_ly (length abc_twice) = 

   813       start_of (layout_of (a [+] dummy_abc (Suc 0))) (length (a [+] dummy_abc (Suc 0)))"

   814       using h

   815       apply(simp add: twice_ly_def abc_twice_def)

   816       done

   817   next

   818     show "tm_of abc_twice = tm_of (a [+] dummy_abc (Suc 0))"

   819       using h

   820       apply(simp add: abc_twice_def)

   821       done

   822   qed

   823   thus "\<exists>stp ln rn. steps (Suc 0, Bk # Bk # ires, Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>n\<^esup>) 

   824             (tm_of abc_twice @ tMp (Suc 0) (start_of twice_ly (length abc_twice) - Suc 0)) stp =

   825        (0, Bk\<^bsup>ln\<^esup> @ Bk # Bk # ires, Oc\<^bsup>Suc (2 * rs)\<^esup> @ Bk\<^bsup>rn\<^esup>)"

   826     apply(simp add: tape_of_nl_abv tape_of_nat_list.simps)

   827     done

   828 qed

   829 

   830 lemma change_termi_state_fetch: "\<lbrakk>fetch ap a b = (aa, st); st > 0\<rbrakk>

   831        \<Longrightarrow> fetch (change_termi_state ap) a b = (aa, st)"

   832 apply(case_tac b, auto simp: fetch.simps nth_of.simps change_termi_state.simps nth_map

   833                        split: if_splits block.splits)

   834 done

   835 

   836 lemma change_termi_state_exec_in_range:

   837      "\<lbrakk>steps (st, l, r) ap stp = (st', l', r'); st' \<noteq> 0\<rbrakk>

   838     \<Longrightarrow> steps (st, l, r) (change_termi_state ap) stp = (st', l', r')"

   839 proof(induct stp arbitrary: st l r st' l' r', simp add: steps.simps)

   840   fix stp st l r st' l' r'

   841   assume ind: "\<And>st l r st' l' r'. 

   842     \<lbrakk>steps (st, l, r) ap stp = (st', l', r'); st' \<noteq> 0\<rbrakk> \<Longrightarrow>

   843     steps (st, l, r) (change_termi_state ap) stp = (st', l', r')"

   844   and h: "steps (st, l, r) ap (Suc stp) = (st', l', r')" "st' \<noteq> 0"

   845   from h show "steps (st, l, r) (change_termi_state ap) (Suc stp) = (st', l', r')"

   846   proof(simp add: tstep_red, case_tac "steps (st, l, r) ap stp", simp)

   847     fix a b c

   848     assume g: "steps (st, l, r) ap stp = (a, b, c)"

   849               "tstep (a, b, c) ap = (st', l', r')" "0 < st'"

   850     hence "steps (st, l, r) (change_termi_state ap) stp = (a, b, c)"

   851       apply(rule_tac ind, simp)

   852       apply(case_tac a, simp_all add: tstep_0)

   853       done

   854     from g and this show "tstep (steps (st, l, r) (change_termi_state ap) stp)

   855       (change_termi_state ap) = (st', l', r')"

   856       apply(simp add: tstep.simps)

   857       apply(case_tac "fetch ap a (case c of [] \<Rightarrow> Bk | x # xs \<Rightarrow> x)", simp)

   858       apply(subgoal_tac "fetch (change_termi_state ap) a (case c of [] \<Rightarrow> Bk | x # xs \<Rightarrow> x)

   859                    = (aa, st')", simp)

   860       apply(simp add: change_termi_state_fetch)

   861       done

   862   qed

   863 qed

   864 

   865 lemma change_termi_state_fetch0: 

   866   "\<lbrakk>0 < a; a \<le> length ap div 2; t_correct ap; fetch ap a b = (aa, 0)\<rbrakk>

   867   \<Longrightarrow> fetch (change_termi_state ap) a b = (aa, Suc (length ap div 2))"

   868 apply(case_tac b, auto simp: fetch.simps nth_of.simps change_termi_state.simps nth_map

   869                        split: if_splits block.splits)

   870 done

   871 

   872 lemma turing_change_termi_state: 

   873   "\<lbrakk>steps (Suc 0, l, r) ap stp = (0, l', r'); t_correct ap\<rbrakk>

   874      \<Longrightarrow> \<exists> stp. steps (Suc 0, l, r) (change_termi_state ap) stp = 

   875         (Suc (length ap div 2), l', r')"

   876 apply(drule first_halt_point)

   877 apply(erule_tac exE)

   878 apply(rule_tac x = "Suc stp" in exI, simp add: tstep_red)

   879 apply(case_tac "steps (Suc 0, l, r) ap stp")

   880 apply(simp add: isS0_def change_termi_state_exec_in_range)

   881 apply(subgoal_tac "steps (Suc 0, l, r) (change_termi_state ap) stp = (a, b, c)", simp)

   882 apply(simp add: tstep.simps)

   883 apply(case_tac "fetch ap a (case c of [] \<Rightarrow> Bk | x # xs \<Rightarrow> x)", simp)

   884 apply(subgoal_tac "fetch (change_termi_state ap) a 

   885   (case c of [] \<Rightarrow> Bk | x # xs \<Rightarrow> x) = (aa, Suc (length ap div 2))", simp)

   886 apply(rule_tac ap = ap in change_termi_state_fetch0, simp_all)

   887 apply(rule_tac tp = "(l, r)" and l = b and r = c  and stp = stp and A = ap in s_keep, simp_all)

   888 apply(simp add: change_termi_state_exec_in_range)

   889 done

   890 

   891 lemma t_twice_change_term_state:

   892   "\<exists> stp ln rn. steps (Suc 0, Bk # Bk # ires, Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>n\<^esup>) t_twice stp

   893      = (Suc t_twice_len, Bk\<^bsup>ln\<^esup> @ Bk # Bk # ires, Oc\<^bsup>Suc (2 * rs)\<^esup> @ Bk\<^bsup>rn\<^esup>)"

   894 using t_twice_correct[of ires rs n]

   895 apply(erule_tac exE)

   896 apply(erule_tac exE)

   897 apply(erule_tac exE)

   898 proof(drule_tac turing_change_termi_state)

   899   fix stp ln rn

   900   show "t_correct (tm_of abc_twice @ tMp (Suc 0) (start_of twice_ly (length abc_twice) - Suc 0))"

   901     apply(rule_tac t_compiled_correct, simp_all)

   902     apply(simp add: twice_ly_def)

   903     done

   904 next

   905   fix stp ln rn

   906   show "\<exists>stp. steps (Suc 0, Bk # Bk # ires, Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>n\<^esup>)

   907     (change_termi_state (tm_of abc_twice @ tMp (Suc 0) 

   908     (start_of twice_ly (length abc_twice) - Suc 0))) stp =

   909     (Suc (length (tm_of abc_twice @ tMp (Suc 0) (start_of twice_ly (length abc_twice) - Suc 0)) div 2),

   910     Bk\<^bsup>ln\<^esup> @ Bk # Bk # ires, Oc\<^bsup>Suc (2 * rs)\<^esup> @ Bk\<^bsup>rn\<^esup>) \<Longrightarrow>

   911     \<exists>stp ln rn. steps (Suc 0, Bk # Bk # ires, Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>n\<^esup>) t_twice stp = 

   912     (Suc t_twice_len, Bk\<^bsup>ln\<^esup> @ Bk # Bk # ires, Oc\<^bsup>Suc (2 * rs)\<^esup> @ Bk\<^bsup>rn\<^esup>)"

   913     apply(erule_tac exE)

   914     apply(simp add: t_twice_len_def t_twice_def)

   915     apply(rule_tac x = stp in exI, rule_tac x = ln in exI, rule_tac x = rn in exI, simp)

   916     done

   917 qed

   918 

   919 lemma t_twice_append_pre:

   920   "steps (Suc 0, Bk # Bk # ires, Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>n\<^esup>) t_twice stp

   921   = (Suc t_twice_len, Bk\<^bsup>ln\<^esup> @ Bk # Bk # ires, Oc\<^bsup>Suc (2 * rs)\<^esup> @ Bk\<^bsup>rn\<^esup>)

   922    \<Longrightarrow> \<exists> stp>0. steps (Suc 0 + length t_wcode_main_first_part div 2, Bk # Bk # ires, Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>n\<^esup>)

   923      (t_wcode_main_first_part @ tshift t_twice (length t_wcode_main_first_part div 2) @

   924       ([(L, 1), (L, 1)] @ tshift t_fourtimes (t_twice_len + 13) @ [(L, 1), (L, 1)])) stp 

   925     = (Suc (t_twice_len) + length t_wcode_main_first_part div 2, Bk\<^bsup>ln\<^esup> @ Bk # Bk # ires, Oc\<^bsup>Suc (2 * rs)\<^esup> @ Bk\<^bsup>rn\<^esup>)"

   926 proof(rule_tac t_tshift_lemma, simp_all add: t_twice_len_ge)

   927   assume "steps (Suc 0, Bk # Bk # ires, Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>n\<^esup>) t_twice stp = 

   928     (Suc t_twice_len, Bk\<^bsup>ln\<^esup> @ Bk # Bk # ires, Oc\<^bsup>Suc (2 * rs)\<^esup> @ Bk\<^bsup>rn\<^esup>)"

   929   thus "0 < stp"

   930     apply(case_tac stp, simp add: steps.simps t_twice_len_ge t_twice_len_def)

   931     using t_twice_len_ge

   932     apply(simp, simp)

   933     done

   934 next

   935   show "t_ncorrect t_wcode_main_first_part"

   936     apply(simp add: t_ncorrect.simps t_wcode_main_first_part_def)

   937     done

   938 next

   939   show "t_ncorrect t_twice"

   940     using length_tm_even[of abc_twice]

   941     apply(auto simp: t_ncorrect.simps t_twice_def)

   942     apply(arith)

   943     done

   944 next

   945   show "t_ncorrect ((L, Suc 0) # (L, Suc 0) #

   946        abacus.tshift t_fourtimes (t_twice_len + 13) @ [(L, Suc 0), (L, Suc 0)])"

   947     using length_tm_even[of abc_fourtimes]

   948     apply(simp add: t_ncorrect.simps shift_length t_fourtimes_def)

   949     apply arith

   950     done

   951 qed

   952   

   953 lemma t_twice_append:

   954   "\<exists> stp ln rn. steps (Suc 0 + length t_wcode_main_first_part div 2, Bk # Bk # ires, Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>n\<^esup>)

   955      (t_wcode_main_first_part @ tshift t_twice (length t_wcode_main_first_part div 2) @

   956       ([(L, 1), (L, 1)] @ tshift t_fourtimes (t_twice_len + 13) @ [(L, 1), (L, 1)])) stp 

   957     = (Suc (t_twice_len) + length t_wcode_main_first_part div 2, Bk\<^bsup>ln\<^esup> @ Bk # Bk # ires, Oc\<^bsup>Suc (2 * rs)\<^esup> @ Bk\<^bsup>rn\<^esup>)"

   958   using t_twice_change_term_state[of ires rs n]

   959   apply(erule_tac exE)

   960   apply(erule_tac exE)

   961   apply(erule_tac exE)

   962   apply(drule_tac t_twice_append_pre)

   963   apply(erule_tac exE)

   964   apply(rule_tac x = stpa in exI, rule_tac x = ln in exI, rule_tac x = rn in exI)

   965   apply(simp)

   966   done

   967   

   968 lemma [simp]: "fetch t_wcode_main (Suc (t_twice_len + length t_wcode_main_first_part div 2)) Oc

   969      = (L, Suc 0)"

   970 apply(subgoal_tac "length (t_twice) mod 2 = 0")

   971 apply(simp add: t_wcode_main_def nth_append fetch.simps t_wcode_main_first_part_def 

   972   nth_of.simps shift_length t_twice_len_def, auto)

   973 apply(simp add: t_twice_def)

   974 apply(subgoal_tac "length (tm_of abc_twice) mod 2 = 0")

   975 apply arith

   976 apply(rule_tac tm_even)

   977 done

   978 

   979 lemma wcode_jump1: 

   980   "\<exists> stp ln rn. steps (Suc (t_twice_len) + length t_wcode_main_first_part div 2,

   981                        Bk\<^bsup>m\<^esup> @ Bk # Bk # ires, Oc\<^bsup>Suc (2 * rs)\<^esup> @ Bk\<^bsup>n\<^esup>)

   982      t_wcode_main stp 

   983     = (Suc 0, Bk\<^bsup>ln\<^esup> @ Bk # ires, Bk # Oc\<^bsup>Suc (2 * rs)\<^esup> @ Bk\<^bsup>rn\<^esup>)"

   984 apply(rule_tac x = "Suc 0" in exI, rule_tac x = "m" in exI, rule_tac x = n in exI)

   985 apply(simp add: steps.simps tstep.simps exp_ind_def new_tape.simps)

   986 apply(case_tac m, simp, simp add: exp_ind_def)

   987 apply(simp add: exp_ind_def[THEN sym] exp_ind[THEN sym])

   988 done

   989 

   990 lemma wcode_main_first_part_len:

   991   "length t_wcode_main_first_part = 24"

   992   apply(simp add: t_wcode_main_first_part_def)

   993   done

   994 

   995 lemma wcode_double_case: 

   996   shows "\<exists>stp ln rn. steps (Suc 0, Bk # Bk\<^bsup>m\<^esup> @ Oc # Oc # ires, Bk # Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>n\<^esup>) t_wcode_main stp =

   997           (Suc 0, Bk # Bk\<^bsup>ln\<^esup> @ Oc # ires, Bk # Oc\<^bsup>Suc (2 * rs + 2)\<^esup> @ Bk\<^bsup>rn\<^esup>)"

   998 proof -

   999   have "\<exists>stp ln rn. steps (Suc 0, Bk # Bk\<^bsup>m\<^esup> @ Oc # Oc # ires, Bk # Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>n\<^esup>) t_wcode_main stp =

  1000           (13,  Bk # Bk # Bk\<^bsup>ln\<^esup> @ Oc # ires, Oc\<^bsup>Suc (Suc rs)\<^esup> @ Bk\<^bsup>rn\<^esup>)"

  1001     using wcode_double_case_first_correctness[of ires rs m n]

  1002     apply(simp)

  1003     apply(erule_tac exE)

  1004     apply(case_tac "steps (Suc 0, Bk # Bk\<^bsup>m\<^esup> @ Oc # Oc # ires, 

  1005            Bk # Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>n\<^esup>) t_wcode_main na",

  1006           auto simp: wcode_double_case_inv.simps

  1007                      wcode_before_double.simps)

  1008     apply(rule_tac x = na in exI, rule_tac x = ln in exI, rule_tac x = rn in exI)

  1009     apply(simp)

  1010     done    

  1011   from this obtain stpa lna rna where stp1: 

  1012     "steps (Suc 0, Bk # Bk\<^bsup>m\<^esup> @ Oc # Oc # ires, Bk # Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>n\<^esup>) t_wcode_main stpa = 

  1013     (13, Bk # Bk # Bk\<^bsup>lna\<^esup> @ Oc # ires, Oc\<^bsup>Suc (Suc rs)\<^esup> @ Bk\<^bsup>rna\<^esup>)" by blast

  1014   have "\<exists> stp ln rn. steps (13, Bk # Bk # Bk\<^bsup>lna\<^esup> @ Oc # ires, Oc\<^bsup>Suc (Suc rs)\<^esup> @ Bk\<^bsup>rna\<^esup>) t_wcode_main stp =

  1015     (13 + t_twice_len, Bk # Bk # Bk\<^bsup>ln\<^esup> @ Oc # ires, Oc\<^bsup>Suc (Suc (Suc (2 *rs)))\<^esup> @ Bk\<^bsup>rn\<^esup>)"

  1016     using t_twice_append[of "Bk\<^bsup>lna\<^esup> @ Oc # ires" "Suc rs" rna]

  1017     apply(erule_tac exE)

  1018     apply(erule_tac exE)

  1019     apply(erule_tac exE)

  1020     apply(simp add: wcode_main_first_part_len)

  1021     apply(rule_tac x = stp in exI, rule_tac x = "ln + lna" in exI, 

  1022           rule_tac x = rn in exI)

  1023     apply(simp add: t_wcode_main_def)

  1024     apply(simp add: exp_ind_def[THEN sym] exp_add[THEN sym])

  1025     done

  1026   from this obtain stpb lnb rnb where stp2: 

  1027     "steps (13, Bk # Bk # Bk\<^bsup>lna\<^esup> @ Oc # ires, Oc\<^bsup>Suc (Suc rs)\<^esup> @ Bk\<^bsup>rna\<^esup>) t_wcode_main stpb =

  1028     (13 + t_twice_len, Bk # Bk # Bk\<^bsup>lnb\<^esup> @ Oc # ires, Oc\<^bsup>Suc (Suc (Suc (2 *rs)))\<^esup> @ Bk\<^bsup>rnb\<^esup>)" by blast

  1029   have "\<exists>stp ln rn. steps (13 + t_twice_len, Bk # Bk # Bk\<^bsup>lnb\<^esup> @ Oc # ires,

  1030     Oc\<^bsup>Suc (Suc (Suc (2 *rs)))\<^esup> @ Bk\<^bsup>rnb\<^esup>) t_wcode_main stp = 

  1031        (Suc 0,  Bk # Bk\<^bsup>ln\<^esup> @ Oc # ires, Bk # Oc\<^bsup>Suc (Suc (Suc (2 *rs)))\<^esup> @ Bk\<^bsup>rn\<^esup>)"

  1032     using wcode_jump1[of lnb "Oc # ires" "Suc rs" rnb]

  1033     apply(erule_tac exE)

  1034     apply(erule_tac exE)

  1035     apply(erule_tac exE)

  1036     apply(rule_tac x = stp in exI, 

  1037           rule_tac x = ln in exI, 

  1038           rule_tac x = rn in exI, simp add:wcode_main_first_part_len t_wcode_main_def)

  1039     apply(subgoal_tac "Bk\<^bsup>lnb\<^esup> @ Bk # Bk # Oc # ires = Bk # Bk # Bk\<^bsup>lnb\<^esup> @ Oc # ires", simp)

  1040     apply(simp add: exp_ind_def[THEN sym] exp_ind[THEN sym])

  1041     apply(simp)

  1042     apply(case_tac lnb, simp, simp add: exp_ind_def[THEN sym] exp_ind)

  1043     done               

  1044   from this obtain stpc lnc rnc where stp3: 

  1045     "steps (13 + t_twice_len, Bk # Bk # Bk\<^bsup>lnb\<^esup> @ Oc # ires,

  1046     Oc\<^bsup>Suc (Suc (Suc (2 *rs)))\<^esup> @ Bk\<^bsup>rnb\<^esup>) t_wcode_main stpc = 

  1047        (Suc 0,  Bk # Bk\<^bsup>lnc\<^esup> @ Oc # ires, Bk # Oc\<^bsup>Suc (Suc (Suc (2 *rs)))\<^esup> @ Bk\<^bsup>rnc\<^esup>)"

  1048     by blast

  1049   from stp1 stp2 stp3 show "?thesis"

  1050     apply(rule_tac x = "stpa + stpb + stpc" in exI, rule_tac x = lnc in exI,

  1051          rule_tac x = rnc in exI)

  1052     apply(simp add: steps_add)

  1053     done

  1054 qed

  1055     

  1056 

  1057 (* Begin: fourtime_case*)

  1058 fun wcode_on_left_moving_2_B :: "bin_inv_t"

  1059   where

  1060   "wcode_on_left_moving_2_B ires rs (l, r) =

  1061      (\<exists> ml mr rn. l = Bk\<^bsup>ml\<^esup> @ Oc # Bk # Oc # ires \<and>

  1062                  r = Bk\<^bsup>mr\<^esup> @ Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>rn\<^esup> \<and> 

  1063                  ml + mr > Suc 0 \<and> mr > 0)"

  1064 

  1065 fun wcode_on_left_moving_2_O :: "bin_inv_t"

  1066   where

  1067   "wcode_on_left_moving_2_O ires rs (l, r) =

  1068      (\<exists> ln rn. l = Bk # Oc # ires \<and>

  1069                r = Oc # Bk\<^bsup>ln\<^esup> @ Bk # Bk # Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>rn\<^esup>)"

  1070 

  1071 fun wcode_on_left_moving_2 :: "bin_inv_t"

  1072   where

  1073   "wcode_on_left_moving_2 ires rs (l, r) = 

  1074       (wcode_on_left_moving_2_B ires rs (l, r) \<or> 

  1075       wcode_on_left_moving_2_O ires rs (l, r))"

  1076 

  1077 fun wcode_on_checking_2 :: "bin_inv_t"

  1078   where

  1079   "wcode_on_checking_2 ires rs (l, r) =

  1080        (\<exists> ln rn. l = Oc#ires \<and> 

  1081                  r = Bk # Oc # Bk\<^bsup>ln\<^esup> @ Bk # Bk # Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>rn\<^esup>)"

  1082 

  1083 fun wcode_goon_checking :: "bin_inv_t"

  1084   where

  1085   "wcode_goon_checking ires rs (l, r) =

  1086        (\<exists> ln rn. l = ires \<and>

  1087                  r = Oc # Bk # Oc # Bk\<^bsup>ln\<^esup> @ Bk # Bk # Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>rn\<^esup>)"

  1088 

  1089 fun wcode_right_move :: "bin_inv_t"

  1090   where

  1091   "wcode_right_move ires rs (l, r) = 

  1092      (\<exists> ln rn. l = Oc # ires \<and>

  1093                  r = Bk # Oc # Bk\<^bsup>ln\<^esup> @ Bk # Bk # Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>rn\<^esup>)"

  1094 

  1095 fun wcode_erase2 :: "bin_inv_t"

  1096   where

  1097   "wcode_erase2 ires rs (l, r) = 

  1098         (\<exists> ln rn. l = Bk # Oc # ires \<and>

  1099                  tl r = Bk\<^bsup>ln\<^esup> @ Bk # Bk # Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>rn\<^esup>)"

  1100 

  1101 fun wcode_on_right_moving_2 :: "bin_inv_t"

  1102   where

  1103   "wcode_on_right_moving_2 ires rs (l, r) = 

  1104         (\<exists> ml mr rn. l = Bk\<^bsup>ml\<^esup> @ Oc # ires \<and> 

  1105                      r = Bk\<^bsup>mr\<^esup> @ Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>rn\<^esup> \<and> ml + mr > Suc 0)"

  1106 

  1107 fun wcode_goon_right_moving_2 :: "bin_inv_t"

  1108   where

  1109   "wcode_goon_right_moving_2 ires rs (l, r) = 

  1110         (\<exists> ml mr ln rn. l = Oc\<^bsup>ml\<^esup> @ Bk # Bk # Bk\<^bsup>ln\<^esup> @ Oc # ires \<and>

  1111                         r = Oc\<^bsup>mr\<^esup> @ Bk\<^bsup>rn\<^esup> \<and> ml + mr = Suc rs)"

  1112 

  1113 fun wcode_backto_standard_pos_2_B :: "bin_inv_t"

  1114   where

  1115   "wcode_backto_standard_pos_2_B ires rs (l, r) = 

  1116            (\<exists> ln rn. l = Bk # Bk\<^bsup>ln\<^esup> @ Oc # ires \<and> 

  1117                      r = Bk # Oc\<^bsup>Suc (Suc rs)\<^esup> @ Bk\<^bsup>rn\<^esup>)"

  1118 

  1119 fun wcode_backto_standard_pos_2_O :: "bin_inv_t"

  1120   where

  1121   "wcode_backto_standard_pos_2_O ires rs (l, r) = 

  1122           (\<exists> ml mr ln rn. l = Oc\<^bsup>ml \<^esup>@ Bk # Bk # Bk\<^bsup>ln\<^esup> @ Oc # ires \<and> 

  1123                           r = Oc\<^bsup>mr\<^esup> @ Bk\<^bsup>rn\<^esup> \<and> 

  1124                           ml + mr = (Suc (Suc rs)) \<and> mr > 0)"

  1125 

  1126 fun wcode_backto_standard_pos_2 :: "bin_inv_t"

  1127   where

  1128   "wcode_backto_standard_pos_2 ires rs (l, r) = 

  1129            (wcode_backto_standard_pos_2_O ires rs (l, r) \<or> 

  1130            wcode_backto_standard_pos_2_B ires rs (l, r))"

  1131 

  1132 fun wcode_before_fourtimes :: "bin_inv_t"

  1133   where

  1134   "wcode_before_fourtimes ires rs (l, r) = 

  1135           (\<exists> ln rn. l = Bk # Bk # Bk\<^bsup>ln\<^esup> @ Oc # ires \<and>