Theory Abacus_alt_Compile

(* Title: thys/Abacus_alt_Compile.thy
   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
   Modifications: Sebastiaan Joosten
 *)

subsection ‹Alternative Definitions for Translating Abacus Machines to TMs›

theory Abacus_alt_Compile
  imports Abacus
begin

abbreviation
  "layout ≡ layout_of"


fun address :: "abc_prog ⇒ nat ⇒ nat"
  where
    "address p x = (Suc (sum_list (take x (layout p)))) "

abbreviation
  "TMGoto ≡ [(Nop, 1), (Nop, 1)]"

abbreviation 
  "TMInc ≡ [(WO, 1), (R, 2), (WO, 3), (R, 2), (WO, 3), (R, 4), 
            (L, 7), (WB, 5), (R, 6), (WB, 5), (WO, 3), (R, 6),
            (L, 8), (L, 7), (R, 9), (L, 7), (R, 10), (WB, 9)]"

abbreviation
  "TMDec ≡ [(WO, 1), (R, 2), (L, 14), (R, 3), (L, 4), (R, 3),
             (R, 5), (WB, 4), (R, 6), (WB, 5), (L, 7), (L, 8),
             (L, 11), (WB, 7), (WO, 8), (R, 9), (L, 10), (R, 9),
             (R, 5), (WB, 10), (L, 12), (L, 11), (R, 13), (L, 11),
             (R, 17), (WB, 13), (L, 15), (L, 14), (R, 16), (L, 14),
             (R, 0), (WB, 16)]"

abbreviation
  "TMFindnth ≡ findnth"

fun compile_goto :: "nat ⇒ instr list" 
  where
    "compile_goto s = shift TMGoto (s - 1)"

fun compile_inc :: "nat ⇒ nat ⇒ instr list"
  where
    "compile_inc s n = (shift (TMFindnth n) (s - 1)) @ (shift (shift TMInc (2 * n)) (s - 1))"

fun compile_dec :: "nat ⇒ nat ⇒ nat ⇒ instr list"
  where
    "compile_dec s n e = (shift (TMFindnth n) (s - 1)) @ (adjust (shift (shift TMDec (2 * n)) (s - 1)) e)"

fun compile :: "abc_prog ⇒ nat ⇒ abc_inst ⇒ instr list"
  where
    "compile ap s (Inc n) = compile_inc s n"
  | "compile ap s (Dec n e) = compile_dec s n (address ap e)"
  | "compile ap s (Goto e) = compile_goto (address ap e)"

lemma
  "compile ap s i = ci (layout ap) s i"
  apply(cases i)
    apply(simp add: ci.simps shift.simps start_of.simps tinc_b_def)
   apply(simp add: ci.simps shift.simps start_of.simps tdec_b_def)
  apply(simp add: ci.simps shift.simps start_of.simps)
  done


end