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