remove unused lemmas
authorhuffman
Tue Oct 12 05:48:32 2010 -0700 (2010-10-12)
changeset 400053e3611136a13
parent 40004 9f6ed6840e8d
child 40006 116e94f9543b
remove unused lemmas
src/HOLCF/Cfun.thy
     1.1 --- a/src/HOLCF/Cfun.thy	Tue Oct 12 05:48:15 2010 -0700
     1.2 +++ b/src/HOLCF/Cfun.thy	Tue Oct 12 05:48:32 2010 -0700
     1.3 @@ -293,29 +293,6 @@
     1.4  apply (rule minimal [THEN monofun_cfun_arg])
     1.5  done
     1.6  
     1.7 -text {* the lub of a chain of continous functions is monotone *}
     1.8 -
     1.9 -lemma lub_cfun_mono: "chain F \<Longrightarrow> monofun (\<lambda>x. \<Squnion>i. F i\<cdot>x)"
    1.10 -apply (drule ch2ch_monofun [OF monofun_Rep_CFun])
    1.11 -apply (simp add: thelub_fun [symmetric])
    1.12 -apply (erule monofun_lub_fun)
    1.13 -apply (simp add: monofun_Rep_CFun2)
    1.14 -done
    1.15 -
    1.16 -text {* a lemma about the exchange of lubs for type @{typ "'a -> 'b"} *}
    1.17 -
    1.18 -lemma ex_lub_cfun:
    1.19 -  "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> (\<Squnion>j. \<Squnion>i. F j\<cdot>(Y i)) = (\<Squnion>i. \<Squnion>j. F j\<cdot>(Y i))"
    1.20 -by (simp add: diag_lub)
    1.21 -
    1.22 -text {* the lub of a chain of cont. functions is continuous *}
    1.23 -
    1.24 -lemma cont_lub_cfun: "chain F \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i\<cdot>x)"
    1.25 -apply (rule cont2cont_lub)
    1.26 -apply (erule monofun_Rep_CFun [THEN ch2ch_monofun])
    1.27 -apply (rule cont_Rep_CFun2)
    1.28 -done
    1.29 -
    1.30  text {* type @{typ "'a -> 'b"} is chain complete *}
    1.31  
    1.32  lemma lub_cfun: "chain F \<Longrightarrow> range F <<| (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"