|
1 (* Title: HOL/Corec_Examples/Paper_Examples.thy |
|
2 Author: Andreas Lochbihler, ETH Zuerich |
|
3 Author: Andrei Popescu, TU Muenchen |
|
4 Copyright 2016 |
|
5 |
|
6 Small examples from the paper. |
|
7 *) |
|
8 |
|
9 section \<open>Small Examples from the Paper\<close> |
|
10 |
|
11 theory Paper_Examples |
|
12 imports "~~/src/HOL/Library/BNF_Corec" |
|
13 begin |
|
14 |
|
15 subsection \<open>Examples from the introduction\<close> |
|
16 |
|
17 codatatype 'a stream = SCons (hd: 'a) (tl: "'a stream") (infixr "\<lhd>" 65) |
|
18 |
|
19 corec "from" :: "nat \<Rightarrow> nat stream" where |
|
20 "from n = n \<lhd> from (n + 1)" |
|
21 |
|
22 corec (friend) addOne :: "nat stream \<Rightarrow> nat stream" where |
|
23 "addOne n = (hd n + 1) \<lhd> addOne (tl n)" |
|
24 |
|
25 corec from' :: "nat \<Rightarrow> nat stream" where |
|
26 "from' n = n \<lhd> addOne (from' n)" |
|
27 |
|
28 |
|
29 subsection \<open>Examples from Section 5\<close> |
|
30 |
|
31 text \<open> |
|
32 We curry the example functions in this section because infix syntax works only for curried |
|
33 functions. |
|
34 \<close> |
|
35 |
|
36 corec (friend) Plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infix "\<oplus>" 67) where |
|
37 "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)" |
|
38 |
|
39 corec zeros :: "nat stream" where "zeros = 0 \<lhd> zeros" |
|
40 |
|
41 corec (friend) Plus' :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infix "\<oplus>''" 67) where |
|
42 "x\<^sub>1 \<oplus>' x\<^sub>2 = hd x\<^sub>1 \<lhd> (tl (tl zeros) \<oplus>' x\<^sub>2)" |
|
43 |
|
44 corec (friend) heart :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infix "\<heartsuit>" 67) where |
|
45 "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)))))" |
|
46 |
|
47 corec spade :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infix "\<spadesuit>" 67) where |
|
48 "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)))" |
|
49 |
|
50 corec collatz :: "nat \<Rightarrow> nat stream" where |
|
51 "collatz n = (if even n \<and> n > 0 then collatz (n div 2) else n \<lhd> collatz (3 * n + 1))" |
|
52 |
|
53 end |