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