--- 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 \<Rightarrow> defl"
+ fixes liftemb :: "'a\<^sub>\<bottom> \<rightarrow> udom"
+ fixes liftprj :: "udom \<rightarrow> 'a\<^sub>\<bottom>"
+ assumes predomain_ep: "ep_pair liftemb liftprj"
+ assumes cast_liftdefl: "cast\<cdot>(liftdefl TYPE('a::cpo)) = liftemb oo liftprj"
+
+syntax "_LIFTDEFL" :: "type \<Rightarrow> logic" ("(1LIFTDEFL/(1'(_')))")
+translations "LIFTDEFL('t)" \<rightleftharpoons> "CONST liftdefl TYPE('t)"
+
+class bifinite = predomain + pcpo +
fixes emb :: "'a::pcpo \<rightarrow> udom"
fixes prj :: "udom \<rightarrow> 'a::pcpo"
fixes defl :: "'a itself \<Rightarrow> 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 \<Rightarrow> defl"})
+ , (@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"})
+ , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::pcpo"})
+ , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"})
+ , (@{const_name liftemb}, SOME @{typ "'a::pcpo u \<rightarrow> udom"})
+ , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::pcpo u"}) ]
+*}
+
+lemma bifinite_class_intro:
+ assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+ assumes liftprj: "(liftprj :: udom \<rightarrow> 'a u) = u_map\<cdot>prj oo udom_prj u_approx"
+ assumes liftdefl: "liftdefl TYPE('a) = u_defl\<cdot>DEFL('a)"
+ assumes ep_pair: "ep_pair emb (prj :: udom \<rightarrow> 'a)"
+ assumes cast_defl: "cast\<cdot>DEFL('a) = emb oo (prj :: udom \<rightarrow> 'a)"
+ shows "OFCLASS('a, bifinite_class)"
+proof
+ show "ep_pair liftemb (liftprj :: udom \<rightarrow> 'a u)"
+ unfolding liftemb liftprj
+ by (intro ep_pair_comp ep_pair_u_map ep_pair ep_pair_udom u_approx)
+ show "cast\<cdot>LIFTDEFL('a) = liftemb oo (liftprj :: udom \<rightarrow> '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 \<Rightarrow> defl"})
+ , (@{const_name emb}, SOME @{typ "'a::bifinite \<rightarrow> udom"})
+ , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::bifinite"})
+ , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> defl"})
+ , (@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom"})
+ , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::predomain u"}) ]
+*}
+
subsection {* The universal domain is bifinite *}
instantiation udom :: bifinite
@@ -257,7 +311,18 @@
definition
"defl (t::udom itself) = (\<Squnion>i. defl_principal (Abs_fin_defl (udom_approx i)))"
-instance proof
+definition
+ "(liftemb :: udom u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> udom u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl (t::udom itself) = u_defl\<cdot>DEFL(udom)"
+
+instance
+using liftemb_udom_def liftprj_udom_def liftdefl_udom_def
+proof (rule bifinite_class_intro)
show "ep_pair emb (prj :: udom \<rightarrow> udom)"
by (simp add: ep_pair.intro)
show "cast\<cdot>DEFL(udom) = emb oo (prj :: udom \<rightarrow> 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 \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> 'a u u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl (t::'a u itself) = u_defl\<cdot>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 \<rightarrow> 'a u)"
+ unfolding emb_u_def prj_u_def
+ by (rule predomain_ep)
+ show "cast\<cdot>DEFL('a u) = emb oo (prj :: udom \<rightarrow> '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\<cdot>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 \<rightarrow> 'b) itself) = cfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
-instance proof
+definition
+ "(liftemb :: ('a \<rightarrow> 'b) u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> ('a \<rightarrow> 'b) u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl (t::('a \<rightarrow> 'b) itself) = u_defl\<cdot>DEFL('a \<rightarrow> 'b)"
+
+instance
+using liftemb_cfun_def liftprj_cfun_def liftdefl_cfun_def
+proof (rule bifinite_class_intro)
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> '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\<cdot>DEFL('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> '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 \<rightarrow> 'b::bifinite) = cfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
by (rule defl_cfun_def)
+lemma LIFTDEFL_cfun:
+ "LIFTDEFL('a::bifinite \<rightarrow> 'b::bifinite) = u_defl\<cdot>DEFL('a \<rightarrow> '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 \<times> 'b) itself) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
-instance proof
+definition
+ "(liftemb :: ('a \<times> 'b) u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> ('a \<times> 'b) u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl (t::('a \<times> 'b) itself) = u_defl\<cdot>DEFL('a \<times> 'b)"
+
+instance
+using liftemb_prod_def liftprj_prod_def liftdefl_prod_def
+proof (rule bifinite_class_intro)
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)"
unfolding emb_prod_def prj_prod_def
using ep_pair_udom [OF prod_approx]
@@ -338,6 +470,10 @@
"DEFL('a::bifinite \<times> 'b::bifinite) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
by (rule defl_prod_def)
+lemma LIFTDEFL_prod:
+ "LIFTDEFL('a::bifinite \<times> 'b::bifinite) = u_defl\<cdot>DEFL('a \<times> '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 \<otimes> 'b) itself) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
-instance proof
+definition
+ "(liftemb :: ('a \<otimes> 'b) u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> ('a \<otimes> 'b) u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl (t::('a \<otimes> 'b) itself) = u_defl\<cdot>DEFL('a \<otimes> 'b)"
+
+instance
+using liftemb_sprod_def liftprj_sprod_def liftdefl_sprod_def
+proof (rule bifinite_class_intro)
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
unfolding emb_sprod_def prj_sprod_def
using ep_pair_udom [OF sprod_approx]
@@ -369,51 +516,23 @@
"DEFL('a::bifinite \<otimes> 'b::bifinite) = sprod_defl\<cdot>DEFL('a)\<cdot>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 \<otimes> 'b::bifinite) = u_defl\<cdot>DEFL('a \<otimes> 'b)"
+by (rule liftdefl_sprod_def)
-definition
- "emb = udom_emb u_approx oo u_map\<cdot>emb"
-
-definition
- "prj = u_map\<cdot>prj oo udom_prj u_approx"
-
-definition
- "defl (t::'a u itself) = u_defl\<cdot>DEFL('a)"
+subsection {* Countable discrete cpos are predomains *}
-instance proof
- show "ep_pair emb (prj :: udom \<rightarrow> '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\<cdot>DEFL('a u) = emb oo (prj :: udom \<rightarrow> '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 \<Rightarrow> 'a::countable discr u \<rightarrow> 'a discr u"
+ where "discr_approx = (\<lambda>i. \<Lambda>(up\<cdot>x). if to_nat (undiscr x) < i then up\<cdot>x else \<bottom>)"
-lemma DEFL_u: "DEFL('a::bifinite u) = u_defl\<cdot>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 \<Rightarrow> 'a::countable lift \<rightarrow> 'a lift"
-where
- "lift_approx = (\<lambda>i. FLIFT x. if to_nat x < i then Def x else \<bottom>)"
-
-lemma chain_lift_approx [simp]: "chain lift_approx"
- unfolding lift_approx_def
- by (rule chainI, simp add: FLIFT_mono)
-
-lemma lub_lift_approx [simp]: "(\<Squnion>i. lift_approx i) = ID"
+lemma lub_discr_approx [simp]: "(\<Squnion>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\<cdot>x \<sqsubseteq> x"
- unfolding lift_approx_def
+ fix x :: "'a discr u"
+ show "discr_approx i\<cdot>x \<sqsubseteq> x"
+ unfolding discr_approx_def
by (cases x, simp, simp)
- show "lift_approx i\<cdot>(lift_approx i\<cdot>x) = lift_approx i\<cdot>x"
- unfolding lift_approx_def
+ show "discr_approx i\<cdot>(discr_approx i\<cdot>x) = discr_approx i\<cdot>x"
+ unfolding discr_approx_def
by (cases x, simp, simp)
- show "finite {x::'a lift. lift_approx i\<cdot>x = x}"
+ show "finite {x::'a discr u. discr_approx i\<cdot>x = x}"
proof (rule finite_subset)
- let ?S = "insert (\<bottom>::'a lift) (Def ` to_nat -` {..<i})"
- show "{x::'a lift. lift_approx i\<cdot>x = x} \<subseteq> ?S"
- unfolding lift_approx_def
+ let ?S = "insert (\<bottom>::'a discr u) ((\<lambda>x. up\<cdot>x) ` undiscr -` to_nat -` {..<i})"
+ show "{x::'a discr u. discr_approx i\<cdot>x = x} \<subseteq> ?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) =
- (\<Squnion>i. defl_principal (Abs_fin_defl (emb oo lift_approx i oo prj)))"
+ "liftdefl (t::'a discr itself) =
+ (\<Squnion>i. defl_principal (Abs_fin_defl (liftemb oo discr_approx i oo liftprj)))"
instance proof
- show ep: "ep_pair emb (prj :: udom \<rightarrow> 'a lift)"
- unfolding emb_lift_def prj_lift_def
- by (rule ep_pair_udom [OF lift_approx])
- show "cast\<cdot>DEFL('a lift) = emb oo (prj :: udom \<rightarrow> 'a lift)"
- unfolding defl_lift_def
+ show "ep_pair liftemb (liftprj :: udom \<rightarrow> 'a discr u)"
+ unfolding liftemb_discr_def liftprj_discr_def
+ by (rule ep_pair_udom [OF discr_approx])
+ show "cast\<cdot>LIFTDEFL('a discr) = liftemb oo (liftprj :: udom \<rightarrow> '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 \<oplus> 'b) itself) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
-instance proof
+definition
+ "(liftemb :: ('a \<oplus> 'b) u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> ('a \<oplus> 'b) u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl (t::('a \<oplus> 'b) itself) = u_defl\<cdot>DEFL('a \<oplus> 'b)"
+
+instance
+using liftemb_ssum_def liftprj_ssum_def liftdefl_ssum_def
+proof (rule bifinite_class_intro)
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> '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\<cdot>DEFL('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> '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 \<oplus> 'b::bifinite) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
by (rule defl_ssum_def)
+lemma LIFTDEFL_ssum:
+ "LIFTDEFL('a::bifinite \<oplus> 'b::bifinite) = u_defl\<cdot>DEFL('a \<oplus> 'b)"
+by (rule liftdefl_ssum_def)
+
+subsection {* Lifted countable types are bifinite domains *}
+
+instantiation lift :: (countable) bifinite
+begin
+
+definition
+ "emb = emb oo (\<Lambda> x. Rep_lift x)"
+
+definition
+ "prj = (\<Lambda> y. Abs_lift y) oo prj"
+
+definition
+ "defl (t::'a lift itself) = DEFL('a discr u)"
+
+definition
+ "(liftemb :: 'a lift u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> 'a lift u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl (t::'a lift itself) = u_defl\<cdot>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 (\<Lambda>(x::'a lift). Rep_lift x) (\<Lambda> y. Abs_lift y)"
+ by (simp add: ep_pair_def)
+ thus "ep_pair emb (prj :: udom \<rightarrow> 'a lift)"
+ unfolding emb_lift_def prj_lift_def
+ using ep_pair_emb_prj by (rule ep_pair_comp)
+ show "cast\<cdot>DEFL('a lift) = emb oo (prj :: udom \<rightarrow> 'a lift)"
+ unfolding emb_lift_def prj_lift_def defl_lift_def cast_DEFL
+ by (simp add: cfcomp1)
+qed
+
end
+
+end
--- 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\<cdot>DEFL('a)"
-instance proof
+definition
+ "(liftemb :: 'a convex_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl (t::'a convex_pd itself) = u_defl\<cdot>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 \<rightarrow> 'a convex_pd)"
unfolding emb_convex_pd_def prj_convex_pd_def
using ep_pair_udom [OF convex_approx]
--- 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) =
(\<Squnion>i. defl_principal (Abs_fin_defl (emb oo defl_approx i oo prj)))"
-instance proof
+definition
+ "(liftemb :: defl u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> defl u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl (t::defl itself) = u_defl\<cdot>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 \<rightarrow> defl)"
unfolding emb_defl_def prj_defl_def
by (rule ep_pair_udom [OF defl_approx])
--- 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 \<rightarrow>! 'b) itself) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
-instance proof
+definition
+ "(liftemb :: ('a \<rightarrow>! 'b) u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> ('a \<rightarrow>! 'b) u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl (t::('a \<rightarrow>! 'b) itself) = u_defl\<cdot>DEFL('a \<rightarrow>! 'b)"
+
+instance
+using liftemb_sfun_def liftprj_sfun_def liftdefl_sfun_def
+proof (rule bifinite_class_intro)
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
unfolding emb_sfun_def prj_sfun_def
using ep_pair_udom [OF sfun_approx]
--- 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\<cdot>DEFL('a)"
-instance proof
+definition
+ "(liftemb :: 'a lower_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl (t::'a lower_pd itself) = u_defl\<cdot>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 \<rightarrow> 'a lower_pd)"
unfolding emb_lower_pd_def prj_lower_pd_def
using ep_pair_udom [OF lower_approx]
--- 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 \<Rightarrow> defl"})
, (@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"})
- , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::pcpo"}) ]
+ , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::pcpo"})
+ , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"})
+ , (@{const_name liftemb}, SOME @{typ "'a::pcpo u \<rightarrow> udom"})
+ , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::pcpo u"}) ]
*}
lemma typedef_rep_class:
@@ -100,8 +101,13 @@
assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)"
assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))"
assumes defl: "defl \<equiv> (\<lambda> a::'a itself. t)"
+ assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
+ assumes liftprj: "(liftprj :: udom \<rightarrow> 'a u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
+ assumes liftdefl: "(liftdefl :: 'a itself \<Rightarrow> defl) \<equiv> (\<lambda>t. u_defl\<cdot>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: "\<And>x. emb\<cdot>x = Rep x"
unfolding emb
apply (rule beta_cfun)
@@ -127,6 +133,8 @@
done
show "cast\<cdot>DEFL('a) = emb oo (prj :: udom \<rightarrow> 'a)"
by (rule cfun_eqI, simp add: defl emb_prj)
+ show "LIFTDEFL('a) = u_defl\<cdot>DEFL('a)"
+ unfolding liftdefl ..
qed
lemma typedef_DEFL:
@@ -134,13 +142,21 @@
shows "DEFL('a::pcpo) = t"
unfolding assms ..
+lemma typedef_LIFTDEFL:
+ assumes "liftdefl \<equiv> (\<lambda>a::'a::pcpo itself. u_defl\<cdot>DEFL('a))"
+ shows "LIFTDEFL('a::pcpo) = u_defl\<cdot>DEFL('a)"
+unfolding assms ..
+
text {* Restore original typing constraints. *}
setup {*
fold Sign.add_const_constraint
[ (@{const_name defl}, SOME @{typ "'a::bifinite itself \<Rightarrow> defl"})
, (@{const_name emb}, SOME @{typ "'a::bifinite \<rightarrow> udom"})
- , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::bifinite"}) ]
+ , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::bifinite"})
+ , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> defl"})
+ , (@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom"})
+ , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::predomain u"}) ]
*}
use "Tools/repdef.ML"
@@ -177,6 +193,11 @@
lemma isodefl_ID_DEFL: "isodefl (ID :: 'a \<rightarrow> 'a) DEFL('a)"
unfolding isodefl_def by (simp add: cast_DEFL)
+lemma isodefl_LIFTDEFL:
+ "isodefl (u_map\<cdot>(ID :: 'a \<rightarrow> 'a)) LIFTDEFL('a::predomain)"
+unfolding u_map_ID DEFL_u [symmetric]
+by (rule isodefl_ID_DEFL)
+
lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) DEFL('a) \<Longrightarrow> d = ID"
unfolding isodefl_def
apply (simp add: cast_DEFL)
@@ -256,13 +277,45 @@
done
lemma isodefl_u:
- "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
+ assumes "(liftemb :: 'a u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+ assumes "(liftprj :: udom \<rightarrow> 'a u) = u_map\<cdot>prj oo udom_prj u_approx"
+ shows "isodefl (d :: 'a \<rightarrow> 'a) t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>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\<cdot>d) (u_defl\<cdot>t)"
+ shows "isodefl (u_map\<cdot>(u_map\<cdot>d)) (u_defl\<cdot>(u_defl\<cdot>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\<cdot>(cfun_map\<cdot>d1\<cdot>d2)) (u_defl\<cdot>(cfun_defl\<cdot>t1\<cdot>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\<cdot>(cprod_map\<cdot>d1\<cdot>d2)) (u_defl\<cdot>(prod_defl\<cdot>t1\<cdot>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\<cdot>(sprod_map\<cdot>d1\<cdot>d2)) (u_defl\<cdot>(sprod_defl\<cdot>t1\<cdot>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\<cdot>(ssum_map\<cdot>d1\<cdot>d2)) (u_defl\<cdot>(ssum_defl\<cdot>t1\<cdot>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
--- 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;
--- 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
--- 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\<cdot>DEFL('a)"
-instance proof
+definition
+ "(liftemb :: 'a upper_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl (t::'a upper_pd itself) = u_defl\<cdot>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 \<rightarrow> 'a upper_pd)"
unfolding emb_upper_pd_def prj_upper_pd_def
using ep_pair_udom [OF upper_approx]
--- 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 \<rightarrow> tr")
and 'a baz = Baz (lazy "'a foo convex_pd \<rightarrow> tr")
+TODO: add another type parameter that is strict,
+to show the different handling of LIFTDEFL vs. DEFL.
+
*)
(********************************************************************)
@@ -32,13 +33,13 @@
"defl \<rightarrow> defl \<times> defl \<times> defl \<rightarrow> defl \<times> defl \<times> defl"
where
"foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3).
- ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t2))
+ ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>t2))
, u_defl\<cdot>(cfun_defl\<cdot>t3\<cdot>DEFL(tr))
, u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>t1)\<cdot>DEFL(tr)))))"
lemma foo_bar_baz_deflF_beta:
"foo_bar_baz_deflF\<cdot>a\<cdot>t =
- ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(fst (snd t))))
+ ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>(fst (snd t))))
, u_defl\<cdot>(cfun_defl\<cdot>(snd (snd t))\<cdot>DEFL(tr))
, u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(fst t))\<cdot>DEFL(tr)))"
unfolding foo_bar_baz_deflF_def
@@ -64,7 +65,7 @@
text {* Unfold rules for each combinator. *}
lemma foo_defl_unfold:
- "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
+ "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(baz_defl\<cdot>a)\<cdot>DEFL(tr))"
@@ -82,13 +83,13 @@
text {* Use @{text pcpodef} with the appropriate type combinator. *}
-pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>DEFL('a))"
+pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>LIFTDEFL('a))"
by (rule defl_set_bottom, rule adm_defl_set)
-pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>DEFL('a))"
+pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>LIFTDEFL('a))"
by (rule defl_set_bottom, rule adm_defl_set)
-pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>DEFL('a))"
+pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>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 \<equiv> (\<Lambda> x. Rep_foo x)"
definition prj_foo :: "udom \<rightarrow> 'a foo"
-where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>DEFL('a))\<cdot>y))"
+where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
definition defl_foo :: "'a foo itself \<Rightarrow> defl"
-where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>DEFL('a)"
+where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>LIFTDEFL('a)"
+
+definition
+ "(liftemb :: 'a foo u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> 'a foo u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl \<equiv> \<lambda>(t::'a foo itself). u_defl\<cdot>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 \<equiv> (\<Lambda> x. Rep_bar x)"
definition prj_bar :: "udom \<rightarrow> 'a bar"
-where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>DEFL('a))\<cdot>y))"
+where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
definition defl_bar :: "'a bar itself \<Rightarrow> defl"
-where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>DEFL('a)"
+where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>LIFTDEFL('a)"
+
+definition
+ "(liftemb :: 'a bar u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> 'a bar u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl \<equiv> \<lambda>(t::'a bar itself). u_defl\<cdot>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 \<equiv> (\<Lambda> x. Rep_baz x)"
definition prj_baz :: "udom \<rightarrow> 'a baz"
-where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>DEFL('a))\<cdot>y))"
+where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
definition defl_baz :: "'a baz itself \<Rightarrow> defl"
-where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>DEFL('a)"
+where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>LIFTDEFL('a)"
+
+definition
+ "(liftemb :: 'a baz u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> 'a baz u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl \<equiv> \<lambda>(t::'a baz itself). u_defl\<cdot>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\<cdot>DEFL('a)"
+lemma DEFL_foo: "DEFL('a foo) = foo_defl\<cdot>LIFTDEFL('a)"
apply (rule typedef_DEFL)
apply (rule defl_foo_def)
done
-lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>DEFL('a)"
+lemma LIFTDEFL_foo [domain_defl_simps]:
+ "LIFTDEFL('a foo) = u_defl\<cdot>DEFL('a foo)"
+apply (rule typedef_LIFTDEFL)
+apply (rule liftdefl_foo_def)
+done
+
+lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>LIFTDEFL('a)"
apply (rule typedef_DEFL)
apply (rule defl_bar_def)
done
-lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>DEFL('a)"
+lemma LIFTDEFL_bar [domain_defl_simps]:
+ "LIFTDEFL('a bar) = u_defl\<cdot>DEFL('a bar)"
+apply (rule typedef_LIFTDEFL)
+apply (rule liftdefl_bar_def)
+done
+
+lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>LIFTDEFL('a)"
apply (rule typedef_DEFL)
apply (rule defl_baz_def)
done
+lemma LIFTDEFL_baz [domain_defl_simps]:
+ "LIFTDEFL('a baz) = u_defl\<cdot>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 \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
-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 \<rightarrow> tr)\<^sub>\<bottom>)"
-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 \<rightarrow> tr)\<^sub>\<bottom>)"
-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 \<Longrightarrow> 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 \<rightarrow> _) t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>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 \<rightarrow> _) t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>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 \<rightarrow> _) t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>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\<cdot>d) t"
shows
"isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and>
isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and>
@@ -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\<cdot>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\<cdot>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
(********************************************************************)