(* Title: thys/Abacus.thy

   Author: Jian Xu, Xingyuan Zhang, and Christian Urban

*)

chapter {* Abacus Machines *}

theory Abacus

imports Turing_Hoare Abacus_Mopup

begin

declare replicate_Suc[simp add]

(* Abacus instructions *)

datatype abc_inst =

     Inc nat

   | Dec nat nat

   | Goto nat

type_synonym abc_prog = "abc_inst list"

type_synonym abc_state = 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)"         

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 = "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 \<Rightarrow> abc_inst option \<Rightarrow> abc_conf"

  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 \<Rightarrow> abc_prog \<Rightarrow> nat \<Rightarrow> abc_conf"

  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> instr list"

  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 :: "instr list"

  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 "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> instr list"

  where

  "tinc ss n = shift (findnth n @ shift 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 :: "instr list"

  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 "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> instr list"

  where

  "tdec ss n e = shift (findnth n) (ss - 1) @ adjust (shift (shift 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> instr list"

  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 x = (Suc (sum_list (take x ly))) "

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> instr list"

  where

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

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

| "ci ly ss (Goto n) = 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> (instr list) 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> instr list"

  where "tm_of ap = concat (tms_of ap)"

lemma length_findnth: 

  "length (findnth n) = 4 * n"

by (induct n, auto)

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

apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth

                 split: abc_inst.splits simp del: adjust.simps)

done

subsection {* Representation of Abacus memory by TM tapes *}

text {*

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

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

*}

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

  where 

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

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

            l = Bk # Bk # inres)"

declare crsp.simps[simp del]

text {*

  The type of invarints expressing correspondence between 

  Abacus configuration and TM configuration.

*}

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

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

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

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

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

        layout_of.simps[simp del]

text {*

  The lemmas in this section lead to the correctness of 

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

*}

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

lemma start_of_nonzero[simp]: "start_of ly as > 0" "(start_of ly as = 0) = False"

apply(auto simp: start_of.simps)

done

lemma abc_steps_l_0: "abc_steps_l ac ap 0 = ac"

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

lemma abc_step_red: 

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

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

proof(induct stp arbitrary: as am bs bm)

  case 0

  thus "?case"

    by(simp add: abc_steps_l.simps abc_steps_l_0)

next

  case (Suc stp as am bs bm)

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

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

    by fact

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

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

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

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

    using h

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

  thus "?case"

    using g

    by(simp add: abc_steps_l.simps)

qed

lemma tm_shift_fetch: 

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

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

apply(case_tac b)

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

done

lemma tm_shift_eq_step:

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

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

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

using assms

apply(simp add: step.simps)

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

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

done

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

lemma tm_shift_eq_steps: 

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

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

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

  using exec notfinal

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

  fix stp s' l' r'

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

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

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

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

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

  moreover then have "s1 \<noteq> 0"

    using h

    apply(simp add: step_red)

    apply(case_tac "0 < s1", auto)

    done

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

                   (s1 + off, l1, r1)"

    apply(rule_tac ind, simp_all)

    done

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

    using h g assms

    apply(simp add: step_red)

    apply(rule_tac tm_shift_eq_step, auto)

    done

qed

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

apply(simp add: start_of.simps)

done

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

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

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

apply(auto simp: start_of.simps layout_of.simps  

                 length_of.simps abc_fetch.simps 

                 take_Suc_conv_app_nth split: if_splits)

done

lemma start_of_Suc2:

  "\<lbrakk>ly = layout_of ap;

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

        start_of ly (Suc as) = 

            start_of ly as + 2 * n + 16"

apply(auto simp: start_of.simps layout_of.simps  

                 length_of.simps abc_fetch.simps 

                 take_Suc_conv_app_nth split: if_splits)

done

lemma start_of_Suc3:

  "\<lbrakk>ly = layout_of ap;

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

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

apply(auto simp: start_of.simps layout_of.simps  

                 length_of.simps abc_fetch.simps 

                 take_Suc_conv_app_nth split: if_splits)

done

lemma length_ci_inc: 

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

apply(auto simp: ci.simps length_findnth tinc_b_def)

done

lemma length_ci_dec: 

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

apply(auto simp: ci.simps length_findnth tdec_b_def)

done

lemma length_ci_goto: 

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

apply(auto simp: ci.simps length_findnth tdec_b_def)

done

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

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

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

apply(case_tac as, simp, simp)

done

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

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

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

by auto

lemma concat_drop_suc_iff: 

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

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

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

apply(case_tac tps, simp, simp)

apply(case_tac n, simp, simp)

done

declare append_assoc[simp del]

lemma  tm_append:

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

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

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

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

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

apply(auto)

apply(induct n, simp)

apply(case_tac tps, simp, simp, simp)

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

               concat (take (Suc n) tps)")

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

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

                  concat (drop (Suc (Suc n)) tps)")

  apply (metis append_take_drop_id concat_append)

   apply(rule concat_drop_suc_iff,force)

  by (simp add: concat_suc)

declare append_assoc[simp]

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

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

done

lemma ci_nth: 

  "\<lbrakk>ly = layout_of aprog; 

  abc_fetch as aprog = Some ins\<rbrakk>

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

apply(simp add: tms_of.simps tpairs_of.simps 

done

lemma t_split:"\<lbrakk>

        ly = layout_of aprog;

        abc_fetch as aprog = Some ins\<rbrakk>

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

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

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

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

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

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

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

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

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

apply(rule_tac ci_nth, auto)

done

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

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

  by(auto)

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

by(auto simp: layout_of.simps)

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

  apply(cases "ap ! n")

  by (auto simp: tms_of.simps tpairs_of.simps ci.simps length_findnth tinc_b_def tdec_b_def)

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

proof(induct n)

  case 0

  then show ?case by (auto simp add: take_Suc_conv_app_nth)

next

  case (Suc n)

  hence "n < length (tms_of ap) \<Longrightarrow> is_even (length (concat (take (Suc n) (tms_of ap))))"

    unfolding take_Suc_conv_app_nth by fastforce

  with Suc show ?case by(cases "n < length (tms_of ap)", auto)

qed

lemma tpa_states:

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

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

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

proof(induct as arbitrary: tp)

  case 0

  thus "?case"

    by(simp add: start_of.simps)

next

  case (Suc as tp)

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

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