# HG changeset patch
# User krauss
# Date 1287996322 -7200
# Node ID 80b7f456600ff8244a8274b31b3f2d5ac526985a
# Parent  dbab949c2717d23192cc078c2b0e048fdf54873c
some partial_function examples

diff -r dbab949c2717 -r 80b7f456600f src/HOL/ex/Fundefs.thy
--- a/src/HOL/ex/Fundefs.thy	Sat Oct 23 23:42:04 2010 +0200
+++ b/src/HOL/ex/Fundefs.thy	Mon Oct 25 10:45:22 2010 +0200
@@ -5,7 +5,7 @@
 header {* Examples of function definitions *}
 
 theory Fundefs 
-imports Main
+imports Parity Monad_Syntax
 begin
 
 subsection {* Very basic *}
@@ -208,6 +208,31 @@
 thm my_monoid.foldL.simps
 thm my_monoid.foldR_foldL
 
+
+subsection {* Partial Function Definitions *}
+
+text {* Partial functions in the option monad: *}
+
+partial_function (option)
+  collatz :: "nat \<Rightarrow> nat list option"
+where
+  "collatz n =
+  (if n \<le> 1 then Some [n]
+   else if even n 
+     then do { ns \<leftarrow> collatz (n div 2); Some (n # ns) }
+     else do { ns \<leftarrow> collatz (3 * n + 1);  Some (n # ns)})"
+
+declare collatz.rec[code]
+value "collatz 23"
+
+
+text {* Tail-recursive functions: *}
+
+partial_function (tailrec) fixpoint :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
+where
+  "fixpoint f x = (if f x = x then x else fixpoint f (f x))"
+
+
 subsection {* Regression tests *}
 
 text {* The following examples mainly serve as tests for the