header {* Definition of Recursive Functions *}

theory Rec_Def
imports Main "~~/src/HOL/Library/Monad_Syntax"
begin

type_synonym heap = "nat \<Rightarrow> nat"
type_synonym exception = nat

datatype 'a Heap = Heap "heap \<Rightarrow> (('a + exception) * heap)"

definition return
where "return x = Heap (Pair (Inl x))"

fun exec
where "exec (Heap f) = f" 

definition bind ("_ >>= _")
where "bind f g = Heap (\<lambda>h. case (exec f h) of 
                           (Inl x, h') \<Rightarrow> exec (g x) h'
                         | (Inr exn, h') \<Rightarrow> (Inr exn, h')
                       )"

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 (tailrec) 
  findzero :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"
where
  "findzero f n = (if f n = 0 then n else findzero f (Suc n))"

print_theorems

declare findzero.simps[simp del] 

lemma "findzero (\<lambda>n. if n = 3 then 0 else 1) 0 = 3"
apply(simp add: findzero.simps)
done

lemma "findzero (\<lambda>n. if n = 3 then 0 else 1) 0 \<noteq> 2"
apply(simp add: findzero.simps)
done


fun
  least :: "(nat \<Rightarrow> bool) \<Rightarrow> nat"
where
  "least P = (SOME n. (P n \<and> (\<forall>m. m < n \<longrightarrow> \<not> P m)))"

lemma [partial_function_mono]:
  "mono_option (\<lambda>eval. if \<forall>g\<in>set list. case eval (g, ba) of None \<Rightarrow> False | Some a \<Rightarrow> True
     then eval (recf, map (\<lambda>g. the (eval (g, ba))) list) else None)"
apply(rule monotoneI)
unfolding flat_ord_def
apply(auto)
oops

partial_function (option) 
  eval :: "recf \<Rightarrow> nat list \<Rightarrow> nat option"
where
 "eval f ns = (case (f, ns) of
                  (Zero, [n]) \<Rightarrow> Some 0
                | (Succ, [n]) \<Rightarrow> Some (n + 1)
                | (Id i j, ns) \<Rightarrow> if (j < i) then Some (ns ! j) else None               
                | (Pr n f g, 0 # ns) \<Rightarrow> eval f ns
                | (Pr n f g, Suc k # ns) \<Rightarrow>
                    do { r \<leftarrow> eval (Pr n f g) (k # ns); eval g (r # k # ns) }            
                | (Cn n f gs, ns) \<Rightarrow>  if (\<forall>g \<in> set gs. case (eval g ns) of None => False | _ => True)
                                      then eval f (map (\<lambda>g. the (eval g ns)) gs) else None
                | (_, _) \<Rightarrow> None)"

(*
                | (Cn n f gs, ns) \<Rightarrow>  if (\<forall>g \<in> set gs. case (eval g ns) of None => False | _ => True)
                                      then eval f (map (\<lambda>g. the (eval g ns)) gs) else None
*)
(*      
                | (Mn n f, ns) \<Rightarrow> Some (least (\<lambda>r. eval f (r # ns) = Some 0)) 
*)
end