--- a/thys/Abacus.thy	Mon Feb 18 00:18:56 2013 +0000
+++ b/thys/Abacus.thy	Mon Feb 18 13:26:27 2013 +0000
@@ -38,7 +38,7 @@
 
 fun mult :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"
   where
-  "mult m1 m2 n p e = [Dec m1 e]@ plus m1 m2 p 1"
+  "mult m1 m2 n p e = [Dec m1 e]@ plus m2 n p 1"
 
 fun expo :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"
   where

--- a/turing.scala	Mon Feb 18 00:18:56 2013 +0000
+++ b/turing.scala	Mon Feb 18 13:26:27 2013 +0000
@@ -149,13 +149,30 @@
 case class Dec(n: Int, l: Int) extends AInst
 case class Goto(l: Int) extends AInst
 
+def ashift(ai: AInst, offset: Int, jump: Int) = ai match {
+  case Inc(n) => Inc(n)
+  case Dec(n, l) => if (l == jump) Dec(n, l) else Dec(n, l + offset)
+  case Goto(l) => if (l == jump) Goto(l) else Goto(l + offset)
+}
+
+def aadjust(ai: AInst, old_jump: Int, jump: Int) = ai match {
+  case Inc(n) => Inc(n)
+  case Dec(n, l) => if (l == old_jump) Dec(n, jump) else Dec(n, l)
+  case Goto(l) => if (l == old_jump) Goto(jump) else Goto(l)
+}
+
+
+
 type AProg = List[AInst]
 type Regs = Map[Int, Int]
 
 case class AConfig(s: Int, regs: Regs)  
 
 case class Abacus(p: AProg) {
-  
+
+  def shift(offset: Int, jump: Int) = Abacus(p.map(ashift(_, offset, jump)))
+  def adjust(old_jump: Int, jump: Int) = Abacus(p.map(aadjust(_, old_jump, jump)))
+ 
   def step(cf: AConfig) : AConfig = (nth_of(p, cf.s), cf.s) match {
     case (None, _) => cf
     case (Some(Inc(n)), s) => AConfig(s + 1, cf.regs + (n -> (dget(cf.regs, n) + 1)))
@@ -181,15 +198,32 @@
 }
 
 // examples
-class Copy(in: Int, out: Int) extends 
+def Copy(in: Int, out: Int) = 
   Abacus(List(Dec(in, -1), Inc(out), Goto(0))) 
 
-class Plus(in1: Int, in2: Int, out: Int) extends 
-  Abacus(List(Dec(in1, 4), Inc(in2), Inc(out),
-              Goto(0), Dec(out, -1), Inc(in1), Goto(4))) 
+def Plus(m: Int, n: Int, tmp: Int, jump: Int) =
+  Abacus(List(Dec(m, 4), Inc(n), Inc(tmp),
+              Goto(0), Dec(tmp, jump), Inc(m), Goto(4))) 
+
+def Mult(in1: Int, in2: Int, out: Int, tmp: Int, jump: Int) = {
+  val tm = Plus(in2, out, tmp, -1).shift(1, -1).adjust(-1, 0)
+  Abacus(Dec(in1, jump) :: tm.p)
+}
+
+def Mult(in1: Int, in2: Int, out: Int, tmp: Int, jump: Int) = {
+  val tm = Plus(in2, out, tmp, -1).shift(1, -1).adjust(-1, 0)
+  Abacus(Dec(in1, jump) :: tm.p)
+}
+
+def Expo(in1: Int, in2: Int, out: Int, tmp: Int, jump: Int) = {
+  val tm = Plus(in2, out, tmp, -1).shift(1, -1).adjust(-1, 0)
+  Abacus(Dec(in1, jump) :: tm.p)
+}
 
 
-println("Ab: " + (new Plus(0, 1, 2)).run(Map(0 -> 3, 1 -> 4)))
+println("Copy: " + (Copy(0, 1).run(Map(0 -> 3, 1 -> 0))))
+println("Plus: " + (Plus(0, 1, 2, -1).run(Map(0 -> 3, 1 -> 4, 2 -> 0))))
+println("Mult: " + (Mult(0, 1, 2, 3, -1).run(Map(0 -> 3, 1 -> 5, 2 -> 0, 3 -> 0))))
 
 
 
@@ -231,7 +265,7 @@
     else throw new IllegalArgumentException("Cn: args")
 }
 case class Mn(n: Int, f: Rec) extends Rec {
-  override def eval(ns: List[Int]) =
+  override def eval(ns: List[Int]) = 0
     
 }