Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HOLCF/Completion.thy
changeset 81583 b6df83045178
parent 81577 a712bf5ccab0 
--- 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}"
isabelle