<commit_before>(*  Title:      HOLCF/Discrete.thy
    ID:         $Id$
    Author:     <NAME>

Discrete CPOs.
*)

header {* Discrete cpo types *}

theory Discrete
imports Cont Datatype
begin

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

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

instance discr :: (type) sq_ord ..

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

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)"
apply (unfold cont is_lub_def is_ub_def)
apply (simp add: discr_chain_f_range0)<commit_msg>replaced cont with cont_def<commit_after>(*  Title:      HOLCF/Discrete.thy
    ID:         $Id$
    Author:     <NAME>

Discrete CPOs.
*)

header {* Discrete cpo types *}

theory Discrete
imports Cont Datatype
begin

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

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

instance discr :: (type) sq_ord ..

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

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)"
apply (unfold cont_def is_lub_def is_ub_def)
apply (simp add: discr_chain_f_range0)
{'fraction_non_alphanumeric': 0.18672665916760406, 'fraction_numerical': 0.005061867266591676, 'mean_word_length': 4.155072463768116, 'pattern_counts': {'":': 0, '<': 41, '<?xml version=': 0, '>': 27, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1840503', 'n_tokens_mistral': 1534, 'n_tokens_neox': 1533, 'n_words': 440}