# HG changeset patch
# User huffman
# Date 1291671245 28800
# Node ID ce5d9e73fb983040621d1acb88d663d71bf3f569
# Parent  7a67a8832da81e514534572e9bfad7eb7e93f0a0
instance unit :: domain

diff -r 7a67a8832da8 -r ce5d9e73fb98 src/HOL/HOLCF/Bifinite.thy
--- a/src/HOL/HOLCF/Bifinite.thy	Mon Dec 06 12:53:06 2010 -0800
+++ b/src/HOL/HOLCF/Bifinite.thy	Mon Dec 06 13:34:05 2010 -0800
@@ -618,6 +618,42 @@
   "LIFTDEFL('a::predomain \<times> 'b::predomain) = DEFL('a u \<otimes> 'b u)"
 by (rule liftdefl_prod_def)
 
+subsubsection {* Unit type *}
+
+instantiation unit :: liftdomain
+begin
+
+definition
+  "emb = (\<bottom> :: unit \<rightarrow> udom)"
+
+definition
+  "prj = (\<bottom> :: udom \<rightarrow> unit)"
+
+definition
+  "defl (t::unit itself) = \<bottom>"
+
+definition
+  "(liftemb :: unit u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+  "(liftprj :: udom \<rightarrow> unit u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+  "liftdefl (t::unit itself) = u_defl\<cdot>DEFL(unit)"
+
+instance
+using liftemb_unit_def liftprj_unit_def liftdefl_unit_def
+proof (rule liftdomain_class_intro)
+  show "ep_pair emb (prj :: udom \<rightarrow> unit)"
+    unfolding emb_unit_def prj_unit_def
+    by (simp add: ep_pair.intro)
+next
+  show "cast\<cdot>DEFL(unit) = emb oo (prj :: udom \<rightarrow> unit)"
+    unfolding emb_unit_def prj_unit_def defl_unit_def by simp
+qed
+
+end
+
 subsubsection {* Discrete cpo *}
 
 definition discr_approx :: "nat \<Rightarrow> 'a::countable discr u \<rightarrow> 'a discr u"