--- 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"
--- 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 =
--- 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)"
--- 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:
--- 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}"
--- 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]:
--- 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"
--- 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"
--- 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 =
--- 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"
--- 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)"
--- 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)"
--- 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]:
--- 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"
--- 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>
--- 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"
--- 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
--- 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
--- 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>
--- 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
--- 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
--- 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]: