implemented new UF in scala; made some small adjustments to the definitions in the theory
files
header {* Definition of Recursive Functions *}theory Rec_Defimports Main "~~/src/HOL/Library/Monad_Syntax"begindatatype recf = Zero | Succ | Id nat nat --"Projection"| Cn nat recf "recf list" --"Composition"| 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 autothm eval.psimpsthm eval.pinductthm eval.domintroslemma "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 "eval f i gs ns = (case (i, gs, f, ns) of (None, None, Zero, [n]) \<Rightarrow> Some 0 | (None, None, Succ, [n]) \<Rightarrow> Some (n + 1) | (None, None, Id i j, ns) \<Rightarrow> if (j < i) then Some (ns ! j) else None | (None, None, Pr n f g, 0 # ns) \<Rightarrow> eval f None None ns | (None, None, Pr n f g, Suc k # ns) \<Rightarrow> do { r \<leftarrow> eval (Pr n f g) None None (k # ns); eval g None None (r # k # ns) } | (None, None, Mn n f, ns) \<Rightarrow> eval f (Some 0) None ns | (Some n, None, f, ns) \<Rightarrow> do { r \<leftarrow> eval f None None (n # ns); if r = 0 then Some n else eval f (Some (Suc n)) None ns } | (None, None, Cn n f [], ns) \<Rightarrow> eval f None None [] | (None, None, Cn n f (g#gs), ns) \<Rightarrow> do { r \<leftarrow> eval g None None ns; eval (Cn n f gs) None (Some [r]) ns } | (None, Some rs, Cn n f [], ns) \<Rightarrow> eval f None None rs | (None, Some rs, Cn n f (g#gs), ns) \<Rightarrow> do { r \<leftarrow> eval g None None ns; eval (Cn n f gs) None (Some (r#rs)) ns } | (_, _) \<Rightarrow> None)"abbreviation "eval0 f ns \<equiv> eval f None None ns"lemma "eval0 Zero [n] = Some 0"apply(subst eval.simps)apply(simp)donelemma "eval0 Succ [n] = Some (n + 1)"apply(subst eval.simps)apply(simp)donelemma "j < i \<Longrightarrow> eval0 (Id i j) ns = Some (ns ! j)"apply(subst eval.simps)apply(simp)donelemma "eval0 (Pr n f g) (0 # ns) = eval0 f ns"apply(subst eval.simps)apply(simp)donelemma "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)donelemma "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)doneend