header {* 

*}

theory abacus

imports Main turing_basic

begin

text {*

  {\em Abacus} instructions:

*}

datatype abc_inst =

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

     *}

     Inc nat

  -- {*

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

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

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

     *}

   | Dec nat nat

  -- {*

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

  *}

   | Goto nat

text {*

  Abacus programs are defined as lists of Abacus instructions.

*}

type_synonym abc_prog = "abc_inst list"

section {*

  Sample Abacus programs

  *}

text {*

  Abacus for addition and clearance.

*}

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

  where

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

text {*

  Abacus for clearing memory untis.

*}

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

  where

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

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

  where

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

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

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

  where

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

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

  where

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

text {*

  The state of Abacus machine.

  *}

type_synonym abc_state = nat

(* text {*

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

*}

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

text {*

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

  every units addressed by index into the list.

  *}

type_synonym abc_lm = "nat list"

text {*

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

  as having content @{text "0"}.

*}

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

  where 

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

(*

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

  where 

    "abc_l2m lm = abc_lm_v lm"

*)

text {*

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

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

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

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

*}

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

  where

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

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

text {*

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

  current memory:

*}

type_synonym abc_conf_l = "abc_state \<times> abc_lm"

text {*

  Fetch instruction out of Abacus program:

*}

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

  where

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

                    else None)"

text {*

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

  configuration does not change.

*}

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

  where

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

               None \<Rightarrow> (s, lm) |

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

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

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

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

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

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

               )"

text {*

  Multi-step execution of Abacus machine.

*}

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

  where

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

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

section {*

  Compiling Abacus machines into Truing machines

*}

subsection {*

  Compiling functions

*}

text {*

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

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

  on the way.

*}

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

  where

  "findnth 0 = []" |

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

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

text {*

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

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

  of cells afterwards to the right accordingly.

  *}

definition tinc_b :: "tprog"

  where

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

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

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

text {*

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

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

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

  *}

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

  where

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

       (action, (if state = 0 then 0

                 else state + off))) tp)"

text {*

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

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

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

  Abacus program.

*}

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

  where

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

text {*

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

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

  of cells afterwards to the left accordingly.

  *}

definition tdec_b :: "tprog"

  where

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

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

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

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

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

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

text {*

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

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

  *}

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

  where

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

text {*

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

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

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

  Abacus program.

*}

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

  where

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

                 (ss - 1)) e"

text {*

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

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

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

*}

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

  where

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

text {*

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

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

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

  in the Abacus program.

*}

type_synonym layout = "nat list"

text {*

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

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

*}

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

  where

  "length_of i = (case i of 

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

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

                    Goto n  \<Rightarrow> 1)"

text {*

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

*}

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

  where "layout_of ap = map length_of ap"

text {*

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

  TM in the finall TM.

*}

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

  where

  "start_of ly 0 = Suc 0" |

  "start_of ly (Suc as) = 

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

         else start_of ly as)"

text {*

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

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

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

*}

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

  where

  "ci ly ss i = (case i of 

                    Inc n   \<Rightarrow> tinc ss n |

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

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

text {*

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

  every instruction with its starting state.

*}

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

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

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

text {*

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

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

*}

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

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

                         (tpairs_of ap)"

text {*

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

*}

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

  where "tm_of ap = concat (tms_of ap)"

text {*

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

*}

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

  where

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

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

  where 

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

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

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

apply(induct n, simp, simp)

done

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

apply(auto simp: ci.simps tinc_b_def tdec_b_def findnth_length

                 split: abc_inst.splits)

done

subsection {*

  Representation of Abacus memory by TM tape

*}

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

text {*

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

  Abacus memory @{text "am"}.

  *}

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

  where 

  "tape_of_nat_list [] = []" |

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

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

defs (overloaded)

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

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

text {*

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

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

*}

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

  where 

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

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

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

declare crsp_l.simps[simp del]

subsection {*

  A more general definition of TM execution. 

*}

(*

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

  where

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

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

thm nth_of.simps

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

  where

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

  "nfetch p (Suc s) b = 

             (case b of 

                Bk \<Rightarrow> nnth_of p s 0 |

                Oc \<Rightarrow> nnth_of p s 1)"

*)

text {*

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

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

*}

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

  where 

  "t_step c (p, off) = 

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

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

                             (case rightn of 

                                [] \<Rightarrow> Bk | 

                                Bk # xs \<Rightarrow> Bk |

                                Oc # xs \<Rightarrow> Oc

                             ) 

             in 

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

text {*

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

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

*}

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

  where

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

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

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

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

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

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

apply(simp add: t_steps.simps)

done

text {*

  The type of invarints expressing correspondence between 

  Abacus configuration and TM configuration.

*}

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

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

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

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

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

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

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

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

        abc2t_correct.simps[simp del]

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

apply(simp add: t_ncorrect.simps)

done

lemma t_shift_fetch: 

    "\<lbrakk>t_ncorrect tp1; t_ncorrect tp; 

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

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

         fetch (tp1 @ tp @ tp2) a b"

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

apply(case_tac x, simp)

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

             Suc (length tp1 div 2 + nat)")

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

apply(case_tac b, simp)

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

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

apply(simp add: t_ncorrect.simps, auto)

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

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

apply(simp add: t_ncorrect.simps, auto)

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

done

lemma t_shift_in_step:

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

        t_ncorrect tp1; t_ncorrect tp;

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

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

apply(simp add: t_step.simps)

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

                   Bk | x # xs \<Rightarrow> x)

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

                   \<Rightarrow> x)")

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

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

apply(auto intro: t_shift_fetch)

apply(case_tac ba, simp, simp)

apply(case_tac aaa, simp, simp)

done

declare add_Suc_right[simp del]

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

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

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

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

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

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

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

                         (p, off) n")

apply(simp, simp add: stepn)

apply(simp only: t_steps.simps)

apply(simp only: add_Suc_right)

done

declare add_Suc_right[simp]

lemma s_out_fetch: "\<lbrakk>t_ncorrect tp; 

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

         length tp div 2)\<rbrakk>

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

apply(auto)

apply(simp add: fetch.simps)

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

apply(erule exE, simp)

apply(case_tac x, simp)

apply(auto simp add: fetch.simps)

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

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

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

     , simp)

done 

lemma conf_keep_step: 

      "\<lbrakk>t_ncorrect tp; 

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

       length tp div 2)\<rbrakk>