theory "HOLCF-Top"
imports
"~~/src/HOL/HOLCF/HOLCF"
begin
default_sort type
class Top_cpo = cpo +
assumes most: "\x. \y. y \ x"
begin
definition top :: "'a"
where "top = (THE x. \y. y \ x)"
notation (xsymbols)
top ("\")
lemma maximal [iff]: "x \ \"
unfolding top_def
apply (rule the1I2)
apply (rule ex_ex1I)
apply (rule most)
apply (blast intro: below_antisym)
apply simp
done
end
default_sort cpo
lemma above_top_iff [simp]: "(\ \ x) = (x = \)"
by (simp add: po_eq_conv)
lemma eq_top_iff: "(x = \) = (\ \ x)"
by simp
lemma topI: "\ \ x ==> x = \"
by (subst eq_top_iff)
end