remove unused lemmas
authorhuffman
Thu Oct 07 13:22:13 2010 -0700 (2010-10-07)
changeset 39983910d3ea1efa8
parent 39982 5681f840688b
child 39984 0300d5170622
remove unused lemmas
src/HOLCF/Completion.thy
     1.1 --- a/src/HOLCF/Completion.thy	Thu Oct 07 13:19:45 2010 -0700
     1.2 +++ b/src/HOLCF/Completion.thy	Thu Oct 07 13:22:13 2010 -0700
     1.3 @@ -40,17 +40,6 @@
     1.4    "\<lbrakk>ideal A; x \<preceq> y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A"
     1.5  unfolding ideal_def by fast
     1.6  
     1.7 -lemma ideal_directed_finite:
     1.8 -  assumes A: "ideal A"
     1.9 -  shows "\<lbrakk>finite U; U \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. \<forall>x\<in>U. x \<preceq> z"
    1.10 -apply (induct U set: finite)
    1.11 -apply (simp add: idealD1 [OF A])
    1.12 -apply (simp, clarify, rename_tac y)
    1.13 -apply (drule (1) idealD2 [OF A])
    1.14 -apply (clarify, erule_tac x=z in rev_bexI)
    1.15 -apply (fast intro: r_trans)
    1.16 -done
    1.17 -
    1.18  lemma ideal_principal: "ideal {x. x \<preceq> z}"
    1.19  apply (rule idealI)
    1.20  apply (rule_tac x=z in exI)
    1.21 @@ -63,20 +52,6 @@
    1.22  lemma ex_ideal: "\<exists>A. ideal A"
    1.23  by (rule exI, rule ideal_principal)
    1.24  
    1.25 -lemma directed_image_ideal:
    1.26 -  assumes A: "ideal A"
    1.27 -  assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y"
    1.28 -  shows "directed (f ` A)"
    1.29 -apply (rule directedI)
    1.30 -apply (cut_tac idealD1 [OF A], fast)
    1.31 -apply (clarify, rename_tac a b)
    1.32 -apply (drule (1) idealD2 [OF A])
    1.33 -apply (clarify, rename_tac c)
    1.34 -apply (rule_tac x="f c" in rev_bexI)
    1.35 -apply (erule imageI)
    1.36 -apply (simp add: f)
    1.37 -done
    1.38 -
    1.39  lemma lub_image_principal:
    1.40    assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y"
    1.41    shows "(\<Squnion>x\<in>{x. x \<preceq> y}. f x) = f y"
    1.42 @@ -227,10 +202,6 @@
    1.43    "\<forall>i. Y i \<preceq> Y (Suc i) \<Longrightarrow> chain (\<lambda>i. principal (Y i))"
    1.44  by (simp add: chainI principal_mono)
    1.45  
    1.46 -lemma belowI: "(\<And>a. principal a \<sqsubseteq> x \<Longrightarrow> principal a \<sqsubseteq> u) \<Longrightarrow> x \<sqsubseteq> u"
    1.47 -unfolding principal_below_iff_mem_rep
    1.48 -by (simp add: below_def subset_eq)
    1.49 -
    1.50  lemma lub_principal_rep: "principal ` rep x <<| x"
    1.51  apply (rule is_lubI)
    1.52  apply (rule ub_imageI)