1(* Title: HOL/Corec_Examples/Tests/Stream_Friends.thy 2 Author: Aymeric Bouzy, Ecole polytechnique 3 Author: Jasmin Blanchette, Inria, LORIA, MPII 4 Copyright 2015, 2016 5 6Friendly functions on streams. 7*) 8 9section \<open>Friendly Functions on Streams\<close> 10 11theory Stream_Friends 12imports "HOL-Library.BNF_Corec" 13begin 14 15codatatype 'a stream = SCons (shd: 'a) (stl: "'a stream") 16 17corec pls :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" where 18 "pls s s' = SCons (shd s + shd s') (pls (stl s) (stl s'))" 19 20friend_of_corec pls :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" where 21 "pls s s' = SCons (shd s + shd s') (pls (stl s) (stl s'))" 22 sorry 23 24corec onetwo :: "nat stream" where 25 "onetwo = SCons 1 (SCons 2 onetwo)" 26 27corec prd :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" where 28 "prd xs ys = SCons (shd xs * shd ys) (pls (prd xs (stl ys)) (prd (stl xs) ys))" 29 30friend_of_corec prd where 31 "prd xs ys = SCons (shd xs * shd ys) (pls (prd xs (stl ys)) (prd (stl xs) ys))" 32 sorry 33 34corec Exp :: "nat stream \<Rightarrow> nat stream" where 35 "Exp xs = SCons (2 ^^ shd xs) (prd (stl xs) (Exp xs))" 36 37friend_of_corec Exp where 38 "Exp xs = SCons (2 ^^ shd xs) (prd (stl xs) (Exp xs))" 39 sorry 40 41corec prd2 :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" where 42 "prd2 xs ys = SCons (shd xs * shd ys) (pls (prd xs (stl ys)) (prd2 (stl xs) ys))" 43 44fun sthe_default :: "'a stream \<Rightarrow> nat \<Rightarrow> 'a stream option \<Rightarrow> 'a stream" where 45 "sthe_default s _ None = s" 46| "sthe_default _ _ (Some t) = t" 47 48(* FIXME: 49friend_of_corec sthe_default where 50 "sthe_default s n opt = SCons (shd (case opt of None \<Rightarrow> s | Some t \<Rightarrow> t)) (stl (case opt of None \<Rightarrow> s | Some t \<Rightarrow> t))" 51 sorry 52 53corec funky0 :: "nat \<Rightarrow> nat stream" where 54 "funky0 n = SCons 0 (sthe_default undefined n (map_option funky0 undefined))" 55 56consts funky0' :: "nat stream \<Rightarrow> nat stream" 57 58friend_of_corec funky0' :: "nat stream \<Rightarrow> nat stream" where 59 "funky0' ns = SCons 0 (sthe_default undefined (shd ns) (map_option funky0' undefined))" 60 sorry 61 62corec funky :: "nat \<Rightarrow> nat stream" where 63 "funky n = SCons 0 (sthe_default (funky (n + 1)) n (map_option funky (Some (n + 2))))" 64 65corec funky' :: "nat \<Rightarrow> nat \<Rightarrow> nat stream" where 66 "funky' m n = SCons 0 (sthe_default (funky' (m - 1) (n + 1)) m (map_option (%(x, y). funky' (Suc x) (Suc y)) (Some (m - 2, n + 2))))" 67 68corec funky'' :: "nat \<Rightarrow> nat stream" where 69 "funky'' n = SCons 0 (sthe_default (funky'' (n + 1)) n (Some (funky'' (n + 2))))" 70 71corec phunky0 :: "nat \<Rightarrow> nat stream" where 72 "phunky0 n = sthe_default undefined n undefined" 73 74fun lthe_default :: "'a stream \<Rightarrow> 'a stream option \<Rightarrow> 'a stream" where 75 "lthe_default s None = s" 76| "lthe_default _ (Some t) = t" 77 78friend_of_corec lthe_default where 79 "lthe_default s opt = SCons (shd (case opt of None \<Rightarrow> s | Some t \<Rightarrow> t)) (stl (case opt of None \<Rightarrow> s | Some t \<Rightarrow> t))" 80 sorry 81 82corec phunky_debug :: "'a \<Rightarrow> 'a stream" where 83 "phunky_debug n = lthe_default (SCons n (lthe_default undefined (map_option phunky_debug undefined))) undefined" 84 85corec phunky1 :: "nat \<Rightarrow> nat stream" where 86 "phunky1 n = sthe_default (SCons 0 (sthe_default (phunky1 (n + 1)) n (map_option phunky1 (Some (n + 2))))) n undefined" 87 88corec phunky2 :: "nat \<Rightarrow> nat stream" where 89 "phunky2 n = sthe_default (SCons 0 (sthe_default (phunky2 (n + 1)) n (map_option phunky2 (Some (n + 2))))) n 90 (map_option (%m. SCons m (sthe_default (phunky2 (n + 1)) n (map_option phunky2 (Some (n + 2))))) (Some n))" 91 92corec phunky3 :: "nat \<Rightarrow> nat stream" where 93 "phunky3 n = sthe_default (SCons 0 (sthe_default (phunky3 (n + 1)) n (map_option phunky3 (Some (n + 3))))) n 94 (Some (SCons n (sthe_default (phunky3 (n + 1)) n (map_option phunky3 (Some (n + 3))))))" 95*) 96 97end 98