--- a/src/HOLCF/Product_Cpo.thy Sat Sep 04 07:26:34 2010 -0700
+++ b/src/HOLCF/Product_Cpo.thy Sat Sep 04 07:35:56 2010 -0700
@@ -239,7 +239,7 @@
assumes f2: "\<And>x b. cont (\<lambda>a. f x a b)"
assumes f3: "\<And>x a. cont (\<lambda>b. f x a b)"
assumes g: "cont (\<lambda>x. g x)"
- shows "cont (\<lambda>x. split (\<lambda>a b. f x a b) (g x))"
+ shows "cont (\<lambda>x. case g x of (a, b) \<Rightarrow> f x a b)"
unfolding split_def
apply (rule cont_apply [OF g])
apply (rule cont_apply [OF cont_fst f2])
@@ -274,6 +274,14 @@
done
qed
+text {* The simple version (due to Joachim Breitner) is needed if
+ either element type of the pair is not a cpo. *}
+
+lemma cont2cont_split_simple [simp, cont2cont]:
+ assumes "\<And>a b. cont (\<lambda>x. f x a b)"
+ shows "cont (\<lambda>x. case p of (a, b) \<Rightarrow> f x a b)"
+using assms by (cases p) auto
+
subsection {* Compactness and chain-finiteness *}
lemma fst_below_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"