remove unused constant 'directed'
authorhuffman
Mon Oct 11 16:14:15 2010 -0700 (2010-10-11)
changeset 400009c6ad000dc89
parent 39999 e3948547b541
child 40001 666c3751227c
remove unused constant 'directed'
src/HOLCF/Porder.thy
     1.1 --- a/src/HOLCF/Porder.thy	Mon Oct 11 09:54:04 2010 -0700
     1.2 +++ b/src/HOLCF/Porder.thy	Mon Oct 11 16:14:15 2010 -0700
     1.3 @@ -344,87 +344,6 @@
     1.4  lemma lub_chain_maxelem: "\<lbrakk>Y i = c; \<forall>i. Y i \<sqsubseteq> c\<rbrakk> \<Longrightarrow> lub (range Y) = c"
     1.5    by (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI)
     1.6  
     1.7 -subsection {* Directed sets *}
     1.8 -
     1.9 -definition directed :: "'a set \<Rightarrow> bool" where
    1.10 -  "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)"
    1.11 -
    1.12 -lemma directedI:
    1.13 -  assumes 1: "\<exists>z. z \<in> S"
    1.14 -  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"
    1.15 -  shows "directed S"
    1.16 -  unfolding directed_def using prems by fast
    1.17 -
    1.18 -lemma directedD1: "directed S \<Longrightarrow> \<exists>z. z \<in> S"
    1.19 -  unfolding directed_def by fast
    1.20 -
    1.21 -lemma directedD2: "\<lbrakk>directed S; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> \<exists>z\<in>S. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
    1.22 -  unfolding directed_def by fast
    1.23 -
    1.24 -lemma directedE1:
    1.25 -  assumes S: "directed S"
    1.26 -  obtains z where "z \<in> S"
    1.27 -  by (insert directedD1 [OF S], fast)
    1.28 -
    1.29 -lemma directedE2:
    1.30 -  assumes S: "directed S"
    1.31 -  assumes x: "x \<in> S" and y: "y \<in> S"
    1.32 -  obtains z where "z \<in> S" "x \<sqsubseteq> z" "y \<sqsubseteq> z"
    1.33 -  by (insert directedD2 [OF S x y], fast)
    1.34 -
    1.35 -lemma directed_finiteI:
    1.36 -  assumes U: "\<And>U. \<lbrakk>finite U; U \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>z\<in>S. U <| z"
    1.37 -  shows "directed S"
    1.38 -proof (rule directedI)
    1.39 -  have "finite {}" and "{} \<subseteq> S" by simp_all
    1.40 -  hence "\<exists>z\<in>S. {} <| z" by (rule U)
    1.41 -  thus "\<exists>z. z \<in> S" by simp
    1.42 -next
    1.43 -  fix x y
    1.44 -  assume "x \<in> S" and "y \<in> S"
    1.45 -  hence "finite {x, y}" and "{x, y} \<subseteq> S" by simp_all
    1.46 -  hence "\<exists>z\<in>S. {x, y} <| z" by (rule U)
    1.47 -  thus "\<exists>z\<in>S. x \<sqsubseteq> z \<and> y \<sqsubseteq> z" by simp
    1.48 -qed
    1.49 -
    1.50 -lemma directed_finiteD:
    1.51 -  assumes S: "directed S"
    1.52 -  shows "\<lbrakk>finite U; U \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>z\<in>S. U <| z"
    1.53 -proof (induct U set: finite)
    1.54 -  case empty
    1.55 -  from S have "\<exists>z. z \<in> S" by (rule directedD1)
    1.56 -  thus "\<exists>z\<in>S. {} <| z" by simp
    1.57 -next
    1.58 -  case (insert x F)
    1.59 -  from `insert x F \<subseteq> S`
    1.60 -  have xS: "x \<in> S" and FS: "F \<subseteq> S" by simp_all
    1.61 -  from FS have "\<exists>y\<in>S. F <| y" by fact
    1.62 -  then obtain y where yS: "y \<in> S" and Fy: "F <| y" ..
    1.63 -  obtain z where zS: "z \<in> S" and xz: "x \<sqsubseteq> z" and yz: "y \<sqsubseteq> z"
    1.64 -    using S xS yS by (rule directedE2)
    1.65 -  from Fy yz have "F <| z" by (rule is_ub_upward)
    1.66 -  with xz have "insert x F <| z" by simp
    1.67 -  with zS show "\<exists>z\<in>S. insert x F <| z" ..
    1.68 -qed
    1.69 -
    1.70 -lemma not_directed_empty [simp]: "\<not> directed {}"
    1.71 -  by (rule notI, drule directedD1, simp)
    1.72 -
    1.73 -lemma directed_singleton: "directed {x}"
    1.74 -  by (rule directedI, auto)
    1.75 -
    1.76 -lemma directed_bin: "x \<sqsubseteq> y \<Longrightarrow> directed {x, y}"
    1.77 -  by (rule directedI, auto)
    1.78 -
    1.79 -lemma directed_chain: "chain S \<Longrightarrow> directed (range S)"
    1.80 -apply (rule directedI)
    1.81 -apply (rule_tac x="S 0" in exI, simp)
    1.82 -apply (clarify, rename_tac m n)
    1.83 -apply (rule_tac x="S (max m n)" in bexI)
    1.84 -apply (simp add: chain_mono)
    1.85 -apply simp
    1.86 -done
    1.87 -
    1.88  text {* lemmata for improved admissibility introdution rule *}
    1.89  
    1.90  lemma infinite_chain_adm_lemma: