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