# HG changeset patch # User huffman # Date 1289349433 28800 # Node ID 6de5839e2fb3bfc9a50865db367b9faf0b047b37 # Parent 05be0c37db1d72b8baf667f484cd945c06710caf add 'predomain' class: unpointed version of bifinite diff -r 05be0c37db1d -r 6de5839e2fb3 src/HOLCF/Bifinite.thy --- a/src/HOLCF/Bifinite.thy Tue Nov 09 08:41:36 2010 -0800 +++ b/src/HOLCF/Bifinite.thy Tue Nov 09 16:37:13 2010 -0800 @@ -13,9 +13,21 @@ text {* We define a bifinite domain as a pcpo that is isomorphic to some algebraic deflation over the universal domain. + + A predomain is a cpo that, when lifted, becomes bifinite. *} -class bifinite = pcpo + +class predomain = cpo + + fixes liftdefl :: "('a::cpo) itself \ defl" + fixes liftemb :: "'a\<^sub>\ \ udom" + fixes liftprj :: "udom \ 'a\<^sub>\" + assumes predomain_ep: "ep_pair liftemb liftprj" + assumes cast_liftdefl: "cast\(liftdefl TYPE('a::cpo)) = liftemb oo liftprj" + +syntax "_LIFTDEFL" :: "type \ logic" ("(1LIFTDEFL/(1'(_')))") +translations "LIFTDEFL('t)" \ "CONST liftdefl TYPE('t)" + +class bifinite = predomain + pcpo + fixes emb :: "'a::pcpo \ udom" fixes prj :: "udom \ 'a::pcpo" fixes defl :: "'a itself \ defl" @@ -243,6 +255,48 @@ using ssum_approx finite_deflation_ssum_map unfolding ssum_defl_def by (rule cast_defl_fun2) +subsection {* Lemma for proving bifinite instances *} + +text {* Temporarily relax type constraints. *} + +setup {* + fold Sign.add_const_constraint + [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \ defl"}) + , (@{const_name emb}, SOME @{typ "'a::pcpo \ udom"}) + , (@{const_name prj}, SOME @{typ "udom \ 'a::pcpo"}) + , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \ defl"}) + , (@{const_name liftemb}, SOME @{typ "'a::pcpo u \ udom"}) + , (@{const_name liftprj}, SOME @{typ "udom \ 'a::pcpo u"}) ] +*} + +lemma bifinite_class_intro: + assumes liftemb: "(liftemb :: 'a u \ udom) = udom_emb u_approx oo u_map\emb" + assumes liftprj: "(liftprj :: udom \ 'a u) = u_map\prj oo udom_prj u_approx" + assumes liftdefl: "liftdefl TYPE('a) = u_defl\DEFL('a)" + assumes ep_pair: "ep_pair emb (prj :: udom \ 'a)" + assumes cast_defl: "cast\DEFL('a) = emb oo (prj :: udom \ 'a)" + shows "OFCLASS('a, bifinite_class)" +proof + show "ep_pair liftemb (liftprj :: udom \ 'a u)" + unfolding liftemb liftprj + by (intro ep_pair_comp ep_pair_u_map ep_pair ep_pair_udom u_approx) + show "cast\LIFTDEFL('a) = liftemb oo (liftprj :: udom \ 'a u)" + unfolding liftemb liftprj liftdefl + by (simp add: cfcomp1 cast_u_defl cast_defl u_map_map) +qed fact+ + +text {* Restore original type constraints. *} + +setup {* + fold Sign.add_const_constraint + [ (@{const_name defl}, SOME @{typ "'a::bifinite itself \ defl"}) + , (@{const_name emb}, SOME @{typ "'a::bifinite \ udom"}) + , (@{const_name prj}, SOME @{typ "udom \ 'a::bifinite"}) + , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \ defl"}) + , (@{const_name liftemb}, SOME @{typ "'a::predomain u \ udom"}) + , (@{const_name liftprj}, SOME @{typ "udom \ 'a::predomain u"}) ] +*} + subsection {* The universal domain is bifinite *} instantiation udom :: bifinite @@ -257,7 +311,18 @@ definition "defl (t::udom itself) = (\i. defl_principal (Abs_fin_defl (udom_approx i)))" -instance proof +definition + "(liftemb :: udom u \ udom) = udom_emb u_approx oo u_map\emb" + +definition + "(liftprj :: udom \ udom u) = u_map\prj oo udom_prj u_approx" + +definition + "liftdefl (t::udom itself) = u_defl\DEFL(udom)" + +instance +using liftemb_udom_def liftprj_udom_def liftdefl_udom_def +proof (rule bifinite_class_intro) show "ep_pair emb (prj :: udom \ udom)" by (simp add: ep_pair.intro) show "cast\DEFL(udom) = emb oo (prj :: udom \ udom)" @@ -276,6 +341,48 @@ end +subsection {* Lifted predomains are bifinite *} + +instantiation u :: (predomain) bifinite +begin + +definition + "emb = liftemb" + +definition + "prj = liftprj" + +definition + "defl (t::'a u itself) = LIFTDEFL('a)" + +definition + "(liftemb :: 'a u u \ udom) = udom_emb u_approx oo u_map\emb" + +definition + "(liftprj :: udom \ 'a u u) = u_map\prj oo udom_prj u_approx" + +definition + "liftdefl (t::'a u itself) = u_defl\DEFL('a u)" + +instance +using liftemb_u_def liftprj_u_def liftdefl_u_def +proof (rule bifinite_class_intro) + show "ep_pair emb (prj :: udom \ 'a u)" + unfolding emb_u_def prj_u_def + by (rule predomain_ep) + show "cast\DEFL('a u) = emb oo (prj :: udom \ 'a u)" + unfolding emb_u_def prj_u_def defl_u_def + by (rule cast_liftdefl) +qed + +end + +lemma DEFL_u: "DEFL('a::predomain u) = LIFTDEFL('a)" +by (rule defl_u_def) + +lemma LIFTDEFL_u: "LIFTDEFL('a::predomain u) = u_defl\DEFL('a u)" +by (rule liftdefl_u_def) + subsection {* Continuous function space is a bifinite domain *} instantiation cfun :: (bifinite, bifinite) bifinite @@ -290,12 +397,22 @@ definition "defl (t::('a \ 'b) itself) = cfun_defl\DEFL('a)\DEFL('b)" -instance proof +definition + "(liftemb :: ('a \ 'b) u \ udom) = udom_emb u_approx oo u_map\emb" + +definition + "(liftprj :: udom \ ('a \ 'b) u) = u_map\prj oo udom_prj u_approx" + +definition + "liftdefl (t::('a \ 'b) itself) = u_defl\DEFL('a \ 'b)" + +instance +using liftemb_cfun_def liftprj_cfun_def liftdefl_cfun_def +proof (rule bifinite_class_intro) show "ep_pair emb (prj :: udom \ 'a \ 'b)" unfolding emb_cfun_def prj_cfun_def using ep_pair_udom [OF cfun_approx] by (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj) -next show "cast\DEFL('a \ 'b) = emb oo (prj :: udom \ 'a \ 'b)" unfolding emb_cfun_def prj_cfun_def defl_cfun_def cast_cfun_defl by (simp add: cast_DEFL oo_def cfun_eq_iff cfun_map_map) @@ -307,6 +424,10 @@ "DEFL('a::bifinite \ 'b::bifinite) = cfun_defl\DEFL('a)\DEFL('b)" by (rule defl_cfun_def) +lemma LIFTDEFL_cfun: + "LIFTDEFL('a::bifinite \ 'b::bifinite) = u_defl\DEFL('a \ 'b)" +by (rule liftdefl_cfun_def) + subsection {* Cartesian product is a bifinite domain *} instantiation prod :: (bifinite, bifinite) bifinite @@ -321,7 +442,18 @@ definition "defl (t::('a \ 'b) itself) = prod_defl\DEFL('a)\DEFL('b)" -instance proof +definition + "(liftemb :: ('a \ 'b) u \ udom) = udom_emb u_approx oo u_map\emb" + +definition + "(liftprj :: udom \ ('a \ 'b) u) = u_map\prj oo udom_prj u_approx" + +definition + "liftdefl (t::('a \ 'b) itself) = u_defl\DEFL('a \ 'b)" + +instance +using liftemb_prod_def liftprj_prod_def liftdefl_prod_def +proof (rule bifinite_class_intro) show "ep_pair emb (prj :: udom \ 'a \ 'b)" unfolding emb_prod_def prj_prod_def using ep_pair_udom [OF prod_approx] @@ -338,6 +470,10 @@ "DEFL('a::bifinite \ 'b::bifinite) = prod_defl\DEFL('a)\DEFL('b)" by (rule defl_prod_def) +lemma LIFTDEFL_prod: + "LIFTDEFL('a::bifinite \ 'b::bifinite) = u_defl\DEFL('a \ 'b)" +by (rule liftdefl_prod_def) + subsection {* Strict product is a bifinite domain *} instantiation sprod :: (bifinite, bifinite) bifinite @@ -352,7 +488,18 @@ definition "defl (t::('a \ 'b) itself) = sprod_defl\DEFL('a)\DEFL('b)" -instance proof +definition + "(liftemb :: ('a \ 'b) u \ udom) = udom_emb u_approx oo u_map\emb" + +definition + "(liftprj :: udom \ ('a \ 'b) u) = u_map\prj oo udom_prj u_approx" + +definition + "liftdefl (t::('a \ 'b) itself) = u_defl\DEFL('a \ 'b)" + +instance +using liftemb_sprod_def liftprj_sprod_def liftdefl_sprod_def +proof (rule bifinite_class_intro) show "ep_pair emb (prj :: udom \ 'a \ 'b)" unfolding emb_sprod_def prj_sprod_def using ep_pair_udom [OF sprod_approx] @@ -369,51 +516,23 @@ "DEFL('a::bifinite \ 'b::bifinite) = sprod_defl\DEFL('a)\DEFL('b)" by (rule defl_sprod_def) -subsection {* Lifted cpo is a bifinite domain *} - -instantiation u :: (bifinite) bifinite -begin +lemma LIFTDEFL_sprod: + "LIFTDEFL('a::bifinite \ 'b::bifinite) = u_defl\DEFL('a \ 'b)" +by (rule liftdefl_sprod_def) -definition - "emb = udom_emb u_approx oo u_map\emb" - -definition - "prj = u_map\prj oo udom_prj u_approx" - -definition - "defl (t::'a u itself) = u_defl\DEFL('a)" +subsection {* Countable discrete cpos are predomains *} -instance proof - show "ep_pair emb (prj :: udom \ 'a u)" - unfolding emb_u_def prj_u_def - using ep_pair_udom [OF u_approx] - by (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj) -next - show "cast\DEFL('a u) = emb oo (prj :: udom \ 'a u)" - unfolding emb_u_def prj_u_def defl_u_def cast_u_defl - by (simp add: cast_DEFL oo_def cfun_eq_iff u_map_map) -qed - -end +definition discr_approx :: "nat \ 'a::countable discr u \ 'a discr u" + where "discr_approx = (\i. \(up\x). if to_nat (undiscr x) < i then up\x else \)" -lemma DEFL_u: "DEFL('a::bifinite u) = u_defl\DEFL('a)" -by (rule defl_u_def) - -subsection {* Lifted countable types are bifinite domains *} +lemma chain_discr_approx [simp]: "chain discr_approx" +unfolding discr_approx_def +by (rule chainI, simp add: monofun_cfun monofun_LAM) -definition - lift_approx :: "nat \ 'a::countable lift \ 'a lift" -where - "lift_approx = (\i. FLIFT x. if to_nat x < i then Def x else \)" - -lemma chain_lift_approx [simp]: "chain lift_approx" - unfolding lift_approx_def - by (rule chainI, simp add: FLIFT_mono) - -lemma lub_lift_approx [simp]: "(\i. lift_approx i) = ID" +lemma lub_discr_approx [simp]: "(\i. discr_approx i) = ID" apply (rule cfun_eqI) apply (simp add: contlub_cfun_fun) -apply (simp add: lift_approx_def) +apply (simp add: discr_approx_def) apply (case_tac x, simp) apply (rule thelubI) apply (rule is_lubI) @@ -424,61 +543,67 @@ apply (rule lessI) done -lemma finite_deflation_lift_approx: "finite_deflation (lift_approx i)" +lemma inj_on_undiscr [simp]: "inj_on undiscr A" +using Discr_undiscr by (rule inj_on_inverseI) + +lemma finite_deflation_discr_approx: "finite_deflation (discr_approx i)" proof - fix x :: "'a lift" - show "lift_approx i\x \ x" - unfolding lift_approx_def + fix x :: "'a discr u" + show "discr_approx i\x \ x" + unfolding discr_approx_def by (cases x, simp, simp) - show "lift_approx i\(lift_approx i\x) = lift_approx i\x" - unfolding lift_approx_def + show "discr_approx i\(discr_approx i\x) = discr_approx i\x" + unfolding discr_approx_def by (cases x, simp, simp) - show "finite {x::'a lift. lift_approx i\x = x}" + show "finite {x::'a discr u. discr_approx i\x = x}" proof (rule finite_subset) - let ?S = "insert (\::'a lift) (Def ` to_nat -` {..x = x} \ ?S" - unfolding lift_approx_def + let ?S = "insert (\::'a discr u) ((\x. up\x) ` undiscr -` to_nat -` {..x = x} \ ?S" + unfolding discr_approx_def by (rule subsetI, case_tac x, simp, simp split: split_if_asm) show "finite ?S" by (simp add: finite_vimageI) qed qed -lemma lift_approx: "approx_chain lift_approx" -using chain_lift_approx lub_lift_approx finite_deflation_lift_approx +lemma discr_approx: "approx_chain discr_approx" +using chain_discr_approx lub_discr_approx finite_deflation_discr_approx by (rule approx_chain.intro) -instantiation lift :: (countable) bifinite +instantiation discr :: (countable) predomain begin definition - "emb = udom_emb lift_approx" + "liftemb = udom_emb discr_approx" definition - "prj = udom_prj lift_approx" + "liftprj = udom_prj discr_approx" definition - "defl (t::'a lift itself) = - (\i. defl_principal (Abs_fin_defl (emb oo lift_approx i oo prj)))" + "liftdefl (t::'a discr itself) = + (\i. defl_principal (Abs_fin_defl (liftemb oo discr_approx i oo liftprj)))" instance proof - show ep: "ep_pair emb (prj :: udom \ 'a lift)" - unfolding emb_lift_def prj_lift_def - by (rule ep_pair_udom [OF lift_approx]) - show "cast\DEFL('a lift) = emb oo (prj :: udom \ 'a lift)" - unfolding defl_lift_def + show "ep_pair liftemb (liftprj :: udom \ 'a discr u)" + unfolding liftemb_discr_def liftprj_discr_def + by (rule ep_pair_udom [OF discr_approx]) + show "cast\LIFTDEFL('a discr) = liftemb oo (liftprj :: udom \ 'a discr u)" + unfolding liftemb_discr_def liftprj_discr_def liftdefl_discr_def apply (subst contlub_cfun_arg) apply (rule chainI) apply (rule defl.principal_mono) apply (simp add: below_fin_defl_def) - apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx - ep_pair.finite_deflation_e_d_p [OF ep]) + apply (simp add: Abs_fin_defl_inverse + ep_pair.finite_deflation_e_d_p [OF ep_pair_udom [OF discr_approx]] + approx_chain.finite_deflation_approx [OF discr_approx]) apply (intro monofun_cfun below_refl) apply (rule chainE) - apply (rule chain_lift_approx) + apply (rule chain_discr_approx) apply (subst cast_defl_principal) - apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx - ep_pair.finite_deflation_e_d_p [OF ep] lub_distribs) + apply (simp add: Abs_fin_defl_inverse + ep_pair.finite_deflation_e_d_p [OF ep_pair_udom [OF discr_approx]] + approx_chain.finite_deflation_approx [OF discr_approx]) + apply (simp add: lub_distribs) done qed @@ -498,12 +623,22 @@ definition "defl (t::('a \ 'b) itself) = ssum_defl\DEFL('a)\DEFL('b)" -instance proof +definition + "(liftemb :: ('a \ 'b) u \ udom) = udom_emb u_approx oo u_map\emb" + +definition + "(liftprj :: udom \ ('a \ 'b) u) = u_map\prj oo udom_prj u_approx" + +definition + "liftdefl (t::('a \ 'b) itself) = u_defl\DEFL('a \ 'b)" + +instance +using liftemb_ssum_def liftprj_ssum_def liftdefl_ssum_def +proof (rule bifinite_class_intro) show "ep_pair emb (prj :: udom \ 'a \ 'b)" unfolding emb_ssum_def prj_ssum_def using ep_pair_udom [OF ssum_approx] by (intro ep_pair_comp ep_pair_ssum_map ep_pair_emb_prj) -next show "cast\DEFL('a \ 'b) = emb oo (prj :: udom \ 'a \ 'b)" unfolding emb_ssum_def prj_ssum_def defl_ssum_def cast_ssum_defl by (simp add: cast_DEFL oo_def cfun_eq_iff ssum_map_map) @@ -515,4 +650,47 @@ "DEFL('a::bifinite \ 'b::bifinite) = ssum_defl\DEFL('a)\DEFL('b)" by (rule defl_ssum_def) +lemma LIFTDEFL_ssum: + "LIFTDEFL('a::bifinite \ 'b::bifinite) = u_defl\DEFL('a \ 'b)" +by (rule liftdefl_ssum_def) + +subsection {* Lifted countable types are bifinite domains *} + +instantiation lift :: (countable) bifinite +begin + +definition + "emb = emb oo (\ x. Rep_lift x)" + +definition + "prj = (\ y. Abs_lift y) oo prj" + +definition + "defl (t::'a lift itself) = DEFL('a discr u)" + +definition + "(liftemb :: 'a lift u \ udom) = udom_emb u_approx oo u_map\emb" + +definition + "(liftprj :: udom \ 'a lift u) = u_map\prj oo udom_prj u_approx" + +definition + "liftdefl (t::'a lift itself) = u_defl\DEFL('a lift)" + +instance +using liftemb_lift_def liftprj_lift_def liftdefl_lift_def +proof (rule bifinite_class_intro) + note [simp] = cont_Rep_lift cont_Abs_lift Rep_lift_inverse Abs_lift_inverse + have "ep_pair (\(x::'a lift). Rep_lift x) (\ y. Abs_lift y)" + by (simp add: ep_pair_def) + thus "ep_pair emb (prj :: udom \ 'a lift)" + unfolding emb_lift_def prj_lift_def + using ep_pair_emb_prj by (rule ep_pair_comp) + show "cast\DEFL('a lift) = emb oo (prj :: udom \ 'a lift)" + unfolding emb_lift_def prj_lift_def defl_lift_def cast_DEFL + by (simp add: cfcomp1) +qed + end + +end diff -r 05be0c37db1d -r 6de5839e2fb3 src/HOLCF/ConvexPD.thy --- a/src/HOLCF/ConvexPD.thy Tue Nov 09 08:41:36 2010 -0800 +++ b/src/HOLCF/ConvexPD.thy Tue Nov 09 16:37:13 2010 -0800 @@ -472,7 +472,18 @@ definition "defl (t::'a convex_pd itself) = convex_defl\DEFL('a)" -instance proof +definition + "(liftemb :: 'a convex_pd u \ udom) = udom_emb u_approx oo u_map\emb" + +definition + "(liftprj :: udom \ 'a convex_pd u) = u_map\prj oo udom_prj u_approx" + +definition + "liftdefl (t::'a convex_pd itself) = u_defl\DEFL('a convex_pd)" + +instance +using liftemb_convex_pd_def liftprj_convex_pd_def liftdefl_convex_pd_def +proof (rule bifinite_class_intro) show "ep_pair emb (prj :: udom \ 'a convex_pd)" unfolding emb_convex_pd_def prj_convex_pd_def using ep_pair_udom [OF convex_approx] diff -r 05be0c37db1d -r 6de5839e2fb3 src/HOLCF/Library/Defl_Bifinite.thy --- a/src/HOLCF/Library/Defl_Bifinite.thy Tue Nov 09 08:41:36 2010 -0800 +++ b/src/HOLCF/Library/Defl_Bifinite.thy Tue Nov 09 16:37:13 2010 -0800 @@ -622,7 +622,18 @@ "defl (t::defl itself) = (\i. defl_principal (Abs_fin_defl (emb oo defl_approx i oo prj)))" -instance proof +definition + "(liftemb :: defl u \ udom) = udom_emb u_approx oo u_map\emb" + +definition + "(liftprj :: udom \ defl u) = u_map\prj oo udom_prj u_approx" + +definition + "liftdefl (t::defl itself) = u_defl\DEFL(defl)" + +instance +using liftemb_defl_def liftprj_defl_def liftdefl_defl_def +proof (rule bifinite_class_intro) show ep: "ep_pair emb (prj :: udom \ defl)" unfolding emb_defl_def prj_defl_def by (rule ep_pair_udom [OF defl_approx]) diff -r 05be0c37db1d -r 6de5839e2fb3 src/HOLCF/Library/Strict_Fun.thy --- a/src/HOLCF/Library/Strict_Fun.thy Tue Nov 09 08:41:36 2010 -0800 +++ b/src/HOLCF/Library/Strict_Fun.thy Tue Nov 09 16:37:13 2010 -0800 @@ -185,7 +185,18 @@ definition "defl (t::('a \! 'b) itself) = sfun_defl\DEFL('a)\DEFL('b)" -instance proof +definition + "(liftemb :: ('a \! 'b) u \ udom) = udom_emb u_approx oo u_map\emb" + +definition + "(liftprj :: udom \ ('a \! 'b) u) = u_map\prj oo udom_prj u_approx" + +definition + "liftdefl (t::('a \! 'b) itself) = u_defl\DEFL('a \! 'b)" + +instance +using liftemb_sfun_def liftprj_sfun_def liftdefl_sfun_def +proof (rule bifinite_class_intro) show "ep_pair emb (prj :: udom \ 'a \! 'b)" unfolding emb_sfun_def prj_sfun_def using ep_pair_udom [OF sfun_approx] diff -r 05be0c37db1d -r 6de5839e2fb3 src/HOLCF/LowerPD.thy --- a/src/HOLCF/LowerPD.thy Tue Nov 09 08:41:36 2010 -0800 +++ b/src/HOLCF/LowerPD.thy Tue Nov 09 16:37:13 2010 -0800 @@ -465,7 +465,18 @@ definition "defl (t::'a lower_pd itself) = lower_defl\DEFL('a)" -instance proof +definition + "(liftemb :: 'a lower_pd u \ udom) = udom_emb u_approx oo u_map\emb" + +definition + "(liftprj :: udom \ 'a lower_pd u) = u_map\prj oo udom_prj u_approx" + +definition + "liftdefl (t::'a lower_pd itself) = u_defl\DEFL('a lower_pd)" + +instance +using liftemb_lower_pd_def liftprj_lower_pd_def liftdefl_lower_pd_def +proof (rule bifinite_class_intro) show "ep_pair emb (prj :: udom \ 'a lower_pd)" unfolding emb_lower_pd_def prj_lower_pd_def using ep_pair_udom [OF lower_approx] diff -r 05be0c37db1d -r 6de5839e2fb3 src/HOLCF/Representable.thy --- a/src/HOLCF/Representable.thy Tue Nov 09 08:41:36 2010 -0800 +++ b/src/HOLCF/Representable.thy Tue Nov 09 16:37:13 2010 -0800 @@ -80,15 +80,16 @@ subsection {* Proving a subtype is representable *} -text {* - Temporarily relax type constraints for @{term emb} and @{term prj}. -*} +text {* Temporarily relax type constraints. *} setup {* fold Sign.add_const_constraint [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \ defl"}) , (@{const_name emb}, SOME @{typ "'a::pcpo \ udom"}) - , (@{const_name prj}, SOME @{typ "udom \ 'a::pcpo"}) ] + , (@{const_name prj}, SOME @{typ "udom \ 'a::pcpo"}) + , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \ defl"}) + , (@{const_name liftemb}, SOME @{typ "'a::pcpo u \ udom"}) + , (@{const_name liftprj}, SOME @{typ "udom \ 'a::pcpo u"}) ] *} lemma typedef_rep_class: @@ -100,8 +101,13 @@ assumes emb: "emb \ (\ x. Rep x)" assumes prj: "prj \ (\ x. Abs (cast\t\x))" assumes defl: "defl \ (\ a::'a itself. t)" + assumes liftemb: "(liftemb :: 'a u \ udom) \ udom_emb u_approx oo u_map\emb" + assumes liftprj: "(liftprj :: udom \ 'a u) \ u_map\prj oo udom_prj u_approx" + assumes liftdefl: "(liftdefl :: 'a itself \ defl) \ (\t. u_defl\DEFL('a))" shows "OFCLASS('a, bifinite_class)" -proof +using liftemb [THEN meta_eq_to_obj_eq] +using liftprj [THEN meta_eq_to_obj_eq] +proof (rule bifinite_class_intro) have emb_beta: "\x. emb\x = Rep x" unfolding emb apply (rule beta_cfun) @@ -127,6 +133,8 @@ done show "cast\DEFL('a) = emb oo (prj :: udom \ 'a)" by (rule cfun_eqI, simp add: defl emb_prj) + show "LIFTDEFL('a) = u_defl\DEFL('a)" + unfolding liftdefl .. qed lemma typedef_DEFL: @@ -134,13 +142,21 @@ shows "DEFL('a::pcpo) = t" unfolding assms .. +lemma typedef_LIFTDEFL: + assumes "liftdefl \ (\a::'a::pcpo itself. u_defl\DEFL('a))" + shows "LIFTDEFL('a::pcpo) = u_defl\DEFL('a)" +unfolding assms .. + text {* Restore original typing constraints. *} setup {* fold Sign.add_const_constraint [ (@{const_name defl}, SOME @{typ "'a::bifinite itself \ defl"}) , (@{const_name emb}, SOME @{typ "'a::bifinite \ udom"}) - , (@{const_name prj}, SOME @{typ "udom \ 'a::bifinite"}) ] + , (@{const_name prj}, SOME @{typ "udom \ 'a::bifinite"}) + , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \ defl"}) + , (@{const_name liftemb}, SOME @{typ "'a::predomain u \ udom"}) + , (@{const_name liftprj}, SOME @{typ "udom \ 'a::predomain u"}) ] *} use "Tools/repdef.ML" @@ -177,6 +193,11 @@ lemma isodefl_ID_DEFL: "isodefl (ID :: 'a \ 'a) DEFL('a)" unfolding isodefl_def by (simp add: cast_DEFL) +lemma isodefl_LIFTDEFL: + "isodefl (u_map\(ID :: 'a \ 'a)) LIFTDEFL('a::predomain)" +unfolding u_map_ID DEFL_u [symmetric] +by (rule isodefl_ID_DEFL) + lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \ 'a) DEFL('a) \ d = ID" unfolding isodefl_def apply (simp add: cast_DEFL) @@ -256,13 +277,45 @@ done lemma isodefl_u: - "isodefl d t \ isodefl (u_map\d) (u_defl\t)" + assumes "(liftemb :: 'a u \ udom) = udom_emb u_approx oo u_map\emb" + assumes "(liftprj :: udom \ 'a u) = u_map\prj oo udom_prj u_approx" + shows "isodefl (d :: 'a \ 'a) t \ isodefl (u_map\d) (u_defl\t)" apply (rule isodeflI) apply (simp add: cast_u_defl cast_isodefl) -apply (simp add: emb_u_def prj_u_def) +apply (simp add: emb_u_def prj_u_def assms) apply (simp add: u_map_map) done +lemma isodefl_u_u: + assumes "isodefl (u_map\d) (u_defl\t)" + shows "isodefl (u_map\(u_map\d)) (u_defl\(u_defl\t))" +using liftemb_u_def liftprj_u_def assms +by (rule isodefl_u) + +lemma isodefl_cfun_u: + assumes "isodefl d1 t1" and "isodefl d2 t2" + shows "isodefl (u_map\(cfun_map\d1\d2)) (u_defl\(cfun_defl\t1\t2))" +using liftemb_cfun_def liftprj_cfun_def isodefl_cfun [OF assms] +by (rule isodefl_u) + +lemma isodefl_cprod_u: + assumes "isodefl d1 t1" and "isodefl d2 t2" + shows "isodefl (u_map\(cprod_map\d1\d2)) (u_defl\(prod_defl\t1\t2))" +using liftemb_prod_def liftprj_prod_def isodefl_cprod [OF assms] +by (rule isodefl_u) + +lemma isodefl_sprod_u: + assumes "isodefl d1 t1" and "isodefl d2 t2" + shows "isodefl (u_map\(sprod_map\d1\d2)) (u_defl\(sprod_defl\t1\t2))" +using liftemb_sprod_def liftprj_sprod_def isodefl_sprod [OF assms] +by (rule isodefl_u) + +lemma isodefl_ssum_u: + assumes "isodefl d1 t1" and "isodefl d2 t2" + shows "isodefl (u_map\(ssum_map\d1\d2)) (u_defl\(ssum_defl\t1\t2))" +using liftemb_ssum_def liftprj_ssum_def isodefl_ssum [OF assms] +by (rule isodefl_u) + subsection {* Constructing Domain Isomorphisms *} use "Tools/Domain/domain_isomorphism.ML" @@ -271,12 +324,14 @@ lemmas [domain_defl_simps] = DEFL_cfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u + LIFTDEFL_cfun LIFTDEFL_ssum LIFTDEFL_sprod LIFTDEFL_prod LIFTDEFL_u lemmas [domain_map_ID] = cfun_map_ID ssum_map_ID sprod_map_ID cprod_map_ID u_map_ID lemmas [domain_isodefl] = - isodefl_cfun isodefl_ssum isodefl_sprod isodefl_cprod isodefl_u + isodefl_cfun isodefl_ssum isodefl_sprod isodefl_cprod isodefl_u_u + isodefl_cfun_u isodefl_ssum_u isodefl_sprod_u isodefl_cprod_u lemmas [domain_deflation] = deflation_cfun_map deflation_ssum_map deflation_sprod_map diff -r 05be0c37db1d -r 6de5839e2fb3 src/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Nov 09 08:41:36 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Nov 09 16:37:13 2010 -0800 @@ -43,7 +43,6 @@ val beta_tac = simp_tac beta_ss; fun is_cpo thy T = Sign.of_sort thy (T, @{sort cpo}); -fun is_bifinite thy T = Sign.of_sort thy (T, @{sort bifinite}); (******************************************************************************) (******************************** theory data *********************************) @@ -82,6 +81,23 @@ fun dest_DEFL (Const (@{const_name defl}, _) $ t) = Logic.dest_type t | dest_DEFL t = raise TERM ("dest_DEFL", [t]); +fun mk_LIFTDEFL T = + Const (@{const_name liftdefl}, Term.itselfT T --> deflT) $ Logic.mk_type T; + +fun dest_LIFTDEFL (Const (@{const_name liftdefl}, _) $ t) = Logic.dest_type t + | dest_LIFTDEFL t = raise TERM ("dest_LIFTDEFL", [t]); + +fun mk_u_defl t = mk_capply (@{const "u_defl"}, t); + +fun mk_u_map t = + let + val (T, U) = dest_cfunT (fastype_of t); + val u_map_type = (T ->> U) ->> (mk_upT T ->> mk_upT U); + val u_map_const = Const (@{const_name u_map}, u_map_type); + in + mk_capply (u_map_const, t) + end; + fun emb_const T = Const (@{const_name emb}, T ->> udomT); fun prj_const T = Const (@{const_name prj}, udomT ->> T); fun coerce_const (T, U) = mk_cfcomp (prj_const U, emb_const T); @@ -114,6 +130,10 @@ (*************** fixed-point definitions and unfolding theorems ***************) (******************************************************************************) +fun mk_projs [] t = [] + | mk_projs (x::[]) t = [(x, t)] + | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t); + fun add_fixdefs (spec : (binding * term) list) (thy : theory) : (thm list * thm list) * theory = @@ -124,9 +144,6 @@ val fixpoint = mk_fix (mk_cabs functional); (* project components of fixpoint *) - fun mk_projs [] t = [] - | mk_projs (x::[]) t = [(x, t)] - | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t); val projs = mk_projs lhss fixpoint; (* convert parameters to lambda abstractions *) @@ -185,24 +202,25 @@ (****************** deflation combinators and map functions *******************) (******************************************************************************) -fun mk_defl_type (flags : bool list) (Ts : typ list) = - map (Term.itselfT o snd) (filter_out fst (flags ~~ Ts)) ---> - map (K deflT) (filter I flags) -->> deflT; - fun defl_of_typ (thy : theory) - (tab : (typ * term) list) + (tab1 : (typ * term) list) + (tab2 : (typ * term) list) (T : typ) : term = let val defl_simps = RepData.get (ProofContext.init_global thy); val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) defl_simps; - val rules' = map (apfst mk_DEFL) tab; - fun defl_proc t = + val rules' = map (apfst mk_DEFL) tab1 @ map (apfst mk_LIFTDEFL) tab2; + fun proc1 t = (case dest_DEFL t of - TFree (a, _) => SOME (Free (Library.unprefix "'" a, deflT)) + TFree (a, _) => SOME (Free ("d" ^ Library.unprefix "'" a, deflT)) + | _ => NONE) handle TERM _ => NONE; + fun proc2 t = + (case dest_LIFTDEFL t of + TFree (a, _) => SOME (Free ("p" ^ Library.unprefix "'" a, deflT)) | _ => NONE) handle TERM _ => NONE; in - Pattern.rewrite_term thy (rules @ rules') [defl_proc] (mk_DEFL T) + Pattern.rewrite_term thy (rules @ rules') [proc1, proc2] (mk_DEFL T) end; (******************************************************************************) @@ -445,39 +463,54 @@ val morphs = map (fn (_, _, _, _, morphs) => morphs) doms; (* determine deflation combinator arguments *) - fun defl_flags (vs, tbind, mx, rhs, morphs) = - let fun argT v = TFree (v, the_sort v); - in map (is_bifinite thy o argT) vs end; - val defl_flagss = map defl_flags doms; + val lhsTs : typ list = map fst dom_eqns; + val defl_rec = Free ("t", mk_tupleT (map (K deflT) lhsTs)); + val defl_recs = mk_projs lhsTs defl_rec; + val defl_recs' = map (apsnd mk_u_defl) defl_recs; + fun defl_body (_, _, _, rhsT, _) = + defl_of_typ tmp_thy defl_recs defl_recs' rhsT; + val functional = Term.lambda defl_rec (mk_tuple (map defl_body doms)); + + val tfrees = map fst (Term.add_tfrees functional []); + val frees = map fst (Term.add_frees functional []); + fun get_defl_flags (vs, _, _, _, _) = + let + fun argT v = TFree (v, the_sort v); + fun mk_d v = "d" ^ Library.unprefix "'" v; + fun mk_p v = "p" ^ Library.unprefix "'" v; + val args = maps (fn v => [(mk_d v, mk_DEFL (argT v)), (mk_p v, mk_LIFTDEFL (argT v))]) vs; + val typeTs = map argT (filter (member (op =) tfrees) vs); + val defl_args = map snd (filter (member (op =) frees o fst) args); + in + (typeTs, defl_args) + end; + val defl_flagss = map get_defl_flags doms; (* declare deflation combinator constants *) - fun declare_defl_const (vs, tbind, mx, rhs, morphs) thy = + fun declare_defl_const ((typeTs, defl_args), (_, tbind, _, _, _)) thy = let - fun argT v = TFree (v, the_sort v); - val Ts = map argT vs; - val flags = map (is_bifinite thy) Ts; - val defl_type = mk_defl_type flags Ts; val defl_bind = Binding.suffix_name "_defl" tbind; + val defl_type = + map Term.itselfT typeTs ---> map (K deflT) defl_args -->> deflT; in Sign.declare_const ((defl_bind, defl_type), NoSyn) thy end; - val (defl_consts, thy) = fold_map declare_defl_const doms thy; - val defl_names = map (fst o dest_Const) defl_consts; + val (defl_consts, thy) = + fold_map declare_defl_const (defl_flagss ~~ doms) thy; (* defining equations for type combinators *) - fun mk_defl_tab (defl_const, (flags, lhsT)) = + fun mk_defl_term (defl_const, (typeTs, defl_args)) = let - val Ts = snd (dest_Type lhsT); - val type_args = map (Logic.mk_type o snd) (filter_out fst (flags ~~ Ts)); - val defl_args = map (mk_DEFL o snd) (filter fst (flags ~~ Ts)); + val type_args = map Logic.mk_type typeTs; in - (lhsT, list_ccomb (list_comb (defl_const, type_args), defl_args)) + list_ccomb (list_comb (defl_const, type_args), defl_args) end; - val defl_tab = - map mk_defl_tab (defl_consts ~~ (defl_flagss ~~ map fst dom_eqns)); + val defl_terms = map mk_defl_term (defl_consts ~~ defl_flagss); + val defl_tab = map fst dom_eqns ~~ defl_terms; + val defl_tab' = map fst dom_eqns ~~ map mk_u_defl defl_terms; fun mk_defl_spec (lhsT, rhsT) = - mk_eqs (defl_of_typ tmp_thy defl_tab lhsT, - defl_of_typ tmp_thy defl_tab rhsT); + mk_eqs (defl_of_typ tmp_thy defl_tab defl_tab' lhsT, + defl_of_typ tmp_thy defl_tab defl_tab' rhsT); val defl_specs = map mk_defl_spec dom_eqns; (* register recursive definition of deflation combinators *) @@ -486,20 +519,26 @@ add_fixdefs (defl_binds ~~ defl_specs) thy; (* define types using deflation combinators *) - fun make_repdef ((vs, tbind, mx, _, _), defl_const) thy = + fun make_repdef ((vs, tbind, mx, _, _), defl) thy = let - fun tfree a = TFree (a, the_sort a); - val Ts = map tfree vs; - val type_args = map Logic.mk_type (filter_out (is_bifinite thy) Ts); - val defl_args = map mk_DEFL (filter (is_bifinite thy) Ts); - val defl = list_ccomb (list_comb (defl_const, type_args), defl_args); - val ((_, _, _, {DEFL, ...}), thy) = - Repdef.add_repdef false NONE (tbind, map (rpair dummyS) vs, mx) defl NONE thy; + val spec = (tbind, map (rpair dummyS) vs, mx); + val ((_, _, _, {DEFL, LIFTDEFL, liftemb_def, liftprj_def, ...}), thy) = + Repdef.add_repdef false NONE spec defl NONE thy; + (* declare domain_defl_simps rules *) + val thy = Context.theory_map (RepData.add_thm DEFL) thy; + val thy = Context.theory_map (RepData.add_thm LIFTDEFL) thy; + (* declare domain_isodefl rule *) + val liftemb' = Thm.transfer thy (liftemb_def RS meta_eq_to_obj_eq); + val liftprj' = Thm.transfer thy (liftprj_def RS meta_eq_to_obj_eq); + val (_, thy) = + Global_Theory.add_thm + ((Binding.suffix_name "_u" (Binding.prefix_name "isodefl_" tbind), + Drule.zero_var_indexes (@{thm isodefl_u} OF [liftemb', liftprj'])), + [IsodeflData.add]) thy; in (DEFL, thy) end; - val (DEFL_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy; - val thy = fold (Context.theory_map o RepData.add_thm) DEFL_thms thy; + val (DEFL_thms, thy) = fold_map make_repdef (doms ~~ defl_terms) thy; (* prove DEFL equations *) fun mk_DEFL_eq_thm (lhsT, rhsT) = @@ -508,7 +547,7 @@ val DEFL_simps = RepData.get (ProofContext.init_global thy); val tac = rewrite_goals_tac (map mk_meta_eq DEFL_simps) - THEN resolve_tac defl_unfold_thms 1; + THEN TRY (resolve_tac defl_unfold_thms 1); in Goal.prove_global thy [] [] goal (K tac) end; @@ -583,18 +622,22 @@ let fun unprime a = Library.unprefix "'" a; fun mk_d T = Free ("d" ^ unprime (fst (dest_TFree T)), deflT); + fun mk_p T = Free ("p" ^ unprime (fst (dest_TFree T)), deflT); fun mk_f T = Free ("f" ^ unprime (fst (dest_TFree T)), T ->> T); - fun mk_assm T = mk_trp (isodefl_const T $ mk_f T $ mk_d T); - fun mk_goal ((map_const, defl_const), (T, rhsT)) = + fun mk_assm t = + case try dest_LIFTDEFL t of + SOME T => mk_trp (isodefl_const (mk_upT T) $ mk_u_map (mk_f T) $ mk_p T) + | NONE => + let val T = dest_DEFL t + in mk_trp (isodefl_const T $ mk_f T $ mk_d T) end; + fun mk_goal (map_const, (T, rhsT)) = let val (_, Ts) = dest_Type T; val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts)); - val type_args = map Logic.mk_type (filter_out (is_bifinite thy) Ts); - val defl_args = map mk_d (filter (is_bifinite thy) Ts); - val defl_term = list_ccomb (list_comb (defl_const, type_args), defl_args); + val defl_term = defl_of_typ thy (Ts ~~ map mk_d Ts) (Ts ~~ map mk_p Ts) T; in isodefl_const T $ map_term $ defl_term end; - val assms = (map mk_assm o filter (is_cpo thy) o snd o dest_Type o fst o hd) dom_eqns; - val goals = map mk_goal (map_consts ~~ defl_consts ~~ dom_eqns); + val assms = (map mk_assm o snd o hd) defl_flagss; + val goals = map mk_goal (map_consts ~~ dom_eqns); val goal = mk_trp (foldr1 HOLogic.mk_conj goals); val start_thms = @{thm split_def} :: defl_apply_thms @ map_apply_thms; @@ -605,7 +648,7 @@ val lthy = ProofContext.init_global thy; val DEFL_simps = map (fn th => th RS sym) (RepData.get lthy); val isodefl_rules = - @{thms conjI isodefl_ID_DEFL} + @{thms conjI isodefl_ID_DEFL isodefl_LIFTDEFL} @ isodefl_abs_rep_thms @ IsodeflData.get (ProofContext.init_global thy); in @@ -647,7 +690,7 @@ [rtac @{thm isodefl_DEFL_imp_ID} 1, stac DEFL_thm 1, rtac isodefl_thm 1, - REPEAT (rtac @{thm isodefl_ID_DEFL} 1)]; + REPEAT (resolve_tac @{thms isodefl_ID_DEFL isodefl_LIFTDEFL} 1)]; in Goal.prove_global thy [] [] goal (K tac) end; diff -r 05be0c37db1d -r 6de5839e2fb3 src/HOLCF/Tools/repdef.ML --- a/src/HOLCF/Tools/repdef.ML Tue Nov 09 08:41:36 2010 -0800 +++ b/src/HOLCF/Tools/repdef.ML Tue Nov 09 16:37:13 2010 -0800 @@ -7,7 +7,16 @@ signature REPDEF = sig type rep_info = - { emb_def: thm, prj_def: thm, defl_def: thm, DEFL: thm } + { + emb_def : thm, + prj_def : thm, + defl_def : thm, + liftemb_def : thm, + liftprj_def : thm, + liftdefl_def : thm, + DEFL : thm, + LIFTDEFL : thm + } val add_repdef: bool -> binding option -> binding * (string * sort) list * mixfix -> term -> (binding * binding) option -> theory -> @@ -28,7 +37,16 @@ (** type definitions **) type rep_info = - { emb_def: thm, prj_def: thm, defl_def: thm, DEFL: thm }; + { + emb_def : thm, + prj_def : thm, + defl_def : thm, + liftemb_def : thm, + liftprj_def : thm, + liftdefl_def : thm, + DEFL : thm, + LIFTDEFL : thm + }; (* building types and terms *) @@ -37,6 +55,18 @@ fun emb_const T = Const (@{const_name emb}, T ->> udomT); fun prj_const T = Const (@{const_name prj}, udomT ->> T); fun defl_const T = Const (@{const_name defl}, Term.itselfT T --> deflT); +fun liftemb_const T = Const (@{const_name liftemb}, mk_upT T ->> udomT); +fun liftprj_const T = Const (@{const_name liftprj}, udomT ->> mk_upT T); +fun liftdefl_const T = Const (@{const_name liftdefl}, Term.itselfT T --> deflT); + +fun mk_u_map t = + let + val (T, U) = dest_cfunT (fastype_of t); + val u_map_type = (T ->> U) ->> (mk_upT T ->> mk_upT U); + val u_map_const = Const (@{const_name u_map}, u_map_type); + in + mk_capply (u_map_const, t) + end; fun mk_cast (t, x) = capply_const (udomT, udomT) @@ -100,10 +130,24 @@ Abs ("x", udomT, Abs_const $ mk_cast (defl, Bound 0))); val defl_eqn = Logic.mk_equals (defl_const newT, Abs ("x", Term.itselfT newT, defl)); + val liftemb_eqn = + Logic.mk_equals (liftemb_const newT, + mk_cfcomp (@{term "udom_emb u_approx"}, mk_u_map (emb_const newT))); + val liftprj_eqn = + Logic.mk_equals (liftprj_const newT, + mk_cfcomp (mk_u_map (prj_const newT), @{term "udom_prj u_approx"})); + val liftdefl_eqn = + Logic.mk_equals (liftdefl_const newT, + Abs ("t", Term.itselfT newT, + mk_capply (@{const u_defl}, defl_const newT $ Logic.mk_type newT))); + val name_def = Binding.suffix_name "_def" name; val emb_bind = (Binding.prefix_name "emb_" name_def, []); val prj_bind = (Binding.prefix_name "prj_" name_def, []); val defl_bind = (Binding.prefix_name "defl_" name_def, []); + val liftemb_bind = (Binding.prefix_name "liftemb_" name_def, []); + val liftprj_bind = (Binding.prefix_name "liftprj_" name_def, []); + val liftdefl_bind = (Binding.prefix_name "liftdefl_" name_def, []); (*instantiate class rep*) val lthy = thy @@ -114,16 +158,26 @@ Specification.definition (NONE, (prj_bind, prj_eqn)) lthy; val ((_, (_, defl_ldef)), lthy) = Specification.definition (NONE, (defl_bind, defl_eqn)) lthy; + val ((_, (_, liftemb_ldef)), lthy) = + Specification.definition (NONE, (liftemb_bind, liftemb_eqn)) lthy; + val ((_, (_, liftprj_ldef)), lthy) = + Specification.definition (NONE, (liftprj_bind, liftprj_eqn)) lthy; + val ((_, (_, liftdefl_ldef)), lthy) = + Specification.definition (NONE, (liftdefl_bind, liftdefl_eqn)) lthy; val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy); val emb_def = singleton (ProofContext.export lthy ctxt_thy) emb_ldef; val prj_def = singleton (ProofContext.export lthy ctxt_thy) prj_ldef; val defl_def = singleton (ProofContext.export lthy ctxt_thy) defl_ldef; + val liftemb_def = singleton (ProofContext.export lthy ctxt_thy) liftemb_ldef; + val liftprj_def = singleton (ProofContext.export lthy ctxt_thy) liftprj_ldef; + val liftdefl_def = singleton (ProofContext.export lthy ctxt_thy) liftdefl_ldef; val type_definition_thm = MetaSimplifier.rewrite_rule (the_list (#set_def (#2 info))) (#type_definition (#2 info)); val typedef_thms = - [type_definition_thm, #below_def cpo_info, emb_def, prj_def, defl_def]; + [type_definition_thm, #below_def cpo_info, emb_def, prj_def, defl_def, + liftemb_def, liftprj_def, liftdefl_def]; val thy = lthy |> Class.prove_instantiation_instance (K (Tactic.rtac (@{thm typedef_rep_class} OF typedef_thms) 1)) @@ -131,15 +185,25 @@ (*other theorems*) val defl_thm' = Thm.transfer thy defl_def; + val liftdefl_thm' = Thm.transfer thy liftdefl_def; val (DEFL_thm, thy) = thy |> Sign.add_path (Binding.name_of name) |> Global_Theory.add_thm ((Binding.prefix_name "DEFL_" name, Drule.zero_var_indexes (@{thm typedef_DEFL} OF [defl_thm'])), []) ||> Sign.restore_naming thy; + val (LIFTDEFL_thm, thy) = thy + |> Sign.add_path (Binding.name_of name) + |> Global_Theory.add_thm + ((Binding.prefix_name "LIFTDEFL_" name, + Drule.zero_var_indexes (@{thm typedef_LIFTDEFL} OF [liftdefl_thm'])), []) + ||> Sign.restore_naming thy; val rep_info = - { emb_def = emb_def, prj_def = prj_def, defl_def = defl_def, DEFL = DEFL_thm }; + { emb_def = emb_def, prj_def = prj_def, defl_def = defl_def, + liftemb_def = liftemb_def, liftprj_def = liftprj_def, + liftdefl_def = liftdefl_def, + DEFL = DEFL_thm, LIFTDEFL = LIFTDEFL_thm }; in ((info, cpo_info, pcpo_info, rep_info), thy) end diff -r 05be0c37db1d -r 6de5839e2fb3 src/HOLCF/UpperPD.thy --- a/src/HOLCF/UpperPD.thy Tue Nov 09 08:41:36 2010 -0800 +++ b/src/HOLCF/UpperPD.thy Tue Nov 09 16:37:13 2010 -0800 @@ -460,7 +460,18 @@ definition "defl (t::'a upper_pd itself) = upper_defl\DEFL('a)" -instance proof +definition + "(liftemb :: 'a upper_pd u \ udom) = udom_emb u_approx oo u_map\emb" + +definition + "(liftprj :: udom \ 'a upper_pd u) = u_map\prj oo udom_prj u_approx" + +definition + "liftdefl (t::'a upper_pd itself) = u_defl\DEFL('a upper_pd)" + +instance +using liftemb_upper_pd_def liftprj_upper_pd_def liftdefl_upper_pd_def +proof (rule bifinite_class_intro) show "ep_pair emb (prj :: udom \ 'a upper_pd)" unfolding emb_upper_pd_def prj_upper_pd_def using ep_pair_udom [OF upper_approx] diff -r 05be0c37db1d -r 6de5839e2fb3 src/HOLCF/ex/Domain_Proofs.thy --- a/src/HOLCF/ex/Domain_Proofs.thy Tue Nov 09 08:41:36 2010 -0800 +++ b/src/HOLCF/ex/Domain_Proofs.thy Tue Nov 09 16:37:13 2010 -0800 @@ -8,8 +8,6 @@ imports HOLCF begin -default_sort bifinite - (* The definitions and proofs below are for the following recursive @@ -19,6 +17,9 @@ and 'a bar = Bar (lazy "'a baz \ tr") and 'a baz = Baz (lazy "'a foo convex_pd \ tr") +TODO: add another type parameter that is strict, +to show the different handling of LIFTDEFL vs. DEFL. + *) (********************************************************************) @@ -32,13 +33,13 @@ "defl \ defl \ defl \ defl \ defl \ defl \ defl" where "foo_bar_baz_deflF = (\ a. Abs_cfun (\(t1, t2, t3). - ( ssum_defl\DEFL(one)\(sprod_defl\(u_defl\a)\(u_defl\t2)) + ( ssum_defl\DEFL(one)\(sprod_defl\a\(u_defl\t2)) , u_defl\(cfun_defl\t3\DEFL(tr)) , u_defl\(cfun_defl\(convex_defl\t1)\DEFL(tr)))))" lemma foo_bar_baz_deflF_beta: "foo_bar_baz_deflF\a\t = - ( ssum_defl\DEFL(one)\(sprod_defl\(u_defl\a)\(u_defl\(fst (snd t)))) + ( ssum_defl\DEFL(one)\(sprod_defl\a\(u_defl\(fst (snd t)))) , u_defl\(cfun_defl\(snd (snd t))\DEFL(tr)) , u_defl\(cfun_defl\(convex_defl\(fst t))\DEFL(tr)))" unfolding foo_bar_baz_deflF_def @@ -64,7 +65,7 @@ text {* Unfold rules for each combinator. *} lemma foo_defl_unfold: - "foo_defl\a = ssum_defl\DEFL(one)\(sprod_defl\(u_defl\a)\(u_defl\(bar_defl\a)))" + "foo_defl\a = ssum_defl\DEFL(one)\(sprod_defl\a\(u_defl\(bar_defl\a)))" unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) lemma bar_defl_unfold: "bar_defl\a = u_defl\(cfun_defl\(baz_defl\a)\DEFL(tr))" @@ -82,13 +83,13 @@ text {* Use @{text pcpodef} with the appropriate type combinator. *} -pcpodef (open) 'a foo = "defl_set (foo_defl\DEFL('a))" +pcpodef (open) 'a foo = "defl_set (foo_defl\LIFTDEFL('a))" by (rule defl_set_bottom, rule adm_defl_set) -pcpodef (open) 'a bar = "defl_set (bar_defl\DEFL('a))" +pcpodef (open) 'a bar = "defl_set (bar_defl\LIFTDEFL('a))" by (rule defl_set_bottom, rule adm_defl_set) -pcpodef (open) 'a baz = "defl_set (baz_defl\DEFL('a))" +pcpodef (open) 'a baz = "defl_set (baz_defl\LIFTDEFL('a))" by (rule defl_set_bottom, rule adm_defl_set) text {* Prove rep instance using lemma @{text typedef_rep_class}. *} @@ -100,10 +101,19 @@ where "emb_foo \ (\ x. Rep_foo x)" definition prj_foo :: "udom \ 'a foo" -where "prj_foo \ (\ y. Abs_foo (cast\(foo_defl\DEFL('a))\y))" +where "prj_foo \ (\ y. Abs_foo (cast\(foo_defl\LIFTDEFL('a))\y))" definition defl_foo :: "'a foo itself \ defl" -where "defl_foo \ \a. foo_defl\DEFL('a)" +where "defl_foo \ \a. foo_defl\LIFTDEFL('a)" + +definition + "(liftemb :: 'a foo u \ udom) \ udom_emb u_approx oo u_map\emb" + +definition + "(liftprj :: udom \ 'a foo u) \ u_map\prj oo udom_prj u_approx" + +definition + "liftdefl \ \(t::'a foo itself). u_defl\DEFL('a foo)" instance apply (rule typedef_rep_class) @@ -112,6 +122,9 @@ apply (rule emb_foo_def) apply (rule prj_foo_def) apply (rule defl_foo_def) +apply (rule liftemb_foo_def) +apply (rule liftprj_foo_def) +apply (rule liftdefl_foo_def) done end @@ -123,10 +136,19 @@ where "emb_bar \ (\ x. Rep_bar x)" definition prj_bar :: "udom \ 'a bar" -where "prj_bar \ (\ y. Abs_bar (cast\(bar_defl\DEFL('a))\y))" +where "prj_bar \ (\ y. Abs_bar (cast\(bar_defl\LIFTDEFL('a))\y))" definition defl_bar :: "'a bar itself \ defl" -where "defl_bar \ \a. bar_defl\DEFL('a)" +where "defl_bar \ \a. bar_defl\LIFTDEFL('a)" + +definition + "(liftemb :: 'a bar u \ udom) \ udom_emb u_approx oo u_map\emb" + +definition + "(liftprj :: udom \ 'a bar u) \ u_map\prj oo udom_prj u_approx" + +definition + "liftdefl \ \(t::'a bar itself). u_defl\DEFL('a bar)" instance apply (rule typedef_rep_class) @@ -135,6 +157,9 @@ apply (rule emb_bar_def) apply (rule prj_bar_def) apply (rule defl_bar_def) +apply (rule liftemb_bar_def) +apply (rule liftprj_bar_def) +apply (rule liftdefl_bar_def) done end @@ -146,10 +171,19 @@ where "emb_baz \ (\ x. Rep_baz x)" definition prj_baz :: "udom \ 'a baz" -where "prj_baz \ (\ y. Abs_baz (cast\(baz_defl\DEFL('a))\y))" +where "prj_baz \ (\ y. Abs_baz (cast\(baz_defl\LIFTDEFL('a))\y))" definition defl_baz :: "'a baz itself \ defl" -where "defl_baz \ \a. baz_defl\DEFL('a)" +where "defl_baz \ \a. baz_defl\LIFTDEFL('a)" + +definition + "(liftemb :: 'a baz u \ udom) \ udom_emb u_approx oo u_map\emb" + +definition + "(liftprj :: udom \ 'a baz u) \ u_map\prj oo udom_prj u_approx" + +definition + "liftdefl \ \(t::'a baz itself). u_defl\DEFL('a baz)" instance apply (rule typedef_rep_class) @@ -158,42 +192,60 @@ apply (rule emb_baz_def) apply (rule prj_baz_def) apply (rule defl_baz_def) +apply (rule liftemb_baz_def) +apply (rule liftprj_baz_def) +apply (rule liftdefl_baz_def) done end text {* Prove DEFL rules using lemma @{text typedef_DEFL}. *} -lemma DEFL_foo: "DEFL('a foo) = foo_defl\DEFL('a)" +lemma DEFL_foo: "DEFL('a foo) = foo_defl\LIFTDEFL('a)" apply (rule typedef_DEFL) apply (rule defl_foo_def) done -lemma DEFL_bar: "DEFL('a bar) = bar_defl\DEFL('a)" +lemma LIFTDEFL_foo [domain_defl_simps]: + "LIFTDEFL('a foo) = u_defl\DEFL('a foo)" +apply (rule typedef_LIFTDEFL) +apply (rule liftdefl_foo_def) +done + +lemma DEFL_bar: "DEFL('a bar) = bar_defl\LIFTDEFL('a)" apply (rule typedef_DEFL) apply (rule defl_bar_def) done -lemma DEFL_baz: "DEFL('a baz) = baz_defl\DEFL('a)" +lemma LIFTDEFL_bar [domain_defl_simps]: + "LIFTDEFL('a bar) = u_defl\DEFL('a bar)" +apply (rule typedef_LIFTDEFL) +apply (rule liftdefl_bar_def) +done + +lemma DEFL_baz: "DEFL('a baz) = baz_defl\LIFTDEFL('a)" apply (rule typedef_DEFL) apply (rule defl_baz_def) done +lemma LIFTDEFL_baz [domain_defl_simps]: + "LIFTDEFL('a baz) = u_defl\DEFL('a baz)" +apply (rule typedef_LIFTDEFL) +apply (rule liftdefl_baz_def) +done + text {* Prove DEFL equations using type combinator unfold lemmas. *} -lemmas DEFL_simps = - DEFL_ssum DEFL_sprod DEFL_u DEFL_cfun - lemma DEFL_foo': "DEFL('a foo) = DEFL(one \ 'a\<^sub>\ \ ('a bar)\<^sub>\)" -unfolding DEFL_foo DEFL_bar DEFL_baz DEFL_simps +unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps by (rule foo_defl_unfold) lemma DEFL_bar': "DEFL('a bar) = DEFL(('a baz \ tr)\<^sub>\)" -unfolding DEFL_foo DEFL_bar DEFL_baz DEFL_simps +unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps by (rule bar_defl_unfold) lemma DEFL_baz': "DEFL('a baz) = DEFL(('a foo convex_pd \ tr)\<^sub>\)" -unfolding DEFL_foo DEFL_bar DEFL_baz DEFL_simps DEFL_convex +unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps by (rule baz_defl_unfold) (********************************************************************) @@ -254,6 +306,24 @@ "isodefl d t \ isodefl (baz_abs oo d oo baz_rep) t" by (rule isodefl_abs_rep [OF DEFL_baz' baz_abs_def baz_rep_def]) +lemma isodefl_foo_u [domain_isodefl]: + "isodefl (d :: 'a foo \ _) t \ isodefl (u_map\d) (u_defl\t)" +using liftemb_foo_def [THEN meta_eq_to_obj_eq] +using liftprj_foo_def [THEN meta_eq_to_obj_eq] +by (rule isodefl_u) + +lemma isodefl_bar_u [domain_isodefl]: + "isodefl (d :: 'a bar \ _) t \ isodefl (u_map\d) (u_defl\t)" +using liftemb_bar_def [THEN meta_eq_to_obj_eq] +using liftprj_bar_def [THEN meta_eq_to_obj_eq] +by (rule isodefl_u) + +lemma isodefl_baz_u [domain_isodefl]: + "isodefl (d :: 'a baz \ _) t \ isodefl (u_map\d) (u_defl\t)" +using liftemb_baz_def [THEN meta_eq_to_obj_eq] +using liftprj_baz_def [THEN meta_eq_to_obj_eq] +by (rule isodefl_u) + (********************************************************************) subsection {* Step 4: Define map functions, prove isodefl property *} @@ -314,7 +384,7 @@ text {* Prove isodefl rules for all map functions simultaneously. *} lemma isodefl_foo_bar_baz: - assumes isodefl_d: "isodefl d t" + assumes isodefl_d: "isodefl (u_map\d) t" shows "isodefl (foo_map\d) (foo_defl\t) \ isodefl (bar_map\d) (bar_defl\t) \ @@ -332,8 +402,8 @@ isodefl_foo_abs isodefl_bar_abs isodefl_baz_abs - isodefl_ssum isodefl_sprod isodefl_ID_DEFL - isodefl_u isodefl_convex isodefl_cfun + domain_isodefl + isodefl_ID_DEFL isodefl_LIFTDEFL isodefl_d ) apply assumption+ @@ -349,21 +419,21 @@ apply (rule isodefl_DEFL_imp_ID) apply (subst DEFL_foo) apply (rule isodefl_foo) -apply (rule isodefl_ID_DEFL) +apply (rule isodefl_LIFTDEFL) done lemma bar_map_ID: "bar_map\ID = ID" apply (rule isodefl_DEFL_imp_ID) apply (subst DEFL_bar) apply (rule isodefl_bar) -apply (rule isodefl_ID_DEFL) +apply (rule isodefl_LIFTDEFL) done lemma baz_map_ID: "baz_map\ID = ID" apply (rule isodefl_DEFL_imp_ID) apply (subst DEFL_baz) apply (rule isodefl_baz) -apply (rule isodefl_ID_DEFL) +apply (rule isodefl_LIFTDEFL) done (********************************************************************)