# HG changeset patch
# User huffman
# Date 1240886670 25200
# Node ID b8f4e351b5bf3cb4b2ddf97b33b428c204d36d00
# Parent  7c871a9cf6f4fc7aabec476ad66b46ee524ece4a
add proper support for bottom-patterns in fixrec package

diff -r 7c871a9cf6f4 -r b8f4e351b5bf src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Mon Apr 27 07:26:17 2009 -0700
+++ b/src/HOLCF/Fixrec.thy	Mon Apr 27 19:44:30 2009 -0700
@@ -520,8 +520,9 @@
   "match_FF = (\<Lambda> x k. If x then fail else k fi)"
 
 lemma match_UU_simps [simp]:
-  "match_UU\<cdot>x\<cdot>k = (if x = \<bottom> then \<bottom> else fail)"
-by (simp add: match_UU_def)
+  "match_UU\<cdot>\<bottom>\<cdot>k = \<bottom>"
+  "x \<noteq> \<bottom> \<Longrightarrow> match_UU\<cdot>x\<cdot>k = fail"
+by (simp_all add: match_UU_def)
 
 lemma match_cpair_simps [simp]:
   "match_cpair\<cdot>\<langle>x, y\<rangle>\<cdot>k = k\<cdot>x\<cdot>y"
@@ -603,7 +604,8 @@
       (@{const_name cpair}, @{const_name match_cpair}),
       (@{const_name ONE}, @{const_name match_ONE}),
       (@{const_name TT}, @{const_name match_TT}),
-      (@{const_name FF}, @{const_name match_FF}) ]
+      (@{const_name FF}, @{const_name match_FF}),
+      (@{const_name UU}, @{const_name match_UU}) ]
 *}
 
 hide (open) const return bind fail run cases
diff -r 7c871a9cf6f4 -r b8f4e351b5bf src/HOLCF/ex/Fixrec_ex.thy
--- a/src/HOLCF/ex/Fixrec_ex.thy	Mon Apr 27 07:26:17 2009 -0700
+++ b/src/HOLCF/ex/Fixrec_ex.thy	Mon Apr 27 19:44:30 2009 -0700
@@ -8,7 +8,7 @@
 imports HOLCF
 begin
 
-subsection {* basic fixrec examples *}
+subsection {* Basic @{text fixrec} examples *}
 
 text {*
   Fixrec patterns can mention any constructor defined by the domain
@@ -16,31 +16,31 @@
   cpair, spair, sinl, sinr, up, ONE, TT, FF.
 *}
 
-text {* typical usage is with lazy constructors *}
+text {* Typical usage is with lazy constructors. *}
 
 fixrec down :: "'a u \<rightarrow> 'a"
 where "down\<cdot>(up\<cdot>x) = x"
 
-text {* with strict constructors, rewrite rules may require side conditions *}
+text {* With strict constructors, rewrite rules may require side conditions. *}
 
 fixrec from_sinl :: "'a \<oplus> 'b \<rightarrow> 'a"
 where "x \<noteq> \<bottom> \<Longrightarrow> from_sinl\<cdot>(sinl\<cdot>x) = x"
 
-text {* lifting can turn a strict constructor into a lazy one *}
+text {* Lifting can turn a strict constructor into a lazy one. *}
 
 fixrec from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a"
 where "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x"
 
 
-subsection {* fixpat examples *}
+subsection {* Examples using @{text fixpat} *}
 
-text {* a type of lazy lists *}
+text {* A type of lazy lists. *}
 
 domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist")
 
-text {* zip function for lazy lists *}
+text {* A zip function for lazy lists. *}
 
-text {* notice that the patterns are not exhaustive *}
+text {* Notice that the patterns are not exhaustive. *}
 
 fixrec
   lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
@@ -48,24 +48,59 @@
   "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)"
 | "lzip\<cdot>lNil\<cdot>lNil = lNil"
 
-text {* fixpat is useful for producing strictness theorems *}
-text {* note that pattern matching is done in left-to-right order *}
+text {* @{text fixpat} is useful for producing strictness theorems. *}
+text {* Note that pattern matching is done in left-to-right order. *}
 
 fixpat lzip_stricts [simp]:
   "lzip\<cdot>\<bottom>\<cdot>ys"
   "lzip\<cdot>lNil\<cdot>\<bottom>"
   "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom>"
 
-text {* fixpat can also produce rules for missing cases *}
+text {* @{text fixpat} can also produce rules for missing cases. *}
 
 fixpat lzip_undefs [simp]:
   "lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys)"
   "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil"
 
 
-subsection {* skipping proofs of rewrite rules *}
+subsection {* Pattern matching with bottoms *}
+
+text {*
+  As an alternative to using @{text fixpat}, it is also possible to
+  use bottom as a constructor pattern.  When using a bottom pattern,
+  the right-hand-side must also be bottom; otherwise, @{text fixrec}
+  will not be able to prove the equation.
+*}
+
+fixrec
+  from_sinr_up :: "'a \<oplus> 'b\<^sub>\<bottom> \<rightarrow> 'b"
+where
+  "from_sinr_up\<cdot>\<bottom> = \<bottom>"
+| "from_sinr_up\<cdot>(sinr\<cdot>(up\<cdot>x)) = x"
 
-text {* another zip function for lazy lists *}
+text {*
+  If the function is already strict in that argument, then the bottom
+  pattern does not change the meaning of the function.  For example,
+  in the definition of @{term from_sinr_up}, the first equation is
+  actually redundant, and could have been proven separately by
+  @{text fixpat}.
+*}
+
+text {*
+  A bottom pattern can also be used to make a function strict in a
+  certain argument, similar to a bang-pattern in Haskell.
+*}
+
+fixrec
+  seq :: "'a \<rightarrow> 'b \<rightarrow> 'b"
+where
+  "seq\<cdot>\<bottom>\<cdot>y = \<bottom>"
+| "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x\<cdot>y = y"
+
+
+subsection {* Skipping proofs of rewrite rules *}
+
+text {* Another zip function for lazy lists. *}
 
 text {*
   Notice that this version has overlapping patterns.
@@ -85,7 +120,7 @@
   does not produce any simp rules.
 *}
 
-text {* simp rules can be generated later using fixpat *}
+text {* Simp rules can be generated later using @{text fixpat}. *}
 
 fixpat lzip2_simps [simp]:
   "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys)"
@@ -97,16 +132,17 @@
   "lzip2\<cdot>\<bottom>\<cdot>ys"
   "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom>"
 
-subsection {* mutual recursion with fixrec *}
 
-text {* tree and forest types *}
+subsection {* Mutual recursion with @{text fixrec} *}
+
+text {* Tree and forest types. *}
 
 domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest")
 and    'a forest = Empty | Trees (lazy "'a tree") "'a forest"
 
 text {*
   To define mutually recursive functions, separate the equations
-  for each function using the keyword "and".
+  for each function using the keyword @{text "and"}.
 *}
 
 fixrec
@@ -125,10 +161,13 @@
 
 text {*
   Theorems generated:
-  map_tree_def map_forest_def
-  map_tree_unfold map_forest_unfold
-  map_tree_simps map_forest_simps
-  map_tree_map_forest_induct
+  @{text map_tree_def}
+  @{text map_forest_def}
+  @{text map_tree_unfold}
+  @{text map_forest_unfold}
+  @{text map_tree_simps}
+  @{text map_forest_simps}
+  @{text map_tree_map_forest_induct}
 *}
 
 end