# HG changeset patch
# User huffman
# Date 1283610956 25200
# Node ID 23b1e67593596bfa8ce2679b5269fd21c483d591
# Parent  d80990d8b90998cde3bbfcd2e879e367032f5f4b
add lemma cont2cont_split_simple

diff -r d80990d8b909 -r 23b1e6759359 src/HOLCF/Product_Cpo.thy
--- 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)"