# HG changeset patch
# User huffman
# Date 1287755925 25200
# Node ID 8adc57fb8454c99e3556894b5e100f20e571fa53
# Parent  49b9d301fadb8bb2eb439bc554f59fd14b0fbe6d
remove finite_po class

diff -r 49b9d301fadb -r 8adc57fb8454 src/HOLCF/Cfun.thy
--- 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
diff -r 49b9d301fadb -r 8adc57fb8454 src/HOLCF/Discrete.thy
--- 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)
diff -r 49b9d301fadb -r 8adc57fb8454 src/HOLCF/Fun_Cpo.thy
--- 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"
diff -r 49b9d301fadb -r 8adc57fb8454 src/HOLCF/Library/Sum_Cpo.thy
--- 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)
 
diff -r 49b9d301fadb -r 8adc57fb8454 src/HOLCF/Lift.thy
--- 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
diff -r 49b9d301fadb -r 8adc57fb8454 src/HOLCF/Pcpo.thy
--- 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
diff -r 49b9d301fadb -r 8adc57fb8454 src/HOLCF/Pcpodef.thy
--- 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:
diff -r 49b9d301fadb -r 8adc57fb8454 src/HOLCF/Product_Cpo.thy
--- 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"
diff -r 49b9d301fadb -r 8adc57fb8454 src/HOLCF/Sprod.thy
--- 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])
 
diff -r 49b9d301fadb -r 8adc57fb8454 src/HOLCF/Ssum.thy
--- 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])
 
diff -r 49b9d301fadb -r 8adc57fb8454 src/HOLCF/Up.thy
--- 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: