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 text {*

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

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

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

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

    96 *}

    97 

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

    99   where

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

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

   102 

   103 

   104 text {*

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

   106   current memory:

   107 *}

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

   109 

   110 text {*

   111   Fetch instruction out of Abacus program:

   112 *}

   113 

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

   115   where

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

   117                     else None)"

   118 

   119 text {*

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

   121   configuration does not change.

   122 *}

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

   124   where

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

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

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

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

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

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

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

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

   133                )"

   134 

   135 text {*

   136   Multi-step execution of Abacus machine.

   137 *}

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

   139   where

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

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

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

   143 

   144 section {*

   145   Compiling Abacus machines into Truing machines

   146 *}

   147 

   148 subsection {*

   149   Compiling functions

   150 *}

   151 

   152 text {*

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

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

   155   on the way.

   156 *}

   157 

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

   159   where

   160   "findnth 0 = []" |

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

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

   163 

   164 text {*

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

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

   167   of cells afterwards to the right accordingly.

   168   *}

   169 

   170 definition tinc_b :: "instr list"

   171   where

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

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

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

   175 

   176 text {*

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

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

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

   180   Abacus program.

   181 *}

   182 

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

   184   where

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

   186 

   187 text {*

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

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

   190   of cells afterwards to the left accordingly.

   191   *}

   192 

   193 definition tdec_b :: "instr list"

   194   where

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

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

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

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

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

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

   201 

   202 text {*

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

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

   205   *}

   206 

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

   208   where

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

   210 

   211 text {*

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

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

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

   215   Abacus program.

   216 *}

   217 

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

   219   where

   220   "tdec ss n e = sete (shift (findnth n @ shift tdec_b (2 * n)) 

   221                  (ss - 1)) e"

   222  

   223 text {*

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

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

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

   227 *}

   228 

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

   230   where

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

   232 

   233 text {*

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

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

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

   237   in the Abacus program.

   238 *}

   239 

   240 type_synonym layout = "nat list"

   241 

   242 text {*

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

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

   245 *}

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

   247   where

   248   "length_of i = (case i of 

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

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

   251                     Goto n  \<Rightarrow> 1)"

   252 

   253 text {*

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

   255 *}

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

   257   where "layout_of ap = map length_of ap"

   258 

   259 

   260 text {*

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

   262   TM in the finall TM.

   263 *}

   264 thm listsum_def

   265 

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

   267   where

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

   269 

   270 text {*

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

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

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

   274 *}

   275 

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

   277   where

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

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

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

   281 

   282 text {*

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

   284   every instruction with its starting state.

   285 *}

   286 

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

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

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

   290 

   291 text {*

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

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

   294 *}

   295 

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

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

   298                          (tpairs_of ap)"

   299 

   300 text {*

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

   302 *}

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

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

   305 

   306 text {*

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

   308 *}

   309 (*

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

   311   where

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

   313 

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

   315   where 

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

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

   318 *)

   319 

   320 lemma length_findnth: 

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

   322 apply(induct n, auto)

   323 done

   324 

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

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

   327                  split: abc_inst.splits)

   328 done

   329 

   330 subsection {*

   331   Representation of Abacus memory by TM tape

   332 *}

   333 

   334 text {*

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

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

   337 *}

   338 

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

   340   where 

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

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

   343             l = Bk # Bk # inres)"

   344 

   345 declare crsp.simps[simp del]

   346 

   347 subsection {*

   348   A more general definition of TM execution. 

   349 *}

   350 

   351                     

   352 text {*

   353   The type of invarints expressing correspondence between 

   354   Abacus configuration and TM configuration.

   355 *}

   356 

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

   358 

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

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

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

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

   363         layout_of.simps[simp del]

   364 

   365 

   366 (*

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

   368 *)

   369 

   370 text {*

   371   The lemmas in this section lead to the correctness of 

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

   373 *}

   374 

   375 

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

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

   378 apply(simp add: start_of.simps)

   379 done

   380 

   381 lemma abc_step_red: 

   382  "abc_steps_l ac aprog stp = (as, am) \<Longrightarrow> 

   383    abc_steps_l ac aprog (Suc stp) = abc_step_l (as, am) (abc_fetch as aprog) "

   384 sorry

   385 

   386 lemma tm_shift_fetch: 

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

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

   389 apply(case_tac b)

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

   391 done

   392 

   393 lemma tm_shift_eq_step:

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

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

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

   397 using assms

   398 apply(simp add: step.simps)

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

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

   401 done

   402 

   403 lemma tm_shift_eq_steps: 

   404   assumes layout: "ly = layout_of ap"

   405   and compile: "tp = tm_of ap"

   406   and exec: "steps (s, l, r) (A, 0) stp = (s', l', r')"

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

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

   409   using exec notfinal

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

   411   fix stp s' l' r'

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

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

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

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

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

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

   418     using h

   419     apply(simp add: step_red, case_tac "0 < s1", simp, simp)

   420     done

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

   422                    (s1 + off, l1, r1)"

   423     apply(rule_tac ind, simp_all)

   424     done

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

   426     using h g assms

   427     apply(simp add: step_red)

   428     apply(rule_tac tm_shift_eq_step, auto)

   429     done

   430 qed

   431 

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

   433 apply(simp add: start_of.simps)

   434 done

   435 

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

   437 apply(simp add: start_of.simps)

   438 done

   439 

   440 lemma step_eq_fetch: 

   441   assumes layout: "ly = layout_of ap"

   442   and compile: "tp = tm_of ap"

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

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

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

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

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

   448 proof -

   449   have "s > start_of ly as \<and> s < start_of ly (Suc as)"

   450     sorry

   451   thus "fetch tp s b = (ac, ns)"

   452     sorry

   453 qed

   454   

   455 lemma step_eq_in:

   456   assumes layout: "ly = layout_of ap"

   457   and compile: "tp = tm_of ap"

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

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

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

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

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

   463   using assms

   464   apply(simp add: step.simps)

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

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

   467   using layout

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

   469   done

   470 

   471 lemma steps_eq_in:

   472   assumes layout: "ly = layout_of ap"

   473   and compile: "tp = tm_of ap"

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

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

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

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

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

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

   480   using exec notfinal

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

   482   fix stp s' l' r'

   483   assume ind: 

   484     "\<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>

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

   486   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"

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

   488                         (s1, l1, r1)"

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

   490   moreover hence "s1 \<noteq> 0"

   491     using h

   492     apply(simp add: step_red)

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

   494     done

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

   496     apply(rule_tac ind, auto)

   497     done

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

   499     using h g assms

   500     apply(simp add: step_red)

   501     apply(rule_tac step_eq_in, auto)

   502     done

   503 qed

   504 

   505 lemma tm_append_fetch_first: 

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

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

   508 apply(case_tac b)

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

   510 done

   511 

   512 lemma tm_append_first_step_eq: 

   513   assumes "step (s, l, r) (A, 0) = (s', l', r')"

   514   and "s' \<noteq> 0"

   515   shows "step (s, l, r) (A @ B, 0) = (s', l', r')"

   516 using assms

   517 apply(simp add: step.simps)

   518 apply(case_tac "fetch A s (read r)")

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

   520 done

   521 

   522 lemma tm_append_first_steps_eq: 

   523   assumes "steps (s, l, r) (A, 0) stp = (s', l', r')"

   524   and "s' \<noteq> 0"

   525   shows "steps (s, l, r) (A @ B, 0) stp = (s', l', r')"

   526 using assms

   527 sorry

   528 

   529 lemma tm_append_second_steps_eq: 

   530   assumes 

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

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

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

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

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

   536 using assms

   537 sorry

   538 

   539 lemma tm_append_steps: 

   540   assumes 

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

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

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

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

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

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

   547 proof -

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

   549     apply(rule_tac tm_append_first_steps_eq)

   550     apply(auto simp: assms)

   551     done

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

   553     apply(rule_tac tm_append_second_steps_eq)

   554     apply(auto simp: assms bexec)

   555     done

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

   557     apply(simp add: steps_add off)

   558     done

   559 qed

   560        

   561 subsection {* Crsp of Inc*}

   562 

   563 lemma crsp_step_inc:

   564   assumes layout: "ly = layout_of ap"

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

   566   and fetch: "abc_fetch as ap = Some (Inc n)"

   567   shows "\<exists>stp. crsp ly (abc_step_l (as, lm) (Some (Inc n)))

   568   (steps (s, l, r) (ci ly (start_of ly as) (Inc n), start_of ly as - Suc 0) stp) ires"

   569   sorry

   570     

   571 subsection{* Crsp of Dec n e*}

   572 lemma crsp_step_dec: 

   573   assumes layout: "ly = layout_of ap"

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

   575   shows "\<exists>stp. crsp ly (abc_step_l (as, lm) (Some (Dec n e)))

   576   (steps (s, l, r) (ci ly (start_of ly as) (Dec n e), start_of ly as - Suc 0) stp) ires"

   577 sorry

   578 

   579 subsection{*Crsp of Goto*}

   580 lemma crsp_step_goto:

   581   assumes layout: "ly = layout_of ap"

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

   583   shows "\<exists>stp. crsp ly (abc_step_l (as, lm) (Some (Goto n)))

   584   (steps (s, l, r) (ci ly (start_of ly as) (Goto n), 

   585             start_of ly as - Suc 0) stp) ires"

   586 sorry

   587 

   588 

   589 lemma crsp_step_in:

   590   assumes layout: "ly = layout_of ap"

   591   and compile: "tp = tm_of ap"

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

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

   594   shows "\<exists> stp. crsp ly (abc_step_l (as, lm) (Some ins))

   595                       (steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp) ires"

   596   using assms

   597   apply(case_tac ins, simp_all)

   598   apply(rule crsp_step_inc, simp_all)

   599   apply(rule crsp_step_dec, simp_all)

   600   apply(rule_tac crsp_step_goto, simp_all)

   601   done

   602 

   603 lemma crsp_step:

   604   assumes layout: "ly = layout_of ap"

   605   and compile: "tp = tm_of ap"

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

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

   608   shows "\<exists> stp. crsp ly (abc_step_l (as, lm) (Some ins))

   609                       (steps (s, l, r) (tp, 0) stp) ires"

   610 proof -

   611   have "\<exists> stp. crsp ly (abc_step_l (as, lm) (Some ins))

   612                       (steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp) ires"

   613     using assms

   614     apply(erule_tac crsp_step_in, simp_all)

   615     done

   616   from this obtain stp where d: "crsp ly (abc_step_l (as, lm) (Some ins))

   617                       (steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp) ires" ..

   618   obtain s' l' r' where e:

   619     "(steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp) = (s', l', r')"

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

   621     by blast

   622   then have "steps (s, l, r) (tp, 0) stp = (s', l', r')"

   623     using assms d

   624     apply(rule_tac steps_eq_in)

   625     apply(simp_all)

   626     apply(case_tac "(abc_step_l (as, lm) (Some ins))", simp add: crsp.simps)

   627     done    

   628   thus " \<exists>stp. crsp ly (abc_step_l (as, lm) (Some ins)) (steps (s, l, r) (tp, 0) stp) ires"

   629     using d e

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

   631     done

   632 qed

   633 

   634 lemma crsp_steps:

   635   assumes layout: "ly = layout_of ap"

   636   and compile: "tp = tm_of ap"

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

   638   shows "\<exists> stp. crsp ly (abc_steps_l (as, lm) ap n)

   639                       (steps (s, l, r) (tp, 0) stp) ires"

   640   using crsp

   641   apply(induct n)

   642   apply(rule_tac x = 0 in exI) 

   643   apply(simp add: steps.simps abc_steps_l.simps, simp)

   644   apply(case_tac "(abc_steps_l (as, lm) ap n)", auto)

   645   apply(frule_tac abc_step_red, simp)

   646   apply(case_tac "abc_fetch a ap", simp add: abc_step_l.simps, auto)

   647   apply(case_tac "steps (s, l, r) (tp, 0) stp", simp)

   648   using assms

   649   apply(drule_tac s = ab and l = ba and r = c in crsp_step, auto)

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

   651   done

   652 

   653 lemma tp_correct': 

   654   assumes layout: "ly = layout_of ap"

   655   and compile: "tp = tm_of ap"

   656   and crsp: "crsp ly (0, lm) (Suc 0, l, r) ires"

   657   and abc_halt: "abc_steps_l (0, lm) ap stp = (length ap, am)"

   658   shows "\<exists> stp k. steps (Suc 0, l, r) (tp, 0) stp = (start_of ly (length ap), Bk # Bk # ires, <am> @ Bk\<up>k)"

   659   using assms

   660   apply(drule_tac n = stp in crsp_steps, auto)

   661   apply(rule_tac x = stpa in exI)

   662   apply(case_tac "steps (Suc 0, l, r) (tm_of ap, 0) stpa", simp add: crsp.simps)

   663   done

   664 

   665 (***normalize the tp compiled from ap, and we can use Hoare_plus when composed with mopup machine*)

   666 definition tp_norm :: "abc_prog \<Rightarrow> instr list"

   667   where

   668   "tp_norm ap = tm_of ap @ [(Nop, 0), (Nop, 0)]"

   669 

   670 lemma tp_correct: 

   671   assumes layout: "ly = layout_of ap"

   672   and crsp: "crsp ly (0, lm) (Suc 0, l, r) ires"

   673   and abc_halt: "abc_steps_l (0, lm) ap stp = (length ap, am)"

   674   shows "\<exists> stp k. steps (Suc 0, l, r) (tp_norm ap, 0) stp = (0, Bk # Bk # ires, <am> @ Bk\<up>k)"

   675  sorry

   676 

   677 (****mop_up***)

   678 fun mopup_a :: "nat \<Rightarrow> instr list"

   679   where

   680   "mopup_a 0 = []" |

   681   "mopup_a (Suc n) = mopup_a n @ 

   682        [(R, 2*n + 3), (W0, 2*n + 2), (R, 2*n + 1), (W1, 2*n + 2)]"

   683 

   684 definition mopup_b :: "instr list"

   685   where

   686   "mopup_b \<equiv> [(R, 2), (R, 1), (L, 5), (W0, 3), (R, 4), (W0, 3),

   687             (R, 2), (W0, 3), (L, 5), (L, 6), (R, 0), (L, 6)]"

   688 

   689 fun mopup :: "nat \<Rightarrow> instr list"

   690   where 

   691   "mopup n = mopup_a n @ shift mopup_b (2*n)"

   692 (****)

   693 

   694 (*we can use Hoare_plus here*)

   695 lemma compile_correct_halt: 

   696   assumes layout: "ly = layout_of ap"

   697   and crsp: "crsp ly (0, lm) (Suc 0, l, r) ires"

   698   and abc_halt: "abc_steps_l (0, lm) ap stp = (length ap, am)"

   699   and rs_loc: "n < length am"

   700   and rs: "rs = abc_lm_v am n"

   701   shows "\<exists> stp i j. steps (Suc 0, l, r) (tp_norm ap |+| mopup n, 0) stp = (0, Bk\<up>i @ Bk # Bk # ires, Oc\<up>Suc rs @ Bk\<up>j)"

   702 sorry

   703 

   704 lemma compile_correct_unhalt: 

   705   assumes layout: "ly = layout_of ap"

   706   and crsp: "crsp ly (0, lm) (Suc 0, l, r) ires"

   707   and abc_unhalt: "\<forall> stp. (\<lambda> (as, am). as < length ap) (abc_steps_l (0, lm) ap stp)"

   708   shows "\<forall> stp.\<not> is_final (steps (Suc 0, l, r) (tp_norm ap |+| mopup n, 0) stp)"

   709 sorry

   710 

   711 end

   712