1 theory turing_basic

     2 imports Main

     3 begin

     4 

     5 section {* Basic definitions of Turing machine *}

     6 

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

     8    Author: Xu Jian <xujian817@hotmail.com>

     9    Maintainer: Xu Jian

    10 *)

    11 

    12 text {*

    13 \label{description of turing machine}

    14 *}

    15 

    16 section {* Basic definitions of Turing machine *}

    17 

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

    19    Author: Xu Jian <xujian817@hotmail.com>

    20    Maintainer: Xu Jian

    21 *)

    22 

    23 text {*

    24   Actions of Turing machine (Abbreviated TM in the following* ).

    25 *}

    26 

    27 datatype taction = 

    28   -- {* Write zero *}

    29   W0 | 

    30   -- {* Write one *}

    31   W1 | 

    32   -- {* Move left *}

    33   L | 

    34   -- {* Move right *}

    35   R | 

    36   -- {* Do nothing *}

    37   Nop

    38 

    39 text {*

    40   Tape contents in every block.

    41 *}

    42 

    43 datatype block = 

    44   -- {* Blank *}

    45   Bk | 

    46   -- {* Occupied *}

    47   Oc

    48 

    49 text {*

    50   Tape is represented as a pair of lists $(L_{left}, L_{right})$,

    51   where $L_left$, named {\em left list}, is used to represent

    52   the tape to the left of RW-head and

    53   $L_{right}$, named {\em right list}, is used to represent the tape

    54   under and to the right of RW-head.

    55 *}

    56 

    57 type_synonym tape = "block list \<times> block list"

    58 

    59 text {* The state of turing machine.*}

    60 type_synonym tstate = nat

    61 

    62 text {*

    63   Turing machine instruction is represented as a 

    64   pair @{text "(action, next_state)"},

    65   where @{text "action"} is the action to take at the current state 

    66   and @{text "next_state"} is the next state the machine is getting into

    67   after the action.

    68 *}

    69 type_synonym tinst = "taction \<times> tstate"

    70 

    71 text {*

    72   Program of Turing machine is represented as a list of Turing instructions

    73   and the execution of the program starts from the head of the list.

    74   *}

    75 type_synonym tprog = "tinst list"

    76 

    77 

    78 text {*

    79   Turing machine configuration, which consists of the current state 

    80   and the tape.

    81 *}

    82 type_synonym t_conf = "tstate \<times> tape"

    83 

    84 fun nth_of ::  "'a list \<Rightarrow> nat \<Rightarrow> 'a option"

    85   where

    86   "nth_of xs n = (if n < length xs then Some (xs!n)

    87                   else None)"

    88 

    89 text {*

    90   The function used to fetech instruction out of Turing program.

    91   *}

    92 

    93 fun fetch :: "tprog \<Rightarrow> tstate \<Rightarrow> block \<Rightarrow> tinst"

    94   where

    95   "fetch p s b = (if s = 0 then (Nop, 0) else

    96                   case b of 

    97                      Bk \<Rightarrow> case nth_of p (2 * (s - 1)) of

    98                           Some i \<Rightarrow> i

    99                         | None \<Rightarrow> (Nop, 0) 

   100                    | Oc \<Rightarrow> case nth_of p (2 * (s - 1) +1) of

   101                           Some i \<Rightarrow> i

   102                         | None \<Rightarrow> (Nop, 0))"

   103 

   104 

   105 fun new_tape :: "taction \<Rightarrow> tape \<Rightarrow> tape"

   106 where 

   107    "new_tape action (leftn, rightn) = (case action of

   108                                          W0 \<Rightarrow> (leftn, Bk#(tl rightn)) |

   109                                          W1 \<Rightarrow> (leftn, Oc#(tl rightn)) |

   110                                          L  \<Rightarrow>  (if leftn = [] then (tl leftn, Bk#rightn)

   111                                                else (tl leftn, (hd leftn) # rightn)) |

   112                                          R  \<Rightarrow> if rightn = [] then (Bk#leftn,tl rightn) 

   113                                                else ((hd rightn)#leftn, tl rightn) |

   114                                          Nop \<Rightarrow> (leftn, rightn)

   115                                        )"

   116 

   117 text {*

   118   The one step function used to transfer Turing machine configuration.

   119 *}

   120 fun tstep :: "t_conf \<Rightarrow> tprog \<Rightarrow> t_conf"

   121   where

   122   "tstep c p = (let (s, l, r) = c in 

   123                      let (ac, ns) = (fetch p s (case r of [] \<Rightarrow> Bk |     

   124                                                                x # xs \<Rightarrow> x)) in

   125                        (ns, new_tape ac (l, r)))"

   126 

   127 text {*

   128   The many-step function.

   129 *}

   130 fun steps :: "t_conf \<Rightarrow> tprog \<Rightarrow> nat \<Rightarrow> t_conf"

   131   where

   132   "steps c p 0 = c" |

   133   "steps c p (Suc n) = steps (tstep c p) p n"

   134 

   135 lemma tstep_red: "steps c p (Suc n) = tstep (steps c p n) p"

   136 proof(induct n arbitrary: c)

   137   fix c

   138   show "steps c p (Suc 0) = tstep (steps c p 0) p" by(simp add: steps.simps)

   139 next

   140   fix n c

   141   assume ind: "\<And> c. steps c p (Suc n) = tstep (steps c p n) p"

   142   have "steps (tstep c p) p (Suc n) = tstep (steps (tstep c p) p n) p"

   143     by(rule ind)

   144   thus "steps c p (Suc (Suc n)) = tstep (steps c p (Suc n)) p" by(simp add: steps.simps)

   145 qed

   146 

   147 declare Let_def[simp] option.split[split]

   148 

   149 definition 

   150   "iseven n \<equiv> \<exists> x. n = 2 * x"

   151 

   152 

   153 text {*

   154   The following @{text "t_correct"} function is used to specify the wellformedness of Turing

   155   machine.

   156 *}

   157 fun t_correct :: "tprog \<Rightarrow> bool"

   158   where

   159   "t_correct p = (length p \<ge> 2 \<and> iseven (length p) \<and> 

   160                    list_all (\<lambda> (acn, s). s \<le> length p div 2) p)"

   161 

   162 declare t_correct.simps[simp del]

   163 

   164 lemma allimp: "\<lbrakk>\<forall>x. P x \<longrightarrow> Q x; \<forall>x. P x\<rbrakk> \<Longrightarrow> \<forall>x. Q x"

   165 by(auto elim: allE)

   166 

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

   168 apply(rule exCI, drule allimp, auto)

   169 apply(drule_tac f = f  in wf_inv_image, simp add: inv_image_def)

   170 apply(erule wf_induct, auto)

   171 done

   172 

   173 lemma steps_add: "steps c t (x + y) = steps (steps c t x) t y"

   174 by(induct x arbitrary: c, auto simp: steps.simps tstep_red)

   175 

   176 lemma listall_set: "list_all p t \<Longrightarrow> \<forall> a \<in> set t. p a"

   177 by(induct t, auto)

   178 

   179 lemma fetch_ex: "\<exists>b a. fetch T aa ab = (b, a)"

   180 by(simp add: fetch.simps)

   181 definition exponent :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" ("_\<^bsup>_\<^esup>" [0, 0]100)

   182   where "exponent x n = replicate n x"

   183 

   184 text {* 

   185   @{text "tinres l1 l2"} means left list @{text "l1"} is congruent with

   186   @{text "l2"} with respect to the execution of Turing machine. 

   187   Appending Blank to the right of eigther one does not affect the 

   188   outcome of excution. 

   189 *}

   190 

   191 definition tinres :: "block list \<Rightarrow> block list \<Rightarrow> bool"

   192   where

   193   "tinres bx by = (\<exists> n. bx = by@Bk\<^bsup>n\<^esup> \<or> by = bx @ Bk\<^bsup>n\<^esup>)"

   194 

   195 lemma exp_zero: "a\<^bsup>0\<^esup> = []"

   196 by(simp add: exponent_def)

   197 lemma exp_ind_def: "a\<^bsup>Suc x \<^esup> = a # a\<^bsup>x\<^esup>"

   198 by(simp add: exponent_def)

   199 

   200 text {*

   201   The following lemma shows the meaning of @{text "tinres"} with respect to 

   202   one step execution.

   203   *}

   204 lemma tinres_step: 

   205   "\<lbrakk>tinres l l'; tstep (ss, l, r) t = (sa, la, ra); tstep (ss, l', r) t = (sb, lb, rb)\<rbrakk>

   206     \<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb"

   207 apply(auto simp: tstep.simps fetch.simps new_tape.simps 

   208         split: if_splits taction.splits list.splits

   209                  block.splits)

   210 apply(case_tac [!] "t ! (2 * (ss - Suc 0))", 

   211      auto simp: exponent_def tinres_def split: if_splits taction.splits list.splits

   212                  block.splits)

   213 apply(case_tac [!] "t ! (2 * (ss - Suc 0) + Suc 0)", 

   214      auto simp: exponent_def tinres_def split: if_splits taction.splits list.splits

   215                  block.splits)

   216 done

   217 

   218 declare tstep.simps[simp del] steps.simps[simp del]

   219 

   220 text {*

   221   The following lemma shows the meaning of @{text "tinres"} with respect to 

   222   many step execution.

   223   *}

   224 lemma tinres_steps: 

   225   "\<lbrakk>tinres l l'; steps (ss, l, r) t stp = (sa, la, ra); steps (ss, l', r) t stp = (sb, lb, rb)\<rbrakk>

   226     \<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb"

   227 apply(induct stp arbitrary: sa la ra sb lb rb, simp add: steps.simps)

   228 apply(simp add: tstep_red)

   229 apply(case_tac "(steps (ss, l, r) t stp)")

   230 apply(case_tac "(steps (ss, l', r) t stp)")

   231 proof -

   232   fix stp sa la ra sb lb rb a b c aa ba ca

   233   assume ind: "\<And>sa la ra sb lb rb. \<lbrakk>steps (ss, l, r) t stp = (sa, la, ra); 

   234           steps (ss, l', r) t stp = (sb, lb, rb)\<rbrakk> \<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb"

   235   and h: " tinres l l'" "tstep (steps (ss, l, r) t stp) t = (sa, la, ra)"

   236          "tstep (steps (ss, l', r) t stp) t = (sb, lb, rb)" "steps (ss, l, r) t stp = (a, b, c)" 

   237          "steps (ss, l', r) t stp = (aa, ba, ca)"

   238   have "tinres b ba \<and> c = ca \<and> a = aa"

   239     apply(rule_tac ind, simp_all add: h)

   240     done

   241   thus "tinres la lb \<and> ra = rb \<and> sa = sb"

   242     apply(rule_tac l = b and l' = ba and r = c  and ss = a   

   243             and t = t in tinres_step)

   244     using h

   245     apply(simp, simp, simp)

   246     done

   247 qed

   248 

   249 text {*

   250   The following function @{text "tshift tp n"} is used to shift Turing programs 

   251   @{text "tp"} by @{text "n"} when it is going to be combined with others.

   252   *}

   253 

   254 fun tshift :: "tprog \<Rightarrow> nat \<Rightarrow> tprog"

   255   where

   256   "tshift tp off = (map (\<lambda> (action, state). (action, (if state = 0 then 0

   257                                                       else state + off))) tp)"

   258 

   259 text {*

   260   When two Turing programs are combined, the end state (state @{text "0"}) of the one 

   261   at the prefix position needs to be connected to the start state 

   262   of the one at postfix position. If @{text "tp"} is the Turing program

   263   to be at the prefix, @{text "change_termi_state tp"} is the transformed Turing program.

   264   *}

   265 fun change_termi_state :: "tprog \<Rightarrow> tprog"

   266   where

   267   "change_termi_state t = 

   268        (map (\<lambda> (acn, ns). if ns = 0 then (acn, Suc ((length t) div 2)) else (acn, ns)) t)"

   269 

   270 text {*

   271   @{text "t_add tp1 tp2"} is the combined Truing program.

   272 *}

   273 

   274 fun t_add :: "tprog \<Rightarrow> tprog \<Rightarrow> tprog" ("_ |+| _" [0, 0] 100)

   275   where

   276   "t_add t1 t2 = ((change_termi_state t1) @ (tshift t2 ((length t1) div 2)))"

   277 

   278 text {*

   279   Tests whether the current configuration is at state @{text "0"}.

   280 *}

   281 definition isS0 :: "t_conf \<Rightarrow> bool"

   282   where

   283   "isS0 c = (let (s, l, r) = c in s = 0)"

   284 

   285 declare tstep.simps[simp del] steps.simps[simp del] 

   286         t_add.simps[simp del] fetch.simps[simp del]

   287         new_tape.simps[simp del]

   288 

   289 

   290 text {*

   291   Single step execution starting from state @{text "0"} will not make any progress.

   292 *}

   293 lemma tstep_0: "tstep (0, tp) p = (0, tp)"

   294 apply(simp add: tstep.simps fetch.simps new_tape.simps)

   295 done

   296 

   297 

   298 text {*

   299   Many step executions starting from state @{text "0"} will not make any progress.

   300 *}

   301 

   302 lemma steps_0: "steps (0, tp) p stp = (0, tp)"

   303 apply(induct stp)

   304 apply(simp add: steps.simps)

   305 apply(simp add: tstep_red tstep_0)

   306 done

   307 

   308 lemma s_keep_step: "\<lbrakk>a \<le> length A div 2; tstep (a, b, c) A = (s, l, r); t_correct A\<rbrakk>

   309   \<Longrightarrow> s \<le> length A div 2"

   310 apply(simp add: tstep.simps fetch.simps t_correct.simps iseven_def 

   311   split: if_splits block.splits list.splits)

   312 apply(case_tac [!] a, auto simp: list_all_length)

   313 apply(erule_tac x = "2 * nat" in allE, auto)

   314 apply(erule_tac x = "2 * nat" in allE, auto)

   315 apply(erule_tac x = "Suc (2 * nat)" in allE, auto)

   316 done

   317 

   318 lemma s_keep: "\<lbrakk>steps (Suc 0, tp) A stp = (s, l, r);  t_correct A\<rbrakk> \<Longrightarrow> s \<le> length A div 2"

   319 proof(induct stp arbitrary: s l r)

   320   case 0 thus "?case" by(auto simp: t_correct.simps steps.simps)

   321 next

   322   fix stp s l r

   323   assume ind: "\<And>s l r. \<lbrakk>steps (Suc 0, tp) A stp = (s, l, r); t_correct A\<rbrakk> \<Longrightarrow> s \<le> length A div 2"

   324   and h1: "steps (Suc 0, tp) A (Suc stp) = (s, l, r)"

   325   and h2: "t_correct A"

   326   from h1 h2 show "s \<le> length A div 2"

   327   proof(simp add: tstep_red, cases "(steps (Suc 0, tp) A stp)", simp)

   328     fix a b c 

   329     assume h3: "tstep (a, b, c) A = (s, l, r)"

   330     and h4: "steps (Suc 0, tp) A stp = (a, b, c)"

   331     have "a \<le> length A div 2"

   332       using h2 h4

   333       by(rule_tac l = b and r = c in ind, auto)

   334     thus "?thesis"

   335       using h3 h2

   336       by(simp add: s_keep_step)

   337   qed

   338 qed

   339 

   340 lemma t_merge_fetch_pre:

   341   "\<lbrakk>fetch A s b = (ac, ns); s \<le> length A div 2; t_correct A; s \<noteq> 0\<rbrakk> \<Longrightarrow> 

   342   fetch (A |+| B) s b = (ac, if ns = 0 then Suc (length A div 2) else ns)"

   343 apply(subgoal_tac "2 * (s - Suc 0) < length A \<and> Suc (2 * (s - Suc 0)) < length A")

   344 apply(auto simp: fetch.simps t_add.simps split: if_splits block.splits)

   345 apply(simp_all add: nth_append change_termi_state.simps)

   346 done

   347 

   348 lemma [simp]:  "\<lbrakk>\<not> a \<le> length A div 2; t_correct A\<rbrakk> \<Longrightarrow> fetch A a b = (Nop, 0)"

   349 apply(auto simp: fetch.simps del: nth_of.simps split: block.splits)

   350 apply(case_tac [!] a, auto simp: t_correct.simps iseven_def)

   351 done

   352 

   353 lemma  [elim]: "\<lbrakk>t_correct A; \<not> isS0 (tstep (a, b, c) A)\<rbrakk> \<Longrightarrow> a \<le> length A div 2"

   354 apply(rule_tac classical, auto simp: tstep.simps new_tape.simps isS0_def)

   355 done

   356 

   357 lemma [elim]: "\<lbrakk>t_correct A; \<not> isS0 (tstep (a, b, c) A)\<rbrakk> \<Longrightarrow> 0 < a"

   358 apply(rule_tac classical, simp add: tstep_0 isS0_def)

   359 done

   360 

   361 

   362 lemma t_merge_pre_eq_step: "\<lbrakk>tstep (a, b, c) A = cf; t_correct A; \<not> isS0 cf\<rbrakk> 

   363         \<Longrightarrow> tstep (a, b, c) (A |+| B) = cf"

   364 apply(subgoal_tac "a \<le> length A div 2 \<and> a \<noteq> 0")

   365 apply(simp add: tstep.simps)

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

   367 apply(drule_tac B = B in t_merge_fetch_pre, simp, simp, simp, simp add: isS0_def, auto)

   368 done

   369 

   370 lemma t_merge_pre_eq:  "\<lbrakk>steps (Suc 0, tp) A stp = cf; \<not> isS0 cf; t_correct A\<rbrakk>

   371     \<Longrightarrow> steps (Suc 0, tp) (A |+| B) stp = cf"

   372 proof(induct stp arbitrary: cf)

   373   case 0 thus "?case" by(simp add: steps.simps)

   374 next

   375   fix stp cf

   376   assume ind: "\<And>cf. \<lbrakk>steps (Suc 0, tp) A stp = cf; \<not> isS0 cf; t_correct A\<rbrakk> 

   377                  \<Longrightarrow> steps (Suc 0, tp) (A |+| B) stp = cf"

   378   and h1: "steps (Suc 0, tp) A (Suc stp) = cf"

   379   and h2: "\<not> isS0 cf"

   380   and h3: "t_correct A"

   381   from h1 h2 h3 show "steps (Suc 0, tp) (A |+| B) (Suc stp) = cf"

   382   proof(simp add: tstep_red, cases "steps (Suc 0, tp) (A) stp", simp)

   383     fix a b c

   384     assume h4: "tstep (a, b, c) A = cf"

   385     and h5: "steps (Suc 0, tp) A stp = (a, b, c)"

   386     have "steps (Suc 0, tp) (A |+| B) stp = (a, b, c)"

   387     proof(cases a)

   388       case 0 thus "?thesis"

   389         using h4 h2

   390         apply(simp add: tstep_0, cases cf, simp add: isS0_def)

   391         done

   392     next

   393       case (Suc n) thus "?thesis"

   394         using h5 h3

   395         apply(rule_tac ind, auto simp: isS0_def)

   396         done

   397     qed

   398     thus "tstep (steps (Suc 0, tp) (A |+| B) stp) (A |+| B) = cf"

   399       using h4 h5 h3 h2

   400       apply(simp)

   401       apply(rule t_merge_pre_eq_step, auto)

   402       done

   403   qed

   404 qed

   405 

   406 declare nth.simps[simp del] tshift.simps[simp del] change_termi_state.simps[simp del]

   407 

   408 lemma [simp]: "length (change_termi_state A) = length A"

   409 by(simp add: change_termi_state.simps)

   410 

   411 lemma first_halt_point: "steps (Suc 0, tp) A stp = (0, tp')

   412  \<Longrightarrow> \<exists>stp. \<not> isS0 (steps (Suc 0, tp) A stp) \<and> steps (Suc 0, tp) A (Suc stp) = (0, tp')"

   413 proof(induct stp)

   414   case 0  thus "?case" by(simp add: steps.simps)

   415 next

   416   case (Suc n) 

   417   fix stp

   418   assume ind: "steps (Suc 0, tp) A stp = (0, tp') \<Longrightarrow> 

   419        \<exists>stp. \<not> isS0 (steps (Suc 0, tp) A stp) \<and> steps (Suc 0, tp) A (Suc stp) = (0, tp')"

   420     and h: "steps (Suc 0, tp) A (Suc stp) = (0, tp')"

   421   from h show "\<exists>stp. \<not> isS0 (steps (Suc 0, tp) A stp) \<and> steps (Suc 0, tp) A (Suc stp) = (0, tp')"

   422   proof(simp add: tstep_red, cases "steps (Suc 0, tp) A stp", simp, case_tac a)

   423     fix a b c

   424     assume g1: "a = (0::nat)"

   425     and g2: "tstep (a, b, c) A = (0, tp')"

   426     and g3: "steps (Suc 0, tp) A stp = (a, b, c)"

   427     have "steps (Suc 0, tp) A stp = (0, tp')"

   428       using g2 g1 g3

   429       by(simp add: tstep_0)

   430     hence "\<exists> stp. \<not> isS0 (steps (Suc 0, tp) A stp) \<and> steps (Suc 0, tp) A (Suc stp) = (0, tp')"

   431       by(rule ind)

   432     thus "\<exists>stp. \<not> isS0 (steps (Suc 0, tp) A stp) \<and> tstep (steps (Suc 0, tp) A stp) A = (0, tp')" 

   433       apply(simp add: tstep_red)

   434       done

   435   next

   436     fix a b c nat

   437     assume g1: "steps (Suc 0, tp) A stp = (a, b, c)"

   438     and g2: "steps (Suc 0, tp) A (Suc stp) = (0, tp')" "a= Suc nat"

   439     thus "\<exists>stp. \<not> isS0 (steps (Suc 0, tp) A stp) \<and> tstep (steps (Suc 0, tp) A stp) A = (0, tp')"

   440       apply(rule_tac x = stp in exI)

   441       apply(simp add: isS0_def tstep_red)

   442       done

   443   qed

   444 qed 

   445    

   446 lemma t_merge_pre_halt_same': 

   447   "\<lbrakk>\<not> isS0 (steps (Suc 0, tp) A stp) ; steps (Suc 0, tp) A (Suc stp) = (0, tp'); t_correct A\<rbrakk>

   448   \<Longrightarrow> steps (Suc 0, tp) (A |+| B) (Suc stp) = (Suc (length A div 2), tp')"    

   449 proof(simp add: tstep_red, cases "steps (Suc 0, tp) A stp", simp)

   450   fix a b c 

   451   assume h1: "\<not> isS0 (a, b, c)"

   452   and h2: "tstep (a, b, c) A = (0, tp')"

   453   and h3: "t_correct A"

   454   and h4: "steps (Suc 0, tp) A stp = (a, b, c)"

   455   have "steps (Suc 0, tp) (A |+| B) stp = (a, b, c)"

   456     using h1 h4 h3

   457     apply(rule_tac  t_merge_pre_eq, auto)

   458     done

   459   moreover have "tstep (a, b, c) (A |+| B) = (Suc (length A div 2), tp')"

   460     using h2 h3 h1 h4 

   461     apply(simp add: tstep.simps)

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

   463     apply(drule_tac B = B in t_merge_fetch_pre, auto simp: isS0_def intro: s_keep)

   464     done

   465   ultimately show "tstep (steps (Suc 0, tp) (A |+| B) stp) (A |+| B) = (Suc (length A div 2), tp')"

   466     by(simp)

   467 qed

   468 

   469 text {*

   470   When Turing machine @{text "A"} and @{text "B"} are combined and the execution

   471   of @{text "A"} can termination within @{text "stp"} steps, 

   472   the combined machine @{text "A |+| B"} will eventually get into the starting 

   473   state of machine @{text "B"}.

   474 *}

   475 lemma t_merge_pre_halt_same: "

   476   \<lbrakk>steps (Suc 0, tp) A stp = (0, tp'); t_correct A; t_correct B\<rbrakk>

   477      \<Longrightarrow> \<exists> stp. steps (Suc 0, tp) (A |+| B) stp = (Suc (length A div 2), tp')"

   478 proof -

   479   assume a_wf: "t_correct A"

   480   and b_wf: "t_correct B"

   481   and a_ht: "steps (Suc 0, tp) A stp = (0, tp')"

   482   have halt_point: "\<exists> stp. \<not> isS0 (steps (Suc 0, tp) A stp) \<and> steps (Suc 0, tp) A (Suc stp) = (0, tp')"

   483     using a_ht

   484     by(erule_tac first_halt_point)

   485   then obtain stp' where "\<not> isS0 (steps (Suc 0, tp) A stp') \<and> steps (Suc 0, tp) A (Suc stp') = (0, tp')"..

   486   hence "steps (Suc 0, tp) (A |+| B) (Suc stp') = (Suc (length A div 2), tp')"

   487     using a_wf

   488     apply(rule_tac t_merge_pre_halt_same', auto)

   489     done

   490   thus "?thesis" ..

   491 qed

   492 

   493 lemma fetch_0: "fetch p 0 b = (Nop, 0)"

   494 by(simp add: fetch.simps)

   495 

   496 lemma [simp]: "length (tshift B x) = length B"

   497 by(simp add: tshift.simps)

   498 

   499 lemma [simp]: "t_correct A \<Longrightarrow> 2 * (length A div 2) = length A"

   500 apply(simp add: t_correct.simps iseven_def, auto)

   501 done

   502 

   503 lemma t_merge_fetch_snd: 

   504   "\<lbrakk>fetch B a b = (ac, ns); t_correct A; t_correct B; a > 0 \<rbrakk>

   505   \<Longrightarrow> fetch (A |+| B) (a + length A div 2) b

   506   = (ac, if ns = 0 then 0 else ns + length A div 2)"

   507 apply(auto simp: fetch.simps t_add.simps split: if_splits block.splits)

   508 apply(case_tac [!] a, simp_all)

   509 apply(simp_all add: nth_append change_termi_state.simps tshift.simps)

   510 done

   511 

   512 lemma t_merge_snd_eq_step: 

   513   "\<lbrakk>tstep (s, l, r) B = (s', l', r'); t_correct A; t_correct B; s > 0\<rbrakk>

   514     \<Longrightarrow> tstep (s + length A div 2, l, r) (A |+| B) = 

   515        (if s' = 0 then 0 else s' + length A div 2, l' ,r') "

   516 apply(simp add: tstep.simps)

   517 apply(cases "fetch B s (case r of [] \<Rightarrow> Bk | x # xs \<Rightarrow> x)")

   518 apply(auto simp: t_merge_fetch_snd)

   519 apply(frule_tac [!] t_merge_fetch_snd, auto)

   520 done 

   521 

   522 text {*

   523   Relates the executions of TM @{text "B"}, one is when @{text "B"} is executed alone,

   524   the other is the execution when @{text "B"} is in the combined TM.

   525 *}

   526 lemma t_merge_snd_eq_steps: 

   527   "\<lbrakk>t_correct A; t_correct B; steps (s, l, r) B stp = (s', l', r'); s > 0\<rbrakk>

   528   \<Longrightarrow> steps (s + length A div 2, l, r) (A |+| B) stp = 

   529       (if s' = 0 then 0 else s' + length A div 2, l', r')"

   530 proof(induct stp arbitrary: s' l' r')

   531   case 0 thus "?case" 

   532     by(simp add: steps.simps)

   533 next

   534   fix stp s' l' r'

   535   assume ind: "\<And>s' l' r'. \<lbrakk>t_correct A; t_correct B; steps (s, l, r) B stp = (s', l', r'); 0 < s\<rbrakk>

   536                    \<Longrightarrow> steps (s + length A div 2, l, r) (A |+| B) stp = 

   537                           (if s' = 0 then 0 else s' + length A div 2, l', r')"

   538   and h1: "steps (s, l, r) B (Suc stp) = (s', l', r')"

   539   and h2: "t_correct A"

   540   and h3: "t_correct B"

   541   and h4: "0 < s"

   542   from h1 show "steps (s + length A div 2, l, r) (A |+| B) (Suc stp) 

   543             = (if s' = 0 then 0 else s' + length A div 2, l', r')"

   544   proof(simp only: tstep_red, cases "steps (s, l, r) B stp")

   545     fix a b c 

   546     assume h5: "steps (s, l, r) B stp = (a, b, c)" "tstep (steps (s, l, r) B stp) B = (s', l', r')"

   547     hence h6: "(steps (s + length A div 2, l, r) (A |+| B) stp) = 

   548                 ((if a = 0 then 0 else a + length A div 2, b, c))"

   549       using h2 h3 h4

   550       by(rule_tac ind, auto)

   551     thus "tstep (steps (s + length A div 2, l, r) (A |+| B) stp) (A |+| B) = 

   552        (if s' = 0 then 0 else s'+ length A div 2, l', r')"

   553       using h5

   554     proof(auto)

   555       assume "tstep (0, b, c) B = (0, l', r')" thus "tstep (0, b, c) (A |+| B) = (0, l', r')"

   556         by(simp add: tstep_0)

   557     next

   558       assume "tstep (0, b, c) B = (s', l', r')" "0 < s'"

   559       thus "tstep (0, b, c) (A |+| B) = (s' + length A div 2, l', r')"

   560         by(simp add: tstep_0)

   561     next

   562       assume "tstep (a, b, c) B = (0, l', r')" "0 < a"

   563       thus "tstep (a + length A div 2, b, c) (A |+| B) = (0, l', r')"

   564         using h2 h3

   565         by(drule_tac t_merge_snd_eq_step, auto)

   566     next

   567       assume "tstep (a, b, c) B = (s', l', r')" "0 < a" "0 < s'"

   568       thus "tstep (a + length A div 2, b, c) (A |+| B) = (s' + length A div 2, l', r')"

   569         using h2 h3

   570         by(drule_tac t_merge_snd_eq_step, auto)

   571     qed

   572   qed

   573 qed

   574 

   575 lemma t_merge_snd_halt_eq: 

   576   "\<lbrakk>steps (Suc 0, tp) B stp = (0, tp'); t_correct A; t_correct B\<rbrakk>

   577   \<Longrightarrow> \<exists>stp. steps (Suc (length A div 2), tp) (A |+| B) stp = (0, tp')"

   578 apply(case_tac tp, cases tp', simp)

   579 apply(drule_tac  s = "Suc 0" in t_merge_snd_eq_steps, auto)

   580 done

   581 

   582 lemma t_inj: "\<lbrakk>steps (Suc 0, tp) A stpa = (0, tp1); steps (Suc 0, tp) A stpb = (0, tp2)\<rbrakk> 

   583       \<Longrightarrow> tp1 = tp2"

   584 proof -

   585   assume h1: "steps (Suc 0, tp) A stpa = (0, tp1)" 

   586   and h2: "steps (Suc 0, tp) A stpb = (0, tp2)"

   587   thus "?thesis"

   588   proof(cases "stpa < stpb")

   589     case True thus "?thesis"

   590       using h1 h2

   591       apply(drule_tac less_imp_Suc_add, auto)

   592       apply(simp del: add_Suc_right add_Suc add: add_Suc_right[THEN sym] steps_add steps_0)

   593       done

   594   next

   595     case False thus "?thesis"

   596       using h1 h2

   597       apply(drule_tac leI)

   598       apply(case_tac "stpb = stpa", auto)

   599       apply(subgoal_tac "stpb < stpa")

   600       apply(drule_tac less_imp_Suc_add, auto)

   601       apply(simp del: add_Suc_right add_Suc add: add_Suc_right[THEN sym] steps_add steps_0)

   602       done

   603   qed

   604 qed

   605 

   606 type_synonym t_assert = "tape \<Rightarrow> bool"

   607 

   608 definition t_imply :: "t_assert \<Rightarrow> t_assert \<Rightarrow> bool" ("_ \<turnstile>-> _" [0, 0] 100)

   609   where

   610   "t_imply a1 a2 = (\<forall> tp. a1 tp \<longrightarrow> a2 tp)"

   611 

   612 

   613 locale turing_merge =

   614   fixes A :: "tprog" and B :: "tprog" and P1 :: "t_assert"

   615   and P2 :: "t_assert"

   616   and P3 :: "t_assert"

   617   and P4 :: "t_assert"

   618   and Q1:: "t_assert"

   619   and Q2 :: "t_assert"

   620   assumes 

   621   A_wf : "t_correct A"

   622   and B_wf : "t_correct B"

   623   and A_halt : "P1 tp \<Longrightarrow> \<exists> stp. let (s, tp') = steps (Suc 0, tp) A stp in s = 0 \<and> Q1 tp'"

   624   and B_halt : "P2 tp \<Longrightarrow> \<exists> stp. let (s, tp') = steps (Suc 0, tp) B stp in s = 0 \<and> Q2 tp'"

   625   and A_uhalt : "P3 tp \<Longrightarrow> \<not> (\<exists> stp. isS0 (steps (Suc 0, tp) A stp))"

   626   and B_uhalt: "P4 tp \<Longrightarrow> \<not> (\<exists> stp. isS0 (steps (Suc 0, tp) B stp))"

   627 begin

   628 

   629 

   630 text {*

   631   The following lemma tries to derive the Hoare logic rule for sequentially combined TMs.

   632   It deals with the situtation when both @{text "A"} and @{text "B"} are terminated.

   633 *}

   634 

   635 lemma t_merge_halt: 

   636   assumes aimpb: "Q1 \<turnstile>-> P2"

   637   shows "P1 \<turnstile>->  \<lambda> tp. (\<exists> stp tp'. steps (Suc 0, tp) (A |+| B)  stp = (0, tp') \<and> Q2 tp')"

   638 proof(simp add: t_imply_def, auto)

   639   fix a b

   640   assume h: "P1 (a, b)"

   641   hence "\<exists> stp. let (s, tp') = steps (Suc 0, a, b) A stp in s = 0 \<and> Q1 tp'"

   642     using A_halt by simp

   643   from this obtain stp1 where "let (s, tp') = steps (Suc 0, a, b) A stp1 in s = 0 \<and> Q1 tp'" ..

   644   thus "\<exists>stp aa ba. steps (Suc 0, a, b) (A |+| B) stp = (0, aa, ba) \<and> Q2 (aa, ba)"

   645   proof(case_tac "steps (Suc 0, a, b) A stp1", simp, erule_tac conjE)

   646     fix aa ba c

   647     assume g1: "Q1 (ba, c)" 

   648       and g2: "steps (Suc 0, a, b) A stp1 = (0, ba, c)"

   649     hence "P2 (ba, c)"

   650       using aimpb apply(simp add: t_imply_def)

   651       done

   652     hence "\<exists> stp. let (s, tp') = steps (Suc 0, ba, c) B stp in s = 0 \<and> Q2 tp'"

   653       using B_halt by simp

   654     from this obtain stp2 where "let (s, tp') = steps (Suc 0, ba, c) B stp2 in s = 0 \<and> Q2 tp'" ..

   655     thus "?thesis"

   656     proof(case_tac "steps (Suc 0, ba, c) B stp2", simp, erule_tac conjE)

   657       fix aa bb ca

   658       assume g3: " Q2 (bb, ca)" "steps (Suc 0, ba, c) B stp2 = (0, bb, ca)"

   659       have "\<exists> stp. steps (Suc 0, a, b) (A |+| B) stp = (Suc (length A div 2), ba , c)"

   660         using g2 A_wf B_wf

   661         by(rule_tac t_merge_pre_halt_same, auto)

   662       moreover have "\<exists> stp. steps (Suc (length A div 2), ba, c) (A |+| B) stp = (0, bb, ca)"

   663         using g3 A_wf B_wf

   664         apply(rule_tac t_merge_snd_halt_eq, auto)

   665         done

   666       ultimately show "\<exists>stp aa ba. steps (Suc 0, a, b) (A |+| B) stp = (0, aa, ba) \<and> Q2 (aa, ba)"

   667         apply(erule_tac exE, erule_tac exE)

   668         apply(rule_tac x = "stp + stpa" in exI, simp add: steps_add)

   669         using g3 by simp

   670     qed

   671   qed

   672 qed

   673 

   674 lemma  t_merge_uhalt_tmp:

   675   assumes B_uh: "\<forall>stp. \<not> isS0 (steps (Suc 0, b, c) B stp)"

   676   and merge_ah: "steps (Suc 0, tp) (A |+| B) stpa = (Suc (length A div 2), b, c)" 

   677   shows "\<forall> stp. \<not> isS0 (steps (Suc 0, tp) (A |+| B) stp)"

   678   using B_uh merge_ah

   679 apply(rule_tac allI)

   680 apply(case_tac "stp > stpa")

   681 apply(erule_tac x = "stp - stpa" in allE)

   682 apply(case_tac "(steps (Suc 0, b, c) B (stp - stpa))", simp)

   683 proof -

   684   fix stp a ba ca 

   685   assume h1: "\<not> isS0 (a, ba, ca)" "stpa < stp"

   686   and h2: "steps (Suc 0, b, c) B (stp - stpa) = (a, ba, ca)"

   687   have "steps (Suc 0 + length A div 2, b, c) (A |+| B) (stp - stpa) = 

   688       (if a = 0 then 0 else a + length A div 2, ba, ca)"

   689     using A_wf B_wf h2

   690     by(rule_tac t_merge_snd_eq_steps, auto)

   691   moreover have "a > 0" using h1 by(simp add: isS0_def)

   692   moreover have "\<exists> stpb. stp = stpa + stpb" 

   693     using h1 by(rule_tac x = "stp - stpa" in exI, simp)

   694   ultimately show "\<not> isS0 (steps (Suc 0, tp) (A |+| B) stp)"

   695     using merge_ah

   696     by(auto simp: steps_add isS0_def)

   697 next

   698   fix stp

   699   assume h: "steps (Suc 0, tp) (A |+| B) stpa = (Suc (length A div 2), b, c)" "\<not> stpa < stp"

   700   hence "\<exists> stpb. stpa = stp + stpb" apply(rule_tac x = "stpa - stp" in exI, auto) done

   701   thus "\<not> isS0 (steps (Suc 0, tp) (A |+| B) stp)"

   702     using h

   703     apply(auto)

   704     apply(cases "steps (Suc 0, tp) (A |+| B) stp", simp add: steps_add isS0_def steps_0)

   705     done

   706 qed

   707 

   708 text {*

   709   The following lemma deals with the situation when TM @{text "B"} can not terminate.

   710   *}

   711 

   712 lemma t_merge_uhalt: 

   713   assumes aimpb: "Q1 \<turnstile>-> P4"

   714   shows "P1 \<turnstile>-> \<lambda> tp. \<not> (\<exists> stp. isS0 (steps (Suc 0, tp) (A |+| B) stp))"

   715 proof(simp only: t_imply_def, rule_tac allI, rule_tac impI)

   716   fix tp 

   717   assume init_asst: "P1 tp"

   718   show "\<not> (\<exists>stp. isS0 (steps (Suc 0, tp) (A |+| B) stp))"

   719   proof -

   720     have "\<exists> stp. let (s, tp') = steps (Suc 0, tp) A stp in s = 0 \<and> Q1 tp'"

   721       using A_halt[of tp] init_asst

   722       by(simp)

   723     from this obtain stpx where "let (s, tp') = steps (Suc 0, tp) A stpx in s = 0 \<and> Q1 tp'" ..

   724     thus "?thesis"

   725     proof(cases "steps (Suc 0, tp) A stpx", simp, erule_tac conjE)

   726       fix a b c

   727       assume "Q1 (b, c)"

   728         and h3: "steps (Suc 0, tp) A stpx = (0, b, c)"

   729       hence h2: "P4 (b, c)"  using aimpb

   730         by(simp add: t_imply_def)

   731       have "\<exists> stp. steps (Suc 0, tp) (A |+| B) stp = (Suc (length A div 2), b, c)"

   732         using h3 A_wf B_wf

   733         apply(rule_tac stp = stpx in t_merge_pre_halt_same, auto)

   734         done

   735       from this obtain stpa where h4:"steps (Suc 0, tp) (A |+| B) stpa = (Suc (length A div 2), b, c)" ..

   736       have " \<not> (\<exists> stp. isS0 (steps (Suc 0, b, c) B stp))"

   737         using B_uhalt [of "(b, c)"] h2 apply simp

   738         done

   739       from this and h4 show "\<forall>stp. \<not> isS0 (steps (Suc 0, tp) (A |+| B) stp)"

   740         by(rule_tac t_merge_uhalt_tmp, auto)

   741     qed

   742   qed

   743 qed

   744 end

   745 

   746 end

   747