# HG changeset patch
# User wenzelm
# Date 1734003359 -3600
# Node ID c3190d0b068c08f54e9ff2c7a0570c7f4c799141
# Parent  8a360893360759efbe462e422c86226d7b29746b
clarified specification context;

diff -r 8a3608933607 -r c3190d0b068c src/HOL/HOLCF/Cpo.thy
--- a/src/HOL/HOLCF/Cpo.thy	Wed Dec 11 12:04:27 2024 +0100
+++ b/src/HOL/HOLCF/Cpo.thy	Thu Dec 12 12:35:59 2024 +0100
@@ -808,7 +808,10 @@
 
 subsection \<open>Definitions\<close>
 
-definition adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool"
+context cpo
+begin
+
+definition adm :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
   where "adm P \<longleftrightarrow> (\<forall>Y. chain Y \<longrightarrow> (\<forall>i. P (Y i)) \<longrightarrow> P (\<Squnion>i. Y i))"
 
 lemma admI: "(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P"
@@ -823,6 +826,8 @@
 lemma triv_admI: "\<forall>x. P x \<Longrightarrow> adm P"
   by (rule admI) (erule spec)
 
+end
+
 
 subsection \<open>Admissibility on chain-finite types\<close>
 
@@ -835,6 +840,9 @@
 
 subsection \<open>Admissibility of special formulae and propagation\<close>
 
+context cpo
+begin
+
 lemma adm_const [simp]: "adm (\<lambda>x. t)"
   by (rule admI, simp)
 
@@ -897,6 +905,8 @@
 lemma adm_iff [simp]: "adm (\<lambda>x. P x \<longrightarrow> Q x) \<Longrightarrow> adm (\<lambda>x. Q x \<longrightarrow> P x) \<Longrightarrow> adm (\<lambda>x. P x \<longleftrightarrow> Q x)"
   by (subst iff_conv_conj_imp) (rule adm_conj)
 
+end
+
 text \<open>admissibility and continuity\<close>
 
 lemma adm_below [simp]: "cont (\<lambda>x. u x) \<Longrightarrow> cont (\<lambda>x. v x) \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
@@ -914,7 +924,10 @@
 
 subsection \<open>Compactness\<close>
 
-definition compact :: "'a::cpo \<Rightarrow> bool"
+context cpo
+begin
+
+definition compact :: "'a \<Rightarrow> bool"
   where "compact k = adm (\<lambda>x. k \<notsqsubseteq> x)"
 
 lemma compactI: "adm (\<lambda>x. k \<notsqsubseteq> x) \<Longrightarrow> compact k"
@@ -932,6 +945,8 @@
 lemma compact_below_lub_iff: "compact x \<Longrightarrow> chain Y \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. Y i) \<longleftrightarrow> (\<exists>i. x \<sqsubseteq> Y i)"
   by (fast intro: compactD2 elim: below_lub)
 
+end
+
 lemma compact_chfin [simp]: "compact x"
   for x :: "'a::chfin"
   by (rule compactI [OF adm_chfin])