Theory One

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