--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/Abacus.thy	Thu Jun 06 17:27:45 2013 +0100
@@ -0,0 +1,98 @@
+theory Abacus
+imports Main
+begin 
+
+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"
+
+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
\ No newline at end of file