--- a/src/HOLCF/Cfun.thy Fri Oct 22 07:44:34 2010 -0700
+++ b/src/HOLCF/Cfun.thy Fri Oct 22 07:45:32 2010 -0700
@@ -95,9 +95,6 @@
lemma UU_CFun: "\<bottom> \<in> CFun"
by (simp add: CFun_def inst_fun_pcpo)
-instance cfun :: ("{finite,cpo}", chfin) chfin
-by (rule typedef_chfin [OF type_definition_CFun below_CFun_def])
-
instance cfun :: (cpo, discrete_cpo) discrete_cpo
by intro_classes (simp add: below_CFun_def Rep_CFun_inject)
--- a/src/HOLCF/Discrete.thy Fri Oct 22 07:44:34 2010 -0700
+++ b/src/HOLCF/Discrete.thy Fri Oct 22 07:45:32 2010 -0700
@@ -44,13 +44,6 @@
"!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"
by (fast elim: discr_chain0)
-instance discr :: (type) chfin
-apply intro_classes
-apply (rule_tac x=0 in exI)
-apply (unfold max_in_chain_def)
-apply (clarify, erule discr_chain0 [symmetric])
-done
-
subsection {* \emph{undiscr} *}
definition
--- a/src/HOLCF/Fun_Cpo.thy Fri Oct 22 07:44:34 2010 -0700
+++ b/src/HOLCF/Fun_Cpo.thy Fri Oct 22 07:45:32 2010 -0700
@@ -110,24 +110,6 @@
from Yij Yik show "Y j = Y k" by auto
qed
-instance "fun" :: (finite, chfin) chfin
-proof
- fix Y :: "nat \<Rightarrow> 'a \<Rightarrow> 'b"
- let ?n = "\<lambda>x. LEAST n. max_in_chain n (\<lambda>i. Y i x)"
- assume "chain Y"
- hence "\<And>x. chain (\<lambda>i. Y i x)"
- by (rule ch2ch_fun)
- hence "\<And>x. \<exists>n. max_in_chain n (\<lambda>i. Y i x)"
- by (rule chfin)
- hence "\<And>x. max_in_chain (?n x) (\<lambda>i. Y i x)"
- by (rule LeastI_ex)
- hence "\<And>x. max_in_chain (Max (range ?n)) (\<lambda>i. Y i x)"
- by (rule maxinch_mono [OF _ Max_ge], simp_all)
- hence "max_in_chain (Max (range ?n)) Y"
- by (rule maxinch2maxinch_lambda)
- thus "\<exists>n. max_in_chain n Y" ..
-qed
-
instance "fun" :: (type, discrete_cpo) discrete_cpo
proof
fix f g :: "'a \<Rightarrow> 'b"
--- a/src/HOLCF/Pcpo.thy Fri Oct 22 07:44:34 2010 -0700
+++ b/src/HOLCF/Pcpo.thy Fri Oct 22 07:45:32 2010 -0700
@@ -287,7 +287,7 @@
end
-text {* Discrete cpos *}
+subsection {* Discrete cpos *}
class discrete_cpo = below +
assumes discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y"
@@ -308,14 +308,14 @@
thus "S i = S 0" by (rule sym)
qed
-subclass cpo
+subclass chfin
proof
fix S :: "nat \<Rightarrow> 'a"
assume S: "chain S"
- hence "\<exists>x. S = (\<lambda>i. x)"
- by (rule discrete_chain_const)
- thus "\<exists>x. range S <<| x"
- by (fast intro: lub_const)
+ hence "\<exists>x. S = (\<lambda>i. x)" by (rule discrete_chain_const)
+ hence "max_in_chain 0 S"
+ unfolding max_in_chain_def by auto
+ thus "\<exists>i. max_in_chain i S" ..
qed
end