(* Title: HOL/HOLCF/Cpodef.thy

Author: Brian Huffman

*)

header {* Subtypes of pcpos *}

theory Cpodef

imports Adm

keywords "pcpodef" "cpodef" :: thy_goal

begin

subsection {* Proving a subtype is a partial order *}

text {*

A subtype of a partial order is itself a partial order,

if the ordering is defined in the standard way.

*}

setup {* Sign.add_const_constraint (@{const_name Porder.below}, NONE) *}

theorem typedef_po:

fixes Abs :: "'a::po => 'b::type"

assumes type: "type_definition Rep Abs A"

and below: "op \<sqsubseteq> ≡ λx y. Rep x \<sqsubseteq> Rep y"

shows "OFCLASS('b, po_class)"

apply (intro_classes, unfold below)

apply (rule below_refl)

apply (erule (1) below_trans)

apply (rule type_definition.Rep_inject [OF type, THEN iffD1])

apply (erule (1) below_antisym)

done

setup {* Sign.add_const_constraint (@{const_name Porder.below},

SOME @{typ "'a::below => 'a::below => bool"}) *}

subsection {* Proving a subtype is finite *}

lemma typedef_finite_UNIV:

fixes Abs :: "'a::type => 'b::type"

assumes type: "type_definition Rep Abs A"

shows "finite A ==> finite (UNIV :: 'b set)"

proof -

assume "finite A"

hence "finite (Abs ` A)" by (rule finite_imageI)

thus "finite (UNIV :: 'b set)"

by (simp only: type_definition.Abs_image [OF type])

qed

subsection {* Proving a subtype is chain-finite *}

lemma ch2ch_Rep:

assumes below: "op \<sqsubseteq> ≡ λx y. Rep x \<sqsubseteq> Rep y"

shows "chain S ==> chain (λi. Rep (S i))"

unfolding chain_def below .

theorem typedef_chfin:

fixes Abs :: "'a::chfin => 'b::po"

assumes type: "type_definition Rep Abs A"

and below: "op \<sqsubseteq> ≡ λx y. Rep x \<sqsubseteq> Rep y"

shows "OFCLASS('b, chfin_class)"

apply intro_classes

apply (drule ch2ch_Rep [OF below])

apply (drule chfin)

apply (unfold max_in_chain_def)

apply (simp add: type_definition.Rep_inject [OF type])

done

subsection {* Proving a subtype is complete *}

text {*

A subtype of a cpo is itself a cpo if the ordering is

defined in the standard way, and the defining subset

is closed with respect to limits of chains. A set is

closed if and only if membership in the set is an

admissible predicate.

*}

lemma typedef_is_lubI:

assumes below: "op \<sqsubseteq> ≡ λx y. Rep x \<sqsubseteq> Rep y"

shows "range (λi. Rep (S i)) <<| Rep x ==> range S <<| x"

unfolding is_lub_def is_ub_def below by simp

lemma Abs_inverse_lub_Rep:

fixes Abs :: "'a::cpo => 'b::po"

assumes type: "type_definition Rep Abs A"

and below: "op \<sqsubseteq> ≡ λx y. Rep x \<sqsubseteq> Rep y"

and adm: "adm (λx. x ∈ A)"

shows "chain S ==> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"

apply (rule type_definition.Abs_inverse [OF type])

apply (erule admD [OF adm ch2ch_Rep [OF below]])

apply (rule type_definition.Rep [OF type])

done

theorem typedef_is_lub:

fixes Abs :: "'a::cpo => 'b::po"

assumes type: "type_definition Rep Abs A"

and below: "op \<sqsubseteq> ≡ λx y. Rep x \<sqsubseteq> Rep y"

and adm: "adm (λx. x ∈ A)"

shows "chain S ==> range S <<| Abs (\<Squnion>i. Rep (S i))"

proof -

assume S: "chain S"

hence "chain (λi. Rep (S i))" by (rule ch2ch_Rep [OF below])

hence "range (λi. Rep (S i)) <<| (\<Squnion>i. Rep (S i))" by (rule cpo_lubI)

hence "range (λi. Rep (S i)) <<| Rep (Abs (\<Squnion>i. Rep (S i)))"

by (simp only: Abs_inverse_lub_Rep [OF type below adm S])

thus "range S <<| Abs (\<Squnion>i. Rep (S i))"

by (rule typedef_is_lubI [OF below])

qed

lemmas typedef_lub = typedef_is_lub [THEN lub_eqI]

theorem typedef_cpo:

fixes Abs :: "'a::cpo => 'b::po"

assumes type: "type_definition Rep Abs A"

and below: "op \<sqsubseteq> ≡ λx y. Rep x \<sqsubseteq> Rep y"

and adm: "adm (λx. x ∈ A)"

shows "OFCLASS('b, cpo_class)"

proof

fix S::"nat => 'b" assume "chain S"

hence "range S <<| Abs (\<Squnion>i. Rep (S i))"

by (rule typedef_is_lub [OF type below adm])

thus "∃x. range S <<| x" ..

qed

subsubsection {* Continuity of \emph{Rep} and \emph{Abs} *}

text {* For any sub-cpo, the @{term Rep} function is continuous. *}

theorem typedef_cont_Rep:

fixes Abs :: "'a::cpo => 'b::cpo"

assumes type: "type_definition Rep Abs A"

and below: "op \<sqsubseteq> ≡ λx y. Rep x \<sqsubseteq> Rep y"

and adm: "adm (λx. x ∈ A)"

shows "cont (λx. f x) ==> cont (λx. Rep (f x))"

apply (erule cont_apply [OF _ _ cont_const])

apply (rule contI)

apply (simp only: typedef_lub [OF type below adm])

apply (simp only: Abs_inverse_lub_Rep [OF type below adm])

apply (rule cpo_lubI)

apply (erule ch2ch_Rep [OF below])

done

text {*

For a sub-cpo, we can make the @{term Abs} function continuous

only if we restrict its domain to the defining subset by

composing it with another continuous function.

*}

theorem typedef_cont_Abs:

fixes Abs :: "'a::cpo => 'b::cpo"

fixes f :: "'c::cpo => 'a::cpo"

assumes type: "type_definition Rep Abs A"

and below: "op \<sqsubseteq> ≡ λx y. Rep x \<sqsubseteq> Rep y"

and adm: "adm (λx. x ∈ A)" (* not used *)

and f_in_A: "!!x. f x ∈ A"

shows "cont f ==> cont (λx. Abs (f x))"

unfolding cont_def is_lub_def is_ub_def ball_simps below

by (simp add: type_definition.Abs_inverse [OF type f_in_A])

subsection {* Proving subtype elements are compact *}

theorem typedef_compact:

fixes Abs :: "'a::cpo => 'b::cpo"

assumes type: "type_definition Rep Abs A"

and below: "op \<sqsubseteq> ≡ λx y. Rep x \<sqsubseteq> Rep y"

and adm: "adm (λx. x ∈ A)"

shows "compact (Rep k) ==> compact k"

proof (unfold compact_def)

have cont_Rep: "cont Rep"

by (rule typedef_cont_Rep [OF type below adm cont_id])

assume "adm (λx. Rep k \<notsqsubseteq> x)"

with cont_Rep have "adm (λx. Rep k \<notsqsubseteq> Rep x)" by (rule adm_subst)

thus "adm (λx. k \<notsqsubseteq> x)" by (unfold below)

qed

subsection {* Proving a subtype is pointed *}

text {*

A subtype of a cpo has a least element if and only if

the defining subset has a least element.

*}

theorem typedef_pcpo_generic:

fixes Abs :: "'a::cpo => 'b::cpo"

assumes type: "type_definition Rep Abs A"

and below: "op \<sqsubseteq> ≡ λx y. Rep x \<sqsubseteq> Rep y"

and z_in_A: "z ∈ A"

and z_least: "!!x. x ∈ A ==> z \<sqsubseteq> x"

shows "OFCLASS('b, pcpo_class)"

apply (intro_classes)

apply (rule_tac x="Abs z" in exI, rule allI)

apply (unfold below)

apply (subst type_definition.Abs_inverse [OF type z_in_A])

apply (rule z_least [OF type_definition.Rep [OF type]])

done

text {*

As a special case, a subtype of a pcpo has a least element

if the defining subset contains @{term ⊥}.

*}

theorem typedef_pcpo:

fixes Abs :: "'a::pcpo => 'b::cpo"

assumes type: "type_definition Rep Abs A"

and below: "op \<sqsubseteq> ≡ λx y. Rep x \<sqsubseteq> Rep y"

and bottom_in_A: "⊥ ∈ A"

shows "OFCLASS('b, pcpo_class)"

by (rule typedef_pcpo_generic [OF type below bottom_in_A], rule minimal)

subsubsection {* Strictness of \emph{Rep} and \emph{Abs} *}

text {*

For a sub-pcpo where @{term ⊥} is a member of the defining

subset, @{term Rep} and @{term Abs} are both strict.

*}

theorem typedef_Abs_strict:

assumes type: "type_definition Rep Abs A"

and below: "op \<sqsubseteq> ≡ λx y. Rep x \<sqsubseteq> Rep y"

and bottom_in_A: "⊥ ∈ A"

shows "Abs ⊥ = ⊥"

apply (rule bottomI, unfold below)

apply (simp add: type_definition.Abs_inverse [OF type bottom_in_A])

done

theorem typedef_Rep_strict:

assumes type: "type_definition Rep Abs A"

and below: "op \<sqsubseteq> ≡ λx y. Rep x \<sqsubseteq> Rep y"

and bottom_in_A: "⊥ ∈ A"

shows "Rep ⊥ = ⊥"

apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst])

apply (rule type_definition.Abs_inverse [OF type bottom_in_A])

done

theorem typedef_Abs_bottom_iff:

assumes type: "type_definition Rep Abs A"

and below: "op \<sqsubseteq> ≡ λx y. Rep x \<sqsubseteq> Rep y"

and bottom_in_A: "⊥ ∈ A"

shows "x ∈ A ==> (Abs x = ⊥) = (x = ⊥)"

apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst])

apply (simp add: type_definition.Abs_inject [OF type] bottom_in_A)

done

theorem typedef_Rep_bottom_iff:

assumes type: "type_definition Rep Abs A"

and below: "op \<sqsubseteq> ≡ λx y. Rep x \<sqsubseteq> Rep y"

and bottom_in_A: "⊥ ∈ A"

shows "(Rep x = ⊥) = (x = ⊥)"

apply (rule typedef_Rep_strict [OF type below bottom_in_A, THEN subst])

apply (simp add: type_definition.Rep_inject [OF type])

done

subsection {* Proving a subtype is flat *}

theorem typedef_flat:

fixes Abs :: "'a::flat => 'b::pcpo"

assumes type: "type_definition Rep Abs A"

and below: "op \<sqsubseteq> ≡ λx y. Rep x \<sqsubseteq> Rep y"

and bottom_in_A: "⊥ ∈ A"

shows "OFCLASS('b, flat_class)"

apply (intro_classes)

apply (unfold below)

apply (simp add: type_definition.Rep_inject [OF type, symmetric])

apply (simp add: typedef_Rep_strict [OF type below bottom_in_A])

apply (simp add: ax_flat)

done

subsection {* HOLCF type definition package *}

ML_file "Tools/cpodef.ML"

end