--- 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