minimize imports; move domain class instances for powerdomain types into Powerdomains.thy

--- a/src/HOL/HOLCF/Compact_Basis.thy	Sun Dec 19 06:39:19 2010 -0800
+++ b/src/HOL/HOLCF/Compact_Basis.thy	Sun Dec 19 06:59:01 2010 -0800
@@ -5,7 +5,7 @@
 header {* A compact basis for powerdomains *}
 
 theory Compact_Basis
-imports Representable
+imports Universal
 begin
 
 default_sort bifinite

--- a/src/HOL/HOLCF/ConvexPD.thy	Sun Dec 19 06:39:19 2010 -0800
+++ b/src/HOL/HOLCF/ConvexPD.thy	Sun Dec 19 06:59:01 2010 -0800
@@ -466,7 +466,7 @@
     by (rule finite_range_imp_finite_fixes)
 qed
 
-subsection {* Convex powerdomain is a domain *}
+subsection {* Convex powerdomain is bifinite *}
 
 lemma approx_chain_convex_map:
   assumes "approx_chain a"
@@ -481,66 +481,6 @@
     by (fast intro!: approx_chain_convex_map)
 qed
 
-definition
-  convex_approx :: "nat \<Rightarrow> udom convex_pd \<rightarrow> udom convex_pd"
-where
-  "convex_approx = (\<lambda>i. convex_map\<cdot>(udom_approx i))"
-
-lemma convex_approx: "approx_chain convex_approx"
-using convex_map_ID finite_deflation_convex_map
-unfolding convex_approx_def by (rule approx_chain_lemma1)
-
-definition convex_defl :: "udom defl \<rightarrow> udom defl"
-where "convex_defl = defl_fun1 convex_approx convex_map"
-
-lemma cast_convex_defl:
-  "cast\<cdot>(convex_defl\<cdot>A) =
-    udom_emb convex_approx oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj convex_approx"
-using convex_approx finite_deflation_convex_map
-unfolding convex_defl_def by (rule cast_defl_fun1)
-
-instantiation convex_pd :: ("domain") liftdomain
-begin
-
-definition
-  "emb = udom_emb convex_approx oo convex_map\<cdot>emb"
-
-definition
-  "prj = convex_map\<cdot>prj oo udom_prj convex_approx"
-
-definition
-  "defl (t::'a convex_pd itself) = convex_defl\<cdot>DEFL('a)"
-
-definition
-  "(liftemb :: 'a convex_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
-
-definition
-  "(liftprj :: udom \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj oo udom_prj u_approx"
-
-definition
-  "liftdefl (t::'a convex_pd itself) = u_defl\<cdot>DEFL('a convex_pd)"
-
-instance
-using liftemb_convex_pd_def liftprj_convex_pd_def liftdefl_convex_pd_def
-proof (rule liftdomain_class_intro)
-  show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)"
-    unfolding emb_convex_pd_def prj_convex_pd_def
-    using ep_pair_udom [OF convex_approx]
-    by (intro ep_pair_comp ep_pair_convex_map ep_pair_emb_prj)
-next
-  show "cast\<cdot>DEFL('a convex_pd) = emb oo (prj :: udom \<rightarrow> 'a convex_pd)"
-    unfolding emb_convex_pd_def prj_convex_pd_def defl_convex_pd_def cast_convex_defl
-    by (simp add: cast_DEFL oo_def cfun_eq_iff convex_map_map)
-qed
-
-end
-
-text {* DEFL of type constructor = type combinator *}
-
-lemma DEFL_convex: "DEFL('a::domain convex_pd) = convex_defl\<cdot>DEFL('a)"
-by (rule defl_convex_pd_def)
-
-
 subsection {* Join *}
 
 definition

--- a/src/HOL/HOLCF/LowerPD.thy	Sun Dec 19 06:39:19 2010 -0800
+++ b/src/HOL/HOLCF/LowerPD.thy	Sun Dec 19 06:59:01 2010 -0800
@@ -458,7 +458,7 @@
     by (rule finite_range_imp_finite_fixes)
 qed
 
-subsection {* Lower powerdomain is a domain *}
+subsection {* Lower powerdomain is bifinite *}
 
 lemma approx_chain_lower_map:
   assumes "approx_chain a"
@@ -473,64 +473,6 @@
     by (fast intro!: approx_chain_lower_map)
 qed
 
-definition
-  lower_approx :: "nat \<Rightarrow> udom lower_pd \<rightarrow> udom lower_pd"
-where
-  "lower_approx = (\<lambda>i. lower_map\<cdot>(udom_approx i))"
-
-lemma lower_approx: "approx_chain lower_approx"
-using lower_map_ID finite_deflation_lower_map
-unfolding lower_approx_def by (rule approx_chain_lemma1)
-
-definition lower_defl :: "udom defl \<rightarrow> udom defl"
-where "lower_defl = defl_fun1 lower_approx lower_map"
-
-lemma cast_lower_defl:
-  "cast\<cdot>(lower_defl\<cdot>A) =
-    udom_emb lower_approx oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj lower_approx"
-using lower_approx finite_deflation_lower_map
-unfolding lower_defl_def by (rule cast_defl_fun1)
-
-instantiation lower_pd :: ("domain") liftdomain
-begin
-
-definition
-  "emb = udom_emb lower_approx oo lower_map\<cdot>emb"
-
-definition
-  "prj = lower_map\<cdot>prj oo udom_prj lower_approx"
-
-definition
-  "defl (t::'a lower_pd itself) = lower_defl\<cdot>DEFL('a)"
-
-definition
-  "(liftemb :: 'a lower_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
-
-definition
-  "(liftprj :: udom \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj oo udom_prj u_approx"
-
-definition
-  "liftdefl (t::'a lower_pd itself) = u_defl\<cdot>DEFL('a lower_pd)"
-
-instance
-using liftemb_lower_pd_def liftprj_lower_pd_def liftdefl_lower_pd_def
-proof (rule liftdomain_class_intro)
-  show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)"
-    unfolding emb_lower_pd_def prj_lower_pd_def
-    using ep_pair_udom [OF lower_approx]
-    by (intro ep_pair_comp ep_pair_lower_map ep_pair_emb_prj)
-next
-  show "cast\<cdot>DEFL('a lower_pd) = emb oo (prj :: udom \<rightarrow> 'a lower_pd)"
-    unfolding emb_lower_pd_def prj_lower_pd_def defl_lower_pd_def cast_lower_defl
-    by (simp add: cast_DEFL oo_def cfun_eq_iff lower_map_map)
-qed
-
-end
-
-lemma DEFL_lower: "DEFL('a::domain lower_pd) = lower_defl\<cdot>DEFL('a)"
-by (rule defl_lower_pd_def)
-
-
 subsection {* Join *}
 
 definition

--- a/src/HOL/HOLCF/Powerdomains.thy	Sun Dec 19 06:39:19 2010 -0800
+++ b/src/HOL/HOLCF/Powerdomains.thy	Sun Dec 19 06:59:01 2010 -0800
@@ -8,6 +8,179 @@
 imports ConvexPD Domain
 begin
 
+subsection {* Universal domain embeddings *}
+
+definition upper_approx :: "nat \<Rightarrow> udom upper_pd \<rightarrow> udom upper_pd"
+  where "upper_approx = (\<lambda>i. upper_map\<cdot>(udom_approx i))"
+
+definition lower_approx :: "nat \<Rightarrow> udom lower_pd \<rightarrow> udom lower_pd"
+  where "lower_approx = (\<lambda>i. lower_map\<cdot>(udom_approx i))"
+
+definition convex_approx :: "nat \<Rightarrow> udom convex_pd \<rightarrow> udom convex_pd"
+  where "convex_approx = (\<lambda>i. convex_map\<cdot>(udom_approx i))"
+
+lemma upper_approx: "approx_chain upper_approx"
+  using upper_map_ID finite_deflation_upper_map
+  unfolding upper_approx_def by (rule approx_chain_lemma1)
+
+lemma lower_approx: "approx_chain lower_approx"
+  using lower_map_ID finite_deflation_lower_map
+  unfolding lower_approx_def by (rule approx_chain_lemma1)
+
+lemma convex_approx: "approx_chain convex_approx"
+  using convex_map_ID finite_deflation_convex_map
+  unfolding convex_approx_def by (rule approx_chain_lemma1)
+
+subsection {* Deflation combinators *}
+
+definition upper_defl :: "udom defl \<rightarrow> udom defl"
+  where "upper_defl = defl_fun1 upper_approx upper_map"
+
+definition lower_defl :: "udom defl \<rightarrow> udom defl"
+  where "lower_defl = defl_fun1 lower_approx lower_map"
+
+definition convex_defl :: "udom defl \<rightarrow> udom defl"
+  where "convex_defl = defl_fun1 convex_approx convex_map"
+
+lemma cast_upper_defl:
+  "cast\<cdot>(upper_defl\<cdot>A) =
+    udom_emb upper_approx oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj upper_approx"
+using upper_approx finite_deflation_upper_map
+unfolding upper_defl_def by (rule cast_defl_fun1)
+
+lemma cast_lower_defl:
+  "cast\<cdot>(lower_defl\<cdot>A) =
+    udom_emb lower_approx oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj lower_approx"
+using lower_approx finite_deflation_lower_map
+unfolding lower_defl_def by (rule cast_defl_fun1)
+
+lemma cast_convex_defl:
+  "cast\<cdot>(convex_defl\<cdot>A) =
+    udom_emb convex_approx oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj convex_approx"
+using convex_approx finite_deflation_convex_map
+unfolding convex_defl_def by (rule cast_defl_fun1)
+
+subsection {* Domain class instances *}
+
+instantiation upper_pd :: ("domain") liftdomain
+begin
+
+definition
+  "emb = udom_emb upper_approx oo upper_map\<cdot>emb"
+
+definition
+  "prj = upper_map\<cdot>prj oo udom_prj upper_approx"
+
+definition
+  "defl (t::'a upper_pd itself) = upper_defl\<cdot>DEFL('a)"
+
+definition
+  "(liftemb :: 'a upper_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+  "(liftprj :: udom \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+  "liftdefl (t::'a upper_pd itself) = u_defl\<cdot>DEFL('a upper_pd)"
+
+instance
+using liftemb_upper_pd_def liftprj_upper_pd_def liftdefl_upper_pd_def
+proof (rule liftdomain_class_intro)
+  show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)"
+    unfolding emb_upper_pd_def prj_upper_pd_def
+    using ep_pair_udom [OF upper_approx]
+    by (intro ep_pair_comp ep_pair_upper_map ep_pair_emb_prj)
+next
+  show "cast\<cdot>DEFL('a upper_pd) = emb oo (prj :: udom \<rightarrow> 'a upper_pd)"
+    unfolding emb_upper_pd_def prj_upper_pd_def defl_upper_pd_def cast_upper_defl
+    by (simp add: cast_DEFL oo_def cfun_eq_iff upper_map_map)
+qed
+
+end
+
+instantiation lower_pd :: ("domain") liftdomain
+begin
+
+definition
+  "emb = udom_emb lower_approx oo lower_map\<cdot>emb"
+
+definition
+  "prj = lower_map\<cdot>prj oo udom_prj lower_approx"
+
+definition
+  "defl (t::'a lower_pd itself) = lower_defl\<cdot>DEFL('a)"
+
+definition
+  "(liftemb :: 'a lower_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+  "(liftprj :: udom \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+  "liftdefl (t::'a lower_pd itself) = u_defl\<cdot>DEFL('a lower_pd)"
+
+instance
+using liftemb_lower_pd_def liftprj_lower_pd_def liftdefl_lower_pd_def
+proof (rule liftdomain_class_intro)
+  show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)"
+    unfolding emb_lower_pd_def prj_lower_pd_def
+    using ep_pair_udom [OF lower_approx]
+    by (intro ep_pair_comp ep_pair_lower_map ep_pair_emb_prj)
+next
+  show "cast\<cdot>DEFL('a lower_pd) = emb oo (prj :: udom \<rightarrow> 'a lower_pd)"
+    unfolding emb_lower_pd_def prj_lower_pd_def defl_lower_pd_def cast_lower_defl
+    by (simp add: cast_DEFL oo_def cfun_eq_iff lower_map_map)
+qed
+
+end
+
+instantiation convex_pd :: ("domain") liftdomain
+begin
+
+definition
+  "emb = udom_emb convex_approx oo convex_map\<cdot>emb"
+
+definition
+  "prj = convex_map\<cdot>prj oo udom_prj convex_approx"
+
+definition
+  "defl (t::'a convex_pd itself) = convex_defl\<cdot>DEFL('a)"
+
+definition
+  "(liftemb :: 'a convex_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+  "(liftprj :: udom \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+  "liftdefl (t::'a convex_pd itself) = u_defl\<cdot>DEFL('a convex_pd)"
+
+instance
+using liftemb_convex_pd_def liftprj_convex_pd_def liftdefl_convex_pd_def
+proof (rule liftdomain_class_intro)
+  show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)"
+    unfolding emb_convex_pd_def prj_convex_pd_def
+    using ep_pair_udom [OF convex_approx]
+    by (intro ep_pair_comp ep_pair_convex_map ep_pair_emb_prj)
+next
+  show "cast\<cdot>DEFL('a convex_pd) = emb oo (prj :: udom \<rightarrow> 'a convex_pd)"
+    unfolding emb_convex_pd_def prj_convex_pd_def defl_convex_pd_def cast_convex_defl
+    by (simp add: cast_DEFL oo_def cfun_eq_iff convex_map_map)
+qed
+
+end
+
+lemma DEFL_upper: "DEFL('a::domain upper_pd) = upper_defl\<cdot>DEFL('a)"
+by (rule defl_upper_pd_def)
+
+lemma DEFL_lower: "DEFL('a::domain lower_pd) = lower_defl\<cdot>DEFL('a)"
+by (rule defl_lower_pd_def)
+
+lemma DEFL_convex: "DEFL('a::domain convex_pd) = convex_defl\<cdot>DEFL('a)"
+by (rule defl_convex_pd_def)
+
+subsection {* Isomorphic deflations *}
+
 lemma isodefl_upper:
   "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)"
 apply (rule isodeflI)

--- a/src/HOL/HOLCF/UpperPD.thy	Sun Dec 19 06:39:19 2010 -0800
+++ b/src/HOL/HOLCF/UpperPD.thy	Sun Dec 19 06:59:01 2010 -0800
@@ -453,7 +453,7 @@
     by (rule finite_range_imp_finite_fixes)
 qed
 
-subsection {* Upper powerdomain is a domain *}
+subsection {* Upper powerdomain is bifinite *}
 
 lemma approx_chain_upper_map:
   assumes "approx_chain a"
@@ -468,64 +468,6 @@
     by (fast intro!: approx_chain_upper_map)
 qed
 
-definition
-  upper_approx :: "nat \<Rightarrow> udom upper_pd \<rightarrow> udom upper_pd"
-where
-  "upper_approx = (\<lambda>i. upper_map\<cdot>(udom_approx i))"
-
-lemma upper_approx: "approx_chain upper_approx"
-using upper_map_ID finite_deflation_upper_map
-unfolding upper_approx_def by (rule approx_chain_lemma1)
-
-definition upper_defl :: "udom defl \<rightarrow> udom defl"
-where "upper_defl = defl_fun1 upper_approx upper_map"
-
-lemma cast_upper_defl:
-  "cast\<cdot>(upper_defl\<cdot>A) =
-    udom_emb upper_approx oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj upper_approx"
-using upper_approx finite_deflation_upper_map
-unfolding upper_defl_def by (rule cast_defl_fun1)
-
-instantiation upper_pd :: ("domain") liftdomain
-begin
-
-definition
-  "emb = udom_emb upper_approx oo upper_map\<cdot>emb"
-
-definition
-  "prj = upper_map\<cdot>prj oo udom_prj upper_approx"
-
-definition
-  "defl (t::'a upper_pd itself) = upper_defl\<cdot>DEFL('a)"
-
-definition
-  "(liftemb :: 'a upper_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
-
-definition
-  "(liftprj :: udom \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj oo udom_prj u_approx"
-
-definition
-  "liftdefl (t::'a upper_pd itself) = u_defl\<cdot>DEFL('a upper_pd)"
-
-instance
-using liftemb_upper_pd_def liftprj_upper_pd_def liftdefl_upper_pd_def
-proof (rule liftdomain_class_intro)
-  show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)"
-    unfolding emb_upper_pd_def prj_upper_pd_def
-    using ep_pair_udom [OF upper_approx]
-    by (intro ep_pair_comp ep_pair_upper_map ep_pair_emb_prj)
-next
-  show "cast\<cdot>DEFL('a upper_pd) = emb oo (prj :: udom \<rightarrow> 'a upper_pd)"
-    unfolding emb_upper_pd_def prj_upper_pd_def defl_upper_pd_def cast_upper_defl
-    by (simp add: cast_DEFL oo_def cfun_eq_iff upper_map_map)
-qed
-
-end
-
-lemma DEFL_upper: "DEFL('a::domain upper_pd) = upper_defl\<cdot>DEFL('a)"
-by (rule defl_upper_pd_def)
-
-
 subsection {* Join *}
 
 definition