# HG changeset patch
# User wenzelm
# Date 1734014729 -3600
# Node ID b6df830451782e6ab8c53ed639450e36017581a8
# Parent  c3190d0b068c08f54e9ff2c7a0570c7f4c799141
clarified default_sort: "cpo" for bootstrap, "domain" for main HOLCF;

diff -r c3190d0b068c -r b6df83045178 src/HOL/HOLCF/Algebraic.thy
--- a/src/HOL/HOLCF/Algebraic.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/Algebraic.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -8,12 +8,9 @@
 imports Universal Map_Functions
 begin
 
-default_sort bifinite
-
-
 subsection \<open>Type constructor for finite deflations\<close>
 
-typedef 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
+typedef 'a::bifinite fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
 by (fast intro: finite_deflation_bottom)
 
 instantiation fin_defl :: (bifinite) below
@@ -76,7 +73,7 @@
 
 subsection \<open>Defining algebraic deflations by ideal completion\<close>
 
-typedef 'a defl = "{S::'a fin_defl set. below.ideal S}"
+typedef 'a::bifinite defl = "{S::'a fin_defl set. below.ideal S}"
 by (rule below.ex_ideal)
 
 instantiation defl :: (bifinite) below
@@ -97,10 +94,10 @@
 by (rule below.typedef_ideal_cpo)
 
 definition
-  defl_principal :: "'a fin_defl \<Rightarrow> 'a defl" where
+  defl_principal :: "'a::bifinite fin_defl \<Rightarrow> 'a defl" where
   "defl_principal t = Abs_defl {u. u \<sqsubseteq> t}"
 
-lemma fin_defl_countable: "\<exists>f::'a fin_defl \<Rightarrow> nat. inj f"
+lemma fin_defl_countable: "\<exists>f::'a::bifinite fin_defl \<Rightarrow> nat. inj f"
 proof -
   obtain f :: "'a compact_basis \<Rightarrow> nat" where inj_f: "inj f"
     using compact_basis.countable ..
@@ -153,7 +150,7 @@
 subsection \<open>Applying algebraic deflations\<close>
 
 definition
-  cast :: "'a defl \<rightarrow> 'a \<rightarrow> 'a"
+  cast :: "'a::bifinite defl \<rightarrow> 'a \<rightarrow> 'a"
 where
   "cast = defl.extension Rep_fin_defl"
 
diff -r c3190d0b068c -r b6df83045178 src/HOL/HOLCF/Bifinite.thy
--- a/src/HOL/HOLCF/Bifinite.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/Bifinite.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -8,9 +8,6 @@
   imports Map_Functions Cprod Sprod Sfun Up "HOL-Library.Countable"
 begin
 
-default_sort cpo
-
-
 subsection \<open>Chains of finite deflations\<close>
 
 locale approx_chain =
diff -r c3190d0b068c -r b6df83045178 src/HOL/HOLCF/Cfun.thy
--- a/src/HOL/HOLCF/Cfun.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/Cfun.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -9,9 +9,6 @@
   imports Cpodef
 begin
 
-default_sort cpo
-
-
 subsection \<open>Definition of continuous function type\<close>
 
 definition "cfun = {f::'a \<Rightarrow> 'b. cont f}"
@@ -455,9 +452,7 @@
 
 subsection \<open>Strictified functions\<close>
 
-default_sort pcpo
-
-definition seq :: "'a \<rightarrow> 'b \<rightarrow> 'b"
+definition seq :: "'a::pcpo \<rightarrow> 'b::pcpo \<rightarrow> 'b"
   where "seq = (\<Lambda> x. if x = \<bottom> then \<bottom> else ID)"
 
 lemma cont2cont_if_bottom [cont2cont, simp]:
@@ -481,7 +476,7 @@
   "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x = ID"
   by (simp_all add: seq_conv_if)
 
-definition strictify  :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b"
+definition strictify  :: "('a::pcpo \<rightarrow> 'b::pcpo) \<rightarrow> 'a \<rightarrow> 'b"
   where "strictify = (\<Lambda> f x. seq\<cdot>x\<cdot>(f\<cdot>x))"
 
 lemma strictify_conv_if: "strictify\<cdot>f\<cdot>x = (if x = \<bottom> then \<bottom> else f\<cdot>x)"
diff -r c3190d0b068c -r b6df83045178 src/HOL/HOLCF/Compact_Basis.thy
--- a/src/HOL/HOLCF/Compact_Basis.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/Compact_Basis.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -8,14 +8,11 @@
 imports Universal
 begin
 
-default_sort bifinite
-
-
 subsection \<open>A compact basis for powerdomains\<close>
 
-definition "pd_basis = {S::'a compact_basis set. finite S \<and> S \<noteq> {}}"
+definition "pd_basis = {S::'a::bifinite compact_basis set. finite S \<and> S \<noteq> {}}"
 
-typedef 'a pd_basis = "pd_basis :: 'a compact_basis set set"
+typedef 'a::bifinite pd_basis = "pd_basis :: 'a compact_basis set set"
   unfolding pd_basis_def
   apply (rule_tac x="{_}" in exI)
   apply simp
@@ -29,7 +26,7 @@
 
 text \<open>The powerdomain basis type is countable.\<close>
 
-lemma pd_basis_countable: "\<exists>f::'a pd_basis \<Rightarrow> nat. inj f"
+lemma pd_basis_countable: "\<exists>f::'a::bifinite pd_basis \<Rightarrow> nat. inj f"
 proof -
   obtain g :: "'a compact_basis \<Rightarrow> nat" where "inj g"
     using compact_basis.countable ..
@@ -45,11 +42,11 @@
 subsection \<open>Unit and plus constructors\<close>
 
 definition
-  PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where
+  PDUnit :: "'a::bifinite compact_basis \<Rightarrow> 'a pd_basis" where
   "PDUnit = (\<lambda>x. Abs_pd_basis {x})"
 
 definition
-  PDPlus :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
+  PDPlus :: "'a::bifinite pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
   "PDPlus t u = Abs_pd_basis (Rep_pd_basis t \<union> Rep_pd_basis u)"
 
 lemma Rep_PDUnit:
@@ -98,7 +95,7 @@
 
 definition
   fold_pd ::
-    "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b"
+    "('a::bifinite compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b"
   where "fold_pd g f t = semilattice_set.F f (g ` Rep_pd_basis t)"
 
 lemma fold_pd_PDUnit:
diff -r c3190d0b068c -r b6df83045178 src/HOL/HOLCF/Completion.thy
--- a/src/HOL/HOLCF/Completion.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/Completion.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -146,8 +146,8 @@
 hide_const (open) Filter.principal
 
 locale ideal_completion = preorder +
-  fixes principal :: "'a::type \<Rightarrow> 'b::cpo"
-  fixes rep :: "'b::cpo \<Rightarrow> 'a::type set"
+  fixes principal :: "'a::type \<Rightarrow> 'b"
+  fixes rep :: "'b \<Rightarrow> 'a::type set"
   assumes ideal_rep: "\<And>x. ideal (rep x)"
   assumes rep_lub: "\<And>Y. chain Y \<Longrightarrow> rep (\<Squnion>i. Y i) = (\<Union>i. rep (Y i))"
   assumes rep_principal: "\<And>a. rep (principal a) = {b. b \<preceq> a}"
@@ -302,11 +302,11 @@
 subsection \<open>Defining functions in terms of basis elements\<close>
 
 definition
-  extension :: "('a::type \<Rightarrow> 'c::cpo) \<Rightarrow> 'b \<rightarrow> 'c" where
+  extension :: "('a::type \<Rightarrow> 'c) \<Rightarrow> 'b \<rightarrow> 'c" where
   "extension = (\<lambda>f. (\<Lambda> x. lub (f ` rep x)))"
 
 lemma extension_lemma:
-  fixes f :: "'a::type \<Rightarrow> 'c::cpo"
+  fixes f :: "'a::type \<Rightarrow> 'c"
   assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
   shows "\<exists>u. f ` rep x <<| u"
 proof -
@@ -336,7 +336,7 @@
 qed
 
 lemma extension_beta:
-  fixes f :: "'a::type \<Rightarrow> 'c::cpo"
+  fixes f :: "'a::type \<Rightarrow> 'c"
   assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
   shows "extension f\<cdot>x = lub (f ` rep x)"
 unfolding extension_def
@@ -357,7 +357,7 @@
 qed
 
 lemma extension_principal:
-  fixes f :: "'a::type \<Rightarrow> 'c::cpo"
+  fixes f :: "'a::type \<Rightarrow> 'c"
   assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
   shows "extension f\<cdot>(principal a) = f a"
 apply (subst extension_beta, erule f_mono)
@@ -406,7 +406,7 @@
 end
 
 lemma (in preorder) typedef_ideal_completion:
-  fixes Abs :: "'a set \<Rightarrow> 'b::cpo"
+  fixes Abs :: "'a set \<Rightarrow> 'b"
   assumes type: "type_definition Rep Abs {S. ideal S}"
   assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
   assumes principal: "\<And>a. principal a = Abs {b. b \<preceq> a}"
diff -r c3190d0b068c -r b6df83045178 src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/ConvexPD.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -11,7 +11,7 @@
 subsection \<open>Basis preorder\<close>
 
 definition
-  convex_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix \<open>\<le>\<natural>\<close> 50) where
+  convex_le :: "'a::bifinite pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix \<open>\<le>\<natural>\<close> 50) where
   "convex_le = (\<lambda>u v. u \<le>\<sharp> v \<and> u \<le>\<flat> v)"
 
 lemma convex_le_refl [simp]: "t \<le>\<natural> t"
@@ -119,7 +119,7 @@
 
 subsection \<open>Type definition\<close>
 
-typedef 'a convex_pd  (\<open>(\<open>notation=\<open>postfix convex_pd\<close>\<close>'(_')\<natural>)\<close>) =
+typedef 'a::bifinite convex_pd  (\<open>(\<open>notation=\<open>postfix convex_pd\<close>\<close>'(_')\<natural>)\<close>) =
   "{S::'a pd_basis set. convex_le.ideal S}"
 by (rule convex_le.ex_ideal)
 
@@ -141,7 +141,7 @@
 by (rule convex_le.typedef_ideal_cpo)
 
 definition
-  convex_principal :: "'a pd_basis \<Rightarrow> 'a convex_pd" where
+  convex_principal :: "'a::bifinite pd_basis \<Rightarrow> 'a convex_pd" where
   "convex_principal t = Abs_convex_pd {u. u \<le>\<natural> t}"
 
 interpretation convex_pd:
@@ -165,16 +165,16 @@
 subsection \<open>Monadic unit and plus\<close>
 
 definition
-  convex_unit :: "'a \<rightarrow> 'a convex_pd" where
+  convex_unit :: "'a::bifinite \<rightarrow> 'a convex_pd" where
   "convex_unit = compact_basis.extension (\<lambda>a. convex_principal (PDUnit a))"
 
 definition
-  convex_plus :: "'a convex_pd \<rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd" where
+  convex_plus :: "'a::bifinite convex_pd \<rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd" where
   "convex_plus = convex_pd.extension (\<lambda>t. convex_pd.extension (\<lambda>u.
       convex_principal (PDPlus t u)))"
 
 abbreviation
-  convex_add :: "'a convex_pd \<Rightarrow> 'a convex_pd \<Rightarrow> 'a convex_pd"
+  convex_add :: "'a::bifinite convex_pd \<Rightarrow> 'a convex_pd \<Rightarrow> 'a convex_pd"
     (infixl \<open>\<union>\<natural>\<close> 65) where
   "xs \<union>\<natural> ys == convex_plus\<cdot>xs\<cdot>ys"
 
@@ -280,7 +280,7 @@
   assumes P: "adm P"
   assumes unit: "\<And>x. P {x}\<natural>"
   assumes insert: "\<And>x ys. \<lbrakk>P {x}\<natural>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<natural> \<union>\<natural> ys)"
-  shows "P (xs::'a convex_pd)"
+  shows "P (xs::'a::bifinite convex_pd)"
 apply (induct xs rule: convex_pd.principal_induct, rule P)
 apply (induct_tac a rule: pd_basis_induct1)
 apply (simp only: convex_unit_Rep_compact_basis [symmetric])
@@ -295,7 +295,7 @@
   assumes P: "adm P"
   assumes unit: "\<And>x. P {x}\<natural>"
   assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<natural> ys)"
-  shows "P (xs::'a convex_pd)"
+  shows "P (xs::'a::bifinite convex_pd)"
 apply (induct xs rule: convex_pd.principal_induct, rule P)
 apply (induct_tac a rule: pd_basis_induct)
 apply (simp only: convex_unit_Rep_compact_basis [symmetric] unit)
@@ -307,7 +307,7 @@
 
 definition
   convex_bind_basis ::
-  "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b convex_pd" where
+  "'a::bifinite pd_basis \<Rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b::bifinite convex_pd" where
   "convex_bind_basis = fold_pd
     (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
     (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<natural> y\<cdot>f)"
@@ -340,7 +340,7 @@
 done
 
 definition
-  convex_bind :: "'a convex_pd \<rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b convex_pd" where
+  convex_bind :: "'a::bifinite convex_pd \<rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b::bifinite convex_pd" where
   "convex_bind = convex_pd.extension convex_bind_basis"
 
 syntax
@@ -378,7 +378,7 @@
 subsection \<open>Map\<close>
 
 definition
-  convex_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a convex_pd \<rightarrow> 'b convex_pd" where
+  convex_map :: "('a::bifinite \<rightarrow> 'b) \<rightarrow> 'a convex_pd \<rightarrow> 'b::bifinite convex_pd" where
   "convex_map = (\<Lambda> f xs. convex_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<natural>))"
 
 lemma convex_map_unit [simp]:
@@ -486,7 +486,7 @@
 subsection \<open>Join\<close>
 
 definition
-  convex_join :: "'a convex_pd convex_pd \<rightarrow> 'a convex_pd" where
+  convex_join :: "'a::bifinite convex_pd convex_pd \<rightarrow> 'a convex_pd" where
   "convex_join = (\<Lambda> xss. convex_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))"
 
 lemma convex_join_unit [simp]:
@@ -522,7 +522,7 @@
 unfolding convex_le_def by simp
 
 definition
-  convex_to_upper :: "'a convex_pd \<rightarrow> 'a upper_pd" where
+  convex_to_upper :: "'a::bifinite convex_pd \<rightarrow> 'a upper_pd" where
   "convex_to_upper = convex_pd.extension upper_principal"
 
 lemma convex_to_upper_principal [simp]:
@@ -562,7 +562,7 @@
 unfolding convex_le_def by simp
 
 definition
-  convex_to_lower :: "'a convex_pd \<rightarrow> 'a lower_pd" where
+  convex_to_lower :: "'a::bifinite convex_pd \<rightarrow> 'a lower_pd" where
   "convex_to_lower = convex_pd.extension lower_principal"
 
 lemma convex_to_lower_principal [simp]:
diff -r c3190d0b068c -r b6df83045178 src/HOL/HOLCF/Cpo.thy
--- a/src/HOL/HOLCF/Cpo.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/Cpo.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -353,6 +353,10 @@
 
 class cpo = po +
   assumes cpo: "chain S \<Longrightarrow> \<exists>x. range S <<| x"
+
+default_sort cpo
+
+context cpo
 begin
 
 text \<open>in cpo's everthing equal to THE lub has lub properties for every chain\<close>
@@ -601,7 +605,7 @@
 definition monofun :: "('a::po \<Rightarrow> 'b::po) \<Rightarrow> bool"  \<comment> \<open>monotonicity\<close>
   where "monofun f \<longleftrightarrow> (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
 
-definition cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"
+definition cont :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
   where "cont f = (\<forall>Y. chain Y \<longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i))"
 
 lemma contI: "(\<And>Y. chain Y \<Longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)) \<Longrightarrow> cont f"
@@ -667,7 +671,7 @@
   done
 
 lemma contI2:
-  fixes f :: "'a::cpo \<Rightarrow> 'b::cpo"
+  fixes f :: "'a \<Rightarrow> 'b"
   assumes mono: "monofun f"
   assumes below: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk> \<Longrightarrow> f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))"
   shows "cont f"
@@ -710,7 +714,7 @@
 text \<open>application of functions is continuous\<close>
 
 lemma cont_apply:
-  fixes f :: "'a::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'c::cpo" and t :: "'a \<Rightarrow> 'b"
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" and t :: "'a \<Rightarrow> 'b"
   assumes 1: "cont (\<lambda>x. t x)"
   assumes 2: "\<And>x. cont (\<lambda>y. f x y)"
   assumes 3: "\<And>y. cont (\<lambda>x. f x y)"
@@ -769,7 +773,7 @@
 text \<open>All monotone functions with chain-finite domain are continuous.\<close>
 
 lemma chfindom_monofun2cont: "monofun f \<Longrightarrow> cont f"
-  for f :: "'a::chfin \<Rightarrow> 'b::cpo"
+  for f :: "'a::chfin \<Rightarrow> 'b"
   apply (erule contI2)
   apply (frule chfin2finch)
   apply (clarsimp simp add: finite_chain_def)
@@ -794,7 +798,7 @@
 text \<open>All functions with discrete domain are continuous.\<close>
 
 lemma cont_discrete_cpo [simp, cont2cont]: "cont f"
-  for f :: "'a::discrete_cpo \<Rightarrow> 'b::cpo"
+  for f :: "'a::discrete_cpo \<Rightarrow> 'b"
   apply (rule contI)
   apply (drule discrete_chain_const, clarify)
   apply simp
@@ -803,9 +807,6 @@
 
 section \<open>Admissibility and compactness\<close>
 
-default_sort cpo
-
-
 subsection \<open>Definitions\<close>
 
 context cpo
@@ -833,8 +834,7 @@
 
 text \<open>For chain-finite (easy) types every formula is admissible.\<close>
 
-lemma adm_chfin [simp]: "adm P"
-  for P :: "'a::chfin \<Rightarrow> bool"
+lemma adm_chfin [simp]: "adm P" for P :: "'a::chfin \<Rightarrow> bool"
   by (rule admI, frule chfin, auto simp add: maxinch_is_thelub)
 
 
@@ -947,8 +947,7 @@
 
 end
 
-lemma compact_chfin [simp]: "compact x"
-  for x :: "'a::chfin"
+lemma compact_chfin [simp]: "compact x" for x :: "'a::chfin"
   by (rule compactI [OF adm_chfin])
 
 lemma compact_imp_max_in_chain: "chain Y \<Longrightarrow> compact (\<Squnion>i. Y i) \<Longrightarrow> \<exists>i. max_in_chain i Y"
@@ -1002,16 +1001,12 @@
 
 instance "fun" :: (type, po) po
 proof
-  fix f :: "'a \<Rightarrow> 'b"
+  fix f g h :: "'a \<Rightarrow> 'b"
   show "f \<sqsubseteq> f"
     by (simp add: below_fun_def)
-next
-  fix f g :: "'a \<Rightarrow> 'b"
-  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" then show "f = g"
+  show "f \<sqsubseteq> g \<Longrightarrow> g \<sqsubseteq> f \<Longrightarrow> f = g"
     by (simp add: below_fun_def fun_eq_iff below_antisym)
-next
-  fix f g h :: "'a \<Rightarrow> 'b"
-  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" then show "f \<sqsubseteq> h"
+  show "f \<sqsubseteq> g \<Longrightarrow> g \<sqsubseteq> h \<Longrightarrow> f \<sqsubseteq> h"
     unfolding below_fun_def by (fast elim: below_trans)
 qed
 
@@ -1044,14 +1039,14 @@
   by (simp add: is_lub_def is_ub_def below_fun_def)
 
 lemma is_lub_fun: "chain S \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)"
-  for S :: "nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo"
+  for S :: "nat \<Rightarrow> 'a::type \<Rightarrow> 'b"
   apply (rule is_lub_lambda)
   apply (rule cpo_lubI)
   apply (erule ch2ch_fun)
   done
 
 lemma lub_fun: "chain S \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
-  for S :: "nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo"
+  for S :: "nat \<Rightarrow> 'a::type \<Rightarrow> 'b"
   by (rule is_lub_fun [THEN lub_eqI])
 
 instance "fun"  :: (type, cpo) cpo
@@ -1125,7 +1120,7 @@
 text \<open>What D.A.Schmidt calls continuity of abstraction; never used here\<close>
 
 lemma contlub_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))"
-  for S :: "nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo"
+  for S :: "nat \<Rightarrow> 'a::type \<Rightarrow> 'b"
   by (simp add: lub_fun ch2ch_lambda)
 
 
@@ -1160,19 +1155,13 @@
 
 instance prod :: (po, po) po
 proof
-  fix x :: "'a \<times> 'b"
+  fix x y z :: "'a \<times> 'b"
   show "x \<sqsubseteq> x"
     by (simp add: below_prod_def)
-next
-  fix x y :: "'a \<times> 'b"
-  assume "x \<sqsubseteq> y" "y \<sqsubseteq> x"
-  then show "x = y"
+  show "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
     unfolding below_prod_def prod_eq_iff
     by (fast intro: below_antisym)
-next
-  fix x y z :: "'a \<times> 'b"
-  assume "x \<sqsubseteq> y" "y \<sqsubseteq> z"
-  then show "x \<sqsubseteq> z"
+  show "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
     unfolding below_prod_def
     by (fast intro: below_trans)
 qed
@@ -1238,17 +1227,17 @@
   by (simp add: is_lub_def is_ub_def below_prod_def)
 
 lemma lub_Pair: "chain A \<Longrightarrow> chain B \<Longrightarrow> (\<Squnion>i. (A i, B i)) = (\<Squnion>i. A i, \<Squnion>i. B i)"
-  for A :: "nat \<Rightarrow> 'a::cpo" and B :: "nat \<Rightarrow> 'b::cpo"
+  for A :: "nat \<Rightarrow> 'a" and B :: "nat \<Rightarrow> 'b"
   by (fast intro: lub_eqI is_lub_Pair elim: thelubE)
 
 lemma is_lub_prod:
-  fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
+  fixes S :: "nat \<Rightarrow> ('a \<times> 'b)"
   assumes "chain S"
   shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   using assms by (auto elim: prod_chain_cases simp: is_lub_Pair cpo_lubI)
 
 lemma lub_prod: "chain S \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
-  for S :: "nat \<Rightarrow> 'a::cpo \<times> 'b::cpo"
+  for S :: "nat \<Rightarrow> 'a \<times> 'b"
   by (rule is_lub_prod [THEN lub_eqI])
 
 instance prod :: (cpo, cpo) cpo
@@ -1262,8 +1251,7 @@
 
 instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo
 proof
-  fix x y :: "'a \<times> 'b"
-  show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
+  show "x \<sqsubseteq> y \<longleftrightarrow> x = y" for x y :: "'a \<times> 'b"
     by (simp add: below_prod_def prod_eq_iff)
 qed
 
@@ -1392,12 +1380,10 @@
 
 subsection \<open>Compactness and chain-finiteness\<close>
 
-lemma fst_below_iff: "fst x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"
-  for x :: "'a \<times> 'b"
+lemma fst_below_iff: "fst x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)" for x :: "'a \<times> 'b"
   by (simp add: below_prod_def)
 
-lemma snd_below_iff: "snd x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (fst x, y)"
-  for x :: "'a \<times> 'b"
+lemma snd_below_iff: "snd x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (fst x, y)" for x :: "'a \<times> 'b"
   by (simp add: below_prod_def)
 
 lemma compact_fst: "compact x \<Longrightarrow> compact (fst x)"
@@ -1424,7 +1410,7 @@
 
 section \<open>Discrete cpo types\<close>
 
-datatype 'a discr = Discr "'a :: type"
+datatype 'a discr = Discr "'a::type"
 
 subsection \<open>Discrete cpo class instance\<close>
 
@@ -1441,7 +1427,7 @@
 
 subsection \<open>\emph{undiscr}\<close>
 
-definition undiscr :: "('a::type)discr \<Rightarrow> 'a"
+definition undiscr :: "'a::type discr \<Rightarrow> 'a"
   where "undiscr x = (case x of Discr y \<Rightarrow> y)"
 
 lemma undiscr_Discr [simp]: "undiscr (Discr x) = x"
diff -r c3190d0b068c -r b6df83045178 src/HOL/HOLCF/Cprod.thy
--- a/src/HOL/HOLCF/Cprod.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/Cprod.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -8,9 +8,6 @@
   imports Cfun
 begin
 
-default_sort cpo
-
-
 subsection \<open>Continuous case function for unit type\<close>
 
 definition unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a"
diff -r c3190d0b068c -r b6df83045178 src/HOL/HOLCF/Deflation.thy
--- a/src/HOL/HOLCF/Deflation.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/Deflation.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -8,9 +8,6 @@
   imports Cfun
 begin
 
-default_sort cpo
-
-
 subsection \<open>Continuous deflations\<close>
 
 locale deflation =
diff -r c3190d0b068c -r b6df83045178 src/HOL/HOLCF/Domain.thy
--- a/src/HOL/HOLCF/Domain.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/Domain.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -17,7 +17,7 @@
 text \<open>A locale for continuous isomorphisms\<close>
 
 locale iso =
-  fixes abs :: "'a \<rightarrow> 'b"
+  fixes abs :: "'a::pcpo \<rightarrow> 'b::pcpo"
   fixes rep :: "'b \<rightarrow> 'a"
   assumes abs_iso [simp]: "rep\<cdot>(abs\<cdot>x) = x"
   assumes rep_iso [simp]: "abs\<cdot>(rep\<cdot>y) = y"
@@ -374,15 +374,13 @@
 
 subsection \<open>Representations of types\<close>
 
-default_sort "domain"
-
-lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a) = cast\<cdot>DEFL('a)\<cdot>x"
+lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a::domain) = cast\<cdot>DEFL('a)\<cdot>x"
 by (simp add: cast_DEFL)
 
 lemma emb_prj_emb:
-  fixes x :: "'a"
+  fixes x :: "'a::domain"
   assumes "DEFL('a) \<sqsubseteq> DEFL('b)"
-  shows "emb\<cdot>(prj\<cdot>(emb\<cdot>x) :: 'b) = emb\<cdot>x"
+  shows "emb\<cdot>(prj\<cdot>(emb\<cdot>x) :: 'b::domain) = emb\<cdot>x"
 unfolding emb_prj
 apply (rule cast.belowD)
 apply (rule monofun_cfun_arg [OF assms])
@@ -390,7 +388,7 @@
 done
 
 lemma prj_emb_prj:
-  assumes "DEFL('a) \<sqsubseteq> DEFL('b)"
+  assumes "DEFL('a::domain) \<sqsubseteq> DEFL('b::domain)"
   shows "prj\<cdot>(emb\<cdot>(prj\<cdot>x :: 'b)) = (prj\<cdot>x :: 'a)"
  apply (rule emb_eq_iff [THEN iffD1])
  apply (simp only: emb_prj)
@@ -404,7 +402,7 @@
 
 lemma domain_abs_iso:
   fixes abs and rep
-  assumes DEFL: "DEFL('b) = DEFL('a)"
+  assumes DEFL: "DEFL('b::domain) = DEFL('a::domain)"
   assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb"
   assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb"
   shows "rep\<cdot>(abs\<cdot>x) = x"
@@ -413,7 +411,7 @@
 
 lemma domain_rep_iso:
   fixes abs and rep
-  assumes DEFL: "DEFL('b) = DEFL('a)"
+  assumes DEFL: "DEFL('b::domain) = DEFL('a::domain)"
   assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb"
   assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb"
   shows "abs\<cdot>(rep\<cdot>x) = x"
@@ -518,7 +516,7 @@
 
 subsection \<open>Isomorphic deflations\<close>
 
-definition isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> udom defl \<Rightarrow> bool"
+definition isodefl :: "('a::domain \<rightarrow> 'a) \<Rightarrow> udom defl \<Rightarrow> bool"
   where "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
 
 definition isodefl' :: "('a::predomain \<rightarrow> 'a) \<Rightarrow> udom u defl \<Rightarrow> bool"
@@ -535,7 +533,7 @@
 by (drule cfun_fun_cong [where x="\<bottom>"], simp)
 
 lemma isodefl_imp_deflation:
-  fixes d :: "'a \<rightarrow> 'a"
+  fixes d :: "'a::domain \<rightarrow> 'a"
   assumes "isodefl d t" shows "deflation d"
 proof
   note assms [unfolded isodefl_def, simp]
@@ -546,14 +544,14 @@
     using cast.below [of t "emb\<cdot>x"] by simp
 qed
 
-lemma isodefl_ID_DEFL: "isodefl (ID :: 'a \<rightarrow> 'a) DEFL('a)"
+lemma isodefl_ID_DEFL: "isodefl (ID :: 'a \<rightarrow> 'a) DEFL('a::domain)"
 unfolding isodefl_def by (simp add: cast_DEFL)
 
 lemma isodefl_LIFTDEFL:
   "isodefl' (ID :: 'a \<rightarrow> 'a) LIFTDEFL('a::predomain)"
 unfolding isodefl'_def by (simp add: cast_liftdefl u_map_ID)
 
-lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) DEFL('a) \<Longrightarrow> d = ID"
+lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) DEFL('a::domain) \<Longrightarrow> d = ID"
 unfolding isodefl_def
 apply (simp add: cast_DEFL)
 apply (simp add: cfun_eq_iff)
@@ -588,7 +586,7 @@
 
 lemma isodefl_abs_rep:
   fixes abs and rep and d
-  assumes DEFL: "DEFL('b) = DEFL('a)"
+  assumes DEFL: "DEFL('b::domain) = DEFL('a::domain)"
   assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb"
   assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb"
   shows "isodefl d t \<Longrightarrow> isodefl (abs oo d oo rep) t"
diff -r c3190d0b068c -r b6df83045178 src/HOL/HOLCF/Fixrec.thy
--- a/src/HOL/HOLCF/Fixrec.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/Fixrec.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -10,12 +10,9 @@
 
 section \<open>Fixed point operator and admissibility\<close>
 
-default_sort pcpo
-
-
 subsection \<open>Iteration\<close>
 
-primrec iterate :: "nat \<Rightarrow> ('a::cpo \<rightarrow> 'a) \<rightarrow> ('a \<rightarrow> 'a)"
+primrec iterate :: "nat \<Rightarrow> ('a \<rightarrow> 'a) \<rightarrow> ('a \<rightarrow> 'a)"
   where
     "iterate 0 = (\<Lambda> F x. x)"
   | "iterate (Suc n) = (\<Lambda> F x. F\<cdot>(iterate n\<cdot>F\<cdot>x))"
@@ -44,12 +41,12 @@
 
 subsection \<open>Least fixed point operator\<close>
 
-definition "fix" :: "('a \<rightarrow> 'a) \<rightarrow> 'a"
+definition "fix" :: "('a::pcpo \<rightarrow> 'a) \<rightarrow> 'a"
   where "fix = (\<Lambda> F. \<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)"
 
 text \<open>Binder syntax for \<^term>\<open>fix\<close>\<close>
 
-abbreviation fix_syn :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  (binder \<open>\<mu> \<close> 10)
+abbreviation fix_syn :: "('a::pcpo \<Rightarrow> 'a) \<Rightarrow> 'a"  (binder \<open>\<mu> \<close> 10)
   where "fix_syn (\<lambda>x. f x) \<equiv> fix\<cdot>(\<Lambda> x. f x)"
 
 notation (ASCII)
@@ -209,9 +206,11 @@
 \<close>
 
 lemma fix_cprod:
-  "fix\<cdot>(F::'a \<times> 'b \<rightarrow> 'a \<times> 'b) =
-   (\<mu> x. fst (F\<cdot>(x, \<mu> y. snd (F\<cdot>(x, y)))),
-    \<mu> y. snd (F\<cdot>(\<mu> x. fst (F\<cdot>(x, \<mu> y. snd (F\<cdot>(x, y)))), y)))"
+  fixes F :: "'a::pcpo \<times> 'b::pcpo \<rightarrow> 'a \<times> 'b"
+  shows
+    "fix\<cdot>F =
+     (\<mu> x. fst (F\<cdot>(x, \<mu> y. snd (F\<cdot>(x, y)))),
+      \<mu> y. snd (F\<cdot>(\<mu> x. fst (F\<cdot>(x, \<mu> y. snd (F\<cdot>(x, y)))), y)))"
   (is "fix\<cdot>F = (?x, ?y)")
 proof (rule fix_eqI)
   have *: "fst (F\<cdot>(?x, ?y)) = ?x"
@@ -250,8 +249,6 @@
 
 subsection \<open>Pattern-match monad\<close>
 
-default_sort cpo
-
 pcpodef 'a match = "UNIV::(one ++ 'a u) set"
 by simp_all
 
@@ -340,50 +337,48 @@
 
 subsection \<open>Match functions for built-in types\<close>
 
-default_sort pcpo
-
 definition
-  match_bottom :: "'a \<rightarrow> 'c match \<rightarrow> 'c match"
+  match_bottom :: "'a::pcpo \<rightarrow> 'c match \<rightarrow> 'c match"
 where
   "match_bottom = (\<Lambda> x k. seq\<cdot>x\<cdot>fail)"
 
 definition
-  match_Pair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
+  match_Pair :: "'a \<times> 'b \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
 where
   "match_Pair = (\<Lambda> x k. csplit\<cdot>k\<cdot>x)"
 
 definition
-  match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
+  match_spair :: "'a::pcpo \<otimes> 'b::pcpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c::pcpo match"
 where
   "match_spair = (\<Lambda> x k. ssplit\<cdot>k\<cdot>x)"
 
 definition
-  match_sinl :: "'a \<oplus> 'b \<rightarrow> ('a \<rightarrow> 'c match) \<rightarrow> 'c match"
+  match_sinl :: "'a::pcpo \<oplus> 'b::pcpo \<rightarrow> ('a \<rightarrow> 'c::pcpo match) \<rightarrow> 'c match"
 where
   "match_sinl = (\<Lambda> x k. sscase\<cdot>k\<cdot>(\<Lambda> b. fail)\<cdot>x)"
 
 definition
-  match_sinr :: "'a \<oplus> 'b \<rightarrow> ('b \<rightarrow> 'c match) \<rightarrow> 'c match"
+  match_sinr :: "'a::pcpo \<oplus> 'b::pcpo \<rightarrow> ('b \<rightarrow> 'c::pcpo match) \<rightarrow> 'c match"
 where
   "match_sinr = (\<Lambda> x k. sscase\<cdot>(\<Lambda> a. fail)\<cdot>k\<cdot>x)"
 
 definition
-  match_up :: "'a::cpo u \<rightarrow> ('a \<rightarrow> 'c match) \<rightarrow> 'c match"
+  match_up :: "'a u \<rightarrow> ('a \<rightarrow> 'c::pcpo match) \<rightarrow> 'c match"
 where
   "match_up = (\<Lambda> x k. fup\<cdot>k\<cdot>x)"
 
 definition
-  match_ONE :: "one \<rightarrow> 'c match \<rightarrow> 'c match"
+  match_ONE :: "one \<rightarrow> 'c::pcpo match \<rightarrow> 'c match"
 where
   "match_ONE = (\<Lambda> ONE k. k)"
 
 definition
-  match_TT :: "tr \<rightarrow> 'c match \<rightarrow> 'c match"
+  match_TT :: "tr \<rightarrow> 'c::pcpo match \<rightarrow> 'c match"
 where
   "match_TT = (\<Lambda> x k. If x then k else fail)"
 
 definition
-  match_FF :: "tr \<rightarrow> 'c match \<rightarrow> 'c match"
+  match_FF :: "tr \<rightarrow> 'c::pcpo match \<rightarrow> 'c match"
 where
   "match_FF = (\<Lambda> x k. If x then fail else k)"
 
diff -r c3190d0b068c -r b6df83045178 src/HOL/HOLCF/Lift.thy
--- a/src/HOL/HOLCF/Lift.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/Lift.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -8,15 +8,13 @@
 imports Up
 begin
 
-default_sort type
-
-pcpodef 'a lift = "UNIV :: 'a discr u set"
+pcpodef 'a::type lift = "UNIV :: 'a discr u set"
 by simp_all
 
 lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]
 
 definition
-  Def :: "'a \<Rightarrow> 'a lift" where
+  Def :: "'a::type \<Rightarrow> 'a lift" where
   "Def x = Abs_lift (up\<cdot>(Discr x))"
 
 
@@ -30,7 +28,7 @@
 apply (simp add: Def_def)
 done
 
-old_rep_datatype "\<bottom>::'a lift" Def
+old_rep_datatype "\<bottom>::'a::type lift" Def
   by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject inst_lift_pcpo)
 
 text \<open>\<^term>\<open>bottom\<close> and \<^term>\<open>Def\<close>\<close>
@@ -88,7 +86,7 @@
 subsection \<open>Further operations\<close>
 
 definition
-  flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)"  (binder \<open>FLIFT \<close> 10)  where
+  flift1 :: "('a::type \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)"  (binder \<open>FLIFT \<close> 10)  where
   "flift1 = (\<lambda>f. (\<Lambda> x. case_lift \<bottom> f x))"
 
 translations
@@ -97,7 +95,7 @@
   "\<Lambda>(CONST Def x). t" <= "FLIFT x. t"
 
 definition
-  flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where
+  flift2 :: "('a::type \<Rightarrow> 'b::type) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where
   "flift2 f = (FLIFT x. Def (f x))"
 
 lemma flift1_Def [simp]: "flift1 f\<cdot>(Def x) = (f x)"
diff -r c3190d0b068c -r b6df83045178 src/HOL/HOLCF/LowerPD.thy
--- a/src/HOL/HOLCF/LowerPD.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/LowerPD.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -11,7 +11,7 @@
 subsection \<open>Basis preorder\<close>
 
 definition
-  lower_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix \<open>\<le>\<flat>\<close> 50) where
+  lower_le :: "'a::bifinite pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix \<open>\<le>\<flat>\<close> 50) where
   "lower_le = (\<lambda>u v. \<forall>x\<in>Rep_pd_basis u. \<exists>y\<in>Rep_pd_basis v. x \<sqsubseteq> y)"
 
 lemma lower_le_refl [simp]: "t \<le>\<flat> t"
@@ -74,7 +74,7 @@
 
 subsection \<open>Type definition\<close>
 
-typedef 'a lower_pd  (\<open>(\<open>notation=\<open>postfix lower_pd\<close>\<close>'(_')\<flat>)\<close>) =
+typedef 'a::bifinite lower_pd  (\<open>(\<open>notation=\<open>postfix lower_pd\<close>\<close>'(_')\<flat>)\<close>) =
   "{S::'a pd_basis set. lower_le.ideal S}"
 by (rule lower_le.ex_ideal)
 
@@ -96,7 +96,7 @@
 by (rule lower_le.typedef_ideal_cpo)
 
 definition
-  lower_principal :: "'a pd_basis \<Rightarrow> 'a lower_pd" where
+  lower_principal :: "'a::bifinite pd_basis \<Rightarrow> 'a lower_pd" where
   "lower_principal t = Abs_lower_pd {u. u \<le>\<flat> t}"
 
 interpretation lower_pd:
@@ -120,16 +120,16 @@
 subsection \<open>Monadic unit and plus\<close>
 
 definition
-  lower_unit :: "'a \<rightarrow> 'a lower_pd" where
+  lower_unit :: "'a::bifinite \<rightarrow> 'a lower_pd" where
   "lower_unit = compact_basis.extension (\<lambda>a. lower_principal (PDUnit a))"
 
 definition
-  lower_plus :: "'a lower_pd \<rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd" where
+  lower_plus :: "'a::bifinite lower_pd \<rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd" where
   "lower_plus = lower_pd.extension (\<lambda>t. lower_pd.extension (\<lambda>u.
       lower_principal (PDPlus t u)))"
 
 abbreviation
-  lower_add :: "'a lower_pd \<Rightarrow> 'a lower_pd \<Rightarrow> 'a lower_pd"
+  lower_add :: "'a::bifinite lower_pd \<Rightarrow> 'a lower_pd \<Rightarrow> 'a lower_pd"
     (infixl \<open>\<union>\<flat>\<close> 65) where
   "xs \<union>\<flat> ys == lower_plus\<cdot>xs\<cdot>ys"
 
@@ -151,7 +151,7 @@
     lower_pd.extension_mono PDPlus_lower_mono)
 
 interpretation lower_add: semilattice lower_add proof
-  fix xs ys zs :: "'a lower_pd"
+  fix xs ys zs :: "'a::bifinite lower_pd"
   show "(xs \<union>\<flat> ys) \<union>\<flat> zs = xs \<union>\<flat> (ys \<union>\<flat> zs)"
     apply (induct xs rule: lower_pd.principal_induct, simp)
     apply (induct ys rule: lower_pd.principal_induct, simp)
@@ -273,7 +273,7 @@
   assumes unit: "\<And>x. P {x}\<flat>"
   assumes insert:
     "\<And>x ys. \<lbrakk>P {x}\<flat>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<flat> \<union>\<flat> ys)"
-  shows "P (xs::'a lower_pd)"
+  shows "P (xs::'a::bifinite lower_pd)"
 apply (induct xs rule: lower_pd.principal_induct, rule P)
 apply (induct_tac a rule: pd_basis_induct1)
 apply (simp only: lower_unit_Rep_compact_basis [symmetric])
@@ -288,7 +288,7 @@
   assumes P: "adm P"
   assumes unit: "\<And>x. P {x}\<flat>"
   assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<flat> ys)"
-  shows "P (xs::'a lower_pd)"
+  shows "P (xs::'a::bifinite lower_pd)"
 apply (induct xs rule: lower_pd.principal_induct, rule P)
 apply (induct_tac a rule: pd_basis_induct)
 apply (simp only: lower_unit_Rep_compact_basis [symmetric] unit)
@@ -300,7 +300,7 @@
 
 definition
   lower_bind_basis ::
-  "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b lower_pd) \<rightarrow> 'b lower_pd" where
+  "'a::bifinite pd_basis \<Rightarrow> ('a \<rightarrow> 'b lower_pd) \<rightarrow> 'b::bifinite lower_pd" where
   "lower_bind_basis = fold_pd
     (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
     (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<flat> y\<cdot>f)"
@@ -334,7 +334,7 @@
 done
 
 definition
-  lower_bind :: "'a lower_pd \<rightarrow> ('a \<rightarrow> 'b lower_pd) \<rightarrow> 'b lower_pd" where
+  lower_bind :: "'a::bifinite lower_pd \<rightarrow> ('a \<rightarrow> 'b lower_pd) \<rightarrow> 'b::bifinite lower_pd" where
   "lower_bind = lower_pd.extension lower_bind_basis"
 
 syntax
@@ -371,7 +371,7 @@
 subsection \<open>Map\<close>
 
 definition
-  lower_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a lower_pd \<rightarrow> 'b lower_pd" where
+  lower_map :: "('a::bifinite \<rightarrow> 'b::bifinite) \<rightarrow> 'a lower_pd \<rightarrow> 'b lower_pd" where
   "lower_map = (\<Lambda> f xs. lower_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<flat>))"
 
 lemma lower_map_unit [simp]:
@@ -479,7 +479,7 @@
 subsection \<open>Join\<close>
 
 definition
-  lower_join :: "'a lower_pd lower_pd \<rightarrow> 'a lower_pd" where
+  lower_join :: "'a::bifinite lower_pd lower_pd \<rightarrow> 'a lower_pd" where
   "lower_join = (\<Lambda> xss. lower_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))"
 
 lemma lower_join_unit [simp]:
diff -r c3190d0b068c -r b6df83045178 src/HOL/HOLCF/Map_Functions.thy
--- a/src/HOL/HOLCF/Map_Functions.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/Map_Functions.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -10,8 +10,6 @@
 
 subsection \<open>Map operator for continuous function space\<close>
 
-default_sort cpo
-
 definition cfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)"
   where "cfun_map = (\<Lambda> a b f x. b\<cdot>(f\<cdot>(a\<cdot>x)))"
 
@@ -214,9 +212,7 @@
 
 subsection \<open>Map function for strict products\<close>
 
-default_sort pcpo
-
-definition sprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<otimes> 'c \<rightarrow> 'b \<otimes> 'd"
+definition sprod_map :: "('a::pcpo \<rightarrow> 'b::pcpo) \<rightarrow> ('c::pcpo \<rightarrow> 'd::pcpo) \<rightarrow> 'a \<otimes> 'c \<rightarrow> 'b \<otimes> 'd"
   where "sprod_map = (\<Lambda> f g. ssplit\<cdot>(\<Lambda> x y. (:f\<cdot>x, g\<cdot>y:)))"
 
 lemma sprod_map_strict [simp]: "sprod_map\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>"
@@ -315,7 +311,7 @@
 
 subsection \<open>Map function for strict sums\<close>
 
-definition ssum_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd"
+definition ssum_map :: "('a::pcpo \<rightarrow> 'b::pcpo) \<rightarrow> ('c::pcpo \<rightarrow> 'd::pcpo) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd"
   where "ssum_map = (\<Lambda> f g. sscase\<cdot>(sinl oo f)\<cdot>(sinr oo g))"
 
 lemma ssum_map_strict [simp]: "ssum_map\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
@@ -422,7 +418,7 @@
 
 subsection \<open>Map operator for strict function space\<close>
 
-definition sfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow>! 'c) \<rightarrow> ('b \<rightarrow>! 'd)"
+definition sfun_map :: "('b::pcpo \<rightarrow> 'a::pcpo) \<rightarrow> ('c::pcpo \<rightarrow> 'd::pcpo) \<rightarrow> ('a \<rightarrow>! 'c) \<rightarrow> ('b \<rightarrow>! 'd)"
   where "sfun_map = (\<Lambda> a b. sfun_abs oo cfun_map\<cdot>a\<cdot>b oo sfun_rep)"
 
 lemma sfun_map_ID: "sfun_map\<cdot>ID\<cdot>ID = ID"
diff -r c3190d0b068c -r b6df83045178 src/HOL/HOLCF/Representable.thy
--- a/src/HOL/HOLCF/Representable.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/Representable.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -8,9 +8,6 @@
 imports Algebraic Map_Functions "HOL-Library.Countable"
 begin
 
-default_sort cpo
-
-
 subsection \<open>Class of representable domains\<close>
 
 text \<open>
diff -r c3190d0b068c -r b6df83045178 src/HOL/HOLCF/Sfun.thy
--- a/src/HOL/HOLCF/Sfun.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/Sfun.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -8,7 +8,7 @@
   imports Cfun
 begin
 
-pcpodef ('a, 'b) sfun (infixr \<open>\<rightarrow>!\<close> 0) = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
+pcpodef ('a::pcpo, 'b::pcpo) sfun (infixr \<open>\<rightarrow>!\<close> 0) = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
   by simp_all
 
 type_notation (ASCII)
@@ -16,10 +16,10 @@
 
 text \<open>TODO: Define nice syntax for abstraction, application.\<close>
 
-definition sfun_abs :: "('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow>! 'b)"
+definition sfun_abs :: "('a::pcpo \<rightarrow> 'b::pcpo) \<rightarrow> ('a \<rightarrow>! 'b)"
   where "sfun_abs = (\<Lambda> f. Abs_sfun (strictify\<cdot>f))"
 
-definition sfun_rep :: "('a \<rightarrow>! 'b) \<rightarrow> 'a \<rightarrow> 'b"
+definition sfun_rep :: "('a::pcpo \<rightarrow>! 'b::pcpo) \<rightarrow> 'a \<rightarrow> 'b"
   where "sfun_rep = (\<Lambda> f. Rep_sfun f)"
 
 lemma sfun_rep_beta: "sfun_rep\<cdot>f = Rep_sfun f"
diff -r c3190d0b068c -r b6df83045178 src/HOL/HOLCF/Sprod.thy
--- a/src/HOL/HOLCF/Sprod.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/Sprod.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -9,14 +9,12 @@
   imports Cfun
 begin
 
-default_sort pcpo
-
-
 subsection \<open>Definition of strict product type\<close>
 
-definition "sprod = {p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
+definition "sprod = {p::'a::pcpo \<times> 'b::pcpo. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
 
-pcpodef ('a, 'b) sprod  (\<open>(\<open>notation=\<open>infix strict product\<close>\<close>_ \<otimes>/ _)\<close> [21,20] 20) = "sprod :: ('a \<times> 'b) set"
+pcpodef ('a::pcpo, 'b::pcpo) sprod  (\<open>(\<open>notation=\<open>infix strict product\<close>\<close>_ \<otimes>/ _)\<close> [21,20] 20) =
+  "sprod :: ('a \<times> 'b) set"
   by (simp_all add: sprod_def)
 
 instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
@@ -28,16 +26,16 @@
 
 subsection \<open>Definitions of constants\<close>
 
-definition sfst :: "('a ** 'b) \<rightarrow> 'a"
+definition sfst :: "('a::pcpo ** 'b::pcpo) \<rightarrow> 'a"
   where "sfst = (\<Lambda> p. fst (Rep_sprod p))"
 
-definition ssnd :: "('a ** 'b) \<rightarrow> 'b"
+definition ssnd :: "('a::pcpo ** 'b::pcpo) \<rightarrow> 'b"
   where "ssnd = (\<Lambda> p. snd (Rep_sprod p))"
 
-definition spair :: "'a \<rightarrow> 'b \<rightarrow> ('a ** 'b)"
+definition spair :: "'a::pcpo \<rightarrow> 'b::pcpo \<rightarrow> ('a ** 'b)"
   where "spair = (\<Lambda> a b. Abs_sprod (seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b))"
 
-definition ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c"
+definition ssplit :: "('a::pcpo \<rightarrow> 'b::pcpo \<rightarrow> 'c::pcpo) \<rightarrow> ('a ** 'b) \<rightarrow> 'c"
   where "ssplit = (\<Lambda> f p. seq\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
 
 syntax
diff -r c3190d0b068c -r b6df83045178 src/HOL/HOLCF/Ssum.thy
--- a/src/HOL/HOLCF/Ssum.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/Ssum.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -9,17 +9,15 @@
   imports Tr
 begin
 
-default_sort pcpo
-
-
 subsection \<open>Definition of strict sum type\<close>
 
 definition "ssum =
-  {p :: tr \<times> ('a \<times> 'b). p = \<bottom> \<or>
+  {p :: tr \<times> ('a::pcpo \<times> 'b::pcpo). p = \<bottom> \<or>
     (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
     (fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>)}"
 
-pcpodef ('a, 'b) ssum  (\<open>(\<open>notation=\<open>infix strict sum\<close>\<close>_ \<oplus>/ _)\<close> [21, 20] 20) = "ssum :: (tr \<times> 'a \<times> 'b) set"
+pcpodef ('a::pcpo, 'b::pcpo) ssum  (\<open>(\<open>notation=\<open>infix strict sum\<close>\<close>_ \<oplus>/ _)\<close> [21, 20] 20) =
+  "ssum :: (tr \<times> 'a \<times> 'b) set"
   by (simp_all add: ssum_def)
 
 instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
@@ -31,10 +29,10 @@
 
 subsection \<open>Definitions of constructors\<close>
 
-definition sinl :: "'a \<rightarrow> ('a ++ 'b)"
+definition sinl :: "'a::pcpo \<rightarrow> ('a ++ 'b::pcpo)"
   where "sinl = (\<Lambda> a. Abs_ssum (seq\<cdot>a\<cdot>TT, a, \<bottom>))"
 
-definition sinr :: "'b \<rightarrow> ('a ++ 'b)"
+definition sinr :: "'b::pcpo \<rightarrow> ('a::pcpo ++ 'b)"
   where "sinr = (\<Lambda> b. Abs_ssum (seq\<cdot>b\<cdot>FF, \<bottom>, b))"
 
 lemma sinl_ssum: "(seq\<cdot>a\<cdot>TT, a, \<bottom>) \<in> ssum"
@@ -161,7 +159,7 @@
 
 subsection \<open>Case analysis combinator\<close>
 
-definition sscase :: "('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c"
+definition sscase :: "('a::pcpo \<rightarrow> 'c::pcpo) \<rightarrow> ('b::pcpo \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c"
   where "sscase = (\<Lambda> f g s. (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y) (Rep_ssum s))"
 
 translations
diff -r c3190d0b068c -r b6df83045178 src/HOL/HOLCF/Tr.thy
--- a/src/HOL/HOLCF/Tr.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/Tr.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -58,12 +58,10 @@
 
 subsection \<open>Case analysis\<close>
 
-default_sort pcpo
-
-definition tr_case :: "'a \<rightarrow> 'a \<rightarrow> tr \<rightarrow> 'a"
+definition tr_case :: "'a::pcpo \<rightarrow> 'a \<rightarrow> tr \<rightarrow> 'a"
   where "tr_case = (\<Lambda> t e (Def b). if b then t else e)"
 
-abbreviation cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c"  (\<open>(\<open>notation=\<open>mixfix If expression\<close>\<close>If (_)/ then (_)/ else (_))\<close> [0, 0, 60] 60)
+abbreviation cifte_syn :: "[tr, 'c::pcpo, 'c] \<Rightarrow> 'c"  (\<open>(\<open>notation=\<open>mixfix If expression\<close>\<close>If (_)/ then (_)/ else (_))\<close> [0, 0, 60] 60)
   where "If b then e1 else e2 \<equiv> tr_case\<cdot>e1\<cdot>e2\<cdot>b"
 
 translations
@@ -94,7 +92,7 @@
 definition neg :: "tr \<rightarrow> tr"
   where "neg = flift2 Not"
 
-definition If2 :: "tr \<Rightarrow> 'c \<Rightarrow> 'c \<Rightarrow> 'c"
+definition If2 :: "tr \<Rightarrow> 'c::pcpo \<Rightarrow> 'c \<Rightarrow> 'c"
   where "If2 Q x y = (If Q then x else y)"
 
 text \<open>tactic for tr-thms with case split\<close>
diff -r c3190d0b068c -r b6df83045178 src/HOL/HOLCF/Universal.thy
--- a/src/HOL/HOLCF/Universal.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/Universal.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -255,7 +255,7 @@
 by (rule typedef_po)
 
 definition
-  approximants :: "'a \<Rightarrow> 'a compact_basis set" where
+  approximants :: "'a::pcpo \<Rightarrow> 'a compact_basis set" where
   "approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
 
 definition
diff -r c3190d0b068c -r b6df83045178 src/HOL/HOLCF/Up.thy
--- a/src/HOL/HOLCF/Up.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/Up.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -9,9 +9,6 @@
   imports Cfun
 begin
 
-default_sort cpo
-
-
 subsection \<open>Definition of new type for lifting\<close>
 
 datatype 'a u  (\<open>(\<open>notation=\<open>postfix lifting\<close>\<close>_\<^sub>\<bottom>)\<close> [1000] 999) = Ibottom | Iup 'a
diff -r c3190d0b068c -r b6df83045178 src/HOL/HOLCF/UpperPD.thy
--- a/src/HOL/HOLCF/UpperPD.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/UpperPD.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -11,7 +11,7 @@
 subsection \<open>Basis preorder\<close>
 
 definition
-  upper_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix \<open>\<le>\<sharp>\<close> 50) where
+  upper_le :: "'a::bifinite pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix \<open>\<le>\<sharp>\<close> 50) where
   "upper_le = (\<lambda>u v. \<forall>y\<in>Rep_pd_basis v. \<exists>x\<in>Rep_pd_basis u. x \<sqsubseteq> y)"
 
 lemma upper_le_refl [simp]: "t \<le>\<sharp> t"
@@ -72,7 +72,7 @@
 
 subsection \<open>Type definition\<close>
 
-typedef 'a upper_pd  (\<open>(\<open>notation=\<open>postfix upper_pd\<close>\<close>'(_')\<sharp>)\<close>) =
+typedef 'a::bifinite upper_pd  (\<open>(\<open>notation=\<open>postfix upper_pd\<close>\<close>'(_')\<sharp>)\<close>) =
   "{S::'a pd_basis set. upper_le.ideal S}"
 by (rule upper_le.ex_ideal)
 
@@ -94,7 +94,7 @@
 by (rule upper_le.typedef_ideal_cpo)
 
 definition
-  upper_principal :: "'a pd_basis \<Rightarrow> 'a upper_pd" where
+  upper_principal :: "'a::bifinite pd_basis \<Rightarrow> 'a upper_pd" where
   "upper_principal t = Abs_upper_pd {u. u \<le>\<sharp> t}"
 
 interpretation upper_pd:
@@ -118,16 +118,16 @@
 subsection \<open>Monadic unit and plus\<close>
 
 definition
-  upper_unit :: "'a \<rightarrow> 'a upper_pd" where
+  upper_unit :: "'a::bifinite \<rightarrow> 'a upper_pd" where
   "upper_unit = compact_basis.extension (\<lambda>a. upper_principal (PDUnit a))"
 
 definition
-  upper_plus :: "'a upper_pd \<rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd" where
+  upper_plus :: "'a::bifinite upper_pd \<rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd" where
   "upper_plus = upper_pd.extension (\<lambda>t. upper_pd.extension (\<lambda>u.
       upper_principal (PDPlus t u)))"
 
 abbreviation
-  upper_add :: "'a upper_pd \<Rightarrow> 'a upper_pd \<Rightarrow> 'a upper_pd"
+  upper_add :: "'a::bifinite upper_pd \<Rightarrow> 'a upper_pd \<Rightarrow> 'a upper_pd"
     (infixl \<open>\<union>\<sharp>\<close> 65) where
   "xs \<union>\<sharp> ys == upper_plus\<cdot>xs\<cdot>ys"
 
@@ -266,7 +266,7 @@
   assumes P: "adm P"
   assumes unit: "\<And>x. P {x}\<sharp>"
   assumes insert: "\<And>x ys. \<lbrakk>P {x}\<sharp>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<sharp> \<union>\<sharp> ys)"
-  shows "P (xs::'a upper_pd)"
+  shows "P (xs::'a::bifinite upper_pd)"
 apply (induct xs rule: upper_pd.principal_induct, rule P)
 apply (induct_tac a rule: pd_basis_induct1)
 apply (simp only: upper_unit_Rep_compact_basis [symmetric])
@@ -281,7 +281,7 @@
   assumes P: "adm P"
   assumes unit: "\<And>x. P {x}\<sharp>"
   assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<sharp> ys)"
-  shows "P (xs::'a upper_pd)"
+  shows "P (xs::'a::bifinite upper_pd)"
 apply (induct xs rule: upper_pd.principal_induct, rule P)
 apply (induct_tac a rule: pd_basis_induct)
 apply (simp only: upper_unit_Rep_compact_basis [symmetric] unit)
@@ -293,7 +293,7 @@
 
 definition
   upper_bind_basis ::
-  "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b upper_pd" where
+  "'a::bifinite pd_basis \<Rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b::bifinite upper_pd" where
   "upper_bind_basis = fold_pd
     (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
     (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<sharp> y\<cdot>f)"
@@ -327,7 +327,7 @@
 done
 
 definition
-  upper_bind :: "'a upper_pd \<rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b upper_pd" where
+  upper_bind :: "'a::bifinite upper_pd \<rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b::bifinite upper_pd" where
   "upper_bind = upper_pd.extension upper_bind_basis"
 
 syntax
@@ -364,7 +364,7 @@
 subsection \<open>Map\<close>
 
 definition
-  upper_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a upper_pd \<rightarrow> 'b upper_pd" where
+  upper_map :: "('a::bifinite \<rightarrow> 'b::bifinite) \<rightarrow> 'a upper_pd \<rightarrow> 'b upper_pd" where
   "upper_map = (\<Lambda> f xs. upper_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<sharp>))"
 
 lemma upper_map_unit [simp]:
@@ -472,7 +472,7 @@
 subsection \<open>Join\<close>
 
 definition
-  upper_join :: "'a upper_pd upper_pd \<rightarrow> 'a upper_pd" where
+  upper_join :: "'a::bifinite upper_pd upper_pd \<rightarrow> 'a upper_pd" where
   "upper_join = (\<Lambda> xss. upper_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))"
 
 lemma upper_join_unit [simp]: