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 (*  FIXME: doubly defined

   181 text {*

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

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

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

   185   *}

   186 

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

   188   where

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

   190        (action, (if state = 0 then 0

   191                  else state + off))) tp)"

   192 *)

   193 

   194 text {*

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

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

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

   198   Abacus program.

   199 *}

   200 

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

   202   where

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

   204 

   205 text {*

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

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

   208   of cells afterwards to the left accordingly.

   209   *}

   210 

   211 definition tdec_b :: "tprog"

   212   where

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

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

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

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

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

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

   219 

   220 text {*

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

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

   223   *}

   224 

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

   226   where

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

   228 

   229 text {*

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

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

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

   233   Abacus program.

   234 *}

   235 

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

   237   where

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

   239                  (ss - 1)) e"

   240  

   241 text {*

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

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

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

   245 *}

   246 

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

   248   where

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

   250 

   251 text {*

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

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

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

   255   in the Abacus program.

   256 *}

   257 

   258 type_synonym layout = "nat list"

   259 

   260 text {*

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

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

   263 *}

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

   265   where

   266   "length_of i = (case i of 

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

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

   269                     Goto n  \<Rightarrow> 1)"

   270 

   271 text {*

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

   273 *}

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

   275   where "layout_of ap = map length_of ap"

   276 

   277 

   278 text {*

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

   280   TM in the finall TM.

   281 *}

   282 

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

   284   where

   285   "start_of ly 0 = Suc 0" |

   286   "start_of ly (Suc as) = 

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

   288          else start_of ly as)"

   289 

   290 text {*

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

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

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

   294 *}

   295 

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

   297   where

   298   "ci ly ss i = (case i of 

   299                     Inc n   \<Rightarrow> tinc ss n |

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

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

   302 

   303 text {*

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

   305   every instruction with its starting state.

   306 *}

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

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

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

   310 

   311 

   312 text {*

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

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

   315 *}

   316 

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

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

   319                          (tpairs_of ap)"

   320 

   321 text {*

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

   323 *}

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

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

   326 

   327 text {*

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

   329 *}

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

   331   where

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

   333 

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

   335   where 

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

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

   338 

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

   340 apply(induct n, simp, simp)

   341 done

   342 

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

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

   345                  split: abc_inst.splits)

   346 done

   347 

   348 subsection {*

   349   Representation of Abacus memory by TM tape

   350 *}

   351 

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

   353 

   354 text {*

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

   356   Abacus memory @{text "am"}.

   357   *}

   358 

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

   360   where 

   361   "tape_of_nat_list [] = []" |

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

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

   364 

   365 defs (overloaded)

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

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

   368 

   369 text {*

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

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

   372 *}

   373 

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

   375   where 

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

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

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

   379 

   380 declare crsp_l.simps[simp del]

   381 

   382 subsection {*

   383   A more general definition of TM execution. 

   384 *}

   385 

   386 (*

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

   388   where

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

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

   391 

   392 thm nth_of.simps

   393 

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

   395   where

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

   397   "nfetch p (Suc s) b = 

   398              (case b of 

   399                 Bk \<Rightarrow> nnth_of p s 0 |

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

   401 *)

   402 

   403 text {*

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

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

   406 *}

   407 

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

   409   where 

   410   "t_step c (p, off) = 

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

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

   413                              (case rightn of 

   414                                 [] \<Rightarrow> Bk | 

   415                                 Bk # xs \<Rightarrow> Bk |

   416                                 Oc # xs \<Rightarrow> Oc

   417                              ) 

   418              in 

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

   420 

   421 

   422 text {*

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

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

   425 *}

   426 

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

   428   where

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

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

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

   432 

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

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

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

   436 apply(simp add: t_steps.simps)

   437 done

   438 

   439 text {*

   440   The type of invarints expressing correspondence between 

   441   Abacus configuration and TM configuration.

   442 *}

   443 

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

   445 

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

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

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

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

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

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

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

   453         abc2t_correct.simps[simp del]

   454 

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

   456 apply(simp add: t_ncorrect.simps)

   457 done

   458 

   459 lemma t_shift_fetch: 

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

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

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

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

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

   465 apply(case_tac x, simp)

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

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

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

   469 apply(case_tac b, simp)

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

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

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

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

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

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

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

   477 done

   478 

   479 lemma t_shift_in_step:

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

   481         t_ncorrect tp1; t_ncorrect tp;

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

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

   484 apply(simp add: t_step.simps)

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

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

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

   488                    \<Rightarrow> x)")

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

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

   491 apply(auto intro: t_shift_fetch)

   492 apply(case_tac ba, simp, simp)

   493 apply(case_tac aaa, simp, simp)

   494 done

   495 

   496 declare add_Suc_right[simp del]

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

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

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

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

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

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

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

   504                          (p, off) n")

   505 apply(simp, simp add: stepn)

   506 apply(simp only: t_steps.simps)

   507 apply(simp only: add_Suc_right)

   508 done

   509 declare add_Suc_right[simp]

   510 

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

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

   513          length tp div 2)\<rbrakk>

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

   515 apply(auto)

   516 apply(simp add: fetch.simps)

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

   518 apply(erule exE, simp)

   519 apply(case_tac x, simp)

   520 apply(auto simp add: fetch.simps)

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

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

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

   524      , simp)

   525 done 

   526 

   527 lemma conf_keep_step: 

   528       "\<lbrakk>t_ncorrect tp; 

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

   530        length tp div 2)\<rbrakk>

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

   532 apply(simp add: t_step.simps)

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

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

   535 apply(simp add: new_tape.simps)

   536 apply(rule s_out_fetch, simp, simp)

   537 done

   538 

   539 lemma conf_keep: 

   540       "\<lbrakk>t_ncorrect tp; 

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

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

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

   544 apply(induct n, simp)

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

   546 apply(rule_tac conf_keep_step, simp+)

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

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

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

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

   551 apply(simp)

   552 apply(rule_tac conf_keep_step, simp, simp)

   553 apply(rule stepn)

   554 done

   555 

   556 lemma state_bef_inside: 

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

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

   559       length tp1 div 2 < s0 \<and> 

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

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

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

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

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

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

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

   567 apply(simp only: t_step_add)

   568 apply(rule classical)

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

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

   571 apply(simp)

   572 apply(rule conf_keep, simp, simp, simp)

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

   574 done

   575 

   576 lemma turing_shift_inside: 

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

   578          length tp1 div 2 < s0 \<and> 

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

   580          t_ncorrect tp1; t_ncorrect tp;

   581          length tp1 div 2 < s \<and> 

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

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

   584 apply(induct stp arbitrary: s l r)

   585 apply(simp add: t_steps.simps)

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

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

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

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

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

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

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

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

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

   595 apply(simp only: stepn, simp)

   596 apply(rule_tac t_shift_in_step, simp+)

   597 defer

   598 apply(rule stepn)

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

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

   601 done

   602 

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

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

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

   606 apply(case_tac as, simp, simp)

   607 done

   608 

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

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

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

   612 by auto

   613 

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

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

   616 apply(drule_tac concat_suc, simp)

   617 done

   618 

   619 lemma concat_drop_suc_iff: 

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

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

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

   623 apply(case_tac tps, simp, simp)

   624 apply(case_tac n, simp, simp)

   625 done

   626 

   627 declare append_assoc[simp del]

   628 

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

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

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

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

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

   634 apply(auto)

   635 apply(induct n, simp)

   636 apply(case_tac tps, simp, simp, simp)

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

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

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

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

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

   642 apply(rule_tac concat_drop_suc_iff, simp)

   643 apply(rule_tac concat_take_suc_iff, simp)

   644 done

   645 

   646 declare append_assoc[simp]

   647 

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

   649 by(auto)

   650 

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

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

   653 done

   654 

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

   656                 abc_fetch as aprog = Some ins\<rbrakk>

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

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

   659       abc_fetch.simps  map_of del: map_append)

   660 done

   661 

   662 lemma t_split:"\<lbrakk>

   663         ly = layout_of aprog;

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

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

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

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

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

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

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

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

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

   673 apply(rule_tac ci_nth, auto)

   674 done

   675 

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

   677 by auto

   678 

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

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

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

   682 done

   683 

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

   685                            t_ncorrect tp"

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

   687 apply(auto)

   688 apply(simp add:list_all_iff, auto)

   689 done

   690 

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

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

   693 apply(drule mod_eqD)+

   694 apply(auto)

   695 done

   696 

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

   698            (x + y) mod 2 = 0"

   699 apply(auto)

   700 done

   701 

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

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

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

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

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

   707 apply(simp add: t_ncorrect.simps)

   708 apply(rule_tac div_apart_iff, simp)

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

   710             simp add: t_ncorrect.simps)

   711 apply(rule_tac tm_ct, simp)

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

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

   714 done

   715 

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

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

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

   719                  length (tms_of aprog ! as) div 2"

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

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

   722 apply(rule_tac div_apart)

   723 apply(rule tct_div2, simp)+

   724 apply(erule_tac tms_ct, simp)

   725 apply(rule_tac tm_ct, simp)

   726 apply(rule_tac nth_mem)

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

   728 done

   729 

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

   731 apply(auto simp: layout_of.simps)

   732 done

   733 

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

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

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

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

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

   739                  tpairs_of.simps)

   740 apply(simp add: ci_length)

   741 done

   742 

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

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

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

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

   747 apply(auto)

   748 done

   749 

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

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

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

   753 apply(rule ci_length)

   754 done

   755  

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

   757 apply(induct n, simp)

   758 apply(simp)

   759 done

   760 

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

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

   763               split: abc_inst.splits, auto)

   764 apply(simp add: findnth_length2)+

   765 done

   766 

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

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

   769 apply(simp add: tms_of.simps)

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

   771               (tpairs_of aprog) ! as

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

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

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

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

   776                  2 * (length_of b)", simp)

   777 apply(rule ci_length2)

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

   779 done

   780 

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

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

   783 apply(induct as, simp, simp)

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

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

   786                        (tms_of aprog ! as)", auto)

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

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

   789 done

   790 

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

   792        \<Longrightarrow> ci (layout_of aprog) 

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

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

   795 done

   796 

   797 lemma startof_not0: "start_of ly as > 0"

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

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

   800 done

   801 

   802 declare abc_step_l.simps[simp del]

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

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

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

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

   807 proof - 

   808   fix as tp

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

   810      start_of (layout_of aprog) as - Suc 0 = 

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

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

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

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

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

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

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

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

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

   820                        length (tms_of aprog ! as)) div 2

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

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

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

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

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

   826            rule_tac startof_not0)

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

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

   829     apply(rule take_Suc_last, simp)

   830     done

   831 qed

   832 

   833 lemma crsp2stateq: 

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

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

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

   837 apply(simp add: crsp_l.simps)

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

   839 , simp)   

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

   841       auto intro: startof_not0)

   842 done

   843 

   844 lemma turing_shift_outside: 

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

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

   847        length tp1 div 2 < s0 \<and> 

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

   849        t_ncorrect tp1; t_ncorrect tp;

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

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

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

   853                 = (s, l, r)"

   854 apply(rule_tac x = stp in exI)

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

   856 apply(simp only: stepn)

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

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

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

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

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

   862 apply(rule_tac t_shift_in_step, simp+)

   863 apply(rule_tac turing_shift_inside, simp+)

   864 apply(rule classical)

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

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

   867 apply(rule_tac conf_keep_step, simp+)

   868 done

   869 

   870 lemma turing_shift: 

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

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

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

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

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

   876                     (s, (l, r))"

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

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

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

   880                    (s, l, r)")

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

   882 apply(rule_tac turing_shift_inside, simp+)

   883 apply(rule_tac turing_shift_outside, simp+)

   884 done

   885 

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

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

   888 apply(simp add: start_of.simps)

   889 done

   890 

   891 lemma s_crsp:

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

   893   abc2t_correct aprog;

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

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

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

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

   898          ins) div 2"

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

   900                    2 + 1", simp)

   901 apply(rule_tac ci_length_not0)

   902 apply(rule crsp2stateq, simp+)

   903 done

   904 

   905 lemma tms_out_ex:

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

   907   abc2t_correct aprog;

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

   909   abc_fetch as aprog = Some ins;

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

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

   912   n > 0; 

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

   914   s = start_of ly as'

   915   \<rbrakk>

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

   917 apply(simp only: tm_of.simps)

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

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

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

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

   922 apply(erule exE, erule exE, erule conjE, erule conjE,

   923       case_tac tc, simp)

   924 apply(rule turing_shift)

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

   926                 = length tp1 div 2", simp)

   927 apply(rule_tac pre_lheq, simp, simp, simp)

   928 apply(simp add: startof_not0, simp)

   929 apply(rule_tac s_crsp, simp, simp, simp, simp)

   930 apply(rule tms_ct, simp, simp)

   931 apply(rule tm_ct, simp)

   932 apply(subgoal_tac "ci (layout_of aprog) 

   933                  (start_of (layout_of aprog) as) ins

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

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

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

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

   938 done

   939 

   940 (*

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

   942 *)

   943 

   944 text {*

   945   The lemmas in this section lead to the correctness of 

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

   947 *}

   948 

   949 fun at_begin_fst_bwtn :: "inc_inv_t"

   950   where

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

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

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

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

   955 

   956 

   957 fun at_begin_fst_awtn :: "inc_inv_t"

   958   where

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

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

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

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

   963   )"

   964 

   965 fun at_begin_norm :: "inc_inv_t"

   966   where

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

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

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

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

   971 

   972 fun in_middle :: "inc_inv_t"

   973   where

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

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

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

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

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

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

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

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

   982       )"

   983 

   984 fun inv_locate_a :: "inc_inv_t"

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

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

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

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

   989       )"

   990 

   991 fun inv_locate_b :: "inc_inv_t"

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

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

   994 

   995 fun inv_after_write :: "inc_inv_t"

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

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

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

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

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

  1001 

  1002 fun inv_after_move :: "inc_inv_t"

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

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

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

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

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

  1008 

  1009 fun inv_after_clear :: "inc_inv_t"

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

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

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

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

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

  1015 

  1016 fun inv_on_right_moving :: "inc_inv_t"

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

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

  1019             ml + mr = m \<and> 

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

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

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

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

  1024 

  1025 fun inv_on_left_moving_norm :: "inc_inv_t"

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

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

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

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

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

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

  1032 

  1033 fun inv_on_left_moving_in_middle_B:: "inc_inv_t"

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

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

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

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

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

  1039 

  1040 fun inv_on_left_moving :: "inc_inv_t"

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

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

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

  1044 

  1045 

  1046 fun inv_check_left_moving_on_leftmost :: "inc_inv_t"

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

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

  1049 

  1050 fun inv_check_left_moving_in_middle :: "inc_inv_t"

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

  1052 

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

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

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

  1056 

  1057 fun inv_check_left_moving :: "inc_inv_t"

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

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

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

  1061 

  1062 fun inv_after_left_moving :: "inc_inv_t"

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

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

  1065 

  1066 fun inv_stop :: "inc_inv_t"

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

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

  1069 

  1070 

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

  1072   where

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

  1074               (let ss = start_of ly as in

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

  1076                 if s = 0 then False

  1077                 else if s < ss then False

  1078                 else if s < ss + 2 * n then 

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

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

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

  1082                 else if s = ss + 2 * n then 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  1102                 else False) "

  1103 

  1104 lemma fetch_intro: 

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

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

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

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

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

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

  1111 

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

  1113 apply(induct n, simp)

  1114 apply(simp)

  1115 done

  1116 

  1117 declare tshift.simps[simp del]

  1118 declare findnth.simps[simp del]

  1119 

  1120 lemma findnth_nth: 

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

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

  1123 apply(induct n, simp)

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

  1125 apply(simp add: nth_append)

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

  1127 apply(arith)

  1128 done

  1129 

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

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

  1132 apply(arith)

  1133 done

  1134 

  1135 lemma fetch_locate_a_o: "