# HG changeset patch
# User huffman
# Date 1257301976 28800
# Node ID 70ed971a79d1f4a569787978e041a2b06d0717a5
# Parent  3182812d33ed2baf831bd665e4e7d5a7e2bd2442
fixrec examples use fixrec_simp instead of fixpat

diff -r 3182812d33ed -r 70ed971a79d1 src/HOLCF/ex/Fixrec_ex.thy
--- a/src/HOLCF/ex/Fixrec_ex.thy	Tue Nov 03 18:32:30 2009 -0800
+++ b/src/HOLCF/ex/Fixrec_ex.thy	Tue Nov 03 18:32:56 2009 -0800
@@ -37,7 +37,7 @@
 where "down2\<cdot>(up\<cdot>x, up\<cdot>y) = (x, y)"
 
 
-subsection {* Examples using @{text fixpat} *}
+subsection {* Examples using @{text fixrec_simp} *}
 
 text {* A type of lazy lists. *}
 
@@ -53,28 +53,30 @@
   "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 {* @{text fixpat} is useful for producing strictness theorems. *}
+text {* @{text fixrec_simp} 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>"
+lemma lzip_stricts [simp]:
+  "lzip\<cdot>\<bottom>\<cdot>ys = \<bottom>"
+  "lzip\<cdot>lNil\<cdot>\<bottom> = \<bottom>"
+  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
+by fixrec_simp+
 
-text {* @{text fixpat} can also produce rules for missing cases. *}
+text {* @{text fixrec_simp} 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"
+lemma lzip_undefs [simp]:
+  "lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = \<bottom>"
+  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = \<bottom>"
+by fixrec_simp+
 
 
 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.
+  As an alternative to using @{text fixrec_simp}, 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
@@ -88,7 +90,7 @@
   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 fixrec_simp}.
 *}
 
 text {*
@@ -125,17 +127,19 @@
   does not produce any simp rules.
 *}
 
-text {* Simp rules can be generated later using @{text fixpat}. *}
+text {* Simp rules can be generated later using @{text fixrec_simp}. *}
 
-fixpat lzip2_simps [simp]:
-  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys)"
-  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil"
-  "lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys)"
-  "lzip2\<cdot>lNil\<cdot>lNil"
+lemma lzip2_simps [simp]:
+  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)"
+  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = lNil"
+  "lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = lNil"
+  "lzip2\<cdot>lNil\<cdot>lNil = lNil"
+by fixrec_simp+
 
-fixpat lzip2_stricts [simp]:
-  "lzip2\<cdot>\<bottom>\<cdot>ys"
-  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom>"
+lemma lzip2_stricts [simp]:
+  "lzip2\<cdot>\<bottom>\<cdot>ys = \<bottom>"
+  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
+by fixrec_simp+
 
 
 subsection {* Mutual recursion with @{text fixrec} *}
@@ -161,8 +165,11 @@
 | "ts \<noteq> \<bottom> \<Longrightarrow>
     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)"
 
-fixpat map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom>"
-fixpat map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom>"
+lemma map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom> = \<bottom>"
+by fixrec_simp
+
+lemma map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom> = \<bottom>"
+by fixrec_simp
 
 text {*
   Theorems generated: