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