(* 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: "(⊑) ≡ λx y. Rep x ⊑ 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" then have "finite (Abs ` A)" by (rule finite_imageI) then show "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: "(⊑) ≡ λx y. Rep x ⊑ 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: "(⊑) ≡ λx y. Rep x ⊑ 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: "(⊑) ≡ λx y. Rep x ⊑ Rep y" shows "range (λi. Rep (S i)) <<| Rep x ⟹ range S <<| x" by (simp add: is_lub_def is_ub_def below) lemma Abs_inverse_lub_Rep: fixes Abs :: "'a::cpo ⇒ 'b::po" assumes type: "type_definition Rep Abs A" and below: "(⊑) ≡ λx y. Rep x ⊑ Rep y" and adm: "adm (λx. x ∈ A)" shows "chain S ⟹ Rep (Abs (⨆i. Rep (S i))) = (⨆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: "(⊑) ≡ λx y. Rep x ⊑ Rep y" and adm: "adm (λx. x ∈ A)" assumes S: "chain S" shows "range S <<| Abs (⨆i. Rep (S i))" proof - from S have "chain (λi. Rep (S i))" by (rule ch2ch_Rep [OF below]) then have "range (λi. Rep (S i)) <<| (⨆i. Rep (S i))" by (rule cpo_lubI) then have "range (λi. Rep (S i)) <<| Rep (Abs (⨆i. Rep (S i)))" by (simp only: Abs_inverse_lub_Rep [OF type below adm S]) then show "range S <<| Abs (⨆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: "(⊑) ≡ λx y. Rep x ⊑ Rep y" and adm: "adm (λx. x ∈ A)" shows "OFCLASS('b, cpo_class)" proof fix S :: "nat ⇒ 'b" assume "chain S" then have "range S <<| Abs (⨆i. Rep (S i))" by (rule typedef_is_lub [OF type below adm]) then show "∃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: "(⊑) ≡ λx y. Rep x ⊑ 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: "(⊑) ≡ λx y. Rep x ⊑ 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: "(⊑) ≡ λx y. Rep x ⊑ 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) then show "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: "(⊑) ≡ λx y. Rep x ⊑ Rep y" and z_in_A: "z ∈ A" and z_least: "⋀x. x ∈ A ⟹ z ⊑ 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: "(⊑) ≡ λx y. Rep x ⊑ 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: "(⊑) ≡ λx y. Rep x ⊑ 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: "(⊑) ≡ λx y. Rep x ⊑ 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: "(⊑) ≡ λx y. Rep x ⊑ 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: "(⊑) ≡ λx y. Rep x ⊑ 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: "(⊑) ≡ λx y. Rep x ⊑ 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