# HG changeset patch
# User huffman
# Date 1119554246 -7200
# Node ID 7abf8a713613ec448985689af49ed7bc095e9905
# Parent  e14b89d6ef1356d9b2da08466778debfbfe80c57
added match functions for spair, sinl, sinr

diff -r e14b89d6ef13 -r 7abf8a713613 src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Thu Jun 23 19:40:03 2005 +0200
+++ b/src/HOLCF/Fixrec.thy	Thu Jun 23 21:17:26 2005 +0200
@@ -6,7 +6,7 @@
 header "Package for defining recursive functions in HOLCF"
 
 theory Fixrec
-imports Ssum One Up Fix Tr
+imports Sprod Ssum Up One Tr Fix
 uses ("fixrec_package.ML")
 begin
 
@@ -119,12 +119,19 @@
 
 subsection {* Match functions for built-in types *}
 
-text {* Currently the package only supports lazy constructors *}
-
 constdefs
   match_cpair :: "'a \<times> 'b \<rightarrow> ('a \<times> 'b) maybe"
   "match_cpair \<equiv> csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
 
+  match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<times> 'b) maybe"
+  "match_spair \<equiv> ssplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
+
+  match_sinl :: "'a \<oplus> 'b \<rightarrow> 'a maybe"
+  "match_sinl \<equiv> sscase\<cdot>return\<cdot>(\<Lambda> y. fail)"
+
+  match_sinr :: "'a \<oplus> 'b \<rightarrow> 'b maybe"
+  "match_sinr \<equiv> sscase\<cdot>(\<Lambda> x. fail)\<cdot>return"
+
   match_up :: "'a u \<rightarrow> 'a maybe"
   "match_up \<equiv> fup\<cdot>return"
 
@@ -141,6 +148,23 @@
   "match_cpair\<cdot><x,y> = return\<cdot><x,y>"
 by (simp add: match_cpair_def)
 
+lemma match_spair_simps [simp]:
+  "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> match_spair\<cdot>(:x,y:) = return\<cdot><x,y>"
+  "match_spair\<cdot>\<bottom> = \<bottom>"
+by (simp_all add: match_spair_def)
+
+lemma match_sinl_simps [simp]:
+  "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinl\<cdot>x) = return\<cdot>x"
+  "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinr\<cdot>x) = fail"
+  "match_sinl\<cdot>\<bottom> = \<bottom>"
+by (simp_all add: match_sinl_def)
+
+lemma match_sinr_simps [simp]:
+  "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinr\<cdot>x) = return\<cdot>x"
+  "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinl\<cdot>x) = fail"
+  "match_sinr\<cdot>\<bottom> = \<bottom>"
+by (simp_all add: match_sinr_def)
+
 lemma match_up_simps [simp]:
   "match_up\<cdot>(up\<cdot>x) = return\<cdot>x"
   "match_up\<cdot>\<bottom> = \<bottom>"