1.1 --- a/src/HOLCF/Fixrec.thy	Tue Jul 12 17:56:03 2005 +0200
     1.2 +++ b/src/HOLCF/Fixrec.thy	Tue Jul 12 18:20:44 2005 +0200
     1.3 @@ -12,6 +12,8 @@
     1.4  
     1.5  subsection {* Maybe monad type *}
     1.6  
     1.7 +defaultsort cpo
     1.8 +
     1.9  types 'a maybe = "one ++ 'a u"
    1.10  
    1.11  constdefs
    1.12 @@ -77,7 +79,7 @@
    1.13  subsection {* Run operator *}
    1.14  
    1.15  constdefs
    1.16 -  run:: "'a maybe \<rightarrow> 'a"
    1.17 +  run:: "'a::pcpo maybe \<rightarrow> 'a"
    1.18    "run \<equiv> sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)"
    1.19  
    1.20  text {* rewrite rules for run *}
    1.21 @@ -119,8 +121,13 @@
    1.22  
    1.23  subsection {* Match functions for built-in types *}
    1.24  
    1.25 +defaultsort pcpo
    1.26 +
    1.27  constdefs
    1.28 -  match_cpair :: "'a \<times> 'b \<rightarrow> ('a \<times> 'b) maybe"
    1.29 +  match_UU :: "'a \<rightarrow> unit maybe"
    1.30 +  "match_UU \<equiv> \<Lambda> x. fail"
    1.31 +
    1.32 +  match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<times> 'b) maybe"
    1.33    "match_cpair \<equiv> csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
    1.34  
    1.35    match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<times> 'b) maybe"
    1.36 @@ -132,7 +139,7 @@
    1.37    match_sinr :: "'a \<oplus> 'b \<rightarrow> 'b maybe"
    1.38    "match_sinr \<equiv> sscase\<cdot>(\<Lambda> x. fail)\<cdot>return"
    1.39  
    1.40 -  match_up :: "'a u \<rightarrow> 'a maybe"
    1.41 +  match_up :: "'a::cpo u \<rightarrow> 'a maybe"
    1.42    "match_up \<equiv> fup\<cdot>return"
    1.43  
    1.44    match_ONE :: "one \<rightarrow> unit maybe"
    1.45 @@ -144,6 +151,10 @@
    1.46    match_FF :: "tr \<rightarrow> unit maybe"
    1.47    "match_FF \<equiv> flift1 (\<lambda>b. if b then fail else return\<cdot>())"
    1.48  
    1.49 +lemma match_UU_simps [simp]:
    1.50 +  "match_UU\<cdot>x = fail"
    1.51 +by (simp add: match_UU_def)
    1.52 +
    1.53  lemma match_cpair_simps [simp]:
    1.54    "match_cpair\<cdot><x,y> = return\<cdot><x,y>"
    1.55  by (simp add: match_cpair_def)