1 header {* Definition of Recursive Functions *}

     2 

     3 theory Rec_Def

     4 imports Main "~~/src/HOL/Library/Monad_Syntax"

     5 begin

     6 

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

     8 type_synonym exception = nat

     9 

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

    11 

    12 definition return

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

    14 

    15 fun exec

    16 where "exec (Heap f) = f" 

    17 

    18 definition bind ("_ >>= _")

    19 where "bind f g = Heap (\<lambda>h. case (exec f h) of 

    20                            (Inl x, h') \<Rightarrow> exec (g x) h'

    21                          | (Inr exn, h') \<Rightarrow> (Inr exn, h')

    22                        )"

    23 

    24 datatype recf = 

    25   Zero 

    26 | Succ 

    27 | Id nat nat              --"Projection"

    28 | Cn nat recf "recf list" --"Composition"

    29 | Pr nat recf recf        --"Primitive recursion"

    30 | Mn nat recf             --"Minimisation"

    31 

    32 partial_function (tailrec) 

    33   findzero :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"

    34 where

    35   "findzero f n = (if f n = 0 then n else findzero f (Suc n))"

    36 

    37 print_theorems

    38 

    39 declare findzero.simps[simp del] 

    40 

    41 lemma "findzero (\<lambda>n. if n = 3 then 0 else 1) 0 = 3"

    42 apply(simp add: findzero.simps)

    43 done

    44 

    45 lemma "findzero (\<lambda>n. if n = 3 then 0 else 1) 0 \<noteq> 2"

    46 apply(simp add: findzero.simps)

    47 done

    48 

    49 

    50 fun

    51   least :: "(nat \<Rightarrow> bool) \<Rightarrow> nat"

    52 where

    53   "least P = (SOME n. (P n \<and> (\<forall>m. m < n \<longrightarrow> \<not> P m)))"

    54 

    55 lemma [partial_function_mono]:

    56   "mono_option (\<lambda>eval. if \<forall>g\<in>set list. case eval (g, ba) of None \<Rightarrow> False | Some a \<Rightarrow> True

    57      then eval (recf, map (\<lambda>g. the (eval (g, ba))) list) else None)"

    58 apply(rule monotoneI)

    59 unfolding flat_ord_def

    60 apply(auto)

    61 oops

    62 

    63 partial_function (option) 

    64   eval :: "recf \<Rightarrow> nat list \<Rightarrow> nat option"

    65 where

    66  "eval f ns = (case (f, ns) of

    67                   (Zero, [n]) \<Rightarrow> Some 0

    68                 | (Succ, [n]) \<Rightarrow> Some (n + 1)

    69                 | (Id i j, ns) \<Rightarrow> if (j < i) then Some (ns ! j) else None               

    70                 | (Pr n f g, 0 # ns) \<Rightarrow> eval f ns

    71                 | (Pr n f g, Suc k # ns) \<Rightarrow>

    72                     do { r \<leftarrow> eval (Pr n f g) (k # ns); eval g (r # k # ns) }            

    73                 | (Cn n f gs, ns) \<Rightarrow>  if (\<forall>g \<in> set gs. case (eval g ns) of None => False | _ => True)

    74                                       then eval f (map (\<lambda>g. the (eval g ns)) gs) else None

    75                 | (_, _) \<Rightarrow> None)"

    76 

    77 (*

    78                 | (Cn n f gs, ns) \<Rightarrow>  if (\<forall>g \<in> set gs. case (eval g ns) of None => False | _ => True)

    79                                       then eval f (map (\<lambda>g. the (eval g ns)) gs) else None

    80 *)

    81 (*      

    82                 | (Mn n f, ns) \<Rightarrow> Some (least (\<lambda>r. eval f (r # ns) = Some 0)) 

    83 *)

    84 end