--- 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