# Theory One

theory One
imports Lift
```(*  Title:      HOL/HOLCF/One.thy
Author:     Oscar Slotosch
*)

section ‹The unit domain›

theory One
imports Lift
begin

type_synonym
one = "unit lift"

translations
(type) "one" <= (type) "unit lift"

definition ONE :: "one"
where "ONE == Def ()"

text ‹Exhaustion and Elimination for type @{typ one}›

lemma Exh_one: "t = ⊥ ∨ t = ONE"
unfolding ONE_def by (induct t) simp_all

lemma oneE [case_names bottom ONE]: "⟦p = ⊥ ⟹ Q; p = ONE ⟹ Q⟧ ⟹ Q"
unfolding ONE_def by (induct p) simp_all

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 \<notsqsubseteq> ⊥"
unfolding ONE_def by simp

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 ≠ ⊥"
unfolding ONE_def by simp

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 ‹Case analysis function for type @{typ one}›

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) = ⊥"