# HG changeset patch # User Christian Urban # Date 1361885080 0 # Node ID d93cc4295306ee694ca70f6f14dc05051f61f117 # Parent 0eef61c568918b31a9e019269d1509ebecec4d7f tuned some files diff -r 0eef61c56891 -r d93cc4295306 Paper/Paper.thy --- 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 diff -r 0eef61c56891 -r d93cc4295306 ROOT --- 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" diff -r 0eef61c56891 -r d93cc4295306 ROOT.ML --- 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", diff -r 0eef61c56891 -r d93cc4295306 scala/ex.scala --- 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))) diff -r 0eef61c56891 -r d93cc4295306 scala/recs.scala --- 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 { diff -r 0eef61c56891 -r d93cc4295306 thys/Rec_Def.thy --- 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, \, xn, j) > 0"}. *} Mn nat recf +(* +partial_function (tailrec) + rec_exec :: "recf \ nat list \ 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 (\ 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 diff -r 0eef61c56891 -r d93cc4295306 thys/UF.thy --- 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