src/HOL/Orderings.thy
changeset 51329 4a3c453f99a1
parent 51263 31e786e0e6a7
child 51487 f4bfdee99304
     1.1 --- a/src/HOL/Orderings.thy	Wed Feb 20 12:04:42 2013 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Wed Feb 20 12:04:42 2013 +0100
     1.3 @@ -1135,10 +1135,10 @@
     1.4  
     1.5  subsection {* Dense orders *}
     1.6  
     1.7 -class dense_linorder = linorder + 
     1.8 -  assumes gt_ex: "\<exists>y. x < y" 
     1.9 -  and lt_ex: "\<exists>y. y < x"
    1.10 -  and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
    1.11 +class inner_dense_order = order +
    1.12 +  assumes dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
    1.13 +
    1.14 +class inner_dense_linorder = linorder + inner_dense_order
    1.15  begin
    1.16  
    1.17  lemma dense_le:
    1.18 @@ -1175,8 +1175,50 @@
    1.19    qed
    1.20  qed
    1.21  
    1.22 +lemma dense_ge:
    1.23 +  fixes y z :: 'a
    1.24 +  assumes "\<And>x. z < x \<Longrightarrow> y \<le> x"
    1.25 +  shows "y \<le> z"
    1.26 +proof (rule ccontr)
    1.27 +  assume "\<not> ?thesis"
    1.28 +  hence "z < y" by simp
    1.29 +  from dense[OF this]
    1.30 +  obtain x where "x < y" and "z < x" by safe
    1.31 +  moreover have "y \<le> x" using assms[OF `z < x`] .
    1.32 +  ultimately show False by auto
    1.33 +qed
    1.34 +
    1.35 +lemma dense_ge_bounded:
    1.36 +  fixes x y z :: 'a
    1.37 +  assumes "z < x"
    1.38 +  assumes *: "\<And>w. \<lbrakk> z < w ; w < x \<rbrakk> \<Longrightarrow> y \<le> w"
    1.39 +  shows "y \<le> z"
    1.40 +proof (rule dense_ge)
    1.41 +  fix w assume "z < w"
    1.42 +  from dense[OF `z < x`] obtain u where "z < u" "u < x" by safe
    1.43 +  from linear[of u w]
    1.44 +  show "y \<le> w"
    1.45 +  proof (rule disjE)
    1.46 +    assume "w \<le> u"
    1.47 +    from `z < w` le_less_trans[OF `w \<le> u` `u < x`]
    1.48 +    show "y \<le> w" by (rule *)
    1.49 +  next
    1.50 +    assume "u \<le> w"
    1.51 +    from *[OF `z < u` `u < x`] `u \<le> w`
    1.52 +    show "y \<le> w" by (rule order_trans)
    1.53 +  qed
    1.54 +qed
    1.55 +
    1.56  end
    1.57  
    1.58 +class no_top = order + 
    1.59 +  assumes gt_ex: "\<exists>y. x < y"
    1.60 +
    1.61 +class no_bot = order + 
    1.62 +  assumes lt_ex: "\<exists>y. y < x"
    1.63 +
    1.64 +class dense_linorder = inner_dense_linorder + no_top + no_bot
    1.65 +
    1.66  subsection {* Wellorders *}
    1.67  
    1.68  class wellorder = linorder +