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