|
(* Title: HOL/HOLCF/Discrete.thy
Author: Tobias Nipkow
*)
section \<open>Discrete cpo types\<close>
theory Discrete
imports Cont
begin
datatype 'a discr = Discr "'a :: type"
subsection \<open>Discrete cpo class instance\<close>
instantiation discr :: (type) discrete_cpo
begin
definition "((\) :: 'a discr \ 'a discr \ bool) = (=)"
instance
by standard (simp add: below_discr_def)
end
subsection \<open>\emph{undiscr}\<close>
definition undiscr :: "('a::type)discr \ 'a"
where "undiscr x = (case x of Discr y \ y)"
lemma undiscr_Discr [simp]: "undiscr (Discr x) = x"
by (simp add: undiscr_def)
lemma Discr_undiscr [simp]: "Discr (undiscr y) = y"
by (induct y) simp
end
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
