1.1 --- a/src/HOLCF/Fixrec.thy	Mon Apr 27 07:26:17 2009 -0700
     1.2 +++ b/src/HOLCF/Fixrec.thy	Mon Apr 27 19:44:30 2009 -0700
     1.3 @@ -520,8 +520,9 @@
     1.4    "match_FF = (\<Lambda> x k. If x then fail else k fi)"
     1.5  
     1.6  lemma match_UU_simps [simp]:
     1.7 -  "match_UU\<cdot>x\<cdot>k = (if x = \<bottom> then \<bottom> else fail)"
     1.8 -by (simp add: match_UU_def)
     1.9 +  "match_UU\<cdot>\<bottom>\<cdot>k = \<bottom>"
    1.10 +  "x \<noteq> \<bottom> \<Longrightarrow> match_UU\<cdot>x\<cdot>k = fail"
    1.11 +by (simp_all add: match_UU_def)
    1.12  
    1.13  lemma match_cpair_simps [simp]:
    1.14    "match_cpair\<cdot>\<langle>x, y\<rangle>\<cdot>k = k\<cdot>x\<cdot>y"
    1.15 @@ -603,7 +604,8 @@
    1.16        (@{const_name cpair}, @{const_name match_cpair}),
    1.17        (@{const_name ONE}, @{const_name match_ONE}),
    1.18        (@{const_name TT}, @{const_name match_TT}),
    1.19 -      (@{const_name FF}, @{const_name match_FF}) ]
    1.20 +      (@{const_name FF}, @{const_name match_FF}),
    1.21 +      (@{const_name UU}, @{const_name match_UU}) ]
    1.22  *}
    1.23  
    1.24  hide (open) const return bind fail run cases

     2.1 --- a/src/HOLCF/ex/Fixrec_ex.thy	Mon Apr 27 07:26:17 2009 -0700
     2.2 +++ b/src/HOLCF/ex/Fixrec_ex.thy	Mon Apr 27 19:44:30 2009 -0700
     2.3 @@ -8,7 +8,7 @@
     2.4  imports HOLCF
     2.5  begin
     2.6  
     2.7 -subsection {* basic fixrec examples *}
     2.8 +subsection {* Basic @{text fixrec} examples *}
     2.9  
    2.10  text {*
    2.11    Fixrec patterns can mention any constructor defined by the domain
    2.12 @@ -16,31 +16,31 @@
    2.13    cpair, spair, sinl, sinr, up, ONE, TT, FF.
    2.14  *}
    2.15  
    2.16 -text {* typical usage is with lazy constructors *}
    2.17 +text {* Typical usage is with lazy constructors. *}
    2.18  
    2.19  fixrec down :: "'a u \<rightarrow> 'a"
    2.20  where "down\<cdot>(up\<cdot>x) = x"
    2.21  
    2.22 -text {* with strict constructors, rewrite rules may require side conditions *}
    2.23 +text {* With strict constructors, rewrite rules may require side conditions. *}
    2.24  
    2.25  fixrec from_sinl :: "'a \<oplus> 'b \<rightarrow> 'a"
    2.26  where "x \<noteq> \<bottom> \<Longrightarrow> from_sinl\<cdot>(sinl\<cdot>x) = x"
    2.27  
    2.28 -text {* lifting can turn a strict constructor into a lazy one *}
    2.29 +text {* Lifting can turn a strict constructor into a lazy one. *}
    2.30  
    2.31  fixrec from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a"
    2.32  where "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x"
    2.33  
    2.34  
    2.35 -subsection {* fixpat examples *}
    2.36 +subsection {* Examples using @{text fixpat} *}
    2.37  
    2.38 -text {* a type of lazy lists *}
    2.39 +text {* A type of lazy lists. *}
    2.40  
    2.41  domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist")
    2.42  
    2.43 -text {* zip function for lazy lists *}
    2.44 +text {* A zip function for lazy lists. *}
    2.45  
    2.46 -text {* notice that the patterns are not exhaustive *}
    2.47 +text {* Notice that the patterns are not exhaustive. *}
    2.48  
    2.49  fixrec
    2.50    lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
    2.51 @@ -48,24 +48,59 @@
    2.52    "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)"
    2.53  | "lzip\<cdot>lNil\<cdot>lNil = lNil"
    2.54  
    2.55 -text {* fixpat is useful for producing strictness theorems *}
    2.56 -text {* note that pattern matching is done in left-to-right order *}
    2.57 +text {* @{text fixpat} is useful for producing strictness theorems. *}
    2.58 +text {* Note that pattern matching is done in left-to-right order. *}
    2.59  
    2.60  fixpat lzip_stricts [simp]:
    2.61    "lzip\<cdot>\<bottom>\<cdot>ys"
    2.62    "lzip\<cdot>lNil\<cdot>\<bottom>"
    2.63    "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom>"
    2.64  
    2.65 -text {* fixpat can also produce rules for missing cases *}
    2.66 +text {* @{text fixpat} can also produce rules for missing cases. *}
    2.67  
    2.68  fixpat lzip_undefs [simp]:
    2.69    "lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys)"
    2.70    "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil"
    2.71  
    2.72  
    2.73 -subsection {* skipping proofs of rewrite rules *}
    2.74 +subsection {* Pattern matching with bottoms *}
    2.75  
    2.76 -text {* another zip function for lazy lists *}
    2.77 +text {*
    2.78 +  As an alternative to using @{text fixpat}, it is also possible to
    2.79 +  use bottom as a constructor pattern.  When using a bottom pattern,
    2.80 +  the right-hand-side must also be bottom; otherwise, @{text fixrec}
    2.81 +  will not be able to prove the equation.
    2.82 +*}
    2.83 +
    2.84 +fixrec
    2.85 +  from_sinr_up :: "'a \<oplus> 'b\<^sub>\<bottom> \<rightarrow> 'b"
    2.86 +where
    2.87 +  "from_sinr_up\<cdot>\<bottom> = \<bottom>"
    2.88 +| "from_sinr_up\<cdot>(sinr\<cdot>(up\<cdot>x)) = x"
    2.89 +
    2.90 +text {*
    2.91 +  If the function is already strict in that argument, then the bottom
    2.92 +  pattern does not change the meaning of the function.  For example,
    2.93 +  in the definition of @{term from_sinr_up}, the first equation is
    2.94 +  actually redundant, and could have been proven separately by
    2.95 +  @{text fixpat}.
    2.96 +*}
    2.97 +
    2.98 +text {*
    2.99 +  A bottom pattern can also be used to make a function strict in a
   2.100 +  certain argument, similar to a bang-pattern in Haskell.
   2.101 +*}
   2.102 +
   2.103 +fixrec
   2.104 +  seq :: "'a \<rightarrow> 'b \<rightarrow> 'b"
   2.105 +where
   2.106 +  "seq\<cdot>\<bottom>\<cdot>y = \<bottom>"
   2.107 +| "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x\<cdot>y = y"
   2.108 +
   2.109 +
   2.110 +subsection {* Skipping proofs of rewrite rules *}
   2.111 +
   2.112 +text {* Another zip function for lazy lists. *}
   2.113  
   2.114  text {*
   2.115    Notice that this version has overlapping patterns.
   2.116 @@ -85,7 +120,7 @@
   2.117    does not produce any simp rules.
   2.118  *}
   2.119  
   2.120 -text {* simp rules can be generated later using fixpat *}
   2.121 +text {* Simp rules can be generated later using @{text fixpat}. *}
   2.122  
   2.123  fixpat lzip2_simps [simp]:
   2.124    "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys)"
   2.125 @@ -97,16 +132,17 @@
   2.126    "lzip2\<cdot>\<bottom>\<cdot>ys"
   2.127    "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom>"
   2.128  
   2.129 -subsection {* mutual recursion with fixrec *}
   2.130  
   2.131 -text {* tree and forest types *}
   2.132 +subsection {* Mutual recursion with @{text fixrec} *}
   2.133 +
   2.134 +text {* Tree and forest types. *}
   2.135  
   2.136  domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest")
   2.137  and    'a forest = Empty | Trees (lazy "'a tree") "'a forest"
   2.138  
   2.139  text {*
   2.140    To define mutually recursive functions, separate the equations
   2.141 -  for each function using the keyword "and".
   2.142 +  for each function using the keyword @{text "and"}.
   2.143  *}
   2.144  
   2.145  fixrec
   2.146 @@ -125,10 +161,13 @@
   2.147  
   2.148  text {*
   2.149    Theorems generated:
   2.150 -  map_tree_def map_forest_def
   2.151 -  map_tree_unfold map_forest_unfold
   2.152 -  map_tree_simps map_forest_simps
   2.153 -  map_tree_map_forest_induct
   2.154 +  @{text map_tree_def}
   2.155 +  @{text map_forest_def}
   2.156 +  @{text map_tree_unfold}
   2.157 +  @{text map_forest_unfold}
   2.158 +  @{text map_tree_simps}
   2.159 +  @{text map_forest_simps}
   2.160 +  @{text map_tree_map_forest_induct}
   2.161  *}
   2.162  
   2.163  end