# 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"
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 \<notsqsubseteq> ⊥"

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 ≠ ⊥"

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