huffman@16554
|
1 |
(* Title: HOLCF/ex/Fixrec_ex.thy
|
huffman@16554
|
2 |
Author: Brian Huffman
|
huffman@16554
|
3 |
*)
|
huffman@16554
|
4 |
|
huffman@16554
|
5 |
header {* Fixrec package examples *}
|
huffman@16554
|
6 |
|
huffman@16554
|
7 |
theory Fixrec_ex
|
huffman@16554
|
8 |
imports HOLCF
|
huffman@16554
|
9 |
begin
|
huffman@16554
|
10 |
|
huffman@31008
|
11 |
subsection {* Basic @{text fixrec} examples *}
|
huffman@16554
|
12 |
|
huffman@16554
|
13 |
text {*
|
huffman@16554
|
14 |
Fixrec patterns can mention any constructor defined by the domain
|
huffman@16554
|
15 |
package, as well as any of the following built-in constructors:
|
huffman@35925
|
16 |
Pair, spair, sinl, sinr, up, ONE, TT, FF.
|
huffman@16554
|
17 |
*}
|
huffman@16554
|
18 |
|
huffman@31008
|
19 |
text {* Typical usage is with lazy constructors. *}
|
huffman@16554
|
20 |
|
huffman@30158
|
21 |
fixrec down :: "'a u \<rightarrow> 'a"
|
huffman@30158
|
22 |
where "down\<cdot>(up\<cdot>x) = x"
|
huffman@16554
|
23 |
|
huffman@31008
|
24 |
text {* With strict constructors, rewrite rules may require side conditions. *}
|
huffman@16554
|
25 |
|
huffman@30158
|
26 |
fixrec from_sinl :: "'a \<oplus> 'b \<rightarrow> 'a"
|
huffman@30158
|
27 |
where "x \<noteq> \<bottom> \<Longrightarrow> from_sinl\<cdot>(sinl\<cdot>x) = x"
|
huffman@16554
|
28 |
|
huffman@31008
|
29 |
text {* Lifting can turn a strict constructor into a lazy one. *}
|
huffman@16554
|
30 |
|
huffman@30158
|
31 |
fixrec from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a"
|
huffman@30158
|
32 |
where "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x"
|
huffman@16554
|
33 |
|
huffman@33401
|
34 |
text {* Fixrec also works with the HOL pair constructor. *}
|
huffman@33401
|
35 |
|
huffman@33401
|
36 |
fixrec down2 :: "'a u \<times> 'b u \<rightarrow> 'a \<times> 'b"
|
huffman@33401
|
37 |
where "down2\<cdot>(up\<cdot>x, up\<cdot>y) = (x, y)"
|
huffman@33401
|
38 |
|
huffman@16554
|
39 |
|
huffman@33417
|
40 |
subsection {* Examples using @{text fixrec_simp} *}
|
huffman@16554
|
41 |
|
huffman@31008
|
42 |
text {* A type of lazy lists. *}
|
huffman@16554
|
43 |
|
huffman@16554
|
44 |
domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist")
|
huffman@16554
|
45 |
|
huffman@31008
|
46 |
text {* A zip function for lazy lists. *}
|
huffman@16554
|
47 |
|
huffman@31008
|
48 |
text {* Notice that the patterns are not exhaustive. *}
|
huffman@16554
|
49 |
|
huffman@16554
|
50 |
fixrec
|
huffman@30158
|
51 |
lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
|
huffman@30158
|
52 |
where
|
huffman@35925
|
53 |
"lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
|
huffman@30158
|
54 |
| "lzip\<cdot>lNil\<cdot>lNil = lNil"
|
huffman@16554
|
55 |
|
huffman@33417
|
56 |
text {* @{text fixrec_simp} is useful for producing strictness theorems. *}
|
huffman@31008
|
57 |
text {* Note that pattern matching is done in left-to-right order. *}
|
huffman@16554
|
58 |
|
huffman@33417
|
59 |
lemma lzip_stricts [simp]:
|
huffman@33417
|
60 |
"lzip\<cdot>\<bottom>\<cdot>ys = \<bottom>"
|
huffman@33417
|
61 |
"lzip\<cdot>lNil\<cdot>\<bottom> = \<bottom>"
|
huffman@33417
|
62 |
"lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
|
huffman@33417
|
63 |
by fixrec_simp+
|
huffman@16554
|
64 |
|
huffman@33417
|
65 |
text {* @{text fixrec_simp} can also produce rules for missing cases. *}
|
huffman@16554
|
66 |
|
huffman@33417
|
67 |
lemma lzip_undefs [simp]:
|
huffman@33417
|
68 |
"lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = \<bottom>"
|
huffman@33417
|
69 |
"lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = \<bottom>"
|
huffman@33417
|
70 |
by fixrec_simp+
|
huffman@16554
|
71 |
|
huffman@16554
|
72 |
|
huffman@31008
|
73 |
subsection {* Pattern matching with bottoms *}
|
huffman@16554
|
74 |
|
huffman@31008
|
75 |
text {*
|
huffman@33417
|
76 |
As an alternative to using @{text fixrec_simp}, it is also possible
|
huffman@33417
|
77 |
to use bottom as a constructor pattern. When using a bottom
|
huffman@33417
|
78 |
pattern, the right-hand-side must also be bottom; otherwise, @{text
|
huffman@33417
|
79 |
fixrec} will not be able to prove the equation.
|
huffman@31008
|
80 |
*}
|
huffman@31008
|
81 |
|
huffman@31008
|
82 |
fixrec
|
huffman@31008
|
83 |
from_sinr_up :: "'a \<oplus> 'b\<^sub>\<bottom> \<rightarrow> 'b"
|
huffman@31008
|
84 |
where
|
huffman@31008
|
85 |
"from_sinr_up\<cdot>\<bottom> = \<bottom>"
|
huffman@31008
|
86 |
| "from_sinr_up\<cdot>(sinr\<cdot>(up\<cdot>x)) = x"
|
huffman@31008
|
87 |
|
huffman@31008
|
88 |
text {*
|
huffman@31008
|
89 |
If the function is already strict in that argument, then the bottom
|
huffman@31008
|
90 |
pattern does not change the meaning of the function. For example,
|
huffman@31008
|
91 |
in the definition of @{term from_sinr_up}, the first equation is
|
huffman@31008
|
92 |
actually redundant, and could have been proven separately by
|
huffman@33417
|
93 |
@{text fixrec_simp}.
|
huffman@31008
|
94 |
*}
|
huffman@31008
|
95 |
|
huffman@31008
|
96 |
text {*
|
huffman@31008
|
97 |
A bottom pattern can also be used to make a function strict in a
|
huffman@31008
|
98 |
certain argument, similar to a bang-pattern in Haskell.
|
huffman@31008
|
99 |
*}
|
huffman@31008
|
100 |
|
huffman@31008
|
101 |
fixrec
|
huffman@31008
|
102 |
seq :: "'a \<rightarrow> 'b \<rightarrow> 'b"
|
huffman@31008
|
103 |
where
|
huffman@31008
|
104 |
"seq\<cdot>\<bottom>\<cdot>y = \<bottom>"
|
huffman@31008
|
105 |
| "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x\<cdot>y = y"
|
huffman@31008
|
106 |
|
huffman@31008
|
107 |
|
huffman@31008
|
108 |
subsection {* Skipping proofs of rewrite rules *}
|
huffman@31008
|
109 |
|
huffman@31008
|
110 |
text {* Another zip function for lazy lists. *}
|
huffman@16554
|
111 |
|
huffman@16554
|
112 |
text {*
|
huffman@16554
|
113 |
Notice that this version has overlapping patterns.
|
huffman@16554
|
114 |
The second equation cannot be proved as a theorem
|
huffman@16554
|
115 |
because it only applies when the first pattern fails.
|
huffman@16554
|
116 |
*}
|
huffman@16554
|
117 |
|
huffman@16554
|
118 |
fixrec (permissive)
|
huffman@30158
|
119 |
lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
|
huffman@30158
|
120 |
where
|
huffman@35925
|
121 |
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
|
huffman@30158
|
122 |
| "lzip2\<cdot>xs\<cdot>ys = lNil"
|
huffman@16554
|
123 |
|
huffman@16554
|
124 |
text {*
|
huffman@16554
|
125 |
Usually fixrec tries to prove all equations as theorems.
|
huffman@16554
|
126 |
The "permissive" option overrides this behavior, so fixrec
|
huffman@16554
|
127 |
does not produce any simp rules.
|
huffman@16554
|
128 |
*}
|
huffman@16554
|
129 |
|
huffman@33417
|
130 |
text {* Simp rules can be generated later using @{text fixrec_simp}. *}
|
huffman@16554
|
131 |
|
huffman@33417
|
132 |
lemma lzip2_simps [simp]:
|
huffman@35925
|
133 |
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
|
huffman@33417
|
134 |
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = lNil"
|
huffman@33417
|
135 |
"lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = lNil"
|
huffman@33417
|
136 |
"lzip2\<cdot>lNil\<cdot>lNil = lNil"
|
huffman@33417
|
137 |
by fixrec_simp+
|
huffman@16554
|
138 |
|
huffman@33417
|
139 |
lemma lzip2_stricts [simp]:
|
huffman@33417
|
140 |
"lzip2\<cdot>\<bottom>\<cdot>ys = \<bottom>"
|
huffman@33417
|
141 |
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
|
huffman@33417
|
142 |
by fixrec_simp+
|
huffman@16554
|
143 |
|
huffman@16554
|
144 |
|
huffman@31008
|
145 |
subsection {* Mutual recursion with @{text fixrec} *}
|
huffman@31008
|
146 |
|
huffman@31008
|
147 |
text {* Tree and forest types. *}
|
huffman@16554
|
148 |
|
huffman@16554
|
149 |
domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest")
|
huffman@16554
|
150 |
and 'a forest = Empty | Trees (lazy "'a tree") "'a forest"
|
huffman@16554
|
151 |
|
huffman@16554
|
152 |
text {*
|
huffman@35770
|
153 |
To define mutually recursive functions, give multiple type signatures
|
huffman@35770
|
154 |
separated by the keyword @{text "and"}.
|
huffman@16554
|
155 |
*}
|
huffman@16554
|
156 |
|
huffman@16554
|
157 |
fixrec
|
huffman@30158
|
158 |
map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)"
|
huffman@30158
|
159 |
and
|
huffman@30158
|
160 |
map_forest :: "('a \<rightarrow> 'b) \<rightarrow> ('a forest \<rightarrow> 'b forest)"
|
huffman@30158
|
161 |
where
|
huffman@16554
|
162 |
"map_tree\<cdot>f\<cdot>(Leaf\<cdot>x) = Leaf\<cdot>(f\<cdot>x)"
|
huffman@30158
|
163 |
| "map_tree\<cdot>f\<cdot>(Branch\<cdot>ts) = Branch\<cdot>(map_forest\<cdot>f\<cdot>ts)"
|
huffman@30158
|
164 |
| "map_forest\<cdot>f\<cdot>Empty = Empty"
|
huffman@30158
|
165 |
| "ts \<noteq> \<bottom> \<Longrightarrow>
|
huffman@16554
|
166 |
map_forest\<cdot>f\<cdot>(Trees\<cdot>t\<cdot>ts) = Trees\<cdot>(map_tree\<cdot>f\<cdot>t)\<cdot>(map_forest\<cdot>f\<cdot>ts)"
|
huffman@16554
|
167 |
|
huffman@33417
|
168 |
lemma map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom> = \<bottom>"
|
huffman@33417
|
169 |
by fixrec_simp
|
huffman@33417
|
170 |
|
huffman@33417
|
171 |
lemma map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom> = \<bottom>"
|
huffman@33417
|
172 |
by fixrec_simp
|
huffman@16554
|
173 |
|
huffman@16554
|
174 |
text {*
|
huffman@16554
|
175 |
Theorems generated:
|
huffman@35770
|
176 |
@{text map_tree_def} @{thm map_tree_def}
|
huffman@35770
|
177 |
@{text map_forest_def} @{thm map_forest_def}
|
huffman@35770
|
178 |
@{text map_tree.unfold} @{thm map_tree.unfold}
|
huffman@35770
|
179 |
@{text map_forest.unfold} @{thm map_forest.unfold}
|
huffman@35770
|
180 |
@{text map_tree.simps} @{thm map_tree.simps}
|
huffman@35770
|
181 |
@{text map_forest.simps} @{thm map_forest.simps}
|
huffman@35770
|
182 |
@{text map_tree_map_forest.induct} @{thm map_tree_map_forest.induct}
|
huffman@16554
|
183 |
*}
|
huffman@16554
|
184 |
|
huffman@35770
|
185 |
|
huffman@36988
|
186 |
subsection {* Looping simp rules *}
|
huffman@36988
|
187 |
|
huffman@36988
|
188 |
text {*
|
huffman@36988
|
189 |
The defining equations of a fixrec definition are declared as simp
|
huffman@36988
|
190 |
rules by default. In some cases, especially for constants with no
|
huffman@36988
|
191 |
arguments or functions with variable patterns, the defining
|
huffman@36988
|
192 |
equations may cause the simplifier to loop. In these cases it will
|
huffman@36988
|
193 |
be necessary to use a @{text "[simp del]"} declaration.
|
huffman@36988
|
194 |
*}
|
huffman@36988
|
195 |
|
huffman@36988
|
196 |
fixrec
|
huffman@36988
|
197 |
repeat :: "'a \<rightarrow> 'a llist"
|
huffman@36988
|
198 |
where
|
huffman@36988
|
199 |
[simp del]: "repeat\<cdot>x = lCons\<cdot>x\<cdot>(repeat\<cdot>x)"
|
huffman@36988
|
200 |
|
huffman@36988
|
201 |
text {*
|
huffman@36988
|
202 |
We can derive other non-looping simp rules for @{const repeat} by
|
huffman@36988
|
203 |
using the @{text subst} method with the @{text repeat.simps} rule.
|
huffman@36988
|
204 |
*}
|
huffman@36988
|
205 |
|
huffman@36988
|
206 |
lemma repeat_simps [simp]:
|
huffman@36988
|
207 |
"repeat\<cdot>x \<noteq> \<bottom>"
|
huffman@36988
|
208 |
"repeat\<cdot>x \<noteq> lNil"
|
huffman@36988
|
209 |
"repeat\<cdot>x = lCons\<cdot>y\<cdot>ys \<longleftrightarrow> x = y \<and> repeat\<cdot>x = ys"
|
huffman@36988
|
210 |
by (subst repeat.simps, simp)+
|
huffman@36988
|
211 |
|
huffman@36988
|
212 |
lemma llist_when_repeat [simp]:
|
huffman@36988
|
213 |
"llist_when\<cdot>z\<cdot>f\<cdot>(repeat\<cdot>x) = f\<cdot>x\<cdot>(repeat\<cdot>x)"
|
huffman@36988
|
214 |
by (subst repeat.simps, simp)
|
huffman@36988
|
215 |
|
huffman@36988
|
216 |
text {*
|
huffman@36988
|
217 |
For mutually-recursive constants, looping might only occur if all
|
huffman@36988
|
218 |
equations are in the simpset at the same time. In such cases it may
|
huffman@36988
|
219 |
only be necessary to declare @{text "[simp del]"} on one equation.
|
huffman@36988
|
220 |
*}
|
huffman@36988
|
221 |
|
huffman@36988
|
222 |
fixrec
|
huffman@36988
|
223 |
inf_tree :: "'a tree" and inf_forest :: "'a forest"
|
huffman@36988
|
224 |
where
|
huffman@36988
|
225 |
[simp del]: "inf_tree = Branch\<cdot>inf_forest"
|
huffman@36988
|
226 |
| "inf_forest = Trees\<cdot>inf_tree\<cdot>(Trees\<cdot>inf_tree\<cdot>Empty)"
|
huffman@36988
|
227 |
|
huffman@36988
|
228 |
|
huffman@35770
|
229 |
subsection {* Using @{text fixrec} inside locales *}
|
huffman@35770
|
230 |
|
huffman@35770
|
231 |
locale test =
|
huffman@35770
|
232 |
fixes foo :: "'a \<rightarrow> 'a"
|
huffman@35770
|
233 |
assumes foo_strict: "foo\<cdot>\<bottom> = \<bottom>"
|
huffman@35770
|
234 |
begin
|
huffman@35770
|
235 |
|
huffman@35770
|
236 |
fixrec
|
huffman@35770
|
237 |
bar :: "'a u \<rightarrow> 'a"
|
huffman@35770
|
238 |
where
|
huffman@35770
|
239 |
"bar\<cdot>(up\<cdot>x) = foo\<cdot>x"
|
huffman@35770
|
240 |
|
huffman@35770
|
241 |
lemma bar_strict: "bar\<cdot>\<bottom> = \<bottom>"
|
huffman@35770
|
242 |
by fixrec_simp
|
huffman@35770
|
243 |
|
huffman@16554
|
244 |
end
|
huffman@35770
|
245 |
|
huffman@35770
|
246 |
end
|