# HG changeset patch
# User huffman
# Date 1287758732 25200
# Node ID 1ca61fbd8a794c02ec10af8b34caca29f626ddf2
# Parent  d57357cda8bb89797f1d22445079de579ed66842
make discrete_cpo a subclass of chfin; remove chfin instances for fun, cfun

diff -r d57357cda8bb -r 1ca61fbd8a79 src/HOLCF/Cfun.thy
--- 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)
 
diff -r d57357cda8bb -r 1ca61fbd8a79 src/HOLCF/Discrete.thy
--- 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
diff -r d57357cda8bb -r 1ca61fbd8a79 src/HOLCF/Fun_Cpo.thy
--- 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"
diff -r d57357cda8bb -r 1ca61fbd8a79 src/HOLCF/Pcpo.thy
--- 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