theory Abacusimports Mainbegin datatype abc_inst = Inc nat | Dec nat nat | Goto nattype_synonym abc_prog = "abc_inst list"type_synonym abc_state = nattext {* 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"fun abc_inst_shift :: "abc_inst \<Rightarrow> nat \<Rightarrow> abc_inst" where "abc_inst_shift (Inc m) n = Inc m" | "abc_inst_shift (Dec m e) n = Dec m (e + n)" | "abc_inst_shift (Goto m) n = Goto (m + n)"fun abc_shift :: "abc_inst list \<Rightarrow> nat \<Rightarrow> abc_inst list" where "abc_shift xs n = map (\<lambda> x. abc_inst_shift x n) xs" fun abc_comp :: "abc_inst list \<Rightarrow> abc_inst list \<Rightarrow> abc_inst list" (infixl ";" 99) where "al; bl = (let al_len = length al in al @ abc_shift bl al_len)"end