--- 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"