--- a/Tests/Rec_Def.thy	Wed Mar 06 07:08:51 2013 +0000
+++ b/Tests/Rec_Def.thy	Thu Mar 07 11:52:08 2013 +0000
@@ -16,6 +16,7 @@
 "hd0 [] = 0" |
 "hd0 (m # ms) = m"
 
+(*
 fun
   primerec :: "recf \<Rightarrow> nat \<Rightarrow> bool"
 where
@@ -49,17 +50,7 @@
 apply(auto intro: eval.domintros)
 ????
 
-
-
-
-
-
-
-
-
-
-
-  
+*)
 
 partial_function (option) 
   eval :: "recf \<Rightarrow> nat option \<Rightarrow> (nat list) option => nat list \<Rightarrow> nat option"
@@ -86,36 +77,40 @@
 abbreviation
   "eval0 f ns \<equiv> eval f None None ns"
 
-abbreviation
-  "eval1 f ns \<equiv> if (\<exists>x. eval0 f ns = Some x) then the (eval0 f ns) else undefined"
-
-lemma "eval1 Zero [n] = 0"
-apply(subst (1 2) eval.simps)
+lemma "eval0 Zero [n] = Some 0"
+apply(subst eval.simps)
 apply(simp)
 done
 
-lemma "eval1 Succ [n] = n + 1"
-apply(subst (1 2) eval.simps)
+lemma "eval0 Succ [n] = Some (n + 1)"
+apply(subst eval.simps)
 apply(simp)
 done
 
-lemma "j < i \<Longrightarrow> eval1 (Id i j) ns = ns ! j"
-apply(subst (1 2) eval.simps)
+lemma "j < i \<Longrightarrow> eval0 (Id i j) ns = Some (ns ! j)"
+apply(subst eval.simps)
 apply(simp)
 done
 
-lemma "eval1 (Pr n f g) (0 # ns) = eval1 f ns"
-apply(subst (1 2) eval.simps)
+lemma "eval0 (Pr n f g) (0 # ns) = eval0 f ns"
+apply(subst eval.simps)
 apply(simp)
 done
 
-lemma "eval1 (Pr n f g) (Suc k # ns) = eval1 g ((eval1 (Pr n f g) (k # ns)) # k # ns)" 
-apply(subst (1 2) eval.simps)
+lemma "eval0 (Pr n f g) (Suc k # ns) = 
+  do { r \<leftarrow> eval0 (Pr n f g) (k # ns); eval0 g (r # k # ns) }"
+apply(subst eval.simps)
 apply(simp)
-apply(auto)
 done
 
 
 
+lemma 
+  "eval0 (Mn n f) ns = Some (LEAST r. eval0 f (r # ns) = Some 0)"
+apply(subst eval.simps)
+apply(simp)
+apply(subst eval.simps)
+apply(simp)
+done
 
 end
\ No newline at end of file