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"
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 "eval0 (Id i j) ns = (if (j < i) then Some (ns ! j) else None)"
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
end