# HG changeset patch
# User huffman
# Date 1292769559 28800
# Node ID a19edebad961195260abbe62ceb29cb4899fa843
# Parent  029a6fc1bfb8f03472faf9f7f887e9a8213b6adf
powerdomain theories require class 'bifinite' instead of 'domain'

diff -r 029a6fc1bfb8 -r a19edebad961 src/HOL/HOLCF/Compact_Basis.thy
--- a/src/HOL/HOLCF/Compact_Basis.thy	Sun Dec 19 06:34:41 2010 -0800
+++ b/src/HOL/HOLCF/Compact_Basis.thy	Sun Dec 19 06:39:19 2010 -0800
@@ -8,7 +8,7 @@
 imports Representable
 begin
 
-default_sort "domain"
+default_sort bifinite
 
 subsection {* A compact basis for powerdomains *}
 
diff -r 029a6fc1bfb8 -r a19edebad961 src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Sun Dec 19 06:34:41 2010 -0800
+++ b/src/HOL/HOLCF/ConvexPD.thy	Sun Dec 19 06:39:19 2010 -0800
@@ -125,7 +125,7 @@
 
 type_notation (xsymbols) convex_pd ("('(_')\<natural>)")
 
-instantiation convex_pd :: ("domain") below
+instantiation convex_pd :: (bifinite) below
 begin
 
 definition
@@ -134,11 +134,11 @@
 instance ..
 end
 
-instance convex_pd :: ("domain") po
+instance convex_pd :: (bifinite) po
 using type_definition_convex_pd below_convex_pd_def
 by (rule convex_le.typedef_ideal_po)
 
-instance convex_pd :: ("domain") cpo
+instance convex_pd :: (bifinite) cpo
 using type_definition_convex_pd below_convex_pd_def
 by (rule convex_le.typedef_ideal_cpo)
 
@@ -157,7 +157,7 @@
 lemma convex_pd_minimal: "convex_principal (PDUnit compact_bot) \<sqsubseteq> ys"
 by (induct ys rule: convex_pd.principal_induct, simp, simp)
 
-instance convex_pd :: ("domain") pcpo
+instance convex_pd :: (bifinite) pcpo
 by intro_classes (fast intro: convex_pd_minimal)
 
 lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)"
@@ -474,7 +474,7 @@
   using assms unfolding approx_chain_def
   by (simp add: lub_APP convex_map_ID finite_deflation_convex_map)
 
-instance convex_pd :: ("domain") bifinite
+instance convex_pd :: (bifinite) bifinite
 proof
   show "\<exists>(a::nat \<Rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd). approx_chain a"
     using bifinite [where 'a='a]
@@ -537,7 +537,7 @@
 
 text {* DEFL of type constructor = type combinator *}
 
-lemma DEFL_convex: "DEFL('a convex_pd) = convex_defl\<cdot>DEFL('a)"
+lemma DEFL_convex: "DEFL('a::domain convex_pd) = convex_defl\<cdot>DEFL('a)"
 by (rule defl_convex_pd_def)
 
 
diff -r 029a6fc1bfb8 -r a19edebad961 src/HOL/HOLCF/LowerPD.thy
--- a/src/HOL/HOLCF/LowerPD.thy	Sun Dec 19 06:34:41 2010 -0800
+++ b/src/HOL/HOLCF/LowerPD.thy	Sun Dec 19 06:39:19 2010 -0800
@@ -80,7 +80,7 @@
 
 type_notation (xsymbols) lower_pd ("('(_')\<flat>)")
 
-instantiation lower_pd :: ("domain") below
+instantiation lower_pd :: (bifinite) below
 begin
 
 definition
@@ -89,11 +89,11 @@
 instance ..
 end
 
-instance lower_pd :: ("domain") po
+instance lower_pd :: (bifinite) po
 using type_definition_lower_pd below_lower_pd_def
 by (rule lower_le.typedef_ideal_po)
 
-instance lower_pd :: ("domain") cpo
+instance lower_pd :: (bifinite) cpo
 using type_definition_lower_pd below_lower_pd_def
 by (rule lower_le.typedef_ideal_cpo)
 
@@ -112,7 +112,7 @@
 lemma lower_pd_minimal: "lower_principal (PDUnit compact_bot) \<sqsubseteq> ys"
 by (induct ys rule: lower_pd.principal_induct, simp, simp)
 
-instance lower_pd :: ("domain") pcpo
+instance lower_pd :: (bifinite) pcpo
 by intro_classes (fast intro: lower_pd_minimal)
 
 lemma inst_lower_pd_pcpo: "\<bottom> = lower_principal (PDUnit compact_bot)"
@@ -466,7 +466,7 @@
   using assms unfolding approx_chain_def
   by (simp add: lub_APP lower_map_ID finite_deflation_lower_map)
 
-instance lower_pd :: ("domain") bifinite
+instance lower_pd :: (bifinite) bifinite
 proof
   show "\<exists>(a::nat \<Rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd). approx_chain a"
     using bifinite [where 'a='a]
@@ -527,7 +527,7 @@
 
 end
 
-lemma DEFL_lower: "DEFL('a lower_pd) = lower_defl\<cdot>DEFL('a)"
+lemma DEFL_lower: "DEFL('a::domain lower_pd) = lower_defl\<cdot>DEFL('a)"
 by (rule defl_lower_pd_def)
 
 
diff -r 029a6fc1bfb8 -r a19edebad961 src/HOL/HOLCF/UpperPD.thy
--- a/src/HOL/HOLCF/UpperPD.thy	Sun Dec 19 06:34:41 2010 -0800
+++ b/src/HOL/HOLCF/UpperPD.thy	Sun Dec 19 06:39:19 2010 -0800
@@ -78,7 +78,7 @@
 
 type_notation (xsymbols) upper_pd ("('(_')\<sharp>)")
 
-instantiation upper_pd :: ("domain") below
+instantiation upper_pd :: (bifinite) below
 begin
 
 definition
@@ -87,11 +87,11 @@
 instance ..
 end
 
-instance upper_pd :: ("domain") po
+instance upper_pd :: (bifinite) po
 using type_definition_upper_pd below_upper_pd_def
 by (rule upper_le.typedef_ideal_po)
 
-instance upper_pd :: ("domain") cpo
+instance upper_pd :: (bifinite) cpo
 using type_definition_upper_pd below_upper_pd_def
 by (rule upper_le.typedef_ideal_cpo)
 
@@ -110,7 +110,7 @@
 lemma upper_pd_minimal: "upper_principal (PDUnit compact_bot) \<sqsubseteq> ys"
 by (induct ys rule: upper_pd.principal_induct, simp, simp)
 
-instance upper_pd :: ("domain") pcpo
+instance upper_pd :: (bifinite) pcpo
 by intro_classes (fast intro: upper_pd_minimal)
 
 lemma inst_upper_pd_pcpo: "\<bottom> = upper_principal (PDUnit compact_bot)"
@@ -461,7 +461,7 @@
   using assms unfolding approx_chain_def
   by (simp add: lub_APP upper_map_ID finite_deflation_upper_map)
 
-instance upper_pd :: ("domain") bifinite
+instance upper_pd :: (bifinite) bifinite
 proof
   show "\<exists>(a::nat \<Rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd). approx_chain a"
     using bifinite [where 'a='a]
@@ -522,7 +522,7 @@
 
 end
 
-lemma DEFL_upper: "DEFL('a upper_pd) = upper_defl\<cdot>DEFL('a)"
+lemma DEFL_upper: "DEFL('a::domain upper_pd) = upper_defl\<cdot>DEFL('a)"
 by (rule defl_upper_pd_def)