--- a/Paper/Paper.thy	Tue Feb 26 12:47:03 2013 +0000
+++ b/Paper/Paper.thy	Tue Feb 26 13:24:40 2013 +0000
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports "../thys/UTM"
+imports "../thys/UTM" "../thys/Abacus_Defs"
 begin
 
 

--- a/ROOT	Tue Feb 26 12:47:03 2013 +0000
+++ b/ROOT	Tue Feb 26 13:24:40 2013 +0000
@@ -6,6 +6,7 @@
     "thys/Uncomputable"
     "thys/Abacus_Mopup"
     "thys/Abacus"
+    "thys/Abacus_Defs"
     "thys/Rec_Def"
     "thys/Recursive"
     "thys/UF"

--- a/ROOT.ML	Tue Feb 26 12:47:03 2013 +0000
+++ b/ROOT.ML	Tue Feb 26 13:24:40 2013 +0000
@@ -5,6 +5,7 @@
 	  "thys/Uncomputable", 
           "thys/Abacus_Mopup",
 	  "thys/Abacus", 
+          "thys/Abacus_Defs",
 	  "thys/Rec_Def", 
 	  "thys/Recursive",
           "thys/UF",

--- a/scala/ex.scala	Tue Feb 26 12:47:03 2013 +0000
+++ b/scala/ex.scala	Tue Feb 26 13:24:40 2013 +0000
@@ -112,8 +112,8 @@
 println("Disj 0 6:  " + Disj.eval(List(0, 6)))
 println("Disj 6 4:  " + Disj.eval(List(6, 4)))
 println("Disj 0 0:  " + Disj.eval(List(0, 0)))
-//println("Sigma:     " + Sigma(S).eval(List(0,1,2)))
-//println("Sigma:     " + Sigma(S).eval(List(0,1,2,3,4,5)))
+println("Sigma:     " + Sigma(Add).eval(List(2,3)))
+
 
 
 val ABCZero = Abacus(List(Goto(1)))

--- a/scala/recs.scala	Tue Feb 26 12:47:03 2013 +0000
+++ b/scala/recs.scala	Tue Feb 26 13:24:40 2013 +0000
@@ -9,21 +9,21 @@
 case object Z extends Rec {
   override def eval(ns: List[Int]) = ns match {
     case n::Nil => 0
-    case _ => throw new IllegalArgumentException("Z: args")
+    case _ => throw new IllegalArgumentException("Z args: " + ns)
   }
 } 
 
 case object S extends Rec {
   override def eval(ns: List[Int]) = ns match {
     case n::Nil => n + 1
-    case _ => throw new IllegalArgumentException("S: args")
+    case _ => throw new IllegalArgumentException("S args: " + ns)
   }
 } 
 
 case class Id(n: Int, m: Int) extends Rec {
   override def eval(ns: List[Int]) = 
     if (ns.length == n && m < n) ns(m)
-    else throw new IllegalArgumentException("Id: args")
+    else throw new IllegalArgumentException("Id args: " + ns + "," + n + "," + m)
 }
 
 case class Cn(n: Int, f: Rec, gs: List[Rec]) extends Rec {

--- a/thys/Rec_Def.thy	Tue Feb 26 12:47:03 2013 +0000
+++ b/thys/Rec_Def.thy	Tue Feb 26 13:24:40 2013 +0000
@@ -31,6 +31,24 @@
   @{text "j"}, @{text "f (x1, x2, \<dots>, xn, j) > 0"}. *}
   Mn nat recf 
 
+(*
+partial_function (tailrec) 
+  rec_exec :: "recf \<Rightarrow> nat list \<Rightarrow> nat"
+where
+  "rec_exec f ns = (case (f, ns) of
+      (z, xs) => 0
+   |  (s, xs) => Suc (xs ! 0)
+   |  (id m n, xs) => (xs ! n) 
+   |  (Cn n f gs, xs) => 
+             (let ys = (map (\<lambda> a. rec_exec a xs) gs) in 
+                                  rec_exec f ys)
+   |  (Pr n f g, xs) => 
+         (if last xs = 0 then rec_exec f (butlast xs)
+          else rec_exec g (butlast xs @ [last xs - 1] @
+            [rec_exec (Pr n f g) (butlast xs @ [last xs - 1])]))
+   |  (Mn n f, xs) => (LEAST x. rec_exec f (xs @ [x]) = 0))"
+*)
+
 text {* 
   The semantis of recursive operators is given by an inductively defined
   relation as follows, where  

--- a/thys/UF.thy	Tue Feb 26 12:47:03 2013 +0000
+++ b/thys/UF.thy	Tue Feb 26 13:24:40 2013 +0000
@@ -58,7 +58,7 @@
 
 
 text {*
-  Signal function, which returns 1 when the input argument is greater than @{text "0"}.
+  Sign function, which returns 1 when the input argument is greater than @{text "0"}.
 *}
 definition rec_sg :: "recf"
   where