--- a/src/HOLCF/Cfun.thy Fri Oct 22 06:08:51 2010 -0700
+++ b/src/HOLCF/Cfun.thy Fri Oct 22 06:58:45 2010 -0700
@@ -95,10 +95,7 @@
lemma UU_CFun: "\<bottom> \<in> CFun"
by (simp add: CFun_def inst_fun_pcpo)
-instance cfun :: (finite_po, finite_po) finite_po
-by (rule typedef_finite_po [OF type_definition_CFun])
-
-instance cfun :: (finite_po, chfin) chfin
+instance cfun :: ("{finite,cpo}", chfin) chfin
by (rule typedef_chfin [OF type_definition_CFun below_CFun_def])
instance cfun :: (cpo, discrete_cpo) discrete_cpo
--- a/src/HOLCF/Discrete.thy Fri Oct 22 06:08:51 2010 -0700
+++ b/src/HOLCF/Discrete.thy Fri Oct 22 06:58:45 2010 -0700
@@ -44,15 +44,6 @@
"!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"
by (fast elim: discr_chain0)
-instance discr :: (finite) finite_po
-proof
- have "finite (Discr ` (UNIV :: 'a set))"
- by (rule finite_imageI [OF finite])
- also have "(Discr ` (UNIV :: 'a set)) = UNIV"
- by (auto, case_tac x, auto)
- finally show "finite (UNIV :: 'a discr set)" .
-qed
-
instance discr :: (type) chfin
apply intro_classes
apply (rule_tac x=0 in exI)
--- a/src/HOLCF/Fun_Cpo.thy Fri Oct 22 06:08:51 2010 -0700
+++ b/src/HOLCF/Fun_Cpo.thy Fri Oct 22 06:58:45 2010 -0700
@@ -128,8 +128,6 @@
thus "\<exists>n. max_in_chain n Y" ..
qed
-instance "fun" :: (finite, finite_po) finite_po ..
-
instance "fun" :: (type, discrete_cpo) discrete_cpo
proof
fix f g :: "'a \<Rightarrow> 'b"
--- a/src/HOLCF/Library/Sum_Cpo.thy Fri Oct 22 06:08:51 2010 -0700
+++ b/src/HOLCF/Library/Sum_Cpo.thy Fri Oct 22 06:58:45 2010 -0700
@@ -213,8 +213,6 @@
apply (case_tac "\<Squnion>i. Y i", simp_all)
done
-instance sum :: (finite_po, finite_po) finite_po ..
-
instance sum :: (discrete_cpo, discrete_cpo) discrete_cpo
by intro_classes (simp add: below_sum_def split: sum.split)
--- a/src/HOLCF/Lift.thy Fri Oct 22 06:08:51 2010 -0700
+++ b/src/HOLCF/Lift.thy Fri Oct 22 06:58:45 2010 -0700
@@ -13,9 +13,6 @@
pcpodef (open) 'a lift = "UNIV :: 'a discr u set"
by simp_all
-instance lift :: (finite) finite_po
-by (rule typedef_finite_po [OF type_definition_lift])
-
lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]
definition
--- a/src/HOLCF/Pcpo.thy Fri Oct 22 06:08:51 2010 -0700
+++ b/src/HOLCF/Pcpo.thy Fri Oct 22 06:58:45 2010 -0700
@@ -262,18 +262,6 @@
end
-class finite_po = finite + po
-begin
-
-subclass chfin
-apply default
-apply (drule finite_range_imp_finch)
-apply (rule finite)
-apply (simp add: finite_chain_def)
-done
-
-end
-
class flat = pcpo +
assumes ax_flat: "x \<sqsubseteq> y \<Longrightarrow> x = \<bottom> \<or> x = y"
begin
--- a/src/HOLCF/Pcpodef.thy Fri Oct 22 06:08:51 2010 -0700
+++ b/src/HOLCF/Pcpodef.thy Fri Oct 22 06:58:45 2010 -0700
@@ -46,15 +46,6 @@
by (simp only: type_definition.Abs_image [OF type])
qed
-theorem typedef_finite_po:
- fixes Abs :: "'a::finite_po \<Rightarrow> 'b::po"
- assumes type: "type_definition Rep Abs A"
- shows "OFCLASS('b, finite_po_class)"
- apply (intro_classes)
- apply (rule typedef_finite_UNIV [OF type])
- apply (rule finite)
-done
-
subsection {* Proving a subtype is chain-finite *}
lemma ch2ch_Rep:
--- a/src/HOLCF/Product_Cpo.thy Fri Oct 22 06:08:51 2010 -0700
+++ b/src/HOLCF/Product_Cpo.thy Fri Oct 22 06:58:45 2010 -0700
@@ -24,8 +24,6 @@
instance unit :: discrete_cpo
by intro_classes simp
-instance unit :: finite_po ..
-
instance unit :: pcpo
by intro_classes simp
@@ -157,8 +155,6 @@
thus "\<exists>x. range S <<| x" ..
qed
-instance prod :: (finite_po, finite_po) finite_po ..
-
instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo
proof
fix x y :: "'a \<times> 'b"
--- a/src/HOLCF/Sprod.thy Fri Oct 22 06:08:51 2010 -0700
+++ b/src/HOLCF/Sprod.thy Fri Oct 22 06:58:45 2010 -0700
@@ -16,9 +16,6 @@
"{p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
by simp_all
-instance sprod :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
-by (rule typedef_finite_po [OF type_definition_Sprod])
-
instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
by (rule typedef_chfin [OF type_definition_Sprod below_Sprod_def])
--- a/src/HOLCF/Ssum.thy Fri Oct 22 06:08:51 2010 -0700
+++ b/src/HOLCF/Ssum.thy Fri Oct 22 06:58:45 2010 -0700
@@ -18,9 +18,6 @@
(fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>) }"
by simp_all
-instance ssum :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
-by (rule typedef_finite_po [OF type_definition_Ssum])
-
instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def])
--- a/src/HOLCF/Up.thy Fri Oct 22 06:08:51 2010 -0700
+++ b/src/HOLCF/Up.thy Fri Oct 22 06:58:45 2010 -0700
@@ -62,13 +62,6 @@
by (auto split: u.split_asm intro: below_trans)
qed
-lemma u_UNIV: "UNIV = insert Ibottom (range Iup)"
-by (auto, case_tac x, auto)
-
-instance u :: (finite_po) finite_po
-by (intro_classes, simp add: u_UNIV)
-
-
subsection {* Lifted cpo is a cpo *}
lemma is_lub_Iup: