src/HOLCF/Discrete.thy
 author huffman Sun, 19 Feb 2006 02:11:27 +0100 changeset 19105 3aabd46340e0 parent 16213 88ddef269510 child 25131 2c8caac48ade permissions -rw-r--r--
use minimal imports
```
(*  Title:      HOLCF/Discrete.thy
ID:         \$Id\$
Author:     Tobias Nipkow

Discrete CPOs.
*)

header {* Discrete cpo types *}

theory Discrete
imports Cont
begin

datatype 'a discr = Discr "'a :: type"

subsection {* Type @{typ "'a discr"} is a partial order *}

instance discr :: (type) sq_ord ..

less_discr_def: "((op <<)::('a::type)discr=>'a discr=>bool)  ==  op ="

lemma discr_less_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
by (unfold less_discr_def) (rule refl)

instance discr :: (type) po
proof
fix x y z :: "'a discr"
show "x << x" by simp
{ assume "x << y" and "y << x" thus "x = y" by simp }
{ assume "x << y" and "y << z" thus "x << z" by simp }
qed

subsection {* Type @{typ "'a discr"} is a cpo *}

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)

lemma discr_cpo:
"!!S. chain S ==> ? x::('a::type)discr. range(S) <<| x"
by (unfold is_lub_def is_ub_def) simp

instance discr :: (type) cpo
by intro_classes (rule discr_cpo)

subsection {* @{term undiscr} *}

constdefs
undiscr :: "('a::type)discr => 'a"
"undiscr x == (case x of Discr y => y)"

lemma undiscr_Discr [simp]: "undiscr(Discr x) = x"