# HG changeset patch
# User huffman
# Date 1286838855 25200
# Node ID 9c6ad000dc890923d775d7440213e040d8975703
# Parent  e3948547b541fb5d71edc0f5a679ef89de40047d
remove unused constant 'directed'

diff -r e3948547b541 -r 9c6ad000dc89 src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Mon Oct 11 09:54:04 2010 -0700
+++ b/src/HOLCF/Porder.thy	Mon Oct 11 16:14:15 2010 -0700
@@ -344,87 +344,6 @@
 lemma lub_chain_maxelem: "\<lbrakk>Y i = c; \<forall>i. Y i \<sqsubseteq> c\<rbrakk> \<Longrightarrow> lub (range Y) = c"
   by (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI)
 
-subsection {* Directed sets *}
-
-definition directed :: "'a set \<Rightarrow> bool" where
-  "directed S \<longleftrightarrow> (\<exists>x. x \<in> S) \<and> (\<forall>x\<in>S. \<forall>y\<in>S. \<exists>z\<in>S. x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
-
-lemma directedI:
-  assumes 1: "\<exists>z. z \<in> S"
-  assumes 2: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> \<exists>z\<in>S. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
-  shows "directed S"
-  unfolding directed_def using prems by fast
-
-lemma directedD1: "directed S \<Longrightarrow> \<exists>z. z \<in> S"
-  unfolding directed_def by fast
-
-lemma directedD2: "\<lbrakk>directed S; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> \<exists>z\<in>S. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
-  unfolding directed_def by fast
-
-lemma directedE1:
-  assumes S: "directed S"
-  obtains z where "z \<in> S"
-  by (insert directedD1 [OF S], fast)
-
-lemma directedE2:
-  assumes S: "directed S"
-  assumes x: "x \<in> S" and y: "y \<in> S"
-  obtains z where "z \<in> S" "x \<sqsubseteq> z" "y \<sqsubseteq> z"
-  by (insert directedD2 [OF S x y], fast)
-
-lemma directed_finiteI:
-  assumes U: "\<And>U. \<lbrakk>finite U; U \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>z\<in>S. U <| z"
-  shows "directed S"
-proof (rule directedI)
-  have "finite {}" and "{} \<subseteq> S" by simp_all
-  hence "\<exists>z\<in>S. {} <| z" by (rule U)
-  thus "\<exists>z. z \<in> S" by simp
-next
-  fix x y
-  assume "x \<in> S" and "y \<in> S"
-  hence "finite {x, y}" and "{x, y} \<subseteq> S" by simp_all
-  hence "\<exists>z\<in>S. {x, y} <| z" by (rule U)
-  thus "\<exists>z\<in>S. x \<sqsubseteq> z \<and> y \<sqsubseteq> z" by simp
-qed
-
-lemma directed_finiteD:
-  assumes S: "directed S"
-  shows "\<lbrakk>finite U; U \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>z\<in>S. U <| z"
-proof (induct U set: finite)
-  case empty
-  from S have "\<exists>z. z \<in> S" by (rule directedD1)
-  thus "\<exists>z\<in>S. {} <| z" by simp
-next
-  case (insert x F)
-  from `insert x F \<subseteq> S`
-  have xS: "x \<in> S" and FS: "F \<subseteq> S" by simp_all
-  from FS have "\<exists>y\<in>S. F <| y" by fact
-  then obtain y where yS: "y \<in> S" and Fy: "F <| y" ..
-  obtain z where zS: "z \<in> S" and xz: "x \<sqsubseteq> z" and yz: "y \<sqsubseteq> z"
-    using S xS yS by (rule directedE2)
-  from Fy yz have "F <| z" by (rule is_ub_upward)
-  with xz have "insert x F <| z" by simp
-  with zS show "\<exists>z\<in>S. insert x F <| z" ..
-qed
-
-lemma not_directed_empty [simp]: "\<not> directed {}"
-  by (rule notI, drule directedD1, simp)
-
-lemma directed_singleton: "directed {x}"
-  by (rule directedI, auto)
-
-lemma directed_bin: "x \<sqsubseteq> y \<Longrightarrow> directed {x, y}"
-  by (rule directedI, auto)
-
-lemma directed_chain: "chain S \<Longrightarrow> directed (range S)"
-apply (rule directedI)
-apply (rule_tac x="S 0" in exI, simp)
-apply (clarify, rename_tac m n)
-apply (rule_tac x="S (max m n)" in bexI)
-apply (simp add: chain_mono)
-apply simp
-done
-
 text {* lemmata for improved admissibility introdution rule *}
 
 lemma infinite_chain_adm_lemma: