Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
整列順序で稠密順序な例。
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment