62696
|
1 |
(* Title: HOL/Corec_Examples/Tests/Small_Concrete.thy
|
|
2 |
Author: Aymeric Bouzy, Ecole polytechnique
|
|
3 |
Author: Jasmin Blanchette, Inria, LORIA, MPII
|
|
4 |
Copyright 2015, 2016
|
|
5 |
|
|
6 |
Small concrete examples.
|
|
7 |
*)
|
|
8 |
|
62726
|
9 |
section \<open>Small Concrete Examples\<close>
|
62696
|
10 |
|
|
11 |
theory Small_Concrete
|
|
12 |
imports "~~/src/HOL/Library/BNF_Corec"
|
|
13 |
begin
|
|
14 |
|
62726
|
15 |
subsection \<open>Streams of Natural Numbers\<close>
|
62696
|
16 |
|
|
17 |
codatatype natstream = S (head: nat) (tail: natstream)
|
|
18 |
|
|
19 |
corec (friend) incr_all where
|
|
20 |
"incr_all s = S (head s + 1) (incr_all (tail s))"
|
|
21 |
|
|
22 |
corec all_numbers where
|
|
23 |
"all_numbers = S 0 (incr_all all_numbers)"
|
|
24 |
|
|
25 |
corec all_numbers_efficient where
|
|
26 |
"all_numbers_efficient n = S n (all_numbers_efficient (n + 1))"
|
|
27 |
|
|
28 |
corec remove_multiples where
|
|
29 |
"remove_multiples n s =
|
|
30 |
(if (head s) mod n = 0 then
|
|
31 |
S (head (tail s)) (remove_multiples n (tail (tail s)))
|
|
32 |
else
|
|
33 |
S (head s) (remove_multiples n (tail s)))"
|
|
34 |
|
|
35 |
corec prime_numbers where
|
|
36 |
"prime_numbers known_primes =
|
|
37 |
(let next_prime = head (fold (%n s. remove_multiples n s) known_primes (tail (tail all_numbers))) in
|
|
38 |
S next_prime (prime_numbers (next_prime # known_primes)))"
|
|
39 |
|
|
40 |
term "prime_numbers []"
|
|
41 |
|
|
42 |
corec prime_numbers_more_efficient where
|
|
43 |
"prime_numbers_more_efficient n remaining_numbers =
|
|
44 |
(let remaining_numbers = remove_multiples n remaining_numbers in
|
|
45 |
S (head remaining_numbers) (prime_numbers_more_efficient (head remaining_numbers) remaining_numbers))"
|
|
46 |
|
|
47 |
term "prime_numbers_more_efficient 0 (tail (tail all_numbers))"
|
|
48 |
|
|
49 |
corec (friend) alternate where
|
|
50 |
"alternate s1 s2 = S (head s1) (S (head s2) (alternate (tail s1) (tail s2)))"
|
|
51 |
|
|
52 |
corec (friend) all_sums where
|
|
53 |
"all_sums s1 s2 = S (head s1 + head s2) (alternate (all_sums s1 (tail s2)) (all_sums (tail s1) s2))"
|
|
54 |
|
|
55 |
corec app_list where
|
|
56 |
"app_list s l = (case l of
|
|
57 |
[] \<Rightarrow> s
|
|
58 |
| a # r \<Rightarrow> S a (app_list s r))"
|
|
59 |
|
|
60 |
friend_of_corec app_list where
|
|
61 |
"app_list s l = (case l of
|
|
62 |
[] \<Rightarrow> (case s of S a b \<Rightarrow> S a b)
|
|
63 |
| a # r \<Rightarrow> S a (app_list s r))"
|
|
64 |
sorry
|
|
65 |
|
|
66 |
corec expand_with where
|
|
67 |
"expand_with f s = (let l = f (head s) in S (hd l) (app_list (expand_with f (tail s)) (tl l)))"
|
|
68 |
|
|
69 |
friend_of_corec expand_with where
|
|
70 |
"expand_with f s = (let l = f (head s) in S (hd l) (app_list (expand_with f (tail s)) (tl l)))"
|
|
71 |
sorry
|
|
72 |
|
|
73 |
corec iterations where
|
|
74 |
"iterations f a = S a (iterations f (f a))"
|
|
75 |
|
|
76 |
corec exponential_iterations where
|
|
77 |
"exponential_iterations f a = S (f a) (exponential_iterations (f o f) a)"
|
|
78 |
|
|
79 |
corec (friend) alternate_list where
|
|
80 |
"alternate_list l = (let heads = (map head l) in S (hd heads) (app_list (alternate_list (map tail l)) (tl heads)))"
|
|
81 |
|
|
82 |
corec switch_one_two0 where
|
|
83 |
"switch_one_two0 f a s = (case s of
|
|
84 |
S b r \<Rightarrow> S b (S a (f r)))"
|
|
85 |
|
|
86 |
corec switch_one_two where
|
|
87 |
"switch_one_two s = (case s of
|
|
88 |
S a (S b r) \<Rightarrow> S b (S a (switch_one_two r)))"
|
|
89 |
|
|
90 |
corec fibonacci where
|
|
91 |
"fibonacci n m = S m (fibonacci (n + m) n)"
|
|
92 |
|
|
93 |
corec sequence2 where
|
|
94 |
"sequence2 f u1 u0 = S u0 (sequence2 f (f u1 u0) u1)"
|
|
95 |
|
|
96 |
corec (friend) alternate_with_function where
|
|
97 |
"alternate_with_function f s =
|
|
98 |
(let f_head_s = f (head s) in S (head f_head_s) (alternate (tail f_head_s) (alternate_with_function f (tail s))))"
|
|
99 |
|
|
100 |
corec h where
|
|
101 |
"h l s = (case l of
|
|
102 |
[] \<Rightarrow> s
|
|
103 |
| (S a s') # r \<Rightarrow> S a (alternate s (h r s')))"
|
|
104 |
|
|
105 |
friend_of_corec h where
|
|
106 |
"h l s = (case l of
|
|
107 |
[] \<Rightarrow> (case s of S a b \<Rightarrow> S a b)
|
|
108 |
| (S a s') # r \<Rightarrow> S a (alternate s (h r s')))"
|
|
109 |
sorry
|
|
110 |
|
|
111 |
corec z where
|
|
112 |
"z = S 0 (S 0 z)"
|
|
113 |
|
|
114 |
lemma "\<And>x. x = S 0 (S 0 x) \<Longrightarrow> x = z"
|
|
115 |
apply corec_unique
|
|
116 |
apply (rule z.code)
|
|
117 |
done
|
|
118 |
|
|
119 |
corec enum where
|
|
120 |
"enum m = S m (enum (m + 1))"
|
|
121 |
|
|
122 |
lemma "(\<And>m. f m = S m (f (m + 1))) \<Longrightarrow> f m = enum m"
|
|
123 |
apply corec_unique
|
|
124 |
apply (rule enum.code)
|
|
125 |
done
|
|
126 |
|
|
127 |
lemma "(\<forall>m. f m = S m (f (m + 1))) \<Longrightarrow> f m = enum m"
|
|
128 |
apply corec_unique
|
|
129 |
apply (rule enum.code)
|
|
130 |
done
|
|
131 |
|
|
132 |
|
62726
|
133 |
subsection \<open>Lazy Lists of Natural Numbers\<close>
|
62696
|
134 |
|
|
135 |
codatatype llist = LNil | LCons nat llist
|
|
136 |
|
|
137 |
corec h1 where
|
|
138 |
"h1 x = (if x = 1 then
|
|
139 |
LNil
|
|
140 |
else
|
|
141 |
let x = if x mod 2 = 0 then x div 2 else 3 * x + 1 in
|
|
142 |
LCons x (h1 x))"
|
|
143 |
|
|
144 |
corec h3 where
|
|
145 |
"h3 s = (case s of
|
|
146 |
LNil \<Rightarrow> LNil
|
|
147 |
| LCons x r \<Rightarrow> LCons x (h3 r))"
|
|
148 |
|
62733
|
149 |
corec fold_map where
|
62696
|
150 |
"fold_map f a s = (let v = f a (head s) in S v (fold_map f v (tail s)))"
|
|
151 |
|
62733
|
152 |
friend_of_corec fold_map where
|
|
153 |
"fold_map f a s = (let v = f a (head s) in S v (fold_map f v (tail s)))"
|
|
154 |
apply (rule fold_map.code)
|
|
155 |
sorry
|
62696
|
156 |
|
62733
|
157 |
|
|
158 |
subsection \<open>Coinductive Natural Numbers\<close>
|
62696
|
159 |
|
|
160 |
codatatype conat = CoZero | CoSuc conat
|
|
161 |
|
|
162 |
corec sum where
|
|
163 |
"sum x y = (case x of
|
|
164 |
CoZero \<Rightarrow> y
|
|
165 |
| CoSuc x \<Rightarrow> CoSuc (sum x y))"
|
|
166 |
|
|
167 |
friend_of_corec sum where
|
|
168 |
"sum x y = (case x of
|
|
169 |
CoZero \<Rightarrow> (case y of CoZero \<Rightarrow> CoZero | CoSuc y \<Rightarrow> CoSuc y)
|
|
170 |
| CoSuc x \<Rightarrow> CoSuc (sum x y))"
|
|
171 |
sorry
|
|
172 |
|
|
173 |
corec (friend) prod where
|
|
174 |
"prod x y = (case (x, y) of
|
|
175 |
(CoZero, _) \<Rightarrow> CoZero
|
|
176 |
| (_, CoZero) \<Rightarrow> CoZero
|
|
177 |
| (CoSuc x, CoSuc y) \<Rightarrow> CoSuc (sum (prod x y) (sum x y)))"
|
|
178 |
|
|
179 |
end
|