# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1362496990 0
# Node ID 30d81499766b5fa2e30dc14204807a54b9ffc9ee
# Parent  203d50aebb1c50f88cf01b5ebb26769cd2565c4f
added a version with partial_function

diff -r 203d50aebb1c -r 30d81499766b Tests/Rec_Def.thy
--- a/Tests/Rec_Def.thy	Sun Mar 03 14:08:33 2013 +0000
+++ b/Tests/Rec_Def.thy	Tue Mar 05 15:23:10 2013 +0000
@@ -4,23 +4,6 @@
 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 
@@ -29,56 +12,58 @@
 | Pr nat recf recf        --"Primitive recursion"
 | Mn nat recf             --"Minimisation"
 
-partial_function (tailrec) 
-  findzero :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"
+partial_function (option) 
+  eval :: "recf \<Rightarrow> nat option \<Rightarrow> (nat list) option => nat list \<Rightarrow> nat option"
 where
-  "findzero f n = (if f n = 0 then n else findzero f (Suc n))"
+ "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)"
 
-print_theorems
+abbreviation
+  "eval0 f ns \<equiv> eval f None None ns"
 
-declare findzero.simps[simp del] 
-
-lemma "findzero (\<lambda>n. if n = 3 then 0 else 1) 0 = 3"
-apply(simp add: findzero.simps)
+lemma "eval0 Zero [n] = Some 0"
+apply(subst eval.simps)
+apply(simp)
 done
 
-lemma "findzero (\<lambda>n. if n = 3 then 0 else 1) 0 \<noteq> 2"
-apply(simp add: findzero.simps)
+lemma "eval0 Succ [n] = Some (n + 1)"
+apply(subst eval.simps)
+apply(simp)
+done
+
+lemma "eval0 (Id i j) ns = (if (j < i) then Some (ns ! j) else None)" 
+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
 
 
-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