1.1 --- a/src/HOL/HOLCF/Cfun.thy	Sat Nov 27 17:44:36 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Sat Nov 27 22:48:08 2010 -0800
     1.3 @@ -481,12 +481,19 @@
     1.4    seq :: "'a \<rightarrow> 'b \<rightarrow> 'b" where
     1.5    "seq = (\<Lambda> x. if x = \<bottom> then \<bottom> else ID)"
     1.6  
     1.7 -lemma cont_seq: "cont (\<lambda>x. if x = \<bottom> then \<bottom> else y)"
     1.8 -unfolding cont_def is_lub_def is_ub_def ball_simps
     1.9 -by (simp add: lub_eq_bottom_iff)
    1.10 +lemma cont2cont_if_bottom [cont2cont, simp]:
    1.11 +  assumes f: "cont (\<lambda>x. f x)" and g: "cont (\<lambda>x. g x)"
    1.12 +  shows "cont (\<lambda>x. if f x = \<bottom> then \<bottom> else g x)"
    1.13 +proof (rule cont_apply [OF f])
    1.14 +  show "\<And>x. cont (\<lambda>y. if y = \<bottom> then \<bottom> else g x)"
    1.15 +    unfolding cont_def is_lub_def is_ub_def ball_simps
    1.16 +    by (simp add: lub_eq_bottom_iff)
    1.17 +  show "\<And>y. cont (\<lambda>x. if y = \<bottom> then \<bottom> else g x)"
    1.18 +    by (simp add: g)
    1.19 +qed
    1.20  
    1.21  lemma seq_conv_if: "seq\<cdot>x = (if x = \<bottom> then \<bottom> else ID)"
    1.22 -unfolding seq_def by (simp add: cont_seq)
    1.23 +unfolding seq_def by simp
    1.24  
    1.25  lemma seq1 [simp]: "seq\<cdot>\<bottom> = \<bottom>"
    1.26  by (simp add: seq_conv_if)