header {* Definition of Recursive Functions *}+ −
+ −
theory Rec_Def+ −
imports Main "~~/src/HOL/Library/Monad_Syntax"+ −
begin+ −
+ −
datatype 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 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+ −
"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)+ −
done+ −
+ −
lemma "eval0 Succ [n] = Some (n + 1)"+ −
apply(subst eval.simps)+ −
apply(simp)+ −
done+ −
+ −
lemma "j < i \<Longrightarrow> eval0 (Id i j) ns = Some (ns ! j)"+ −
apply(subst eval.simps)+ −
apply(simp)+ −
done+ −
+ −
lemma "eval0 (Pr n f g) (0 # ns) = eval0 f ns"+ −
apply(subst 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)+ −
apply(simp)+ −
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+ −