1.1 --- a/src/HOLCF/Library/List_Cpo.thy	Tue Sep 07 17:36:33 2010 +0200
     1.2 +++ b/src/HOLCF/Library/List_Cpo.thy	Tue Sep 07 15:56:33 2010 -0700
     1.3 @@ -207,4 +207,32 @@
     1.4  deserve to have continuity lemmas.  I'll add more as they are
     1.5  needed. *}
     1.6  
     1.7 +subsection {* Using lists with fixrec *}
     1.8 +
     1.9 +definition
    1.10 +  match_Nil :: "'a::cpo list \<rightarrow> 'b match \<rightarrow> 'b match"
    1.11 +where
    1.12 +  "match_Nil = (\<Lambda> xs k. case xs of [] \<Rightarrow> k | y # ys \<Rightarrow> Fixrec.fail)"
    1.13 +
    1.14 +definition
    1.15 +  match_Cons :: "'a::cpo list \<rightarrow> ('a \<rightarrow> 'a list \<rightarrow> 'b match) \<rightarrow> 'b match"
    1.16 +where
    1.17 +  "match_Cons = (\<Lambda> xs k. case xs of [] \<Rightarrow> Fixrec.fail | y # ys \<Rightarrow> k\<cdot>y\<cdot>ys)"
    1.18 +
    1.19 +lemma match_Nil_simps [simp]:
    1.20 +  "match_Nil\<cdot>[]\<cdot>k = k"
    1.21 +  "match_Nil\<cdot>(x # xs)\<cdot>k = Fixrec.fail"
    1.22 +unfolding match_Nil_def by simp_all
    1.23 +
    1.24 +lemma match_Cons_simps [simp]:
    1.25 +  "match_Cons\<cdot>[]\<cdot>k = Fixrec.fail"
    1.26 +  "match_Cons\<cdot>(x # xs)\<cdot>k = k\<cdot>x\<cdot>xs"
    1.27 +unfolding match_Cons_def by simp_all
    1.28 +
    1.29 +setup {*
    1.30 +  Fixrec.add_matchers
    1.31 +    [ (@{const_name Nil}, @{const_name match_Nil}),
    1.32 +      (@{const_name Cons}, @{const_name match_Cons}) ]
    1.33 +*}
    1.34 +
    1.35  end