src/HOLCF/Fun_Cpo.thy
changeset 40622 e40e9e9769f4
parent 40091 1ca61fbd8a79
child 40771 1c6f7d4b110e
     1.1 --- a/src/HOLCF/Fun_Cpo.thy	Wed Nov 17 12:19:19 2010 -0800
     1.2 +++ b/src/HOLCF/Fun_Cpo.thy	Wed Nov 17 16:05:18 2010 -0800
     1.3 @@ -46,11 +46,6 @@
     1.4  
     1.5  subsection {* Full function space is chain complete *}
     1.6  
     1.7 -text {* Function application is monotone. *}
     1.8 -
     1.9 -lemma monofun_app: "monofun (\<lambda>f. f x)"
    1.10 -by (rule monofunI, simp add: below_fun_def)
    1.11 -
    1.12  text {* Properties of chains of functions. *}
    1.13  
    1.14  lemma fun_chain_iff: "chain S \<longleftrightarrow> (\<forall>x. chain (\<lambda>i. S i x))"
    1.15 @@ -158,6 +153,9 @@
    1.16  apply (simp add: cont2contlubE thelub_fun ch2ch_cont)
    1.17  done
    1.18  
    1.19 +lemma cont_fun: "cont (\<lambda>f. f x)"
    1.20 +using cont_id by (rule cont2cont_fun)
    1.21 +
    1.22  text {*
    1.23    Lambda abstraction preserves monotonicity and continuity.
    1.24    (Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"}.)