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