Quelle  One.thy   Sprache: Isabelle

(*  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 🍋‹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 \ \"
  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 🍋‹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