|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
Representable.thy
Sprache: Isabelle
|
|
(* Title: HOL/HOLCF/Representable.thy
Author: Brian Huffman
*)
section \<open>Representable domains\<close>
theory Representable
imports Algebraic Map_Functions "HOL-Library.Countable"
begin
default_sort cpo
subsection \<open>Class of representable domains\<close>
text \<open>
We define a ``domain'' as a pcpo that is isomorphic to some
algebraic deflation over the universal domain; this is equivalent
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.
\<close>
class predomain_syn = cpo +
fixes liftemb :: "'a\<^sub>\ \ udom\<^sub>\"
fixes liftprj :: "udom\<^sub>\ \ 'a\<^sub>\"
fixes liftdefl :: "'a itself \ udom u defl"
class predomain = predomain_syn +
assumes predomain_ep: "ep_pair liftemb liftprj"
assumes cast_liftdefl: "cast\(liftdefl TYPE('a)) = liftemb oo liftprj"
syntax "_LIFTDEFL" :: "type \ logic" ("(1LIFTDEFL/(1'(_')))")
translations "LIFTDEFL('t)" \<rightleftharpoons> "CONST liftdefl TYPE('t)"
definition liftdefl_of :: "udom defl \ udom u defl"
where "liftdefl_of = defl_fun1 ID ID u_map"
lemma cast_liftdefl_of: "cast\(liftdefl_of\t) = u_map\(cast\t)"
by (simp add: liftdefl_of_def cast_defl_fun1 ep_pair_def finite_deflation_u_map)
class "domain" = predomain_syn + pcpo +
fixes emb :: "'a \ udom"
fixes prj :: "udom \ 'a"
fixes defl :: "'a itself \ udom defl"
assumes ep_pair_emb_prj: "ep_pair emb prj"
assumes cast_DEFL: "cast\(defl TYPE('a)) = emb oo prj"
assumes liftemb_eq: "liftemb = u_map\emb"
assumes liftprj_eq: "liftprj = u_map\prj"
assumes liftdefl_eq: "liftdefl TYPE('a) = liftdefl_of\(defl TYPE('a))"
syntax "_DEFL" :: "type \ logic" ("(1DEFL/(1'(_')))")
translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)"
instance "domain" \<subseteq> predomain
proof
show "ep_pair liftemb (liftprj::udom\<^sub>\ \ 'a\<^sub>\)"
unfolding liftemb_eq liftprj_eq
by (intro ep_pair_u_map ep_pair_emb_prj)
show "cast\LIFTDEFL('a) = liftemb oo (liftprj::udom\<^sub>\ \ 'a\<^sub>\)"
unfolding liftemb_eq liftprj_eq liftdefl_eq
by (simp add: cast_liftdefl_of cast_DEFL u_map_oo)
qed
text \<open>
Constants \<^const>\<open>liftemb\<close> and \<^const>\<open>liftprj\<close> imply class predomain.
\<close>
setup \<open>
fold Sign.add_const_constraint
[(\<^const_name>\<open>liftemb\<close>, SOME \<^typ>\<open>'a::predomain u \<rightarrow> udom u\<close>),
(\<^const_name>\<open>liftprj\<close>, SOME \<^typ>\<open>udom u \<rightarrow> 'a::predomain u\<close>),
(\<^const_name>\<open>liftdefl\<close>, SOME \<^typ>\<open>'a::predomain itself \<Rightarrow> udom u defl\<close>)]
\<close>
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)
lemmas emb_inverse = domain.e_inverse
lemmas emb_prj_below = domain.e_p_below
lemmas emb_eq_iff = domain.e_eq_iff
lemmas emb_strict = domain.e_strict
lemmas prj_strict = domain.p_strict
subsection \<open>Domains are bifinite\<close>
lemma approx_chain_ep_cast:
assumes ep: "ep_pair (e::'a::pcpo \ 'b::bifinite) (p::'b \ 'a)"
assumes cast_t: "cast\t = e oo p"
shows "\(a::nat \ 'a::pcpo \ 'a). approx_chain a"
proof -
interpret ep_pair e p by fact
obtain Y where Y: "\i. Y i \ Y (Suc i)"
and t: "t = (\i. defl_principal (Y i))"
by (rule defl.obtain_principal_chain)
define approx where "approx i = (p oo cast\(defl_principal (Y i)) oo e)" for i
have "approx_chain approx"
proof (rule approx_chain.intro)
show "chain (\i. approx i)"
unfolding approx_def by (simp add: Y)
show "(\i. approx i) = ID"
unfolding approx_def
by (simp add: lub_distribs Y t [symmetric] cast_t cfun_eq_iff)
show "\i. finite_deflation (approx i)"
unfolding approx_def
apply (rule finite_deflation_p_d_e)
apply (rule finite_deflation_cast)
apply (rule defl.compact_principal)
apply (rule below_trans [OF monofun_cfun_fun])
apply (rule is_ub_thelub, simp add: Y)
apply (simp add: lub_distribs Y t [symmetric] cast_t)
done
qed
thus "\(a::nat \ 'a \ 'a). approx_chain a" by - (rule exI)
qed
instance "domain" \<subseteq> bifinite
by standard (rule approx_chain_ep_cast [OF ep_pair_emb_prj cast_DEFL])
instance predomain \<subseteq> profinite
by standard (rule approx_chain_ep_cast [OF predomain_ep cast_liftdefl])
subsection \<open>Universal domain ep-pairs\<close>
definition "u_emb = udom_emb (\i. u_map\(udom_approx i))"
definition "u_prj = udom_prj (\i. u_map\(udom_approx i))"
definition "prod_emb = udom_emb (\i. prod_map\(udom_approx i)\(udom_approx i))"
definition "prod_prj = udom_prj (\i. prod_map\(udom_approx i)\(udom_approx i))"
definition "sprod_emb = udom_emb (\i. sprod_map\(udom_approx i)\(udom_approx i))"
definition "sprod_prj = udom_prj (\i. sprod_map\(udom_approx i)\(udom_approx i))"
definition "ssum_emb = udom_emb (\i. ssum_map\(udom_approx i)\(udom_approx i))"
definition "ssum_prj = udom_prj (\i. ssum_map\(udom_approx i)\(udom_approx i))"
definition "sfun_emb = udom_emb (\i. sfun_map\(udom_approx i)\(udom_approx i))"
definition "sfun_prj = udom_prj (\i. sfun_map\(udom_approx i)\(udom_approx i))"
lemma ep_pair_u: "ep_pair u_emb u_prj"
unfolding u_emb_def u_prj_def
by (simp add: ep_pair_udom approx_chain_u_map)
lemma ep_pair_prod: "ep_pair prod_emb prod_prj"
unfolding prod_emb_def prod_prj_def
by (simp add: ep_pair_udom approx_chain_prod_map)
lemma ep_pair_sprod: "ep_pair sprod_emb sprod_prj"
unfolding sprod_emb_def sprod_prj_def
by (simp add: ep_pair_udom approx_chain_sprod_map)
lemma ep_pair_ssum: "ep_pair ssum_emb ssum_prj"
unfolding ssum_emb_def ssum_prj_def
by (simp add: ep_pair_udom approx_chain_ssum_map)
lemma ep_pair_sfun: "ep_pair sfun_emb sfun_prj"
unfolding sfun_emb_def sfun_prj_def
by (simp add: ep_pair_udom approx_chain_sfun_map)
subsection \<open>Type combinators\<close>
definition u_defl :: "udom defl \ udom defl"
where "u_defl = defl_fun1 u_emb u_prj u_map"
definition prod_defl :: "udom defl \ udom defl \ udom defl"
where "prod_defl = defl_fun2 prod_emb prod_prj prod_map"
definition sprod_defl :: "udom defl \ udom defl \ udom defl"
where "sprod_defl = defl_fun2 sprod_emb sprod_prj sprod_map"
definition ssum_defl :: "udom defl \ udom defl \ udom defl"
where "ssum_defl = defl_fun2 ssum_emb ssum_prj ssum_map"
definition sfun_defl :: "udom defl \ udom defl \ udom defl"
where "sfun_defl = defl_fun2 sfun_emb sfun_prj sfun_map"
lemma cast_u_defl:
"cast\(u_defl\A) = u_emb oo u_map\(cast\A) oo u_prj"
using ep_pair_u finite_deflation_u_map
unfolding u_defl_def by (rule cast_defl_fun1)
lemma cast_prod_defl:
"cast\(prod_defl\A\B) =
prod_emb oo prod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo prod_prj"
using ep_pair_prod finite_deflation_prod_map
unfolding prod_defl_def by (rule cast_defl_fun2)
lemma cast_sprod_defl:
"cast\(sprod_defl\A\B) =
sprod_emb oo sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo sprod_prj"
using ep_pair_sprod finite_deflation_sprod_map
unfolding sprod_defl_def by (rule cast_defl_fun2)
lemma cast_ssum_defl:
"cast\(ssum_defl\A\B) =
ssum_emb oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo ssum_prj"
using ep_pair_ssum finite_deflation_ssum_map
unfolding ssum_defl_def by (rule cast_defl_fun2)
lemma cast_sfun_defl:
"cast\(sfun_defl\A\B) =
sfun_emb oo sfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo sfun_prj"
using ep_pair_sfun finite_deflation_sfun_map
unfolding sfun_defl_def by (rule cast_defl_fun2)
text \<open>Special deflation combinator for unpointed types.\<close>
definition u_liftdefl :: "udom u defl \ udom defl"
where "u_liftdefl = defl_fun1 u_emb u_prj ID"
lemma cast_u_liftdefl:
"cast\(u_liftdefl\A) = u_emb oo cast\A oo u_prj"
unfolding u_liftdefl_def by (simp add: cast_defl_fun1 ep_pair_u)
lemma u_liftdefl_liftdefl_of:
"u_liftdefl\(liftdefl_of\A) = u_defl\A"
by (rule cast_eq_imp_eq)
(simp add: cast_u_liftdefl cast_liftdefl_of cast_u_defl)
subsection \<open>Class instance proofs\<close>
subsubsection \<open>Universal domain\<close>
instantiation udom :: "domain"
begin
definition [simp]:
"emb = (ID :: udom \ udom)"
definition [simp]:
"prj = (ID :: udom \ udom)"
definition
"defl (t::udom itself) = (\i. defl_principal (Abs_fin_defl (udom_approx i)))"
definition
"(liftemb :: udom u \ udom u) = u_map\emb"
definition
"(liftprj :: udom u \ udom u) = u_map\prj"
definition
"liftdefl (t::udom itself) = liftdefl_of\DEFL(udom)"
instance proof
show "ep_pair emb (prj :: udom \ udom)"
by (simp add: ep_pair.intro)
show "cast\DEFL(udom) = emb oo (prj :: udom \ udom)"
unfolding defl_udom_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_udom_approx)
apply (rule chainE)
apply (rule chain_udom_approx)
apply (subst cast_defl_principal)
apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
done
qed (fact liftemb_udom_def liftprj_udom_def liftdefl_udom_def)+
end
subsubsection \<open>Lifted cpo\<close>
instantiation u :: (predomain) "domain"
begin
definition
"emb = u_emb oo liftemb"
definition
"prj = liftprj oo u_prj"
definition
"defl (t::'a u itself) = u_liftdefl\LIFTDEFL('a)"
definition
"(liftemb :: 'a u u \ udom u) = u_map\emb"
definition
"(liftprj :: udom u \ 'a u u) = u_map\prj"
definition
"liftdefl (t::'a u itself) = liftdefl_of\DEFL('a u)"
instance proof
show "ep_pair emb (prj :: udom \ 'a u)"
unfolding emb_u_def prj_u_def
by (intro ep_pair_comp ep_pair_u predomain_ep)
show "cast\DEFL('a u) = emb oo (prj :: udom \ 'a u)"
unfolding emb_u_def prj_u_def defl_u_def
by (simp add: cast_u_liftdefl cast_liftdefl assoc_oo)
qed (fact liftemb_u_def liftprj_u_def liftdefl_u_def)+
end
lemma DEFL_u: "DEFL('a::predomain u) = u_liftdefl\LIFTDEFL('a)"
by (rule defl_u_def)
subsubsection \<open>Strict function space\<close>
instantiation sfun :: ("domain", "domain") "domain"
begin
definition
"emb = sfun_emb oo sfun_map\prj\emb"
definition
"prj = sfun_map\emb\prj oo sfun_prj"
definition
"defl (t::('a \! 'b) itself) = sfun_defl\DEFL('a)\DEFL('b)"
definition
"(liftemb :: ('a \! 'b) u \ udom u) = u_map\emb"
definition
"(liftprj :: udom u \ ('a \! 'b) u) = u_map\prj"
definition
"liftdefl (t::('a \! 'b) itself) = liftdefl_of\DEFL('a \! 'b)"
instance proof
show "ep_pair emb (prj :: udom \ 'a \! '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\DEFL('a \! 'b) = emb oo (prj :: udom \ 'a \! '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 (fact liftemb_sfun_def liftprj_sfun_def liftdefl_sfun_def)+
end
lemma DEFL_sfun:
"DEFL('a::domain \! 'b::domain) = sfun_defl\DEFL('a)\DEFL('b)"
by (rule defl_sfun_def)
subsubsection \<open>Continuous function space\<close>
instantiation cfun :: (predomain, "domain") "domain"
begin
definition
"emb = emb oo encode_cfun"
definition
"prj = decode_cfun oo prj"
definition
"defl (t::('a \ 'b) itself) = DEFL('a u \! 'b)"
definition
"(liftemb :: ('a \ 'b) u \ udom u) = u_map\emb"
definition
"(liftprj :: udom u \ ('a \ 'b) u) = u_map\prj"
definition
"liftdefl (t::('a \ 'b) itself) = liftdefl_of\DEFL('a \ 'b)"
instance proof
have "ep_pair encode_cfun decode_cfun"
by (rule ep_pair.intro, simp_all)
thus "ep_pair emb (prj :: udom \ 'a \ 'b)"
unfolding emb_cfun_def prj_cfun_def
using ep_pair_emb_prj by (rule ep_pair_comp)
show "cast\DEFL('a \ 'b) = emb oo (prj :: udom \ 'a \ 'b)"
unfolding emb_cfun_def prj_cfun_def defl_cfun_def
by (simp add: cast_DEFL cfcomp1)
qed (fact liftemb_cfun_def liftprj_cfun_def liftdefl_cfun_def)+
end
lemma DEFL_cfun:
"DEFL('a::predomain \ 'b::domain) = DEFL('a u \! 'b)"
by (rule defl_cfun_def)
subsubsection \<open>Strict product\<close>
instantiation sprod :: ("domain", "domain") "domain"
begin
definition
"emb = sprod_emb oo sprod_map\emb\emb"
definition
"prj = sprod_map\prj\prj oo sprod_prj"
definition
"defl (t::('a \ 'b) itself) = sprod_defl\DEFL('a)\DEFL('b)"
definition
"(liftemb :: ('a \ 'b) u \ udom u) = u_map\emb"
definition
"(liftprj :: udom u \ ('a \ 'b) u) = u_map\prj"
definition
"liftdefl (t::('a \ 'b) itself) = liftdefl_of\DEFL('a \ 'b)"
instance proof
show "ep_pair emb (prj :: udom \ 'a \ 'b)"
unfolding emb_sprod_def prj_sprod_def
by (intro ep_pair_comp ep_pair_sprod ep_pair_sprod_map ep_pair_emb_prj)
show "cast\DEFL('a \ 'b) = emb oo (prj :: udom \ 'a \ '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 (fact liftemb_sprod_def liftprj_sprod_def liftdefl_sprod_def)+
end
lemma DEFL_sprod:
"DEFL('a::domain \ 'b::domain) = sprod_defl\DEFL('a)\DEFL('b)"
by (rule defl_sprod_def)
subsubsection \<open>Cartesian product\<close>
definition prod_liftdefl :: "udom u defl \ udom u defl \ udom u defl"
where "prod_liftdefl = defl_fun2 (u_map\prod_emb oo decode_prod_u)
(encode_prod_u oo u_map\<cdot>prod_prj) sprod_map"
lemma cast_prod_liftdefl:
"cast\(prod_liftdefl\a\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 = (u_map\prod_emb oo decode_prod_u) oo
(sprod_map\<cdot>liftemb\<cdot>liftemb oo encode_prod_u)"
definition
"liftprj = (decode_prod_u oo sprod_map\liftprj\liftprj) oo
(encode_prod_u oo u_map\<cdot>prod_prj)"
definition
"liftdefl (t::('a \ 'b) itself) = prod_liftdefl\LIFTDEFL('a)\LIFTDEFL('b)"
instance proof
show "ep_pair liftemb (liftprj :: udom u \ ('a \ 'b) u)"
unfolding liftemb_prod_def liftprj_prod_def
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\LIFTDEFL('a \ 'b) = liftemb oo (liftprj :: udom u \ ('a \ 'b) u)"
unfolding liftemb_prod_def liftprj_prod_def liftdefl_prod_def
by (simp add: cast_prod_liftdefl cast_liftdefl cfcomp1 sprod_map_map)
qed
end
instantiation prod :: ("domain", "domain") "domain"
begin
definition
"emb = prod_emb oo prod_map\emb\emb"
definition
"prj = prod_map\prj\prj oo prod_prj"
definition
"defl (t::('a \ 'b) itself) = prod_defl\DEFL('a)\DEFL('b)"
instance proof
show 1: "ep_pair emb (prj :: udom \ 'a \ 'b)"
unfolding emb_prod_def prj_prod_def
by (intro ep_pair_comp ep_pair_prod ep_pair_prod_map ep_pair_emb_prj)
show 2: "cast\DEFL('a \ 'b) = emb oo (prj :: udom \ 'a \ 'b)"
unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl
by (simp add: cast_DEFL oo_def cfun_eq_iff prod_map_map)
show 3: "liftemb = u_map\(emb :: 'a \ 'b \ 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\(prj :: udom \ 'a \ '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\y", simp)
done
show 5: "LIFTDEFL('a \ 'b) = liftdefl_of\DEFL('a \ 'b)"
by (rule cast_eq_imp_eq)
(simp add: cast_liftdefl cast_liftdefl_of cast_DEFL 2 3 4 u_map_oo)
qed
end
lemma DEFL_prod:
"DEFL('a::domain \ 'b::domain) = prod_defl\DEFL('a)\DEFL('b)"
by (rule defl_prod_def)
lemma LIFTDEFL_prod:
"LIFTDEFL('a::predomain \ 'b::predomain) =
prod_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
by (rule liftdefl_prod_def)
subsubsection \<open>Unit type\<close>
instantiation unit :: "domain"
begin
definition
"emb = (\ :: unit \ udom)"
definition
"prj = (\ :: udom \ unit)"
definition
"defl (t::unit itself) = \"
definition
"(liftemb :: unit u \ udom u) = u_map\emb"
definition
"(liftprj :: udom u \ unit u) = u_map\prj"
definition
"liftdefl (t::unit itself) = liftdefl_of\DEFL(unit)"
instance proof
show "ep_pair emb (prj :: udom \ unit)"
unfolding emb_unit_def prj_unit_def
by (simp add: ep_pair.intro)
show "cast\DEFL(unit) = emb oo (prj :: udom \ unit)"
unfolding emb_unit_def prj_unit_def defl_unit_def by simp
qed (fact liftemb_unit_def liftprj_unit_def liftdefl_unit_def)+
end
subsubsection \<open>Discrete cpo\<close>
instantiation discr :: (countable) predomain
begin
definition
"(liftemb :: 'a discr u \ udom u) = strictify\up oo udom_emb discr_approx"
definition
"(liftprj :: udom u \ 'a discr u) = udom_prj discr_approx oo fup\ID"
definition
"liftdefl (t::'a discr itself) =
(\<Squnion>i. defl_principal (Abs_fin_defl (liftemb oo discr_approx i oo (liftprj::udom u \<rightarrow> 'a discr u))))"
instance proof
show 1: "ep_pair liftemb (liftprj :: udom u \ 'a discr u)"
unfolding liftemb_discr_def liftprj_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\LIFTDEFL('a discr) = liftemb oo (liftprj :: udom u \ '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 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 1]
approx_chain.finite_deflation_approx [OF discr_approx])
apply (simp add: lub_distribs)
done
qed
end
subsubsection \<open>Strict sum\<close>
instantiation ssum :: ("domain", "domain") "domain"
begin
definition
"emb = ssum_emb oo ssum_map\emb\emb"
definition
"prj = ssum_map\prj\prj oo ssum_prj"
definition
"defl (t::('a \ 'b) itself) = ssum_defl\DEFL('a)\DEFL('b)"
definition
"(liftemb :: ('a \ 'b) u \ udom u) = u_map\emb"
definition
"(liftprj :: udom u \ ('a \ 'b) u) = u_map\prj"
definition
"liftdefl (t::('a \ 'b) itself) = liftdefl_of\DEFL('a \ 'b)"
instance proof
show "ep_pair emb (prj :: udom \ 'a \ '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\DEFL('a \ 'b) = emb oo (prj :: udom \ 'a \ 'b)"
unfolding emb_ssum_def prj_ssum_def defl_ssum_def cast_ssum_defl
by (simp add: cast_DEFL oo_def cfun_eq_iff ssum_map_map)
qed (fact liftemb_ssum_def liftprj_ssum_def liftdefl_ssum_def)+
end
lemma DEFL_ssum:
"DEFL('a::domain \ 'b::domain) = ssum_defl\DEFL('a)\DEFL('b)"
by (rule defl_ssum_def)
subsubsection \<open>Lifted HOL type\<close>
instantiation lift :: (countable) "domain"
begin
definition
"emb = emb oo (\ x. Rep_lift x)"
definition
"prj = (\ y. Abs_lift y) oo prj"
definition
"defl (t::'a lift itself) = DEFL('a discr u)"
definition
"(liftemb :: 'a lift u \ udom u) = u_map\emb"
definition
"(liftprj :: udom u \ 'a lift u) = u_map\prj"
definition
"liftdefl (t::'a lift itself) = liftdefl_of\DEFL('a lift)"
instance proof
note [simp] = cont_Rep_lift cont_Abs_lift Rep_lift_inverse Abs_lift_inverse
have "ep_pair (\(x::'a lift). Rep_lift x) (\ y. Abs_lift y)"
by (simp add: ep_pair_def)
thus "ep_pair emb (prj :: udom \ 'a lift)"
unfolding emb_lift_def prj_lift_def
using ep_pair_emb_prj by (rule ep_pair_comp)
show "cast\DEFL('a lift) = emb oo (prj :: udom \ 'a lift)"
unfolding emb_lift_def prj_lift_def defl_lift_def cast_DEFL
by (simp add: cfcomp1)
qed (fact liftemb_lift_def liftprj_lift_def liftdefl_lift_def)+
end
end
¤ Dauer der Verarbeitung: 0.21 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
|
|
|
|
|
