# HG changeset patch
# User blanchet
# Date 1467839967 -7200
# Node ID 32866eff1843cd0f10d0128f922969efaf46ad3d
# Parent  9202173231471945d9b443e464c8346fe2cd16ad
updated examples

diff -r 920217323147 -r 32866eff1843 src/HOL/Corec_Examples/Paper_Examples.thy
--- a/src/HOL/Corec_Examples/Paper_Examples.thy	Wed Jul 06 22:52:10 2016 +0200
+++ b/src/HOL/Corec_Examples/Paper_Examples.thy	Wed Jul 06 23:19:27 2016 +0200
@@ -3,51 +3,114 @@
     Author:     Andrei Popescu, TU Muenchen
     Copyright   2016
 
-Small examples from the paper.
+Small examples from the paper "Friends with Benefits".
 *)
 
-section \<open>Small Examples from the Paper\<close>
+section \<open>Small Examples from the Paper ``Friends with Benefits''\<close>
 
 theory Paper_Examples
-imports "~~/src/HOL/Library/BNF_Corec"
+imports "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/FSet" "Complex_Main"
 begin
 
-subsection \<open>Examples from the introduction\<close>
+section \<open>Examples from the introduction\<close>
 
-codatatype 'a stream = SCons (hd: 'a) (tl: "'a stream") (infixr "\<lhd>" 65)
+codatatype 'a stream = SCons (shd: 'a) (stl: "'a stream") (infixr "\<lhd>" 65)
 
-corec "from" :: "nat \<Rightarrow> nat stream" where
-  "from n = n \<lhd> from (n + 1)"
+corec "natsFrom" :: "nat \<Rightarrow> nat stream" where
+  "natsFrom n = n \<lhd> natsFrom (n + 1)"
 
-corec (friend) addOne :: "nat stream \<Rightarrow> nat stream" where
-  "addOne n = (hd n + 1) \<lhd> addOne (tl n)"
+corec (friend) addOne :: "nat stream \<Rightarrow> nat stream"
+where "addOne n = (shd n + 1) \<lhd> addOne (stl n)"
 
-corec from' :: "nat \<Rightarrow> nat stream" where
-  "from' n = n \<lhd> addOne (from' n)"
+corec natsFrom' :: "nat \<Rightarrow> nat stream" where
+  "natsFrom' n = n \<lhd> addOne (natsFrom' n)"
 
 
-subsection \<open>Examples from Section 5\<close>
+section \<open>Examples from section 3\<close>
 
-text \<open>
-We curry the example functions in this section because infix syntax works only for curried
-functions.
-\<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"
+  "x\<^sub>1 \<oplus> x\<^sub>2 = (shd x\<^sub>1 + shd x\<^sub>2) \<lhd> (stl x\<^sub>1 \<oplus> stl x\<^sub>2)"
 
-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)))"
+section \<open>Examples from section 4\<close>
 
 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))"
 
+datatype 'a nelist = NEList (hd:'a) (tl:"'a list")
+
+primrec (transfer) postpend :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a nelist" (infix "\<rhd>" 64) where
+ "[] \<rhd> a = NEList a []"
+|"(b # bs) \<rhd> a = NEList b (bs @ [a])"
+
+corec (friend) inter :: "nat stream nelist \<Rightarrow> nat stream" where
+"inter x = shd (hd x) \<lhd> inter (tl x \<rhd> stl (hd x))"
+
+corec (friend) inter2 :: "nat stream nelist \<Rightarrow> nat stream" where
+"inter2 x = (case hd x of n \<lhd> y \<Rightarrow> n \<lhd> inter2 (tl x \<rhd> y))"
+
+corec zero :: "nat stream" where "zero = 0 \<lhd> zero"
+
+corec (friend) inter3 :: "nat stream nelist \<Rightarrow> nat stream" where
+"inter3 x = shd (stl zero) \<lhd> inter3 ([hd x] \<rhd> stl (hd x))"
+
+
+section \<open>Examples from Blanchette et al. (ICFP 2015)\<close>
+
+corec oneTwos :: "nat stream" where "oneTwos = 1 \<lhd> 2 \<lhd> oneTwos"
+
+corec everyOther :: "'a stream \<Rightarrow> 'a stream"
+where "everyOther xs = shd xs \<lhd> everyOther (stl (stl xs))"
+
+corec fibA :: "nat stream"
+where "fibA = 0 \<lhd> (1 \<lhd> fibA \<oplus> fibA)"
+
+corec fibB :: "nat stream"
+where "fibB = (0 \<lhd> 1 \<lhd> fibB) \<oplus> (0 \<lhd> fibB)"
+
+corec (friend) times :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infix "\<otimes>" 69)
+where "xs \<otimes> ys = (shd xs * shd ys) \<lhd> xs \<otimes> stl ys \<oplus> stl xs \<otimes> ys"
+
+corec (friend) exp :: "nat stream \<Rightarrow> nat stream"
+where "exp xs = 2 ^ shd xs \<lhd> (stl xs \<otimes> exp xs)"
+
+corec facA :: "nat stream"
+where "facA = (1 \<lhd> facA) \<otimes> (1 \<lhd> facA)"
+
+corec facB :: "nat stream"
+where "facB = exp (0 \<lhd> facB)"
+
+corec (friend) sfsup :: "nat stream fset \<Rightarrow> nat stream"
+where "sfsup X = Sup (fset (fimage shd X)) \<lhd> sfsup (fimage stl X)"
+
+codatatype tree = Node (val: nat) (sub: "tree list")
+
+corec (friend) tplus :: "tree \<Rightarrow> tree \<Rightarrow> tree"
+where "tplus t u = Node (val t + val u) (map (\<lambda>(t', u'). tplus t' u') (zip (sub t) (sub u)))"
+
+corec (friend) ttimes :: "tree \<Rightarrow> tree \<Rightarrow> tree"
+where "ttimes t u = Node (val t * val u) (map (\<lambda>(t , u ). tplus (ttimes t u ) (ttimes t u)) (zip (sub t) (sub u)))"
+
+corecursive primes :: "nat \<Rightarrow> nat \<Rightarrow> nat stream"
+where "primes m n =
+  (if (m = 0 \<and> n > 1) \<or> coprime m n then n \<lhd> primes (m * n) (n + 1) else primes m (n + 1))"
+apply (relation "measure (\<lambda>(m, n). if n = 0 then 1 else if coprime m n then 0 else m - n mod m)")
+apply (auto simp: mod_Suc intro: Suc_lessI )
+apply (metis One_nat_def coprime_Suc_nat gcd.commute gcd_red_nat)
+by (metis diff_less_mono2 lessI mod_less_divisor)
+
+corec facC :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat stream"
+where "facC n a i = (if i = 0 then a \<lhd> facC (n + 1) 1 (n + 1) else facC n (a * i) (i - 1))"
+
+corec catalan :: "nat \<Rightarrow> nat stream"
+where "catalan n = (if n > 0 then catalan (n - 1) \<oplus> (0 \<lhd> catalan (n + 1)) else 1 \<lhd> catalan 1)"
+
+corec (friend) heart :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infix "\<heartsuit>" 65)
+where "xs \<heartsuit> ys = SCons (shd xs * shd ys) ((((xs \<heartsuit> stl ys) \<oplus> (stl xs \<otimes> ys)) \<heartsuit> ys) \<otimes> ys)"
+
+corec (friend) g :: "'a stream \<Rightarrow> 'a stream"
+where "g xs = shd xs \<lhd> g (g (stl xs))"
+
 end