(* Title: HOLCF/One.thy ID: $Id: One.thy,v 1.14 2005/07/07 18:41:12 huffman Exp $ Author: Oscar Slotosch The unit domain. *) header {* The unit domain *} theory One imports Lift begin types one = "unit lift" constdefs ONE :: "one" "ONE ≡ Def ()" translations "one" <= (type) "unit lift" text {* Exhaustion and Elimination for type @{typ one} *} lemma Exh_one: "t = ⊥ ∨ t = ONE" apply (unfold ONE_def) apply (induct t) apply simp apply simp done lemma oneE: "[|p = ⊥ ==> Q; p = ONE ==> Q|] ==> Q" apply (rule Exh_one [THEN disjE]) apply fast apply fast done lemma dist_less_one [simp]: "¬ ONE \<sqsubseteq> ⊥" apply (unfold ONE_def) apply simp done lemma dist_eq_one [simp]: "ONE ≠ ⊥" "⊥ ≠ ONE" apply (unfold ONE_def) apply simp_all done end
lemma Exh_one:
t = UU ∨ t = ONE
lemma oneE:
[| p = UU ==> Q; p = ONE ==> Q |] ==> Q
lemma dist_less_one:
¬ ONE << UU
lemma dist_eq_one:
ONE ≠ UU
UU ≠ ONE