# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1362319713 0
# Node ID 203d50aebb1c50f88cf01b5ebb26769cd2565c4f
# Parent  1d6a0fd9f7f488ff04ba851cdafa0f1878d55442
partial_function test

diff -r 1d6a0fd9f7f4 -r 203d50aebb1c Tests/Rec_Def.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Tests/Rec_Def.thy	Sun Mar 03 14:08:33 2013 +0000
@@ -0,0 +1,84 @@
+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
\ No newline at end of file