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 +
```