# HG changeset patch # User huffman # Date 1286483586 25200 # Node ID 0300d5170622dad6d92175aed352c3fc088766f2 # Parent 910d3ea1efa8b6909cc9020249049024b7c284fb add lemma typedef_ideal_completion diff -r 910d3ea1efa8 -r 0300d5170622 src/HOLCF/Algebraic.thy --- a/src/HOLCF/Algebraic.thy Thu Oct 07 13:22:13 2010 -0700 +++ b/src/HOLCF/Algebraic.thy Thu Oct 07 13:33:06 2010 -0700 @@ -99,23 +99,10 @@ using type_definition_sfp below_sfp_def by (rule below.typedef_ideal_cpo) -lemma Rep_sfp_lub: - "chain Y \ Rep_sfp (\i. Y i) = (\i. Rep_sfp (Y i))" -using type_definition_sfp below_sfp_def -by (rule below.typedef_ideal_rep_contlub) - -lemma ideal_Rep_sfp: "below.ideal (Rep_sfp xs)" -by (rule Rep_sfp [unfolded mem_Collect_eq]) - definition sfp_principal :: "fin_defl \ sfp" where "sfp_principal t = Abs_sfp {u. u \ t}" -lemma Rep_sfp_principal: - "Rep_sfp (sfp_principal t) = {u. u \ t}" -unfolding sfp_principal_def -by (simp add: Abs_sfp_inverse below.ideal_principal) - lemma fin_defl_countable: "\f::fin_defl \ nat. inj f" proof have *: "\d. finite (approx_chain.place udom_approx ` @@ -144,13 +131,9 @@ qed interpretation sfp: ideal_completion below sfp_principal Rep_sfp -apply default -apply (rule ideal_Rep_sfp) -apply (erule Rep_sfp_lub) -apply (rule Rep_sfp_principal) -apply (simp only: below_sfp_def) -apply (rule fin_defl_countable) -done +using type_definition_sfp below_sfp_def +using sfp_principal_def fin_defl_countable +by (rule below.typedef_ideal_completion) text {* Algebraic deflations are pointed *} diff -r 910d3ea1efa8 -r 0300d5170622 src/HOLCF/Completion.thy --- a/src/HOLCF/Completion.thy Thu Oct 07 13:22:13 2010 -0700 +++ b/src/HOLCF/Completion.thy Thu Oct 07 13:33:06 2010 -0700 @@ -410,4 +410,26 @@ end +lemma (in preorder) typedef_ideal_completion: + fixes Abs :: "'a set \ 'b::cpo" + assumes type: "type_definition Rep Abs {S. ideal S}" + assumes below: "\x y. x \ y \ Rep x \ Rep y" + assumes principal: "\a. principal a = Abs {b. b \ a}" + assumes countable: "\f::'a \ nat. inj f" + shows "ideal_completion r principal Rep" +proof + interpret type_definition Rep Abs "{S. ideal S}" by fact + fix a b :: 'a and x y :: 'b and Y :: "nat \ 'b" + show "ideal (Rep x)" + using Rep [of x] by simp + show "chain Y \ Rep (\i. Y i) = (\i. Rep (Y i))" + using type below by (rule typedef_ideal_rep_contlub) + show "Rep (principal a) = {b. b \ a}" + by (simp add: principal Abs_inverse ideal_principal) + show "Rep x \ Rep y \ x \ y" + by (simp only: below) + show "\f::'a \ nat. inj f" + by (rule countable) +qed + end diff -r 910d3ea1efa8 -r 0300d5170622 src/HOLCF/ConvexPD.thy --- a/src/HOLCF/ConvexPD.thy Thu Oct 07 13:22:13 2010 -0700 +++ b/src/HOLCF/ConvexPD.thy Thu Oct 07 13:33:06 2010 -0700 @@ -140,32 +140,15 @@ using type_definition_convex_pd below_convex_pd_def by (rule convex_le.typedef_ideal_cpo) -lemma Rep_convex_pd_lub: - "chain Y \ Rep_convex_pd (\i. Y i) = (\i. Rep_convex_pd (Y i))" -using type_definition_convex_pd below_convex_pd_def -by (rule convex_le.typedef_ideal_rep_contlub) - -lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_convex_pd xs)" -by (rule Rep_convex_pd [unfolded mem_Collect_eq]) - definition convex_principal :: "'a pd_basis \ 'a convex_pd" where "convex_principal t = Abs_convex_pd {u. u \\ t}" -lemma Rep_convex_principal: - "Rep_convex_pd (convex_principal t) = {u. u \\ t}" -unfolding convex_principal_def -by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal) - interpretation convex_pd: ideal_completion convex_le convex_principal Rep_convex_pd -apply unfold_locales -apply (rule ideal_Rep_convex_pd) -apply (erule Rep_convex_pd_lub) -apply (rule Rep_convex_principal) -apply (simp only: below_convex_pd_def) -apply (rule pd_basis_countable) -done +using type_definition_convex_pd below_convex_pd_def +using convex_principal_def pd_basis_countable +by (rule convex_le.typedef_ideal_completion) text {* Convex powerdomain is pointed *} diff -r 910d3ea1efa8 -r 0300d5170622 src/HOLCF/LowerPD.thy --- a/src/HOLCF/LowerPD.thy Thu Oct 07 13:22:13 2010 -0700 +++ b/src/HOLCF/LowerPD.thy Thu Oct 07 13:33:06 2010 -0700 @@ -88,39 +88,22 @@ end instance lower_pd :: (sfp) po -by (rule lower_le.typedef_ideal_po - [OF type_definition_lower_pd below_lower_pd_def]) +using type_definition_lower_pd below_lower_pd_def +by (rule lower_le.typedef_ideal_po) instance lower_pd :: (sfp) cpo -by (rule lower_le.typedef_ideal_cpo - [OF type_definition_lower_pd below_lower_pd_def]) - -lemma Rep_lower_pd_lub: - "chain Y \ Rep_lower_pd (\i. Y i) = (\i. Rep_lower_pd (Y i))" -by (rule lower_le.typedef_ideal_rep_contlub - [OF type_definition_lower_pd below_lower_pd_def]) - -lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_lower_pd xs)" -by (rule Rep_lower_pd [unfolded mem_Collect_eq]) +using type_definition_lower_pd below_lower_pd_def +by (rule lower_le.typedef_ideal_cpo) definition lower_principal :: "'a pd_basis \ 'a lower_pd" where "lower_principal t = Abs_lower_pd {u. u \\ t}" -lemma Rep_lower_principal: - "Rep_lower_pd (lower_principal t) = {u. u \\ t}" -unfolding lower_principal_def -by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal) - interpretation lower_pd: ideal_completion lower_le lower_principal Rep_lower_pd -apply unfold_locales -apply (rule ideal_Rep_lower_pd) -apply (erule Rep_lower_pd_lub) -apply (rule Rep_lower_principal) -apply (simp only: below_lower_pd_def) -apply (rule pd_basis_countable) -done +using type_definition_lower_pd below_lower_pd_def +using lower_principal_def pd_basis_countable +by (rule lower_le.typedef_ideal_completion) text {* Lower powerdomain is pointed *} diff -r 910d3ea1efa8 -r 0300d5170622 src/HOLCF/Universal.thy --- a/src/HOLCF/Universal.thy Thu Oct 07 13:22:13 2010 -0700 +++ b/src/HOLCF/Universal.thy Thu Oct 07 13:33:06 2010 -0700 @@ -218,32 +218,18 @@ using type_definition_udom below_udom_def by (rule udom.typedef_ideal_cpo) -lemma Rep_udom_lub: - "chain Y \ Rep_udom (\i. Y i) = (\i. Rep_udom (Y i))" -using type_definition_udom below_udom_def -by (rule udom.typedef_ideal_rep_contlub) - -lemma ideal_Rep_udom: "udom.ideal (Rep_udom xs)" -by (rule Rep_udom [unfolded mem_Collect_eq]) - definition udom_principal :: "nat \ udom" where "udom_principal t = Abs_udom {u. ubasis_le u t}" -lemma Rep_udom_principal: - "Rep_udom (udom_principal t) = {u. ubasis_le u t}" -unfolding udom_principal_def -by (simp add: Abs_udom_inverse udom.ideal_principal) +lemma ubasis_countable: "\f::ubasis \ nat. inj f" +by (rule exI, rule inj_on_id) interpretation udom: ideal_completion ubasis_le udom_principal Rep_udom -apply unfold_locales -apply (rule ideal_Rep_udom) -apply (erule Rep_udom_lub) -apply (rule Rep_udom_principal) -apply (simp only: below_udom_def) -apply (rule exI, rule inj_on_id) -done +using type_definition_udom below_udom_def +using udom_principal_def ubasis_countable +by (rule udom.typedef_ideal_completion) text {* Universal domain is pointed *} diff -r 910d3ea1efa8 -r 0300d5170622 src/HOLCF/UpperPD.thy --- a/src/HOLCF/UpperPD.thy Thu Oct 07 13:22:13 2010 -0700 +++ b/src/HOLCF/UpperPD.thy Thu Oct 07 13:33:06 2010 -0700 @@ -93,32 +93,15 @@ using type_definition_upper_pd below_upper_pd_def by (rule upper_le.typedef_ideal_cpo) -lemma Rep_upper_pd_lub: - "chain Y \ Rep_upper_pd (\i. Y i) = (\i. Rep_upper_pd (Y i))" -using type_definition_upper_pd below_upper_pd_def -by (rule upper_le.typedef_ideal_rep_contlub) - -lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_upper_pd xs)" -by (rule Rep_upper_pd [unfolded mem_Collect_eq]) - definition upper_principal :: "'a pd_basis \ 'a upper_pd" where "upper_principal t = Abs_upper_pd {u. u \\ t}" -lemma Rep_upper_principal: - "Rep_upper_pd (upper_principal t) = {u. u \\ t}" -unfolding upper_principal_def -by (simp add: Abs_upper_pd_inverse upper_le.ideal_principal) - interpretation upper_pd: ideal_completion upper_le upper_principal Rep_upper_pd -apply unfold_locales -apply (rule ideal_Rep_upper_pd) -apply (erule Rep_upper_pd_lub) -apply (rule Rep_upper_principal) -apply (simp only: below_upper_pd_def) -apply (rule pd_basis_countable) -done +using type_definition_upper_pd below_upper_pd_def +using upper_principal_def pd_basis_countable +by (rule upper_le.typedef_ideal_completion) text {* Upper powerdomain is pointed *}