1 header {* 

     2  {\em abacus} a kind of register machine

     3 *}

     4 

     5 theory Abacus

     6 imports Uncomputable

     7 begin

     8 

     9 (*

    10 declare tm_comp.simps [simp add] 

    11 declare adjust.simps[simp add] 

    12 declare shift.simps[simp add]

    13 declare tm_wf.simps[simp add]

    14 declare step.simps[simp add]

    15 declare steps.simps[simp add]

    16 *)

    17 declare replicate_Suc[simp add]

    18 

    19 text {*

    20   {\em Abacus} instructions:

    21 *}

    22 

    23 datatype abc_inst =

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

    25      *}

    26      Inc nat

    27   -- {*

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

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

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

    31      *}

    32    | Dec nat nat

    33   -- {*

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

    35   *}

    36    | Goto nat

    37   

    38 

    39 text {*

    40   Abacus programs are defined as lists of Abacus instructions.

    41 *}

    42 type_synonym abc_prog = "abc_inst list"

    43 

    44 section {*

    45   Sample Abacus programs

    46   *}

    47 

    48 text {*

    49   Abacus for addition and clearance.

    50 *}

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

    52   where

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

    54 

    55 text {*

    56   Abacus for clearing memory untis.

    57 *}

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

    59   where

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

    61 

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

    63   where

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

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

    66 

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

    68   where

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

    70 

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

    72   where

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

    74 

    75 

    76 text {*

    77   The state of Abacus machine.

    78   *}

    79 type_synonym abc_state = nat

    80 

    81 (* text {*

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

    83 *}

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

    85 

    86 text {*

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

    88   every units addressed by index into the list.

    89   *}

    90 type_synonym abc_lm = "nat list"

    91 

    92 text {*

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

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

    95 *}

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

    97   where 

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

    99 

   100 

   101 text {*

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

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

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

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

   106 *}

   107 

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

   109   where

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

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

   112 

   113 

   114 text {*

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

   116   current memory:

   117 *}

   118 type_synonym abc_conf = "abc_state \<times> abc_lm"

   119 

   120 text {*

   121   Fetch instruction out of Abacus program:

   122 *}

   123 

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

   125   where

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

   127                     else None)"

   128 

   129 text {*

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

   131   configuration does not change.

   132 *}

   133 fun abc_step_l :: "abc_conf \<Rightarrow> abc_inst option \<Rightarrow> abc_conf"

   134   where

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

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

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

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

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

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

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

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

   143                )"

   144 

   145 text {*

   146   Multi-step execution of Abacus machine.

   147 *}

   148 fun abc_steps_l :: "abc_conf \<Rightarrow> abc_prog \<Rightarrow> nat \<Rightarrow> abc_conf"

   149   where

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

   151   "abc_steps_l (s, lm) p (Suc n) = 

   152       abc_steps_l (abc_step_l (s, lm) (abc_fetch s p)) p n"

   153 

   154 section {*

   155   Compiling Abacus machines into Truing machines

   156 *}

   157 

   158 subsection {*

   159   Compiling functions

   160 *}

   161 

   162 text {*

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

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

   165   on the way.

   166 *}

   167 

   168 fun findnth :: "nat \<Rightarrow> instr list"

   169   where

   170   "findnth 0 = []" |

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

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

   173 

   174 text {*

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

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

   177   of cells afterwards to the right accordingly.

   178   *}

   179 

   180 definition tinc_b :: "instr list"

   181   where

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

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

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

   185 

   186 text {*

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

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

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

   190   Abacus program.

   191 *}

   192 

   193 fun tinc :: "nat \<Rightarrow> nat \<Rightarrow> instr list"

   194   where

   195   "tinc ss n = shift (findnth n @ shift tinc_b (2 * n)) (ss - 1)"

   196 

   197 text {*

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

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

   200   of cells afterwards to the left accordingly.

   201   *}

   202 

   203 definition tdec_b :: "instr list"

   204   where

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

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

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

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

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

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

   211 

   212 text {*

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

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

   215   *}

   216 

   217 fun sete :: "instr list \<Rightarrow> nat \<Rightarrow> instr list"

   218   where

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

   220 

   221 text {*

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

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

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

   225   Abacus program.

   226 *}

   227 

   228 fun tdec :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> instr list"

   229   where

   230   "tdec ss n e = shift (findnth n) (ss - 1) @ sete (shift (shift tdec_b (2 * n)) (ss - 1)) e"

   231  

   232 text {*

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

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

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

   236 *}

   237 

   238 fun tgoto :: "nat \<Rightarrow> instr list"

   239   where

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

   241 

   242 text {*

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

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

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

   246   in the Abacus program.

   247 *}

   248 

   249 type_synonym layout = "nat list"

   250 

   251 text {*

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

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

   254 *}

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

   256   where

   257   "length_of i = (case i of 

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

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

   260                     Goto n  \<Rightarrow> 1)"

   261 

   262 text {*

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

   264 *}

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

   266   where "layout_of ap = map length_of ap"

   267 

   268 

   269 text {*

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

   271   TM in the finall TM.

   272 *}

   273 thm listsum_def

   274 

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

   276   where

   277   "start_of ly x = (Suc (listsum (take x ly))) "

   278 

   279 text {*

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

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

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

   283 *}

   284 

   285 fun ci :: "layout \<Rightarrow> nat \<Rightarrow> abc_inst \<Rightarrow> instr list"

   286   where

   287   "ci ly ss (Inc n) = tinc ss n"

   288 | "ci ly ss (Dec n e) = tdec ss n (start_of ly e)"

   289 | "ci ly ss (Goto n) = tgoto (start_of ly n)"

   290 

   291 text {*

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

   293   every instruction with its starting state.

   294 *}

   295 

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

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

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

   299 

   300 text {*

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

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

   303 *}

   304 

   305 fun tms_of :: "abc_prog \<Rightarrow> (instr list) list"

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

   307                          (tpairs_of ap)"

   308 

   309 text {*

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

   311 *}

   312 fun tm_of :: "abc_prog \<Rightarrow> instr list"

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

   314 

   315 text {*

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

   317 *}

   318 (*

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

   320   where

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

   322 

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

   324   where 

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

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

   327 *)

   328 

   329 lemma length_findnth: 

   330   "length (findnth n) = 4 * n"

   331 apply(induct n, auto)

   332 done

   333 

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

   335 apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth

   336                  split: abc_inst.splits)

   337 done

   338 

   339 subsection {*

   340   Representation of Abacus memory by TM tape

   341 *}

   342 

   343 text {*

   344   @{text "crsp acf tcf"} meams the abacus configuration @{text "acf"}

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

   346 *}

   347 

   348 fun crsp :: "layout \<Rightarrow> abc_conf \<Rightarrow> config \<Rightarrow> cell list \<Rightarrow> bool"

   349   where 

   350   "crsp ly (as, lm) (s, l, r) inres = 

   351            (s = start_of ly as \<and> (\<exists> x. r = <lm> @ Bk\<up>x) \<and> 

   352             l = Bk # Bk # inres)"

   353 

   354 declare crsp.simps[simp del]

   355 

   356 subsection {*

   357   A more general definition of TM execution. 

   358 *}

   359 

   360 (*

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

   362   where

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

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

   365 

   366 thm nth_of.simps

   367 

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

   369   where

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

   371   "nfetch p (Suc s) b = 

   372              (case b of 

   373                 Bk \<Rightarrow> nnth_of p s 0 |

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

   375 *)

   376 

   377                     

   378 text {*

   379   The type of invarints expressing correspondence between 

   380   Abacus configuration and TM configuration.

   381 *}

   382 

   383 type_synonym inc_inv_t = "abc_conf \<Rightarrow> config \<Rightarrow> cell list \<Rightarrow> bool"

   384 

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

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

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

   388         ci.simps [simp del] length_of.simps[simp del] 

   389         layout_of.simps[simp del]

   390 

   391 (*

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

   393 *)

   394 

   395 text {*

   396   The lemmas in this section lead to the correctness of 

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

   398 *}

   399 

   400 declare abc_step_l.simps[simp del] abc_steps_l.simps[simp del]

   401 lemma [simp]: "start_of ly as > 0"

   402 apply(simp add: start_of.simps)

   403 done

   404 

   405 lemma abc_steps_l_0: "abc_steps_l ac ap 0 = ac"

   406 by(case_tac ac, simp add: abc_steps_l.simps)

   407 

   408 lemma abc_step_red: 

   409  "abc_steps_l (as, am) ap stp = (bs, bm) \<Longrightarrow> 

   410   abc_steps_l (as, am) ap (Suc stp) = abc_step_l (bs, bm) (abc_fetch bs ap) "

   411 proof(induct stp arbitrary: as am bs bm)

   412   case 0

   413   thus "?case"

   414     by(simp add: abc_steps_l.simps abc_steps_l_0)

   415 next

   416   case (Suc stp as am bs bm)

   417   have ind: "\<And>as am bs bm. abc_steps_l (as, am) ap stp = (bs, bm) \<Longrightarrow> 

   418     abc_steps_l (as, am) ap (Suc stp) = abc_step_l (bs, bm) (abc_fetch bs ap)"

   419     by fact

   420   have h:" abc_steps_l (as, am) ap (Suc stp) = (bs, bm)" by fact

   421   obtain as' am' where g: "abc_step_l (as, am) (abc_fetch as ap) = (as', am')"

   422     by(case_tac "abc_step_l (as, am) (abc_fetch as ap)", auto)

   423   then have "abc_steps_l (as', am') ap (Suc stp) = abc_step_l (bs, bm) (abc_fetch bs ap)"

   424     using h

   425     by(rule_tac ind, simp add: abc_steps_l.simps)

   426   thus "?case"

   427     using g

   428     by(simp add: abc_steps_l.simps)

   429 qed

   430 

   431 lemma tm_shift_fetch: 

   432   "\<lbrakk>fetch A s b = (ac, ns); ns \<noteq> 0 \<rbrakk>

   433   \<Longrightarrow> fetch (shift A off) s b = (ac, ns + off)"

   434 apply(case_tac b)

   435 apply(case_tac [!] s, auto simp: fetch.simps shift.simps)

   436 done

   437 

   438 lemma tm_shift_eq_step:

   439   assumes exec: "step (s, l, r) (A, 0) = (s', l', r')"

   440   and notfinal: "s' \<noteq> 0"

   441   shows "step (s + off, l, r) (shift A off, off) = (s' + off, l', r')"

   442 using assms

   443 apply(simp add: step.simps)

   444 apply(case_tac "fetch A s (read r)", auto)

   445 apply(drule_tac [!] off = off in tm_shift_fetch, simp_all)

   446 done

   447 

   448 declare step.simps[simp del] steps.simps[simp del] shift.simps[simp del]

   449 

   450 lemma tm_shift_eq_steps: 

   451   assumes exec: "steps (s, l, r) (A, 0) stp = (s', l', r')"

   452   and notfinal: "s' \<noteq> 0"

   453   shows "steps (s + off, l, r) (shift A off, off) stp = (s' + off, l', r')"

   454   using exec notfinal

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

   456   fix stp s' l' r'

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

   458      \<Longrightarrow> steps (s + off, l, r) (shift A off, off) stp = (s' + off, l', r')"

   459   and h: " steps (s, l, r) (A, 0) (Suc stp) = (s', l', r')" "s' \<noteq> 0"

   460   obtain s1 l1 r1 where g: "steps (s, l, r) (A, 0) stp = (s1, l1, r1)" 

   461     apply(case_tac "steps (s, l, r) (A, 0) stp") by blast

   462   moreover then have "s1 \<noteq> 0"

   463     using h

   464     apply(simp add: step_red)

   465     apply(case_tac "0 < s1", auto)

   466     done

   467   ultimately have "steps (s + off, l, r) (shift A off, off) stp =

   468                    (s1 + off, l1, r1)"

   469     apply(rule_tac ind, simp_all)

   470     done

   471   thus "steps (s + off, l, r) (shift A off, off) (Suc stp) = (s' + off, l', r')"

   472     using h g assms

   473     apply(simp add: step_red)

   474     apply(rule_tac tm_shift_eq_step, auto)

   475     done

   476 qed

   477 

   478 lemma startof_not0[simp]: "0 < start_of ly as"

   479 apply(simp add: start_of.simps)

   480 done

   481 

   482 lemma startof_ge1[simp]: "Suc 0 \<le> start_of ly as"

   483 apply(simp add: start_of.simps)

   484 done

   485 

   486 lemma start_of_Suc1: "\<lbrakk>ly = layout_of ap; 

   487        abc_fetch as ap = Some (Inc n)\<rbrakk>

   488        \<Longrightarrow> start_of ly (Suc as) = start_of ly as + 2 * n + 9"

   489 apply(auto simp: start_of.simps layout_of.simps  

   490                  length_of.simps abc_fetch.simps 

   491                  take_Suc_conv_app_nth split: if_splits)

   492 done

   493 

   494 lemma start_of_Suc2:

   495   "\<lbrakk>ly = layout_of ap;

   496   abc_fetch as ap = Some (Dec n e)\<rbrakk> \<Longrightarrow> 

   497         start_of ly (Suc as) = 

   498             start_of ly as + 2 * n + 16"

   499 apply(auto simp: start_of.simps layout_of.simps  

   500                  length_of.simps abc_fetch.simps 

   501                  take_Suc_conv_app_nth split: if_splits)

   502 done

   503 

   504 lemma start_of_Suc3:

   505   "\<lbrakk>ly = layout_of ap;

   506   abc_fetch as ap = Some (Goto n)\<rbrakk> \<Longrightarrow> 

   507   start_of ly (Suc as) = start_of ly as + 1"

   508 apply(auto simp: start_of.simps layout_of.simps  

   509                  length_of.simps abc_fetch.simps 

   510                  take_Suc_conv_app_nth split: if_splits)

   511 done

   512 

   513 lemma length_ci_inc: 

   514   "length (ci ly ss (Inc n)) = 4*n + 18"

   515 apply(auto simp: ci.simps length_findnth tinc_b_def)

   516 done

   517 

   518 lemma length_ci_dec: 

   519   "length (ci ly ss (Dec n e)) = 4*n + 32"

   520 apply(auto simp: ci.simps length_findnth tdec_b_def)

   521 done

   522 

   523 lemma length_ci_goto: 

   524   "length (ci ly ss (Goto n )) = 2"

   525 apply(auto simp: ci.simps length_findnth tdec_b_def)

   526 done

   527 

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

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

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

   531 apply(case_tac as, simp, simp)

   532 done

   533 

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

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

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

   537 by auto

   538 

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

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

   541 apply(drule_tac concat_suc, simp)

   542 done

   543 

   544 lemma concat_drop_suc_iff: 

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

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

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

   548 apply(case_tac tps, simp, simp)

   549 apply(case_tac n, simp, simp)

   550 done

   551 

   552 declare append_assoc[simp del]

   553 

   554 lemma  tm_append:

   555   "\<lbrakk>n < length tps; tp = tps ! n\<rbrakk> \<Longrightarrow> 

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

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

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

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

   560 apply(auto)

   561 apply(induct n, simp)

   562 apply(case_tac tps, simp, simp, simp)

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

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

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

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

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

   568 apply(rule_tac concat_drop_suc_iff, simp)

   569 apply(rule_tac concat_take_suc_iff, simp)

   570 done

   571 

   572 declare append_assoc[simp]

   573 

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

   575 by(auto)

   576 

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

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

   579 done

   580 

   581 lemma ci_nth: 

   582   "\<lbrakk>ly = layout_of aprog; 

   583   abc_fetch as aprog = Some ins\<rbrakk>

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

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

   586       abc_fetch.simps  map_of del: map_append split: if_splits)

   587 done

   588 

   589 lemma t_split:"\<lbrakk>

   590         ly = layout_of aprog;

   591         abc_fetch as aprog = Some ins\<rbrakk>

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

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

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

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

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

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

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

   599 apply(subgoal_tac "length (tms_of aprog) = length aprog")

   600 apply(simp add: abc_fetch.simps split: if_splits, simp)

   601 apply(rule_tac ci_nth, auto)

   602 done

   603 

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

   605 by auto

   606 

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

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

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

   610 done

   611 

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

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

   614 apply(drule mod_eqD)+

   615 apply(auto)

   616 done

   617 

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

   619            (x + y) mod 2 = 0"

   620 apply(auto)

   621 done

   622 

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

   624 apply(auto simp: layout_of.simps)

   625 done

   626 

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

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

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

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

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

   632                  tpairs_of.simps)

   633 apply(simp add: ci_length take_Suc take_Suc_conv_app_nth)

   634 done

   635 

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

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

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

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

   640 apply(auto)

   641 done

   642 

   643 lemma [simp]: 

   644   "\<lbrakk>as < length aprog; (abc_fetch as aprog) = Some ins\<rbrakk>

   645   \<Longrightarrow> ci (layout_of aprog) 

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

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

   648 done

   649 

   650 lemma [simp]: "length (tms_of ap) = length ap"

   651 by(auto simp: tms_of.simps tpairs_of.simps)

   652 

   653 lemma [intro]:  "n < length ap \<Longrightarrow> length (tms_of ap ! n) mod 2 = 0"

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

   655 apply(case_tac "ap ! n", auto simp: ci.simps length_findnth tinc_b_def tdec_b_def)

   656 apply arith

   657 by arith

   658 

   659 lemma compile_mod2: "length (concat (take n (tms_of ap))) mod 2 = 0"

   660 apply(induct n, auto)

   661 apply(case_tac "n < length (tms_of ap)", simp add: take_Suc_conv_app_nth, auto)

   662 apply(subgoal_tac "length (tms_of ap ! n) mod 2 = 0")

   663 apply arith

   664 by auto

   665 

   666 lemma tpa_states:

   667   "\<lbrakk>tp = concat (take as (tms_of ap));

   668   as \<le> length ap\<rbrakk> \<Longrightarrow> 

   669   start_of (layout_of ap) as = Suc (length tp div 2)"

   670 proof(induct as arbitrary: tp)

   671   case 0

   672   thus "?case"

   673     by(simp add: start_of.simps)

   674 next

   675   case (Suc as tp)

   676   have ind: "\<And>tp. \<lbrakk>tp = concat (take as (tms_of ap)); as \<le> length ap\<rbrakk> \<Longrightarrow>

   677     start_of (layout_of ap) as = Suc (length tp div 2)" by fact

   678   have tp: "tp = concat (take (Suc as) (tms_of ap))" by fact

   679   have le: "Suc as \<le> length ap" by fact

   680   have a: "start_of (layout_of ap) as = Suc (length (concat (take as (tms_of ap))) div 2)"

   681     using le

   682     by(rule_tac ind, simp_all)

   683   from a tp le show "?case"

   684     apply(simp add: start_of.simps take_Suc_conv_app_nth)

   685     apply(subgoal_tac "length (concat (take as (tms_of ap))) mod 2= 0")

   686     apply(subgoal_tac " length (tms_of ap ! as) mod 2 = 0")

   687     apply(simp add: Abacus.div_apart) 

   688     apply(simp add: layout_of.simps ci_length  tms_of.simps tpairs_of.simps)

   689     apply(auto  intro: compile_mod2)

   690     done

   691 qed

   692 

   693 lemma append_append_fetch: 

   694     "\<lbrakk>length tp1 mod 2 = 0; length tp mod 2 = 0;

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

   696     \<Longrightarrow>fetch (tp1 @ tp @ tp2) a b = fetch tp (a - length tp1 div 2) b "

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

   698 apply(case_tac x, simp)

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

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

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

   702 apply(case_tac b, simp)

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

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

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

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

   707 apply(auto simp: nth_append)

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

   709 done

   710 

   711 lemma step_eq_fetch':

   712   assumes layout: "ly = layout_of ap"

   713   and compile: "tp = tm_of ap"

   714   and fetch: "abc_fetch as ap = Some ins"

   715   and range1: "s \<ge> start_of ly as"

   716   and range2: "s < start_of ly (Suc as)"

   717   shows "fetch tp s b = fetch (ci ly (start_of ly as) ins)

   718        (Suc s - start_of ly as) b "

   719 proof -

   720   have "\<exists>tp1 tp2. concat (tms_of ap) = tp1 @ ci ly (start_of ly as) ins @ tp2 \<and>

   721     tp1 = concat (take as (tms_of ap)) \<and> tp2 = concat (drop (Suc as) (tms_of ap))"

   722     using assms

   723     by(rule_tac t_split, simp_all)

   724   then obtain tp1 tp2 where a: "concat (tms_of ap) = tp1 @ ci ly (start_of ly as) ins @ tp2 \<and>

   725     tp1 = concat (take as (tms_of ap)) \<and> tp2 = concat (drop (Suc as) (tms_of ap))" by blast

   726   then have b: "start_of (layout_of ap) as = Suc (length tp1 div 2)"

   727     using fetch

   728     apply(rule_tac tpa_states, simp, simp add: abc_fetch.simps split: if_splits)

   729     done

   730   have "fetch (tp1 @ (ci ly (start_of ly as) ins) @ tp2)  s b = 

   731         fetch (ci ly (start_of ly as) ins) (s - length tp1 div 2) b"

   732   proof(rule_tac append_append_fetch)

   733     show "length tp1 mod 2 = 0"

   734       using a

   735       by(auto, rule_tac compile_mod2)

   736   next

   737     show "length (ci ly (start_of ly as) ins) mod 2 = 0"

   738       apply(case_tac ins, auto simp: ci.simps length_findnth tinc_b_def tdec_b_def)

   739       by(arith, arith)

   740   next

   741     show "length tp1 div 2 < s \<and> s \<le> 

   742       length tp1 div 2 + length (ci ly (start_of ly as) ins) div 2"

   743     proof -

   744       have "length (ci ly (start_of ly as) ins) div 2 = length_of ins"

   745         using ci_length by simp

   746       moreover have "start_of ly (Suc as) = start_of ly as + length_of ins"

   747         using fetch layout

   748         apply(simp add: start_of.simps abc_fetch.simps List.take_Suc_conv_app_nth 

   749           split: if_splits)

   750         apply(simp add: layout_of.simps)

   751         done

   752       ultimately show "?thesis"

   753         using b layout range1 range2

   754         apply(simp)

   755         done

   756     qed

   757   qed

   758   thus "?thesis"

   759     using b layout a compile  

   760     apply(simp add: tm_of.simps)

   761     done

   762 qed

   763 

   764 lemma step_eq_fetch: 

   765   assumes layout: "ly = layout_of ap"

   766   and compile: "tp = tm_of ap"

   767   and abc_fetch: "abc_fetch as ap = Some ins" 

   768   and fetch: "fetch (ci ly (start_of ly as) ins)

   769        (Suc s - start_of ly as) b = (ac, ns)"

   770   and notfinal: "ns \<noteq> 0"

   771   shows "fetch tp s b = (ac, ns)"

   772 proof -

   773   have "s \<ge> start_of ly as"

   774   proof(cases "s \<ge> start_of ly as")

   775     case True thus "?thesis" by simp

   776   next

   777     case False 

   778     have "\<not> start_of ly as \<le> s" by fact

   779     then have "Suc s - start_of ly as = 0"

   780       by arith

   781     then have "fetch (ci ly (start_of ly as) ins)

   782        (Suc s - start_of ly as) b = (Nop, 0)"

   783       by(simp add: fetch.simps)

   784     with notfinal fetch show "?thesis"

   785       by(simp)

   786   qed

   787   moreover have "s < start_of ly (Suc as)"

   788   proof(cases "s < start_of ly (Suc as)")

   789     case True thus "?thesis" by simp

   790   next

   791     case False

   792     have h: "\<not> s < start_of ly (Suc as)"

   793       by fact

   794     then have "s > start_of ly as"

   795       using abc_fetch layout

   796       apply(simp add: start_of.simps abc_fetch.simps split: if_splits)

   797       apply(simp add: List.take_Suc_conv_app_nth, auto)

   798       apply(subgoal_tac "layout_of ap ! as > 0") 

   799       apply arith

   800       apply(simp add: layout_of.simps)

   801       apply(case_tac "ap!as", auto simp: length_of.simps)

   802       done

   803     from this and h have "fetch (ci ly (start_of ly as) ins) (Suc s - start_of ly as) b = (Nop, 0)"

   804       using abc_fetch layout

   805       apply(case_tac b, simp_all add: Suc_diff_le)

   806       apply(case_tac [!] ins, simp_all add: start_of_Suc2 start_of_Suc1 start_of_Suc3)

   807       apply(simp_all only: length_ci_inc length_ci_dec length_ci_goto, auto)

   808       using layout

   809       apply(subgoal_tac [!] "start_of ly (Suc as) = start_of ly as + 2*nat1 + 16", simp_all)

   810       apply(rule_tac [!] start_of_Suc2, auto)

   811       done

   812     from fetch and notfinal this show "?thesis"by simp

   813   qed

   814   ultimately show "?thesis"

   815     using assms

   816     apply(drule_tac b= b and ins = ins in step_eq_fetch', auto)

   817     done

   818 qed

   819 

   820 

   821 lemma step_eq_in:

   822   assumes layout: "ly = layout_of ap"

   823   and compile: "tp = tm_of ap"

   824   and fetch: "abc_fetch as ap = Some ins"    

   825   and exec: "step (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) 

   826   = (s', l', r')"

   827   and notfinal: "s' \<noteq> 0"

   828   shows "step (s, l, r) (tp, 0) = (s', l', r')"

   829   using assms

   830   apply(simp add: step.simps)

   831   apply(case_tac "fetch (ci (layout_of ap) (start_of (layout_of ap) as) ins)

   832     (Suc s - start_of (layout_of ap) as) (read r)", simp)

   833   using layout

   834   apply(drule_tac s = s and b = "read r" and ac = a in step_eq_fetch, auto)

   835   done

   836 

   837 lemma steps_eq_in:

   838   assumes layout: "ly = layout_of ap"

   839   and compile: "tp = tm_of ap"

   840   and crsp: "crsp ly (as, lm) (s, l, r) ires"

   841   and fetch: "abc_fetch as ap = Some ins"    

   842   and exec: "steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp 

   843   = (s', l', r')"

   844   and notfinal: "s' \<noteq> 0"

   845   shows "steps (s, l, r) (tp, 0) stp = (s', l', r')"

   846   using exec notfinal

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

   848   fix stp s' l' r'

   849   assume ind: 

   850     "\<And>s' l' r'. \<lbrakk>steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp = (s', l', r'); s' \<noteq> 0\<rbrakk>

   851               \<Longrightarrow> steps (s, l, r) (tp, 0) stp = (s', l', r')"

   852   and h: "steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) (Suc stp) = (s', l', r')" "s' \<noteq> 0"

   853   obtain s1 l1 r1 where g: "steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp = 

   854                         (s1, l1, r1)"

   855     apply(case_tac "steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp") by blast

   856   moreover hence "s1 \<noteq> 0"

   857     using h

   858     apply(simp add: step_red)

   859     apply(case_tac "0 < s1", simp_all)

   860     done

   861   ultimately have "steps (s, l, r) (tp, 0) stp = (s1, l1, r1)"

   862     apply(rule_tac ind, auto)

   863     done

   864   thus "steps (s, l, r) (tp, 0) (Suc stp) = (s', l', r')"

   865     using h g assms

   866     apply(simp add: step_red)

   867     apply(rule_tac step_eq_in, auto)

   868     done

   869 qed

   870 

   871 lemma tm_append_fetch_first: 

   872   "\<lbrakk>fetch A s b = (ac, ns); ns \<noteq> 0\<rbrakk> \<Longrightarrow> 

   873     fetch (A @ B) s b = (ac, ns)"

   874 apply(case_tac b)

   875 apply(case_tac [!] s, auto simp: fetch.simps nth_append split: if_splits)

   876 done

   877 

   878 lemma tm_append_first_step_eq: 

   879   assumes "step (s, l, r) (A, off) = (s', l', r')"

   880   and "s' \<noteq> 0"

   881   shows "step (s, l, r) (A @ B, off) = (s', l', r')"

   882 using assms

   883 apply(simp add: step.simps)

   884 apply(case_tac "fetch A (s - off) (read r)")

   885 apply(frule_tac  B = B and b = "read r" in tm_append_fetch_first, auto)

   886 done

   887 

   888 lemma tm_append_first_steps_eq: 

   889   assumes "steps (s, l, r) (A, off) stp = (s', l', r')"

   890   and "s' \<noteq> 0"

   891   shows "steps (s, l, r) (A @ B, off) stp = (s', l', r')"

   892 using assms

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

   894   fix stp s' l' r'

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

   896     \<Longrightarrow> steps (s, l, r) (A @ B, off) stp = (s', l', r')"

   897     and h: "steps (s, l, r) (A, off) (Suc stp) = (s', l', r')" "s' \<noteq> 0"

   898   obtain sa la ra where a: "steps (s, l, r) (A, off) stp = (sa, la, ra)"

   899     apply(case_tac "steps (s, l, r) (A, off) stp") by blast

   900   hence "steps (s, l, r) (A @ B, off) stp = (sa, la, ra) \<and> sa \<noteq> 0"

   901     using h ind[of sa la ra]

   902     apply(case_tac sa, simp_all)

   903     done

   904   thus "steps (s, l, r) (A @ B, off) (Suc stp) = (s', l', r')"

   905     using h a

   906     apply(simp add: step_red)

   907     apply(rule_tac tm_append_first_step_eq, simp_all)

   908     done

   909 qed

   910 

   911 lemma tm_append_second_fetch_eq:

   912   assumes

   913   even: "length A mod 2 = 0"

   914   and off: "off = length A div 2"

   915   and fetch: "fetch B s b = (ac, ns)"

   916   and notfinal: "ns \<noteq> 0"

   917   shows "fetch (A @ shift B off) (s + off) b = (ac, ns + off)"

   918 using assms

   919 apply(case_tac b)

   920 apply(case_tac [!] s, auto simp: fetch.simps nth_append shift.simps 

   921   split: if_splits)

   922 done

   923 

   924 

   925 lemma tm_append_second_step_eq: 

   926   assumes 

   927   exec: "step0 (s, l, r) B = (s', l', r')"

   928   and notfinal: "s' \<noteq> 0"

   929   and off: "off = length A div 2"

   930   and even: "length A mod 2 = 0"

   931   shows "step0 (s + off, l, r) (A @ shift B off) = (s' + off, l', r')"

   932 using assms

   933 apply(simp add: step.simps)

   934 apply(case_tac "fetch B s (read r)")

   935 apply(frule_tac tm_append_second_fetch_eq, simp_all, auto)

   936 done

   937 

   938 

   939 lemma tm_append_second_steps_eq: 

   940   assumes 

   941   exec: "steps (s, l, r) (B, 0) stp = (s', l', r')"

   942   and notfinal: "s' \<noteq> 0"

   943   and off: "off = length A div 2"

   944   and even: "length A mod 2 = 0"

   945   shows "steps (s + off, l, r) (A @ shift B off, 0) stp = (s' + off, l', r')"

   946 using exec notfinal

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

   948   case 0

   949   thus "steps0 (s + off, l, r) (A @ shift B off) 0 = (s' + off, l', r')"

   950     by(simp add: steps.simps)

   951 next

   952   case (Suc stp s' l' r')

   953   have ind: "\<And>s' l' r'. \<lbrakk>steps0 (s, l, r) B stp = (s', l', r'); s' \<noteq> 0\<rbrakk> \<Longrightarrow> 

   954     steps0 (s + off, l, r) (A @ shift B off) stp = (s' + off, l', r')"

   955     by fact

   956   have h: "steps0 (s, l, r) B (Suc stp) = (s', l', r')" by fact

   957   have k: "s' \<noteq> 0" by fact

   958   obtain s'' l'' r'' where a: "steps0 (s, l, r) B stp = (s'', l'', r'')"

   959     by (metis prod_cases3)

   960   then have b: "s'' \<noteq> 0"

   961     using h k

   962     by(rule_tac notI, auto simp: step_red)

   963   from a b have c: "steps0 (s + off, l, r) (A @ shift B off) stp = (s'' + off, l'', r'')"

   964     by(erule_tac ind, simp)

   965   from c b h a k assms show "?case"

   966     thm tm_append_second_step_eq

   967     apply(simp add: step_red) by(rule tm_append_second_step_eq, simp_all)

   968 qed

   969 

   970 lemma tm_append_second_fetch0_eq:

   971   assumes

   972   even: "length A mod 2 = 0"

   973   and off: "off = length A div 2"

   974   and fetch: "fetch B s b = (ac, 0)"

   975   and notfinal: "s \<noteq> 0"

   976   shows "fetch (A @ shift B off) (s + off) b = (ac, 0)"

   977 using assms

   978 apply(case_tac b)

   979 apply(case_tac [!] s, auto simp: fetch.simps nth_append shift.simps 

   980   split: if_splits)

   981 done

   982 

   983 lemma tm_append_second_halt_eq:

   984   assumes 

   985   exec: "steps (Suc 0, l, r) (B, 0) stp = (0, l', r')"

   986   and wf_B: "tm_wf (B, 0)"

   987   and off: "off = length A div 2"

   988   and even: "length A mod 2 = 0"

   989   shows "steps (Suc off, l, r) (A @ shift B off, 0) stp = (0, l', r')"

   990 proof -

   991   thm before_final

   992   have "\<exists>n. \<not> is_final (steps0 (1, l, r) B n) \<and> steps0 (1, l, r) B (Suc n) = (0, l', r')"

   993     using exec by(rule_tac before_final, simp)

   994  then obtain n where a: 

   995    "\<not> is_final (steps0 (1, l, r) B n) \<and> steps0 (1, l, r) B (Suc n) = (0, l', r')" ..

   996  obtain s'' l'' r'' where b: "steps0 (1, l, r) B n = (s'', l'', r'') \<and> s'' >0"

   997    using a

   998    by(case_tac "steps0 (1, l, r) B n", auto)

   999  have c: "steps (Suc 0 + off, l, r) (A @ shift B off, 0) n = (s'' + off, l'', r'')"

  1000    using a b assms

  1001    by(rule_tac tm_append_second_steps_eq, simp_all)

  1002  obtain ac where d: "fetch B s'' (read r'') = (ac, 0)"

  1003    using  b a

  1004    by(case_tac "fetch B s'' (read r'')", auto simp: step_red step.simps)

  1005  then have "fetch (A @ shift B off) (s'' + off) (read r'') = (ac, 0)"

  1006    using assms b

  1007    by(rule_tac tm_append_second_fetch0_eq, simp_all)

  1008  then have e: "steps (Suc 0 + off, l, r) (A @ shift B off, 0) (Suc n) = (0, l', r')"

  1009    using a b assms c d

  1010    by(simp add: step_red step.simps)

  1011  from a have "n < stp"

  1012    using exec

  1013  proof(cases "n < stp")

  1014    case  True thus "?thesis" by simp

  1015  next

  1016    case False

  1017    have "\<not> n < stp" by fact

  1018    then obtain d where  "n = stp + d"

  1019      by (metis add.comm_neutral less_imp_add_positive nat_neq_iff)

  1020    thus "?thesis"

  1021      using a e exec

  1022      by(simp add: steps_add)

  1023  qed

  1024  then obtain d where "stp = Suc n + d"

  1025    by(metis add_Suc less_iff_Suc_add)

  1026  thus "?thesis"

  1027    using e

  1028    by(simp only: steps_add, simp)

  1029 qed

  1030 

  1031 lemma tm_append_steps: 

  1032   assumes 

  1033   aexec: "steps (s, l, r) (A, 0) stpa = (Suc (length A div 2), la, ra)"

  1034   and bexec: "steps (Suc 0, la, ra) (B, 0) stpb =  (sb, lb, rb)"

  1035   and notfinal: "sb \<noteq> 0"

  1036   and off: "off = length A div 2"

  1037   and even: "length A mod 2 = 0"

  1038   shows "steps (s, l, r) (A @ shift B off, 0) (stpa + stpb) = (sb + off, lb, rb)"

  1039 proof -

  1040   have "steps (s, l, r) (A@shift B off, 0) stpa = (Suc (length A div 2), la, ra)"

  1041     apply(rule_tac tm_append_first_steps_eq)

  1042     apply(auto simp: assms)

  1043     done

  1044   moreover have "steps (1 + off, la, ra) (A @ shift B off, 0) stpb = (sb + off, lb, rb)"

  1045     apply(rule_tac tm_append_second_steps_eq)

  1046     apply(auto simp: assms bexec)

  1047     done

  1048   ultimately show "steps (s, l, r) (A @ shift B off, 0) (stpa + stpb) = (sb + off, lb, rb)"

  1049     apply(simp add: steps_add off)

  1050     done

  1051 qed

  1052        

  1053 subsection {* Crsp of Inc*}

  1054 

  1055 fun at_begin_fst_bwtn :: "inc_inv_t"

  1056   where

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

  1058       (\<exists> lm1 tn rn. lm1 = (lm @ 0\<up>tn) \<and> length lm1 = s \<and> 

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

  1060            else l = [Bk]@<rev lm1>@Bk#Bk#ires) \<and> r = Bk\<up>rn)" 

  1061 

  1062 

  1063 fun at_begin_fst_awtn :: "inc_inv_t"

  1064   where

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

  1066       (\<exists> lm1 tn rn. lm1 = (lm @ 0\<up>tn) \<and> length lm1 = s \<and>

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

  1068           else l = [Bk]@<rev lm1>@Bk#Bk#ires) \<and> r = [Oc]@Bk\<up>rn)"

  1069 

  1070 fun at_begin_norm :: "inc_inv_t"

  1071   where

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

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

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

  1075          else l = Bk # <rev lm1> @ Bk # Bk # ires ) \<and> r = <lm2>@Bk\<up>rn)"

  1076 

  1077 fun in_middle :: "inc_inv_t"

  1078   where

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

  1080       (\<exists> lm1 lm2 tn m ml mr rn. lm @ 0\<up>tn = lm1 @ [m] @ lm2

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

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

  1083        (if lm1 = [] then l = Oc\<up>ml @ Bk # Bk # ires 

  1084         else l = Oc\<up>ml@[Bk]@<rev lm1>@

  1085                  Bk # Bk # ires) \<and> (r = Oc\<up>mr @ [Bk] @ <lm2>@ Bk\<up>rn \<or> 

  1086       (lm2 = [] \<and> r = Oc\<up>mr))

  1087       )"

  1088 

  1089 fun inv_locate_a :: "inc_inv_t"

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

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

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

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

  1094       )"

  1095 

  1096 fun inv_locate_b :: "inc_inv_t"

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

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

  1099 

  1100 fun inv_after_write :: "inc_inv_t"

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

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

  1103              (if lm1 = [] then l = Oc\<up>m @ Bk # Bk # ires

  1104               else Oc # l = Oc\<up>Suc m@ Bk # <rev lm1> @ 

  1105                       Bk # Bk # ires) \<and> r = [Oc] @ <lm2> @ Bk\<up>rn)"

  1106 

  1107 fun inv_after_move :: "inc_inv_t"

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

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

  1110         (if lm1 = [] then l = Oc\<up>Suc m @ Bk # Bk # ires

  1111          else l = Oc\<up>Suc m@ Bk # <rev lm1> @ Bk # Bk # ires) \<and> 

  1112         r = <lm2> @ Bk\<up>rn)"

  1113 

  1114 fun inv_after_clear :: "inc_inv_t"

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

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

  1117         (if lm1 = [] then l = Oc\<up>Suc m @ Bk # Bk # ires

  1118          else l = Oc\<up>Suc m @ Bk # <rev lm1> @ Bk # Bk # ires) \<and> 

  1119           r = Bk # r' \<and> Oc # r' = <lm2> @ Bk\<up>rn)"

  1120 

  1121 fun inv_on_right_moving :: "inc_inv_t"

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

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

  1124             ml + mr = m \<and> 

  1125           (if lm1 = [] then l = Oc\<up>ml @ Bk # Bk # ires

  1126           else l = Oc\<up>ml  @ [Bk] @ <rev lm1> @ Bk # Bk # ires) \<and> 

  1127          ((r = Oc\<up>mr @ [Bk] @ <lm2> @ Bk\<up>rn) \<or> 

  1128           (r = Oc\<up>mr \<and> lm2 = [])))"

  1129 

  1130 fun inv_on_left_moving_norm :: "inc_inv_t"

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

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

  1133              ml + mr = Suc m \<and> mr > 0 \<and> (if lm1 = [] then l = Oc\<up>ml @ Bk # Bk # ires

  1134                                          else l =  Oc\<up>ml @ Bk # <rev lm1> @ Bk # Bk # ires)