(* Title: HOL/HOLCF/Cpodef.thy Author: Brian Huffman *) section {* 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