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