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 |
|
63406
|
6 |
Small examples from the paper "Friends with Benefits".
|
62734
|
7 |
*)
|
|
8 |
|
63406
|
9 |
section \<open>Small Examples from the Paper ``Friends with Benefits''\<close>
|
62734
|
10 |
|
|
11 |
theory Paper_Examples
|
65538
|
12 |
imports "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/FSet" Complex_Main
|
62734
|
13 |
begin
|
|
14 |
|
63406
|
15 |
section \<open>Examples from the introduction\<close>
|
62734
|
16 |
|
63406
|
17 |
codatatype 'a stream = SCons (shd: 'a) (stl: "'a stream") (infixr "\<lhd>" 65)
|
62734
|
18 |
|
63406
|
19 |
corec "natsFrom" :: "nat \<Rightarrow> nat stream" where
|
|
20 |
"natsFrom n = n \<lhd> natsFrom (n + 1)"
|
62734
|
21 |
|
63408
|
22 |
corec (friend) add1 :: "nat stream \<Rightarrow> nat stream"
|
63468
|
23 |
where "add1 ns = (shd ns + 1) \<lhd> add1 (stl ns)"
|
62734
|
24 |
|
63406
|
25 |
corec natsFrom' :: "nat \<Rightarrow> nat stream" where
|
63408
|
26 |
"natsFrom' n = n \<lhd> add1 (natsFrom' n)"
|
62734
|
27 |
|
63406
|
28 |
section \<open>Examples from section 3\<close>
|
62734
|
29 |
|
63406
|
30 |
text \<open>We curry the example functions in this section because infix syntax works only for curried functions.\<close>
|
62734
|
31 |
|
|
32 |
corec (friend) Plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infix "\<oplus>" 67) where
|
63406
|
33 |
"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)"
|
62734
|
34 |
|
63406
|
35 |
section \<open>Examples from section 4\<close>
|
62734
|
36 |
|
63408
|
37 |
codatatype 'a llist = LNil | LCons 'a "'a llist"
|
|
38 |
|
|
39 |
corec collatz :: "nat \<Rightarrow> nat llist" where
|
|
40 |
"collatz n = (if n \<le> 1 then LNil
|
|
41 |
else if even n then collatz (n div 2)
|
|
42 |
else LCons n (collatz (3 * n + 1)))"
|
62734
|
43 |
|
63406
|
44 |
datatype 'a nelist = NEList (hd:'a) (tl:"'a list")
|
|
45 |
|
63408
|
46 |
primrec (transfer) snoc :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a nelist" (infix "\<rhd>" 64) where
|
63406
|
47 |
"[] \<rhd> a = NEList a []"
|
|
48 |
|"(b # bs) \<rhd> a = NEList b (bs @ [a])"
|
|
49 |
|
|
50 |
corec (friend) inter :: "nat stream nelist \<Rightarrow> nat stream" where
|
63408
|
51 |
"inter xss = shd (hd xss) \<lhd> inter (tl xss \<rhd> stl (hd xss))"
|
63406
|
52 |
|
63408
|
53 |
corec (friend) inter' :: "nat stream nelist \<Rightarrow> nat stream" where
|
|
54 |
"inter' xss = (case hd xss of x \<lhd> xs \<Rightarrow> x \<lhd> inter' (tl xss \<rhd> xs))"
|
63406
|
55 |
|
|
56 |
corec zero :: "nat stream" where "zero = 0 \<lhd> zero"
|
|
57 |
|
|
58 |
section \<open>Examples from Blanchette et al. (ICFP 2015)\<close>
|
|
59 |
|
|
60 |
corec oneTwos :: "nat stream" where "oneTwos = 1 \<lhd> 2 \<lhd> oneTwos"
|
|
61 |
|
|
62 |
corec everyOther :: "'a stream \<Rightarrow> 'a stream"
|
|
63 |
where "everyOther xs = shd xs \<lhd> everyOther (stl (stl xs))"
|
|
64 |
|
|
65 |
corec fibA :: "nat stream"
|
|
66 |
where "fibA = 0 \<lhd> (1 \<lhd> fibA \<oplus> fibA)"
|
|
67 |
|
|
68 |
corec fibB :: "nat stream"
|
|
69 |
where "fibB = (0 \<lhd> 1 \<lhd> fibB) \<oplus> (0 \<lhd> fibB)"
|
|
70 |
|
|
71 |
corec (friend) times :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infix "\<otimes>" 69)
|
|
72 |
where "xs \<otimes> ys = (shd xs * shd ys) \<lhd> xs \<otimes> stl ys \<oplus> stl xs \<otimes> ys"
|
|
73 |
|
|
74 |
corec (friend) exp :: "nat stream \<Rightarrow> nat stream"
|
|
75 |
where "exp xs = 2 ^ shd xs \<lhd> (stl xs \<otimes> exp xs)"
|
|
76 |
|
|
77 |
corec facA :: "nat stream"
|
|
78 |
where "facA = (1 \<lhd> facA) \<otimes> (1 \<lhd> facA)"
|
|
79 |
|
|
80 |
corec facB :: "nat stream"
|
|
81 |
where "facB = exp (0 \<lhd> facB)"
|
|
82 |
|
|
83 |
corec (friend) sfsup :: "nat stream fset \<Rightarrow> nat stream"
|
|
84 |
where "sfsup X = Sup (fset (fimage shd X)) \<lhd> sfsup (fimage stl X)"
|
|
85 |
|
|
86 |
codatatype tree = Node (val: nat) (sub: "tree list")
|
|
87 |
|
|
88 |
corec (friend) tplus :: "tree \<Rightarrow> tree \<Rightarrow> tree"
|
|
89 |
where "tplus t u = Node (val t + val u) (map (\<lambda>(t', u'). tplus t' u') (zip (sub t) (sub u)))"
|
|
90 |
|
|
91 |
corec (friend) ttimes :: "tree \<Rightarrow> tree \<Rightarrow> tree"
|
63408
|
92 |
where "ttimes t u = Node (val t * val u)
|
|
93 |
(map (\<lambda>(t, u). tplus (ttimes t u) (ttimes t u)) (zip (sub t) (sub u)))"
|
63406
|
94 |
|
|
95 |
corecursive primes :: "nat \<Rightarrow> nat \<Rightarrow> nat stream"
|
|
96 |
where "primes m n =
|
|
97 |
(if (m = 0 \<and> n > 1) \<or> coprime m n then n \<lhd> primes (m * n) (n + 1) else primes m (n + 1))"
|
|
98 |
apply (relation "measure (\<lambda>(m, n). if n = 0 then 1 else if coprime m n then 0 else m - n mod m)")
|
|
99 |
apply (auto simp: mod_Suc intro: Suc_lessI )
|
|
100 |
apply (metis One_nat_def coprime_Suc_nat gcd.commute gcd_red_nat)
|
|
101 |
by (metis diff_less_mono2 lessI mod_less_divisor)
|
|
102 |
|
|
103 |
corec facC :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat stream"
|
|
104 |
where "facC n a i = (if i = 0 then a \<lhd> facC (n + 1) 1 (n + 1) else facC n (a * i) (i - 1))"
|
|
105 |
|
|
106 |
corec catalan :: "nat \<Rightarrow> nat stream"
|
|
107 |
where "catalan n = (if n > 0 then catalan (n - 1) \<oplus> (0 \<lhd> catalan (n + 1)) else 1 \<lhd> catalan 1)"
|
|
108 |
|
|
109 |
corec (friend) heart :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infix "\<heartsuit>" 65)
|
|
110 |
where "xs \<heartsuit> ys = SCons (shd xs * shd ys) ((((xs \<heartsuit> stl ys) \<oplus> (stl xs \<otimes> ys)) \<heartsuit> ys) \<otimes> ys)"
|
|
111 |
|
|
112 |
corec (friend) g :: "'a stream \<Rightarrow> 'a stream"
|
|
113 |
where "g xs = shd xs \<lhd> g (g (stl xs))"
|
|
114 |
|
62734
|
115 |
end
|