# HG changeset patch
# User huffman
# Date 1286482933 25200
# Node ID 910d3ea1efa8b6909cc9020249049024b7c284fb
# Parent  5681f840688b9f9c2066c386181cca8058c30262
remove unused lemmas

diff -r 5681f840688b -r 910d3ea1efa8 src/HOLCF/Completion.thy
--- a/src/HOLCF/Completion.thy	Thu Oct 07 13:19:45 2010 -0700
+++ b/src/HOLCF/Completion.thy	Thu Oct 07 13:22:13 2010 -0700
@@ -40,17 +40,6 @@
   "\<lbrakk>ideal A; x \<preceq> y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A"
 unfolding ideal_def by fast
 
-lemma ideal_directed_finite:
-  assumes A: "ideal A"
-  shows "\<lbrakk>finite U; U \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. \<forall>x\<in>U. x \<preceq> z"
-apply (induct U set: finite)
-apply (simp add: idealD1 [OF A])
-apply (simp, clarify, rename_tac y)
-apply (drule (1) idealD2 [OF A])
-apply (clarify, erule_tac x=z in rev_bexI)
-apply (fast intro: r_trans)
-done
-
 lemma ideal_principal: "ideal {x. x \<preceq> z}"
 apply (rule idealI)
 apply (rule_tac x=z in exI)
@@ -63,20 +52,6 @@
 lemma ex_ideal: "\<exists>A. ideal A"
 by (rule exI, rule ideal_principal)
 
-lemma directed_image_ideal:
-  assumes A: "ideal A"
-  assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y"
-  shows "directed (f ` A)"
-apply (rule directedI)
-apply (cut_tac idealD1 [OF A], fast)
-apply (clarify, rename_tac a b)
-apply (drule (1) idealD2 [OF A])
-apply (clarify, rename_tac c)
-apply (rule_tac x="f c" in rev_bexI)
-apply (erule imageI)
-apply (simp add: f)
-done
-
 lemma lub_image_principal:
   assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y"
   shows "(\<Squnion>x\<in>{x. x \<preceq> y}. f x) = f y"
@@ -227,10 +202,6 @@
   "\<forall>i. Y i \<preceq> Y (Suc i) \<Longrightarrow> chain (\<lambda>i. principal (Y i))"
 by (simp add: chainI principal_mono)
 
-lemma belowI: "(\<And>a. principal a \<sqsubseteq> x \<Longrightarrow> principal a \<sqsubseteq> u) \<Longrightarrow> x \<sqsubseteq> u"
-unfolding principal_below_iff_mem_rep
-by (simp add: below_def subset_eq)
-
 lemma lub_principal_rep: "principal ` rep x <<| x"
 apply (rule is_lubI)
 apply (rule ub_imageI)