--- 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 *}
--- 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)
--- 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)
--- 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)