remove unused lemmas cont_fst_snd_D1, cont_fst_snd_D2
authorhuffman
Tue Oct 12 05:25:21 2010 -0700 (2010-10-12)
changeset 40003427106657e04
parent 40002 c5b5f7a3a3b1
child 40004 9f6ed6840e8d
remove unused lemmas cont_fst_snd_D1, cont_fst_snd_D2
src/HOLCF/Cfun.thy
src/HOLCF/Product_Cpo.thy
     1.1 --- a/src/HOLCF/Cfun.thy	Mon Oct 11 21:35:31 2010 -0700
     1.2 +++ b/src/HOLCF/Cfun.thy	Tue Oct 12 05:25:21 2010 -0700
     1.3 @@ -600,10 +600,10 @@
     1.4  using f
     1.5  proof (rule cont2cont_Let)
     1.6    fix x show "cont (\<lambda>y. g x y)"
     1.7 -    using g by (rule cont_fst_snd_D2)
     1.8 +    using g by (simp add: prod_cont_iff)
     1.9  next
    1.10    fix y show "cont (\<lambda>x. g x y)"
    1.11 -    using g by (rule cont_fst_snd_D1)
    1.12 +    using g by (simp add: prod_cont_iff)
    1.13  qed
    1.14  
    1.15  text {* The simple version (suggested by Joachim Breitner) is needed if
     2.1 --- a/src/HOLCF/Product_Cpo.thy	Mon Oct 11 21:35:31 2010 -0700
     2.2 +++ b/src/HOLCF/Product_Cpo.thy	Tue Oct 12 05:25:21 2010 -0700
     2.3 @@ -267,14 +267,6 @@
     2.4  apply (simp only: prod_contI)
     2.5  done
     2.6  
     2.7 -lemma cont_fst_snd_D1:
     2.8 -  "cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>x. f x y)"
     2.9 -by (drule cont_compose [OF _ cont_pair1], simp)
    2.10 -
    2.11 -lemma cont_fst_snd_D2:
    2.12 -  "cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>y. f x y)"
    2.13 -by (drule cont_compose [OF _ cont_pair2], simp)
    2.14 -
    2.15  lemma cont2cont_prod_case' [simp, cont2cont]:
    2.16    assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))"
    2.17    assumes g: "cont (\<lambda>x. g x)"