|
(* Title: HOL/HOLCF/One.thy
Author: Oscar Slotosch
*)
section \<open>The unit domain\<close>
theory One
imports Lift
begin
type_synonym one = "unit lift"
translations
(type) "one" \<leftharpoondown> (type) "unit lift"
definition ONE :: "one"
where "ONE \ Def ()"
text \<open>Exhaustion and Elimination for type \<^typ>\<open>one\<close>\<close>
lemma Exh_one: "t = \ \ t = ONE"
by (induct t) (simp_all add: ONE_def)
lemma oneE [case_names bottom ONE]: "\p = \ \ Q; p = ONE \ Q\ \ Q"
by (induct p) (simp_all add: ONE_def)
lemma one_induct [case_names bottom ONE]: "P \ \ P ONE \ P x"
by (cases x rule: oneE) simp_all
lemma dist_below_one [simp]: "ONE \ \"
by (simp add: ONE_def)
lemma below_ONE [simp]: "x \ ONE"
by (induct x rule: one_induct) simp_all
lemma ONE_below_iff [simp]: "ONE \ x \ x = ONE"
by (induct x rule: one_induct) simp_all
lemma ONE_defined [simp]: "ONE \ \"
by (simp add: ONE_def)
lemma one_neq_iffs [simp]:
"x \ ONE \ x = \"
"ONE \ x \ x = \"
"x \ \ \ x = ONE"
"\ \ x \ x = ONE"
by (induct x rule: one_induct) simp_all
lemma compact_ONE: "compact ONE"
by (rule compact_chfin)
text \<open>Case analysis function for type \<^typ>\<open>one\<close>\<close>
definition one_case :: "'a::pcpo \ one \ 'a"
where "one_case = (\ a x. seq\x\a)"
translations
"case x of XCONST ONE \ t" \ "CONST one_case\t\x"
"case x of XCONST ONE :: 'a \ t" \ "CONST one_case\t\x"
"\ (XCONST ONE). t" \ "CONST one_case\t"
lemma one_case1 [simp]: "(case \ of ONE \ t) = \"
by (simp add: one_case_def)
lemma one_case2 [simp]: "(case ONE of ONE \ t) = t"
by (simp add: one_case_def)
lemma one_case3 [simp]: "(case x of ONE \ ONE) = x"
by (induct x rule: one_induct) simp_all
end
¤ Dauer der Verarbeitung: 0.0 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.
|
