1 header {* 

     2  {\em abacus} a kind of register machine

     3 *}

     4 

     5 theory abacus

     6 imports Main turing_basic

     7 begin

     8 

     9 text {*

    10   {\em Abacus} instructions:

    11 *}

    12 

    13 datatype abc_inst =

    14   -- {* @{text "Inc n"} increments the memory cell (or register) with address @{text "n"} by one.

    15      *}

    16      Inc nat

    17   -- {*

    18      @{text "Dec n label"} decrements the memory cell with address @{text "n"} by one. 

    19       If cell @{text "n"} is already zero, no decrements happens and the executio jumps to

    20       the instruction labeled by @{text "label"}.

    21      *}

    22    | Dec nat nat

    23   -- {*

    24   @{text "Goto label"} unconditionally jumps to the instruction labeled by @{text "label"}.

    25   *}

    26    | Goto nat

    27   

    28 

    29 text {*

    30   Abacus programs are defined as lists of Abacus instructions.

    31 *}

    32 type_synonym abc_prog = "abc_inst list"

    33 

    34 section {*

    35   Sample Abacus programs

    36   *}

    37 

    38 text {*

    39   Abacus for addition and clearance.

    40 *}

    41 fun plus_clear :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"  

    42   where

    43   "plus_clear m n e = [Dec m e, Inc n, Goto 0]"

    44 

    45 text {*

    46   Abacus for clearing memory untis.

    47 *}

    48 fun clear :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"

    49   where

    50   "clear n e = [Dec n e, Goto 0]"

    51 

    52 fun plus:: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"

    53   where

    54   "plus m n p e = [Dec m 4, Inc n, Inc p,

    55                    Goto 0, Dec p e, Inc m, Goto 4]"

    56 

    57 fun mult :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"

    58   where

    59   "mult m1 m2 n p e = [Dec m1 e]@ plus m1 m2 p 1"

    60 

    61 fun expo :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"

    62   where

    63   "expo n m1 m2 p e = [Inc n, Dec m1 e] @ mult m2 n n p 2"

    64 

    65 

    66 text {*

    67   The state of Abacus machine.

    68   *}

    69 type_synonym abc_state = nat

    70 

    71 (* text {*

    72   The memory of Abacus machine is defined as a function from address to contents.

    73 *}

    74 type_synonym abc_mem = "nat \<Rightarrow> nat" *)

    75 

    76 text {*

    77   The memory of Abacus machine is defined as a list of contents, with 

    78   every units addressed by index into the list.

    79   *}

    80 type_synonym abc_lm = "nat list"

    81 

    82 text {*

    83   Fetching contents out of memory. Units not represented by list elements are considered

    84   as having content @{text "0"}.

    85 *}

    86 fun abc_lm_v :: "abc_lm \<Rightarrow> nat \<Rightarrow> nat"

    87   where 

    88     "abc_lm_v lm n = (if (n < length lm) then (lm!n) else 0)"         

    89 

    90 (*

    91 fun abc_l2m :: "abc_lm \<Rightarrow> abc_mem"

    92   where 

    93     "abc_l2m lm = abc_lm_v lm"

    94 *)

    95 

    96 text {*

    97   Set the content of memory unit @{text "n"} to value @{text "v"}.

    98   @{text "am"} is the Abacus memory before setting.

    99   If address @{text "n"} is outside to scope of @{text "am"}, @{text "am"} 

   100   is extended so that @{text "n"} becomes in scope.

   101 *}

   102 fun abc_lm_s :: "abc_lm \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_lm"

   103   where

   104     "abc_lm_s am n v = (if (n < length am) then (am[n:=v]) else 

   105                            am@ (replicate (n - length am) 0) @ [v])"

   106 

   107 

   108 text {*

   109   The configuration of Abaucs machines consists of its current state and its

   110   current memory:

   111 *}

   112 type_synonym abc_conf_l = "abc_state \<times> abc_lm"

   113 

   114 text {*

   115   Fetch instruction out of Abacus program:

   116 *}

   117 

   118 fun abc_fetch :: "nat \<Rightarrow> abc_prog \<Rightarrow> abc_inst option" 

   119   where

   120   "abc_fetch s p = (if (s < length p) then Some (p ! s)

   121                     else None)"

   122 

   123 text {*

   124   Single step execution of Abacus machine. If no instruction is feteched, 

   125   configuration does not change.

   126 *}

   127 fun abc_step_l :: "abc_conf_l \<Rightarrow> abc_inst option \<Rightarrow> abc_conf_l"

   128   where

   129   "abc_step_l (s, lm) a = (case a of 

   130                None \<Rightarrow> (s, lm) |

   131                Some (Inc n)  \<Rightarrow> (let nv = abc_lm_v lm n in

   132                        (s + 1, abc_lm_s lm n (nv + 1))) |

   133                Some (Dec n e) \<Rightarrow> (let nv = abc_lm_v lm n in

   134                        if (nv = 0) then (e, abc_lm_s lm n 0) 

   135                        else (s + 1,  abc_lm_s lm n (nv - 1))) |

   136                Some (Goto n) \<Rightarrow> (n, lm) 

   137                )"

   138 

   139 text {*

   140   Multi-step execution of Abacus machine.

   141 *}

   142 fun abc_steps_l :: "abc_conf_l \<Rightarrow> abc_prog \<Rightarrow> nat \<Rightarrow> abc_conf_l"

   143   where

   144   "abc_steps_l (s, lm) p 0 = (s, lm)" |

   145   "abc_steps_l (s, lm) p (Suc n) = abc_steps_l (abc_step_l (s, lm) (abc_fetch s p)) p n"

   146 

   147 section {*

   148   Compiling Abacus machines into Truing machines

   149 *}

   150 

   151 

   152 subsection {*

   153   Compiling functions

   154 *}

   155 

   156 text {*

   157   @{text "findnth n"} returns the TM which locates the represention of

   158   memory cell @{text "n"} on the tape and changes representation of zero

   159   on the way.

   160 *}

   161 

   162 fun findnth :: "nat \<Rightarrow> tprog"

   163   where

   164   "findnth 0 = []" |

   165   "findnth (Suc n) = (findnth n @ [(W1, 2 * n + 1), 

   166            (R, 2 * n + 2), (R, 2 * n + 3), (R, 2 * n + 2)])"

   167 

   168 text {*

   169   @{text "tinc_b"} returns the TM which increments the representation 

   170   of the memory cell under rw-head by one and move the representation 

   171   of cells afterwards to the right accordingly.

   172   *}

   173 

   174 definition tinc_b :: "tprog"

   175   where

   176   "tinc_b \<equiv> [(W1, 1), (R, 2), (W1, 3), (R, 2), (W1, 3), (R, 4), 

   177              (L, 7), (W0, 5), (R, 6), (W0, 5), (W1, 3), (R, 6),

   178              (L, 8), (L, 7), (R, 9), (L, 7), (R, 10), (W0, 9)]" 

   179 

   180 text {*

   181   @{text "tshift tm off"} shifts @{text "tm"} by offset @{text "off"}, leaving 

   182   instructions concerning state @{text "0"} unchanged, because state @{text "0"} 

   183   is the end state, which needs not be changed with shift operation.

   184   *}

   185 

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

   187   where

   188   "tshift tp off = (map (\<lambda> (action, state). 

   189        (action, (if state = 0 then 0

   190                  else state + off))) tp)"

   191 

   192 text {*

   193   @{text "tinc ss n"} returns the TM which simulates the execution of 

   194   Abacus instruction @{text "Inc n"}, assuming that TM is located at

   195   location @{text "ss"} in the final TM complied from the whole

   196   Abacus program.

   197 *}

   198 

   199 fun tinc :: "nat \<Rightarrow> nat \<Rightarrow> tprog"

   200   where

   201   "tinc ss n = tshift (findnth n @ tshift tinc_b (2 * n)) (ss - 1)"

   202 

   203 text {*

   204   @{text "tinc_b"} returns the TM which decrements the representation 

   205   of the memory cell under rw-head by one and move the representation 

   206   of cells afterwards to the left accordingly.

   207   *}

   208 

   209 definition tdec_b :: "tprog"

   210   where

   211   "tdec_b \<equiv>  [(W1, 1), (R, 2), (L, 14), (R, 3), (L, 4), (R, 3),

   212               (R, 5), (W0, 4), (R, 6), (W0, 5), (L, 7), (L, 8),

   213               (L, 11), (W0, 7), (W1, 8), (R, 9), (L, 10), (R, 9),

   214               (R, 5), (W0, 10), (L, 12), (L, 11), (R, 13), (L, 11),

   215               (R, 17), (W0, 13), (L, 15), (L, 14), (R, 16), (L, 14),

   216               (R, 0), (W0, 16)]"

   217 

   218 text {*

   219   @{text "sete tp e"} attaches the termination edges (edges leading to state @{text "0"}) 

   220   of TM @{text "tp"} to the intruction labelled by @{text "e"}.

   221   *}

   222 

   223 fun sete :: "tprog \<Rightarrow> nat \<Rightarrow> tprog"

   224   where

   225   "sete tp e = map (\<lambda> (action, state). (action, if state = 0 then e else state)) tp"

   226 

   227 text {*

   228   @{text "tdec ss n label"} returns the TM which simulates the execution of 

   229   Abacus instruction @{text "Dec n label"}, assuming that TM is located at

   230   location @{text "ss"} in the final TM complied from the whole

   231   Abacus program.

   232 *}

   233 

   234 fun tdec :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> tprog"

   235   where

   236   "tdec ss n e = sete (tshift (findnth n @ tshift tdec_b (2 * n)) 

   237                  (ss - 1)) e"

   238  

   239 text {*

   240   @{text "tgoto f(label)"} returns the TM simulating the execution of Abacus instruction

   241   @{text "Goto label"}, where @{text "f(label)"} is the corresponding location of

   242   @{text "label"} in the final TM compiled from the overall Abacus program.

   243 *}

   244 

   245 fun tgoto :: "nat \<Rightarrow> tprog"

   246   where

   247   "tgoto n = [(Nop, n), (Nop, n)]"

   248 

   249 text {*

   250   The layout of the final TM compiled from an Abacus program is represented

   251   as a list of natural numbers, where the list element at index @{text "n"} represents the 

   252   starting state of the TM simulating the execution of @{text "n"}-th instruction

   253   in the Abacus program.

   254 *}

   255 

   256 type_synonym layout = "nat list"

   257 

   258 text {*

   259   @{text "length_of i"} is the length of the 

   260   TM simulating the Abacus instruction @{text "i"}.

   261 *}

   262 fun length_of :: "abc_inst \<Rightarrow> nat"

   263   where

   264   "length_of i = (case i of 

   265                     Inc n   \<Rightarrow> 2 * n + 9 |

   266                     Dec n e \<Rightarrow> 2 * n + 16 |

   267                     Goto n  \<Rightarrow> 1)"

   268 

   269 text {*

   270   @{text "layout_of ap"} returns the layout of Abacus program @{text "ap"}.

   271 *}

   272 fun layout_of :: "abc_prog \<Rightarrow> layout"

   273   where "layout_of ap = map length_of ap"

   274 

   275 

   276 text {*

   277   @{text "start_of layout n"} looks out the starting state of @{text "n"}-th

   278   TM in the finall TM.

   279 *}

   280 

   281 fun start_of :: "nat list \<Rightarrow> nat \<Rightarrow> nat"

   282   where

   283   "start_of ly 0 = Suc 0" |

   284   "start_of ly (Suc as) = 

   285         (if as < length ly then start_of ly as + (ly ! as)

   286          else start_of ly as)"

   287 

   288 text {*

   289   @{text "ci lo ss i"} complies Abacus instruction @{text "i"}

   290   assuming the TM of @{text "i"} starts from state @{text "ss"} 

   291   within the overal layout @{text "lo"}.

   292 *}

   293 

   294 fun ci :: "layout \<Rightarrow> nat \<Rightarrow> abc_inst \<Rightarrow> tprog"

   295   where

   296   "ci ly ss i = (case i of 

   297                     Inc n   \<Rightarrow> tinc ss n |

   298                     Dec n e \<Rightarrow> tdec ss n (start_of ly e) |

   299                     Goto n  \<Rightarrow> tgoto (start_of ly n))"

   300 

   301 text {*

   302   @{text "tpairs_of ap"} transfroms Abacus program @{text "ap"} pairing

   303   every instruction with its starting state.

   304 *}

   305 fun tpairs_of :: "abc_prog \<Rightarrow> (nat \<times> abc_inst) list"

   306   where "tpairs_of ap = (zip (map (start_of (layout_of ap)) 

   307                          [0..<(length ap)]) ap)"

   308 

   309 

   310 text {*

   311   @{text "tms_of ap"} returns the list of TMs, where every one of them simulates

   312   the corresponding Abacus intruction in @{text "ap"}.

   313 *}

   314 

   315 fun tms_of :: "abc_prog \<Rightarrow> tprog list"

   316   where "tms_of ap = map (\<lambda> (n, tm). ci (layout_of ap) n tm) 

   317                          (tpairs_of ap)"

   318 

   319 text {*

   320   @{text "tm_of ap"} returns the final TM machine compiled from Abacus program @{text "ap"}.

   321 *}

   322 fun tm_of :: "abc_prog \<Rightarrow> tprog"

   323   where "tm_of ap = concat (tms_of ap)"

   324 

   325 text {*

   326   The following two functions specify the well-formedness of complied TM.

   327 *}

   328 fun t_ncorrect :: "tprog \<Rightarrow> bool"

   329   where

   330   "t_ncorrect tp = (length tp mod 2 = 0)"

   331 

   332 fun abc2t_correct :: "abc_prog \<Rightarrow> bool"

   333   where 

   334   "abc2t_correct ap = list_all (\<lambda> (n, tm). 

   335              t_ncorrect (ci (layout_of ap) n tm)) (tpairs_of ap)"

   336 

   337 lemma findnth_length: "length (findnth n) div 2 = 2 * n"

   338 apply(induct n, simp, simp)

   339 done

   340 

   341 lemma ci_length : "length (ci ns n ai) div 2 = length_of ai"

   342 apply(auto simp: ci.simps tinc_b_def tdec_b_def findnth_length

   343                  split: abc_inst.splits)

   344 done

   345 

   346 subsection {*

   347   Representation of Abacus memory by TM tape

   348 *}

   349 

   350 consts tape_of :: "'a \<Rightarrow> block list" ("<_>" 100)

   351 

   352 text {*

   353   @{text "tape_of_nat_list am"} returns the TM tape representing

   354   Abacus memory @{text "am"}.

   355   *}

   356 

   357 fun tape_of_nat_list :: "nat list \<Rightarrow> block list"

   358   where 

   359   "tape_of_nat_list [] = []" |

   360   "tape_of_nat_list [n] = Oc\<^bsup>n+1\<^esup>" |

   361   "tape_of_nat_list (n#ns) = (Oc\<^bsup>n+1\<^esup>) @ [Bk] @ (tape_of_nat_list ns)"

   362 

   363 defs (overloaded)

   364   tape_of_nl_abv: "<am> \<equiv> tape_of_nat_list am"

   365   tape_of_nat_abv : "<(n::nat)> \<equiv> Oc\<^bsup>n+1\<^esup>"

   366 

   367 text {*

   368   @{text "crsp_l acf tcf"} meams the abacus configuration @{text "acf"}

   369   is corretly represented by the TM configuration @{text "tcf"}.

   370 *}

   371 

   372 fun crsp_l :: "layout \<Rightarrow> abc_conf_l \<Rightarrow> t_conf \<Rightarrow> block list \<Rightarrow> bool"

   373   where 

   374   "crsp_l ly (as, lm) (ts, (l, r)) inres = 

   375            (ts = start_of ly as \<and> (\<exists> rn. r = <lm> @ Bk\<^bsup>rn\<^esup>)

   376             \<and> l = Bk # Bk # inres)"

   377 

   378 declare crsp_l.simps[simp del]

   379 

   380 subsection {*

   381   A more general definition of TM execution. 

   382 *}

   383 

   384 (*

   385 fun nnth_of :: "(taction \<times> nat) list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (taction \<times> nat)"

   386   where

   387   "nnth_of p s b = (if 2*s < length p 

   388                     then (p ! (2*s + b)) else (Nop, 0))"

   389 

   390 thm nth_of.simps

   391 

   392 fun nfetch :: "tprog \<Rightarrow> nat \<Rightarrow> block \<Rightarrow> taction \<times> nat"

   393   where

   394   "nfetch p 0 b = (Nop, 0)" |

   395   "nfetch p (Suc s) b = 

   396              (case b of 

   397                 Bk \<Rightarrow> nnth_of p s 0 |

   398                 Oc \<Rightarrow> nnth_of p s 1)"

   399 *)

   400 

   401 text {*

   402   @{text "t_step tcf (tp, ss)"} returns the result of one step exection of TM @{text "tp"}

   403   assuming @{text "tp"} starts from instial state @{text "ss"}.

   404 *}

   405 

   406 fun t_step :: "t_conf \<Rightarrow> (tprog \<times> nat) \<Rightarrow> t_conf"

   407   where 

   408   "t_step c (p, off) = 

   409            (let (state, leftn, rightn) = c in

   410             let (action, next_state) = fetch p (state-off)

   411                              (case rightn of 

   412                                 [] \<Rightarrow> Bk | 

   413                                 Bk # xs \<Rightarrow> Bk |

   414                                 Oc # xs \<Rightarrow> Oc

   415                              ) 

   416              in 

   417             (next_state, new_tape action (leftn, rightn)))"

   418 

   419 

   420 text {*

   421   @{text "t_steps tcf (tp, ss) n"} returns the result of @{text "n"}-step exection 

   422   of TM @{text "tp"} assuming @{text "tp"} starts from instial state @{text "ss"}.

   423 *}

   424 

   425 fun t_steps :: "t_conf \<Rightarrow> (tprog \<times> nat) \<Rightarrow> nat \<Rightarrow> t_conf"

   426   where

   427   "t_steps c (p, off) 0 = c" |

   428   "t_steps c (p, off) (Suc n) = t_steps 

   429                      (t_step c (p, off)) (p, off) n" 

   430 

   431 lemma stepn: "t_steps c (p, off) (Suc n) = 

   432               t_step (t_steps c (p, off) n) (p, off)"

   433 apply(induct n arbitrary: c, simp add: t_steps.simps)

   434 apply(simp add: t_steps.simps)

   435 done

   436 

   437 text {*

   438   The type of invarints expressing correspondence between 

   439   Abacus configuration and TM configuration.

   440 *}

   441 

   442 type_synonym inc_inv_t = "abc_conf_l \<Rightarrow> t_conf \<Rightarrow> block list \<Rightarrow> bool"

   443 

   444 declare tms_of.simps[simp del] tm_of.simps[simp del]

   445         layout_of.simps[simp del] abc_fetch.simps [simp del]  

   446         t_step.simps[simp del] t_steps.simps[simp del] 

   447         tpairs_of.simps[simp del] start_of.simps[simp del]

   448         fetch.simps [simp del] t_ncorrect.simps[simp del]

   449         new_tape.simps [simp del] ci.simps [simp del] length_of.simps[simp del] 

   450         layout_of.simps[simp del] crsp_l.simps[simp del]

   451         abc2t_correct.simps[simp del]

   452 

   453 lemma tct_div2: "t_ncorrect tp \<Longrightarrow> (length tp) mod 2 = 0"

   454 apply(simp add: t_ncorrect.simps)

   455 done

   456 

   457 lemma t_shift_fetch: 

   458     "\<lbrakk>t_ncorrect tp1; t_ncorrect tp; 

   459       length tp1 div 2 < a \<and> a \<le> length tp1 div 2 + length tp div 2\<rbrakk>

   460     \<Longrightarrow> fetch tp (a - length tp1 div 2) b = 

   461          fetch (tp1 @ tp @ tp2) a b"

   462 apply(subgoal_tac "\<exists> x. a = length tp1 div 2 + x", erule exE, simp)

   463 apply(case_tac x, simp)

   464 apply(subgoal_tac "length tp1 div 2 + Suc nat = 

   465              Suc (length tp1 div 2 + nat)")

   466 apply(simp only: fetch.simps nth_of.simps, auto)

   467 apply(case_tac b, simp)

   468 apply(subgoal_tac "2 * (length tp1 div 2) = length tp1", simp)

   469 apply(subgoal_tac "2 * nat < length tp", simp add: nth_append, simp)

   470 apply(simp add: t_ncorrect.simps, auto)

   471 apply(subgoal_tac "2 * (length tp1 div 2) = length tp1", simp)

   472 apply(subgoal_tac "2 * nat < length tp", simp add: nth_append, auto)

   473 apply(simp add: t_ncorrect.simps, auto)

   474 apply(rule_tac x = "a - length tp1 div 2" in exI, simp)

   475 done

   476 

   477 lemma t_shift_in_step:

   478       "\<lbrakk>t_step (a, aa, ba) (tp, length tp1 div 2) = (s, l, r);

   479         t_ncorrect tp1; t_ncorrect tp;

   480         length tp1 div 2 < a \<and> a \<le> length tp1 div 2 + length tp div 2\<rbrakk>

   481        \<Longrightarrow> t_step (a, aa, ba) (tp1 @ tp @ tp2, 0) = (s, l, r)"

   482 apply(simp add: t_step.simps)

   483 apply(subgoal_tac "fetch tp (a - length tp1 div 2) (case ba of [] \<Rightarrow> 

   484                    Bk | x # xs \<Rightarrow> x)

   485              = fetch (tp1 @ tp @ tp2) a (case ba of [] \<Rightarrow> Bk | x # xs

   486                    \<Rightarrow> x)")

   487 apply(case_tac "fetch tp (a - length tp1 div 2) (case ba of [] \<Rightarrow> Bk

   488                 | x # xs \<Rightarrow> x)")

   489 apply(auto intro: t_shift_fetch)

   490 apply(case_tac ba, simp, simp)

   491 apply(case_tac aaa, simp, simp)

   492 done

   493 

   494 declare add_Suc_right[simp del]

   495 lemma t_step_add: "t_steps c (p, off) (m + n) = 

   496           t_steps (t_steps c (p, off) m) (p, off) n"

   497 apply(induct m arbitrary: n,  simp add: t_steps.simps, simp)

   498 apply(subgoal_tac "t_steps c (p, off) (Suc (m + n)) = 

   499                          t_steps c (p, off) (m + Suc n)", simp)

   500 apply(subgoal_tac "t_steps (t_steps c (p, off) m) (p, off) (Suc n) =

   501                 t_steps (t_step (t_steps c (p, off) m) (p, off)) 

   502                          (p, off) n")

   503 apply(simp, simp add: stepn)

   504 apply(simp only: t_steps.simps)

   505 apply(simp only: add_Suc_right)

   506 done

   507 declare add_Suc_right[simp]

   508 

   509 lemma s_out_fetch: "\<lbrakk>t_ncorrect tp; 

   510         \<not> (length tp1 div 2 < a \<and> a \<le> length tp1 div 2 + 

   511          length tp div 2)\<rbrakk>

   512       \<Longrightarrow> fetch tp (a - length tp1 div 2) b = (Nop, 0)"

   513 apply(auto)

   514 apply(simp add: fetch.simps)

   515 apply(subgoal_tac "\<exists> x. a - length tp1 div 2 = length tp div 2 + x")

   516 apply(erule exE, simp)

   517 apply(case_tac x, simp)

   518 apply(auto simp add: fetch.simps)

   519 apply(subgoal_tac "2 * (length tp div 2) =  length tp")

   520 apply(auto simp: t_ncorrect.simps split: block.splits)

   521 apply(rule_tac x = "a - length tp1 div 2 - length tp div 2" in exI

   522      , simp)

   523 done 

   524 

   525 lemma conf_keep_step: 

   526       "\<lbrakk>t_ncorrect tp; 

   527         \<not> (length tp1 div 2 < a \<and> a \<le> length tp1 div 2 + 

   528        length tp div 2)\<rbrakk>

   529       \<Longrightarrow> t_step (a, aa, ba) (tp, length tp1 div 2) = (0, aa, ba)"

   530 apply(simp add: t_step.simps)

   531 apply(subgoal_tac "fetch tp (a - length tp1 div 2) (case ba of [] \<Rightarrow> 

   532   Bk | Bk # xs \<Rightarrow> Bk | Oc # xs \<Rightarrow> Oc) = (Nop, 0)")

   533 apply(simp add: new_tape.simps)

   534 apply(rule s_out_fetch, simp, simp)

   535 done

   536 

   537 lemma conf_keep: 

   538       "\<lbrakk>t_ncorrect tp; 

   539         \<not> (length tp1 div 2 < a \<and>

   540         a \<le> length tp1 div 2 + length tp div 2); n > 0\<rbrakk>

   541       \<Longrightarrow> t_steps (a, aa, ba) (tp, length tp1 div 2) n = (0, aa, ba)"

   542 apply(induct n, simp)

   543 apply(case_tac n, simp add: t_steps.simps)

   544 apply(rule_tac conf_keep_step, simp+)

   545 apply(subgoal_tac " t_steps (a, aa, ba) 

   546                (tp, length tp1 div 2) (Suc (Suc nat))

   547          = t_step (t_steps (a, aa, ba) 

   548             (tp, length tp1 div 2) (Suc nat)) (tp, length tp1 div 2)")

   549 apply(simp)

   550 apply(rule_tac conf_keep_step, simp, simp)

   551 apply(rule stepn)

   552 done

   553 

   554 lemma state_bef_inside: 

   555     "\<lbrakk>t_ncorrect tp1; t_ncorrect tp; 

   556       t_steps (s0, l0, r0) (tp, length tp1 div 2) stp = (s, l, r);

   557       length tp1 div 2 < s0 \<and> 

   558          s0 \<le> length tp1 div 2 + length tp div 2;

   559       length tp1 div 2 < s \<and> s \<le> length tp1 div 2 + length tp div 2; 

   560       n < stp; t_steps (s0, l0, r0) (tp, length tp1 div 2) n = 

   561       (a, aa, ba)\<rbrakk>

   562       \<Longrightarrow>  length tp1 div 2 < a \<and> 

   563          a \<le> length tp1 div 2 + length tp div 2"

   564 apply(subgoal_tac "\<exists> x. stp = n + x", erule exE)

   565 apply(simp only: t_step_add)

   566 apply(rule classical)

   567 apply(subgoal_tac "t_steps (a, aa, ba) 

   568           (tp, length tp1 div 2) x = (0, aa, ba)")

   569 apply(simp)

   570 apply(rule conf_keep, simp, simp, simp)

   571 apply(rule_tac x = "stp - n" in exI, simp)

   572 done

   573 

   574 lemma turing_shift_inside: 

   575        "\<lbrakk>t_steps (s0, l0, r0) (tp, length tp1 div 2) stp = (s, l, r);

   576          length tp1 div 2 < s0 \<and> 

   577          s0 \<le> length tp1 div 2 + length tp div 2; 

   578          t_ncorrect tp1; t_ncorrect tp;

   579          length tp1 div 2 < s \<and> 

   580          s \<le> length tp1 div 2 + length tp div 2\<rbrakk>

   581        \<Longrightarrow> t_steps (s0, l0, r0) (tp1 @ tp @ tp2, 0) stp = (s, l, r)"

   582 apply(induct stp arbitrary: s l r)

   583 apply(simp add: t_steps.simps)

   584 apply(subgoal_tac " t_steps (s0, l0, r0) 

   585         (tp, length tp1 div 2) (Suc stp)

   586                   = t_step (t_steps (s0, l0, r0) 

   587         (tp, length tp1 div 2) stp) (tp, length tp1 div 2)")

   588 apply(case_tac "t_steps (s0, l0, r0) (tp, length tp1 div 2) stp")

   589 apply(subgoal_tac "length tp1 div 2 < a \<and> 

   590             a \<le> length tp1 div 2 + length tp div 2")

   591 apply(subgoal_tac "t_steps (s0, l0, r0) 

   592            (tp1 @ tp @ tp2, 0) stp = (a, b, c)")

   593 apply(simp only: stepn, simp)

   594 apply(rule_tac t_shift_in_step, simp+)

   595 defer

   596 apply(rule stepn)

   597 apply(rule_tac n = stp and stp = "Suc stp" and a = a 

   598                and aa = b and ba = c in state_bef_inside, simp+)

   599 done

   600 

   601 lemma take_Suc_last[elim]: "Suc as \<le> length xs \<Longrightarrow> 

   602             take (Suc as) xs = take as xs @ [xs ! as]"

   603 apply(induct xs arbitrary: as, simp, simp)

   604 apply(case_tac as, simp, simp)

   605 done

   606 

   607 lemma concat_suc: "Suc as \<le> length xs \<Longrightarrow> 

   608        concat (take (Suc as) xs) = concat (take as xs) @ xs! as"

   609 apply(subgoal_tac "take (Suc as) xs = take as xs @ [xs ! as]", simp)

   610 by auto

   611 

   612 lemma concat_take_suc_iff: "Suc n \<le> length tps \<Longrightarrow> 

   613        concat (take n tps) @ (tps ! n) = concat (take (Suc n) tps)"

   614 apply(drule_tac concat_suc, simp)

   615 done

   616 

   617 lemma concat_drop_suc_iff: 

   618    "Suc n < length tps \<Longrightarrow> concat (drop (Suc n) tps) = 

   619            tps ! Suc n @ concat (drop (Suc (Suc n)) tps)"

   620 apply(induct tps arbitrary: n, simp, simp)

   621 apply(case_tac tps, simp, simp)

   622 apply(case_tac n, simp, simp)

   623 done

   624 

   625 declare append_assoc[simp del]

   626 

   627 lemma  tm_append: "\<lbrakk>n < length tps; tp = tps ! n\<rbrakk> \<Longrightarrow> 

   628            \<exists> tp1 tp2. concat tps = tp1 @ tp @ tp2 \<and> tp1 = 

   629               concat (take n tps) \<and> tp2 = concat (drop (Suc n) tps)"

   630 apply(rule_tac x = "concat (take n tps)" in exI)

   631 apply(rule_tac x = "concat (drop (Suc n) tps)" in exI)

   632 apply(auto)

   633 apply(induct n, simp)

   634 apply(case_tac tps, simp, simp, simp)

   635 apply(subgoal_tac "concat (take n tps) @ (tps ! n) = 

   636                concat (take (Suc n) tps)")

   637 apply(simp only: append_assoc[THEN sym], simp only: append_assoc)

   638 apply(subgoal_tac " concat (drop (Suc n) tps) = tps ! Suc n @ 

   639                   concat (drop (Suc (Suc n)) tps)", simp)

   640 apply(rule_tac concat_drop_suc_iff, simp)

   641 apply(rule_tac concat_take_suc_iff, simp)

   642 done

   643 

   644 declare append_assoc[simp]

   645 

   646 lemma map_of:  "n < length xs \<Longrightarrow> (map f xs) ! n = f (xs ! n)"

   647 by(auto)

   648 

   649 lemma [simp]: "length (tms_of aprog) = length aprog"

   650 apply(auto simp: tms_of.simps tpairs_of.simps)

   651 done

   652 

   653 lemma ci_nth: "\<lbrakk>ly = layout_of aprog; as < length aprog; 

   654                 abc_fetch as aprog = Some ins\<rbrakk>

   655     \<Longrightarrow> ci ly (start_of ly as) ins = tms_of aprog ! as"

   656 apply(simp add: tms_of.simps tpairs_of.simps 

   657       abc_fetch.simps  map_of del: map_append)

   658 done

   659 

   660 lemma t_split:"\<lbrakk>

   661         ly = layout_of aprog;

   662         as < length aprog; abc_fetch as aprog = Some ins\<rbrakk>

   663       \<Longrightarrow> \<exists> tp1 tp2. concat (tms_of aprog) = 

   664             tp1 @ (ci ly (start_of ly as) ins) @ tp2

   665             \<and> tp1 = concat (take as (tms_of aprog)) \<and> 

   666               tp2 = concat (drop (Suc as) (tms_of aprog))"

   667 apply(insert tm_append[of "as" "tms_of aprog" 

   668                              "ci ly (start_of ly as) ins"], simp)

   669 apply(subgoal_tac "ci ly (start_of ly as) ins = (tms_of aprog) ! as")

   670 apply(subgoal_tac "length (tms_of aprog) = length aprog", simp, simp)

   671 apply(rule_tac ci_nth, auto)

   672 done

   673 

   674 lemma math_sub: "\<lbrakk>x >= Suc 0; x - 1 = z\<rbrakk> \<Longrightarrow> x + y - Suc 0 = z + y"

   675 by auto

   676 

   677 lemma start_more_one: "as \<noteq> 0 \<Longrightarrow> start_of ly as >= Suc 0"

   678 apply(induct as, simp add: start_of.simps)

   679 apply(case_tac as, auto simp: start_of.simps)

   680 done

   681 

   682 lemma tm_ct: "\<lbrakk>abc2t_correct aprog; tp \<in> set (tms_of aprog)\<rbrakk> \<Longrightarrow> 

   683                            t_ncorrect tp"

   684 apply(simp add: abc2t_correct.simps tms_of.simps)

   685 apply(auto)

   686 apply(simp add:list_all_iff, auto)

   687 done

   688 

   689 lemma div_apart: "\<lbrakk>x mod (2::nat) = 0; y mod 2 = 0\<rbrakk> 

   690           \<Longrightarrow> (x + y) div 2 = x div 2 + y div 2"

   691 apply(drule mod_eqD)+

   692 apply(auto)

   693 done

   694 

   695 lemma div_apart_iff: "\<lbrakk>x mod (2::nat) = 0; y mod 2 = 0\<rbrakk> \<Longrightarrow> 

   696            (x + y) mod 2 = 0"

   697 apply(auto)

   698 done

   699 

   700 lemma tms_ct: "\<lbrakk>abc2t_correct aprog; n < length aprog\<rbrakk> \<Longrightarrow> 

   701          t_ncorrect (concat (take n (tms_of aprog)))"

   702 apply(induct n, simp add: t_ncorrect.simps, simp)

   703 apply(subgoal_tac "concat (take (Suc n) (tms_of aprog)) = 

   704         concat (take n (tms_of aprog)) @ (tms_of aprog ! n)", simp)

   705 apply(simp add: t_ncorrect.simps)

   706 apply(rule_tac div_apart_iff, simp)

   707 apply(subgoal_tac "t_ncorrect (tms_of aprog ! n)", 

   708             simp add: t_ncorrect.simps)

   709 apply(rule_tac tm_ct, simp)

   710 apply(rule_tac nth_mem, simp add: tms_of.simps tpairs_of.simps)

   711 apply(rule_tac concat_suc, simp add: tms_of.simps tpairs_of.simps)

   712 done

   713 

   714 lemma tcorrect_div2: "\<lbrakk>abc2t_correct aprog; Suc as < length aprog\<rbrakk>

   715   \<Longrightarrow> (length (concat (take as (tms_of aprog))) + length (tms_of aprog

   716  ! as)) div 2 = length (concat (take as (tms_of aprog))) div 2 + 

   717                  length (tms_of aprog ! as) div 2"

   718 apply(subgoal_tac "t_ncorrect (tms_of aprog ! as)")

   719 apply(subgoal_tac "t_ncorrect (concat (take as (tms_of aprog)))")

   720 apply(rule_tac div_apart)

   721 apply(rule tct_div2, simp)+

   722 apply(erule_tac tms_ct, simp)

   723 apply(rule_tac tm_ct, simp)

   724 apply(rule_tac nth_mem)

   725 apply(simp add: tms_of.simps tpairs_of.simps)

   726 done

   727 

   728 lemma [simp]: "length (layout_of aprog) = length aprog"

   729 apply(auto simp: layout_of.simps)

   730 done

   731 

   732 lemma start_of_ind: "\<lbrakk>as < length aprog; ly = layout_of aprog\<rbrakk> \<Longrightarrow> 

   733        start_of ly (Suc as) = start_of ly as + 

   734                           length ((tms_of aprog) ! as) div 2"

   735 apply(simp only: start_of.simps, simp)

   736 apply(auto simp: start_of.simps tms_of.simps layout_of.simps 

   737                  tpairs_of.simps)

   738 apply(simp add: ci_length)

   739 done

   740 

   741 lemma concat_take_suc: "Suc n \<le> length xs \<Longrightarrow>

   742   concat (take (Suc n) xs) = concat (take n xs) @ (xs ! n)"

   743 apply(subgoal_tac "take (Suc n) xs =

   744                    take n xs @ [xs ! n]")

   745 apply(auto)

   746 done

   747 

   748 lemma ci_length_not0: "Suc 0 <= length (ci ly as i) div 2"

   749 apply(subgoal_tac "length (ci ly as i) div 2 = length_of i")

   750 apply(simp add: length_of.simps split: abc_inst.splits)

   751 apply(rule ci_length)

   752 done

   753  

   754 lemma findnth_length2: "length (findnth n) = 4 * n"

   755 apply(induct n, simp)

   756 apply(simp)

   757 done

   758 

   759 lemma ci_length2: "length (ci ly as i) = 2 * (length_of i)"

   760 apply(simp add: ci.simps length_of.simps tinc_b_def tdec_b_def

   761               split: abc_inst.splits, auto)

   762 apply(simp add: findnth_length2)+

   763 done

   764 

   765 lemma tm_mod2: "as < length aprog \<Longrightarrow> 

   766              length (tms_of aprog ! as) mod 2 = 0"

   767 apply(simp add: tms_of.simps)

   768 apply(subgoal_tac "map (\<lambda>(x, y). ci (layout_of aprog) x y) 

   769               (tpairs_of aprog) ! as

   770                 = (\<lambda>(x, y). ci (layout_of aprog) x y) 

   771               ((tpairs_of aprog) ! as)", simp)

   772 apply(case_tac "(tpairs_of aprog ! as)", simp)

   773 apply(subgoal_tac "length (ci (layout_of aprog) a b) =

   774                  2 * (length_of b)", simp)

   775 apply(rule ci_length2)

   776 apply(rule map_of, simp add: tms_of.simps tpairs_of.simps)

   777 done

   778 

   779 lemma tms_mod2: "as \<le> length aprog \<Longrightarrow> 

   780         length (concat (take as (tms_of aprog))) mod 2 = 0"

   781 apply(induct as, simp, simp)

   782 apply(subgoal_tac "concat (take (Suc as) (tms_of aprog))

   783                   = concat (take as (tms_of aprog)) @ 

   784                        (tms_of aprog ! as)", auto)

   785 apply(rule div_apart_iff, simp, rule tm_mod2, simp)

   786 apply(rule concat_take_suc, simp add: tms_of.simps tpairs_of.simps)

   787 done

   788 

   789 lemma [simp]: "\<lbrakk>as < length aprog; (abc_fetch as aprog) = Some ins\<rbrakk>

   790        \<Longrightarrow> ci (layout_of aprog) 

   791           (start_of (layout_of aprog) as) (ins) \<in> set (tms_of aprog)"

   792 apply(insert ci_nth[of "layout_of aprog" aprog as], simp)

   793 done

   794 

   795 lemma startof_not0: "start_of ly as > 0"

   796 apply(induct as, simp add: start_of.simps)

   797 apply(case_tac as, auto simp: start_of.simps)

   798 done

   799 

   800 declare abc_step_l.simps[simp del]

   801 lemma pre_lheq: "\<lbrakk>tp = concat (take as (tms_of aprog));

   802    abc2t_correct aprog; as \<le> length aprog\<rbrakk> \<Longrightarrow> 

   803          start_of (layout_of aprog) as - Suc 0 = length tp div 2"

   804 apply(induct as arbitrary: tp, simp add: start_of.simps, simp)

   805 proof - 

   806   fix as tp

   807   assume h1: "\<And>tp. tp = concat (take as (tms_of aprog)) \<Longrightarrow> 

   808      start_of (layout_of aprog) as - Suc 0 = 

   809             length (concat (take as (tms_of aprog))) div 2"

   810   and h2: " abc2t_correct aprog" "Suc as \<le> length aprog" 

   811   from h2 show "start_of (layout_of aprog) (Suc as) - Suc 0 = 

   812           length (concat (take (Suc as) (tms_of aprog))) div 2"

   813     apply(insert h1[of "concat (take as (tms_of aprog))"], simp)

   814     apply(insert start_of_ind[of as aprog "layout_of aprog"], simp)

   815     apply(subgoal_tac "(take (Suc as) (tms_of aprog)) = 

   816             take as (tms_of aprog) @ [(tms_of aprog) ! as]", simp)

   817     apply(subgoal_tac "(length (concat (take as (tms_of aprog))) + 

   818                        length (tms_of aprog ! as)) div 2

   819             = length (concat (take as (tms_of aprog))) div 2 + 

   820               length (tms_of aprog ! as) div 2", simp)

   821     apply(subgoal_tac "start_of (layout_of aprog) as = 

   822        length (concat (take as (tms_of aprog))) div 2 + Suc 0", simp)

   823     apply(subgoal_tac "start_of (layout_of aprog) as > 0", simp, 

   824            rule_tac startof_not0)

   825     apply(insert tm_mod2[of as aprog], simp)

   826     apply(insert tms_mod2[of as aprog], simp, arith)

   827     apply(rule take_Suc_last, simp)

   828     done

   829 qed

   830 

   831 lemma crsp2stateq: 

   832   "\<lbrakk>as < length aprog; abc2t_correct aprog;

   833        crsp_l (layout_of aprog) (as, am) (a, aa, ba) inres\<rbrakk> \<Longrightarrow> 

   834         a = length (concat (take as (tms_of aprog))) div 2 + 1"

   835 apply(simp add: crsp_l.simps)

   836 apply(insert pre_lheq[of "(concat (take as (tms_of aprog)))" as aprog]

   837 , simp)   

   838 apply(subgoal_tac "start_of (layout_of aprog) as > 0", 

   839       auto intro: startof_not0)

   840 done

   841 

   842 lemma turing_shift_outside: 

   843      "\<lbrakk>t_steps (s0, l0, r0) (tp, length tp1 div 2) stp = (s, l, r); 

   844        s \<noteq> 0; stp > 0;

   845        length tp1 div 2 < s0 \<and> 

   846        s0 \<le> length tp1 div 2 + length tp div 2; 

   847        t_ncorrect tp1; t_ncorrect tp;

   848        \<not> (length tp1 div 2 < s \<and> 

   849       s \<le> length tp1 div 2 + length tp div 2)\<rbrakk>

   850     \<Longrightarrow> \<exists>stp' > 0. t_steps (s0, l0, r0) (tp1 @ tp @ tp2, 0) stp' 

   851                 = (s, l, r)"

   852 apply(rule_tac x = stp in exI)

   853 apply(case_tac stp, simp add: t_steps.simps)

   854 apply(simp only: stepn)

   855 apply(case_tac "t_steps (s0, l0, r0) (tp, length tp1 div 2) nat")

   856 apply(subgoal_tac "length tp1 div 2 < a \<and> 

   857                    a \<le> length tp1 div 2 + length tp div 2")

   858 apply(subgoal_tac "t_steps (s0, l0, r0) (tp1 @ tp @ tp2, 0) nat 

   859                    = (a, b, c)", simp)

   860 apply(rule_tac t_shift_in_step, simp+)

   861 apply(rule_tac turing_shift_inside, simp+)

   862 apply(rule classical)

   863 apply(subgoal_tac "t_step (a,b,c) 

   864             (tp, length tp1 div 2) = (0, b, c)", simp)

   865 apply(rule_tac conf_keep_step, simp+)

   866 done

   867 

   868 lemma turing_shift: 

   869   "\<lbrakk>t_steps (s0, (l0, r0)) (tp, (length tp1 div 2)) stp

   870    = (s, (l, r)); s \<noteq> 0; stp > 0;

   871   (length tp1 div 2 < s0 \<and> s0 <= length tp1 div 2 + length tp div 2);

   872   t_ncorrect tp1; t_ncorrect tp\<rbrakk> \<Longrightarrow> 

   873          \<exists> stp' > 0. t_steps (s0, (l0, r0)) (tp1 @ tp @ tp2, 0) stp' =

   874                     (s, (l, r))"

   875 apply(case_tac "s > length tp1 div 2 \<and> 

   876               s <= length tp1 div 2 + length tp div 2")

   877 apply(subgoal_tac " t_steps (s0, l0, r0) (tp1 @ tp @ tp2, 0) stp = 

   878                    (s, l, r)")

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

   880 apply(rule_tac turing_shift_inside, simp+)

   881 apply(rule_tac turing_shift_outside, simp+)

   882 done

   883 

   884 lemma inc_startof_not0:  "start_of ly as \<ge> Suc 0"

   885 apply(induct as, simp add: start_of.simps)

   886 apply(simp add: start_of.simps)

   887 done

   888 

   889 lemma s_crsp:

   890   "\<lbrakk>as < length aprog; abc_fetch as aprog = Some ins;

   891   abc2t_correct aprog;

   892   crsp_l (layout_of aprog) (as, am) (a, aa, ba) inres\<rbrakk> \<Longrightarrow>  

   893   length (concat (take as (tms_of aprog))) div 2 < a 

   894       \<and> a \<le> length (concat (take as (tms_of aprog))) div 2 + 

   895          length (ci (layout_of aprog) (start_of (layout_of aprog) as)

   896          ins) div 2"

   897 apply(subgoal_tac "a = length (concat (take as (tms_of aprog))) div 

   898                    2 + 1", simp)

   899 apply(rule_tac ci_length_not0)

   900 apply(rule crsp2stateq, simp+)

   901 done

   902 

   903 lemma tms_out_ex:

   904   "\<lbrakk>ly = layout_of aprog; tprog = tm_of aprog;

   905   abc2t_correct aprog;

   906   crsp_l ly (as, am) tc inres; as < length aprog;

   907   abc_fetch as aprog = Some ins;

   908   t_steps tc (ci ly (start_of ly as) ins, 

   909   (start_of ly as) - 1) n = (s, l, r);

   910   n > 0; 

   911   abc_step_l (as, am) (abc_fetch as aprog) = (as', am');

   912   s = start_of ly as'

   913   \<rbrakk>

   914   \<Longrightarrow> \<exists> stp > 0. (t_steps tc (tprog, 0) stp = (s, (l, r)))"

   915 apply(simp only: tm_of.simps)

   916 apply(subgoal_tac "\<exists> tp1 tp2. concat (tms_of aprog) = 

   917       tp1 @ (ci ly (start_of ly as) ins) @ tp2

   918     \<and> tp1 = concat (take as (tms_of aprog)) \<and> 

   919       tp2 = concat (drop (Suc as) (tms_of aprog))")

   920 apply(erule exE, erule exE, erule conjE, erule conjE,

   921       case_tac tc, simp)

   922 apply(rule turing_shift)

   923 apply(subgoal_tac "start_of (layout_of aprog) as - Suc 0 

   924                 = length tp1 div 2", simp)

   925 apply(rule_tac pre_lheq, simp, simp, simp)

   926 apply(simp add: startof_not0, simp)

   927 apply(rule_tac s_crsp, simp, simp, simp, simp)

   928 apply(rule tms_ct, simp, simp)

   929 apply(rule tm_ct, simp)

   930 apply(subgoal_tac "ci (layout_of aprog) 

   931                  (start_of (layout_of aprog) as) ins

   932                 = (tms_of aprog ! as)", simp)

   933 apply(simp add: tms_of.simps tpairs_of.simps)

   934 apply(simp add: tms_of.simps tpairs_of.simps abc_fetch.simps)

   935 apply(erule_tac t_split, auto simp: tm_of.simps)

   936 done

   937 

   938 (*

   939 subsection {* The compilation of @{text "Inc n"} *}

   940 *)

   941 

   942 text {*

   943   The lemmas in this section lead to the correctness of 

   944   the compilation of @{text "Inc n"} instruction.

   945 *}

   946 

   947 fun at_begin_fst_bwtn :: "inc_inv_t"

   948   where

   949   "at_begin_fst_bwtn (as, lm) (s, l, r) ires = 

   950       (\<exists> lm1 tn rn. lm1 = (lm @ (0\<^bsup>tn\<^esup>)) \<and> length lm1 = s \<and> 

   951           (if lm1 = [] then l = Bk # Bk # ires

   952            else l = [Bk]@<rev lm1>@Bk#Bk#ires) \<and> r = (Bk\<^bsup>rn\<^esup>))" 

   953 

   954 

   955 fun at_begin_fst_awtn :: "inc_inv_t"

   956   where

   957   "at_begin_fst_awtn (as, lm) (s, l, r) ires = 

   958       (\<exists> lm1 tn rn. lm1 = (lm @ (0\<^bsup>tn\<^esup>)) \<and> length lm1 = s \<and>

   959          (if lm1 = []  then l = Bk # Bk # ires

   960           else l = [Bk]@<rev lm1>@Bk#Bk#ires) \<and> r = [Oc]@Bk\<^bsup>rn\<^esup>

   961   )"

   962 

   963 fun at_begin_norm :: "inc_inv_t"

   964   where

   965   "at_begin_norm (as, lm) (s, l, r) ires= 

   966       (\<exists> lm1 lm2 rn. lm = lm1 @ lm2 \<and> length lm1 = s \<and> 

   967         (if lm1 = [] then l = Bk # Bk # ires

   968          else l = Bk # <rev lm1> @ Bk# Bk # ires ) \<and> r = <lm2> @ (Bk\<^bsup>rn\<^esup>))"

   969 

   970 fun in_middle :: "inc_inv_t"

   971   where

   972   "in_middle (as, lm) (s, l, r) ires = 

   973       (\<exists> lm1 lm2 tn m ml mr rn. lm @ 0\<^bsup>tn\<^esup> = lm1 @ [m] @ lm2

   974        \<and> length lm1 = s \<and> m + 1 = ml + mr \<and>  

   975          ml \<noteq> 0 \<and> tn = s + 1 - length lm \<and> 

   976        (if lm1 = [] then l = Oc\<^bsup>ml\<^esup> @ Bk # Bk # ires 

   977         else l = (Oc\<^bsup>ml\<^esup>)@[Bk]@<rev lm1>@

   978                  Bk # Bk # ires) \<and> (r = (Oc\<^bsup>mr\<^esup>) @ [Bk] @ <lm2>@ (Bk\<^bsup>rn\<^esup>) \<or> 

   979       (lm2 = [] \<and> r = (Oc\<^bsup>mr\<^esup>)))

   980       )"

   981 

   982 fun inv_locate_a :: "inc_inv_t"

   983   where "inv_locate_a (as, lm) (s, l, r) ires = 

   984      (at_begin_norm (as, lm) (s, l, r) ires \<or>

   985       at_begin_fst_bwtn (as, lm) (s, l, r) ires \<or>

   986       at_begin_fst_awtn (as, lm) (s, l, r) ires

   987       )"

   988 

   989 fun inv_locate_b :: "inc_inv_t"

   990   where "inv_locate_b (as, lm) (s, l, r) ires = 

   991         (in_middle (as, lm) (s, l, r)) ires "

   992 

   993 fun inv_after_write :: "inc_inv_t"

   994   where "inv_after_write (as, lm) (s, l, r) ires = 

   995            (\<exists> rn m lm1 lm2. lm = lm1 @ m # lm2 \<and>

   996              (if lm1 = [] then l = Oc\<^bsup>m\<^esup> @ Bk # Bk # ires

   997               else Oc # l = Oc\<^bsup>Suc m \<^esup>@ Bk # <rev lm1> @ 

   998                       Bk # Bk # ires) \<and> r = [Oc] @ <lm2> @ (Bk\<^bsup>rn\<^esup>))"

   999 

  1000 fun inv_after_move :: "inc_inv_t"

  1001   where "inv_after_move (as, lm) (s, l, r) ires = 

  1002       (\<exists> rn m lm1 lm2. lm = lm1 @ m # lm2 \<and>

  1003         (if lm1 = [] then l = Oc\<^bsup>Suc m\<^esup> @ Bk # Bk # ires

  1004          else l = Oc\<^bsup>Suc m\<^esup>@ Bk # <rev lm1> @ Bk # Bk # ires) \<and> 

  1005         r = <lm2> @ (Bk\<^bsup>rn\<^esup>))"

  1006 

  1007 fun inv_after_clear :: "inc_inv_t"

  1008   where "inv_after_clear (as, lm) (s, l, r) ires =

  1009        (\<exists> rn m lm1 lm2 r'. lm = lm1 @ m # lm2 \<and> 

  1010         (if lm1 = [] then l = Oc\<^bsup>Suc m\<^esup> @ Bk # Bk # ires

  1011          else l = Oc\<^bsup>Suc m\<^esup>@ Bk # <rev lm1> @ Bk # Bk # ires) \<and> 

  1012           r = Bk # r' \<and> Oc # r' = <lm2> @ (Bk\<^bsup>rn\<^esup>))"

  1013 

  1014 fun inv_on_right_moving :: "inc_inv_t"

  1015   where "inv_on_right_moving (as, lm) (s, l, r) ires = 

  1016        (\<exists> lm1 lm2 m ml mr rn. lm = lm1 @ [m] @ lm2 \<and> 

  1017             ml + mr = m \<and> 

  1018           (if lm1 = [] then l = Oc\<^bsup>ml\<^esup> @ Bk # Bk # ires

  1019           else l = (Oc\<^bsup>ml\<^esup>) @ [Bk] @ <rev lm1> @ Bk # Bk # ires) \<and> 

  1020          ((r = (Oc\<^bsup>mr\<^esup>) @ [Bk] @ <lm2> @ (Bk\<^bsup>rn\<^esup>)) \<or> 

  1021           (r = (Oc\<^bsup>mr\<^esup>) \<and> lm2 = [])))"

  1022 

  1023 fun inv_on_left_moving_norm :: "inc_inv_t"

  1024   where "inv_on_left_moving_norm (as, lm) (s, l, r) ires =

  1025       (\<exists> lm1 lm2 m ml mr rn. lm = lm1 @ [m] @ lm2 \<and>  

  1026              ml + mr = Suc m \<and> mr > 0 \<and> (if lm1 = [] then l = Oc\<^bsup>ml\<^esup> @ Bk # Bk # ires

  1027                                          else l = (Oc\<^bsup>ml\<^esup>) @ Bk # <rev lm1> @ Bk # Bk # ires)

  1028         \<and> (r = (Oc\<^bsup>mr\<^esup>) @ Bk # <lm2> @ (Bk\<^bsup>rn\<^esup>) \<or> 

  1029            (lm2 = [] \<and> r = Oc\<^bsup>mr\<^esup>)))"

  1030 

  1031 fun inv_on_left_moving_in_middle_B:: "inc_inv_t"

  1032   where "inv_on_left_moving_in_middle_B (as, lm) (s, l, r) ires =

  1033                 (\<exists> lm1 lm2 rn. lm = lm1 @ lm2 \<and>  

  1034                      (if lm1 = [] then l = Bk # ires

  1035                       else l = <rev lm1> @ Bk # Bk # ires) \<and> 

  1036                       r = Bk # <lm2> @ (Bk\<^bsup>rn\<^esup>))"

  1037 

  1038 fun inv_on_left_moving :: "inc_inv_t"

  1039   where "inv_on_left_moving (as, lm) (s, l, r) ires = 

  1040        (inv_on_left_moving_norm  (as, lm) (s, l, r) ires \<or>

  1041         inv_on_left_moving_in_middle_B (as, lm) (s, l, r) ires)"

  1042 

  1043 

  1044 fun inv_check_left_moving_on_leftmost :: "inc_inv_t"

  1045   where "inv_check_left_moving_on_leftmost (as, lm) (s, l, r) ires = 

  1046                 (\<exists> rn. l = ires \<and> r = [Bk, Bk] @ <lm> @ (Bk\<^bsup>rn\<^esup>))"

  1047 

  1048 fun inv_check_left_moving_in_middle :: "inc_inv_t"

  1049   where "inv_check_left_moving_in_middle (as, lm) (s, l, r) ires = 

  1050 

  1051               (\<exists> lm1 lm2 r' rn. lm = lm1 @ lm2 \<and>

  1052                  (Oc # l = <rev lm1> @ Bk # Bk # ires) \<and> r = Oc # Bk # r' \<and> 

  1053                            r' = <lm2> @ (Bk\<^bsup>rn\<^esup>))"

  1054 

  1055 fun inv_check_left_moving :: "inc_inv_t"

  1056   where "inv_check_left_moving (as, lm) (s, l, r) ires = 

  1057              (inv_check_left_moving_on_leftmost (as, lm) (s, l, r) ires \<or>

  1058              inv_check_left_moving_in_middle (as, lm) (s, l, r) ires)"

  1059 

  1060 fun inv_after_left_moving :: "inc_inv_t"

  1061   where "inv_after_left_moving (as, lm) (s, l, r) ires= 

  1062               (\<exists> rn. l = Bk # ires \<and> r = Bk # <lm> @ (Bk\<^bsup>rn\<^esup>))"

  1063 

  1064 fun inv_stop :: "inc_inv_t"

  1065   where "inv_stop (as, lm) (s, l, r) ires= 

  1066               (\<exists> rn. l = Bk # Bk # ires \<and> r = <lm> @ (Bk\<^bsup>rn\<^esup>))"

  1067 

  1068 

  1069 fun inc_inv :: "layout \<Rightarrow> nat \<Rightarrow> inc_inv_t"

  1070   where

  1071   "inc_inv ly n (as, lm) (s, l, r) ires =

  1072               (let ss = start_of ly as in

  1073                let lm' = abc_lm_s lm n ((abc_lm_v lm n)+1) in

  1074                 if s = 0 then False

  1075                 else if s < ss then False

  1076                 else if s < ss + 2 * n then 

  1077                    if (s - ss) mod 2 = 0 then 

  1078                        inv_locate_a (as, lm) ((s - ss) div 2, l, r) ires

  1079                    else inv_locate_b (as, lm) ((s - ss) div 2, l, r) ires

  1080                 else if s = ss + 2 * n then 

  1081                         inv_locate_a (as, lm) (n, l, r) ires

  1082                 else if s = ss + 2 * n + 1 then 

  1083                    inv_locate_b (as, lm) (n, l, r) ires

  1084                 else if s = ss + 2 * n + 2 then 

  1085                    inv_after_write (as, lm') (s - ss, l, r) ires

  1086                 else if s = ss + 2 * n + 3 then 

  1087                    inv_after_move (as, lm') (s - ss, l, r) ires

  1088                 else if s = ss + 2 * n + 4 then 

  1089                    inv_after_clear (as, lm') (s - ss, l, r) ires

  1090                 else if s = ss + 2 * n + 5 then 

  1091                    inv_on_right_moving (as, lm') (s - ss, l, r) ires

  1092                 else if s = ss + 2 * n + 6 then 

  1093                    inv_on_left_moving (as, lm') (s - ss, l, r) ires

  1094                 else if s = ss + 2 * n + 7 then 

  1095                    inv_check_left_moving (as, lm') (s - ss, l, r) ires

  1096                 else if s = ss + 2 * n + 8 then 

  1097                    inv_after_left_moving (as, lm') (s - ss, l, r) ires

  1098                 else if s = ss + 2 * n + 9 then 

  1099                    inv_stop (as, lm') (s - ss, l, r) ires

  1100                 else False) "

  1101 

  1102 lemma fetch_intro: 

  1103   "\<lbrakk>\<And>xs.\<lbrakk>ba = Oc # xs\<rbrakk> \<Longrightarrow> P (fetch prog i Oc);

  1104    \<And>xs.\<lbrakk>ba = Bk # xs\<rbrakk> \<Longrightarrow> P (fetch prog i Bk);

  1105    ba = [] \<Longrightarrow> P (fetch prog i Bk)

  1106    \<rbrakk> \<Longrightarrow> P (fetch prog i 

  1107              (case ba of [] \<Rightarrow> Bk | Bk # xs \<Rightarrow> Bk | Oc # xs \<Rightarrow> Oc))"

  1108 by (auto split:list.splits block.splits)

  1109 

  1110 lemma length_findnth[simp]: "length (findnth n) = 4 * n"

  1111 apply(induct n, simp)

  1112 apply(simp)

  1113 done

  1114 

  1115 declare tshift.simps[simp del]

  1116 declare findnth.simps[simp del]

  1117 

  1118 lemma findnth_nth: 

  1119  "\<lbrakk>n > q; x < 4\<rbrakk> \<Longrightarrow> 

  1120         (findnth n) ! (4 * q + x) = (findnth (Suc q) ! (4 * q + x))"

  1121 apply(induct n, simp)

  1122 apply(case_tac "q < n", simp add: findnth.simps, auto)

  1123 apply(simp add: nth_append)

  1124 apply(subgoal_tac "q = n", simp)

  1125 apply(arith)

  1126 done

  1127 

  1128 lemma Suc_pre[simp]: "\<not> a < start_of ly as \<Longrightarrow> 

  1129           (Suc a - start_of ly as) = Suc (a - start_of ly as)"

  1130 apply(arith)

  1131 done

  1132 

  1133 lemma fetch_locate_a_o: "

  1134 \<And>a  q xs.

  1135     \<lbrakk>\<not> a < start_of (layout_of aprog) as;