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.16 Sekunden
(vorverarbeitet)
¤
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.
