|
62734
|
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
|