diff -r ebfc41a47641 -r 38fefd98c929 src/HOL/Corec_Examples/Paper_Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Corec_Examples/Paper_Examples.thy	Mon Mar 28 12:05:47 2016 +0200
@@ -0,0 +1,53 @@
+(*  Title:      HOL/Corec_Examples/Paper_Examples.thy
+    Author:     Andreas Lochbihler, ETH Zuerich
+    Author:     Andrei Popescu, TU Muenchen
+    Copyright   2016
+
+Small examples from the paper.
+*)
+
+section \<open>Small Examples from the Paper\<close>
+
+theory Paper_Examples
+imports "~~/src/HOL/Library/BNF_Corec"
+begin
+
+subsection \<open>Examples from the introduction\<close>
+
+codatatype 'a stream = SCons (hd: 'a) (tl: "'a stream") (infixr "\<lhd>" 65)
+
+corec "from" :: "nat \<Rightarrow> nat stream" where
+  "from n = n \<lhd> from (n + 1)"
+
+corec (friend) addOne :: "nat stream \<Rightarrow> nat stream" where
+  "addOne n = (hd n + 1) \<lhd> addOne (tl n)"
+
+corec from' :: "nat \<Rightarrow> nat stream" where
+  "from' n = n \<lhd> addOne (from' n)"
+
+
+subsection \<open>Examples from Section 5\<close>
+
+text \<open>
+We curry the example functions in this section because infix syntax works only for curried
+functions.
+\<close>
+
+corec (friend) Plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infix "\<oplus>" 67) where
+  "x\<^sub>1 \<oplus> x\<^sub>2 = (hd x\<^sub>1 + hd x\<^sub>2) \<lhd> (tl x\<^sub>1 \<oplus> tl x\<^sub>2)"
+
+corec zeros :: "nat stream" where "zeros = 0 \<lhd> zeros"
+
+corec (friend) Plus' :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infix "\<oplus>''" 67) where
+  "x\<^sub>1 \<oplus>' x\<^sub>2 = hd x\<^sub>1 \<lhd> (tl (tl zeros) \<oplus>' x\<^sub>2)"
+
+corec (friend) heart :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infix "\<heartsuit>" 67) where
+  "x\<^sub>1 \<heartsuit> x\<^sub>2 = (hd x\<^sub>1 * hd x\<^sub>2) \<lhd> (x\<^sub>2 \<heartsuit> ((x\<^sub>1 \<heartsuit> ((x\<^sub>1 \<heartsuit> tl x\<^sub>2) \<oplus> (tl x\<^sub>1 \<heartsuit> x\<^sub>2)))))"
+
+corec spade :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infix "\<spadesuit>" 67) where
+  "x\<^sub>1 \<spadesuit> x\<^sub>2 = (hd x\<^sub>1 \<lhd> (x\<^sub>1 \<spadesuit> x\<^sub>2)) \<oplus> (hd x\<^sub>1 \<lhd> ((x\<^sub>1 \<spadesuit> tl x\<^sub>2) \<oplus> (tl x\<^sub>1 \<spadesuit> x\<^sub>2)))"
+
+corec collatz :: "nat \<Rightarrow> nat stream" where
+  "collatz n = (if even n \<and> n > 0 then collatz (n div 2) else n \<lhd> collatz (3 * n + 1))"
+
+end