# HG changeset patch
# User wenzelm
# Date 1731526553 -3600
#      Wed Nov 13 20:35:53 2024 +0100
# Node ID e5e20175c534859bd1814eee51e5cb5fdeef7c20
# Parent  b3c0d032ed6e440172993616c562f932434ff893
avoid clash with HOL-Library.Discrete;

diff -r b3c0d032ed6e -r e5e20175c534 src/HOL/HOLCF/Lift.thy
--- a/src/HOL/HOLCF/Lift.thy	Wed Nov 13 20:14:24 2024 +0100
+++ b/src/HOL/HOLCF/Lift.thy	Wed Nov 13 20:35:53 2024 +0100
@@ -5,9 +5,40 @@
 section \<open>Lifting types of class type to flat pcpo's\<close>
 
 theory Lift
-imports Discrete Up
+imports Cont Up
+begin
+
+section \<open>Discrete cpo types\<close>
+
+datatype 'a discr = Discr "'a :: type"
+
+subsection \<open>Discrete cpo class instance\<close>
+
+instantiation discr :: (type) discrete_cpo
 begin
 
+definition "((\<sqsubseteq>) :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (=)"
+
+instance
+  by standard (simp add: below_discr_def)
+
+end
+
+
+subsection \<open>\emph{undiscr}\<close>
+
+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"
+  by (simp add: undiscr_def)
+
+lemma Discr_undiscr [simp]: "Discr (undiscr y) = y"
+  by (induct y) simp
+
+
+section \<open>Lifting types\<close>
+
 default_sort type
 
 pcpodef 'a lift = "UNIV :: 'a discr u set"