move lemmas from Lift.thy to Cfun.thy
authorhuffman
Tue Oct 12 09:08:27 2010 -0700 (2010-10-12)
changeset 4000858ead6f77f8e
parent 40007 bb04a995bbd3
child 40009 f2c78550c0b7
move lemmas from Lift.thy to Cfun.thy
src/HOLCF/Cfun.thy
src/HOLCF/Lift.thy
     1.1 --- a/src/HOLCF/Cfun.thy	Tue Oct 12 07:46:44 2010 -0700
     1.2 +++ b/src/HOLCF/Cfun.thy	Tue Oct 12 09:08:27 2010 -0700
     1.3 @@ -316,6 +316,18 @@
     1.4      using t cont_Rep_CFun2 1 by (rule cont_apply)
     1.5  qed
     1.6  
     1.7 +text {*
     1.8 +  Two specific lemmas for the combination of LCF and HOL terms.
     1.9 +  These lemmas are needed in theories that use types like @{typ "'a \<rightarrow> 'b \<Rightarrow> 'c"}.
    1.10 +*}
    1.11 +
    1.12 +lemma cont_Rep_CFun_app [simp]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s)"
    1.13 +by (rule cont2cont_Rep_CFun [THEN cont2cont_fun])
    1.14 +
    1.15 +lemma cont_Rep_CFun_app_app [simp]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s t)"
    1.16 +by (rule cont_Rep_CFun_app [THEN cont2cont_fun])
    1.17 +
    1.18 +
    1.19  text {* cont2mono Lemma for @{term "%x. LAM y. c1(x)(y)"} *}
    1.20  
    1.21  lemma cont2mono_LAM:
     2.1 --- a/src/HOLCF/Lift.thy	Tue Oct 12 07:46:44 2010 -0700
     2.2 +++ b/src/HOLCF/Lift.thy	Tue Oct 12 09:08:27 2010 -0700
     2.3 @@ -86,17 +86,6 @@
     2.4      by (induct x) auto
     2.5  qed
     2.6  
     2.7 -text {*
     2.8 -  \medskip Two specific lemmas for the combination of LCF and HOL
     2.9 -  terms.
    2.10 -*}
    2.11 -
    2.12 -lemma cont_Rep_CFun_app [simp]: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s)"
    2.13 -by (rule cont2cont_Rep_CFun [THEN cont2cont_fun])
    2.14 -
    2.15 -lemma cont_Rep_CFun_app_app [simp]: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s t)"
    2.16 -by (rule cont_Rep_CFun_app [THEN cont2cont_fun])
    2.17 -
    2.18  subsection {* Further operations *}
    2.19  
    2.20  definition