1 (* Title: thys/Abacus.thy

     2    Author: Jian Xu, Xingyuan Zhang, and Christian Urban

     3 *)

     4 

     5 header {* Alternative Definitions for Translating Abacus Machines to TMs *}

     6 

     7 theory Abacus_Defs

     8 imports Abacus

     9 begin

    10 

    11 abbreviation

    12   "layout \<equiv> layout_of"

    13 

    14 fun address :: "abc_prog \<Rightarrow> nat \<Rightarrow> nat"

    15   where

    16   "address p x = (Suc (listsum (take x (layout p)))) "

    17 

    18 abbreviation

    19   "TMGoto \<equiv> [(Nop, 1), (Nop, 1)]"

    20 

    21 abbreviation 

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

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

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

    25 

    26 abbreviation

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

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

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

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

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

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

    33 

    34 abbreviation

    35   "TMFindnth \<equiv> findnth"

    36 

    37 fun compile_goto :: "nat \<Rightarrow> instr list" 

    38   where

    39   "compile_goto s = shift TMGoto (s - 1)"

    40 

    41 fun compile_inc :: "nat \<Rightarrow> nat \<Rightarrow> instr list"

    42   where

    43   "compile_inc s n = (shift (TMFindnth n) (s - 1)) @ (shift (shift TMInc (2 * n)) (s - 1))"

    44 

    45 fun compile_dec :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> instr list"

    46   where

    47   "compile_dec s n e = (shift (TMFindnth n) (s - 1)) @ (adjust (shift (shift TMDec (2 * n)) (s - 1)) e)"

    48 

    49 fun compile :: "abc_prog \<Rightarrow> nat \<Rightarrow> abc_inst \<Rightarrow> instr list"

    50   where

    51   "compile ap s (Inc n) = compile_inc s n"

    52 | "compile ap s (Dec n e) = compile_dec s n (address ap e)"

    53 | "compile ap s (Goto e) = compile_goto (address ap e)"

    54 

    55 lemma

    56   "compile ap s i = ci (layout ap) s i"

    57 apply(cases i)

    58 apply(simp add: ci.simps shift.simps start_of.simps tinc_b_def)

    59 apply(simp add: ci.simps shift.simps start_of.simps tdec_b_def)

    60 apply(simp add: ci.simps shift.simps start_of.simps)

    61 done

    62 

    63 

    64 end