diff -r 763ed488fa79 -r 12f278bd67aa Tests/Rec_Def.thy
--- a/Tests/Rec_Def.thy	Wed Mar 06 00:59:18 2013 +0000
+++ b/Tests/Rec_Def.thy	Wed Mar 06 07:08:51 2013 +0000
@@ -12,6 +12,55 @@
 | Pr nat recf recf        --"Primitive recursion"
 | Mn nat recf             --"Minimisation"
 
+primrec hd0 :: "nat list => nat" where
+"hd0 [] = 0" |
+"hd0 (m # ms) = m"
+
+fun
+  primerec :: "recf \<Rightarrow> nat \<Rightarrow> bool"
+where
+  "primerec Zero m = (m = 1)" |
+  "primerec Succ m = (m = 1)" |
+  "primerec (Id i j) m = (j < i \<and> i = m) " |
+  "primerec (Cn n f gs) m = (primerec f (length gs) \<and> (\<forall>g \<in> set gs. primerec g m))" |
+  "primerec (Pr n f g) m = (0 < m \<and> primerec f (m - 1) \<and> primerec g (m + 2))" |
+  "primerec (Mn n f) m = False"
+
+function (domintros) eval :: "recf \<Rightarrow> nat list \<Rightarrow> nat"
+  where
+  "eval Zero ns = 0" |
+  "eval Succ ns = (Suc (hd0 ns))" |
+  "eval (Id m n) ns = (ns ! n)" |
+  "eval (Cn n f gs) ns = 
+      (let ys = (map (\<lambda>a. eval a ns) gs) in eval f ys)" | 
+  "eval (Pr n f g) [] = eval f []" |
+  "eval (Pr n f g) (0#ns) = eval f ns" |
+  "eval (Pr n f g) (Suc m#ns) = eval g (eval (Pr n f g) (m # ns) # m # ns)" |
+  "eval (Mn n f) ns = (LEAST x. eval f (x # ns) = 0)"
+by pat_completeness auto
+
+thm eval.psimps
+thm eval.pinduct
+thm eval.domintros
+
+lemma
+  "primerec f (length ns) \<Longrightarrow> eval_dom (f, (ns::nat list))"
+apply(induct arbitrary: ns rule: primerec.induct)
+apply(auto intro: eval.domintros)
+????
+
+
+
+
+
+
+
+
+
+
+
+  
+
 partial_function (option) 
   eval :: "recf \<Rightarrow> nat option \<Rightarrow> (nat list) option => nat list \<Rightarrow> nat option"
 where
@@ -37,30 +86,33 @@
 abbreviation
   "eval0 f ns \<equiv> eval f None None ns"
 
-lemma "eval0 Zero [n] = Some 0"
-apply(subst eval.simps)
+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)
 apply(simp)
 done
 
-lemma "eval0 Succ [n] = Some (n + 1)"
-apply(subst eval.simps)
+lemma "eval1 Succ [n] = n + 1"
+apply(subst (1 2) eval.simps)
 apply(simp)
 done
 
-lemma "eval0 (Id i j) ns = (if (j < i) then Some (ns ! j) else None)" 
-apply(subst eval.simps)
+lemma "j < i \<Longrightarrow> eval1 (Id i j) ns = ns ! j"
+apply(subst (1 2) eval.simps)
 apply(simp)
 done
 
-lemma "eval0 (Pr n f g) (0 # ns) = eval0 f ns"
-apply(subst eval.simps)
+lemma "eval1 (Pr n f g) (0 # ns) = eval1 f ns"
+apply(subst (1 2) eval.simps)
 apply(simp)
 done
 
-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)
+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)
 apply(simp)
+apply(auto)
 done