use deflations over type 'udom u' to represent predomains;
removed now-unnecessary class liftdomain;
--- a/src/HOL/HOLCF/Domain.thy Sun Dec 19 10:33:46 2010 -0800
+++ b/src/HOL/HOLCF/Domain.thy Sun Dec 19 17:37:19 2010 -0800
@@ -89,12 +89,12 @@
[ (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> udom 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> udom defl"})
- , (@{const_name liftemb}, SOME @{typ "'a::pcpo u \<rightarrow> udom"})
- , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::pcpo u"}) ]
+ , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \<Rightarrow> udom u defl"})
+ , (@{const_name liftemb}, SOME @{typ "'a::pcpo u \<rightarrow> udom u"})
+ , (@{const_name liftprj}, SOME @{typ "udom u \<rightarrow> 'a::pcpo u"}) ]
*}
-lemma typedef_liftdomain_class:
+lemma typedef_domain_class:
fixes Rep :: "'a::pcpo \<Rightarrow> udom"
fixes Abs :: "udom \<Rightarrow> 'a::pcpo"
fixes t :: "udom defl"
@@ -103,13 +103,11 @@
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> u_emb oo u_map\<cdot>emb"
- assumes liftprj: "(liftprj :: udom \<rightarrow> 'a u) \<equiv> u_map\<cdot>prj oo u_prj"
- assumes liftdefl: "(liftdefl :: 'a itself \<Rightarrow> _) \<equiv> (\<lambda>t. u_defl\<cdot>DEFL('a))"
- shows "OFCLASS('a, liftdomain_class)"
-using liftemb [THEN meta_eq_to_obj_eq]
-using liftprj [THEN meta_eq_to_obj_eq]
-proof (rule liftdomain_class_intro)
+ assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom u) \<equiv> u_map\<cdot>emb"
+ assumes liftprj: "(liftprj :: udom u \<rightarrow> 'a u) \<equiv> u_map\<cdot>prj"
+ assumes liftdefl: "(liftdefl :: 'a itself \<Rightarrow> _) \<equiv> (\<lambda>t. pdefl\<cdot>DEFL('a))"
+ shows "OFCLASS('a, domain_class)"
+proof
have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
unfolding emb
apply (rule beta_cfun)
@@ -135,9 +133,7 @@
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
+qed (simp_all only: liftemb liftprj liftdefl)
lemma typedef_DEFL:
assumes "defl \<equiv> (\<lambda>a::'a::pcpo itself. t)"
@@ -151,19 +147,20 @@
[ (@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> udom defl"})
, (@{const_name emb}, SOME @{typ "'a::domain \<rightarrow> udom"})
, (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::domain"})
- , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> udom defl"})
- , (@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom"})
- , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::predomain u"}) ]
+ , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> udom u defl"})
+ , (@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom u"})
+ , (@{const_name liftprj}, SOME @{typ "udom u \<rightarrow> 'a::predomain u"}) ]
*}
use "Tools/domaindef.ML"
subsection {* Isomorphic deflations *}
-definition
- isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> udom defl \<Rightarrow> bool"
-where
- "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
+definition isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> udom defl \<Rightarrow> bool"
+ where "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
+
+definition isodefl' :: "('a::predomain \<rightarrow> 'a) \<Rightarrow> udom u defl \<Rightarrow> bool"
+ where "isodefl' d t \<longleftrightarrow> cast\<cdot>t = liftemb oo u_map\<cdot>d oo liftprj"
lemma isodeflI: "(\<And>x. cast\<cdot>t\<cdot>x = emb\<cdot>(d\<cdot>(prj\<cdot>x))) \<Longrightarrow> isodefl d t"
unfolding isodefl_def by (simp add: cfun_eqI)
@@ -191,9 +188,8 @@
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)
+ "isodefl' (ID :: 'a \<rightarrow> 'a) LIFTDEFL('a::predomain)"
+unfolding isodefl'_def by (simp add: cast_liftdefl u_map_ID)
lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) DEFL('a) \<Longrightarrow> d = ID"
unfolding isodefl_def
@@ -237,6 +233,10 @@
unfolding isodefl_def
by (simp add: cfun_eq_iff assms prj_emb_prj emb_prj_emb)
+lemma isodefl'_pdefl: "isodefl d t \<Longrightarrow> isodefl' d (pdefl\<cdot>t)"
+unfolding isodefl_def isodefl'_def
+by (simp add: cast_pdefl u_map_oo liftemb_eq liftprj_eq)
+
lemma isodefl_sfun:
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)"
@@ -274,12 +274,10 @@
done
lemma isodefl_u:
- fixes d :: "'a::liftdomain \<rightarrow> 'a"
- shows "isodefl (d :: 'a \<rightarrow> 'a) t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
+ "isodefl' d 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: cast_u_defl isodefl'_def)
apply (simp add: emb_u_def prj_u_def liftemb_eq liftprj_eq)
-apply (simp add: u_map_map)
done
lemma encode_prod_u_map:
@@ -291,11 +289,11 @@
done
lemma isodefl_cprod_u:
- assumes "isodefl (u_map\<cdot>d1) t1" and "isodefl (u_map\<cdot>d2) t2"
- shows "isodefl (u_map\<cdot>(cprod_map\<cdot>d1\<cdot>d2)) (sprod_defl\<cdot>t1\<cdot>t2)"
-using isodefl_sprod [OF assms] unfolding isodefl_def
-unfolding emb_u_def prj_u_def liftemb_prod_def liftprj_prod_def
-by (simp add: cfcomp1 encode_prod_u_map)
+ assumes "isodefl' d1 t1" and "isodefl' d2 t2"
+ shows "isodefl' (cprod_map\<cdot>d1\<cdot>d2) (prod_liftdefl\<cdot>t1\<cdot>t2)"
+using assms unfolding isodefl'_def
+unfolding liftemb_prod_def liftprj_prod_def
+by (simp add: cast_prod_liftdefl cfcomp1 encode_prod_u_map sprod_map_map)
lemma encode_cfun_map:
"encode_cfun\<cdot>(cfun_map\<cdot>f\<cdot>g\<cdot>(decode_cfun\<cdot>x))
@@ -328,7 +326,7 @@
lemmas [domain_isodefl] =
isodefl_u isodefl_sfun isodefl_ssum isodefl_sprod
- isodefl_cfun isodefl_cprod isodefl_cprod_u
+ isodefl_cfun isodefl_cprod isodefl_cprod_u isodefl'_pdefl
lemmas [domain_deflation] =
deflation_cfun_map deflation_sfun_map deflation_ssum_map
--- a/src/HOL/HOLCF/Library/Bool_Discrete.thy Sun Dec 19 10:33:46 2010 -0800
+++ b/src/HOL/HOLCF/Library/Bool_Discrete.thy Sun Dec 19 17:37:19 2010 -0800
@@ -29,23 +29,23 @@
begin
definition
- "(liftemb :: bool u \<rightarrow> udom) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
+ "(liftemb :: bool u \<rightarrow> udom u) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
definition
- "(liftprj :: udom \<rightarrow> bool u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
+ "(liftprj :: udom u \<rightarrow> bool u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
definition
"liftdefl \<equiv> (\<lambda>(t::bool itself). LIFTDEFL(bool discr))"
instance proof
- show "ep_pair liftemb (liftprj :: udom \<rightarrow> bool u)"
+ show "ep_pair liftemb (liftprj :: udom u \<rightarrow> bool u)"
unfolding liftemb_bool_def liftprj_bool_def
apply (rule ep_pair_comp)
apply (rule ep_pair_u_map)
apply (simp add: ep_pair.intro)
apply (rule predomain_ep)
done
- show "cast\<cdot>LIFTDEFL(bool) = liftemb oo (liftprj :: udom \<rightarrow> bool u)"
+ show "cast\<cdot>LIFTDEFL(bool) = liftemb oo (liftprj :: udom u \<rightarrow> bool u)"
unfolding liftemb_bool_def liftprj_bool_def liftdefl_bool_def
apply (simp add: cast_liftdefl cfcomp1 u_map_map)
apply (simp add: ID_def [symmetric] u_map_ID)
--- a/src/HOL/HOLCF/Library/Char_Discrete.thy Sun Dec 19 10:33:46 2010 -0800
+++ b/src/HOL/HOLCF/Library/Char_Discrete.thy Sun Dec 19 17:37:19 2010 -0800
@@ -29,23 +29,23 @@
begin
definition
- "(liftemb :: nibble u \<rightarrow> udom) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
+ "(liftemb :: nibble u \<rightarrow> udom u) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
definition
- "(liftprj :: udom \<rightarrow> nibble u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
+ "(liftprj :: udom u \<rightarrow> nibble u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
definition
"liftdefl \<equiv> (\<lambda>(t::nibble itself). LIFTDEFL(nibble discr))"
instance proof
- show "ep_pair liftemb (liftprj :: udom \<rightarrow> nibble u)"
+ show "ep_pair liftemb (liftprj :: udom u \<rightarrow> nibble u)"
unfolding liftemb_nibble_def liftprj_nibble_def
apply (rule ep_pair_comp)
apply (rule ep_pair_u_map)
apply (simp add: ep_pair.intro)
apply (rule predomain_ep)
done
- show "cast\<cdot>LIFTDEFL(nibble) = liftemb oo (liftprj :: udom \<rightarrow> nibble u)"
+ show "cast\<cdot>LIFTDEFL(nibble) = liftemb oo (liftprj :: udom u \<rightarrow> nibble u)"
unfolding liftemb_nibble_def liftprj_nibble_def liftdefl_nibble_def
apply (simp add: cast_liftdefl cfcomp1 u_map_map)
apply (simp add: ID_def [symmetric] u_map_ID)
@@ -75,23 +75,23 @@
begin
definition
- "(liftemb :: char u \<rightarrow> udom) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
+ "(liftemb :: char u \<rightarrow> udom u) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
definition
- "(liftprj :: udom \<rightarrow> char u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
+ "(liftprj :: udom u \<rightarrow> char u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
definition
"liftdefl \<equiv> (\<lambda>(t::char itself). LIFTDEFL(char discr))"
instance proof
- show "ep_pair liftemb (liftprj :: udom \<rightarrow> char u)"
+ show "ep_pair liftemb (liftprj :: udom u \<rightarrow> char u)"
unfolding liftemb_char_def liftprj_char_def
apply (rule ep_pair_comp)
apply (rule ep_pair_u_map)
apply (simp add: ep_pair.intro)
apply (rule predomain_ep)
done
- show "cast\<cdot>LIFTDEFL(char) = liftemb oo (liftprj :: udom \<rightarrow> char u)"
+ show "cast\<cdot>LIFTDEFL(char) = liftemb oo (liftprj :: udom u \<rightarrow> char u)"
unfolding liftemb_char_def liftprj_char_def liftdefl_char_def
apply (simp add: cast_liftdefl cfcomp1 u_map_map)
apply (simp add: ID_def [symmetric] u_map_ID)
--- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy Sun Dec 19 10:33:46 2010 -0800
+++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy Sun Dec 19 17:37:19 2010 -0800
@@ -637,7 +637,7 @@
apply (rule someI_ex [OF bifinite])
done
-instantiation defl :: (bifinite) liftdomain
+instantiation defl :: (bifinite) "domain"
begin
definition
@@ -651,17 +651,15 @@
(\<Squnion>i. defl_principal (Abs_fin_defl (emb oo defl_approx i oo prj)))"
definition
- "(liftemb :: 'a defl u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
-
-definition
- "(liftprj :: udom \<rightarrow> 'a defl u) = u_map\<cdot>prj oo u_prj"
+ "(liftemb :: 'a defl u \<rightarrow> udom u) = u_map\<cdot>emb"
definition
- "liftdefl (t::'a defl itself) = u_defl\<cdot>DEFL('a defl)"
+ "(liftprj :: udom u \<rightarrow> 'a defl u) = u_map\<cdot>prj"
-instance
-using liftemb_defl_def liftprj_defl_def liftdefl_defl_def
-proof (rule liftdomain_class_intro)
+definition
+ "liftdefl (t::'a defl itself) = pdefl\<cdot>DEFL('a defl)"
+
+instance proof
show ep: "ep_pair emb (prj :: udom \<rightarrow> 'a defl)"
unfolding emb_defl_def prj_defl_def
by (rule ep_pair_udom [OF defl_approx])
@@ -682,7 +680,7 @@
apply (simp add: lub_distribs approx_chain.chain_approx [OF defl_approx]
approx_chain.lub_approx [OF defl_approx])
done
-qed
+qed (fact liftemb_defl_def liftprj_defl_def liftdefl_defl_def)+
end
--- a/src/HOL/HOLCF/Library/Int_Discrete.thy Sun Dec 19 10:33:46 2010 -0800
+++ b/src/HOL/HOLCF/Library/Int_Discrete.thy Sun Dec 19 17:37:19 2010 -0800
@@ -29,23 +29,23 @@
begin
definition
- "(liftemb :: int u \<rightarrow> udom) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
+ "(liftemb :: int u \<rightarrow> udom u) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
definition
- "(liftprj :: udom \<rightarrow> int u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
+ "(liftprj :: udom u \<rightarrow> int u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
definition
"liftdefl \<equiv> (\<lambda>(t::int itself). LIFTDEFL(int discr))"
instance proof
- show "ep_pair liftemb (liftprj :: udom \<rightarrow> int u)"
+ show "ep_pair liftemb (liftprj :: udom u \<rightarrow> int u)"
unfolding liftemb_int_def liftprj_int_def
apply (rule ep_pair_comp)
apply (rule ep_pair_u_map)
apply (simp add: ep_pair.intro)
apply (rule predomain_ep)
done
- show "cast\<cdot>LIFTDEFL(int) = liftemb oo (liftprj :: udom \<rightarrow> int u)"
+ show "cast\<cdot>LIFTDEFL(int) = liftemb oo (liftprj :: udom u \<rightarrow> int u)"
unfolding liftemb_int_def liftprj_int_def liftdefl_int_def
apply (simp add: cast_liftdefl cfcomp1 u_map_map)
apply (simp add: ID_def [symmetric] u_map_ID)
--- a/src/HOL/HOLCF/Library/List_Predomain.thy Sun Dec 19 10:33:46 2010 -0800
+++ b/src/HOL/HOLCF/Library/List_Predomain.thy Sun Dec 19 17:37:19 2010 -0800
@@ -5,13 +5,61 @@
header {* Predomain class instance for HOL list type *}
theory List_Predomain
-imports List_Cpo
+imports List_Cpo Sum_Cpo
begin
subsection {* Strict list type *}
domain 'a slist = SNil | SCons "'a" "'a slist"
+text {* Polymorphic map function for strict lists. *}
+
+text {* FIXME: The domain package should generate this! *}
+
+fixrec slist_map' :: "('a \<rightarrow> 'b) \<rightarrow> 'a slist \<rightarrow> 'b slist"
+ where "slist_map'\<cdot>f\<cdot>SNil = SNil"
+ | "\<lbrakk>x \<noteq> \<bottom>; xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow>
+ slist_map'\<cdot>f\<cdot>(SCons\<cdot>x\<cdot>xs) = SCons\<cdot>(f\<cdot>x)\<cdot>(slist_map'\<cdot>f\<cdot>xs)"
+
+lemma slist_map'_strict [simp]: "slist_map'\<cdot>f\<cdot>\<bottom> = \<bottom>"
+by fixrec_simp
+
+lemma slist_map_conv [simp]: "slist_map = slist_map'"
+apply (rule cfun_eqI, rule cfun_eqI, rename_tac f xs)
+apply (induct_tac xs, simp_all)
+apply (subst slist_map_unfold, simp)
+apply (subst slist_map_unfold, simp add: SNil_def)
+apply (subst slist_map_unfold, simp add: SCons_def)
+done
+
+lemma slist_map'_slist_map':
+ "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> slist_map'\<cdot>f\<cdot>(slist_map'\<cdot>g\<cdot>xs) = slist_map'\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
+apply (induct xs, simp, simp)
+apply (case_tac "g\<cdot>a = \<bottom>", simp, simp)
+apply (case_tac "slist_map'\<cdot>g\<cdot>xs = \<bottom>", simp, simp)
+done
+
+lemma slist_map'_oo:
+ "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> slist_map'\<cdot>(f oo g) = slist_map'\<cdot>f oo slist_map'\<cdot>g"
+by (simp add: cfcomp1 slist_map'_slist_map' eta_cfun)
+
+lemma slist_map'_ID: "slist_map'\<cdot>ID = ID"
+by (rule cfun_eqI, induct_tac x, simp_all)
+
+lemma ep_pair_slist_map':
+ "ep_pair e p \<Longrightarrow> ep_pair (slist_map'\<cdot>e) (slist_map'\<cdot>p)"
+apply (rule ep_pair.intro)
+apply (subst slist_map'_slist_map')
+apply (erule pcpo_ep_pair.p_strict [unfolded pcpo_ep_pair_def])
+apply (simp add: ep_pair.e_inverse ID_def [symmetric] slist_map'_ID)
+apply (subst slist_map'_slist_map')
+apply (erule pcpo_ep_pair.e_strict [unfolded pcpo_ep_pair_def])
+apply (rule below_eq_trans [OF _ ID1])
+apply (subst slist_map'_ID [symmetric])
+apply (intro monofun_cfun below_refl)
+apply (simp add: cfun_below_iff ep_pair.e_p_below)
+done
+
text {*
Types @{typ "'a list u"}. and @{typ "'a u slist"} are isomorphic.
*}
@@ -48,34 +96,52 @@
subsection {* Lists are a predomain *}
+definition udefl :: "udom defl \<rightarrow> udom u defl"
+ where "udefl = defl_fun1 (strictify\<cdot>up) (fup\<cdot>ID) ID"
+
+lemma cast_udefl:
+ "cast\<cdot>(udefl\<cdot>t) = strictify\<cdot>up oo cast\<cdot>t oo fup\<cdot>ID"
+unfolding udefl_def by (simp add: cast_defl_fun1 ep_pair_strictify_up)
+
+definition list_liftdefl :: "udom u defl \<rightarrow> udom u defl"
+ where "list_liftdefl = (\<Lambda> a. udefl\<cdot>(slist_defl\<cdot>(u_defl\<cdot>a)))"
+
+lemma cast_slist_defl: "cast\<cdot>(slist_defl\<cdot>a) = emb oo slist_map\<cdot>(cast\<cdot>a) oo prj"
+using isodefl_slist [where fa="cast\<cdot>a" and da="a"]
+unfolding isodefl_def by simp
+
+lemma u_emb_bottom: "u_emb\<cdot>\<bottom> = \<bottom>"
+by (rule pcpo_ep_pair.e_strict [unfolded pcpo_ep_pair_def, OF ep_pair_u])
+
instantiation list :: (predomain) predomain
begin
definition
- "liftemb = emb oo encode_list_u"
+ "liftemb = (strictify\<cdot>up oo emb oo slist_map'\<cdot>u_emb) oo slist_map'\<cdot>liftemb oo encode_list_u"
definition
- "liftprj = decode_list_u oo prj"
+ "liftprj = (decode_list_u oo slist_map'\<cdot>liftprj) oo (slist_map'\<cdot>u_prj oo prj) oo fup\<cdot>ID"
definition
- "liftdefl (t::('a list) itself) = DEFL(('a\<^sub>\<bottom>) slist)"
+ "liftdefl (t::('a list) itself) = list_liftdefl\<cdot>LIFTDEFL('a)"
instance proof
- have "ep_pair encode_list_u decode_list_u"
- by (rule ep_pair.intro, simp_all)
- thus "ep_pair liftemb (liftprj :: udom \<rightarrow> ('a list) u)"
+ show "ep_pair liftemb (liftprj :: udom u \<rightarrow> ('a list) u)"
unfolding liftemb_list_def liftprj_list_def
- using ep_pair_emb_prj by (rule ep_pair_comp)
- show "cast\<cdot>LIFTDEFL('a list) = liftemb oo (liftprj :: udom \<rightarrow> ('a list) u)"
+ by (intro ep_pair_comp ep_pair_slist_map' ep_pair_strictify_up
+ ep_pair_emb_prj predomain_ep ep_pair_u, simp add: ep_pair.intro)
+ show "cast\<cdot>LIFTDEFL('a list) = liftemb oo (liftprj :: udom u \<rightarrow> ('a list) u)"
unfolding liftemb_list_def liftprj_list_def liftdefl_list_def
- by (simp add: cfcomp1 cast_DEFL)
+ apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_defl cast_liftdefl)
+ apply (simp add: slist_map'_oo u_emb_bottom cfun_eq_iff)
+ done
qed
end
lemma liftdefl_list [domain_defl_simps]:
- "LIFTDEFL('a::predomain list) = slist_defl\<cdot>LIFTDEFL('a)"
-unfolding liftdefl_list_def by (simp add: domain_defl_simps)
+ "LIFTDEFL('a::predomain list) = list_liftdefl\<cdot>LIFTDEFL('a)"
+by (rule liftdefl_list_def)
subsection {* Continuous map operation for lists *}
@@ -105,21 +171,21 @@
lemma encode_list_u_map:
"encode_list_u\<cdot>(u_map\<cdot>(list_map\<cdot>f)\<cdot>(decode_list_u\<cdot>xs))
= slist_map\<cdot>(u_map\<cdot>f)\<cdot>xs"
-apply (induct xs)
-apply (simp, subst slist_map_unfold, simp)
-apply (simp, subst slist_map_unfold, simp add: SNil_def)
+apply (induct xs, simp, simp)
apply (case_tac a, simp, rename_tac b)
apply (case_tac "decode_list_u\<cdot>xs")
-apply (drule_tac f="encode_list_u" in cfun_arg_cong, simp)
-by (simp, subst slist_map_unfold, simp add: SCons_def)
+apply (drule_tac f="encode_list_u" in cfun_arg_cong, simp, simp)
+done
lemma isodefl_list_u [domain_isodefl]:
fixes d :: "'a::predomain \<rightarrow> 'a"
- assumes "isodefl (u_map\<cdot>d) t"
- shows "isodefl (u_map\<cdot>(list_map\<cdot>d)) (slist_defl\<cdot>t)"
-using assms [THEN isodefl_slist] unfolding isodefl_def
-unfolding emb_u_def prj_u_def liftemb_list_def liftprj_list_def
-by (simp add: cfcomp1 encode_list_u_map)
+ assumes "isodefl' d t"
+ shows "isodefl' (list_map\<cdot>d) (list_liftdefl\<cdot>t)"
+using assms unfolding isodefl'_def liftemb_list_def liftprj_list_def
+apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_defl)
+apply (simp add: cfcomp1 encode_list_u_map)
+apply (simp add: slist_map'_slist_map' u_emb_bottom)
+done
setup {*
Domain_Take_Proofs.add_rec_type (@{type_name "list"}, [true])
--- a/src/HOL/HOLCF/Library/Nat_Discrete.thy Sun Dec 19 10:33:46 2010 -0800
+++ b/src/HOL/HOLCF/Library/Nat_Discrete.thy Sun Dec 19 17:37:19 2010 -0800
@@ -29,23 +29,23 @@
begin
definition
- "(liftemb :: nat u \<rightarrow> udom) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
+ "(liftemb :: nat u \<rightarrow> udom u) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
definition
- "(liftprj :: udom \<rightarrow> nat u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
+ "(liftprj :: udom u \<rightarrow> nat u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
definition
"liftdefl \<equiv> (\<lambda>(t::nat itself). LIFTDEFL(nat discr))"
instance proof
- show "ep_pair liftemb (liftprj :: udom \<rightarrow> nat u)"
+ show "ep_pair liftemb (liftprj :: udom u \<rightarrow> nat u)"
unfolding liftemb_nat_def liftprj_nat_def
apply (rule ep_pair_comp)
apply (rule ep_pair_u_map)
apply (simp add: ep_pair.intro)
apply (rule predomain_ep)
done
- show "cast\<cdot>LIFTDEFL(nat) = liftemb oo (liftprj :: udom \<rightarrow> nat u)"
+ show "cast\<cdot>LIFTDEFL(nat) = liftemb oo (liftprj :: udom u \<rightarrow> nat u)"
unfolding liftemb_nat_def liftprj_nat_def liftdefl_nat_def
apply (simp add: cast_liftdefl cfcomp1 u_map_map)
apply (simp add: ID_def [symmetric] u_map_ID)
--- a/src/HOL/HOLCF/Library/Option_Cpo.thy Sun Dec 19 10:33:46 2010 -0800
+++ b/src/HOL/HOLCF/Library/Option_Cpo.thy Sun Dec 19 17:37:19 2010 -0800
@@ -5,7 +5,7 @@
header {* Cpo class instance for HOL option type *}
theory Option_Cpo
-imports HOLCF
+imports HOLCF Sum_Cpo
begin
subsection {* Ordering on option type *}
@@ -209,45 +209,40 @@
subsection {* Option type is a predomain *}
definition
- "encode_option_u =
- (\<Lambda>(up\<cdot>x). case x of None \<Rightarrow> sinl\<cdot>ONE | Some a \<Rightarrow> sinr\<cdot>(up\<cdot>a))"
+ "encode_option = (\<Lambda> x. case x of None \<Rightarrow> Inl () | Some a \<Rightarrow> Inr a)"
definition
- "decode_option_u = sscase\<cdot>(\<Lambda> ONE. up\<cdot>None)\<cdot>(\<Lambda>(up\<cdot>a). up\<cdot>(Some a))"
-
-lemma decode_encode_option_u [simp]: "decode_option_u\<cdot>(encode_option_u\<cdot>x) = x"
-unfolding decode_option_u_def encode_option_u_def
-by (case_tac x, simp, rename_tac y, case_tac y, simp_all)
+ "decode_option = (\<Lambda> x. case x of Inl (u::unit) \<Rightarrow> None | Inr a \<Rightarrow> Some a)"
-lemma encode_decode_option_u [simp]: "encode_option_u\<cdot>(decode_option_u\<cdot>x) = x"
-unfolding decode_option_u_def encode_option_u_def
-apply (case_tac x, simp)
-apply (rename_tac a, case_tac a rule: oneE, simp, simp)
-apply (rename_tac b, case_tac b, simp, simp)
-done
+lemma decode_encode_option [simp]: "decode_option\<cdot>(encode_option\<cdot>x) = x"
+unfolding decode_option_def encode_option_def
+by (cases x, simp_all)
+
+lemma encode_decode_option [simp]: "encode_option\<cdot>(decode_option\<cdot>x) = x"
+unfolding decode_option_def encode_option_def
+by (cases x, simp_all)
instantiation option :: (predomain) predomain
begin
definition
- "liftemb = emb oo encode_option_u"
+ "liftemb = liftemb oo u_map\<cdot>encode_option"
definition
- "liftprj = decode_option_u oo prj"
+ "liftprj = u_map\<cdot>decode_option oo liftprj"
definition
- "liftdefl (t::('a option) itself) = DEFL(one \<oplus> 'a u)"
+ "liftdefl (t::('a option) itself) = LIFTDEFL(unit + 'a)"
instance proof
- show "ep_pair liftemb (liftprj :: udom \<rightarrow> ('a option) u)"
+ show "ep_pair liftemb (liftprj :: udom u \<rightarrow> ('a option) u)"
unfolding liftemb_option_def liftprj_option_def
- apply (rule ep_pair_comp)
+ apply (intro ep_pair_comp ep_pair_u_map predomain_ep)
apply (rule ep_pair.intro, simp, simp)
- apply (rule ep_pair_emb_prj)
done
- show "cast\<cdot>LIFTDEFL('a option) = liftemb oo (liftprj :: udom \<rightarrow> ('a option) u)"
+ show "cast\<cdot>LIFTDEFL('a option) = liftemb oo (liftprj :: udom u \<rightarrow> ('a option) u)"
unfolding liftemb_option_def liftprj_option_def liftdefl_option_def
- by (simp add: cast_DEFL cfcomp1)
+ by (simp add: cast_liftdefl cfcomp1 u_map_map ID_def [symmetric] u_map_ID)
qed
end
--- a/src/HOL/HOLCF/Library/Sum_Cpo.thy Sun Dec 19 10:33:46 2010 -0800
+++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy Sun Dec 19 17:37:19 2010 -0800
@@ -260,28 +260,43 @@
apply (rename_tac b, case_tac b, simp, simp)
done
+lemma ep_pair_strictify_up:
+ "ep_pair (strictify\<cdot>up) (fup\<cdot>ID)"
+apply (rule ep_pair.intro)
+apply (simp add: strictify_conv_if)
+apply (case_tac y, simp, simp add: strictify_conv_if)
+done
+
+definition sum_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl"
+ where "sum_liftdefl = defl_fun2 (u_map\<cdot>emb oo strictify\<cdot>up)
+ (fup\<cdot>ID oo u_map\<cdot>prj) ssum_map"
+
instantiation sum :: (predomain, predomain) predomain
begin
definition
- "liftemb = emb oo encode_sum_u"
+ "liftemb = (u_map\<cdot>emb oo strictify\<cdot>up) oo
+ (ssum_map\<cdot>liftemb\<cdot>liftemb oo encode_sum_u)"
definition
- "liftprj = decode_sum_u oo prj"
+ "liftprj = (decode_sum_u oo ssum_map\<cdot>liftprj\<cdot>liftprj) oo
+ (fup\<cdot>ID oo u_map\<cdot>prj)"
definition
- "liftdefl (t::('a + 'b) itself) = DEFL('a u \<oplus> 'b u)"
+ "liftdefl (t::('a + 'b) itself) = sum_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
instance proof
- show "ep_pair liftemb (liftprj :: udom \<rightarrow> ('a + 'b) u)"
+ show "ep_pair liftemb (liftprj :: udom u \<rightarrow> ('a + 'b) u)"
unfolding liftemb_sum_def liftprj_sum_def
- apply (rule ep_pair_comp)
- apply (rule ep_pair.intro, simp, simp)
- apply (rule ep_pair_emb_prj)
- done
- show "cast\<cdot>LIFTDEFL('a + 'b) = liftemb oo (liftprj :: udom \<rightarrow> ('a + 'b) u)"
+ by (intro ep_pair_comp ep_pair_ssum_map ep_pair_u_map ep_pair_emb_prj
+ ep_pair_strictify_up predomain_ep, simp add: ep_pair.intro)
+ show "cast\<cdot>LIFTDEFL('a + 'b) = liftemb oo (liftprj :: udom u \<rightarrow> ('a + 'b) u)"
unfolding liftemb_sum_def liftprj_sum_def liftdefl_sum_def
- by (simp add: cast_DEFL cfcomp1)
+ apply (subst sum_liftdefl_def, subst cast_defl_fun2)
+ apply (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj
+ ep_pair_strictify_up)
+ apply (erule (1) finite_deflation_ssum_map)
+ by (simp add: cast_liftdefl cfcomp1 ssum_map_map)
qed
end
--- a/src/HOL/HOLCF/Powerdomains.thy Sun Dec 19 10:33:46 2010 -0800
+++ b/src/HOL/HOLCF/Powerdomains.thy Sun Dec 19 17:37:19 2010 -0800
@@ -59,7 +59,7 @@
subsection {* Domain class instances *}
-instantiation upper_pd :: ("domain") liftdomain
+instantiation upper_pd :: ("domain") "domain"
begin
definition
@@ -72,17 +72,15 @@
"defl (t::'a upper_pd itself) = upper_defl\<cdot>DEFL('a)"
definition
- "(liftemb :: 'a upper_pd u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
-
-definition
- "(liftprj :: udom \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj oo u_prj"
+ "(liftemb :: 'a upper_pd u \<rightarrow> udom u) = u_map\<cdot>emb"
definition
- "liftdefl (t::'a upper_pd itself) = u_defl\<cdot>DEFL('a upper_pd)"
+ "(liftprj :: udom u \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj"
-instance
-using liftemb_upper_pd_def liftprj_upper_pd_def liftdefl_upper_pd_def
-proof (rule liftdomain_class_intro)
+definition
+ "liftdefl (t::'a upper_pd itself) = pdefl\<cdot>DEFL('a upper_pd)"
+
+instance proof
show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)"
unfolding emb_upper_pd_def prj_upper_pd_def
by (intro ep_pair_comp ep_pair_upper ep_pair_upper_map ep_pair_emb_prj)
@@ -90,11 +88,11 @@
show "cast\<cdot>DEFL('a upper_pd) = emb oo (prj :: udom \<rightarrow> 'a upper_pd)"
unfolding emb_upper_pd_def prj_upper_pd_def defl_upper_pd_def cast_upper_defl
by (simp add: cast_DEFL oo_def cfun_eq_iff upper_map_map)
-qed
+qed (fact liftemb_upper_pd_def liftprj_upper_pd_def liftdefl_upper_pd_def)+
end
-instantiation lower_pd :: ("domain") liftdomain
+instantiation lower_pd :: ("domain") "domain"
begin
definition
@@ -107,17 +105,15 @@
"defl (t::'a lower_pd itself) = lower_defl\<cdot>DEFL('a)"
definition
- "(liftemb :: 'a lower_pd u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
-
-definition
- "(liftprj :: udom \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj oo u_prj"
+ "(liftemb :: 'a lower_pd u \<rightarrow> udom u) = u_map\<cdot>emb"
definition
- "liftdefl (t::'a lower_pd itself) = u_defl\<cdot>DEFL('a lower_pd)"
+ "(liftprj :: udom u \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj"
-instance
-using liftemb_lower_pd_def liftprj_lower_pd_def liftdefl_lower_pd_def
-proof (rule liftdomain_class_intro)
+definition
+ "liftdefl (t::'a lower_pd itself) = pdefl\<cdot>DEFL('a lower_pd)"
+
+instance proof
show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)"
unfolding emb_lower_pd_def prj_lower_pd_def
by (intro ep_pair_comp ep_pair_lower ep_pair_lower_map ep_pair_emb_prj)
@@ -125,11 +121,11 @@
show "cast\<cdot>DEFL('a lower_pd) = emb oo (prj :: udom \<rightarrow> 'a lower_pd)"
unfolding emb_lower_pd_def prj_lower_pd_def defl_lower_pd_def cast_lower_defl
by (simp add: cast_DEFL oo_def cfun_eq_iff lower_map_map)
-qed
+qed (fact liftemb_lower_pd_def liftprj_lower_pd_def liftdefl_lower_pd_def)+
end
-instantiation convex_pd :: ("domain") liftdomain
+instantiation convex_pd :: ("domain") "domain"
begin
definition
@@ -142,17 +138,15 @@
"defl (t::'a convex_pd itself) = convex_defl\<cdot>DEFL('a)"
definition
- "(liftemb :: 'a convex_pd u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
-
-definition
- "(liftprj :: udom \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj oo u_prj"
+ "(liftemb :: 'a convex_pd u \<rightarrow> udom u) = u_map\<cdot>emb"
definition
- "liftdefl (t::'a convex_pd itself) = u_defl\<cdot>DEFL('a convex_pd)"
+ "(liftprj :: udom u \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj"
-instance
-using liftemb_convex_pd_def liftprj_convex_pd_def liftdefl_convex_pd_def
-proof (rule liftdomain_class_intro)
+definition
+ "liftdefl (t::'a convex_pd itself) = pdefl\<cdot>DEFL('a convex_pd)"
+
+instance proof
show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)"
unfolding emb_convex_pd_def prj_convex_pd_def
by (intro ep_pair_comp ep_pair_convex ep_pair_convex_map ep_pair_emb_prj)
@@ -160,7 +154,7 @@
show "cast\<cdot>DEFL('a convex_pd) = emb oo (prj :: udom \<rightarrow> 'a convex_pd)"
unfolding emb_convex_pd_def prj_convex_pd_def defl_convex_pd_def cast_convex_defl
by (simp add: cast_DEFL oo_def cfun_eq_iff convex_map_map)
-qed
+qed (fact liftemb_convex_pd_def liftprj_convex_pd_def liftdefl_convex_pd_def)+
end
--- a/src/HOL/HOLCF/Representable.thy Sun Dec 19 10:33:46 2010 -0800
+++ b/src/HOL/HOLCF/Representable.thy Sun Dec 19 17:37:19 2010 -0800
@@ -8,6 +8,8 @@
imports Algebraic Map_Functions Countable
begin
+default_sort cpo
+
subsection {* Class of representable domains *}
text {*
@@ -16,31 +18,67 @@
to being omega-bifinite.
A predomain is a cpo that, when lifted, becomes a domain.
+ Predomains are represented by deflations over a lifted universal
+ domain type.
*}
-class predomain = cpo +
- fixes liftdefl :: "('a::cpo) itself \<Rightarrow> udom defl"
- fixes liftemb :: "'a\<^sub>\<bottom> \<rightarrow> udom"
- fixes liftprj :: "udom \<rightarrow> 'a\<^sub>\<bottom>"
+class predomain_syn = cpo +
+ fixes liftemb :: "'a\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
+ fixes liftprj :: "udom\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>"
+ fixes liftdefl :: "'a itself \<Rightarrow> udom u defl"
+
+class predomain = predomain_syn +
assumes predomain_ep: "ep_pair liftemb liftprj"
- assumes cast_liftdefl: "cast\<cdot>(liftdefl TYPE('a::cpo)) = liftemb oo liftprj"
+ assumes cast_liftdefl: "cast\<cdot>(liftdefl TYPE('a)) = liftemb oo liftprj"
syntax "_LIFTDEFL" :: "type \<Rightarrow> logic" ("(1LIFTDEFL/(1'(_')))")
translations "LIFTDEFL('t)" \<rightleftharpoons> "CONST liftdefl TYPE('t)"
-class "domain" = predomain + pcpo +
- fixes emb :: "'a::cpo \<rightarrow> udom"
- fixes prj :: "udom \<rightarrow> 'a::cpo"
+definition pdefl :: "udom defl \<rightarrow> udom u defl"
+ where "pdefl = defl_fun1 ID ID u_map"
+
+lemma cast_pdefl: "cast\<cdot>(pdefl\<cdot>t) = u_map\<cdot>(cast\<cdot>t)"
+by (simp add: pdefl_def cast_defl_fun1 ep_pair_def finite_deflation_u_map)
+
+class "domain" = predomain_syn + pcpo +
+ fixes emb :: "'a \<rightarrow> udom"
+ fixes prj :: "udom \<rightarrow> 'a"
fixes defl :: "'a itself \<Rightarrow> udom defl"
assumes ep_pair_emb_prj: "ep_pair emb prj"
assumes cast_DEFL: "cast\<cdot>(defl TYPE('a)) = emb oo prj"
+ assumes liftemb_eq: "liftemb = u_map\<cdot>emb"
+ assumes liftprj_eq: "liftprj = u_map\<cdot>prj"
+ assumes liftdefl_eq: "liftdefl TYPE('a) = pdefl\<cdot>(defl TYPE('a))"
syntax "_DEFL" :: "type \<Rightarrow> logic" ("(1DEFL/(1'(_')))")
translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)"
+instance "domain" \<subseteq> predomain
+proof
+ show "ep_pair liftemb (liftprj::udom\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>)"
+ unfolding liftemb_eq liftprj_eq
+ by (intro ep_pair_u_map ep_pair_emb_prj)
+ show "cast\<cdot>LIFTDEFL('a) = liftemb oo (liftprj::udom\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>)"
+ unfolding liftemb_eq liftprj_eq liftdefl_eq
+ by (simp add: cast_pdefl cast_DEFL u_map_oo)
+qed
+
+text {*
+ Constants @{const liftemb} and @{const liftprj} imply class predomain.
+*}
+
+setup {*
+ fold Sign.add_const_constraint
+ [(@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom u"}),
+ (@{const_name liftprj}, SOME @{typ "udom u \<rightarrow> 'a::predomain u"}),
+ (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> udom u defl"})]
+*}
+
+interpretation predomain: pcpo_ep_pair liftemb liftprj
+ unfolding pcpo_ep_pair_def by (rule predomain_ep)
+
interpretation "domain": pcpo_ep_pair emb prj
- unfolding pcpo_ep_pair_def
- by (rule ep_pair_emb_prj)
+ unfolding pcpo_ep_pair_def by (rule ep_pair_emb_prj)
lemmas emb_inverse = domain.e_inverse
lemmas emb_prj_below = domain.e_p_below
@@ -51,7 +89,7 @@
subsection {* Domains are bifinite *}
lemma approx_chain_ep_cast:
- assumes ep: "ep_pair (e::'a::pcpo \<rightarrow> udom) (p::udom \<rightarrow> 'a)"
+ assumes ep: "ep_pair (e::'a::pcpo \<rightarrow> 'b::bifinite) (p::'b \<rightarrow> 'a)"
assumes cast_t: "cast\<cdot>t = e oo p"
shows "\<exists>(a::nat \<Rightarrow> 'a::pcpo \<rightarrow> 'a). approx_chain a"
proof -
@@ -125,8 +163,8 @@
subsection {* Type combinators *}
-definition u_defl :: "udom defl \<rightarrow> udom defl"
- where "u_defl = defl_fun1 u_emb u_prj u_map"
+definition u_defl :: "udom u defl \<rightarrow> udom defl"
+ where "u_defl = defl_fun1 u_emb u_prj ID"
definition prod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
where "prod_defl = defl_fun2 prod_emb prod_prj cprod_map"
@@ -141,9 +179,8 @@
where "sfun_defl = defl_fun2 sfun_emb sfun_prj sfun_map"
lemma cast_u_defl:
- "cast\<cdot>(u_defl\<cdot>A) = u_emb oo u_map\<cdot>(cast\<cdot>A) oo u_prj"
-using ep_pair_u finite_deflation_u_map
-unfolding u_defl_def by (rule cast_defl_fun1)
+ "cast\<cdot>(u_defl\<cdot>A) = u_emb oo cast\<cdot>A oo u_prj"
+unfolding u_defl_def by (simp add: cast_defl_fun1 ep_pair_u)
lemma cast_prod_defl:
"cast\<cdot>(prod_defl\<cdot>A\<cdot>B) =
@@ -169,66 +206,11 @@
using ep_pair_sfun finite_deflation_sfun_map
unfolding sfun_defl_def by (rule cast_defl_fun2)
-subsection {* Lemma for proving domain instances *}
-
-text {*
- A class of domains where @{const liftemb}, @{const liftprj},
- and @{const liftdefl} are all defined in the standard way.
-*}
-
-class liftdomain = "domain" +
- assumes liftemb_eq: "liftemb = u_emb oo u_map\<cdot>emb"
- assumes liftprj_eq: "liftprj = u_map\<cdot>prj oo u_prj"
- assumes liftdefl_eq: "liftdefl TYPE('a::cpo) = u_defl\<cdot>DEFL('a)"
-
-text {* Temporarily relax type constraints. *}
-
-setup {*
- fold Sign.add_const_constraint
- [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> udom 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> udom defl"})
- , (@{const_name liftemb}, SOME @{typ "'a::pcpo u \<rightarrow> udom"})
- , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::pcpo u"}) ]
-*}
-
-default_sort pcpo
-
-lemma liftdomain_class_intro:
- assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
- assumes liftprj: "(liftprj :: udom \<rightarrow> 'a u) = u_map\<cdot>prj oo u_prj"
- 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, liftdomain_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_u)
- 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)
-next
-qed fact+
-
-text {* Restore original type constraints. *}
-
-setup {*
- fold Sign.add_const_constraint
- [ (@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> udom defl"})
- , (@{const_name emb}, SOME @{typ "'a::domain \<rightarrow> udom"})
- , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::domain"})
- , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> udom defl"})
- , (@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom"})
- , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::predomain u"}) ]
-*}
-
subsection {* Class instance proofs *}
subsubsection {* Universal domain *}
-instantiation udom :: liftdomain
+instantiation udom :: "domain"
begin
definition [simp]:
@@ -241,17 +223,15 @@
"defl (t::udom itself) = (\<Squnion>i. defl_principal (Abs_fin_defl (udom_approx i)))"
definition
- "(liftemb :: udom u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
-
-definition
- "(liftprj :: udom \<rightarrow> udom u) = u_map\<cdot>prj oo u_prj"
+ "(liftemb :: udom u \<rightarrow> udom u) = u_map\<cdot>emb"
definition
- "liftdefl (t::udom itself) = u_defl\<cdot>DEFL(udom)"
+ "(liftprj :: udom u \<rightarrow> udom u) = u_map\<cdot>prj"
-instance
-using liftemb_udom_def liftprj_udom_def liftdefl_udom_def
-proof (rule liftdomain_class_intro)
+definition
+ "liftdefl (t::udom itself) = pdefl\<cdot>DEFL(udom)"
+
+instance proof
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)"
@@ -266,52 +246,50 @@
apply (subst cast_defl_principal)
apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
done
-qed
+qed (fact liftemb_udom_def liftprj_udom_def liftdefl_udom_def)+
end
subsubsection {* Lifted cpo *}
-instantiation u :: (predomain) liftdomain
+instantiation u :: (predomain) "domain"
begin
definition
- "emb = liftemb"
+ "emb = u_emb oo liftemb"
definition
- "prj = liftprj"
+ "prj = liftprj oo u_prj"
definition
- "defl (t::'a u itself) = LIFTDEFL('a)"
+ "defl (t::'a u itself) = u_defl\<cdot>LIFTDEFL('a)"
definition
- "(liftemb :: 'a u u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
+ "(liftemb :: 'a u u \<rightarrow> udom u) = u_map\<cdot>emb"
definition
- "(liftprj :: udom \<rightarrow> 'a u u) = u_map\<cdot>prj oo u_prj"
+ "(liftprj :: udom u \<rightarrow> 'a u u) = u_map\<cdot>prj"
definition
- "liftdefl (t::'a u itself) = u_defl\<cdot>DEFL('a u)"
+ "liftdefl (t::'a u itself) = pdefl\<cdot>DEFL('a u)"
-instance
-using liftemb_u_def liftprj_u_def liftdefl_u_def
-proof (rule liftdomain_class_intro)
+instance proof
show "ep_pair emb (prj :: udom \<rightarrow> 'a u)"
unfolding emb_u_def prj_u_def
- by (rule predomain_ep)
+ by (intro ep_pair_comp ep_pair_u 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
+ by (simp add: cast_u_defl cast_liftdefl assoc_oo)
+qed (fact liftemb_u_def liftprj_u_def liftdefl_u_def)+
end
-lemma DEFL_u: "DEFL('a::predomain u) = LIFTDEFL('a)"
+lemma DEFL_u: "DEFL('a::predomain u) = u_defl\<cdot>LIFTDEFL('a)"
by (rule defl_u_def)
subsubsection {* Strict function space *}
-instantiation sfun :: ("domain", "domain") liftdomain
+instantiation sfun :: ("domain", "domain") "domain"
begin
definition
@@ -324,24 +302,22 @@
"defl (t::('a \<rightarrow>! 'b) itself) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
definition
- "(liftemb :: ('a \<rightarrow>! 'b) u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
-
-definition
- "(liftprj :: udom \<rightarrow> ('a \<rightarrow>! 'b) u) = u_map\<cdot>prj oo u_prj"
+ "(liftemb :: ('a \<rightarrow>! 'b) u \<rightarrow> udom u) = u_map\<cdot>emb"
definition
- "liftdefl (t::('a \<rightarrow>! 'b) itself) = u_defl\<cdot>DEFL('a \<rightarrow>! 'b)"
+ "(liftprj :: udom u \<rightarrow> ('a \<rightarrow>! 'b) u) = u_map\<cdot>prj"
-instance
-using liftemb_sfun_def liftprj_sfun_def liftdefl_sfun_def
-proof (rule liftdomain_class_intro)
+definition
+ "liftdefl (t::('a \<rightarrow>! 'b) itself) = pdefl\<cdot>DEFL('a \<rightarrow>! 'b)"
+
+instance proof
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
unfolding emb_sfun_def prj_sfun_def
by (intro ep_pair_comp ep_pair_sfun ep_pair_sfun_map ep_pair_emb_prj)
show "cast\<cdot>DEFL('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl
by (simp add: cast_DEFL oo_def sfun_eq_iff sfun_map_map)
-qed
+qed (fact liftemb_sfun_def liftprj_sfun_def liftdefl_sfun_def)+
end
@@ -351,7 +327,7 @@
subsubsection {* Continuous function space *}
-instantiation cfun :: (predomain, "domain") liftdomain
+instantiation cfun :: (predomain, "domain") "domain"
begin
definition
@@ -364,17 +340,15 @@
"defl (t::('a \<rightarrow> 'b) itself) = DEFL('a u \<rightarrow>! 'b)"
definition
- "(liftemb :: ('a \<rightarrow> 'b) u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
-
-definition
- "(liftprj :: udom \<rightarrow> ('a \<rightarrow> 'b) u) = u_map\<cdot>prj oo u_prj"
+ "(liftemb :: ('a \<rightarrow> 'b) u \<rightarrow> udom u) = u_map\<cdot>emb"
definition
- "liftdefl (t::('a \<rightarrow> 'b) itself) = u_defl\<cdot>DEFL('a \<rightarrow> 'b)"
+ "(liftprj :: udom u \<rightarrow> ('a \<rightarrow> 'b) u) = u_map\<cdot>prj"
-instance
-using liftemb_cfun_def liftprj_cfun_def liftdefl_cfun_def
-proof (rule liftdomain_class_intro)
+definition
+ "liftdefl (t::('a \<rightarrow> 'b) itself) = pdefl\<cdot>DEFL('a \<rightarrow> 'b)"
+
+instance proof
have "ep_pair encode_cfun decode_cfun"
by (rule ep_pair.intro, simp_all)
thus "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
@@ -383,7 +357,7 @@
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
by (simp add: cast_DEFL cfcomp1)
-qed
+qed (fact liftemb_cfun_def liftprj_cfun_def liftdefl_cfun_def)+
end
@@ -393,7 +367,7 @@
subsubsection {* Strict product *}
-instantiation sprod :: ("domain", "domain") liftdomain
+instantiation sprod :: ("domain", "domain") "domain"
begin
definition
@@ -406,25 +380,22 @@
"defl (t::('a \<otimes> 'b) itself) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
definition
- "(liftemb :: ('a \<otimes> 'b) u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
-
-definition
- "(liftprj :: udom \<rightarrow> ('a \<otimes> 'b) u) = u_map\<cdot>prj oo u_prj"
+ "(liftemb :: ('a \<otimes> 'b) u \<rightarrow> udom u) = u_map\<cdot>emb"
definition
- "liftdefl (t::('a \<otimes> 'b) itself) = u_defl\<cdot>DEFL('a \<otimes> 'b)"
+ "(liftprj :: udom u \<rightarrow> ('a \<otimes> 'b) u) = u_map\<cdot>prj"
-instance
-using liftemb_sprod_def liftprj_sprod_def liftdefl_sprod_def
-proof (rule liftdomain_class_intro)
+definition
+ "liftdefl (t::('a \<otimes> 'b) itself) = pdefl\<cdot>DEFL('a \<otimes> 'b)"
+
+instance proof
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
unfolding emb_sprod_def prj_sprod_def
by (intro ep_pair_comp ep_pair_sprod ep_pair_sprod_map ep_pair_emb_prj)
-next
show "cast\<cdot>DEFL('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
unfolding emb_sprod_def prj_sprod_def defl_sprod_def cast_sprod_defl
by (simp add: cast_DEFL oo_def cfun_eq_iff sprod_map_map)
-qed
+qed (fact liftemb_sprod_def liftprj_sprod_def liftdefl_sprod_def)+
end
@@ -434,27 +405,43 @@
subsubsection {* Cartesian product *}
+definition prod_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl"
+ where "prod_liftdefl = defl_fun2 (u_map\<cdot>prod_emb oo decode_prod_u)
+ (encode_prod_u oo u_map\<cdot>prod_prj) sprod_map"
+
+lemma cast_prod_liftdefl:
+ "cast\<cdot>(prod_liftdefl\<cdot>a\<cdot>b) =
+ (u_map\<cdot>prod_emb oo decode_prod_u) oo sprod_map\<cdot>(cast\<cdot>a)\<cdot>(cast\<cdot>b) oo
+ (encode_prod_u oo u_map\<cdot>prod_prj)"
+unfolding prod_liftdefl_def
+apply (rule cast_defl_fun2)
+apply (intro ep_pair_comp ep_pair_u_map ep_pair_prod)
+apply (simp add: ep_pair.intro)
+apply (erule (1) finite_deflation_sprod_map)
+done
+
instantiation prod :: (predomain, predomain) predomain
begin
definition
- "liftemb = emb oo encode_prod_u"
+ "liftemb = (u_map\<cdot>prod_emb oo decode_prod_u) oo
+ (sprod_map\<cdot>liftemb\<cdot>liftemb oo encode_prod_u)"
definition
- "liftprj = decode_prod_u oo prj"
+ "liftprj = (decode_prod_u oo sprod_map\<cdot>liftprj\<cdot>liftprj) oo
+ (encode_prod_u oo u_map\<cdot>prod_prj)"
definition
- "liftdefl (t::('a \<times> 'b) itself) = DEFL('a\<^sub>\<bottom> \<otimes> 'b\<^sub>\<bottom>)"
+ "liftdefl (t::('a \<times> 'b) itself) = prod_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
instance proof
- have "ep_pair encode_prod_u decode_prod_u"
- by (rule ep_pair.intro, simp_all)
- thus "ep_pair liftemb (liftprj :: udom \<rightarrow> ('a \<times> 'b) u)"
+ show "ep_pair liftemb (liftprj :: udom u \<rightarrow> ('a \<times> 'b) u)"
unfolding liftemb_prod_def liftprj_prod_def
- using ep_pair_emb_prj by (rule ep_pair_comp)
- show "cast\<cdot>LIFTDEFL('a \<times> 'b) = liftemb oo (liftprj :: udom \<rightarrow> ('a \<times> 'b) u)"
+ by (intro ep_pair_comp ep_pair_sprod_map ep_pair_u_map
+ ep_pair_prod predomain_ep, simp_all add: ep_pair.intro)
+ show "cast\<cdot>LIFTDEFL('a \<times> 'b) = liftemb oo (liftprj :: udom u \<rightarrow> ('a \<times> 'b) u)"
unfolding liftemb_prod_def liftprj_prod_def liftdefl_prod_def
- by (simp add: cast_DEFL cfcomp1)
+ by (simp add: cast_prod_liftdefl cast_liftdefl cfcomp1 sprod_map_map)
qed
end
@@ -472,13 +459,25 @@
"defl (t::('a \<times> 'b) itself) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
instance proof
- show "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)"
+ show 1: "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)"
unfolding emb_prod_def prj_prod_def
by (intro ep_pair_comp ep_pair_prod ep_pair_cprod_map ep_pair_emb_prj)
-next
- show "cast\<cdot>DEFL('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
+ show 2: "cast\<cdot>DEFL('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl
by (simp add: cast_DEFL oo_def cfun_eq_iff cprod_map_map)
+ show 3: "liftemb = u_map\<cdot>(emb :: 'a \<times> 'b \<rightarrow> udom)"
+ unfolding emb_prod_def liftemb_prod_def liftemb_eq
+ unfolding encode_prod_u_def decode_prod_u_def
+ by (rule cfun_eqI, case_tac x, simp, clarsimp)
+ show 4: "liftprj = u_map\<cdot>(prj :: udom \<rightarrow> 'a \<times> 'b)"
+ unfolding prj_prod_def liftprj_prod_def liftprj_eq
+ unfolding encode_prod_u_def decode_prod_u_def
+ apply (rule cfun_eqI, case_tac x, simp)
+ apply (rename_tac y, case_tac "prod_prj\<cdot>y", simp)
+ done
+ show 5: "LIFTDEFL('a \<times> 'b) = pdefl\<cdot>DEFL('a \<times> 'b)"
+ by (rule cast_eq_imp_eq)
+ (simp add: cast_liftdefl cast_pdefl cast_DEFL 2 3 4 u_map_oo)
qed
end
@@ -488,12 +487,13 @@
by (rule defl_prod_def)
lemma LIFTDEFL_prod:
- "LIFTDEFL('a::predomain \<times> 'b::predomain) = DEFL('a u \<otimes> 'b u)"
+ "LIFTDEFL('a::predomain \<times> 'b::predomain) =
+ prod_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
by (rule liftdefl_prod_def)
subsubsection {* Unit type *}
-instantiation unit :: liftdomain
+instantiation unit :: "domain"
begin
definition
@@ -506,24 +506,21 @@
"defl (t::unit itself) = \<bottom>"
definition
- "(liftemb :: unit u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
-
-definition
- "(liftprj :: udom \<rightarrow> unit u) = u_map\<cdot>prj oo u_prj"
+ "(liftemb :: unit u \<rightarrow> udom u) = u_map\<cdot>emb"
definition
- "liftdefl (t::unit itself) = u_defl\<cdot>DEFL(unit)"
+ "(liftprj :: udom u \<rightarrow> unit u) = u_map\<cdot>prj"
-instance
-using liftemb_unit_def liftprj_unit_def liftdefl_unit_def
-proof (rule liftdomain_class_intro)
+definition
+ "liftdefl (t::unit itself) = pdefl\<cdot>DEFL(unit)"
+
+instance proof
show "ep_pair emb (prj :: udom \<rightarrow> unit)"
unfolding emb_unit_def prj_unit_def
by (simp add: ep_pair.intro)
-next
show "cast\<cdot>DEFL(unit) = emb oo (prj :: udom \<rightarrow> unit)"
unfolding emb_unit_def prj_unit_def defl_unit_def by simp
-qed
+qed (fact liftemb_unit_def liftprj_unit_def liftdefl_unit_def)+
end
@@ -533,34 +530,38 @@
begin
definition
- "(liftemb :: 'a discr u \<rightarrow> udom) = udom_emb discr_approx"
+ "(liftemb :: 'a discr u \<rightarrow> udom u) = strictify\<cdot>up oo udom_emb discr_approx"
definition
- "(liftprj :: udom \<rightarrow> 'a discr u) = udom_prj discr_approx"
+ "(liftprj :: udom u \<rightarrow> 'a discr u) = udom_prj discr_approx oo fup\<cdot>ID"
definition
"liftdefl (t::'a discr itself) =
- (\<Squnion>i. defl_principal (Abs_fin_defl (liftemb oo discr_approx i oo (liftprj::udom \<rightarrow> 'a discr u))))"
+ (\<Squnion>i. defl_principal (Abs_fin_defl (liftemb oo discr_approx i oo (liftprj::udom u \<rightarrow> 'a discr u))))"
instance proof
- show "ep_pair liftemb (liftprj :: udom \<rightarrow> 'a discr u)"
+ show 1: "ep_pair liftemb (liftprj :: udom u \<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 (intro ep_pair_comp ep_pair_udom [OF discr_approx])
+ apply (rule ep_pair.intro)
+ apply (simp add: strictify_conv_if)
+ apply (case_tac y, simp, simp add: strictify_conv_if)
+ done
+ show "cast\<cdot>LIFTDEFL('a discr) = liftemb oo (liftprj :: udom u \<rightarrow> 'a discr u)"
+ unfolding 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
- ep_pair.finite_deflation_e_d_p [OF ep_pair_udom [OF discr_approx]]
+ ep_pair.finite_deflation_e_d_p [OF 1]
approx_chain.finite_deflation_approx [OF discr_approx])
apply (intro monofun_cfun below_refl)
apply (rule chainE)
apply (rule chain_discr_approx)
apply (subst cast_defl_principal)
apply (simp add: Abs_fin_defl_inverse
- ep_pair.finite_deflation_e_d_p [OF ep_pair_udom [OF discr_approx]]
+ ep_pair.finite_deflation_e_d_p [OF 1]
approx_chain.finite_deflation_approx [OF discr_approx])
apply (simp add: lub_distribs)
done
@@ -570,7 +571,7 @@
subsubsection {* Strict sum *}
-instantiation ssum :: ("domain", "domain") liftdomain
+instantiation ssum :: ("domain", "domain") "domain"
begin
definition
@@ -583,24 +584,22 @@
"defl (t::('a \<oplus> 'b) itself) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
definition
- "(liftemb :: ('a \<oplus> 'b) u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
-
-definition
- "(liftprj :: udom \<rightarrow> ('a \<oplus> 'b) u) = u_map\<cdot>prj oo u_prj"
+ "(liftemb :: ('a \<oplus> 'b) u \<rightarrow> udom u) = u_map\<cdot>emb"
definition
- "liftdefl (t::('a \<oplus> 'b) itself) = u_defl\<cdot>DEFL('a \<oplus> 'b)"
+ "(liftprj :: udom u \<rightarrow> ('a \<oplus> 'b) u) = u_map\<cdot>prj"
-instance
-using liftemb_ssum_def liftprj_ssum_def liftdefl_ssum_def
-proof (rule liftdomain_class_intro)
+definition
+ "liftdefl (t::('a \<oplus> 'b) itself) = pdefl\<cdot>DEFL('a \<oplus> 'b)"
+
+instance proof
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
unfolding emb_ssum_def prj_ssum_def
by (intro ep_pair_comp ep_pair_ssum ep_pair_ssum_map ep_pair_emb_prj)
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)
-qed
+qed (fact liftemb_ssum_def liftprj_ssum_def liftdefl_ssum_def)+
end
@@ -610,7 +609,7 @@
subsubsection {* Lifted HOL type *}
-instantiation lift :: (countable) liftdomain
+instantiation lift :: (countable) "domain"
begin
definition
@@ -623,17 +622,15 @@
"defl (t::'a lift itself) = DEFL('a discr u)"
definition
- "(liftemb :: 'a lift u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
-
-definition
- "(liftprj :: udom \<rightarrow> 'a lift u) = u_map\<cdot>prj oo u_prj"
+ "(liftemb :: 'a lift u \<rightarrow> udom u) = u_map\<cdot>emb"
definition
- "liftdefl (t::'a lift itself) = u_defl\<cdot>DEFL('a lift)"
+ "(liftprj :: udom u \<rightarrow> 'a lift u) = u_map\<cdot>prj"
-instance
-using liftemb_lift_def liftprj_lift_def liftdefl_lift_def
-proof (rule liftdomain_class_intro)
+definition
+ "liftdefl (t::'a lift itself) = pdefl\<cdot>DEFL('a lift)"
+
+instance proof
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)
@@ -643,7 +640,7 @@
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
+qed (fact liftemb_lift_def liftprj_lift_def liftdefl_lift_def)+
end
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Dec 19 10:33:46 2010 -0800
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Dec 19 17:37:19 2010 -0800
@@ -69,6 +69,7 @@
val udomT = @{typ udom}
val deflT = @{typ "udom defl"}
+val udeflT = @{typ "udom u defl"}
fun mk_DEFL T =
Const (@{const_name defl}, Term.itselfT T --> deflT) $ Logic.mk_type T
@@ -77,7 +78,7 @@
| dest_DEFL t = raise TERM ("dest_DEFL", [t])
fun mk_LIFTDEFL T =
- Const (@{const_name liftdefl}, Term.itselfT T --> deflT) $ Logic.mk_type T
+ Const (@{const_name liftdefl}, Term.itselfT T --> udeflT) $ Logic.mk_type T
fun dest_LIFTDEFL (Const (@{const_name liftdefl}, _) $ t) = Logic.dest_type t
| dest_LIFTDEFL t = raise TERM ("dest_LIFTDEFL", [t])
@@ -100,6 +101,9 @@
fun isodefl_const T =
Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT)
+fun isodefl'_const T =
+ Const (@{const_name isodefl'}, (T ->> T) --> udeflT --> HOLogic.boolT)
+
fun mk_deflation t =
Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t
@@ -218,7 +222,7 @@
| _ => NONE) handle TERM _ => NONE
fun proc2 t =
(case dest_LIFTDEFL t of
- TFree (a, _) => SOME (Free ("p" ^ Library.unprefix "'" a, deflT))
+ TFree (a, _) => SOME (Free ("p" ^ Library.unprefix "'" a, udeflT))
| _ => NONE) handle TERM _ => NONE
in
Pattern.rewrite_term thy (rules @ rules') [proc1, proc2] (mk_DEFL T)
@@ -492,7 +496,7 @@
let
val defl_bind = Binding.suffix_name "_defl" tbind
val defl_type =
- map Term.itselfT typeTs ---> map (K deflT) defl_args -->> deflT
+ map Term.itselfT typeTs ---> map fastype_of defl_args -->> deflT
in
Sign.declare_const ((defl_bind, defl_type), NoSyn) thy
end
@@ -614,11 +618,11 @@
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_p T = Free ("p" ^ unprime (fst (dest_TFree T)), udeflT)
fun mk_f T = Free ("f" ^ unprime (fst (dest_TFree T)), T ->> T)
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)
+ SOME T => mk_trp (isodefl'_const T $ 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
--- a/src/HOL/HOLCF/Tools/domaindef.ML Sun Dec 19 10:33:46 2010 -0800
+++ b/src/HOL/HOLCF/Tools/domaindef.ML Sun Dec 19 17:37:19 2010 -0800
@@ -50,12 +50,13 @@
val udomT = @{typ udom}
val deflT = @{typ "udom defl"}
+val udeflT = @{typ "udom u defl"}
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 liftemb_const T = Const (@{const_name liftemb}, mk_upT T ->> mk_upT udomT)
+fun liftprj_const T = Const (@{const_name liftprj}, mk_upT udomT ->> mk_upT T)
+fun liftdefl_const T = Const (@{const_name liftdefl}, Term.itselfT T --> udeflT)
fun mk_u_map t =
let
@@ -129,15 +130,13 @@
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 (@{const u_emb}, mk_u_map (emb_const newT)))
+ Logic.mk_equals (liftemb_const newT, mk_u_map (emb_const newT))
val liftprj_eqn =
- Logic.mk_equals (liftprj_const newT,
- mk_cfcomp (mk_u_map (prj_const newT), @{const u_prj}))
+ Logic.mk_equals (liftprj_const newT, mk_u_map (prj_const newT))
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)))
+ mk_capply (@{const pdefl}, defl_const newT $ Logic.mk_type newT)))
val name_def = Binding.suffix_name "_def" name
val emb_bind = (Binding.prefix_name "emb_" name_def, [])
@@ -149,7 +148,7 @@
(*instantiate class rep*)
val lthy = thy
- |> Class.instantiation ([full_tname], lhs_tfrees, @{sort liftdomain})
+ |> Class.instantiation ([full_tname], lhs_tfrees, @{sort domain})
val ((_, (_, emb_ldef)), lthy) =
Specification.definition (NONE, (emb_bind, emb_eqn)) lthy
val ((_, (_, prj_ldef)), lthy) =
@@ -178,7 +177,7 @@
liftemb_def, liftprj_def, liftdefl_def]
val thy = lthy
|> Class.prove_instantiation_instance
- (K (Tactic.rtac (@{thm typedef_liftdomain_class} OF typedef_thms) 1))
+ (K (Tactic.rtac (@{thm typedef_domain_class} OF typedef_thms) 1))
|> Local_Theory.exit_global
(*other theorems*)
--- a/src/HOL/HOLCF/ex/Domain_Proofs.thy Sun Dec 19 10:33:46 2010 -0800
+++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy Sun Dec 19 17:37:19 2010 -0800
@@ -17,9 +17,6 @@
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.
-
*)
(********************************************************************)
@@ -33,15 +30,15 @@
"udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl"
where
"foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3).
- ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>t2))
- , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>t3)\<cdot>DEFL(tr))
- , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>t1))\<cdot>DEFL(tr)))))"
+ ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>a))\<cdot>(u_defl\<cdot>(pdefl\<cdot>t2)))
+ , u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>t3))\<cdot>DEFL(tr)))
+ , u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<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>a\<cdot>(u_defl\<cdot>(fst (snd t))))
- , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(snd (snd t)))\<cdot>DEFL(tr))
- , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(fst t)))\<cdot>DEFL(tr)))"
+ ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>a))\<cdot>(u_defl\<cdot>(pdefl\<cdot>(fst (snd t)))))
+ , u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>(snd (snd t))))\<cdot>DEFL(tr)))
+ , u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>(convex_defl\<cdot>(fst t))))\<cdot>DEFL(tr))))"
unfolding foo_bar_baz_deflF_def
by (simp add: split_def)
@@ -65,13 +62,13 @@
text {* Unfold rules for each combinator. *}
lemma foo_defl_unfold:
- "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
+ "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>a))\<cdot>(u_defl\<cdot>(pdefl\<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>(sfun_defl\<cdot>(u_defl\<cdot>(baz_defl\<cdot>a))\<cdot>DEFL(tr))"
+lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>(baz_defl\<cdot>a)))\<cdot>DEFL(tr)))"
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
-lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a)))\<cdot>DEFL(tr))"
+lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a))))\<cdot>DEFL(tr)))"
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
text "The automation for the previous steps will be quite similar to
@@ -83,40 +80,40 @@
text {* Use @{text pcpodef} with the appropriate type combinator. *}
-pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>LIFTDEFL('a))"
+pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>DEFL('a))"
by (rule defl_set_bottom, rule adm_defl_set)
-pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>LIFTDEFL('a))"
+pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>DEFL('a))"
by (rule defl_set_bottom, rule adm_defl_set)
-pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>LIFTDEFL('a))"
+pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>DEFL('a))"
by (rule defl_set_bottom, rule adm_defl_set)
text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
-instantiation foo :: ("domain") liftdomain
+instantiation foo :: ("domain") "domain"
begin
definition emb_foo :: "'a foo \<rightarrow> udom"
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>LIFTDEFL('a))\<cdot>y))"
+where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>DEFL('a))\<cdot>y))"
definition defl_foo :: "'a foo itself \<Rightarrow> udom defl"
-where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>LIFTDEFL('a)"
+where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>DEFL('a)"
definition
- "(liftemb :: 'a foo u \<rightarrow> udom) \<equiv> u_emb oo u_map\<cdot>emb"
+ "(liftemb :: 'a foo u \<rightarrow> udom u) \<equiv> u_map\<cdot>emb"
definition
- "(liftprj :: udom \<rightarrow> 'a foo u) \<equiv> u_map\<cdot>prj oo u_prj"
+ "(liftprj :: udom u \<rightarrow> 'a foo u) \<equiv> u_map\<cdot>prj"
definition
- "liftdefl \<equiv> \<lambda>(t::'a foo itself). u_defl\<cdot>DEFL('a foo)"
+ "liftdefl \<equiv> \<lambda>(t::'a foo itself). pdefl\<cdot>DEFL('a foo)"
instance
-apply (rule typedef_liftdomain_class)
+apply (rule typedef_domain_class)
apply (rule type_definition_foo)
apply (rule below_foo_def)
apply (rule emb_foo_def)
@@ -129,29 +126,29 @@
end
-instantiation bar :: ("domain") liftdomain
+instantiation bar :: ("domain") "domain"
begin
definition emb_bar :: "'a bar \<rightarrow> udom"
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>LIFTDEFL('a))\<cdot>y))"
+where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>DEFL('a))\<cdot>y))"
definition defl_bar :: "'a bar itself \<Rightarrow> udom defl"
-where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>LIFTDEFL('a)"
+where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>DEFL('a)"
definition
- "(liftemb :: 'a bar u \<rightarrow> udom) \<equiv> u_emb oo u_map\<cdot>emb"
+ "(liftemb :: 'a bar u \<rightarrow> udom u) \<equiv> u_map\<cdot>emb"
definition
- "(liftprj :: udom \<rightarrow> 'a bar u) \<equiv> u_map\<cdot>prj oo u_prj"
+ "(liftprj :: udom u \<rightarrow> 'a bar u) \<equiv> u_map\<cdot>prj"
definition
- "liftdefl \<equiv> \<lambda>(t::'a bar itself). u_defl\<cdot>DEFL('a bar)"
+ "liftdefl \<equiv> \<lambda>(t::'a bar itself). pdefl\<cdot>DEFL('a bar)"
instance
-apply (rule typedef_liftdomain_class)
+apply (rule typedef_domain_class)
apply (rule type_definition_bar)
apply (rule below_bar_def)
apply (rule emb_bar_def)
@@ -164,29 +161,29 @@
end
-instantiation baz :: ("domain") liftdomain
+instantiation baz :: ("domain") "domain"
begin
definition emb_baz :: "'a baz \<rightarrow> udom"
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>LIFTDEFL('a))\<cdot>y))"
+where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>DEFL('a))\<cdot>y))"
definition defl_baz :: "'a baz itself \<Rightarrow> udom defl"
-where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>LIFTDEFL('a)"
+where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>DEFL('a)"
definition
- "(liftemb :: 'a baz u \<rightarrow> udom) \<equiv> u_emb oo u_map\<cdot>emb"
+ "(liftemb :: 'a baz u \<rightarrow> udom u) \<equiv> u_map\<cdot>emb"
definition
- "(liftprj :: udom \<rightarrow> 'a baz u) \<equiv> u_map\<cdot>prj oo u_prj"
+ "(liftprj :: udom u \<rightarrow> 'a baz u) \<equiv> u_map\<cdot>prj"
definition
- "liftdefl \<equiv> \<lambda>(t::'a baz itself). u_defl\<cdot>DEFL('a baz)"
+ "liftdefl \<equiv> \<lambda>(t::'a baz itself). pdefl\<cdot>DEFL('a baz)"
instance
-apply (rule typedef_liftdomain_class)
+apply (rule typedef_domain_class)
apply (rule type_definition_baz)
apply (rule below_baz_def)
apply (rule emb_baz_def)
@@ -201,17 +198,17 @@
text {* Prove DEFL rules using lemma @{text typedef_DEFL}. *}
-lemma DEFL_foo: "DEFL('a foo) = foo_defl\<cdot>LIFTDEFL('a)"
+lemma DEFL_foo: "DEFL('a foo) = foo_defl\<cdot>DEFL('a)"
apply (rule typedef_DEFL)
apply (rule defl_foo_def)
done
-lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>LIFTDEFL('a)"
+lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>DEFL('a)"
apply (rule typedef_DEFL)
apply (rule defl_bar_def)
done
-lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>LIFTDEFL('a)"
+lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>DEFL('a)"
apply (rule typedef_DEFL)
apply (rule defl_baz_def)
done
@@ -348,7 +345,7 @@
text {* Prove isodefl rules for all map functions simultaneously. *}
lemma isodefl_foo_bar_baz:
- assumes isodefl_d: "isodefl (u_map\<cdot>d) t"
+ assumes isodefl_d: "isodefl d t"
shows
"isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and>
isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and>
@@ -383,21 +380,21 @@
apply (rule isodefl_DEFL_imp_ID)
apply (subst DEFL_foo)
apply (rule isodefl_foo)
-apply (rule isodefl_LIFTDEFL)
+apply (rule isodefl_ID_DEFL)
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_LIFTDEFL)
+apply (rule isodefl_ID_DEFL)
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_LIFTDEFL)
+apply (rule isodefl_ID_DEFL)
done
(********************************************************************)