1.1 --- a/src/HOLCF/Cont.thy	Fri Nov 26 15:11:08 2010 -0800
     1.2 +++ b/src/HOLCF/Cont.thy	Fri Nov 26 14:13:34 2010 -0800
     1.3 @@ -97,22 +97,26 @@
     1.4  done
     1.5  
     1.6  lemma contI2:
     1.7 +  fixes f :: "'a::cpo \<Rightarrow> 'b::cpo"
     1.8    assumes mono: "monofun f"
     1.9    assumes below: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk>
    1.10       \<Longrightarrow> f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))"
    1.11    shows "cont f"
    1.12 -apply (rule contI)
    1.13 -apply (rule thelubE)
    1.14 -apply (erule ch2ch_monofun [OF mono])
    1.15 -apply (rule below_antisym)
    1.16 -apply (rule is_lub_thelub)
    1.17 -apply (erule ch2ch_monofun [OF mono])
    1.18 -apply (rule ub2ub_monofun [OF mono])
    1.19 -apply (rule is_lubD1)
    1.20 -apply (erule cpo_lubI)
    1.21 -apply (rule below, assumption)
    1.22 -apply (erule ch2ch_monofun [OF mono])
    1.23 -done
    1.24 +proof (rule contI)
    1.25 +  fix Y :: "nat \<Rightarrow> 'a"
    1.26 +  assume Y: "chain Y"
    1.27 +  with mono have fY: "chain (\<lambda>i. f (Y i))"
    1.28 +    by (rule ch2ch_monofun)
    1.29 +  have "(\<Squnion>i. f (Y i)) = f (\<Squnion>i. Y i)"
    1.30 +    apply (rule below_antisym)
    1.31 +    apply (rule lub_below [OF fY])
    1.32 +    apply (rule monofunE [OF mono])
    1.33 +    apply (rule is_ub_thelub [OF Y])
    1.34 +    apply (rule below [OF Y fY])
    1.35 +    done
    1.36 +  with fY show "range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)"
    1.37 +    by (rule thelubE)
    1.38 +qed
    1.39  
    1.40  subsection {* Collection of continuity rules *}
    1.41