# 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: "\x b. cont (\a. f x a b)" assumes f3: "\x a. cont (\b. f x a b)" assumes g: "cont (\x. g x)" - shows "cont (\x. split (\a b. f x a b) (g x))" + shows "cont (\x. case g x of (a, b) \ 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 "\a b. cont (\x. f x a b)" + shows "cont (\x. case p of (a, b) \ f x a b)" +using assms by (cases p) auto + subsection {* Compactness and chain-finiteness *} lemma fst_below_iff: "fst (x::'a \ 'b) \ y \ x \ (y, snd x)"