src/HOL/Orderings.thy
changeset 35579 cc9a5a0ab5ea
parent 35364 b8c62d60195c
child 35828 46cfc4b8112e
     1.1 --- a/src/HOL/Orderings.thy	Thu Mar 04 17:28:45 2010 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Thu Mar 04 18:42:39 2010 +0100
     1.3 @@ -1097,7 +1097,43 @@
     1.4    assumes gt_ex: "\<exists>y. x < y" 
     1.5    and lt_ex: "\<exists>y. y < x"
     1.6    and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
     1.7 +begin
     1.8  
     1.9 +lemma dense_le:
    1.10 +  fixes y z :: 'a
    1.11 +  assumes "\<And>x. x < y \<Longrightarrow> x \<le> z"
    1.12 +  shows "y \<le> z"
    1.13 +proof (rule ccontr)
    1.14 +  assume "\<not> ?thesis"
    1.15 +  hence "z < y" by simp
    1.16 +  from dense[OF this]
    1.17 +  obtain x where "x < y" and "z < x" by safe
    1.18 +  moreover have "x \<le> z" using assms[OF `x < y`] .
    1.19 +  ultimately show False by auto
    1.20 +qed
    1.21 +
    1.22 +lemma dense_le_bounded:
    1.23 +  fixes x y z :: 'a
    1.24 +  assumes "x < y"
    1.25 +  assumes *: "\<And>w. \<lbrakk> x < w ; w < y \<rbrakk> \<Longrightarrow> w \<le> z"
    1.26 +  shows "y \<le> z"
    1.27 +proof (rule dense_le)
    1.28 +  fix w assume "w < y"
    1.29 +  from dense[OF `x < y`] obtain u where "x < u" "u < y" by safe
    1.30 +  from linear[of u w]
    1.31 +  show "w \<le> z"
    1.32 +  proof (rule disjE)
    1.33 +    assume "u \<le> w"
    1.34 +    from less_le_trans[OF `x < u` `u \<le> w`] `w < y`
    1.35 +    show "w \<le> z" by (rule *)
    1.36 +  next
    1.37 +    assume "w \<le> u"
    1.38 +    from `w \<le> u` *[OF `x < u` `u < y`]
    1.39 +    show "w \<le> z" by (rule order_trans)
    1.40 +  qed
    1.41 +qed
    1.42 +
    1.43 +end
    1.44  
    1.45  subsection {* Wellorders *}
    1.46