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