partial_function (option) 

  eval :: "recf \<Rightarrow> nat option \<Rightarrow> (nat list) option => nat list \<Rightarrow> nat option"

 "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)

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)