remove some junk that made it in by accient
authorhuffman
Thu Oct 07 13:18:48 2010 -0700 (2010-10-07)
changeset 39981fdff0444fa7d
parent 39974 b525988432e9
child 39982 5681f840688b
remove some junk that made it in by accient
src/HOLCF/CompactBasis.thy
     1.1 --- a/src/HOLCF/CompactBasis.thy	Wed Oct 06 10:49:27 2010 -0700
     1.2 +++ b/src/HOLCF/CompactBasis.thy	Thu Oct 07 13:18:48 2010 -0700
     1.3 @@ -108,26 +108,4 @@
     1.4      by (simp add: image_Un fold1_Un2)
     1.5  qed
     1.6  
     1.7 -subsection {* Lemmas for proving if-and-only-if inequalities *}
     1.8 -
     1.9 -lemma chain_max_below_iff:
    1.10 -  assumes Y: "chain Y" shows "Y (max i j) \<sqsubseteq> x \<longleftrightarrow> Y i \<sqsubseteq> x \<and> Y j \<sqsubseteq> x"
    1.11 -apply auto
    1.12 -apply (erule below_trans [OF chain_mono [OF Y le_maxI1]])
    1.13 -apply (erule below_trans [OF chain_mono [OF Y le_maxI2]])
    1.14 -apply (simp add: max_def)
    1.15 -done
    1.16 -
    1.17 -lemma all_ex_below_disj_iff:
    1.18 -  assumes "chain X" and "chain Y"
    1.19 -  shows "(\<forall>i. \<exists>j. X i \<sqsubseteq> Z j \<or> Y i \<sqsubseteq> Z j) \<longleftrightarrow>
    1.20 -         (\<forall>i. \<exists>j. X i \<sqsubseteq> Z j) \<or> (\<forall>i. \<exists>j. Y i \<sqsubseteq> Z j)"
    1.21 -by (metis chain_max_below_iff assms)
    1.22 -
    1.23 -lemma all_ex_below_conj_iff:
    1.24 -  assumes "chain X" and "chain Y" and "chain Z"
    1.25 -  shows "(\<forall>i. \<exists>j. X i \<sqsubseteq> Z j \<and> Y i \<sqsubseteq> Z j) \<longleftrightarrow>
    1.26 -         (\<forall>i. \<exists>j. X i \<sqsubseteq> Z j) \<and> (\<forall>i. \<exists>j. Y i \<sqsubseteq> Z j)"
    1.27 -oops
    1.28 -
    1.29  end