# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1372253743 -3600
# Node ID fa40fd8abb549c4809c6e7614dc2f14b3f71d46d
# Parent  002b07ea0a5797546148e4a70f543e591b48dbca
implemented new UF in scala; made some small adjustments to the definitions in the theory
files

diff -r 002b07ea0a57 -r fa40fd8abb54 scala/ex.scala
--- a/scala/ex.scala	Thu Jun 06 17:27:45 2013 +0100
+++ b/scala/ex.scala	Wed Jun 26 14:35:43 2013 +0100
@@ -60,51 +60,75 @@
 println("Compiled Expo 3 ^ 4: " + toTM(Expo(0, 1, 2, 3, 4, 10000).p).run(Tape(3,4,0,0,0)))
 
 // Recursive function examples 
+println("Const 8:   " + Const(8).eval(67))
 println("Add 3 4:   " + Add.eval(3, 4))
 println("Mult 3 4:  " + recs.Mult.eval(3, 4))
-println("Twice 4:   " + Twice.eval(4))
-println("FourTm 4:  " + Fourtimes.eval(4))
+println("Power 2 3: " + Power.eval(2, 3))
+println("Fact 5:    " + Fact.eval(5))
 println("Pred 9:    " + Pred.eval(9))
 println("Pred 0:    " + Pred.eval(0))
 println("Minus 6 2: " + Minus.eval(6, 2))
 println("Minus 6 8: " + Minus.eval(6, 8))
-println("Const 8:   " + Const(8).eval(67))
-println("Power 2 3: " + Power.eval(2, 3))
+
+
 println("Sign 8:    " + Sign.eval(8))
 println("Sign 0:    " + Sign.eval(0))
+println("Not 0:     " + Not.eval(0))
+println("Not 6:     " + Not.eval(6))
+println("Eq 4 4:    " + Eq.eval(4, 4))
+println("Eq 4 6:    " + Eq.eval(4, 6))
+println("Eq 6 4:    " + Eq.eval(6, 4))
+println("NotEq 4 4: " + Noteq.eval(4, 4))
+println("NotEq 4 6: " + Noteq.eval(4, 6))
+println("NotEq 6 4: " + Noteq.eval(6, 4))
+println("Conj 0 6:  " + Conj.eval(0, 6))
+println("Conj 6 4:  " + Conj.eval(6, 4))
+println("Conj 0 0:  " + Conj.eval(0, 0))
+println("Disj 0 6:  " + Disj.eval(0, 6))
+println("Disj 6 4:  " + Disj.eval(6, 4))
+println("Disj 0 0:  " + Disj.eval(0, 0))
+println("Imp  6 1:  " + Imp.eval(6, 1))
+println("Imp  6 4:  " + Imp.eval(6, 4))
+println("Imp  1 0:  " + Imp.eval(1, 0))
+println("Ifz  0 1 2:" + Ifz.eval(0, 1, 2))
+println("Ifz  1 1 2:" + Ifz.eval(1, 1, 2))
+println("If   0 1 2:" + If.eval(0, 1, 2))
+println("If   1 1 2:" + If.eval(1, 1, 2))
+
+
 println("Less 4 4:  " + Less.eval(4, 4))
 println("Less 4 6:  " + Less.eval(4, 6))
 println("Less 6 4:  " + Less.eval(6, 4))
 println("Le 4 4:    " + recs.Le.eval(4, 4))
 println("Le 4 6:    " + recs.Le.eval(4, 6))
 println("Le 6 4:    " + recs.Le.eval(6, 4))
-println("Not 0:     " + Not.eval(0))
-println("Not 6:     " + Not.eval(6))
-println("Eq 4 4:    " + Eq.eval(4, 4))
-println("Eq 4 6:    " + Eq.eval(4, 6))
-println("Eq 6 4:    " + Eq.eval(6, 4))
-println("Conj 0 6:  " + Conj.eval(0, 6))
-println("Conj 6 4:  " + Conj.eval(6, 4))
-println("Conj 0 0:  " + Conj.eval(0, 0))
-println("Disj 0 6:  " + Disj.eval(0, 6))
-println("Disj 6 4:  " + Disj.eval(6, 4))
-println("Disj 0 0:  " + Disj.eval(0, 0))
-println("Sigma Add 2 3 -> 14:  " + Sigma(Add).eval(2,3))
-println("Accum Add 2 3 -> 120: " + Accum(Add).eval(2,3))
-println("Accum Mult 2 3 -> 0:  " + Accum(recs.Mult).eval(2,3))
-println("Fact 5:  " + Fact.eval(5))
-println("Prime 0..15: " + (0 to 15).map(n => (n, Prime.eval(n))))
-println("NextPrime 3: " + NextPrime.eval(3))
-println("NthPrime 1:  " + NthPrime.eval(1))
-println("Listsum [2, 3, 4 , 5, 6]: " + Listsum(5, 4).eval(2, 3, 4, 5, 6))
-println("Strt:  " + Strt(2).eval(2, 3))
-println("(<=5) 1: " + (Less o (Id(1, 0), Const(5))).eval(1))
-println("(<=5) 5: " + (Less o (Id(1, 0), Const(5))).eval(5))
-println("(<=5) 6: " + (Less o (Id(1, 0), Const(5))).eval(6))
-println("Max (<=9): " + Maxr(Le o (Id(1, 0), Const(9))).eval(10))
-println("Max (>=9): " + Maxr(Le o (Const(9), Id(1, 0))).eval(8))
-println("test")
-println("Lg 4 2: " + Lg.eval(4, 2))
+
+println("Sigma1 Add 2 3 -> 12: " + Sigma1(Add).eval(2, 3))
+println("Accum1 Add 2 3 -> 60:  " + Accum1(Add).eval(2,3))
+println("Accum1 Mult 2 3 -> 0:  " + Accum1(Mult).eval(2,3))
+println("Accum1 (Id(2, 1)) 2 3 -> 27:  " + Accum1(Id(2, 1)).eval(2,3))
+println("Accum2 (Id(3, 1)) 2 3 3 -> 27:  " + Accum2(Id(3, 1)).eval(2,3,3))
+println("Accum3 (Id(4, 1)) 2 3 3 3 -> 27:  " + Accum3(Id(4, 1)).eval(2,3,3,3))
+println("All1 Add 2 0 -> 0:  " + All1(Add).eval(2,0))
+println("All1 Add 2 1 -> 1:  " + All1(Add).eval(2,1))
+println("All1_less Add 3 0 -> 0:  " + All1_less(Add).eval(2,0))
+println("All1_less Add 3 1 -> 1:  " + All1_less(Add).eval(2,1))
+println("All2_less (Id 3 1) 2 3 0 -> 1:  " + All2_less(Id(3, 1)).eval(2,3,0))
+println("All2_less (Id 3 0) 2 3 0 -> 0:  " + All2_less(Id(3, 0)).eval(2,3,0))
+println("Ex1 Add 2 0 -> 1:       " + Ex1(Add).eval(2,0))
+println("Ex2 Id(3,1) 2 1 0 -> 1: " + Ex2(Id(3, 1)).eval(2,1,0))
+println("Ex2 Id(3,2) 2 1 0 -> 0: " + Ex2(Id(3, 2)).eval(2,1,0))
+
+println("Quo 6 4 -> 1:   " + Quo.eval(6, 4))
+println("Quo 13 4 -> 3:  " + Quo.eval(13, 4))
+
+println("Triangle 0 - 5: " + (0 until 5).map(Triangle.eval(_)).mkString(","))
+println("MaxTriangle 10 -> 4 " + MaxTriangle.eval(10))
+
+println("Penc 1 2 -> 7: " + Penc.eval(1, 2))
+println("Pdec1 7 -> 1:  " + Pdec1.eval(7))
+println("Pdec2 7 -> 2:  " + Pdec2.eval(7))
+println("Enclen 0 .. 10: " + (0 until 10).map(EncLen.eval(_)))
 
 // compilation of rec to abacus tests
 def test_comp2(f: Rec, ns: Int*) = {
@@ -125,9 +149,6 @@
 println("Power(3, 4)   " + test_comp2(Power, 3, 4))
 println("Minus(30, 4)  " + test_comp2(Minus, 30, 4))
 println("Fact(5)       " + test_comp2(Fact, 5))
-println("Prime(5)      " + test_comp2(Prime, 5))
-//println("Prime(4)      " + test_comp2(Prime, 4))
-println("Strt(1)(2)    " + test_comp2(Strt(1), 2))
 
 
 def test_comp1(f: Rec, ns: Int*) = {
diff -r 002b07ea0a57 -r fa40fd8abb54 scala/recs2.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/scala/recs2.scala	Wed Jun 26 14:35:43 2013 +0100
@@ -0,0 +1,349 @@
+package object recs2 {
+
+//Recursive Functions
+
+abstract class Rec {
+  def eval(ns: List[Int]) : Int
+  def eval(ns: Int*) : Int = eval(ns.toList)
+
+  //syntactic convenience for composition
+  def o(r: Rec) = Cn(r.arity, this, List(r))
+  def o(r: Rec, f: Rec) = Cn(r.arity, this, List(r, f))
+  def o(r: Rec, f: Rec, g: Rec) = Cn(r.arity, this, List(r, f, g))
+  def o(r: Rec, f: Rec, g: Rec, h: Rec) = Cn(r.arity, this, List(r, f, g, h))
+  def arity : Int
+}
+
+case object Z extends Rec {
+  override def eval(ns: List[Int]) = ns match {
+    case n::Nil => 0
+    case _ => throw new IllegalArgumentException("Z args: " + ns)
+  }
+  override def arity = 1
+} 
+
+case object S extends Rec {
+  override def eval(ns: List[Int]) = ns match {
+    case n::Nil => n + 1
+    case _ => throw new IllegalArgumentException("S args: " + ns)
+  }
+  override def arity = 1 
+} 
+
+case class Id(n: Int, m: Int) extends Rec {
+  require(m < n, println("Id m < n:" + m + " " + n))
+
+  override def eval(ns: List[Int]) = 
+    if (ns.length == n && m < n) ns(m)
+    else throw new IllegalArgumentException("Id args: " + ns + "," + n + "," + m)
+
+  override def arity = n
+}
+
+case class Cn(n: Int, f: Rec, gs: List[Rec]) extends Rec {
+  require(f.arity == gs.length, 
+          println("CN " + f + "  " + gs.mkString(",") + "\n" + 
+                  "f.arity gs.length:" + f.arity + " " + gs.length))
+  
+  override def eval(ns: List[Int]) = 
+    if (ns.length == n && gs.forall(_.arity == n) && f.arity == gs.length) f.eval(gs.map(_.eval(ns)))
+    else { 
+      val msg = List("Cn f: " + f, 
+                     "n: " + n,
+                     "f arity: " + f.arity, 
+                     "ns-args: " + ns,
+                     "gs arities: " + gs.map(_.arity).mkString(", "),
+                     "gs: " + gs.mkString(", "),
+                     "ns.length == n " + (ns.length == n).toString,
+                     "gs.forall(_.arity == n) " + (gs.forall(_.arity == n)).toString,
+                     "f.arity == gs.length " + (f.arity == gs.length).toString
+                    )
+      throw new IllegalArgumentException(msg.mkString("\n"))
+    }
+
+  override def arity = n
+  override def toString = f.toString + gs.map(_.toString).mkString ("(",", ", ")")
+}
+
+// syntactic convenience
+object Cn {
+  def apply(n: Int, f: Rec, g: Rec) : Rec = new Cn(n, f, List(g))
+}
+
+case class Pr(n: Int, f: Rec, g: Rec) extends Rec {
+  override def eval(ns: List[Int]) = 
+    if (ns.length == n + 1) {
+      if (ns.head == 0) f.eval(ns.tail)
+      else {
+        val r = Pr(n, f, g).eval(ns.head - 1 :: ns.tail)
+        g.eval(ns.head - 1 :: r :: ns.tail)
+      }
+    }
+    else {
+      val msg = List("Pr f: " + f, 
+                     "g: " + g,
+                     "n: " + n,
+                     "f arity: " + f.arity,
+                     "g arity: " + g.arity,
+                     "ns-args: " + ns)
+      throw new IllegalArgumentException(msg.mkString("\n"))
+    }
+
+  override def arity = n + 1
+  override def toString = "Pr(" + f.toString + ", " + g.toString + ")"
+}
+
+// syntactic convenience
+object Pr {
+  def apply(r: Rec, f: Rec) : Rec = Pr(r.arity, r, f) 
+}
+
+case class Mn(n: Int, f: Rec) extends Rec {
+  def evaln(ns: List[Int], n: Int) : Int = 
+    if (f.eval(n :: ns) == 0) n else evaln(ns, n + 1)
+
+  override def eval(ns: List[Int]) = 
+    if (ns.length == n) evaln(ns, 0) 
+    else throw new IllegalArgumentException("Mn: args")
+
+  override def arity = n
+}
+
+object Mn {
+  def apply(f: Rec) : Rec = Mn(f.arity - 1, f)
+}
+
+
+
+
+// Recursive Function examples
+def Const(n: Int) : Rec = n match {
+  case 0 => Z
+  case n => S o Const(n - 1)
+}
+
+def Swap(f: Rec) = f o (Id(2, 1), Id(2, 0))
+val Add = Pr(Id(1, 0), S o Id(3, 1))
+val Mult = Pr(Z, Add o (Id(3, 1), Id(3, 2)))
+val Power = Swap(Pr(Const(1), Mult o (Id(3, 1), Id(3, 2))))
+val Fact = (Pr (Const(1), Mult o (S o Id(3, 0), Id(3, 1)))) o (Id(1, 0), Id(1, 0))
+val Pred = Pr(Z, Id(3, 0)) o (Id(1, 0), Id(1, 0))
+val Minus = Swap(Pr(Id(1, 0), Pred o Id(3, 1)))
+
+val Sign = Minus o (Const(1), Minus o (Const(1), Id(1, 0)))
+val Not = Minus o (Const(1), Id(1, 0))
+val Eq = Minus o (Const(1) o Id(2, 0), Add o (Minus, Swap(Minus))) 
+val Noteq = Not o Eq 
+val Conj = Sign o Mult
+val Disj = Sign o Add 
+val Imp = Disj o (Not o Id(2, 0), Id(2, 1))
+val Ifz = Pr(Id(2, 0), Id(4, 3))
+val If = Ifz o (Not o Id(3, 0), Id(3, 1), Id (3, 2))
+
+val Less = Sign o (Swap(Minus))
+val Le = Disj o (Less, Eq)
+
+def Sigma1(f: Rec) = Pr(f o (Z o (Id(1, 0)), Id(1, 0)), 
+                        Add o (Id(3, 1), f o (S o Id(3, 0), Id(3, 2))))
+def Sigma2(f: Rec) = Pr(f o (Z o (Id(2, 0)), Id(2, 0), Id(2, 1)), 
+                        Add o (Id(4, 1), f o (S o Id(4, 0), Id(4, 2), Id(4, 3))))
+
+def Accum1(f: Rec) = Pr(f o (Z o (Id(1, 0)), Id(1, 0)), 
+                        Mult o (Id(3, 1), f o (S o Id(3, 0), Id(3, 2))))
+def Accum2(f: Rec) = Pr(f o (Z o (Id(2, 0)), Id(2, 0), Id(2, 1)), 
+                        Mult o (Id(4, 1), f o (S o Id(4, 0), Id(4, 2), Id(4, 3))))
+def Accum3(f: Rec) = Pr(f o (Z o (Id(3, 0)), Id(3, 0), Id(3, 1), Id(3, 2)), 
+                        Mult o (Id(5, 1), f o (S o Id(5, 0), Id(5, 2), Id(5, 3), Id(5, 4))))
+
+def All1(f: Rec) = Sign o (Accum1(f))
+def All2(f: Rec) = Sign o (Accum2(f))
+def All3(f: Rec) = Sign o (Accum3(f))
+
+def All1_less(f: Rec) = {
+  val cond1 = Eq o (Id(3, 0), Id(3, 1))
+  val cond2 = f o (Id(3, 0), Id(3, 2))
+  All2(Disj o (cond1, cond2)) o (Id(2, 0), Id(2, 0), Id(2, 1))
+}
+
+def All2_less(f: Rec) = {
+  val cond1 = Eq o (Id(4, 0), Id(4, 1))
+  val cond2 = f o (Id(4, 0), Id(4, 2), Id(4, 3))
+  All3(Disj o (cond1, cond2)) o (Id(3, 0), Id(3, 0), Id(3, 1), Id(3, 2))
+}
+
+def Ex1(f: Rec) = Sign o (Sigma1(f))
+def Ex2(f: Rec) = Sign o (Sigma2(f))
+
+val Quo = {
+  val lhs = S o (Id(3, 0))
+  val rhs = Mult o (Id(3, 2), S o (Id(3, 1)))
+  val cond = Eq o (lhs, rhs)
+  val if_stmt = If o (cond, S o (Id(3, 1)), Id(3, 1))
+  Pr(Z, if_stmt)
+}
+
+def Iter(f: Rec) = Pr(Id(1, 0), f o (Id(3, 1)))
+
+def Max1(f: Rec) = Pr(Z, Ifz o (f o (S o (Id(3, 0)), Id(3, 2)), S o (Id(3, 0)), Id(3, 1)))
+def Max2(f: Rec) = Pr(Z, Ifz o (f o (S o (Id(4, 0)), Id(4, 2), Id(4, 3)), S o (Id(4, 0)), Id(4, 1)))
+ 
+val Triangle = Quo o (Mult o (Id(1, 0), S), Const(2))
+
+val MaxTriangle = {
+  val cond = Not o (Le o (Triangle o (Id(2, 0)), Id(2, 1))) 
+  Max1(cond) o (Id(1, 0), Id(1, 0))
+}
+
+val MaxTriangle2 = {
+  Pred o Mn(Le o (Triangle o (Id(2, 0)), Id(2, 1)))
+}
+
+case object MaxTriangleFast extends Rec {
+  def triangle(n: Int) : Int = (n * (n + 1)) / 2
+
+  def search(m: Int, n: Int) : Int = {
+    if (triangle(n) > m) n - 1 else search(m, n + 1)
+  }
+
+  override def eval(ns: List[Int]) = ns match {
+    case n::Nil => search(n, 0)
+    case _ => throw new IllegalArgumentException("MT args: " + ns)
+  }
+
+  override def arity = 1
+}
+
+case object TriangleFast extends Rec {
+  def triangle(n: Int) : Int = (n * (n + 1)) / 2
+
+  override def eval(ns: List[Int]) = ns match {
+    case n::Nil => triangle(n)
+    case _ => throw new IllegalArgumentException("Tr args: " + ns)
+  }
+
+  override def arity = 1
+}
+
+//(0 until 200).map(MaxTriangleFast.eval(_))
+
+
+val Penc = Add o (TriangleFast o (Add o (Id(2, 0), Id(2, 1))), Id(2, 0))
+val Pdec1 = Minus o (Id(1, 0), Triangle o (MaxTriangle o (Id(1, 0)))) 
+val Pdec2 = Minus o (MaxTriangle o (Id(1, 0)), Pdec1 o (Id(1, 0))) 
+
+def Lenc(fs: List[Rec]) : Rec = fs match {
+  case Nil => Z
+  case f::fs => Penc o (S o (f), Lenc(fs))
+}
+
+val Ldec = Pred o (Pdec1 o (Swap (Iter(Pdec2))))
+
+val Within = Less o (Z o (Id(2, 0)), Swap (Iter(Pdec2)))
+val Enclen = (Max1(Not o (Within o (Id(2, 1), Pred o (Id(2, 0)))))) o (Id(1, 0), Id(1, 0))
+ 
+
+val Read = Ldec o (Id(1, 0), Const(0))
+val Write = Penc o (S o (Id(2, 0)), Pdec2 o (Id(2, 1)))
+
+val Newleft = {
+  val cond0 = Eq o (Id(3, 2), Const(0))
+  val cond1 = Eq o (Id(3, 2), Const(1))
+  val cond2 = Eq o (Id(3, 2), Const(2))
+  val cond3 = Eq o (Id(3, 2), Const(3))
+  val case3 = Penc o (S o (Read o (Id(3, 1))), Id(3, 0)) 
+  If o (cond0, 
+        Id(3, 0),
+        If o (cond1, 
+              Id(3, 0),  
+              If o (cond2, 
+                    Pdec2 o (Id(3, 0)),
+                    If o (cond3, case3, Id(3, 0)))))
+}
+
+val Newright = {
+  val cond0 = Eq o (Id(3, 2), Const(0))
+  val cond1 = Eq o (Id(3, 2), Const(1))
+  val cond2 = Eq o (Id(3, 2), Const(2))
+  val cond3 = Eq o (Id(3, 2), Const(3))
+  val case2 = Penc o (S o (Read o (Id(3, 0))), Id(3, 1))
+  If o (cond0, 
+        Write o (Const(0), Id(3, 1)),
+        If o (cond1, 
+              Write o (Const(1), Id(3, 1)),  
+              If o (cond2, 
+                    case2,
+                    If o (cond3, Pdec2 o (Id(3, 1)), Id(3, 0)))))
+}
+
+val Actn = Swap (Pr(Pdec1 o (Pdec1 o (Id(1, 0))), Pdec1 o (Pdec2 o (Id(3, 2)))))
+
+val Action = {
+  val cond1 = Noteq o (Id(3, 1), Z)
+  val cond2 = Within o (Id(3, 0), Pred o (Id(3, 1)))
+  val if_branch = Actn o (Ldec o (Id(3, 0), Pred o (Id(3, 1))), Id(3, 2))
+  If o (Conj o (cond1, cond2), if_branch, Const(4))
+}
+
+val Newstat = Swap (Pr (Pdec2 o (Pdec1 o (Id(1, 0))),
+                        Pdec2 o (Pdec2 o (Id(3, 2)))))
+
+val Newstate = {
+  val cond = Noteq o (Id(3, 1), Z)
+  val if_branch = Newstat o (Ldec o (Id(3, 0), Pred o (Id(3, 1))), Id(3, 2))
+  If o (cond, if_branch, Z)
+}
+
+val Conf = Lenc (List(Id(3, 0), Id(3, 1), Id(3, 2)))
+
+val State = Ldec o (Id(1, 0), Z)
+
+val Left = Ldec o (Id(1, 0), Const(1))
+
+val Right = Ldec o (Id(1, 0), Const(2))
+
+val Step = {
+  val left = Left o (Id(2, 0))
+  val right = Right o (Id(2, 0))
+  val state = State o (Id(2, 0))
+  val read = Read o (right)
+  val action = Action o (Id(2, 1), state, read)
+  val newstate = Newstate o (Id(2, 1), state, read)
+  val newleft = Newleft o (left, right, action)
+  val newright = Newright o (left, right, action) 
+  Conf o (newstate, newleft, newright)
+ } 
+
+val Steps = Pr (Id(2, 0), Step o (Id(4, 1), Id(4, 3)))
+
+val Stknum = Minus o (Sigma1(Ldec o (Id(2, 1), Id(2, 0))) o (Enclen o (Id(1, 0)), Id(1, 0)),
+                      Ldec o (Id(1, 0), Enclen o (Id(1, 0))))
+
+val Right_std = {
+  val bound = Enclen o (Id(1, 0))
+  val cond1 = Le o (Const(1) o (Id(2, 0)), Id(2, 0))
+  val cond2 = All1_less (Eq o (Ldec o (Id(2, 1), Id(2, 0)), Const(1)))
+  val bound2 = Minus o (Enclen o (Id(2, 1)), Id(2, 0))
+  val cond3 = 
+    (All2_less (Eq o (Ldec o (Id(3, 2), Add o (Id(3, 1), Id(3, 0))), Z))) o (bound2, Id(2, 0), Id(2, 1)) 
+  Ex1(Conj o (Conj o (cond1, cond2), cond3)) o (bound, Id(1, 0))
+}
+
+val Left_std = {
+  val cond = Eq o (Ldec o (Id(2, 1), Id(2, 0)), Z)
+  (All1_less(cond)) o (Enclen o (Id(1, 0)), Id(1, 0))
+}
+
+val Std = Conj o (Left_std o (Left o (Id(1, 0))), Right_std o (Right o (Id(1, 0))))
+
+val Final = Eq o (State o (Id(1, 0)), Z)
+
+val Stop = {
+  val stps = Steps o (Id(3, 2), Id(3, 1), Id(3, 0))
+  Conj o (Final o (stps), Std o (stps))
+}
+
+val Halt = Mn (Not o (Stop o (Id(3, 1), Id(3, 2), Id(3, 0))))
+
+val UF = Pred o (Stknum o (Right o (Steps o (Halt o (Id(2, 0), Id(2, 1)), Id(2, 1), Id(2, 0)))))
+
+}
diff -r 002b07ea0a57 -r fa40fd8abb54 thys2/Recs.thy
--- a/thys2/Recs.thy	Thu Jun 06 17:27:45 2013 +0100
+++ b/thys2/Recs.thy	Wed Jun 26 14:35:43 2013 +0100
@@ -213,7 +213,7 @@
 | termi_pr: "\<lbrakk>\<forall> y < x. terminates g (y # (rec_eval (Pr n f g) (y # xs) # xs));
               terminates f xs;
               length xs = n\<rbrakk> 
-              \<Longrightarrow> terminates (Pr n f g) (xs @ [x])"
+              \<Longrightarrow> terminates (Pr n f g) (x # xs)"
 | termi_mn: "\<lbrakk>length xs = n; terminates f (r # xs); 
               rec_eval f (r # xs) = 0;
               \<forall> i < r. terminates f (i # xs) \<and> rec_eval f (i # xs) > 0\<rbrakk> \<Longrightarrow> terminates (Mn n f) xs"
@@ -242,8 +242,11 @@
 definition 
   "rec_power = rec_swap (PR (constn 1) (CN rec_mult [Id 3 1, Id 3 2]))"
 
+definition 
+  "rec_fact_aux = PR (constn 1) (CN rec_mult [CN S [Id 3 0], Id 3 1])"
+
 definition
-  "rec_fact = PR (constn 1) (CN rec_mult [CN S [Id 3 0], Id 3 1])"
+  "rec_fact = CN rec_fact_aux [Id 1 0, Id 1 0]"
 
 definition 
   "rec_pred = CN (PR Z (Id 3 0)) [Id 1 0, Id 1 0]"
@@ -271,9 +274,13 @@
   "rec_eval rec_power [x, y] = x ^ y"
 by (induct y) (simp_all add: rec_power_def)
 
+lemma fact_aux_lemma [simp]: 
+  "rec_eval rec_fact_aux [x, y] = fact x"
+by (induct x) (simp_all add: rec_fact_aux_def)
+
 lemma fact_lemma [simp]: 
   "rec_eval rec_fact [x] = fact x"
-by (induct x) (simp_all add: rec_fact_def)
+by (simp add: rec_fact_def)
 
 lemma pred_lemma [simp]: 
   "rec_eval rec_pred [x] =  x - 1"
@@ -300,7 +307,7 @@
   @{text "rec_eq"} compares two arguments: returns @{text "1"}
   if they are equal; @{text "0"} otherwise. *}
 definition 
-  "rec_eq = CN rec_minus [constn 1, CN rec_add [rec_minus, rec_swap rec_minus]]"
+  "rec_eq = CN rec_minus [CN (constn 1) [Id 2 0], CN rec_add [rec_minus, rec_swap rec_minus]]"
 
 definition 
   "rec_noteq = CN rec_not [rec_eq]"
@@ -385,36 +392,40 @@
 section {* Summation and Product Functions *}
 
 definition 
-  "rec_sigma1 f = PR (CN f [Z, Id 1 0]) (CN rec_add [Id 3 1, CN f [S, Id 3 2]])"
+  "rec_sigma1 f = PR (CN f [CN Z [Id 1 0], Id 1 0]) 
+                     (CN rec_add [Id 3 1, CN f [CN S [Id 3 0], Id 3 2]])"
 
 definition 
-  "rec_sigma2 f = PR (CN f [Z, Id 2 0, Id 2 1]) (CN rec_add [Id 4 1, CN f [S, Id 4 2, Id 4 3]])"
+  "rec_sigma2 f = PR (CN f [CN Z [Id 2 0], Id 2 0, Id 2 1]) 
+                     (CN rec_add [Id 4 1, CN f [CN S [Id 4 0], Id 4 2, Id 4 3]])"
 
 definition 
-  "rec_accum1 f = PR (CN f [Z, Id 1 0]) (CN rec_mult [Id 3 1, CN f [S, Id 3 2]])"
+  "rec_accum1 f = PR (CN f [CN Z [Id 1 0], Id 1 0]) 
+                     (CN rec_mult [Id 3 1, CN f [CN S [Id 3 0], Id 3 2]])"
 
 definition 
-  "rec_accum2 f = PR (CN f [Z, Id 2 0, Id 2 1]) (CN rec_mult [Id 4 1, CN f [S, Id 4 2, Id 4 3]])"
+  "rec_accum2 f = PR (CN f [CN Z [Id 2 0], Id 2 0, Id 2 1]) 
+                     (CN rec_mult [Id 4 1, CN f [CN S [Id 4 0], Id 4 2, Id 4 3]])"
 
 definition 
-  "rec_accum3 f = PR (CN f [Z, Id 3 0, Id 3 1, Id 3 2]) 
-                     (CN rec_mult [Id 5 1, CN f [S, Id 5 2, Id 5 3, Id 5 4]])"
+  "rec_accum3 f = PR (CN f [CN Z [Id 3 0], Id 3 0, Id 3 1, Id 3 2]) 
+                     (CN rec_mult [Id 5 1, CN f [CN S [Id 5 0], Id 5 2, Id 5 3, Id 5 4]])"
 
 
 lemma sigma1_lemma [simp]: 
-  shows "rec_eval (rec_sigma1 f) [x, y] = (\<Sum> z \<le> x. (rec_eval f)  [z, y])"
+  shows "rec_eval (rec_sigma1 f) [x, y] = (\<Sum> z \<le> x. rec_eval f [z, y])"
 by (induct x) (simp_all add: rec_sigma1_def)
 
 lemma sigma2_lemma [simp]: 
-  shows "rec_eval (rec_sigma2 f) [x, y1, y2] = (\<Sum> z \<le> x. (rec_eval f)  [z, y1, y2])"
+  shows "rec_eval (rec_sigma2 f) [x, y1, y2] = (\<Sum> z \<le> x. rec_eval f  [z, y1, y2])"
 by (induct x) (simp_all add: rec_sigma2_def)
 
 lemma accum1_lemma [simp]: 
-  shows "rec_eval (rec_accum1 f) [x, y] = (\<Prod> z \<le> x. (rec_eval f)  [z, y])"
+  shows "rec_eval (rec_accum1 f) [x, y] = (\<Prod> z \<le> x. rec_eval f  [z, y])"
 by (induct x) (simp_all add: rec_accum1_def)
 
 lemma accum2_lemma [simp]: 
-  shows "rec_eval (rec_accum2 f) [x, y1, y2] = (\<Prod> z \<le> x. (rec_eval f)  [z, y1, y2])"
+  shows "rec_eval (rec_accum2 f) [x, y1, y2] = (\<Prod> z \<le> x. rec_eval f  [z, y1, y2])"
 by (induct x) (simp_all add: rec_accum2_def)
 
 lemma accum3_lemma [simp]: 
@@ -434,8 +445,9 @@
   "rec_all3 f = CN rec_sign [rec_accum3 f]"
 
 definition
-  "rec_all1_less f = (let f' = CN rec_disj [CN rec_eq [Id 3 0, Id 3 1], CN f [Id 3 0, Id 3 2]] 
-                      in CN (rec_all2 f') [Id 2 0, Id 2 0, Id 2 1])"
+  "rec_all1_less f = (let cond1 = CN rec_eq [Id 3 0, Id 3 1] in
+                      let cond2 = CN f [Id 3 0, Id 3 2] 
+                      in CN (rec_all2 (CN rec_disj [cond1, cond2])) [Id 2 0, Id 2 0, Id 2 1])"
 
 definition
   "rec_all2_less f = (let cond1 = CN rec_eq [Id 4 0, Id 4 1] in 
@@ -540,7 +552,7 @@
 section {* Iteration *}
 
 definition
-   "rec_iter f = PR (Id 2 0) (CN f [Id 3 1])"
+   "rec_iter f = PR (Id 1 0) (CN f [Id 3 1])"
 
 fun Iter where
   "Iter f 0 = id"
@@ -585,14 +597,14 @@
 by (simp add: BMax_rec_eq2 Set.filter_def)
 
 definition 
-  "rec_max1 f = PR (constn 0) (CN rec_ifz [CN f [CN S [Id 3 0], Id 3 2], CN S [Id 4 0], Id 4 1])"
+  "rec_max1 f = PR Z (CN rec_ifz [CN f [CN S [Id 3 0], Id 3 2], CN S [Id 3 0], Id 3 1])"
  
 lemma max1_lemma [simp]:
   "rec_eval (rec_max1 f) [x, y] = BMax_rec (\<lambda>u. rec_eval f [u, y] = 0) x"
 by (induct x) (simp_all add: rec_max1_def)
 
 definition 
-  "rec_max2 f = PR (constn 0) (CN rec_ifz [CN f [CN S [Id 4 0], Id 4 2, Id 4 3], CN S [Id 4 0], Id 4 1])"
+  "rec_max2 f = PR Z (CN rec_ifz [CN f [CN S [Id 4 0], Id 4 2, Id 4 3], CN S [Id 4 0], Id 4 1])"
  
 lemma max2_lemma [simp]:
   "rec_eval (rec_max2 f) [x, y1, y2] = BMax_rec (\<lambda>u. rec_eval f [u, y1, y2] = 0) x"
@@ -801,7 +813,7 @@
 by (simp add: enclen_def)
 
 
-text {* Recursive De3finitions for List Encodings *}
+text {* Recursive Definitions for List Encodings *}
 
 fun 
   rec_lenc :: "recf list \<Rightarrow> recf" 
diff -r 002b07ea0a57 -r fa40fd8abb54 thys2/UF_Rec.thy
--- a/thys2/UF_Rec.thy	Thu Jun 06 17:27:45 2013 +0100
+++ b/thys2/UF_Rec.thy	Wed Jun 26 14:35:43 2013 +0100
@@ -461,7 +461,7 @@
   "rec_read = CN rec_ldec [Id 1 0, constn 0]"
 
 definition 
-  "rec_write = CN rec_penc [S, CN rec_pdec2 [Id 2 1]]"
+  "rec_write = CN rec_penc [CN S [Id 2 0], CN rec_pdec2 [Id 2 1]]"
 
 definition
     "rec_newleft =
@@ -530,7 +530,7 @@
                in CN rec_conf [newstate, newleft, newright])" 
 
 definition 
-  "rec_steps = PR (Id 3 0) (CN rec_step [Id 4 1, Id 4 3])"
+  "rec_steps = PR (Id 2 0) (CN rec_step [Id 4 1, Id 4 3])"
 
 definition
   "rec_stknum = CN rec_minus 
@@ -539,7 +539,7 @@
 
 definition
   "rec_right_std = (let bound = CN rec_enclen [Id 1 0] in
-                    let cond1 = CN rec_le [constn 1, Id 2 0] in
+                    let cond1 = CN rec_le [CN (constn 1) [Id 2 0], Id 2 0] in
                     let cond2 = rec_all1_less (CN rec_eq [CN rec_ldec [Id 2 1, Id 2 0], constn 1]) in
                     let bound2 = CN rec_minus [CN rec_enclen [Id 2 1], Id 2 0] in
                     let cond3 = CN (rec_all2_less