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