instances for class discrete_cpo

--- a/src/HOLCF/Cfun.thy	Thu Jan 31 21:22:03 2008 +0100
+++ b/src/HOLCF/Cfun.thy	Thu Jan 31 21:23:14 2008 +0100
@@ -109,6 +109,9 @@
 instance "->" :: (finite_po, chfin) chfin
 by (rule typedef_chfin [OF type_definition_CFun less_CFun_def])
 
+instance "->" :: (cpo, discrete_cpo) discrete_cpo
+by intro_classes (simp add: less_CFun_def Rep_CFun_inject)
+
 instance "->" :: (cpo, pcpo) pcpo
 by (rule typedef_pcpo [OF type_definition_CFun less_CFun_def UU_CFun])
 

--- a/src/HOLCF/Cprod.thy	Thu Jan 31 21:22:03 2008 +0100
+++ b/src/HOLCF/Cprod.thy	Thu Jan 31 21:23:14 2008 +0100
@@ -15,16 +15,17 @@
 
 subsection {* Type @{typ unit} is a pcpo *}
 
-instantiation unit :: po
+instantiation unit :: sq_ord
 begin
 
 definition
   less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True"
 
-instance
-by intro_classes simp_all
+instance ..
+end
 
-end
+instance unit :: discrete_cpo
+by intro_classes simp
 
 instance unit :: finite_po ..
 
@@ -135,6 +136,14 @@
 
 instance "*" :: (finite_po, finite_po) finite_po ..
 
+instance "*" :: (discrete_cpo, discrete_cpo) discrete_cpo
+proof
+  fix x y :: "'a \<times> 'b"
+  show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
+    unfolding less_cprod_def Pair_fst_snd_eq
+    by simp
+qed
+
 subsection {* Product type is pointed *}
 
 lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"

--- a/src/HOLCF/Discrete.thy	Thu Jan 31 21:22:03 2008 +0100
+++ b/src/HOLCF/Discrete.thy	Thu Jan 31 21:23:14 2008 +0100
@@ -13,24 +13,20 @@
 
 datatype 'a discr = Discr "'a :: type"
 
-subsection {* Type @{typ "'a discr"} is a partial order *}
+subsection {* Type @{typ "'a discr"} is a discrete cpo *}
 
-instantiation discr :: (type) po
+instantiation discr :: (type) sq_ord
 begin
 
 definition
-  less_discr_def [simp]:
+  less_discr_def:
     "(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
 
-instance
-proof
-  fix x y z :: "'a discr"
-  show "x << x" by simp
-  { assume "x << y" and "y << x" thus "x = y" by simp }
-  { assume "x << y" and "y << z" thus "x << z" by simp }
-qed
+instance ..
+end
 
-end
+instance discr :: (type) discrete_cpo
+by intro_classes (simp add: less_discr_def)
 
 lemma discr_less_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
 by simp
@@ -73,16 +69,17 @@
   undiscr :: "('a::type)discr => 'a" where
   "undiscr x = (case x of Discr y => y)"
 
-lemma undiscr_Discr [simp]: "undiscr(Discr x) = x"
+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
+
 lemma discr_chain_f_range0:
  "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}"
 by (fast dest: discr_chain0 elim: arg_cong)
 
 lemma cont_discr [iff]: "cont (%x::('a::type)discr. f x)"
-apply (rule chfindom_monofun2cont)
-apply (rule monofunI, simp)
-done
+by (rule cont_discrete_cpo)
 
 end

--- a/src/HOLCF/Ffun.thy	Thu Jan 31 21:22:03 2008 +0100
+++ b/src/HOLCF/Ffun.thy	Thu Jan 31 21:23:14 2008 +0100
@@ -98,6 +98,14 @@
 
 instance "fun" :: (finite, finite_po) finite_po ..
 
+instance "fun" :: (type, discrete_cpo) discrete_cpo
+proof
+  fix f g :: "'a \<Rightarrow> 'b"
+  show "f \<sqsubseteq> g \<longleftrightarrow> f = g" 
+    unfolding expand_fun_less expand_fun_eq
+    by simp
+qed
+
 text {* chain-finite function spaces *}
 
 lemma maxinch2maxinch_lambda: