# HG changeset patch
# User huffman
# Date 1283900193 25200
# Node ID 3989b2b44dbaf0e38cbee3a08d6e26d2936a6542
# Parent  202618462644951dffcbb719ab10dde20c4ad90e
set up Nil and Cons to work as fixrec patterns

diff -r 202618462644 -r 3989b2b44dba src/HOLCF/Library/List_Cpo.thy
--- a/src/HOLCF/Library/List_Cpo.thy	Tue Sep 07 17:36:33 2010 +0200
+++ b/src/HOLCF/Library/List_Cpo.thy	Tue Sep 07 15:56:33 2010 -0700
@@ -207,4 +207,32 @@
 deserve to have continuity lemmas.  I'll add more as they are
 needed. *}
 
+subsection {* Using lists with fixrec *}
+
+definition
+  match_Nil :: "'a::cpo list \<rightarrow> 'b match \<rightarrow> 'b match"
+where
+  "match_Nil = (\<Lambda> xs k. case xs of [] \<Rightarrow> k | y # ys \<Rightarrow> Fixrec.fail)"
+
+definition
+  match_Cons :: "'a::cpo list \<rightarrow> ('a \<rightarrow> 'a list \<rightarrow> 'b match) \<rightarrow> 'b match"
+where
+  "match_Cons = (\<Lambda> xs k. case xs of [] \<Rightarrow> Fixrec.fail | y # ys \<Rightarrow> k\<cdot>y\<cdot>ys)"
+
+lemma match_Nil_simps [simp]:
+  "match_Nil\<cdot>[]\<cdot>k = k"
+  "match_Nil\<cdot>(x # xs)\<cdot>k = Fixrec.fail"
+unfolding match_Nil_def by simp_all
+
+lemma match_Cons_simps [simp]:
+  "match_Cons\<cdot>[]\<cdot>k = Fixrec.fail"
+  "match_Cons\<cdot>(x # xs)\<cdot>k = k\<cdot>x\<cdot>xs"
+unfolding match_Cons_def by simp_all
+
+setup {*
+  Fixrec.add_matchers
+    [ (@{const_name Nil}, @{const_name match_Nil}),
+      (@{const_name Cons}, @{const_name match_Cons}) ]
+*}
+
 end