remove unneeded lemmas from Fun_Cpo.thy
authorhuffman
Tue Oct 12 06:20:05 2010 -0700 (2010-10-12)
changeset 40006116e94f9543b
parent 40005 3e3611136a13
child 40007 bb04a995bbd3
remove unneeded lemmas from Fun_Cpo.thy
src/HOLCF/Cfun.thy
src/HOLCF/Fun_Cpo.thy
src/HOLCF/Lift.thy
     1.1 --- a/src/HOLCF/Cfun.thy	Tue Oct 12 05:48:32 2010 -0700
     1.2 +++ b/src/HOLCF/Cfun.thy	Tue Oct 12 06:20:05 2010 -0700
     1.3 @@ -310,10 +310,10 @@
     1.4    assumes t: "cont (\<lambda>x. t x)"
     1.5    shows "cont (\<lambda>x. (f x)\<cdot>(t x))"
     1.6  proof -
     1.7 -  have "cont (\<lambda>x. Rep_CFun (f x))"
     1.8 -    using cont_Rep_CFun f by (rule cont2cont_app3)
     1.9 -  thus "cont (\<lambda>x. (f x)\<cdot>(t x))"
    1.10 -    using cont_Rep_CFun2 t by (rule cont2cont_app2)
    1.11 +  have 1: "\<And>y. cont (\<lambda>x. (f x)\<cdot>y)"
    1.12 +    using cont_Rep_CFun1 f by (rule cont_compose)
    1.13 +  show "cont (\<lambda>x. (f x)\<cdot>(t x))"
    1.14 +    using t cont_Rep_CFun2 1 by (rule cont_apply)
    1.15  qed
    1.16  
    1.17  text {* cont2mono Lemma for @{term "%x. LAM y. c1(x)(y)"} *}
     2.1 --- a/src/HOLCF/Fun_Cpo.thy	Tue Oct 12 05:48:32 2010 -0700
     2.2 +++ b/src/HOLCF/Fun_Cpo.thy	Tue Oct 12 06:20:05 2010 -0700
     2.3 @@ -89,12 +89,8 @@
     2.4      \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
     2.5  by (rule lub_fun [THEN thelubI])
     2.6  
     2.7 -lemma cpo_fun:
     2.8 -  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x"
     2.9 -by (rule exI, erule lub_fun)
    2.10 -
    2.11  instance "fun"  :: (type, cpo) cpo
    2.12 -by intro_classes (rule cpo_fun)
    2.13 +by intro_classes (rule exI, erule lub_fun)
    2.14  
    2.15  instance "fun" :: (finite, finite_po) finite_po ..
    2.16  
    2.17 @@ -240,29 +236,4 @@
    2.18      \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))"
    2.19  by (simp add: thelub_fun ch2ch_lambda)
    2.20  
    2.21 -lemma contlub_abstraction:
    2.22 -  "\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow>
    2.23 -    (\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))"
    2.24 -apply (rule thelub_fun [symmetric])
    2.25 -apply (simp add: ch2ch_cont)
    2.26 -done
    2.27 -
    2.28 -lemma mono2mono_app:
    2.29 -  "\<lbrakk>monofun f; \<forall>x. monofun (f x); monofun t\<rbrakk> \<Longrightarrow> monofun (\<lambda>x. (f x) (t x))"
    2.30 -apply (rule monofunI)
    2.31 -apply (simp add: monofun_fun monofunE)
    2.32 -done
    2.33 -
    2.34 -lemma cont2cont_app:
    2.35 -  "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x) (t x))"
    2.36 -apply (erule cont_apply [where t=t])
    2.37 -apply (erule spec)
    2.38 -apply (erule cont2cont_fun)
    2.39 -done
    2.40 -
    2.41 -lemmas cont2cont_app2 = cont2cont_app [rule_format]
    2.42 -
    2.43 -lemma cont2cont_app3: "\<lbrakk>cont f; cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. f (t x))"
    2.44 -by (rule cont2cont_app2 [OF cont_const])
    2.45 -
    2.46  end
     3.1 --- a/src/HOLCF/Lift.thy	Tue Oct 12 05:48:32 2010 -0700
     3.2 +++ b/src/HOLCF/Lift.thy	Tue Oct 12 06:20:05 2010 -0700
     3.3 @@ -139,7 +139,7 @@
     3.4  
     3.5  lemma cont2cont_flift1 [simp, cont2cont]:
     3.6    "\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)"
     3.7 -apply (rule cont_flift1 [THEN cont2cont_app3])
     3.8 +apply (rule cont_flift1 [THEN cont_compose])
     3.9  apply simp
    3.10  done
    3.11