1 (* Title: HOLCF/ex/Fixrec_ex.thy
5 header {* Fixrec package examples *}
11 subsection {* Basic @{text fixrec} examples *}
14 Fixrec patterns can mention any constructor defined by the domain
15 package, as well as any of the following built-in constructors:
16 Pair, spair, sinl, sinr, up, ONE, TT, FF.
19 text {* Typical usage is with lazy constructors. *}
21 fixrec down :: "'a u \<rightarrow> 'a"
22 where "down\<cdot>(up\<cdot>x) = x"
24 text {* With strict constructors, rewrite rules may require side conditions. *}
26 fixrec from_sinl :: "'a \<oplus> 'b \<rightarrow> 'a"
27 where "x \<noteq> \<bottom> \<Longrightarrow> from_sinl\<cdot>(sinl\<cdot>x) = x"
29 text {* Lifting can turn a strict constructor into a lazy one. *}
31 fixrec from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a"
32 where "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x"
34 text {* Fixrec also works with the HOL pair constructor. *}
36 fixrec down2 :: "'a u \<times> 'b u \<rightarrow> 'a \<times> 'b"
37 where "down2\<cdot>(up\<cdot>x, up\<cdot>y) = (x, y)"
40 subsection {* Examples using @{text fixrec_simp} *}
42 text {* A type of lazy lists. *}
44 domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist")
46 text {* A zip function for lazy lists. *}
48 text {* Notice that the patterns are not exhaustive. *}
51 lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
53 "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
54 | "lzip\<cdot>lNil\<cdot>lNil = lNil"
56 text {* @{text fixrec_simp} is useful for producing strictness theorems. *}
57 text {* Note that pattern matching is done in left-to-right order. *}
59 lemma lzip_stricts [simp]:
60 "lzip\<cdot>\<bottom>\<cdot>ys = \<bottom>"
61 "lzip\<cdot>lNil\<cdot>\<bottom> = \<bottom>"
62 "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
65 text {* @{text fixrec_simp} can also produce rules for missing cases. *}
67 lemma lzip_undefs [simp]:
68 "lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = \<bottom>"
69 "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = \<bottom>"
73 subsection {* Pattern matching with bottoms *}
76 As an alternative to using @{text fixrec_simp}, it is also possible
77 to use bottom as a constructor pattern. When using a bottom
78 pattern, the right-hand-side must also be bottom; otherwise, @{text
79 fixrec} will not be able to prove the equation.
83 from_sinr_up :: "'a \<oplus> 'b\<^sub>\<bottom> \<rightarrow> 'b"
85 "from_sinr_up\<cdot>\<bottom> = \<bottom>"
86 | "from_sinr_up\<cdot>(sinr\<cdot>(up\<cdot>x)) = x"
89 If the function is already strict in that argument, then the bottom
90 pattern does not change the meaning of the function. For example,
91 in the definition of @{term from_sinr_up}, the first equation is
92 actually redundant, and could have been proven separately by
97 A bottom pattern can also be used to make a function strict in a
98 certain argument, similar to a bang-pattern in Haskell.
102 seq :: "'a \<rightarrow> 'b \<rightarrow> 'b"
104 "seq\<cdot>\<bottom>\<cdot>y = \<bottom>"
105 | "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x\<cdot>y = y"
108 subsection {* Skipping proofs of rewrite rules *}
110 text {* Another zip function for lazy lists. *}
113 Notice that this version has overlapping patterns.
114 The second equation cannot be proved as a theorem
115 because it only applies when the first pattern fails.
119 lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
121 "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
122 | "lzip2\<cdot>xs\<cdot>ys = lNil"
125 Usually fixrec tries to prove all equations as theorems.
126 The "permissive" option overrides this behavior, so fixrec
127 does not produce any simp rules.
130 text {* Simp rules can be generated later using @{text fixrec_simp}. *}
132 lemma lzip2_simps [simp]:
133 "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
134 "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = lNil"
135 "lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = lNil"
136 "lzip2\<cdot>lNil\<cdot>lNil = lNil"
139 lemma lzip2_stricts [simp]:
140 "lzip2\<cdot>\<bottom>\<cdot>ys = \<bottom>"
141 "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
145 subsection {* Mutual recursion with @{text fixrec} *}
147 text {* Tree and forest types. *}
149 domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest")
150 and 'a forest = Empty | Trees (lazy "'a tree") "'a forest"
153 To define mutually recursive functions, give multiple type signatures
154 separated by the keyword @{text "and"}.
158 map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)"
160 map_forest :: "('a \<rightarrow> 'b) \<rightarrow> ('a forest \<rightarrow> 'b forest)"
162 "map_tree\<cdot>f\<cdot>(Leaf\<cdot>x) = Leaf\<cdot>(f\<cdot>x)"
163 | "map_tree\<cdot>f\<cdot>(Branch\<cdot>ts) = Branch\<cdot>(map_forest\<cdot>f\<cdot>ts)"
164 | "map_forest\<cdot>f\<cdot>Empty = Empty"
165 | "ts \<noteq> \<bottom> \<Longrightarrow>
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)"
168 lemma map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom> = \<bottom>"
171 lemma map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom> = \<bottom>"
176 @{text map_tree_def} @{thm map_tree_def}
177 @{text map_forest_def} @{thm map_forest_def}
178 @{text map_tree.unfold} @{thm map_tree.unfold}
179 @{text map_forest.unfold} @{thm map_forest.unfold}
180 @{text map_tree.simps} @{thm map_tree.simps}
181 @{text map_forest.simps} @{thm map_forest.simps}
182 @{text map_tree_map_forest.induct} @{thm map_tree_map_forest.induct}
186 subsection {* Looping simp rules *}
189 The defining equations of a fixrec definition are declared as simp
190 rules by default. In some cases, especially for constants with no
191 arguments or functions with variable patterns, the defining
192 equations may cause the simplifier to loop. In these cases it will
193 be necessary to use a @{text "[simp del]"} declaration.
197 repeat :: "'a \<rightarrow> 'a llist"
199 [simp del]: "repeat\<cdot>x = lCons\<cdot>x\<cdot>(repeat\<cdot>x)"
202 We can derive other non-looping simp rules for @{const repeat} by
203 using the @{text subst} method with the @{text repeat.simps} rule.
206 lemma repeat_simps [simp]:
207 "repeat\<cdot>x \<noteq> \<bottom>"
208 "repeat\<cdot>x \<noteq> lNil"
209 "repeat\<cdot>x = lCons\<cdot>y\<cdot>ys \<longleftrightarrow> x = y \<and> repeat\<cdot>x = ys"
210 by (subst repeat.simps, simp)+
212 lemma llist_when_repeat [simp]:
213 "llist_when\<cdot>z\<cdot>f\<cdot>(repeat\<cdot>x) = f\<cdot>x\<cdot>(repeat\<cdot>x)"
214 by (subst repeat.simps, simp)
217 For mutually-recursive constants, looping might only occur if all
218 equations are in the simpset at the same time. In such cases it may
219 only be necessary to declare @{text "[simp del]"} on one equation.
223 inf_tree :: "'a tree" and inf_forest :: "'a forest"
225 [simp del]: "inf_tree = Branch\<cdot>inf_forest"
226 | "inf_forest = Trees\<cdot>inf_tree\<cdot>(Trees\<cdot>inf_tree\<cdot>Empty)"
229 subsection {* Using @{text fixrec} inside locales *}
232 fixes foo :: "'a \<rightarrow> 'a"
233 assumes foo_strict: "foo\<cdot>\<bottom> = \<bottom>"
237 bar :: "'a u \<rightarrow> 'a"
239 "bar\<cdot>(up\<cdot>x) = foo\<cdot>x"
241 lemma bar_strict: "bar\<cdot>\<bottom> = \<bottom>"