# HG changeset patch
# User huffman
# Date 1289411570 28800
# Node ID 2a92d3f5026c016c5fcb9bec31d0c9d2c4e08e54
# Parent  db8a09daba7b8b1f7a80bfcb09afd75327939e1d
configure sum type for fixrec

diff -r db8a09daba7b -r 2a92d3f5026c src/HOLCF/Library/Sum_Cpo.thy
--- a/src/HOLCF/Library/Sum_Cpo.thy	Wed Nov 10 08:18:32 2010 -0800
+++ b/src/HOLCF/Library/Sum_Cpo.thy	Wed Nov 10 09:52:50 2010 -0800
@@ -216,4 +216,28 @@
 instance sum :: (discrete_cpo, discrete_cpo) discrete_cpo
 by intro_classes (simp add: below_sum_def split: sum.split)
 
+subsection {* Using sum types with fixrec *}
+
+definition
+  "match_Inl = (\<Lambda> x k. case x of Inl a \<Rightarrow> k\<cdot>a | Inr b \<Rightarrow> Fixrec.fail)"
+
+definition
+  "match_Inr = (\<Lambda> x k. case x of Inl a \<Rightarrow> Fixrec.fail | Inr b \<Rightarrow> k\<cdot>b)"
+
+lemma match_Inl_simps [simp]:
+  "match_Inl\<cdot>(Inl a)\<cdot>k = k\<cdot>a"
+  "match_Inl\<cdot>(Inr b)\<cdot>k = Fixrec.fail"
+unfolding match_Inl_def by simp_all
+
+lemma match_Inr_simps [simp]:
+  "match_Inr\<cdot>(Inl a)\<cdot>k = Fixrec.fail"
+  "match_Inr\<cdot>(Inr b)\<cdot>k = k\<cdot>b"
+unfolding match_Inr_def by simp_all
+
+setup {*
+  Fixrec.add_matchers
+    [ (@{const_name Inl}, @{const_name match_Inl}),
+      (@{const_name Inr}, @{const_name match_Inr}) ]
+*}
+
 end