src/HOLCF/ex/Fixrec_ex.thy
author huffman
Tue Nov 03 18:32:56 2009 -0800 (2009-11-03)
changeset 33428 70ed971a79d1
parent 33401 fc43fa403a69
child 35770 a57ab2c01369
permissions -rw-r--r--
fixrec examples use fixrec_simp instead of fixpat
     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 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 (permissive)
   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>(lzip\<cdot>xs\<cdot>ys)"
   122 | "lzip2\<cdot>xs\<cdot>ys = lNil"
   123 
   124 text {*
   125   Usually fixrec tries to prove all equations as theorems.
   126   The "permissive" option overrides this behavior, so fixrec
   127   does not produce any simp rules.
   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>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)"
   134   "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = lNil"
   135   "lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = lNil"
   136   "lzip2\<cdot>lNil\<cdot>lNil = lNil"
   137 by fixrec_simp+
   138 
   139 lemma lzip2_stricts [simp]:
   140   "lzip2\<cdot>\<bottom>\<cdot>ys = \<bottom>"
   141   "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
   142 by fixrec_simp+
   143 
   144 
   145 subsection {* Mutual recursion with @{text fixrec} *}
   146 
   147 text {* Tree and forest types. *}
   148 
   149 domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest")
   150 and    'a forest = Empty | Trees (lazy "'a tree") "'a forest"
   151 
   152 text {*
   153   To define mutually recursive functions, separate the equations
   154   for each function using the keyword @{text "and"}.
   155 *}
   156 
   157 fixrec
   158   map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)"
   159 and
   160   map_forest :: "('a \<rightarrow> 'b) \<rightarrow> ('a forest \<rightarrow> 'b forest)"
   161 where
   162   "map_tree\<cdot>f\<cdot>(Leaf\<cdot>x) = Leaf\<cdot>(f\<cdot>x)"
   163 | "map_tree\<cdot>f\<cdot>(Branch\<cdot>ts) = Branch\<cdot>(map_forest\<cdot>f\<cdot>ts)"
   164 | "map_forest\<cdot>f\<cdot>Empty = Empty"
   165 | "ts \<noteq> \<bottom> \<Longrightarrow>
   166     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)"
   167 
   168 lemma map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom> = \<bottom>"
   169 by fixrec_simp
   170 
   171 lemma map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom> = \<bottom>"
   172 by fixrec_simp
   173 
   174 text {*
   175   Theorems generated:
   176   @{text map_tree_def}
   177   @{text map_forest_def}
   178   @{text map_tree_unfold}
   179   @{text map_forest_unfold}
   180   @{text map_tree_simps}
   181   @{text map_forest_simps}
   182   @{text map_tree_map_forest_induct}
   183 *}
   184 
   185 end