src/HOLCF/Discrete.thy

 imports Cont
 begin
 
 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 =)"
+  "(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
 
-instance ..
+instance
+by default (simp add: below_discr_def)
+
 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? *)
-
-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
-
-lemma discr_chain_range0 [simp]: 
- "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"
-by (fast elim: discr_chain0)
 
 subsection {* \emph{undiscr} *}
 
 definition
   undiscr :: "('a::type)discr => 'a" where

 by (simp add: undiscr_def)
 
 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