remove unneeded lemmas from Fun_Cpo.thy

--- a/src/HOLCF/Cfun.thy	Tue Oct 12 05:48:32 2010 -0700
+++ b/src/HOLCF/Cfun.thy	Tue Oct 12 06:20:05 2010 -0700
@@ -310,10 +310,10 @@
   assumes t: "cont (\<lambda>x. t x)"
   shows "cont (\<lambda>x. (f x)\<cdot>(t x))"
 proof -
-  have "cont (\<lambda>x. Rep_CFun (f x))"
-    using cont_Rep_CFun f by (rule cont2cont_app3)
-  thus "cont (\<lambda>x. (f x)\<cdot>(t x))"
-    using cont_Rep_CFun2 t by (rule cont2cont_app2)
+  have 1: "\<And>y. cont (\<lambda>x. (f x)\<cdot>y)"
+    using cont_Rep_CFun1 f by (rule cont_compose)
+  show "cont (\<lambda>x. (f x)\<cdot>(t x))"
+    using t cont_Rep_CFun2 1 by (rule cont_apply)
 qed
 
 text {* cont2mono Lemma for @{term "%x. LAM y. c1(x)(y)"} *}

--- a/src/HOLCF/Fun_Cpo.thy	Tue Oct 12 05:48:32 2010 -0700
+++ b/src/HOLCF/Fun_Cpo.thy	Tue Oct 12 06:20:05 2010 -0700
@@ -89,12 +89,8 @@
     \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
 by (rule lub_fun [THEN thelubI])
 
-lemma cpo_fun:
-  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x"
-by (rule exI, erule lub_fun)
-
 instance "fun"  :: (type, cpo) cpo
-by intro_classes (rule cpo_fun)
+by intro_classes (rule exI, erule lub_fun)
 
 instance "fun" :: (finite, finite_po) finite_po ..
 
@@ -240,29 +236,4 @@
     \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))"
 by (simp add: thelub_fun ch2ch_lambda)
 
-lemma contlub_abstraction:
-  "\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow>
-    (\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))"
-apply (rule thelub_fun [symmetric])
-apply (simp add: ch2ch_cont)
-done
-
-lemma mono2mono_app:
-  "\<lbrakk>monofun f; \<forall>x. monofun (f x); monofun t\<rbrakk> \<Longrightarrow> monofun (\<lambda>x. (f x) (t x))"
-apply (rule monofunI)
-apply (simp add: monofun_fun monofunE)
-done
-
-lemma cont2cont_app:
-  "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x) (t x))"
-apply (erule cont_apply [where t=t])
-apply (erule spec)
-apply (erule cont2cont_fun)
-done
-
-lemmas cont2cont_app2 = cont2cont_app [rule_format]
-
-lemma cont2cont_app3: "\<lbrakk>cont f; cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. f (t x))"
-by (rule cont2cont_app2 [OF cont_const])
-
 end

--- a/src/HOLCF/Lift.thy	Tue Oct 12 05:48:32 2010 -0700
+++ b/src/HOLCF/Lift.thy	Tue Oct 12 06:20:05 2010 -0700
@@ -139,7 +139,7 @@
 
 lemma cont2cont_flift1 [simp, cont2cont]:
   "\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)"
-apply (rule cont_flift1 [THEN cont2cont_app3])
+apply (rule cont_flift1 [THEN cont_compose])
 apply simp
 done