Well_Not_Dense_Order.thy

theory "Well_Not_Dense_Order" imports Main begin
context wellorder
begin

definition bot :: 'a
  where "bot ≡ LEAST x. True"

sublocale order_bot bot less_eq less
proof standard
  fix a
  show "bot ≤ a"
  unfolding bot_def by (simp add: local.Least_le)
qed

lemma no_dense:
  fixes a :: 'a
  assumes "a ≠ bot"
    and "⋀a b. ⟦⋀x. ⟦a ≤ x; x ≤ b⟧ ⟹ thesis; a ≠ b⟧ ⟹ thesis"
  shows "thesis"
  using assms le_bot by metis

end
end