整列順序で稠密順序な例。

Well_Dense_Order.thy

theory "Well_Dense_Order" imports Main begin

datatype a = A

text "a は整列順序である。"
instantiation a :: wellorder
begin

definition less_eq_a :: "a ⇒ a ⇒ bool"
  where "less_eq_a a b ≡ True"

definition less_a :: "a ⇒ a ⇒ bool"
  where "less_a a b ≡ False"

instance proof (standard; unfold less_eq_a_def less_a_def; simp)
  fix x y :: a show "x = y" by (metis (full_types) a.exhaust)
qed
end

text "a は稠密順序である"
instantiation a :: dense_order
begin
instance proof (standard; unfold less_eq_a_def less_a_def; simp)
qed
end

end