--- 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