src/HOLCF/Product_Cpo.thy
changeset 31041 85b4843d9939
parent 29535 08824fad8879
child 31076 99fe356cbbc2
     1.1 --- a/src/HOLCF/Product_Cpo.thy	Wed May 06 09:08:47 2009 +0200
     1.2 +++ b/src/HOLCF/Product_Cpo.thy	Wed May 06 00:57:29 2009 -0700
     1.3 @@ -206,14 +206,54 @@
     1.4    assumes f: "cont (\<lambda>x. f x)"
     1.5    assumes g: "cont (\<lambda>x. g x)"
     1.6    shows "cont (\<lambda>x. (f x, g x))"
     1.7 -apply (rule cont2cont_apply [OF _ cont_pair1 f])
     1.8 -apply (rule cont2cont_apply [OF _ cont_pair2 g])
     1.9 +apply (rule cont_apply [OF f cont_pair1])
    1.10 +apply (rule cont_apply [OF g cont_pair2])
    1.11  apply (rule cont_const)
    1.12  done
    1.13  
    1.14 -lemmas cont2cont_fst [cont2cont] = cont2cont_compose [OF cont_fst]
    1.15 +lemmas cont2cont_fst [cont2cont] = cont_compose [OF cont_fst]
    1.16 +
    1.17 +lemmas cont2cont_snd [cont2cont] = cont_compose [OF cont_snd]
    1.18 +
    1.19 +lemma cont2cont_split:
    1.20 +  assumes f1: "\<And>a b. cont (\<lambda>x. f x a b)"
    1.21 +  assumes f2: "\<And>x b. cont (\<lambda>a. f x a b)"
    1.22 +  assumes f3: "\<And>x a. cont (\<lambda>b. f x a b)"
    1.23 +  assumes g: "cont (\<lambda>x. g x)"
    1.24 +  shows "cont (\<lambda>x. split (\<lambda>a b. f x a b) (g x))"
    1.25 +unfolding split_def
    1.26 +apply (rule cont_apply [OF g])
    1.27 +apply (rule cont_apply [OF cont_fst f2])
    1.28 +apply (rule cont_apply [OF cont_snd f3])
    1.29 +apply (rule cont_const)
    1.30 +apply (rule f1)
    1.31 +done
    1.32 +
    1.33 +lemma cont_fst_snd_D1:
    1.34 +  "cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>x. f x y)"
    1.35 +by (drule cont_compose [OF _ cont_pair1], simp)
    1.36  
    1.37 -lemmas cont2cont_snd [cont2cont] = cont2cont_compose [OF cont_snd]
    1.38 +lemma cont_fst_snd_D2:
    1.39 +  "cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>y. f x y)"
    1.40 +by (drule cont_compose [OF _ cont_pair2], simp)
    1.41 +
    1.42 +lemma cont2cont_split' [cont2cont]:
    1.43 +  assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))"
    1.44 +  assumes g: "cont (\<lambda>x. g x)"
    1.45 +  shows "cont (\<lambda>x. split (f x) (g x))"
    1.46 +proof -
    1.47 +  note f1 = f [THEN cont_fst_snd_D1]
    1.48 +  note f2 = f [THEN cont_fst_snd_D2, THEN cont_fst_snd_D1]
    1.49 +  note f3 = f [THEN cont_fst_snd_D2, THEN cont_fst_snd_D2]
    1.50 +  show ?thesis
    1.51 +    unfolding split_def
    1.52 +    apply (rule cont_apply [OF g])
    1.53 +    apply (rule cont_apply [OF cont_fst f2])
    1.54 +    apply (rule cont_apply [OF cont_snd f3])
    1.55 +    apply (rule cont_const)
    1.56 +    apply (rule f1)
    1.57 +    done
    1.58 +qed
    1.59  
    1.60  subsection {* Compactness and chain-finiteness *}
    1.61