# HG changeset patch
# User huffman
# Date 1288829181 25200
# Node ID f775e6e0dc998c1962ac592c9f2a5d1327c1be6e
# Parent  3128c2a54785e383f42a0eac6cb2ac56e3cff691
remove unnecessary stuff from Discrete.thy

diff -r 3128c2a54785 -r f775e6e0dc99 src/HOLCF/Discrete.thy
--- a/src/HOLCF/Discrete.thy	Wed Nov 03 16:39:23 2010 -0700
+++ b/src/HOLCF/Discrete.thy	Wed Nov 03 17:06:21 2010 -0700
@@ -10,39 +10,18 @@
 
 datatype 'a discr = Discr "'a :: type"
 
-subsection {* Discrete ordering *}
+subsection {* Discrete cpo class instance *}
 
-instantiation discr :: (type) below
+instantiation discr :: (type) discrete_cpo
 begin
 
 definition
-  below_discr_def:
-    "(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
-
-instance ..
-end
-
-subsection {* Discrete cpo class instance *}
-
-instance discr :: (type) discrete_cpo
-by intro_classes (simp add: below_discr_def)
-
-lemma discr_below_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
-by simp (* FIXME: same discrete_cpo - remove? is [iff] important? *)
+  "(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
 
-lemma discr_chain0: 
- "!!S::nat=>('a::type)discr. chain S ==> S i = S 0"
-apply (unfold chain_def)
-apply (induct_tac "i")
-apply (rule refl)
-apply (erule subst)
-apply (rule sym)
-apply fast
-done
+instance
+by default (simp add: below_discr_def)
 
-lemma discr_chain_range0 [simp]: 
- "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"
-by (fast elim: discr_chain0)
+end
 
 subsection {* \emph{undiscr} *}
 
@@ -56,11 +35,4 @@
 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)"
-by (rule cont_discrete_cpo)
-
 end