src/HOLCF/ex/Fixrec_ex.thy
author huffman
Mon Apr 27 19:44:30 2009 -0700 (2009-04-27)
changeset 31008 b8f4e351b5bf
parent 30158 83c50c62cf23
child 33401 fc43fa403a69
permissions -rw-r--r--
add proper support for bottom-patterns in fixrec package
     1 (*  Title:      HOLCF/ex/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   cpair, 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 
    35 subsection {* Examples using @{text fixpat} *}
    36 
    37 text {* A type of lazy lists. *}
    38 
    39 domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist")
    40 
    41 text {* A zip function for lazy lists. *}
    42 
    43 text {* Notice that the patterns are not exhaustive. *}
    44 
    45 fixrec
    46   lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
    47 where
    48   "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)"
    49 | "lzip\<cdot>lNil\<cdot>lNil = lNil"
    50 
    51 text {* @{text fixpat} is useful for producing strictness theorems. *}
    52 text {* Note that pattern matching is done in left-to-right order. *}
    53 
    54 fixpat lzip_stricts [simp]:
    55   "lzip\<cdot>\<bottom>\<cdot>ys"
    56   "lzip\<cdot>lNil\<cdot>\<bottom>"
    57   "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom>"
    58 
    59 text {* @{text fixpat} can also produce rules for missing cases. *}
    60 
    61 fixpat lzip_undefs [simp]:
    62   "lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys)"
    63   "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil"
    64 
    65 
    66 subsection {* Pattern matching with bottoms *}
    67 
    68 text {*
    69   As an alternative to using @{text fixpat}, it is also possible to
    70   use bottom as a constructor pattern.  When using a bottom pattern,
    71   the right-hand-side must also be bottom; otherwise, @{text fixrec}
    72   will not be able to prove the equation.
    73 *}
    74 
    75 fixrec
    76   from_sinr_up :: "'a \<oplus> 'b\<^sub>\<bottom> \<rightarrow> 'b"
    77 where
    78   "from_sinr_up\<cdot>\<bottom> = \<bottom>"
    79 | "from_sinr_up\<cdot>(sinr\<cdot>(up\<cdot>x)) = x"
    80 
    81 text {*
    82   If the function is already strict in that argument, then the bottom
    83   pattern does not change the meaning of the function.  For example,
    84   in the definition of @{term from_sinr_up}, the first equation is
    85   actually redundant, and could have been proven separately by
    86   @{text fixpat}.
    87 *}
    88 
    89 text {*
    90   A bottom pattern can also be used to make a function strict in a
    91   certain argument, similar to a bang-pattern in Haskell.
    92 *}
    93 
    94 fixrec
    95   seq :: "'a \<rightarrow> 'b \<rightarrow> 'b"
    96 where
    97   "seq\<cdot>\<bottom>\<cdot>y = \<bottom>"
    98 | "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x\<cdot>y = y"
    99 
   100 
   101 subsection {* Skipping proofs of rewrite rules *}
   102 
   103 text {* Another zip function for lazy lists. *}
   104 
   105 text {*
   106   Notice that this version has overlapping patterns.
   107   The second equation cannot be proved as a theorem
   108   because it only applies when the first pattern fails.
   109 *}
   110 
   111 fixrec (permissive)
   112   lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
   113 where
   114   "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)"
   115 | "lzip2\<cdot>xs\<cdot>ys = lNil"
   116 
   117 text {*
   118   Usually fixrec tries to prove all equations as theorems.
   119   The "permissive" option overrides this behavior, so fixrec
   120   does not produce any simp rules.
   121 *}
   122 
   123 text {* Simp rules can be generated later using @{text fixpat}. *}
   124 
   125 fixpat lzip2_simps [simp]:
   126   "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys)"
   127   "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil"
   128   "lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys)"
   129   "lzip2\<cdot>lNil\<cdot>lNil"
   130 
   131 fixpat lzip2_stricts [simp]:
   132   "lzip2\<cdot>\<bottom>\<cdot>ys"
   133   "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom>"
   134 
   135 
   136 subsection {* Mutual recursion with @{text fixrec} *}
   137 
   138 text {* Tree and forest types. *}
   139 
   140 domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest")
   141 and    'a forest = Empty | Trees (lazy "'a tree") "'a forest"
   142 
   143 text {*
   144   To define mutually recursive functions, separate the equations
   145   for each function using the keyword @{text "and"}.
   146 *}
   147 
   148 fixrec
   149   map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)"
   150 and
   151   map_forest :: "('a \<rightarrow> 'b) \<rightarrow> ('a forest \<rightarrow> 'b forest)"
   152 where
   153   "map_tree\<cdot>f\<cdot>(Leaf\<cdot>x) = Leaf\<cdot>(f\<cdot>x)"
   154 | "map_tree\<cdot>f\<cdot>(Branch\<cdot>ts) = Branch\<cdot>(map_forest\<cdot>f\<cdot>ts)"
   155 | "map_forest\<cdot>f\<cdot>Empty = Empty"
   156 | "ts \<noteq> \<bottom> \<Longrightarrow>
   157     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)"
   158 
   159 fixpat map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom>"
   160 fixpat map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom>"
   161 
   162 text {*
   163   Theorems generated:
   164   @{text map_tree_def}
   165   @{text map_forest_def}
   166   @{text map_tree_unfold}
   167   @{text map_forest_unfold}
   168   @{text map_tree_simps}
   169   @{text map_forest_simps}
   170   @{text map_tree_map_forest_induct}
   171 *}
   172 
   173 end