src/HOLCF/ex/Fixrec_ex.thy
changeset 31008 b8f4e351b5bf
parent 30158 83c50c62cf23
child 33401 fc43fa403a69
     1.1 --- a/src/HOLCF/ex/Fixrec_ex.thy	Mon Apr 27 07:26:17 2009 -0700
     1.2 +++ b/src/HOLCF/ex/Fixrec_ex.thy	Mon Apr 27 19:44:30 2009 -0700
     1.3 @@ -8,7 +8,7 @@
     1.4  imports HOLCF
     1.5  begin
     1.6  
     1.7 -subsection {* basic fixrec examples *}
     1.8 +subsection {* Basic @{text fixrec} examples *}
     1.9  
    1.10  text {*
    1.11    Fixrec patterns can mention any constructor defined by the domain
    1.12 @@ -16,31 +16,31 @@
    1.13    cpair, spair, sinl, sinr, up, ONE, TT, FF.
    1.14  *}
    1.15  
    1.16 -text {* typical usage is with lazy constructors *}
    1.17 +text {* Typical usage is with lazy constructors. *}
    1.18  
    1.19  fixrec down :: "'a u \<rightarrow> 'a"
    1.20  where "down\<cdot>(up\<cdot>x) = x"
    1.21  
    1.22 -text {* with strict constructors, rewrite rules may require side conditions *}
    1.23 +text {* With strict constructors, rewrite rules may require side conditions. *}
    1.24  
    1.25  fixrec from_sinl :: "'a \<oplus> 'b \<rightarrow> 'a"
    1.26  where "x \<noteq> \<bottom> \<Longrightarrow> from_sinl\<cdot>(sinl\<cdot>x) = x"
    1.27  
    1.28 -text {* lifting can turn a strict constructor into a lazy one *}
    1.29 +text {* Lifting can turn a strict constructor into a lazy one. *}
    1.30  
    1.31  fixrec from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a"
    1.32  where "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x"
    1.33  
    1.34  
    1.35 -subsection {* fixpat examples *}
    1.36 +subsection {* Examples using @{text fixpat} *}
    1.37  
    1.38 -text {* a type of lazy lists *}
    1.39 +text {* A type of lazy lists. *}
    1.40  
    1.41  domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist")
    1.42  
    1.43 -text {* zip function for lazy lists *}
    1.44 +text {* A zip function for lazy lists. *}
    1.45  
    1.46 -text {* notice that the patterns are not exhaustive *}
    1.47 +text {* Notice that the patterns are not exhaustive. *}
    1.48  
    1.49  fixrec
    1.50    lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
    1.51 @@ -48,24 +48,59 @@
    1.52    "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)"
    1.53  | "lzip\<cdot>lNil\<cdot>lNil = lNil"
    1.54  
    1.55 -text {* fixpat is useful for producing strictness theorems *}
    1.56 -text {* note that pattern matching is done in left-to-right order *}
    1.57 +text {* @{text fixpat} is useful for producing strictness theorems. *}
    1.58 +text {* Note that pattern matching is done in left-to-right order. *}
    1.59  
    1.60  fixpat lzip_stricts [simp]:
    1.61    "lzip\<cdot>\<bottom>\<cdot>ys"
    1.62    "lzip\<cdot>lNil\<cdot>\<bottom>"
    1.63    "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom>"
    1.64  
    1.65 -text {* fixpat can also produce rules for missing cases *}
    1.66 +text {* @{text fixpat} can also produce rules for missing cases. *}
    1.67  
    1.68  fixpat lzip_undefs [simp]:
    1.69    "lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys)"
    1.70    "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil"
    1.71  
    1.72  
    1.73 -subsection {* skipping proofs of rewrite rules *}
    1.74 +subsection {* Pattern matching with bottoms *}
    1.75 +
    1.76 +text {*
    1.77 +  As an alternative to using @{text fixpat}, it is also possible to
    1.78 +  use bottom as a constructor pattern.  When using a bottom pattern,
    1.79 +  the right-hand-side must also be bottom; otherwise, @{text fixrec}
    1.80 +  will not be able to prove the equation.
    1.81 +*}
    1.82 +
    1.83 +fixrec
    1.84 +  from_sinr_up :: "'a \<oplus> 'b\<^sub>\<bottom> \<rightarrow> 'b"
    1.85 +where
    1.86 +  "from_sinr_up\<cdot>\<bottom> = \<bottom>"
    1.87 +| "from_sinr_up\<cdot>(sinr\<cdot>(up\<cdot>x)) = x"
    1.88  
    1.89 -text {* another zip function for lazy lists *}
    1.90 +text {*
    1.91 +  If the function is already strict in that argument, then the bottom
    1.92 +  pattern does not change the meaning of the function.  For example,
    1.93 +  in the definition of @{term from_sinr_up}, the first equation is
    1.94 +  actually redundant, and could have been proven separately by
    1.95 +  @{text fixpat}.
    1.96 +*}
    1.97 +
    1.98 +text {*
    1.99 +  A bottom pattern can also be used to make a function strict in a
   1.100 +  certain argument, similar to a bang-pattern in Haskell.
   1.101 +*}
   1.102 +
   1.103 +fixrec
   1.104 +  seq :: "'a \<rightarrow> 'b \<rightarrow> 'b"
   1.105 +where
   1.106 +  "seq\<cdot>\<bottom>\<cdot>y = \<bottom>"
   1.107 +| "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x\<cdot>y = y"
   1.108 +
   1.109 +
   1.110 +subsection {* Skipping proofs of rewrite rules *}
   1.111 +
   1.112 +text {* Another zip function for lazy lists. *}
   1.113  
   1.114  text {*
   1.115    Notice that this version has overlapping patterns.
   1.116 @@ -85,7 +120,7 @@
   1.117    does not produce any simp rules.
   1.118  *}
   1.119  
   1.120 -text {* simp rules can be generated later using fixpat *}
   1.121 +text {* Simp rules can be generated later using @{text fixpat}. *}
   1.122  
   1.123  fixpat lzip2_simps [simp]:
   1.124    "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys)"
   1.125 @@ -97,16 +132,17 @@
   1.126    "lzip2\<cdot>\<bottom>\<cdot>ys"
   1.127    "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom>"
   1.128  
   1.129 -subsection {* mutual recursion with fixrec *}
   1.130  
   1.131 -text {* tree and forest types *}
   1.132 +subsection {* Mutual recursion with @{text fixrec} *}
   1.133 +
   1.134 +text {* Tree and forest types. *}
   1.135  
   1.136  domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest")
   1.137  and    'a forest = Empty | Trees (lazy "'a tree") "'a forest"
   1.138  
   1.139  text {*
   1.140    To define mutually recursive functions, separate the equations
   1.141 -  for each function using the keyword "and".
   1.142 +  for each function using the keyword @{text "and"}.
   1.143  *}
   1.144  
   1.145  fixrec
   1.146 @@ -125,10 +161,13 @@
   1.147  
   1.148  text {*
   1.149    Theorems generated:
   1.150 -  map_tree_def map_forest_def
   1.151 -  map_tree_unfold map_forest_unfold
   1.152 -  map_tree_simps map_forest_simps
   1.153 -  map_tree_map_forest_induct
   1.154 +  @{text map_tree_def}
   1.155 +  @{text map_forest_def}
   1.156 +  @{text map_tree_unfold}
   1.157 +  @{text map_forest_unfold}
   1.158 +  @{text map_tree_simps}
   1.159 +  @{text map_forest_simps}
   1.160 +  @{text map_tree_map_forest_induct}
   1.161  *}
   1.162  
   1.163  end