--- a/src/HOLCF/Adm.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Adm.thy Fri Nov 12 12:57:02 2010 +0100
@@ -146,7 +146,7 @@
lemma compact_below_lub_iff:
"\<lbrakk>compact x; chain Y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. Y i) \<longleftrightarrow> (\<exists>i. x \<sqsubseteq> Y i)"
-by (fast intro: compactD2 elim: below_trans is_ub_thelub)
+by (fast intro: compactD2 elim: below_lub)
lemma compact_chfin [simp]: "compact (x::'a::chfin)"
by (rule compactI [OF adm_chfin])
--- a/src/HOLCF/Algebraic.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Algebraic.thy Fri Nov 12 12:57:02 2010 +0100
@@ -5,7 +5,7 @@
header {* Algebraic deflations *}
theory Algebraic
-imports Universal
+imports Universal Map_Functions
begin
subsection {* Type constructor for finite deflations *}
--- a/src/HOLCF/Bifinite.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Bifinite.thy Fri Nov 12 12:57:02 2010 +0100
@@ -5,19 +5,32 @@
header {* Bifinite domains *}
theory Bifinite
-imports Algebraic Cprod Sprod Ssum Up Lift One Tr Countable
+imports Algebraic Map_Functions Countable
begin
subsection {* Class of bifinite domains *}
text {*
- We define a bifinite domain as a pcpo that is isomorphic to some
- algebraic deflation over the universal domain.
+ 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.
*}
-class bifinite = pcpo +
- fixes emb :: "'a::pcpo \<rightarrow> udom"
- fixes prj :: "udom \<rightarrow> 'a::pcpo"
+class predomain = cpo +
+ fixes liftdefl :: "('a::cpo) itself \<Rightarrow> defl"
+ fixes liftemb :: "'a\<^sub>\<bottom> \<rightarrow> udom"
+ fixes liftprj :: "udom \<rightarrow> 'a\<^sub>\<bottom>"
+ assumes predomain_ep: "ep_pair liftemb liftprj"
+ assumes cast_liftdefl: "cast\<cdot>(liftdefl TYPE('a::cpo)) = liftemb oo liftprj"
+
+syntax "_LIFTDEFL" :: "type \<Rightarrow> logic" ("(1LIFTDEFL/(1'(_')))")
+translations "LIFTDEFL('t)" \<rightleftharpoons> "CONST liftdefl TYPE('t)"
+
+class "domain" = predomain + pcpo +
+ fixes emb :: "'a::cpo \<rightarrow> udom"
+ fixes prj :: "udom \<rightarrow> 'a::cpo"
fixes defl :: "'a itself \<Rightarrow> defl"
assumes ep_pair_emb_prj: "ep_pair emb prj"
assumes cast_DEFL: "cast\<cdot>(defl TYPE('a)) = emb oo prj"
@@ -25,26 +38,25 @@
syntax "_DEFL" :: "type \<Rightarrow> defl" ("(1DEFL/(1'(_')))")
translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)"
-interpretation bifinite:
- pcpo_ep_pair "emb :: 'a::bifinite \<rightarrow> udom" "prj :: udom \<rightarrow> 'a::bifinite"
+interpretation "domain": pcpo_ep_pair emb prj
unfolding pcpo_ep_pair_def
by (rule ep_pair_emb_prj)
-lemmas emb_inverse = bifinite.e_inverse
-lemmas emb_prj_below = bifinite.e_p_below
-lemmas emb_eq_iff = bifinite.e_eq_iff
-lemmas emb_strict = bifinite.e_strict
-lemmas prj_strict = bifinite.p_strict
+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 {* Bifinite domains have a countable compact basis *}
+subsection {* Domains have a countable compact basis *}
text {*
Eventually it should be possible to generalize this to an unpointed
- variant of the bifinite class.
+ variant of the domain class.
*}
interpretation compact_basis:
- ideal_completion below Rep_compact_basis "approximants::'a::bifinite \<Rightarrow> _"
+ ideal_completion below Rep_compact_basis "approximants::'a::domain \<Rightarrow> _"
proof -
obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)"
and DEFL: "DEFL('a) = (\<Squnion>i. defl_principal (Y i))"
@@ -59,7 +71,7 @@
by (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL cfun_eq_iff)
show "\<And>i. finite_deflation (approx i)"
unfolding approx_def
- apply (rule bifinite.finite_deflation_p_d_e)
+ apply (rule domain.finite_deflation_p_d_e)
apply (rule finite_deflation_cast)
apply (rule defl.compact_principal)
apply (rule below_trans [OF monofun_cfun_fun])
@@ -71,6 +83,58 @@
show "ideal_completion below Rep_compact_basis (approximants::'a \<Rightarrow> _)" ..
qed
+subsection {* Chains of approx functions *}
+
+definition u_approx :: "nat \<Rightarrow> udom\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
+ where "u_approx = (\<lambda>i. u_map\<cdot>(udom_approx i))"
+
+definition cfun_approx :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom)"
+ where "cfun_approx = (\<lambda>i. cfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+
+definition prod_approx :: "nat \<Rightarrow> udom \<times> udom \<rightarrow> udom \<times> udom"
+ where "prod_approx = (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+
+definition sprod_approx :: "nat \<Rightarrow> udom \<otimes> udom \<rightarrow> udom \<otimes> udom"
+ where "sprod_approx = (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+
+definition ssum_approx :: "nat \<Rightarrow> udom \<oplus> udom \<rightarrow> udom \<oplus> udom"
+ where "ssum_approx = (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+
+lemma approx_chain_lemma1:
+ assumes "m\<cdot>ID = ID"
+ assumes "\<And>d. finite_deflation d \<Longrightarrow> finite_deflation (m\<cdot>d)"
+ shows "approx_chain (\<lambda>i. m\<cdot>(udom_approx i))"
+by (rule approx_chain.intro)
+ (simp_all add: lub_distribs finite_deflation_udom_approx assms)
+
+lemma approx_chain_lemma2:
+ assumes "m\<cdot>ID\<cdot>ID = ID"
+ assumes "\<And>a b. \<lbrakk>finite_deflation a; finite_deflation b\<rbrakk>
+ \<Longrightarrow> finite_deflation (m\<cdot>a\<cdot>b)"
+ shows "approx_chain (\<lambda>i. m\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+by (rule approx_chain.intro)
+ (simp_all add: lub_distribs finite_deflation_udom_approx assms)
+
+lemma u_approx: "approx_chain u_approx"
+using u_map_ID finite_deflation_u_map
+unfolding u_approx_def by (rule approx_chain_lemma1)
+
+lemma cfun_approx: "approx_chain cfun_approx"
+using cfun_map_ID finite_deflation_cfun_map
+unfolding cfun_approx_def by (rule approx_chain_lemma2)
+
+lemma prod_approx: "approx_chain prod_approx"
+using cprod_map_ID finite_deflation_cprod_map
+unfolding prod_approx_def by (rule approx_chain_lemma2)
+
+lemma sprod_approx: "approx_chain sprod_approx"
+using sprod_map_ID finite_deflation_sprod_map
+unfolding sprod_approx_def by (rule approx_chain_lemma2)
+
+lemma ssum_approx: "approx_chain ssum_approx"
+using ssum_map_ID finite_deflation_ssum_map
+unfolding ssum_approx_def by (rule approx_chain_lemma2)
+
subsection {* Type combinators *}
definition
@@ -144,9 +208,111 @@
Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
qed
-subsection {* The universal domain is bifinite *}
+definition u_defl :: "defl \<rightarrow> defl"
+ where "u_defl = defl_fun1 u_approx u_map"
+
+definition cfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+ where "cfun_defl = defl_fun2 cfun_approx cfun_map"
+
+definition prod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+ where "prod_defl = defl_fun2 prod_approx cprod_map"
+
+definition sprod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+ where "sprod_defl = defl_fun2 sprod_approx sprod_map"
+
+definition ssum_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+where "ssum_defl = defl_fun2 ssum_approx ssum_map"
+
+lemma cast_u_defl:
+ "cast\<cdot>(u_defl\<cdot>A) =
+ udom_emb u_approx oo u_map\<cdot>(cast\<cdot>A) oo udom_prj u_approx"
+using u_approx finite_deflation_u_map
+unfolding u_defl_def by (rule cast_defl_fun1)
+
+lemma cast_cfun_defl:
+ "cast\<cdot>(cfun_defl\<cdot>A\<cdot>B) =
+ udom_emb cfun_approx oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj cfun_approx"
+using cfun_approx finite_deflation_cfun_map
+unfolding cfun_defl_def by (rule cast_defl_fun2)
+
+lemma cast_prod_defl:
+ "cast\<cdot>(prod_defl\<cdot>A\<cdot>B) = udom_emb prod_approx oo
+ cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj prod_approx"
+using prod_approx finite_deflation_cprod_map
+unfolding prod_defl_def by (rule cast_defl_fun2)
+
+lemma cast_sprod_defl:
+ "cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) =
+ udom_emb sprod_approx oo
+ sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo
+ udom_prj sprod_approx"
+using sprod_approx finite_deflation_sprod_map
+unfolding sprod_defl_def by (rule cast_defl_fun2)
+
+lemma cast_ssum_defl:
+ "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) =
+ udom_emb ssum_approx oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj ssum_approx"
+using ssum_approx finite_deflation_ssum_map
+unfolding ssum_defl_def by (rule cast_defl_fun2)
+
+subsection {* Lemma for proving domain instances *}
-instantiation udom :: bifinite
+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 = udom_emb u_approx oo u_map\<cdot>emb"
+ assumes liftprj_eq: "liftprj = u_map\<cdot>prj oo udom_prj u_approx"
+ 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> defl"})
+ , (@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"})
+ , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::pcpo"})
+ , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"})
+ , (@{const_name liftemb}, SOME @{typ "'a::pcpo u \<rightarrow> udom"})
+ , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::pcpo u"}) ]
+*}
+
+lemma liftdomain_class_intro:
+ assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+ assumes liftprj: "(liftprj :: udom \<rightarrow> 'a u) = u_map\<cdot>prj oo udom_prj u_approx"
+ assumes liftdefl: "liftdefl TYPE('a) = u_defl\<cdot>DEFL('a)"
+ assumes ep_pair: "ep_pair emb (prj :: udom \<rightarrow> 'a)"
+ assumes cast_defl: "cast\<cdot>DEFL('a) = emb oo (prj :: udom \<rightarrow> 'a)"
+ shows "OFCLASS('a, 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_udom u_approx)
+ show "cast\<cdot>LIFTDEFL('a) = liftemb oo (liftprj :: udom \<rightarrow> 'a u)"
+ unfolding liftemb liftprj liftdefl
+ by (simp add: cfcomp1 cast_u_defl cast_defl u_map_map)
+next
+qed fact+
+
+text {* Restore original type constraints. *}
+
+setup {*
+ fold Sign.add_const_constraint
+ [ (@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> 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> 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
begin
definition [simp]:
@@ -158,10 +324,20 @@
definition
"defl (t::udom itself) = (\<Squnion>i. defl_principal (Abs_fin_defl (udom_approx i)))"
-instance proof
+definition
+ "(liftemb :: udom u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> udom u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl (t::udom itself) = u_defl\<cdot>DEFL(udom)"
+
+instance
+using liftemb_udom_def liftprj_udom_def liftdefl_udom_def
+proof (rule liftdomain_class_intro)
show "ep_pair emb (prj :: udom \<rightarrow> udom)"
by (simp add: ep_pair.intro)
-next
show "cast\<cdot>DEFL(udom) = emb oo (prj :: udom \<rightarrow> udom)"
unfolding defl_udom_def
apply (subst contlub_cfun_arg)
@@ -178,37 +354,50 @@
end
-subsection {* Continuous function space is a bifinite domain *}
+subsubsection {* Lifted cpo *}
+
+instantiation u :: (predomain) liftdomain
+begin
+
+definition
+ "emb = liftemb"
+
+definition
+ "prj = liftprj"
+
+definition
+ "defl (t::'a u itself) = LIFTDEFL('a)"
+
+definition
+ "(liftemb :: 'a u u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> 'a u u) = u_map\<cdot>prj oo udom_prj u_approx"
definition
- cfun_approx :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom)"
-where
- "cfun_approx = (\<lambda>i. cfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+ "liftdefl (t::'a u itself) = u_defl\<cdot>DEFL('a u)"
-lemma cfun_approx: "approx_chain cfun_approx"
-proof (rule approx_chain.intro)
- show "chain (\<lambda>i. cfun_approx i)"
- unfolding cfun_approx_def by simp
- show "(\<Squnion>i. cfun_approx i) = ID"
- unfolding cfun_approx_def
- by (simp add: lub_distribs cfun_map_ID)
- show "\<And>i. finite_deflation (cfun_approx i)"
- unfolding cfun_approx_def
- by (intro finite_deflation_cfun_map finite_deflation_udom_approx)
+instance
+using liftemb_u_def liftprj_u_def liftdefl_u_def
+proof (rule liftdomain_class_intro)
+ show "ep_pair emb (prj :: udom \<rightarrow> 'a u)"
+ unfolding emb_u_def prj_u_def
+ by (rule predomain_ep)
+ show "cast\<cdot>DEFL('a u) = emb oo (prj :: udom \<rightarrow> 'a u)"
+ unfolding emb_u_def prj_u_def defl_u_def
+ by (rule cast_liftdefl)
qed
-definition cfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
-where "cfun_defl = defl_fun2 cfun_approx cfun_map"
+end
+
+lemma DEFL_u: "DEFL('a::predomain u) = LIFTDEFL('a)"
+by (rule defl_u_def)
-lemma cast_cfun_defl:
- "cast\<cdot>(cfun_defl\<cdot>A\<cdot>B) =
- udom_emb cfun_approx oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj cfun_approx"
-unfolding cfun_defl_def
-apply (rule cast_defl_fun2 [OF cfun_approx])
-apply (erule (1) finite_deflation_cfun_map)
-done
+subsubsection {* Continuous function space *}
-instantiation cfun :: (bifinite, bifinite) bifinite
+text {* TODO: Allow argument type to be a predomain. *}
+
+instantiation cfun :: ("domain", "domain") liftdomain
begin
definition
@@ -220,12 +409,22 @@
definition
"defl (t::('a \<rightarrow> 'b) itself) = cfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
-instance proof
+definition
+ "(liftemb :: ('a \<rightarrow> 'b) u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> ('a \<rightarrow> 'b) u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl (t::('a \<rightarrow> 'b) itself) = u_defl\<cdot>DEFL('a \<rightarrow> 'b)"
+
+instance
+using liftemb_cfun_def liftprj_cfun_def liftdefl_cfun_def
+proof (rule liftdomain_class_intro)
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
unfolding emb_cfun_def prj_cfun_def
using ep_pair_udom [OF cfun_approx]
by (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj)
-next
show "cast\<cdot>DEFL('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
unfolding emb_cfun_def prj_cfun_def defl_cfun_def cast_cfun_defl
by (simp add: cast_DEFL oo_def cfun_eq_iff cfun_map_map)
@@ -234,40 +433,63 @@
end
lemma DEFL_cfun:
- "DEFL('a::bifinite \<rightarrow> 'b::bifinite) = cfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+ "DEFL('a::domain \<rightarrow> 'b::domain) = cfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
by (rule defl_cfun_def)
-subsection {* Cartesian product is a bifinite domain *}
+subsubsection {* Cartesian product *}
+
+text {*
+ Types @{typ "('a * 'b) u"} and @{typ "'a u \<otimes> 'b u"} are isomorphic.
+*}
+
+definition
+ "encode_prod_u = (\<Lambda>(up\<cdot>(x, y)). (:up\<cdot>x, up\<cdot>y:))"
+
+definition
+ "decode_prod_u = (\<Lambda>(:up\<cdot>x, up\<cdot>y:). up\<cdot>(x, y))"
+
+lemma decode_encode_prod_u [simp]: "decode_prod_u\<cdot>(encode_prod_u\<cdot>x) = x"
+unfolding encode_prod_u_def decode_prod_u_def
+by (case_tac x, simp, rename_tac y, case_tac y, simp)
+
+lemma encode_decode_prod_u [simp]: "encode_prod_u\<cdot>(decode_prod_u\<cdot>y) = y"
+unfolding encode_prod_u_def decode_prod_u_def
+apply (case_tac y, simp, rename_tac a b)
+apply (case_tac a, simp, case_tac b, simp, simp)
+done
+
+instantiation prod :: (predomain, predomain) predomain
+begin
definition
- prod_approx :: "nat \<Rightarrow> udom \<times> udom \<rightarrow> udom \<times> udom"
-where
- "prod_approx = (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+ "liftemb =
+ (udom_emb sprod_approx oo sprod_map\<cdot>emb\<cdot>emb) oo encode_prod_u"
+
+definition
+ "liftprj =
+ decode_prod_u oo (sprod_map\<cdot>prj\<cdot>prj oo udom_prj sprod_approx)"
+
+definition
+ "liftdefl (t::('a \<times> 'b) itself) = sprod_defl\<cdot>DEFL('a u)\<cdot>DEFL('b u)"
-lemma prod_approx: "approx_chain prod_approx"
-proof (rule approx_chain.intro)
- show "chain (\<lambda>i. prod_approx i)"
- unfolding prod_approx_def by simp
- show "(\<Squnion>i. prod_approx i) = ID"
- unfolding prod_approx_def
- by (simp add: lub_distribs cprod_map_ID)
- show "\<And>i. finite_deflation (prod_approx i)"
- unfolding prod_approx_def
- by (intro finite_deflation_cprod_map finite_deflation_udom_approx)
+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)"
+ unfolding liftemb_prod_def liftprj_prod_def
+ apply (rule ep_pair_comp)
+ apply (rule ep_pair_comp)
+ apply (intro ep_pair_sprod_map ep_pair_emb_prj)
+ apply (rule ep_pair_udom [OF sprod_approx])
+ done
+ show "cast\<cdot>LIFTDEFL('a \<times> 'b) = liftemb oo (liftprj :: udom \<rightarrow> ('a \<times> 'b) u)"
+ unfolding liftemb_prod_def liftprj_prod_def liftdefl_prod_def
+ by (simp add: cast_sprod_defl cast_DEFL cfcomp1 sprod_map_map)
qed
-definition prod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
-where "prod_defl = defl_fun2 prod_approx cprod_map"
+end
-lemma cast_prod_defl:
- "cast\<cdot>(prod_defl\<cdot>A\<cdot>B) = udom_emb prod_approx oo
- cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj prod_approx"
-unfolding prod_defl_def
-apply (rule cast_defl_fun2 [OF prod_approx])
-apply (erule (1) finite_deflation_cprod_map)
-done
-
-instantiation prod :: (bifinite, bifinite) bifinite
+instantiation prod :: ("domain", "domain") "domain"
begin
definition
@@ -293,42 +515,16 @@
end
lemma DEFL_prod:
- "DEFL('a::bifinite \<times> 'b::bifinite) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+ "DEFL('a::domain \<times> 'b::domain) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
by (rule defl_prod_def)
-subsection {* Strict product is a bifinite domain *}
-
-definition
- sprod_approx :: "nat \<Rightarrow> udom \<otimes> udom \<rightarrow> udom \<otimes> udom"
-where
- "sprod_approx = (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+lemma LIFTDEFL_prod:
+ "LIFTDEFL('a::predomain \<times> 'b::predomain) = sprod_defl\<cdot>DEFL('a u)\<cdot>DEFL('b u)"
+by (rule liftdefl_prod_def)
-lemma sprod_approx: "approx_chain sprod_approx"
-proof (rule approx_chain.intro)
- show "chain (\<lambda>i. sprod_approx i)"
- unfolding sprod_approx_def by simp
- show "(\<Squnion>i. sprod_approx i) = ID"
- unfolding sprod_approx_def
- by (simp add: lub_distribs sprod_map_ID)
- show "\<And>i. finite_deflation (sprod_approx i)"
- unfolding sprod_approx_def
- by (intro finite_deflation_sprod_map finite_deflation_udom_approx)
-qed
+subsubsection {* Strict product *}
-definition sprod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
-where "sprod_defl = defl_fun2 sprod_approx sprod_map"
-
-lemma cast_sprod_defl:
- "cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) =
- udom_emb sprod_approx oo
- sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo
- udom_prj sprod_approx"
-unfolding sprod_defl_def
-apply (rule cast_defl_fun2 [OF sprod_approx])
-apply (erule (1) finite_deflation_sprod_map)
-done
-
-instantiation sprod :: (bifinite, bifinite) bifinite
+instantiation sprod :: ("domain", "domain") liftdomain
begin
definition
@@ -340,7 +536,18 @@
definition
"defl (t::('a \<otimes> 'b) itself) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
-instance proof
+definition
+ "(liftemb :: ('a \<otimes> 'b) u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> ('a \<otimes> 'b) u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl (t::('a \<otimes> 'b) itself) = u_defl\<cdot>DEFL('a \<otimes> 'b)"
+
+instance
+using liftemb_sprod_def liftprj_sprod_def liftdefl_sprod_def
+proof (rule liftdomain_class_intro)
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
unfolding emb_sprod_def prj_sprod_def
using ep_pair_udom [OF sprod_approx]
@@ -354,80 +561,22 @@
end
lemma DEFL_sprod:
- "DEFL('a::bifinite \<otimes> 'b::bifinite) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+ "DEFL('a::domain \<otimes> 'b::domain) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
by (rule defl_sprod_def)
-subsection {* Lifted cpo is a bifinite domain *}
-
-definition u_approx :: "nat \<Rightarrow> udom\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
-where "u_approx = (\<lambda>i. u_map\<cdot>(udom_approx i))"
-
-lemma u_approx: "approx_chain u_approx"
-proof (rule approx_chain.intro)
- show "chain (\<lambda>i. u_approx i)"
- unfolding u_approx_def by simp
- show "(\<Squnion>i. u_approx i) = ID"
- unfolding u_approx_def
- by (simp add: lub_distribs u_map_ID)
- show "\<And>i. finite_deflation (u_approx i)"
- unfolding u_approx_def
- by (intro finite_deflation_u_map finite_deflation_udom_approx)
-qed
+subsubsection {* Discrete cpo *}
-definition u_defl :: "defl \<rightarrow> defl"
-where "u_defl = defl_fun1 u_approx u_map"
-
-lemma cast_u_defl:
- "cast\<cdot>(u_defl\<cdot>A) =
- udom_emb u_approx oo u_map\<cdot>(cast\<cdot>A) oo udom_prj u_approx"
-unfolding u_defl_def
-apply (rule cast_defl_fun1 [OF u_approx])
-apply (erule finite_deflation_u_map)
-done
-
-instantiation u :: (bifinite) bifinite
-begin
-
-definition
- "emb = udom_emb u_approx oo u_map\<cdot>emb"
+definition discr_approx :: "nat \<Rightarrow> 'a::countable discr u \<rightarrow> 'a discr u"
+ where "discr_approx = (\<lambda>i. \<Lambda>(up\<cdot>x). if to_nat (undiscr x) < i then up\<cdot>x else \<bottom>)"
-definition
- "prj = u_map\<cdot>prj oo udom_prj u_approx"
-
-definition
- "defl (t::'a u itself) = u_defl\<cdot>DEFL('a)"
-
-instance proof
- show "ep_pair emb (prj :: udom \<rightarrow> 'a u)"
- unfolding emb_u_def prj_u_def
- using ep_pair_udom [OF u_approx]
- by (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj)
-next
- show "cast\<cdot>DEFL('a u) = emb oo (prj :: udom \<rightarrow> 'a u)"
- unfolding emb_u_def prj_u_def defl_u_def cast_u_defl
- by (simp add: cast_DEFL oo_def cfun_eq_iff u_map_map)
-qed
+lemma chain_discr_approx [simp]: "chain discr_approx"
+unfolding discr_approx_def
+by (rule chainI, simp add: monofun_cfun monofun_LAM)
-end
-
-lemma DEFL_u: "DEFL('a::bifinite u) = u_defl\<cdot>DEFL('a)"
-by (rule defl_u_def)
-
-subsection {* Lifted countable types are bifinite domains *}
-
-definition
- lift_approx :: "nat \<Rightarrow> 'a::countable lift \<rightarrow> 'a lift"
-where
- "lift_approx = (\<lambda>i. FLIFT x. if to_nat x < i then Def x else \<bottom>)"
-
-lemma chain_lift_approx [simp]: "chain lift_approx"
- unfolding lift_approx_def
- by (rule chainI, simp add: FLIFT_mono)
-
-lemma lub_lift_approx [simp]: "(\<Squnion>i. lift_approx i) = ID"
+lemma lub_discr_approx [simp]: "(\<Squnion>i. discr_approx i) = ID"
apply (rule cfun_eqI)
apply (simp add: contlub_cfun_fun)
-apply (simp add: lift_approx_def)
+apply (simp add: discr_approx_def)
apply (case_tac x, simp)
apply (rule thelubI)
apply (rule is_lubI)
@@ -438,97 +587,75 @@
apply (rule lessI)
done
-lemma finite_deflation_lift_approx: "finite_deflation (lift_approx i)"
+lemma inj_on_undiscr [simp]: "inj_on undiscr A"
+using Discr_undiscr by (rule inj_on_inverseI)
+
+lemma finite_deflation_discr_approx: "finite_deflation (discr_approx i)"
proof
- fix x :: "'a lift"
- show "lift_approx i\<cdot>x \<sqsubseteq> x"
- unfolding lift_approx_def
+ fix x :: "'a discr u"
+ show "discr_approx i\<cdot>x \<sqsubseteq> x"
+ unfolding discr_approx_def
by (cases x, simp, simp)
- show "lift_approx i\<cdot>(lift_approx i\<cdot>x) = lift_approx i\<cdot>x"
- unfolding lift_approx_def
+ show "discr_approx i\<cdot>(discr_approx i\<cdot>x) = discr_approx i\<cdot>x"
+ unfolding discr_approx_def
by (cases x, simp, simp)
- show "finite {x::'a lift. lift_approx i\<cdot>x = x}"
+ show "finite {x::'a discr u. discr_approx i\<cdot>x = x}"
proof (rule finite_subset)
- let ?S = "insert (\<bottom>::'a lift) (Def ` to_nat -` {..<i})"
- show "{x::'a lift. lift_approx i\<cdot>x = x} \<subseteq> ?S"
- unfolding lift_approx_def
+ let ?S = "insert (\<bottom>::'a discr u) ((\<lambda>x. up\<cdot>x) ` undiscr -` to_nat -` {..<i})"
+ show "{x::'a discr u. discr_approx i\<cdot>x = x} \<subseteq> ?S"
+ unfolding discr_approx_def
by (rule subsetI, case_tac x, simp, simp split: split_if_asm)
show "finite ?S"
by (simp add: finite_vimageI)
qed
qed
-lemma lift_approx: "approx_chain lift_approx"
-using chain_lift_approx lub_lift_approx finite_deflation_lift_approx
+lemma discr_approx: "approx_chain discr_approx"
+using chain_discr_approx lub_discr_approx finite_deflation_discr_approx
by (rule approx_chain.intro)
-instantiation lift :: (countable) bifinite
+instantiation discr :: (countable) predomain
begin
definition
- "emb = udom_emb lift_approx"
+ "liftemb = udom_emb discr_approx"
definition
- "prj = udom_prj lift_approx"
+ "liftprj = udom_prj discr_approx"
definition
- "defl (t::'a lift itself) =
- (\<Squnion>i. defl_principal (Abs_fin_defl (emb oo lift_approx i oo prj)))"
+ "liftdefl (t::'a discr itself) =
+ (\<Squnion>i. defl_principal (Abs_fin_defl (liftemb oo discr_approx i oo liftprj)))"
instance proof
- show ep: "ep_pair emb (prj :: udom \<rightarrow> 'a lift)"
- unfolding emb_lift_def prj_lift_def
- by (rule ep_pair_udom [OF lift_approx])
- show "cast\<cdot>DEFL('a lift) = emb oo (prj :: udom \<rightarrow> 'a lift)"
- unfolding defl_lift_def
+ show "ep_pair liftemb (liftprj :: udom \<rightarrow> 'a discr u)"
+ unfolding liftemb_discr_def liftprj_discr_def
+ by (rule ep_pair_udom [OF discr_approx])
+ show "cast\<cdot>LIFTDEFL('a discr) = liftemb oo (liftprj :: udom \<rightarrow> 'a discr u)"
+ unfolding liftemb_discr_def liftprj_discr_def liftdefl_discr_def
apply (subst contlub_cfun_arg)
apply (rule chainI)
apply (rule defl.principal_mono)
apply (simp add: below_fin_defl_def)
- apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx
- ep_pair.finite_deflation_e_d_p [OF ep])
+ apply (simp add: Abs_fin_defl_inverse
+ ep_pair.finite_deflation_e_d_p [OF ep_pair_udom [OF discr_approx]]
+ approx_chain.finite_deflation_approx [OF discr_approx])
apply (intro monofun_cfun below_refl)
apply (rule chainE)
- apply (rule chain_lift_approx)
+ apply (rule chain_discr_approx)
apply (subst cast_defl_principal)
- apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx
- ep_pair.finite_deflation_e_d_p [OF ep] lub_distribs)
+ apply (simp add: Abs_fin_defl_inverse
+ ep_pair.finite_deflation_e_d_p [OF ep_pair_udom [OF discr_approx]]
+ approx_chain.finite_deflation_approx [OF discr_approx])
+ apply (simp add: lub_distribs)
done
qed
end
-subsection {* Strict sum is a bifinite domain *}
-
-definition
- ssum_approx :: "nat \<Rightarrow> udom \<oplus> udom \<rightarrow> udom \<oplus> udom"
-where
- "ssum_approx = (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+subsubsection {* Strict sum *}
-lemma ssum_approx: "approx_chain ssum_approx"
-proof (rule approx_chain.intro)
- show "chain (\<lambda>i. ssum_approx i)"
- unfolding ssum_approx_def by simp
- show "(\<Squnion>i. ssum_approx i) = ID"
- unfolding ssum_approx_def
- by (simp add: lub_distribs ssum_map_ID)
- show "\<And>i. finite_deflation (ssum_approx i)"
- unfolding ssum_approx_def
- by (intro finite_deflation_ssum_map finite_deflation_udom_approx)
-qed
-
-definition ssum_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
-where "ssum_defl = defl_fun2 ssum_approx ssum_map"
-
-lemma cast_ssum_defl:
- "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) =
- udom_emb ssum_approx oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj ssum_approx"
-unfolding ssum_defl_def
-apply (rule cast_defl_fun2 [OF ssum_approx])
-apply (erule (1) finite_deflation_ssum_map)
-done
-
-instantiation ssum :: (bifinite, bifinite) bifinite
+instantiation ssum :: ("domain", "domain") liftdomain
begin
definition
@@ -540,12 +667,22 @@
definition
"defl (t::('a \<oplus> 'b) itself) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
-instance proof
+definition
+ "(liftemb :: ('a \<oplus> 'b) u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> ('a \<oplus> 'b) u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl (t::('a \<oplus> 'b) itself) = u_defl\<cdot>DEFL('a \<oplus> 'b)"
+
+instance
+using liftemb_ssum_def liftprj_ssum_def liftdefl_ssum_def
+proof (rule liftdomain_class_intro)
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
unfolding emb_ssum_def prj_ssum_def
using ep_pair_udom [OF ssum_approx]
by (intro ep_pair_comp ep_pair_ssum_map ep_pair_emb_prj)
-next
show "cast\<cdot>DEFL('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
unfolding emb_ssum_def prj_ssum_def defl_ssum_def cast_ssum_defl
by (simp add: cast_DEFL oo_def cfun_eq_iff ssum_map_map)
@@ -554,7 +691,46 @@
end
lemma DEFL_ssum:
- "DEFL('a::bifinite \<oplus> 'b::bifinite) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+ "DEFL('a::domain \<oplus> 'b::domain) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
by (rule defl_ssum_def)
+subsubsection {* Lifted HOL type *}
+
+instantiation lift :: (countable) liftdomain
+begin
+
+definition
+ "emb = emb oo (\<Lambda> x. Rep_lift x)"
+
+definition
+ "prj = (\<Lambda> y. Abs_lift y) oo prj"
+
+definition
+ "defl (t::'a lift itself) = DEFL('a discr u)"
+
+definition
+ "(liftemb :: 'a lift u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> 'a lift u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl (t::'a lift itself) = u_defl\<cdot>DEFL('a lift)"
+
+instance
+using liftemb_lift_def liftprj_lift_def liftdefl_lift_def
+proof (rule liftdomain_class_intro)
+ note [simp] = cont_Rep_lift cont_Abs_lift Rep_lift_inverse Abs_lift_inverse
+ have "ep_pair (\<Lambda>(x::'a lift). Rep_lift x) (\<Lambda> y. Abs_lift y)"
+ by (simp add: ep_pair_def)
+ thus "ep_pair emb (prj :: udom \<rightarrow> 'a lift)"
+ unfolding emb_lift_def prj_lift_def
+ using ep_pair_emb_prj by (rule ep_pair_comp)
+ show "cast\<cdot>DEFL('a lift) = emb oo (prj :: udom \<rightarrow> 'a lift)"
+ unfolding emb_lift_def prj_lift_def defl_lift_def cast_DEFL
+ by (simp add: cfcomp1)
+qed
+
end
+
+end
--- a/src/HOLCF/Cfun.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Cfun.thy Fri Nov 12 12:57:02 2010 +0100
@@ -479,24 +479,6 @@
lemma assoc_oo: "f oo (g oo h) = (f oo g) oo h"
by (rule cfun_eqI, simp)
-subsection {* Map operator for continuous function space *}
-
-definition
- cfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)"
-where
- "cfun_map = (\<Lambda> a b f x. b\<cdot>(f\<cdot>(a\<cdot>x)))"
-
-lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))"
-unfolding cfun_map_def by simp
-
-lemma cfun_map_ID: "cfun_map\<cdot>ID\<cdot>ID = ID"
-unfolding cfun_eq_iff by simp
-
-lemma cfun_map_map:
- "cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
- cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
-by (rule cfun_eqI) simp
-
subsection {* Strictified functions *}
default_sort pcpo
--- a/src/HOLCF/CompactBasis.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/CompactBasis.thy Fri Nov 12 12:57:02 2010 +0100
@@ -8,7 +8,7 @@
imports Bifinite
begin
-default_sort bifinite
+default_sort "domain"
subsection {* A compact basis for powerdomains *}
--- a/src/HOLCF/Completion.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Completion.thy Fri Nov 12 12:57:02 2010 +0100
@@ -5,7 +5,7 @@
header {* Defining algebraic domains by ideal completion *}
theory Completion
-imports Cfun
+imports Plain_HOLCF
begin
subsection {* Ideals over a preorder *}
@@ -351,11 +351,9 @@
apply (rule ub_imageI, rename_tac a)
apply (clarsimp simp add: rep_x)
apply (drule f_mono)
- apply (erule below_trans)
- apply (rule is_ub_thelub [OF chain])
- apply (rule is_lub_thelub [OF chain])
- apply (rule ub_rangeI)
- apply (drule_tac x="Y i" in ub_imageD)
+ apply (erule below_lub [OF chain])
+ apply (rule lub_below [OF chain])
+ apply (drule_tac x="Y n" in ub_imageD)
apply (simp add: rep_x, fast intro: r_refl)
apply assumption
done
--- a/src/HOLCF/ConvexPD.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/ConvexPD.thy Fri Nov 12 12:57:02 2010 +0100
@@ -123,7 +123,7 @@
"{S::'a pd_basis set. convex_le.ideal S}"
by (fast intro: convex_le.ideal_principal)
-instantiation convex_pd :: (bifinite) below
+instantiation convex_pd :: ("domain") below
begin
definition
@@ -132,11 +132,11 @@
instance ..
end
-instance convex_pd :: (bifinite) po
+instance convex_pd :: ("domain") po
using type_definition_convex_pd below_convex_pd_def
by (rule convex_le.typedef_ideal_po)
-instance convex_pd :: (bifinite) cpo
+instance convex_pd :: ("domain") cpo
using type_definition_convex_pd below_convex_pd_def
by (rule convex_le.typedef_ideal_cpo)
@@ -155,7 +155,7 @@
lemma convex_pd_minimal: "convex_principal (PDUnit compact_bot) \<sqsubseteq> ys"
by (induct ys rule: convex_pd.principal_induct, simp, simp)
-instance convex_pd :: (bifinite) pcpo
+instance convex_pd :: ("domain") pcpo
by intro_classes (fast intro: convex_pd_minimal)
lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)"
@@ -440,7 +440,7 @@
by (rule finite_range_imp_finite_fixes)
qed
-subsection {* Convex powerdomain is a bifinite domain *}
+subsection {* Convex powerdomain is a domain *}
definition
convex_approx :: "nat \<Rightarrow> udom convex_pd \<rightarrow> udom convex_pd"
@@ -448,16 +448,8 @@
"convex_approx = (\<lambda>i. convex_map\<cdot>(udom_approx i))"
lemma convex_approx: "approx_chain convex_approx"
-proof (rule approx_chain.intro)
- show "chain (\<lambda>i. convex_approx i)"
- unfolding convex_approx_def by simp
- show "(\<Squnion>i. convex_approx i) = ID"
- unfolding convex_approx_def
- by (simp add: lub_distribs convex_map_ID)
- show "\<And>i. finite_deflation (convex_approx i)"
- unfolding convex_approx_def
- by (intro finite_deflation_convex_map finite_deflation_udom_approx)
-qed
+using convex_map_ID finite_deflation_convex_map
+unfolding convex_approx_def by (rule approx_chain_lemma1)
definition convex_defl :: "defl \<rightarrow> defl"
where "convex_defl = defl_fun1 convex_approx convex_map"
@@ -465,12 +457,10 @@
lemma cast_convex_defl:
"cast\<cdot>(convex_defl\<cdot>A) =
udom_emb convex_approx oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj convex_approx"
-unfolding convex_defl_def
-apply (rule cast_defl_fun1 [OF convex_approx])
-apply (erule finite_deflation_convex_map)
-done
+using convex_approx finite_deflation_convex_map
+unfolding convex_defl_def by (rule cast_defl_fun1)
-instantiation convex_pd :: (bifinite) bifinite
+instantiation convex_pd :: ("domain") liftdomain
begin
definition
@@ -482,7 +472,18 @@
definition
"defl (t::'a convex_pd itself) = convex_defl\<cdot>DEFL('a)"
-instance proof
+definition
+ "(liftemb :: 'a convex_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl (t::'a convex_pd itself) = u_defl\<cdot>DEFL('a convex_pd)"
+
+instance
+using liftemb_convex_pd_def liftprj_convex_pd_def liftdefl_convex_pd_def
+proof (rule liftdomain_class_intro)
show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)"
unfolding emb_convex_pd_def prj_convex_pd_def
using ep_pair_udom [OF convex_approx]
--- a/src/HOLCF/Cprod.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Cprod.thy Fri Nov 12 12:57:02 2010 +0100
@@ -5,7 +5,7 @@
header {* The cpo of cartesian products *}
theory Cprod
-imports Deflation
+imports Cfun
begin
default_sort cpo
@@ -40,61 +40,4 @@
lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y"
by (simp add: csplit_def)
-subsection {* Map operator for product type *}
-
-definition
- cprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
-where
- "cprod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))"
-
-lemma cprod_map_Pair [simp]: "cprod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
-unfolding cprod_map_def by simp
-
-lemma cprod_map_ID: "cprod_map\<cdot>ID\<cdot>ID = ID"
-unfolding cfun_eq_iff by auto
-
-lemma cprod_map_map:
- "cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
- cprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
-by (induct p) simp
-
-lemma ep_pair_cprod_map:
- assumes "ep_pair e1 p1" and "ep_pair e2 p2"
- shows "ep_pair (cprod_map\<cdot>e1\<cdot>e2) (cprod_map\<cdot>p1\<cdot>p2)"
-proof
- interpret e1p1: ep_pair e1 p1 by fact
- interpret e2p2: ep_pair e2 p2 by fact
- fix x show "cprod_map\<cdot>p1\<cdot>p2\<cdot>(cprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
- by (induct x) simp
- fix y show "cprod_map\<cdot>e1\<cdot>e2\<cdot>(cprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
- by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below)
-qed
-
-lemma deflation_cprod_map:
- assumes "deflation d1" and "deflation d2"
- shows "deflation (cprod_map\<cdot>d1\<cdot>d2)"
-proof
- interpret d1: deflation d1 by fact
- interpret d2: deflation d2 by fact
- fix x
- show "cprod_map\<cdot>d1\<cdot>d2\<cdot>(cprod_map\<cdot>d1\<cdot>d2\<cdot>x) = cprod_map\<cdot>d1\<cdot>d2\<cdot>x"
- by (induct x) (simp add: d1.idem d2.idem)
- show "cprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
- by (induct x) (simp add: d1.below d2.below)
-qed
-
-lemma finite_deflation_cprod_map:
- assumes "finite_deflation d1" and "finite_deflation d2"
- shows "finite_deflation (cprod_map\<cdot>d1\<cdot>d2)"
-proof (rule finite_deflation_intro)
- interpret d1: finite_deflation d1 by fact
- interpret d2: finite_deflation d2 by fact
- have "deflation d1" and "deflation d2" by fact+
- thus "deflation (cprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_cprod_map)
- have "{p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}"
- by clarsimp
- thus "finite {p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p}"
- by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
-qed
-
end
--- a/src/HOLCF/Deflation.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Deflation.thy Fri Nov 12 12:57:02 2010 +0100
@@ -5,7 +5,7 @@
header {* Continuous deflations and ep-pairs *}
theory Deflation
-imports Cfun
+imports Plain_HOLCF
begin
default_sort cpo
@@ -405,93 +405,4 @@
end
-subsection {* Map operator for continuous functions *}
-
-lemma ep_pair_cfun_map:
- assumes "ep_pair e1 p1" and "ep_pair e2 p2"
- shows "ep_pair (cfun_map\<cdot>p1\<cdot>e2) (cfun_map\<cdot>e1\<cdot>p2)"
-proof
- interpret e1p1: ep_pair e1 p1 by fact
- interpret e2p2: ep_pair e2 p2 by fact
- fix f show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
- by (simp add: cfun_eq_iff)
- fix g show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
- apply (rule cfun_belowI, simp)
- apply (rule below_trans [OF e2p2.e_p_below])
- apply (rule monofun_cfun_arg)
- apply (rule e1p1.e_p_below)
- done
-qed
-
-lemma deflation_cfun_map:
- assumes "deflation d1" and "deflation d2"
- shows "deflation (cfun_map\<cdot>d1\<cdot>d2)"
-proof
- interpret d1: deflation d1 by fact
- interpret d2: deflation d2 by fact
- fix f
- show "cfun_map\<cdot>d1\<cdot>d2\<cdot>(cfun_map\<cdot>d1\<cdot>d2\<cdot>f) = cfun_map\<cdot>d1\<cdot>d2\<cdot>f"
- by (simp add: cfun_eq_iff d1.idem d2.idem)
- show "cfun_map\<cdot>d1\<cdot>d2\<cdot>f \<sqsubseteq> f"
- apply (rule cfun_belowI, simp)
- apply (rule below_trans [OF d2.below])
- apply (rule monofun_cfun_arg)
- apply (rule d1.below)
- done
-qed
-
-lemma finite_range_cfun_map:
- assumes a: "finite (range (\<lambda>x. a\<cdot>x))"
- assumes b: "finite (range (\<lambda>y. b\<cdot>y))"
- shows "finite (range (\<lambda>f. cfun_map\<cdot>a\<cdot>b\<cdot>f))" (is "finite (range ?h)")
-proof (rule finite_imageD)
- let ?f = "\<lambda>g. range (\<lambda>x. (a\<cdot>x, g\<cdot>x))"
- show "finite (?f ` range ?h)"
- proof (rule finite_subset)
- let ?B = "Pow (range (\<lambda>x. a\<cdot>x) \<times> range (\<lambda>y. b\<cdot>y))"
- show "?f ` range ?h \<subseteq> ?B"
- by clarsimp
- show "finite ?B"
- by (simp add: a b)
- qed
- show "inj_on ?f (range ?h)"
- proof (rule inj_onI, rule cfun_eqI, clarsimp)
- fix x f g
- assume "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) = range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
- hence "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) \<subseteq> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
- by (rule equalityD1)
- hence "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) \<in> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
- by (simp add: subset_eq)
- then obtain y where "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) = (a\<cdot>y, b\<cdot>(g\<cdot>(a\<cdot>y)))"
- by (rule rangeE)
- thus "b\<cdot>(f\<cdot>(a\<cdot>x)) = b\<cdot>(g\<cdot>(a\<cdot>x))"
- by clarsimp
- qed
-qed
-
-lemma finite_deflation_cfun_map:
- assumes "finite_deflation d1" and "finite_deflation d2"
- shows "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
-proof (rule finite_deflation_intro)
- interpret d1: finite_deflation d1 by fact
- interpret d2: finite_deflation d2 by fact
- have "deflation d1" and "deflation d2" by fact+
- thus "deflation (cfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_cfun_map)
- have "finite (range (\<lambda>f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f))"
- using d1.finite_range d2.finite_range
- by (rule finite_range_cfun_map)
- thus "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
- by (rule finite_range_imp_finite_fixes)
-qed
-
-text {* Finite deflations are compact elements of the function space *}
-
-lemma finite_deflation_imp_compact: "finite_deflation d \<Longrightarrow> compact d"
-apply (frule finite_deflation_imp_deflation)
-apply (subgoal_tac "compact (cfun_map\<cdot>d\<cdot>d\<cdot>d)")
-apply (simp add: cfun_map_def deflation.idem eta_cfun)
-apply (rule finite_deflation.compact)
-apply (simp only: finite_deflation_cfun_map)
-done
-
end
--- a/src/HOLCF/Domain.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Domain.thy Fri Nov 12 12:57:02 2010 +0100
@@ -5,115 +5,330 @@
header {* Domain package *}
theory Domain
-imports Ssum Sprod Up One Tr Fixrec Representable
+imports Bifinite Domain_Aux
uses
- ("Tools/cont_consts.ML")
- ("Tools/cont_proc.ML")
- ("Tools/Domain/domain_constructors.ML")
+ ("Tools/repdef.ML")
+ ("Tools/Domain/domain_isomorphism.ML")
("Tools/Domain/domain_axioms.ML")
- ("Tools/Domain/domain_induction.ML")
("Tools/Domain/domain.ML")
begin
-default_sort pcpo
+default_sort "domain"
+subsection {* Representations of types *}
+
+lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a) = cast\<cdot>DEFL('a)\<cdot>x"
+by (simp add: cast_DEFL)
-subsection {* Casedist *}
+lemma emb_prj_emb:
+ fixes x :: "'a"
+ assumes "DEFL('a) \<sqsubseteq> DEFL('b)"
+ shows "emb\<cdot>(prj\<cdot>(emb\<cdot>x) :: 'b) = emb\<cdot>x"
+unfolding emb_prj
+apply (rule cast.belowD)
+apply (rule monofun_cfun_arg [OF assms])
+apply (simp add: cast_DEFL)
+done
-text {* Lemmas for proving nchotomy rule: *}
+lemma prj_emb_prj:
+ assumes "DEFL('a) \<sqsubseteq> DEFL('b)"
+ shows "prj\<cdot>(emb\<cdot>(prj\<cdot>x :: 'b)) = (prj\<cdot>x :: 'a)"
+ apply (rule emb_eq_iff [THEN iffD1])
+ apply (simp only: emb_prj)
+ apply (rule deflation_below_comp1)
+ apply (rule deflation_cast)
+ apply (rule deflation_cast)
+ apply (rule monofun_cfun_arg [OF assms])
+done
+
+text {* Isomorphism lemmas used internally by the domain package: *}
-lemma ex_one_bottom_iff:
- "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = P ONE"
-by simp
+lemma domain_abs_iso:
+ fixes abs and rep
+ assumes DEFL: "DEFL('b) = DEFL('a)"
+ assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb"
+ assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb"
+ shows "rep\<cdot>(abs\<cdot>x) = x"
+unfolding abs_def rep_def
+by (simp add: emb_prj_emb DEFL)
+
+lemma domain_rep_iso:
+ fixes abs and rep
+ assumes DEFL: "DEFL('b) = DEFL('a)"
+ assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb"
+ assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb"
+ shows "abs\<cdot>(rep\<cdot>x) = x"
+unfolding abs_def rep_def
+by (simp add: emb_prj_emb DEFL)
+
+subsection {* Deflations as sets *}
-lemma ex_up_bottom_iff:
- "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = (\<exists>x. P (up\<cdot>x))"
-by (safe, case_tac x, auto)
+definition defl_set :: "defl \<Rightarrow> udom set"
+where "defl_set A = {x. cast\<cdot>A\<cdot>x = x}"
+
+lemma adm_defl_set: "adm (\<lambda>x. x \<in> defl_set A)"
+unfolding defl_set_def by simp
+
+lemma defl_set_bottom: "\<bottom> \<in> defl_set A"
+unfolding defl_set_def by simp
-lemma ex_sprod_bottom_iff:
- "(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
- (\<exists>x y. (P (:x, y:) \<and> x \<noteq> \<bottom>) \<and> y \<noteq> \<bottom>)"
-by (safe, case_tac y, auto)
+lemma defl_set_cast [simp]: "cast\<cdot>A\<cdot>x \<in> defl_set A"
+unfolding defl_set_def by simp
+
+lemma defl_set_subset_iff: "defl_set A \<subseteq> defl_set B \<longleftrightarrow> A \<sqsubseteq> B"
+apply (simp add: defl_set_def subset_eq cast_below_cast [symmetric])
+apply (auto simp add: cast.belowI cast.belowD)
+done
+
+subsection {* Proving a subtype is representable *}
+
+text {* Temporarily relax type constraints. *}
-lemma ex_sprod_up_bottom_iff:
- "(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
- (\<exists>x y. P (:up\<cdot>x, y:) \<and> y \<noteq> \<bottom>)"
-by (safe, case_tac y, simp, case_tac x, auto)
-
-lemma ex_ssum_bottom_iff:
- "(\<exists>x. P x \<and> x \<noteq> \<bottom>) =
- ((\<exists>x. P (sinl\<cdot>x) \<and> x \<noteq> \<bottom>) \<or>
- (\<exists>x. P (sinr\<cdot>x) \<and> x \<noteq> \<bottom>))"
-by (safe, case_tac x, auto)
-
-lemma exh_start: "p = \<bottom> \<or> (\<exists>x. p = x \<and> x \<noteq> \<bottom>)"
- by auto
+setup {*
+ fold Sign.add_const_constraint
+ [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"})
+ , (@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"})
+ , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::pcpo"})
+ , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"})
+ , (@{const_name liftemb}, SOME @{typ "'a::pcpo u \<rightarrow> udom"})
+ , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::pcpo u"}) ]
+*}
-lemmas ex_bottom_iffs =
- ex_ssum_bottom_iff
- ex_sprod_up_bottom_iff
- ex_sprod_bottom_iff
- ex_up_bottom_iff
- ex_one_bottom_iff
+lemma typedef_rep_class:
+ fixes Rep :: "'a::pcpo \<Rightarrow> udom"
+ fixes Abs :: "udom \<Rightarrow> 'a::pcpo"
+ fixes t :: defl
+ assumes type: "type_definition Rep Abs (defl_set t)"
+ assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)"
+ assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))"
+ assumes defl: "defl \<equiv> (\<lambda> a::'a itself. t)"
+ assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
+ assumes liftprj: "(liftprj :: udom \<rightarrow> 'a u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
+ assumes liftdefl: "(liftdefl :: 'a itself \<Rightarrow> defl) \<equiv> (\<lambda>t. u_defl\<cdot>DEFL('a))"
+ shows "OFCLASS('a, liftdomain_class)"
+using liftemb [THEN meta_eq_to_obj_eq]
+using liftprj [THEN meta_eq_to_obj_eq]
+proof (rule liftdomain_class_intro)
+ have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
+ unfolding emb
+ apply (rule beta_cfun)
+ apply (rule typedef_cont_Rep [OF type below adm_defl_set])
+ done
+ have prj_beta: "\<And>y. prj\<cdot>y = Abs (cast\<cdot>t\<cdot>y)"
+ unfolding prj
+ apply (rule beta_cfun)
+ apply (rule typedef_cont_Abs [OF type below adm_defl_set])
+ apply simp_all
+ done
+ have prj_emb: "\<And>x::'a. prj\<cdot>(emb\<cdot>x) = x"
+ using type_definition.Rep [OF type]
+ unfolding prj_beta emb_beta defl_set_def
+ by (simp add: type_definition.Rep_inverse [OF type])
+ have emb_prj: "\<And>y. emb\<cdot>(prj\<cdot>y :: 'a) = cast\<cdot>t\<cdot>y"
+ unfolding prj_beta emb_beta
+ by (simp add: type_definition.Abs_inverse [OF type])
+ show "ep_pair (emb :: 'a \<rightarrow> udom) prj"
+ apply default
+ apply (simp add: prj_emb)
+ apply (simp add: emb_prj cast.below)
+ 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
-text {* Rules for turning nchotomy into exhaust: *}
+lemma typedef_DEFL:
+ assumes "defl \<equiv> (\<lambda>a::'a::pcpo itself. t)"
+ shows "DEFL('a::pcpo) = t"
+unfolding assms ..
+
+text {* Restore original typing constraints. *}
-lemma exh_casedist0: "\<lbrakk>R; R \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" (* like make_elim *)
- by auto
+setup {*
+ fold Sign.add_const_constraint
+ [ (@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> 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> defl"})
+ , (@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom"})
+ , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::predomain u"}) ]
+*}
-lemma exh_casedist1: "((P \<or> Q \<Longrightarrow> R) \<Longrightarrow> S) \<equiv> (\<lbrakk>P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> S)"
- by rule auto
+use "Tools/repdef.ML"
-lemma exh_casedist2: "(\<exists>x. P x \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)"
- by rule auto
+subsection {* Isomorphic deflations *}
+
+definition
+ isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> defl \<Rightarrow> bool"
+where
+ "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
+
+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)
+
+lemma cast_isodefl: "isodefl d t \<Longrightarrow> cast\<cdot>t = (\<Lambda> x. emb\<cdot>(d\<cdot>(prj\<cdot>x)))"
+unfolding isodefl_def by (simp add: cfun_eqI)
-lemma exh_casedist3: "(P \<and> Q \<Longrightarrow> R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> R)"
- by rule auto
+lemma isodefl_strict: "isodefl d t \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>"
+unfolding isodefl_def
+by (drule cfun_fun_cong [where x="\<bottom>"], simp)
-lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3
+lemma isodefl_imp_deflation:
+ fixes d :: "'a \<rightarrow> 'a"
+ assumes "isodefl d t" shows "deflation d"
+proof
+ note assms [unfolded isodefl_def, simp]
+ fix x :: 'a
+ show "d\<cdot>(d\<cdot>x) = d\<cdot>x"
+ using cast.idem [of t "emb\<cdot>x"] by simp
+ show "d\<cdot>x \<sqsubseteq> x"
+ using cast.below [of t "emb\<cdot>x"] by simp
+qed
-
-subsection {* Installing the domain package *}
+lemma isodefl_ID_DEFL: "isodefl (ID :: 'a \<rightarrow> 'a) DEFL('a)"
+unfolding isodefl_def by (simp add: cast_DEFL)
-lemmas con_strict_rules =
- sinl_strict sinr_strict spair_strict1 spair_strict2
+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)
-lemmas con_bottom_iff_rules =
- sinl_bottom_iff sinr_bottom_iff spair_bottom_iff up_defined ONE_defined
+lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) DEFL('a) \<Longrightarrow> d = ID"
+unfolding isodefl_def
+apply (simp add: cast_DEFL)
+apply (simp add: cfun_eq_iff)
+apply (rule allI)
+apply (drule_tac x="emb\<cdot>x" in spec)
+apply simp
+done
+
+lemma isodefl_bottom: "isodefl \<bottom> \<bottom>"
+unfolding isodefl_def by (simp add: cfun_eq_iff)
-lemmas con_below_iff_rules =
- sinl_below sinr_below sinl_below_sinr sinr_below_sinl con_bottom_iff_rules
+lemma adm_isodefl:
+ "cont f \<Longrightarrow> cont g \<Longrightarrow> adm (\<lambda>x. isodefl (f x) (g x))"
+unfolding isodefl_def by simp
-lemmas con_eq_iff_rules =
- sinl_eq sinr_eq sinl_eq_sinr sinr_eq_sinl con_bottom_iff_rules
+lemma isodefl_lub:
+ assumes "chain d" and "chain t"
+ assumes "\<And>i. isodefl (d i) (t i)"
+ shows "isodefl (\<Squnion>i. d i) (\<Squnion>i. t i)"
+using prems unfolding isodefl_def
+by (simp add: contlub_cfun_arg contlub_cfun_fun)
+
+lemma isodefl_fix:
+ assumes "\<And>d t. isodefl d t \<Longrightarrow> isodefl (f\<cdot>d) (g\<cdot>t)"
+ shows "isodefl (fix\<cdot>f) (fix\<cdot>g)"
+unfolding fix_def2
+apply (rule isodefl_lub, simp, simp)
+apply (induct_tac i)
+apply (simp add: isodefl_bottom)
+apply (simp add: assms)
+done
-lemmas sel_strict_rules =
- cfcomp2 sscase1 sfst_strict ssnd_strict fup1
+lemma isodefl_abs_rep:
+ fixes abs and rep and d
+ assumes DEFL: "DEFL('b) = DEFL('a)"
+ assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb"
+ assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb"
+ shows "isodefl d t \<Longrightarrow> isodefl (abs oo d oo rep) t"
+unfolding isodefl_def
+by (simp add: cfun_eq_iff assms prj_emb_prj emb_prj_emb)
+
+lemma isodefl_cfun:
+ "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
+ isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_defl\<cdot>t1\<cdot>t2)"
+apply (rule isodeflI)
+apply (simp add: cast_cfun_defl cast_isodefl)
+apply (simp add: emb_cfun_def prj_cfun_def)
+apply (simp add: cfun_map_map cfcomp1)
+done
-lemma sel_app_extra_rules:
- "sscase\<cdot>ID\<cdot>\<bottom>\<cdot>(sinr\<cdot>x) = \<bottom>"
- "sscase\<cdot>ID\<cdot>\<bottom>\<cdot>(sinl\<cdot>x) = x"
- "sscase\<cdot>\<bottom>\<cdot>ID\<cdot>(sinl\<cdot>x) = \<bottom>"
- "sscase\<cdot>\<bottom>\<cdot>ID\<cdot>(sinr\<cdot>x) = x"
- "fup\<cdot>ID\<cdot>(up\<cdot>x) = x"
-by (cases "x = \<bottom>", simp, simp)+
+lemma isodefl_ssum:
+ "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
+ isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_defl\<cdot>t1\<cdot>t2)"
+apply (rule isodeflI)
+apply (simp add: cast_ssum_defl cast_isodefl)
+apply (simp add: emb_ssum_def prj_ssum_def)
+apply (simp add: ssum_map_map isodefl_strict)
+done
+
+lemma isodefl_sprod:
+ "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
+ isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_defl\<cdot>t1\<cdot>t2)"
+apply (rule isodeflI)
+apply (simp add: cast_sprod_defl cast_isodefl)
+apply (simp add: emb_sprod_def prj_sprod_def)
+apply (simp add: sprod_map_map isodefl_strict)
+done
-lemmas sel_app_rules =
- sel_strict_rules sel_app_extra_rules
- ssnd_spair sfst_spair up_defined spair_defined
+lemma isodefl_cprod:
+ "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
+ isodefl (cprod_map\<cdot>d1\<cdot>d2) (prod_defl\<cdot>t1\<cdot>t2)"
+apply (rule isodeflI)
+apply (simp add: cast_prod_defl cast_isodefl)
+apply (simp add: emb_prod_def prj_prod_def)
+apply (simp add: cprod_map_map cfcomp1)
+done
-lemmas sel_bottom_iff_rules =
- cfcomp2 sfst_bottom_iff ssnd_bottom_iff
+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)"
+apply (rule isodeflI)
+apply (simp add: cast_u_defl cast_isodefl)
+apply (simp add: emb_u_def prj_u_def liftemb_eq liftprj_eq)
+apply (simp add: u_map_map)
+done
-lemmas take_con_rules =
- ssum_map_sinl' ssum_map_sinr' sprod_map_spair' u_map_up
- deflation_strict deflation_ID ID1 cfcomp2
+lemma encode_prod_u_map:
+ "encode_prod_u\<cdot>(u_map\<cdot>(cprod_map\<cdot>f\<cdot>g)\<cdot>(decode_prod_u\<cdot>x))
+ = sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>g)\<cdot>x"
+unfolding encode_prod_u_def decode_prod_u_def
+apply (case_tac x, simp, rename_tac a b)
+apply (case_tac a, simp, case_tac b, simp, simp)
+done
-use "Tools/cont_consts.ML"
-use "Tools/cont_proc.ML"
+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 assms unfolding isodefl_def
+apply (simp add: emb_u_def prj_u_def liftemb_prod_def liftprj_prod_def)
+apply (simp add: emb_u_def [symmetric] prj_u_def [symmetric])
+apply (simp add: cfcomp1 encode_prod_u_map cast_sprod_defl sprod_map_map)
+done
+
+subsection {* Setting up the domain package *}
+
+use "Tools/Domain/domain_isomorphism.ML"
use "Tools/Domain/domain_axioms.ML"
-use "Tools/Domain/domain_constructors.ML"
-use "Tools/Domain/domain_induction.ML"
use "Tools/Domain/domain.ML"
+setup Domain_Isomorphism.setup
+
+lemmas [domain_defl_simps] =
+ DEFL_cfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u
+ liftdefl_eq LIFTDEFL_prod
+
+lemmas [domain_map_ID] =
+ cfun_map_ID ssum_map_ID sprod_map_ID cprod_map_ID u_map_ID
+
+lemmas [domain_isodefl] =
+ isodefl_u isodefl_cfun isodefl_ssum isodefl_sprod
+ isodefl_cprod isodefl_cprod_u
+
+lemmas [domain_deflation] =
+ deflation_cfun_map deflation_ssum_map deflation_sprod_map
+ deflation_cprod_map deflation_u_map
+
+setup {*
+ fold Domain_Take_Proofs.add_map_function
+ [(@{type_name cfun}, @{const_name cfun_map}, [true, true]),
+ (@{type_name ssum}, @{const_name ssum_map}, [true, true]),
+ (@{type_name sprod}, @{const_name sprod_map}, [true, true]),
+ (@{type_name prod}, @{const_name cprod_map}, [true, true]),
+ (@{type_name "u"}, @{const_name u_map}, [true])]
+*}
+
end
--- a/src/HOLCF/Domain_Aux.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Domain_Aux.thy Fri Nov 12 12:57:02 2010 +0100
@@ -5,9 +5,13 @@
header {* Domain package support *}
theory Domain_Aux
-imports Ssum Sprod Fixrec
+imports Map_Functions Fixrec
uses
("Tools/Domain/domain_take_proofs.ML")
+ ("Tools/cont_consts.ML")
+ ("Tools/cont_proc.ML")
+ ("Tools/Domain/domain_constructors.ML")
+ ("Tools/Domain/domain_induction.ML")
begin
subsection {* Continuous isomorphisms *}
@@ -110,7 +114,6 @@
end
-
subsection {* Proofs about take functions *}
text {*
@@ -172,7 +175,6 @@
with `chain t` `(\<Squnion>n. t n) = ID` show "P x" by (simp add: lub_distribs)
qed
-
subsection {* Finiteness *}
text {*
@@ -256,9 +258,103 @@
shows "(\<And>n. P (d n\<cdot>x)) \<Longrightarrow> P x"
using lub_ID_finite [OF assms] by metis
+subsection {* Proofs about constructor functions *}
+
+text {* Lemmas for proving nchotomy rule: *}
+
+lemma ex_one_bottom_iff:
+ "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = P ONE"
+by simp
+
+lemma ex_up_bottom_iff:
+ "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = (\<exists>x. P (up\<cdot>x))"
+by (safe, case_tac x, auto)
+
+lemma ex_sprod_bottom_iff:
+ "(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
+ (\<exists>x y. (P (:x, y:) \<and> x \<noteq> \<bottom>) \<and> y \<noteq> \<bottom>)"
+by (safe, case_tac y, auto)
+
+lemma ex_sprod_up_bottom_iff:
+ "(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
+ (\<exists>x y. P (:up\<cdot>x, y:) \<and> y \<noteq> \<bottom>)"
+by (safe, case_tac y, simp, case_tac x, auto)
+
+lemma ex_ssum_bottom_iff:
+ "(\<exists>x. P x \<and> x \<noteq> \<bottom>) =
+ ((\<exists>x. P (sinl\<cdot>x) \<and> x \<noteq> \<bottom>) \<or>
+ (\<exists>x. P (sinr\<cdot>x) \<and> x \<noteq> \<bottom>))"
+by (safe, case_tac x, auto)
+
+lemma exh_start: "p = \<bottom> \<or> (\<exists>x. p = x \<and> x \<noteq> \<bottom>)"
+ by auto
+
+lemmas ex_bottom_iffs =
+ ex_ssum_bottom_iff
+ ex_sprod_up_bottom_iff
+ ex_sprod_bottom_iff
+ ex_up_bottom_iff
+ ex_one_bottom_iff
+
+text {* Rules for turning nchotomy into exhaust: *}
+
+lemma exh_casedist0: "\<lbrakk>R; R \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" (* like make_elim *)
+ by auto
+
+lemma exh_casedist1: "((P \<or> Q \<Longrightarrow> R) \<Longrightarrow> S) \<equiv> (\<lbrakk>P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> S)"
+ by rule auto
+
+lemma exh_casedist2: "(\<exists>x. P x \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)"
+ by rule auto
+
+lemma exh_casedist3: "(P \<and> Q \<Longrightarrow> R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> R)"
+ by rule auto
+
+lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3
+
+text {* Rules for proving constructor properties *}
+
+lemmas con_strict_rules =
+ sinl_strict sinr_strict spair_strict1 spair_strict2
+
+lemmas con_bottom_iff_rules =
+ sinl_bottom_iff sinr_bottom_iff spair_bottom_iff up_defined ONE_defined
+
+lemmas con_below_iff_rules =
+ sinl_below sinr_below sinl_below_sinr sinr_below_sinl con_bottom_iff_rules
+
+lemmas con_eq_iff_rules =
+ sinl_eq sinr_eq sinl_eq_sinr sinr_eq_sinl con_bottom_iff_rules
+
+lemmas sel_strict_rules =
+ cfcomp2 sscase1 sfst_strict ssnd_strict fup1
+
+lemma sel_app_extra_rules:
+ "sscase\<cdot>ID\<cdot>\<bottom>\<cdot>(sinr\<cdot>x) = \<bottom>"
+ "sscase\<cdot>ID\<cdot>\<bottom>\<cdot>(sinl\<cdot>x) = x"
+ "sscase\<cdot>\<bottom>\<cdot>ID\<cdot>(sinl\<cdot>x) = \<bottom>"
+ "sscase\<cdot>\<bottom>\<cdot>ID\<cdot>(sinr\<cdot>x) = x"
+ "fup\<cdot>ID\<cdot>(up\<cdot>x) = x"
+by (cases "x = \<bottom>", simp, simp)+
+
+lemmas sel_app_rules =
+ sel_strict_rules sel_app_extra_rules
+ ssnd_spair sfst_spair up_defined spair_defined
+
+lemmas sel_bottom_iff_rules =
+ cfcomp2 sfst_bottom_iff ssnd_bottom_iff
+
+lemmas take_con_rules =
+ ssum_map_sinl' ssum_map_sinr' sprod_map_spair' u_map_up
+ deflation_strict deflation_ID ID1 cfcomp2
+
subsection {* ML setup *}
use "Tools/Domain/domain_take_proofs.ML"
+use "Tools/cont_consts.ML"
+use "Tools/cont_proc.ML"
+use "Tools/Domain/domain_constructors.ML"
+use "Tools/Domain/domain_induction.ML"
setup Domain_Take_Proofs.setup
--- a/src/HOLCF/Fix.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Fix.thy Fri Nov 12 12:57:02 2010 +0100
@@ -82,9 +82,8 @@
lemma fix_least_below: "F\<cdot>x \<sqsubseteq> x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
apply (simp add: fix_def2)
-apply (rule is_lub_thelub)
+apply (rule lub_below)
apply (rule chain_iterate)
-apply (rule ub_rangeI)
apply (induct_tac i)
apply simp
apply simp
--- a/src/HOLCF/Fixrec.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Fixrec.thy Fri Nov 12 12:57:02 2010 +0100
@@ -5,7 +5,7 @@
header "Package for defining recursive functions in HOLCF"
theory Fixrec
-imports Cprod Sprod Ssum Up One Tr Fix
+imports Plain_HOLCF
uses
("Tools/holcf_library.ML")
("Tools/fixrec.ML")
--- a/src/HOLCF/HOLCF.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/HOLCF.thy Fri Nov 12 12:57:02 2010 +0100
@@ -11,7 +11,7 @@
Powerdomains
begin
-default_sort bifinite
+default_sort "domain"
ML {* path_add "~~/src/HOLCF/Library" *}
--- a/src/HOLCF/IsaMakefile Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/IsaMakefile Fri Nov 12 12:57:02 2010 +0100
@@ -54,13 +54,14 @@
HOLCF.thy \
Lift.thy \
LowerPD.thy \
+ Map_Functions.thy \
One.thy \
Pcpodef.thy \
Pcpo.thy \
+ Plain_HOLCF.thy \
Porder.thy \
Powerdomains.thy \
Product_Cpo.thy \
- Representable.thy \
Sprod.thy \
Ssum.thy \
Tr.thy \
--- a/src/HOLCF/Library/Defl_Bifinite.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Library/Defl_Bifinite.thy Fri Nov 12 12:57:02 2010 +0100
@@ -609,7 +609,7 @@
subsection {* Algebraic deflations are a bifinite domain *}
-instantiation defl :: bifinite
+instantiation defl :: liftdomain
begin
definition
@@ -622,7 +622,18 @@
"defl (t::defl itself) =
(\<Squnion>i. defl_principal (Abs_fin_defl (emb oo defl_approx i oo prj)))"
-instance proof
+definition
+ "(liftemb :: defl u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> defl u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl (t::defl itself) = u_defl\<cdot>DEFL(defl)"
+
+instance
+using liftemb_defl_def liftprj_defl_def liftdefl_defl_def
+proof (rule liftdomain_class_intro)
show ep: "ep_pair emb (prj :: udom \<rightarrow> defl)"
unfolding emb_defl_def prj_defl_def
by (rule ep_pair_udom [OF defl_approx])
--- a/src/HOLCF/Library/Strict_Fun.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Library/Strict_Fun.thy Fri Nov 12 12:57:02 2010 +0100
@@ -173,7 +173,7 @@
apply (erule (1) finite_deflation_sfun_map)
done
-instantiation sfun :: (bifinite, bifinite) bifinite
+instantiation sfun :: ("domain", "domain") liftdomain
begin
definition
@@ -185,7 +185,18 @@
definition
"defl (t::('a \<rightarrow>! 'b) itself) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
-instance proof
+definition
+ "(liftemb :: ('a \<rightarrow>! 'b) u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> ('a \<rightarrow>! 'b) u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl (t::('a \<rightarrow>! 'b) itself) = u_defl\<cdot>DEFL('a \<rightarrow>! 'b)"
+
+instance
+using liftemb_sfun_def liftprj_sfun_def liftdefl_sfun_def
+proof (rule liftdomain_class_intro)
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
unfolding emb_sfun_def prj_sfun_def
using ep_pair_udom [OF sfun_approx]
@@ -199,7 +210,7 @@
end
lemma DEFL_sfun [domain_defl_simps]:
- "DEFL('a::bifinite \<rightarrow>! 'b::bifinite) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+ "DEFL('a \<rightarrow>! 'b) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
by (rule defl_sfun_def)
lemma isodefl_sfun [domain_isodefl]:
@@ -212,8 +223,8 @@
done
setup {*
- Domain_Isomorphism.add_type_constructor
- (@{type_name "sfun"}, @{const_name sfun_defl}, @{const_name sfun_map}, [true, true])
+ Domain_Take_Proofs.add_map_function
+ (@{type_name "sfun"}, @{const_name sfun_map}, [true, true])
*}
end
--- a/src/HOLCF/Library/Sum_Cpo.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Library/Sum_Cpo.thy Fri Nov 12 12:57:02 2010 +0100
@@ -216,4 +216,77 @@
instance sum :: (discrete_cpo, discrete_cpo) discrete_cpo
by intro_classes (simp add: below_sum_def split: sum.split)
+subsection {* Using sum types with fixrec *}
+
+definition
+ "match_Inl = (\<Lambda> x k. case x of Inl a \<Rightarrow> k\<cdot>a | Inr b \<Rightarrow> Fixrec.fail)"
+
+definition
+ "match_Inr = (\<Lambda> x k. case x of Inl a \<Rightarrow> Fixrec.fail | Inr b \<Rightarrow> k\<cdot>b)"
+
+lemma match_Inl_simps [simp]:
+ "match_Inl\<cdot>(Inl a)\<cdot>k = k\<cdot>a"
+ "match_Inl\<cdot>(Inr b)\<cdot>k = Fixrec.fail"
+unfolding match_Inl_def by simp_all
+
+lemma match_Inr_simps [simp]:
+ "match_Inr\<cdot>(Inl a)\<cdot>k = Fixrec.fail"
+ "match_Inr\<cdot>(Inr b)\<cdot>k = k\<cdot>b"
+unfolding match_Inr_def by simp_all
+
+setup {*
+ Fixrec.add_matchers
+ [ (@{const_name Inl}, @{const_name match_Inl}),
+ (@{const_name Inr}, @{const_name match_Inr}) ]
+*}
+
+subsection {* Disjoint sum is a predomain *}
+
+definition
+ "encode_sum_u =
+ (\<Lambda>(up\<cdot>x). case x of Inl a \<Rightarrow> sinl\<cdot>(up\<cdot>a) | Inr b \<Rightarrow> sinr\<cdot>(up\<cdot>b))"
+
+definition
+ "decode_sum_u = sscase\<cdot>(\<Lambda>(up\<cdot>a). up\<cdot>(Inl a))\<cdot>(\<Lambda>(up\<cdot>b). up\<cdot>(Inr b))"
+
+lemma decode_encode_sum_u [simp]: "decode_sum_u\<cdot>(encode_sum_u\<cdot>x) = x"
+unfolding decode_sum_u_def encode_sum_u_def
+by (case_tac x, simp, rename_tac y, case_tac y, simp_all)
+
+lemma encode_decode_sum_u [simp]: "encode_sum_u\<cdot>(decode_sum_u\<cdot>x) = x"
+unfolding decode_sum_u_def encode_sum_u_def
+apply (case_tac x, simp)
+apply (rename_tac a, case_tac a, simp, simp)
+apply (rename_tac b, case_tac b, simp, simp)
+done
+
+instantiation sum :: (predomain, predomain) predomain
+begin
+
+definition
+ "liftemb = (udom_emb ssum_approx oo ssum_map\<cdot>emb\<cdot>emb) oo encode_sum_u"
+
+definition
+ "liftprj =
+ decode_sum_u oo (ssum_map\<cdot>prj\<cdot>prj oo udom_prj ssum_approx)"
+
+definition
+ "liftdefl (t::('a + 'b) itself) = ssum_defl\<cdot>DEFL('a u)\<cdot>DEFL('b u)"
+
+instance proof
+ show "ep_pair liftemb (liftprj :: udom \<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_comp)
+ apply (intro ep_pair_ssum_map ep_pair_emb_prj)
+ apply (rule ep_pair_udom [OF ssum_approx])
+ done
+ show "cast\<cdot>LIFTDEFL('a + 'b) = liftemb oo (liftprj :: udom \<rightarrow> ('a + 'b) u)"
+ unfolding liftemb_sum_def liftprj_sum_def liftdefl_sum_def
+ by (simp add: cast_ssum_defl cast_DEFL cfcomp1 ssum_map_map)
+qed
+
end
+
+end
--- a/src/HOLCF/LowerPD.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/LowerPD.thy Fri Nov 12 12:57:02 2010 +0100
@@ -78,7 +78,7 @@
"{S::'a pd_basis set. lower_le.ideal S}"
by (fast intro: lower_le.ideal_principal)
-instantiation lower_pd :: (bifinite) below
+instantiation lower_pd :: ("domain") below
begin
definition
@@ -87,11 +87,11 @@
instance ..
end
-instance lower_pd :: (bifinite) po
+instance lower_pd :: ("domain") po
using type_definition_lower_pd below_lower_pd_def
by (rule lower_le.typedef_ideal_po)
-instance lower_pd :: (bifinite) cpo
+instance lower_pd :: ("domain") cpo
using type_definition_lower_pd below_lower_pd_def
by (rule lower_le.typedef_ideal_cpo)
@@ -110,7 +110,7 @@
lemma lower_pd_minimal: "lower_principal (PDUnit compact_bot) \<sqsubseteq> ys"
by (induct ys rule: lower_pd.principal_induct, simp, simp)
-instance lower_pd :: (bifinite) pcpo
+instance lower_pd :: ("domain") pcpo
by intro_classes (fast intro: lower_pd_minimal)
lemma inst_lower_pd_pcpo: "\<bottom> = lower_principal (PDUnit compact_bot)"
@@ -433,7 +433,7 @@
by (rule finite_range_imp_finite_fixes)
qed
-subsection {* Lower powerdomain is a bifinite domain *}
+subsection {* Lower powerdomain is a domain *}
definition
lower_approx :: "nat \<Rightarrow> udom lower_pd \<rightarrow> udom lower_pd"
@@ -441,16 +441,8 @@
"lower_approx = (\<lambda>i. lower_map\<cdot>(udom_approx i))"
lemma lower_approx: "approx_chain lower_approx"
-proof (rule approx_chain.intro)
- show "chain (\<lambda>i. lower_approx i)"
- unfolding lower_approx_def by simp
- show "(\<Squnion>i. lower_approx i) = ID"
- unfolding lower_approx_def
- by (simp add: lub_distribs lower_map_ID)
- show "\<And>i. finite_deflation (lower_approx i)"
- unfolding lower_approx_def
- by (intro finite_deflation_lower_map finite_deflation_udom_approx)
-qed
+using lower_map_ID finite_deflation_lower_map
+unfolding lower_approx_def by (rule approx_chain_lemma1)
definition lower_defl :: "defl \<rightarrow> defl"
where "lower_defl = defl_fun1 lower_approx lower_map"
@@ -458,12 +450,10 @@
lemma cast_lower_defl:
"cast\<cdot>(lower_defl\<cdot>A) =
udom_emb lower_approx oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj lower_approx"
-unfolding lower_defl_def
-apply (rule cast_defl_fun1 [OF lower_approx])
-apply (erule finite_deflation_lower_map)
-done
+using lower_approx finite_deflation_lower_map
+unfolding lower_defl_def by (rule cast_defl_fun1)
-instantiation lower_pd :: (bifinite) bifinite
+instantiation lower_pd :: ("domain") liftdomain
begin
definition
@@ -475,7 +465,18 @@
definition
"defl (t::'a lower_pd itself) = lower_defl\<cdot>DEFL('a)"
-instance proof
+definition
+ "(liftemb :: 'a lower_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl (t::'a lower_pd itself) = u_defl\<cdot>DEFL('a lower_pd)"
+
+instance
+using liftemb_lower_pd_def liftprj_lower_pd_def liftdefl_lower_pd_def
+proof (rule liftdomain_class_intro)
show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)"
unfolding emb_lower_pd_def prj_lower_pd_def
using ep_pair_udom [OF lower_approx]
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Map_Functions.thy Fri Nov 12 12:57:02 2010 +0100
@@ -0,0 +1,383 @@
+(* Title: HOLCF/Map_Functions.thy
+ Author: Brian Huffman
+*)
+
+header {* Map functions for various types *}
+
+theory Map_Functions
+imports Deflation
+begin
+
+subsection {* Map operator for continuous function space *}
+
+default_sort cpo
+
+definition
+ cfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)"
+where
+ "cfun_map = (\<Lambda> a b f x. b\<cdot>(f\<cdot>(a\<cdot>x)))"
+
+lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))"
+unfolding cfun_map_def by simp
+
+lemma cfun_map_ID: "cfun_map\<cdot>ID\<cdot>ID = ID"
+unfolding cfun_eq_iff by simp
+
+lemma cfun_map_map:
+ "cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
+ cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
+by (rule cfun_eqI) simp
+
+lemma ep_pair_cfun_map:
+ assumes "ep_pair e1 p1" and "ep_pair e2 p2"
+ shows "ep_pair (cfun_map\<cdot>p1\<cdot>e2) (cfun_map\<cdot>e1\<cdot>p2)"
+proof
+ interpret e1p1: ep_pair e1 p1 by fact
+ interpret e2p2: ep_pair e2 p2 by fact
+ fix f show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
+ by (simp add: cfun_eq_iff)
+ fix g show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
+ apply (rule cfun_belowI, simp)
+ apply (rule below_trans [OF e2p2.e_p_below])
+ apply (rule monofun_cfun_arg)
+ apply (rule e1p1.e_p_below)
+ done
+qed
+
+lemma deflation_cfun_map:
+ assumes "deflation d1" and "deflation d2"
+ shows "deflation (cfun_map\<cdot>d1\<cdot>d2)"
+proof
+ interpret d1: deflation d1 by fact
+ interpret d2: deflation d2 by fact
+ fix f
+ show "cfun_map\<cdot>d1\<cdot>d2\<cdot>(cfun_map\<cdot>d1\<cdot>d2\<cdot>f) = cfun_map\<cdot>d1\<cdot>d2\<cdot>f"
+ by (simp add: cfun_eq_iff d1.idem d2.idem)
+ show "cfun_map\<cdot>d1\<cdot>d2\<cdot>f \<sqsubseteq> f"
+ apply (rule cfun_belowI, simp)
+ apply (rule below_trans [OF d2.below])
+ apply (rule monofun_cfun_arg)
+ apply (rule d1.below)
+ done
+qed
+
+lemma finite_range_cfun_map:
+ assumes a: "finite (range (\<lambda>x. a\<cdot>x))"
+ assumes b: "finite (range (\<lambda>y. b\<cdot>y))"
+ shows "finite (range (\<lambda>f. cfun_map\<cdot>a\<cdot>b\<cdot>f))" (is "finite (range ?h)")
+proof (rule finite_imageD)
+ let ?f = "\<lambda>g. range (\<lambda>x. (a\<cdot>x, g\<cdot>x))"
+ show "finite (?f ` range ?h)"
+ proof (rule finite_subset)
+ let ?B = "Pow (range (\<lambda>x. a\<cdot>x) \<times> range (\<lambda>y. b\<cdot>y))"
+ show "?f ` range ?h \<subseteq> ?B"
+ by clarsimp
+ show "finite ?B"
+ by (simp add: a b)
+ qed
+ show "inj_on ?f (range ?h)"
+ proof (rule inj_onI, rule cfun_eqI, clarsimp)
+ fix x f g
+ assume "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) = range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
+ hence "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) \<subseteq> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
+ by (rule equalityD1)
+ hence "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) \<in> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
+ by (simp add: subset_eq)
+ then obtain y where "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) = (a\<cdot>y, b\<cdot>(g\<cdot>(a\<cdot>y)))"
+ by (rule rangeE)
+ thus "b\<cdot>(f\<cdot>(a\<cdot>x)) = b\<cdot>(g\<cdot>(a\<cdot>x))"
+ by clarsimp
+ qed
+qed
+
+lemma finite_deflation_cfun_map:
+ assumes "finite_deflation d1" and "finite_deflation d2"
+ shows "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
+proof (rule finite_deflation_intro)
+ interpret d1: finite_deflation d1 by fact
+ interpret d2: finite_deflation d2 by fact
+ have "deflation d1" and "deflation d2" by fact+
+ thus "deflation (cfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_cfun_map)
+ have "finite (range (\<lambda>f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f))"
+ using d1.finite_range d2.finite_range
+ by (rule finite_range_cfun_map)
+ thus "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
+ by (rule finite_range_imp_finite_fixes)
+qed
+
+text {* Finite deflations are compact elements of the function space *}
+
+lemma finite_deflation_imp_compact: "finite_deflation d \<Longrightarrow> compact d"
+apply (frule finite_deflation_imp_deflation)
+apply (subgoal_tac "compact (cfun_map\<cdot>d\<cdot>d\<cdot>d)")
+apply (simp add: cfun_map_def deflation.idem eta_cfun)
+apply (rule finite_deflation.compact)
+apply (simp only: finite_deflation_cfun_map)
+done
+
+subsection {* Map operator for product type *}
+
+definition
+ cprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
+where
+ "cprod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))"
+
+lemma cprod_map_Pair [simp]: "cprod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
+unfolding cprod_map_def by simp
+
+lemma cprod_map_ID: "cprod_map\<cdot>ID\<cdot>ID = ID"
+unfolding cfun_eq_iff by auto
+
+lemma cprod_map_map:
+ "cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
+ cprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
+by (induct p) simp
+
+lemma ep_pair_cprod_map:
+ assumes "ep_pair e1 p1" and "ep_pair e2 p2"
+ shows "ep_pair (cprod_map\<cdot>e1\<cdot>e2) (cprod_map\<cdot>p1\<cdot>p2)"
+proof
+ interpret e1p1: ep_pair e1 p1 by fact
+ interpret e2p2: ep_pair e2 p2 by fact
+ fix x show "cprod_map\<cdot>p1\<cdot>p2\<cdot>(cprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
+ by (induct x) simp
+ fix y show "cprod_map\<cdot>e1\<cdot>e2\<cdot>(cprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
+ by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below)
+qed
+
+lemma deflation_cprod_map:
+ assumes "deflation d1" and "deflation d2"
+ shows "deflation (cprod_map\<cdot>d1\<cdot>d2)"
+proof
+ interpret d1: deflation d1 by fact
+ interpret d2: deflation d2 by fact
+ fix x
+ show "cprod_map\<cdot>d1\<cdot>d2\<cdot>(cprod_map\<cdot>d1\<cdot>d2\<cdot>x) = cprod_map\<cdot>d1\<cdot>d2\<cdot>x"
+ by (induct x) (simp add: d1.idem d2.idem)
+ show "cprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
+ by (induct x) (simp add: d1.below d2.below)
+qed
+
+lemma finite_deflation_cprod_map:
+ assumes "finite_deflation d1" and "finite_deflation d2"
+ shows "finite_deflation (cprod_map\<cdot>d1\<cdot>d2)"
+proof (rule finite_deflation_intro)
+ interpret d1: finite_deflation d1 by fact
+ interpret d2: finite_deflation d2 by fact
+ have "deflation d1" and "deflation d2" by fact+
+ thus "deflation (cprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_cprod_map)
+ have "{p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}"
+ by clarsimp
+ thus "finite {p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p}"
+ by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
+qed
+
+subsection {* Map function for lifted cpo *}
+
+definition
+ u_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u"
+where
+ "u_map = (\<Lambda> f. fup\<cdot>(up oo f))"
+
+lemma u_map_strict [simp]: "u_map\<cdot>f\<cdot>\<bottom> = \<bottom>"
+unfolding u_map_def by simp
+
+lemma u_map_up [simp]: "u_map\<cdot>f\<cdot>(up\<cdot>x) = up\<cdot>(f\<cdot>x)"
+unfolding u_map_def by simp
+
+lemma u_map_ID: "u_map\<cdot>ID = ID"
+unfolding u_map_def by (simp add: cfun_eq_iff eta_cfun)
+
+lemma u_map_map: "u_map\<cdot>f\<cdot>(u_map\<cdot>g\<cdot>p) = u_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>p"
+by (induct p) simp_all
+
+lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)"
+apply default
+apply (case_tac x, simp, simp add: ep_pair.e_inverse)
+apply (case_tac y, simp, simp add: ep_pair.e_p_below)
+done
+
+lemma deflation_u_map: "deflation d \<Longrightarrow> deflation (u_map\<cdot>d)"
+apply default
+apply (case_tac x, simp, simp add: deflation.idem)
+apply (case_tac x, simp, simp add: deflation.below)
+done
+
+lemma finite_deflation_u_map:
+ assumes "finite_deflation d" shows "finite_deflation (u_map\<cdot>d)"
+proof (rule finite_deflation_intro)
+ interpret d: finite_deflation d by fact
+ have "deflation d" by fact
+ thus "deflation (u_map\<cdot>d)" by (rule deflation_u_map)
+ have "{x. u_map\<cdot>d\<cdot>x = x} \<subseteq> insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x. d\<cdot>x = x})"
+ by (rule subsetI, case_tac x, simp_all)
+ thus "finite {x. u_map\<cdot>d\<cdot>x = x}"
+ by (rule finite_subset, simp add: d.finite_fixes)
+qed
+
+subsection {* Map function for strict products *}
+
+default_sort pcpo
+
+definition
+ sprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<otimes> 'c \<rightarrow> 'b \<otimes> 'd"
+where
+ "sprod_map = (\<Lambda> f g. ssplit\<cdot>(\<Lambda> x y. (:f\<cdot>x, g\<cdot>y:)))"
+
+lemma sprod_map_strict [simp]: "sprod_map\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>"
+unfolding sprod_map_def by simp
+
+lemma sprod_map_spair [simp]:
+ "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
+by (simp add: sprod_map_def)
+
+lemma sprod_map_spair':
+ "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
+by (cases "x = \<bottom> \<or> y = \<bottom>") auto
+
+lemma sprod_map_ID: "sprod_map\<cdot>ID\<cdot>ID = ID"
+unfolding sprod_map_def by (simp add: cfun_eq_iff eta_cfun)
+
+lemma sprod_map_map:
+ "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
+ sprod_map\<cdot>f1\<cdot>g1\<cdot>(sprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
+ sprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
+apply (induct p, simp)
+apply (case_tac "f2\<cdot>x = \<bottom>", simp)
+apply (case_tac "g2\<cdot>y = \<bottom>", simp)
+apply simp
+done
+
+lemma ep_pair_sprod_map:
+ assumes "ep_pair e1 p1" and "ep_pair e2 p2"
+ shows "ep_pair (sprod_map\<cdot>e1\<cdot>e2) (sprod_map\<cdot>p1\<cdot>p2)"
+proof
+ interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact
+ interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact
+ fix x show "sprod_map\<cdot>p1\<cdot>p2\<cdot>(sprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
+ by (induct x) simp_all
+ fix y show "sprod_map\<cdot>e1\<cdot>e2\<cdot>(sprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
+ apply (induct y, simp)
+ apply (case_tac "p1\<cdot>x = \<bottom>", simp, case_tac "p2\<cdot>y = \<bottom>", simp)
+ apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below)
+ done
+qed
+
+lemma deflation_sprod_map:
+ assumes "deflation d1" and "deflation d2"
+ shows "deflation (sprod_map\<cdot>d1\<cdot>d2)"
+proof
+ interpret d1: deflation d1 by fact
+ interpret d2: deflation d2 by fact
+ fix x
+ show "sprod_map\<cdot>d1\<cdot>d2\<cdot>(sprod_map\<cdot>d1\<cdot>d2\<cdot>x) = sprod_map\<cdot>d1\<cdot>d2\<cdot>x"
+ apply (induct x, simp)
+ apply (case_tac "d1\<cdot>x = \<bottom>", simp, case_tac "d2\<cdot>y = \<bottom>", simp)
+ apply (simp add: d1.idem d2.idem)
+ done
+ show "sprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
+ apply (induct x, simp)
+ apply (simp add: monofun_cfun d1.below d2.below)
+ done
+qed
+
+lemma finite_deflation_sprod_map:
+ assumes "finite_deflation d1" and "finite_deflation d2"
+ shows "finite_deflation (sprod_map\<cdot>d1\<cdot>d2)"
+proof (rule finite_deflation_intro)
+ interpret d1: finite_deflation d1 by fact
+ interpret d2: finite_deflation d2 by fact
+ have "deflation d1" and "deflation d2" by fact+
+ thus "deflation (sprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_sprod_map)
+ have "{x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq> insert \<bottom>
+ ((\<lambda>(x, y). (:x, y:)) ` ({x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}))"
+ by (rule subsetI, case_tac x, auto simp add: spair_eq_iff)
+ thus "finite {x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x}"
+ by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
+qed
+
+subsection {* Map function for strict sums *}
+
+definition
+ ssum_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd"
+where
+ "ssum_map = (\<Lambda> f g. sscase\<cdot>(sinl oo f)\<cdot>(sinr oo g))"
+
+lemma ssum_map_strict [simp]: "ssum_map\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
+unfolding ssum_map_def by simp
+
+lemma ssum_map_sinl [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"
+unfolding ssum_map_def by simp
+
+lemma ssum_map_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
+unfolding ssum_map_def by simp
+
+lemma ssum_map_sinl': "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"
+by (cases "x = \<bottom>") simp_all
+
+lemma ssum_map_sinr': "g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
+by (cases "x = \<bottom>") simp_all
+
+lemma ssum_map_ID: "ssum_map\<cdot>ID\<cdot>ID = ID"
+unfolding ssum_map_def by (simp add: cfun_eq_iff eta_cfun)
+
+lemma ssum_map_map:
+ "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
+ ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) =
+ ssum_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
+apply (induct p, simp)
+apply (case_tac "f2\<cdot>x = \<bottom>", simp, simp)
+apply (case_tac "g2\<cdot>y = \<bottom>", simp, simp)
+done
+
+lemma ep_pair_ssum_map:
+ assumes "ep_pair e1 p1" and "ep_pair e2 p2"
+ shows "ep_pair (ssum_map\<cdot>e1\<cdot>e2) (ssum_map\<cdot>p1\<cdot>p2)"
+proof
+ interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact
+ interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact
+ fix x show "ssum_map\<cdot>p1\<cdot>p2\<cdot>(ssum_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
+ by (induct x) simp_all
+ fix y show "ssum_map\<cdot>e1\<cdot>e2\<cdot>(ssum_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
+ apply (induct y, simp)
+ apply (case_tac "p1\<cdot>x = \<bottom>", simp, simp add: e1p1.e_p_below)
+ apply (case_tac "p2\<cdot>y = \<bottom>", simp, simp add: e2p2.e_p_below)
+ done
+qed
+
+lemma deflation_ssum_map:
+ assumes "deflation d1" and "deflation d2"
+ shows "deflation (ssum_map\<cdot>d1\<cdot>d2)"
+proof
+ interpret d1: deflation d1 by fact
+ interpret d2: deflation d2 by fact
+ fix x
+ show "ssum_map\<cdot>d1\<cdot>d2\<cdot>(ssum_map\<cdot>d1\<cdot>d2\<cdot>x) = ssum_map\<cdot>d1\<cdot>d2\<cdot>x"
+ apply (induct x, simp)
+ apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.idem)
+ apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.idem)
+ done
+ show "ssum_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
+ apply (induct x, simp)
+ apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.below)
+ apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.below)
+ done
+qed
+
+lemma finite_deflation_ssum_map:
+ assumes "finite_deflation d1" and "finite_deflation d2"
+ shows "finite_deflation (ssum_map\<cdot>d1\<cdot>d2)"
+proof (rule finite_deflation_intro)
+ interpret d1: finite_deflation d1 by fact
+ interpret d2: finite_deflation d2 by fact
+ have "deflation d1" and "deflation d2" by fact+
+ thus "deflation (ssum_map\<cdot>d1\<cdot>d2)" by (rule deflation_ssum_map)
+ have "{x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq>
+ (\<lambda>x. sinl\<cdot>x) ` {x. d1\<cdot>x = x} \<union>
+ (\<lambda>x. sinr\<cdot>x) ` {x. d2\<cdot>x = x} \<union> {\<bottom>}"
+ by (rule subsetI, case_tac x, simp_all)
+ thus "finite {x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x}"
+ by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
+qed
+
+end
--- a/src/HOLCF/Pcpo.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Pcpo.thy Fri Nov 12 12:57:02 2010 +0100
@@ -36,11 +36,16 @@
lemma lub_below_iff: "chain S \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x \<longleftrightarrow> (\<forall>i. S i \<sqsubseteq> x)"
by (simp add: is_lub_below_iff [OF cpo_lubI] is_ub_def)
+lemma lub_below: "\<lbrakk>chain S; \<And>i. S i \<sqsubseteq> x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x"
+ by (simp add: lub_below_iff)
+
+lemma below_lub: "\<lbrakk>chain S; x \<sqsubseteq> S i\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. S i)"
+ by (erule below_trans, erule is_ub_thelub)
+
lemma lub_range_mono:
"\<lbrakk>range X \<subseteq> range Y; chain Y; chain X\<rbrakk>
\<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
-apply (erule is_lub_thelub)
-apply (rule ub_rangeI)
+apply (erule lub_below)
apply (subgoal_tac "\<exists>j. X i = Y j")
apply clarsimp
apply (erule is_ub_thelub)
@@ -54,14 +59,12 @@
apply fast
apply assumption
apply (erule chain_shift)
-apply (rule is_lub_thelub)
+apply (rule lub_below)
apply assumption
-apply (rule ub_rangeI)
-apply (rule_tac y="Y (i + j)" in below_trans)
+apply (rule_tac i="i" in below_lub)
+apply (erule chain_shift)
apply (erule chain_mono)
apply (rule le_add1)
-apply (rule is_ub_thelub)
-apply (erule chain_shift)
done
lemma maxinch_is_thelub:
@@ -80,52 +83,14 @@
lemma lub_mono:
"\<lbrakk>chain X; chain Y; \<And>i. X i \<sqsubseteq> Y i\<rbrakk>
\<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
-apply (erule is_lub_thelub)
-apply (rule ub_rangeI)
-apply (rule below_trans)
-apply (erule meta_spec)
-apply (erule is_ub_thelub)
-done
+by (fast elim: lub_below below_lub)
text {* the = relation between two chains is preserved by their lubs *}
-lemma lub_equal:
- "\<lbrakk>chain X; chain Y; \<forall>k. X k = Y k\<rbrakk>
- \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
- by (simp only: fun_eq_iff [symmetric])
-
lemma lub_eq:
"(\<And>i. X i = Y i) \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
by simp
-text {* more results about mono and = of lubs of chains *}
-
-lemma lub_mono2:
- "\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain X; chain Y\<rbrakk>
- \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
-apply (erule exE)
-apply (subgoal_tac "(\<Squnion>i. X (i + Suc j)) \<sqsubseteq> (\<Squnion>i. Y (i + Suc j))")
-apply (thin_tac "\<forall>i>j. X i = Y i")
-apply (simp only: lub_range_shift)
-apply simp
-done
-
-lemma lub_equal2:
- "\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain X; chain Y\<rbrakk>
- \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
- by (blast intro: below_antisym lub_mono2 sym)
-
-lemma lub_mono3:
- "\<lbrakk>chain Y; chain X; \<forall>i. \<exists>j. Y i \<sqsubseteq> X j\<rbrakk>
- \<Longrightarrow> (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. X i)"
-apply (erule is_lub_thelub)
-apply (rule ub_rangeI)
-apply (erule allE)
-apply (erule exE)
-apply (erule below_trans)
-apply (erule is_ub_thelub)
-done
-
lemma ch2ch_lub:
assumes 1: "\<And>j. chain (\<lambda>i. Y i j)"
assumes 2: "\<And>i. chain (\<lambda>j. Y i j)"
@@ -149,10 +114,9 @@
have 4: "chain (\<lambda>i. \<Squnion>j. Y i j)"
by (rule ch2ch_lub [OF 1 2])
show "(\<Squnion>i. \<Squnion>j. Y i j) \<sqsubseteq> (\<Squnion>i. Y i i)"
- apply (rule is_lub_thelub [OF 4])
- apply (rule ub_rangeI)
- apply (rule lub_mono3 [rule_format, OF 2 3])
- apply (rule exI)
+ apply (rule lub_below [OF 4])
+ apply (rule lub_below [OF 2])
+ apply (rule below_lub [OF 3])
apply (rule below_trans)
apply (rule chain_mono [OF 1 le_maxI1])
apply (rule chain_mono [OF 2 le_maxI2])
@@ -238,9 +202,6 @@
lemma notUU_I: "\<lbrakk>x \<sqsubseteq> y; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> y \<noteq> \<bottom>"
by (blast intro: UU_I)
-lemma chain_mono2: "\<lbrakk>\<exists>j. Y j \<noteq> \<bottom>; chain Y\<rbrakk> \<Longrightarrow> \<exists>j. \<forall>i>j. Y i \<noteq> \<bottom>"
- by (blast dest: notUU_I chain_mono_less)
-
end
subsection {* Chain-finite and flat cpos *}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Plain_HOLCF.thy Fri Nov 12 12:57:02 2010 +0100
@@ -0,0 +1,15 @@
+(* Title: HOLCF/Plain_HOLCF.thy
+ Author: Brian Huffman
+*)
+
+header {* Plain HOLCF *}
+
+theory Plain_HOLCF
+imports Cfun Cprod Sprod Ssum Up Discrete Lift One Tr Fix
+begin
+
+text {*
+ Basic HOLCF concepts and types; does not include definition packages.
+*}
+
+end
--- a/src/HOLCF/Powerdomains.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Powerdomains.thy Fri Nov 12 12:57:02 2010 +0100
@@ -42,10 +42,10 @@
deflation_upper_map deflation_lower_map deflation_convex_map
setup {*
- fold Domain_Isomorphism.add_type_constructor
- [(@{type_name "upper_pd"}, @{const_name upper_defl}, @{const_name upper_map}, [true]),
- (@{type_name "lower_pd"}, @{const_name lower_defl}, @{const_name lower_map}, [true]),
- (@{type_name "convex_pd"}, @{const_name convex_defl}, @{const_name convex_map}, [true])]
+ fold Domain_Take_Proofs.add_map_function
+ [(@{type_name "upper_pd"}, @{const_name upper_map}, [true]),
+ (@{type_name "lower_pd"}, @{const_name lower_map}, [true]),
+ (@{type_name "convex_pd"}, @{const_name convex_map}, [true])]
*}
end
--- a/src/HOLCF/ROOT.ML Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/ROOT.ML Fri Nov 12 12:57:02 2010 +0100
@@ -6,4 +6,4 @@
no_document use_thys ["Nat_Bijection", "Countable"];
-use_thys ["HOLCF"];
+use_thys ["Plain_HOLCF", "Fixrec", "HOLCF"];
--- a/src/HOLCF/Representable.thy Fri Nov 12 11:36:01 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,294 +0,0 @@
-(* Title: HOLCF/Representable.thy
- Author: Brian Huffman
-*)
-
-header {* Representable Types *}
-
-theory Representable
-imports Algebraic Bifinite Universal Ssum One Fixrec Domain_Aux
-uses
- ("Tools/repdef.ML")
- ("Tools/Domain/domain_isomorphism.ML")
-begin
-
-default_sort bifinite
-
-subsection {* Representations of types *}
-
-lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a) = cast\<cdot>DEFL('a)\<cdot>x"
-by (simp add: cast_DEFL)
-
-lemma emb_prj_emb:
- fixes x :: "'a"
- assumes "DEFL('a) \<sqsubseteq> DEFL('b)"
- shows "emb\<cdot>(prj\<cdot>(emb\<cdot>x) :: 'b) = emb\<cdot>x"
-unfolding emb_prj
-apply (rule cast.belowD)
-apply (rule monofun_cfun_arg [OF assms])
-apply (simp add: cast_DEFL)
-done
-
-lemma prj_emb_prj:
- assumes "DEFL('a) \<sqsubseteq> DEFL('b)"
- shows "prj\<cdot>(emb\<cdot>(prj\<cdot>x :: 'b)) = (prj\<cdot>x :: 'a)"
- apply (rule emb_eq_iff [THEN iffD1])
- apply (simp only: emb_prj)
- apply (rule deflation_below_comp1)
- apply (rule deflation_cast)
- apply (rule deflation_cast)
- apply (rule monofun_cfun_arg [OF assms])
-done
-
-text {* Isomorphism lemmas used internally by the domain package: *}
-
-lemma domain_abs_iso:
- fixes abs and rep
- assumes DEFL: "DEFL('b) = DEFL('a)"
- assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb"
- assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb"
- shows "rep\<cdot>(abs\<cdot>x) = x"
-unfolding abs_def rep_def
-by (simp add: emb_prj_emb DEFL)
-
-lemma domain_rep_iso:
- fixes abs and rep
- assumes DEFL: "DEFL('b) = DEFL('a)"
- assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb"
- assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb"
- shows "abs\<cdot>(rep\<cdot>x) = x"
-unfolding abs_def rep_def
-by (simp add: emb_prj_emb DEFL)
-
-subsection {* Deflations as sets *}
-
-definition defl_set :: "defl \<Rightarrow> udom set"
-where "defl_set A = {x. cast\<cdot>A\<cdot>x = x}"
-
-lemma adm_defl_set: "adm (\<lambda>x. x \<in> defl_set A)"
-unfolding defl_set_def by simp
-
-lemma defl_set_bottom: "\<bottom> \<in> defl_set A"
-unfolding defl_set_def by simp
-
-lemma defl_set_cast [simp]: "cast\<cdot>A\<cdot>x \<in> defl_set A"
-unfolding defl_set_def by simp
-
-lemma defl_set_subset_iff: "defl_set A \<subseteq> defl_set B \<longleftrightarrow> A \<sqsubseteq> B"
-apply (simp add: defl_set_def subset_eq cast_below_cast [symmetric])
-apply (auto simp add: cast.belowI cast.belowD)
-done
-
-subsection {* Proving a subtype is representable *}
-
-text {*
- Temporarily relax type constraints for @{term emb} and @{term prj}.
-*}
-
-setup {*
- fold Sign.add_const_constraint
- [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"})
- , (@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"})
- , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::pcpo"}) ]
-*}
-
-lemma typedef_rep_class:
- fixes Rep :: "'a::pcpo \<Rightarrow> udom"
- fixes Abs :: "udom \<Rightarrow> 'a::pcpo"
- fixes t :: defl
- assumes type: "type_definition Rep Abs (defl_set t)"
- assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
- 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)"
- shows "OFCLASS('a, bifinite_class)"
-proof
- have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
- unfolding emb
- apply (rule beta_cfun)
- apply (rule typedef_cont_Rep [OF type below adm_defl_set])
- done
- have prj_beta: "\<And>y. prj\<cdot>y = Abs (cast\<cdot>t\<cdot>y)"
- unfolding prj
- apply (rule beta_cfun)
- apply (rule typedef_cont_Abs [OF type below adm_defl_set])
- apply simp_all
- done
- have prj_emb: "\<And>x::'a. prj\<cdot>(emb\<cdot>x) = x"
- using type_definition.Rep [OF type]
- unfolding prj_beta emb_beta defl_set_def
- by (simp add: type_definition.Rep_inverse [OF type])
- have emb_prj: "\<And>y. emb\<cdot>(prj\<cdot>y :: 'a) = cast\<cdot>t\<cdot>y"
- unfolding prj_beta emb_beta
- by (simp add: type_definition.Abs_inverse [OF type])
- show "ep_pair (emb :: 'a \<rightarrow> udom) prj"
- apply default
- apply (simp add: prj_emb)
- apply (simp add: emb_prj cast.below)
- done
- show "cast\<cdot>DEFL('a) = emb oo (prj :: udom \<rightarrow> 'a)"
- by (rule cfun_eqI, simp add: defl emb_prj)
-qed
-
-lemma typedef_DEFL:
- assumes "defl \<equiv> (\<lambda>a::'a::pcpo itself. t)"
- shows "DEFL('a::pcpo) = t"
-unfolding assms ..
-
-text {* Restore original typing constraints. *}
-
-setup {*
- fold Sign.add_const_constraint
- [ (@{const_name defl}, SOME @{typ "'a::bifinite itself \<Rightarrow> defl"})
- , (@{const_name emb}, SOME @{typ "'a::bifinite \<rightarrow> udom"})
- , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::bifinite"}) ]
-*}
-
-use "Tools/repdef.ML"
-
-subsection {* Isomorphic deflations *}
-
-definition
- isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> defl \<Rightarrow> bool"
-where
- "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
-
-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)
-
-lemma cast_isodefl: "isodefl d t \<Longrightarrow> cast\<cdot>t = (\<Lambda> x. emb\<cdot>(d\<cdot>(prj\<cdot>x)))"
-unfolding isodefl_def by (simp add: cfun_eqI)
-
-lemma isodefl_strict: "isodefl d t \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>"
-unfolding isodefl_def
-by (drule cfun_fun_cong [where x="\<bottom>"], simp)
-
-lemma isodefl_imp_deflation:
- fixes d :: "'a \<rightarrow> 'a"
- assumes "isodefl d t" shows "deflation d"
-proof
- note assms [unfolded isodefl_def, simp]
- fix x :: 'a
- show "d\<cdot>(d\<cdot>x) = d\<cdot>x"
- using cast.idem [of t "emb\<cdot>x"] by simp
- show "d\<cdot>x \<sqsubseteq> x"
- using cast.below [of t "emb\<cdot>x"] by simp
-qed
-
-lemma isodefl_ID_DEFL: "isodefl (ID :: 'a \<rightarrow> 'a) DEFL('a)"
-unfolding isodefl_def by (simp add: cast_DEFL)
-
-lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) DEFL('a) \<Longrightarrow> d = ID"
-unfolding isodefl_def
-apply (simp add: cast_DEFL)
-apply (simp add: cfun_eq_iff)
-apply (rule allI)
-apply (drule_tac x="emb\<cdot>x" in spec)
-apply simp
-done
-
-lemma isodefl_bottom: "isodefl \<bottom> \<bottom>"
-unfolding isodefl_def by (simp add: cfun_eq_iff)
-
-lemma adm_isodefl:
- "cont f \<Longrightarrow> cont g \<Longrightarrow> adm (\<lambda>x. isodefl (f x) (g x))"
-unfolding isodefl_def by simp
-
-lemma isodefl_lub:
- assumes "chain d" and "chain t"
- assumes "\<And>i. isodefl (d i) (t i)"
- shows "isodefl (\<Squnion>i. d i) (\<Squnion>i. t i)"
-using prems unfolding isodefl_def
-by (simp add: contlub_cfun_arg contlub_cfun_fun)
-
-lemma isodefl_fix:
- assumes "\<And>d t. isodefl d t \<Longrightarrow> isodefl (f\<cdot>d) (g\<cdot>t)"
- shows "isodefl (fix\<cdot>f) (fix\<cdot>g)"
-unfolding fix_def2
-apply (rule isodefl_lub, simp, simp)
-apply (induct_tac i)
-apply (simp add: isodefl_bottom)
-apply (simp add: assms)
-done
-
-lemma isodefl_abs_rep:
- fixes abs and rep and d
- assumes DEFL: "DEFL('b) = DEFL('a)"
- assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb"
- assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb"
- shows "isodefl d t \<Longrightarrow> isodefl (abs oo d oo rep) t"
-unfolding isodefl_def
-by (simp add: cfun_eq_iff assms prj_emb_prj emb_prj_emb)
-
-lemma isodefl_cfun:
- "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
- isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_defl\<cdot>t1\<cdot>t2)"
-apply (rule isodeflI)
-apply (simp add: cast_cfun_defl cast_isodefl)
-apply (simp add: emb_cfun_def prj_cfun_def)
-apply (simp add: cfun_map_map cfcomp1)
-done
-
-lemma isodefl_ssum:
- "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
- isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_defl\<cdot>t1\<cdot>t2)"
-apply (rule isodeflI)
-apply (simp add: cast_ssum_defl cast_isodefl)
-apply (simp add: emb_ssum_def prj_ssum_def)
-apply (simp add: ssum_map_map isodefl_strict)
-done
-
-lemma isodefl_sprod:
- "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
- isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_defl\<cdot>t1\<cdot>t2)"
-apply (rule isodeflI)
-apply (simp add: cast_sprod_defl cast_isodefl)
-apply (simp add: emb_sprod_def prj_sprod_def)
-apply (simp add: sprod_map_map isodefl_strict)
-done
-
-lemma isodefl_cprod:
- "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
- isodefl (cprod_map\<cdot>d1\<cdot>d2) (prod_defl\<cdot>t1\<cdot>t2)"
-apply (rule isodeflI)
-apply (simp add: cast_prod_defl cast_isodefl)
-apply (simp add: emb_prod_def prj_prod_def)
-apply (simp add: cprod_map_map cfcomp1)
-done
-
-lemma isodefl_u:
- "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: emb_u_def prj_u_def)
-apply (simp add: u_map_map)
-done
-
-subsection {* Constructing Domain Isomorphisms *}
-
-use "Tools/Domain/domain_isomorphism.ML"
-
-setup Domain_Isomorphism.setup
-
-lemmas [domain_defl_simps] =
- DEFL_cfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u
-
-lemmas [domain_map_ID] =
- cfun_map_ID ssum_map_ID sprod_map_ID cprod_map_ID u_map_ID
-
-lemmas [domain_isodefl] =
- isodefl_cfun isodefl_ssum isodefl_sprod isodefl_cprod isodefl_u
-
-lemmas [domain_deflation] =
- deflation_cfun_map deflation_ssum_map deflation_sprod_map
- deflation_cprod_map deflation_u_map
-
-setup {*
- fold Domain_Isomorphism.add_type_constructor
- [(@{type_name cfun}, @{const_name cfun_defl}, @{const_name cfun_map}, [true, true]),
- (@{type_name ssum}, @{const_name ssum_defl}, @{const_name ssum_map}, [true, true]),
- (@{type_name sprod}, @{const_name sprod_defl}, @{const_name sprod_map}, [true, true]),
- (@{type_name prod}, @{const_name prod_defl}, @{const_name cprod_map}, [true, true]),
- (@{type_name "u"}, @{const_name u_defl}, @{const_name u_map}, [true])]
-*}
-
-end
--- a/src/HOLCF/Sprod.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Sprod.thy Fri Nov 12 12:57:02 2010 +0100
@@ -1,11 +1,12 @@
(* Title: HOLCF/Sprod.thy
- Author: Franz Regensburger and Brian Huffman
+ Author: Franz Regensburger
+ Author: Brian Huffman
*)
header {* The type of strict products *}
theory Sprod
-imports Deflation
+imports Cfun
begin
default_sort pcpo
@@ -210,83 +211,4 @@
done
qed
-subsection {* Map function for strict products *}
-
-definition
- sprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<otimes> 'c \<rightarrow> 'b \<otimes> 'd"
-where
- "sprod_map = (\<Lambda> f g. ssplit\<cdot>(\<Lambda> x y. (:f\<cdot>x, g\<cdot>y:)))"
-
-lemma sprod_map_strict [simp]: "sprod_map\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>"
-unfolding sprod_map_def by simp
-
-lemma sprod_map_spair [simp]:
- "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
-by (simp add: sprod_map_def)
-
-lemma sprod_map_spair':
- "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
-by (cases "x = \<bottom> \<or> y = \<bottom>") auto
-
-lemma sprod_map_ID: "sprod_map\<cdot>ID\<cdot>ID = ID"
-unfolding sprod_map_def by (simp add: cfun_eq_iff eta_cfun)
-
-lemma sprod_map_map:
- "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
- sprod_map\<cdot>f1\<cdot>g1\<cdot>(sprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
- sprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
-apply (induct p, simp)
-apply (case_tac "f2\<cdot>x = \<bottom>", simp)
-apply (case_tac "g2\<cdot>y = \<bottom>", simp)
-apply simp
-done
-
-lemma ep_pair_sprod_map:
- assumes "ep_pair e1 p1" and "ep_pair e2 p2"
- shows "ep_pair (sprod_map\<cdot>e1\<cdot>e2) (sprod_map\<cdot>p1\<cdot>p2)"
-proof
- interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact
- interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact
- fix x show "sprod_map\<cdot>p1\<cdot>p2\<cdot>(sprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
- by (induct x) simp_all
- fix y show "sprod_map\<cdot>e1\<cdot>e2\<cdot>(sprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
- apply (induct y, simp)
- apply (case_tac "p1\<cdot>x = \<bottom>", simp, case_tac "p2\<cdot>y = \<bottom>", simp)
- apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below)
- done
-qed
-
-lemma deflation_sprod_map:
- assumes "deflation d1" and "deflation d2"
- shows "deflation (sprod_map\<cdot>d1\<cdot>d2)"
-proof
- interpret d1: deflation d1 by fact
- interpret d2: deflation d2 by fact
- fix x
- show "sprod_map\<cdot>d1\<cdot>d2\<cdot>(sprod_map\<cdot>d1\<cdot>d2\<cdot>x) = sprod_map\<cdot>d1\<cdot>d2\<cdot>x"
- apply (induct x, simp)
- apply (case_tac "d1\<cdot>x = \<bottom>", simp, case_tac "d2\<cdot>y = \<bottom>", simp)
- apply (simp add: d1.idem d2.idem)
- done
- show "sprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
- apply (induct x, simp)
- apply (simp add: monofun_cfun d1.below d2.below)
- done
-qed
-
-lemma finite_deflation_sprod_map:
- assumes "finite_deflation d1" and "finite_deflation d2"
- shows "finite_deflation (sprod_map\<cdot>d1\<cdot>d2)"
-proof (rule finite_deflation_intro)
- interpret d1: finite_deflation d1 by fact
- interpret d2: finite_deflation d2 by fact
- have "deflation d1" and "deflation d2" by fact+
- thus "deflation (sprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_sprod_map)
- have "{x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq> insert \<bottom>
- ((\<lambda>(x, y). (:x, y:)) ` ({x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}))"
- by (rule subsetI, case_tac x, auto simp add: spair_eq_iff)
- thus "finite {x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x}"
- by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
-qed
-
end
--- a/src/HOLCF/Ssum.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Ssum.thy Fri Nov 12 12:57:02 2010 +0100
@@ -1,5 +1,6 @@
(* Title: HOLCF/Ssum.thy
- Author: Franz Regensburger and Brian Huffman
+ Author: Franz Regensburger
+ Author: Brian Huffman
*)
header {* The type of strict sums *}
@@ -194,88 +195,4 @@
apply (case_tac y, simp_all add: flat_below_iff)
done
-subsection {* Map function for strict sums *}
-
-definition
- ssum_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd"
-where
- "ssum_map = (\<Lambda> f g. sscase\<cdot>(sinl oo f)\<cdot>(sinr oo g))"
-
-lemma ssum_map_strict [simp]: "ssum_map\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
-unfolding ssum_map_def by simp
-
-lemma ssum_map_sinl [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"
-unfolding ssum_map_def by simp
-
-lemma ssum_map_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
-unfolding ssum_map_def by simp
-
-lemma ssum_map_sinl': "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"
-by (cases "x = \<bottom>") simp_all
-
-lemma ssum_map_sinr': "g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
-by (cases "x = \<bottom>") simp_all
-
-lemma ssum_map_ID: "ssum_map\<cdot>ID\<cdot>ID = ID"
-unfolding ssum_map_def by (simp add: cfun_eq_iff eta_cfun)
-
-lemma ssum_map_map:
- "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
- ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) =
- ssum_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
-apply (induct p, simp)
-apply (case_tac "f2\<cdot>x = \<bottom>", simp, simp)
-apply (case_tac "g2\<cdot>y = \<bottom>", simp, simp)
-done
-
-lemma ep_pair_ssum_map:
- assumes "ep_pair e1 p1" and "ep_pair e2 p2"
- shows "ep_pair (ssum_map\<cdot>e1\<cdot>e2) (ssum_map\<cdot>p1\<cdot>p2)"
-proof
- interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact
- interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact
- fix x show "ssum_map\<cdot>p1\<cdot>p2\<cdot>(ssum_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
- by (induct x) simp_all
- fix y show "ssum_map\<cdot>e1\<cdot>e2\<cdot>(ssum_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
- apply (induct y, simp)
- apply (case_tac "p1\<cdot>x = \<bottom>", simp, simp add: e1p1.e_p_below)
- apply (case_tac "p2\<cdot>y = \<bottom>", simp, simp add: e2p2.e_p_below)
- done
-qed
-
-lemma deflation_ssum_map:
- assumes "deflation d1" and "deflation d2"
- shows "deflation (ssum_map\<cdot>d1\<cdot>d2)"
-proof
- interpret d1: deflation d1 by fact
- interpret d2: deflation d2 by fact
- fix x
- show "ssum_map\<cdot>d1\<cdot>d2\<cdot>(ssum_map\<cdot>d1\<cdot>d2\<cdot>x) = ssum_map\<cdot>d1\<cdot>d2\<cdot>x"
- apply (induct x, simp)
- apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.idem)
- apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.idem)
- done
- show "ssum_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
- apply (induct x, simp)
- apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.below)
- apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.below)
- done
-qed
-
-lemma finite_deflation_ssum_map:
- assumes "finite_deflation d1" and "finite_deflation d2"
- shows "finite_deflation (ssum_map\<cdot>d1\<cdot>d2)"
-proof (rule finite_deflation_intro)
- interpret d1: finite_deflation d1 by fact
- interpret d2: finite_deflation d2 by fact
- have "deflation d1" and "deflation d2" by fact+
- thus "deflation (ssum_map\<cdot>d1\<cdot>d2)" by (rule deflation_ssum_map)
- have "{x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq>
- (\<lambda>x. sinl\<cdot>x) ` {x. d1\<cdot>x = x} \<union>
- (\<lambda>x. sinr\<cdot>x) ` {x. d2\<cdot>x = x} \<union> {\<bottom>}"
- by (rule subsetI, case_tac x, simp_all)
- thus "finite {x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x}"
- by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
-qed
-
end
--- a/src/HOLCF/Tools/Domain/domain.ML Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain.ML Fri Nov 12 12:57:02 2010 +0100
@@ -42,6 +42,11 @@
type info =
Domain_Take_Proofs.iso_info list * Domain_Take_Proofs.take_induct_info;
+fun add_arity ((b, sorts, mx), sort) thy : theory =
+ thy
+ |> Sign.add_types [(b, length sorts, mx)]
+ |> AxClass.axiomatize_arity (Sign.full_name thy b, sorts, sort);
+
fun gen_add_domain
(prep_sort : theory -> 'a -> sort)
(prep_typ : theory -> (string * sort) list -> 'b -> typ)
@@ -59,15 +64,13 @@
(dbind, map prep_tvar vs, mx)) raw_specs
end;
- fun thy_type (dbind, tvars, mx) = (dbind, length tvars, mx);
fun thy_arity (dbind, tvars, mx) =
- (Sign.full_name thy dbind, map (snd o dest_TFree) tvars, arg_sort false);
+ ((dbind, map (snd o dest_TFree) tvars, mx), arg_sort false);
(* this theory is used just for parsing and error checking *)
val tmp_thy = thy
|> Theory.copy
- |> Sign.add_types (map thy_type dtnvs)
- |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
+ |> fold (add_arity o thy_arity) dtnvs;
val dbinds : binding list =
map (fn (_,dbind,_,_) => dbind) raw_specs;
@@ -182,7 +185,7 @@
end;
fun pcpo_arg lazy = if lazy then @{sort cpo} else @{sort pcpo};
-fun rep_arg lazy = @{sort bifinite};
+fun rep_arg lazy = if lazy then @{sort predomain} else @{sort "domain"};
fun read_sort thy (SOME s) = Syntax.read_sort_global thy s
| read_sort thy NONE = Sign.defaultS thy;
--- a/src/HOLCF/Tools/Domain/domain_induction.ML Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_induction.ML Fri Nov 12 12:57:02 2010 +0100
@@ -50,7 +50,7 @@
fun is_ID (Const (c, _)) = (c = @{const_name ID})
| is_ID _ = false;
in
- fun map_of_arg v T =
+ fun map_of_arg thy v T =
let val m = Domain_Take_Proofs.map_of_typ thy subs T;
in if is_ID m then v else mk_capply (m, v) end;
end
@@ -66,7 +66,7 @@
val ns = Name.variant_list ["n"] (Datatype_Prop.make_tnames Ts);
val vs = map Free (ns ~~ Ts);
val lhs = mk_capply (take_const $ n', list_ccomb (con_const, vs));
- val rhs = list_ccomb (con_const, map2 map_of_arg vs Ts);
+ val rhs = list_ccomb (con_const, map2 (map_of_arg thy) vs Ts);
val goal = mk_trp (mk_eq (lhs, rhs));
val rules =
[abs_inverse] @ con_betas @ @{thms take_con_rules}
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Nov 12 12:57:02 2010 +0100
@@ -28,9 +28,6 @@
(string list * binding * mixfix * string * (binding * binding) option) list
-> theory -> theory
- val add_type_constructor :
- (string * string * string * bool list) -> theory -> theory
-
val setup : theory -> theory
end;
@@ -46,48 +43,24 @@
val beta_tac = simp_tac beta_ss;
fun is_cpo thy T = Sign.of_sort thy (T, @{sort cpo});
-fun is_bifinite thy T = Sign.of_sort thy (T, @{sort bifinite});
(******************************************************************************)
(******************************** theory data *********************************)
(******************************************************************************)
-structure DeflData = Theory_Data
-(
- (* constant names like "foo_defl" *)
- (* list indicates which type arguments correspond to deflation parameters *)
- (* alternatively, which type arguments allow indirect recursion *)
- type T = (string * bool list) Symtab.table;
- val empty = Symtab.empty;
- val extend = I;
- fun merge data = Symtab.merge (K true) data;
-);
-
structure RepData = Named_Thms
(
val name = "domain_defl_simps"
val description = "theorems like DEFL('a t) = t_defl$DEFL('a)"
)
-structure MapIdData = Named_Thms
-(
- val name = "domain_map_ID"
- val description = "theorems like foo_map$ID = ID"
-);
-
structure IsodeflData = Named_Thms
(
val name = "domain_isodefl"
val description = "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
);
-fun add_type_constructor
- (tname, defl_name, map_name, flags) =
- DeflData.map (Symtab.insert (K true) (tname, (defl_name, flags)))
- #> Domain_Take_Proofs.add_map_function (tname, map_name, flags)
-
-val setup =
- RepData.setup #> MapIdData.setup #> IsodeflData.setup
+val setup = RepData.setup #> IsodeflData.setup
(******************************************************************************)
@@ -105,6 +78,26 @@
fun mk_DEFL T =
Const (@{const_name defl}, Term.itselfT T --> deflT) $ Logic.mk_type T;
+fun dest_DEFL (Const (@{const_name defl}, _) $ t) = Logic.dest_type t
+ | dest_DEFL t = raise TERM ("dest_DEFL", [t]);
+
+fun mk_LIFTDEFL T =
+ Const (@{const_name liftdefl}, Term.itselfT T --> deflT) $ Logic.mk_type T;
+
+fun dest_LIFTDEFL (Const (@{const_name liftdefl}, _) $ t) = Logic.dest_type t
+ | dest_LIFTDEFL t = raise TERM ("dest_LIFTDEFL", [t]);
+
+fun mk_u_defl t = mk_capply (@{const "u_defl"}, t);
+
+fun mk_u_map t =
+ let
+ val (T, U) = dest_cfunT (fastype_of t);
+ val u_map_type = (T ->> U) ->> (mk_upT T ->> mk_upT U);
+ val u_map_const = Const (@{const_name u_map}, u_map_type);
+ in
+ mk_capply (u_map_const, t)
+ end;
+
fun emb_const T = Const (@{const_name emb}, T ->> udomT);
fun prj_const T = Const (@{const_name prj}, udomT ->> T);
fun coerce_const (T, U) = mk_cfcomp (prj_const U, emb_const T);
@@ -137,6 +130,10 @@
(*************** fixed-point definitions and unfolding theorems ***************)
(******************************************************************************)
+fun mk_projs [] t = []
+ | mk_projs (x::[]) t = [(x, t)]
+ | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);
+
fun add_fixdefs
(spec : (binding * term) list)
(thy : theory) : (thm list * thm list) * theory =
@@ -147,9 +144,6 @@
val fixpoint = mk_fix (mk_cabs functional);
(* project components of fixpoint *)
- fun mk_projs [] t = []
- | mk_projs (x::[]) t = [(x, t)]
- | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);
val projs = mk_projs lhss fixpoint;
(* convert parameters to lambda abstractions *)
@@ -208,35 +202,26 @@
(****************** deflation combinators and map functions *******************)
(******************************************************************************)
-fun mk_defl_type (flags : bool list) (Ts : typ list) =
- map (Term.itselfT o snd) (filter_out fst (flags ~~ Ts)) --->
- map (K deflT) (filter I flags) -->> deflT;
-
fun defl_of_typ
(thy : theory)
- (tab : (string * bool list) Symtab.table)
+ (tab1 : (typ * term) list)
+ (tab2 : (typ * term) list)
(T : typ) : term =
let
- fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts
- | is_closed_typ (TFree (n, s)) = not (Sign.subsort thy (s, @{sort bifinite}))
- | is_closed_typ _ = false;
- fun defl_of (TFree (a, _)) = Free (Library.unprefix "'" a, deflT)
- | defl_of (TVar _) = error ("defl_of_typ: TVar")
- | defl_of (T as Type (c, Ts)) =
- case Symtab.lookup tab c of
- SOME (s, flags) =>
- let
- val defl_const = Const (s, mk_defl_type flags Ts);
- val type_args = map (Logic.mk_type o snd) (filter_out fst (flags ~~ Ts));
- val defl_args = map (defl_of o snd) (filter fst (flags ~~ Ts));
- in
- list_ccomb (list_comb (defl_const, type_args), defl_args)
- end
- | NONE => if is_closed_typ T
- then mk_DEFL T
- else error ("defl_of_typ: type variable under unsupported type constructor " ^ c);
- in defl_of T end;
-
+ val defl_simps = RepData.get (ProofContext.init_global thy);
+ val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) defl_simps;
+ val rules' = map (apfst mk_DEFL) tab1 @ map (apfst mk_LIFTDEFL) tab2;
+ fun proc1 t =
+ (case dest_DEFL t of
+ TFree (a, _) => SOME (Free ("d" ^ Library.unprefix "'" a, deflT))
+ | _ => NONE) handle TERM _ => NONE;
+ fun proc2 t =
+ (case dest_LIFTDEFL t of
+ TFree (a, _) => SOME (Free ("p" ^ Library.unprefix "'" a, deflT))
+ | _ => NONE) handle TERM _ => NONE;
+ in
+ Pattern.rewrite_term thy (rules @ rules') [proc1, proc2] (mk_DEFL T)
+ end;
(******************************************************************************)
(********************* declaring definitions and theorems *********************)
@@ -426,8 +411,8 @@
(* this theory is used just for parsing *)
val tmp_thy = thy |>
Theory.copy |>
- Sign.add_types (map (fn (tvs, tname, mx, _, morphs) =>
- (tname, length tvs, mx)) doms_raw);
+ Sign.add_types (map (fn (tvs, tbind, mx, _, morphs) =>
+ (tbind, length tvs, mx)) doms_raw);
fun prep_dom thy (vs, t, mx, typ_raw, morphs) sorts =
let val (typ, sorts') = prep_typ thy typ_raw sorts
@@ -437,9 +422,28 @@
sorts : (string * sort) list) =
fold_map (prep_dom tmp_thy) doms_raw [];
+ (* lookup function for sorts of type variables *)
+ fun the_sort v = the (AList.lookup (op =) sorts v);
+
+ (* declare arities in temporary theory *)
+ val tmp_thy =
+ let
+ fun arity (vs, tbind, mx, _, _) =
+ (Sign.full_name thy tbind, map the_sort vs, @{sort "domain"});
+ in
+ fold AxClass.axiomatize_arity (map arity doms) tmp_thy
+ end;
+
+ (* check bifiniteness of right-hand sides *)
+ fun check_rhs (vs, tbind, mx, rhs, morphs) =
+ if Sign.of_sort tmp_thy (rhs, @{sort "domain"}) then ()
+ else error ("Type not of sort domain: " ^
+ quote (Syntax.string_of_typ_global tmp_thy rhs));
+ val _ = map check_rhs doms;
+
(* domain equations *)
fun mk_dom_eqn (vs, tbind, mx, rhs, morphs) =
- let fun arg v = TFree (v, the (AList.lookup (op =) sorts v));
+ let fun arg v = TFree (v, the_sort v);
in (Type (Sign.full_name tmp_thy tbind, map arg vs), rhs) end;
val dom_eqns = map mk_dom_eqn doms;
@@ -459,34 +463,54 @@
val morphs = map (fn (_, _, _, _, morphs) => morphs) doms;
(* determine deflation combinator arguments *)
- fun defl_flags (vs, tbind, mx, rhs, morphs) =
- let fun argT v = TFree (v, the (AList.lookup (op =) sorts v));
- in map (is_bifinite thy o argT) vs end;
- val defl_flagss = map defl_flags doms;
+ val lhsTs : typ list = map fst dom_eqns;
+ val defl_rec = Free ("t", mk_tupleT (map (K deflT) lhsTs));
+ val defl_recs = mk_projs lhsTs defl_rec;
+ val defl_recs' = map (apsnd mk_u_defl) defl_recs;
+ fun defl_body (_, _, _, rhsT, _) =
+ defl_of_typ tmp_thy defl_recs defl_recs' rhsT;
+ val functional = Term.lambda defl_rec (mk_tuple (map defl_body doms));
+
+ val tfrees = map fst (Term.add_tfrees functional []);
+ val frees = map fst (Term.add_frees functional []);
+ fun get_defl_flags (vs, _, _, _, _) =
+ let
+ fun argT v = TFree (v, the_sort v);
+ fun mk_d v = "d" ^ Library.unprefix "'" v;
+ fun mk_p v = "p" ^ Library.unprefix "'" v;
+ val args = maps (fn v => [(mk_d v, mk_DEFL (argT v)), (mk_p v, mk_LIFTDEFL (argT v))]) vs;
+ val typeTs = map argT (filter (member (op =) tfrees) vs);
+ val defl_args = map snd (filter (member (op =) frees o fst) args);
+ in
+ (typeTs, defl_args)
+ end;
+ val defl_flagss = map get_defl_flags doms;
(* declare deflation combinator constants *)
- fun declare_defl_const (vs, tbind, mx, rhs, morphs) thy =
+ fun declare_defl_const ((typeTs, defl_args), (_, tbind, _, _, _)) thy =
let
- fun argT v = TFree (v, the (AList.lookup (op =) sorts v));
- val Ts = map argT vs;
- val flags = map (is_bifinite thy) Ts;
- val defl_type = mk_defl_type flags Ts;
val defl_bind = Binding.suffix_name "_defl" tbind;
+ val defl_type =
+ map Term.itselfT typeTs ---> map (K deflT) defl_args -->> deflT;
in
Sign.declare_const ((defl_bind, defl_type), NoSyn) thy
end;
- val (defl_consts, thy) = fold_map declare_defl_const doms thy;
- val defl_names = map (fst o dest_Const) defl_consts;
+ val (defl_consts, thy) =
+ fold_map declare_defl_const (defl_flagss ~~ doms) thy;
(* defining equations for type combinators *)
- val dnames = map (fst o dest_Type o fst) dom_eqns;
- val defl_tab1 = DeflData.get thy;
- val defl_tab2 = Symtab.make (dnames ~~ (defl_names ~~ defl_flagss));
- val defl_tab' = Symtab.merge (K true) (defl_tab1, defl_tab2);
- val thy = DeflData.put defl_tab' thy;
+ fun mk_defl_term (defl_const, (typeTs, defl_args)) =
+ let
+ val type_args = map Logic.mk_type typeTs;
+ in
+ list_ccomb (list_comb (defl_const, type_args), defl_args)
+ end;
+ val defl_terms = map mk_defl_term (defl_consts ~~ defl_flagss);
+ val defl_tab = map fst dom_eqns ~~ defl_terms;
+ val defl_tab' = map fst dom_eqns ~~ map mk_u_defl defl_terms;
fun mk_defl_spec (lhsT, rhsT) =
- mk_eqs (defl_of_typ thy defl_tab' lhsT,
- defl_of_typ thy defl_tab' rhsT);
+ mk_eqs (defl_of_typ tmp_thy defl_tab defl_tab' lhsT,
+ defl_of_typ tmp_thy defl_tab defl_tab' rhsT);
val defl_specs = map mk_defl_spec dom_eqns;
(* register recursive definition of deflation combinators *)
@@ -495,20 +519,17 @@
add_fixdefs (defl_binds ~~ defl_specs) thy;
(* define types using deflation combinators *)
- fun make_repdef ((vs, tbind, mx, _, _), defl_const) thy =
+ fun make_repdef ((vs, tbind, mx, _, _), defl) thy =
let
- fun tfree a = TFree (a, the (AList.lookup (op =) sorts a));
- val Ts = map tfree vs;
- val type_args = map Logic.mk_type (filter_out (is_bifinite thy) Ts);
- val defl_args = map mk_DEFL (filter (is_bifinite thy) Ts);
- val defl = list_ccomb (list_comb (defl_const, type_args), defl_args);
- val ((_, _, _, {DEFL, ...}), thy) =
- Repdef.add_repdef false NONE (tbind, map (rpair dummyS) vs, mx) defl NONE thy;
+ val spec = (tbind, map (rpair dummyS) vs, mx);
+ val ((_, _, _, {DEFL, liftemb_def, liftprj_def, ...}), thy) =
+ Repdef.add_repdef false NONE spec defl NONE thy;
+ (* declare domain_defl_simps rules *)
+ val thy = Context.theory_map (RepData.add_thm DEFL) thy;
in
(DEFL, thy)
end;
- val (DEFL_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy;
- val thy = fold (Context.theory_map o RepData.add_thm) DEFL_thms thy;
+ val (DEFL_thms, thy) = fold_map make_repdef (doms ~~ defl_terms) thy;
(* prove DEFL equations *)
fun mk_DEFL_eq_thm (lhsT, rhsT) =
@@ -517,7 +538,7 @@
val DEFL_simps = RepData.get (ProofContext.init_global thy);
val tac =
rewrite_goals_tac (map mk_meta_eq DEFL_simps)
- THEN resolve_tac defl_unfold_thms 1;
+ THEN TRY (resolve_tac defl_unfold_thms 1);
in
Goal.prove_global thy [] [] goal (K tac)
end;
@@ -592,18 +613,22 @@
let
fun unprime a = Library.unprefix "'" a;
fun mk_d T = Free ("d" ^ unprime (fst (dest_TFree T)), deflT);
+ fun mk_p T = Free ("p" ^ unprime (fst (dest_TFree T)), deflT);
fun mk_f T = Free ("f" ^ unprime (fst (dest_TFree T)), T ->> T);
- fun mk_assm T = mk_trp (isodefl_const T $ mk_f T $ mk_d T);
- fun mk_goal ((map_const, defl_const), (T, rhsT)) =
+ fun mk_assm t =
+ case try dest_LIFTDEFL t of
+ SOME T => mk_trp (isodefl_const (mk_upT T) $ mk_u_map (mk_f T) $ mk_p T)
+ | NONE =>
+ let val T = dest_DEFL t
+ in mk_trp (isodefl_const T $ mk_f T $ mk_d T) end;
+ fun mk_goal (map_const, (T, rhsT)) =
let
val (_, Ts) = dest_Type T;
val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts));
- val type_args = map Logic.mk_type (filter_out (is_bifinite thy) Ts);
- val defl_args = map mk_d (filter (is_bifinite thy) Ts);
- val defl_term = list_ccomb (list_comb (defl_const, type_args), defl_args);
+ val defl_term = defl_of_typ thy (Ts ~~ map mk_d Ts) (Ts ~~ map mk_p Ts) T;
in isodefl_const T $ map_term $ defl_term end;
- val assms = (map mk_assm o filter (is_cpo thy) o snd o dest_Type o fst o hd) dom_eqns;
- val goals = map mk_goal (map_consts ~~ defl_consts ~~ dom_eqns);
+ val assms = (map mk_assm o snd o hd) defl_flagss;
+ val goals = map mk_goal (map_consts ~~ dom_eqns);
val goal = mk_trp (foldr1 HOLogic.mk_conj goals);
val start_thms =
@{thm split_def} :: defl_apply_thms @ map_apply_thms;
@@ -611,10 +636,10 @@
@{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id};
val bottom_rules =
@{thms fst_strict snd_strict isodefl_bottom simp_thms};
- val lthy = ProofContext.init_global thy;
- val DEFL_simps = map (fn th => th RS sym) (RepData.get lthy);
+ val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy;
+ val map_ID_simps = map (fn th => th RS sym) map_ID_thms;
val isodefl_rules =
- @{thms conjI isodefl_ID_DEFL}
+ @{thms conjI isodefl_ID_DEFL isodefl_LIFTDEFL}
@ isodefl_abs_rep_thms
@ IsodeflData.get (ProofContext.init_global thy);
in
@@ -628,7 +653,7 @@
simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
simp_tac beta_ss 1,
simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1,
- simp_tac (HOL_basic_ss addsimps DEFL_simps) 1,
+ simp_tac (HOL_basic_ss addsimps map_ID_simps) 1,
REPEAT (etac @{thm conjE} 1),
REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)])
end;
@@ -656,7 +681,7 @@
[rtac @{thm isodefl_DEFL_imp_ID} 1,
stac DEFL_thm 1,
rtac isodefl_thm 1,
- REPEAT (rtac @{thm isodefl_ID_DEFL} 1)];
+ REPEAT (resolve_tac @{thms isodefl_ID_DEFL isodefl_LIFTDEFL} 1)];
in
Goal.prove_global thy [] [] goal (K tac)
end;
@@ -665,9 +690,8 @@
map prove_map_ID_thm
(map_consts ~~ dom_eqns ~~ DEFL_thms ~~ isodefl_thms);
val (_, thy) = thy |>
- (Global_Theory.add_thms o map Thm.no_attributes)
+ (Global_Theory.add_thms o map (rpair [Domain_Take_Proofs.map_ID_add]))
(map_ID_binds ~~ map_ID_thms);
- val thy = fold (Context.theory_map o MapIdData.add_thm) map_ID_thms thy;
(* definitions and proofs related to take functions *)
val (take_info, thy) =
@@ -685,7 +709,7 @@
list_ccomb (map_const, map mk_ID (filter is_cpo (snd (dest_Type lhsT))));
val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns));
val goal = mk_trp (mk_eq (lhs, rhs));
- val map_ID_thms = MapIdData.get (ProofContext.init_global thy);
+ val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy;
val start_rules =
@{thms thelub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms
@ @{thms pair_collapse split_def}
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Fri Nov 12 12:57:02 2010 +0100
@@ -59,6 +59,8 @@
val get_map_tab : theory -> (string * bool list) Symtab.table
val add_deflation_thm : thm -> theory -> theory
val get_deflation_thms : theory -> thm list
+ val map_ID_add : attribute
+ val get_map_ID_thms : theory -> thm list
val setup : theory -> theory
end;
@@ -134,6 +136,12 @@
val description = "theorems like deflation a ==> deflation (foo_map$a)"
);
+structure Map_Id_Data = Named_Thms
+(
+ val name = "domain_map_ID"
+ val description = "theorems like foo_map$ID = ID"
+);
+
fun add_map_function (tname, map_name, bs) =
MapData.map (Symtab.insert (K true) (tname, (map_name, bs)));
@@ -143,7 +151,10 @@
val get_map_tab = MapData.get;
fun get_deflation_thms thy = DeflMapData.get (ProofContext.init_global thy);
-val setup = DeflMapData.setup;
+val map_ID_add = Map_Id_Data.add;
+val get_map_ID_thms = Map_Id_Data.get o ProofContext.init_global;
+
+val setup = DeflMapData.setup #> Map_Id_Data.setup;
(******************************************************************************)
(************************** building types and terms **************************)
@@ -183,30 +194,15 @@
fun map_of_typ (thy : theory) (sub : (typ * term) list) (T : typ) : term =
let
- val map_tab = get_map_tab thy;
- fun auto T = T ->> T;
- fun map_of T =
- case AList.lookup (op =) sub T of
- SOME m => (m, true) | NONE => map_of' T
- and map_of' (T as (Type (c, Ts))) =
- (case Symtab.lookup map_tab c of
- SOME (map_name, ds) =>
- let
- val Ts' = map snd (filter fst (ds ~~ Ts));
- val map_type = map auto Ts' -->> auto T;
- val (ms, bs) = map_split map_of Ts';
- in
- if exists I bs
- then (list_ccomb (Const (map_name, map_type), ms), true)
- else (mk_ID T, false)
- end
- | NONE => (mk_ID T, false))
- | map_of' T = (mk_ID T, false);
+ val thms = get_map_ID_thms thy;
+ val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) thms;
+ val rules' = map (apfst mk_ID) sub @ map swap rules;
in
- fst (map_of T)
+ mk_ID T
+ |> Pattern.rewrite_term thy rules' []
+ |> Pattern.rewrite_term thy rules []
end;
-
(******************************************************************************)
(********************* declaring definitions and theorems *********************)
(******************************************************************************)
--- a/src/HOLCF/Tools/repdef.ML Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Tools/repdef.ML Fri Nov 12 12:57:02 2010 +0100
@@ -7,7 +7,15 @@
signature REPDEF =
sig
type rep_info =
- { emb_def: thm, prj_def: thm, defl_def: thm, DEFL: thm }
+ {
+ emb_def : thm,
+ prj_def : thm,
+ defl_def : thm,
+ liftemb_def : thm,
+ liftprj_def : thm,
+ liftdefl_def : thm,
+ DEFL : thm
+ }
val add_repdef: bool -> binding option -> binding * (string * sort) list * mixfix ->
term -> (binding * binding) option -> theory ->
@@ -28,7 +36,15 @@
(** type definitions **)
type rep_info =
- { emb_def: thm, prj_def: thm, defl_def: thm, DEFL: thm };
+ {
+ emb_def : thm,
+ prj_def : thm,
+ defl_def : thm,
+ liftemb_def : thm,
+ liftprj_def : thm,
+ liftdefl_def : thm,
+ DEFL : thm
+ };
(* building types and terms *)
@@ -37,6 +53,18 @@
fun emb_const T = Const (@{const_name emb}, T ->> udomT);
fun prj_const T = Const (@{const_name prj}, udomT ->> T);
fun defl_const T = Const (@{const_name defl}, Term.itselfT T --> deflT);
+fun liftemb_const T = Const (@{const_name liftemb}, mk_upT T ->> udomT);
+fun liftprj_const T = Const (@{const_name liftprj}, udomT ->> mk_upT T);
+fun liftdefl_const T = Const (@{const_name liftdefl}, Term.itselfT T --> deflT);
+
+fun mk_u_map t =
+ let
+ val (T, U) = dest_cfunT (fastype_of t);
+ val u_map_type = (T ->> U) ->> (mk_upT T ->> mk_upT U);
+ val u_map_const = Const (@{const_name u_map}, u_map_type);
+ in
+ mk_capply (u_map_const, t)
+ end;
fun mk_cast (t, x) =
capply_const (udomT, udomT)
@@ -100,30 +128,54 @@
Abs ("x", udomT, Abs_const $ mk_cast (defl, Bound 0)));
val defl_eqn = Logic.mk_equals (defl_const newT,
Abs ("x", Term.itselfT newT, defl));
+ val liftemb_eqn =
+ Logic.mk_equals (liftemb_const newT,
+ mk_cfcomp (@{term "udom_emb u_approx"}, mk_u_map (emb_const newT)));
+ val liftprj_eqn =
+ Logic.mk_equals (liftprj_const newT,
+ mk_cfcomp (mk_u_map (prj_const newT), @{term "udom_prj u_approx"}));
+ val liftdefl_eqn =
+ Logic.mk_equals (liftdefl_const newT,
+ Abs ("t", Term.itselfT newT,
+ mk_capply (@{const u_defl}, defl_const newT $ Logic.mk_type newT)));
+
val name_def = Binding.suffix_name "_def" name;
val emb_bind = (Binding.prefix_name "emb_" name_def, []);
val prj_bind = (Binding.prefix_name "prj_" name_def, []);
val defl_bind = (Binding.prefix_name "defl_" name_def, []);
+ val liftemb_bind = (Binding.prefix_name "liftemb_" name_def, []);
+ val liftprj_bind = (Binding.prefix_name "liftprj_" name_def, []);
+ val liftdefl_bind = (Binding.prefix_name "liftdefl_" name_def, []);
(*instantiate class rep*)
val lthy = thy
- |> Class.instantiation ([full_tname], lhs_tfrees, @{sort bifinite});
+ |> Class.instantiation ([full_tname], lhs_tfrees, @{sort liftdomain});
val ((_, (_, emb_ldef)), lthy) =
Specification.definition (NONE, (emb_bind, emb_eqn)) lthy;
val ((_, (_, prj_ldef)), lthy) =
Specification.definition (NONE, (prj_bind, prj_eqn)) lthy;
val ((_, (_, defl_ldef)), lthy) =
Specification.definition (NONE, (defl_bind, defl_eqn)) lthy;
+ val ((_, (_, liftemb_ldef)), lthy) =
+ Specification.definition (NONE, (liftemb_bind, liftemb_eqn)) lthy;
+ val ((_, (_, liftprj_ldef)), lthy) =
+ Specification.definition (NONE, (liftprj_bind, liftprj_eqn)) lthy;
+ val ((_, (_, liftdefl_ldef)), lthy) =
+ Specification.definition (NONE, (liftdefl_bind, liftdefl_eqn)) lthy;
val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy);
val emb_def = singleton (ProofContext.export lthy ctxt_thy) emb_ldef;
val prj_def = singleton (ProofContext.export lthy ctxt_thy) prj_ldef;
val defl_def = singleton (ProofContext.export lthy ctxt_thy) defl_ldef;
+ val liftemb_def = singleton (ProofContext.export lthy ctxt_thy) liftemb_ldef;
+ val liftprj_def = singleton (ProofContext.export lthy ctxt_thy) liftprj_ldef;
+ val liftdefl_def = singleton (ProofContext.export lthy ctxt_thy) liftdefl_ldef;
val type_definition_thm =
MetaSimplifier.rewrite_rule
(the_list (#set_def (#2 info)))
(#type_definition (#2 info));
val typedef_thms =
- [type_definition_thm, #below_def cpo_info, emb_def, prj_def, defl_def];
+ [type_definition_thm, #below_def cpo_info, emb_def, prj_def, defl_def,
+ liftemb_def, liftprj_def, liftdefl_def];
val thy = lthy
|> Class.prove_instantiation_instance
(K (Tactic.rtac (@{thm typedef_rep_class} OF typedef_thms) 1))
@@ -139,7 +191,9 @@
||> Sign.restore_naming thy;
val rep_info =
- { emb_def = emb_def, prj_def = prj_def, defl_def = defl_def, DEFL = DEFL_thm };
+ { emb_def = emb_def, prj_def = prj_def, defl_def = defl_def,
+ liftemb_def = liftemb_def, liftprj_def = liftprj_def,
+ liftdefl_def = liftdefl_def, DEFL = DEFL_thm };
in
((info, cpo_info, pcpo_info, rep_info), thy)
end
--- a/src/HOLCF/Tutorial/Domain_ex.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Tutorial/Domain_ex.thy Fri Nov 12 12:57:02 2010 +0100
@@ -105,13 +105,13 @@
text {* Lazy constructor arguments may have unpointed types. *}
-domain (unsafe) natlist = nnil | ncons (lazy "nat discr") natlist
+domain natlist = nnil | ncons (lazy "nat discr") natlist
text {* Class constraints may be given for type parameters on the LHS. *}
-domain (unsafe) ('a::cpo) box = Box (lazy 'a)
+domain ('a::predomain) box = Box (lazy 'a)
-domain (unsafe) ('a::type) stream = snil | scons (lazy "'a discr") "'a stream"
+domain ('a::countable) stream = snil | scons (lazy "'a discr") "'a stream"
subsection {* Generated constants and theorems *}
--- a/src/HOLCF/Tutorial/New_Domain.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Tutorial/New_Domain.thy Fri Nov 12 12:57:02 2010 +0100
@@ -13,10 +13,8 @@
package. This file should be merged with @{text Domain_ex.thy}.
*}
-default_sort bifinite
-
text {*
- Provided that @{text bifinite} is the default sort, the @{text new_domain}
+ Provided that @{text domain} is the default sort, the @{text new_domain}
package should work with any type definition supported by the old
domain package.
*}
--- a/src/HOLCF/Universal.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Universal.thy Fri Nov 12 12:57:02 2010 +0100
@@ -851,7 +851,7 @@
unfolding approximants_def
apply safe
apply (simp add: compactD2 [OF compact_Rep_compact_basis Y])
- apply (erule below_trans, rule is_ub_thelub [OF Y])
+ apply (erule below_lub [OF Y])
done
next
fix a :: "'a compact_basis"
@@ -990,14 +990,12 @@
lemma lub_udom_approx [simp]: "(\<Squnion>i. udom_approx i) = ID"
apply (rule cfun_eqI, simp add: contlub_cfun_fun)
apply (rule below_antisym)
-apply (rule is_lub_thelub)
+apply (rule lub_below)
apply (simp)
-apply (rule ub_rangeI)
apply (rule udom_approx.below)
apply (rule_tac x=x in udom.principal_induct)
apply (simp add: lub_distribs)
-apply (rule rev_below_trans)
-apply (rule_tac x=a in is_ub_thelub)
+apply (rule_tac i=a in below_lub)
apply simp
apply (simp add: udom_approx_principal)
apply (simp add: ubasis_until_same ubasis_le_refl)
--- a/src/HOLCF/Up.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/Up.thy Fri Nov 12 12:57:02 2010 +0100
@@ -1,11 +1,12 @@
(* Title: HOLCF/Up.thy
- Author: Franz Regensburger and Brian Huffman
+ Author: Franz Regensburger
+ Author: Brian Huffman
*)
header {* The type of lifted values *}
theory Up
-imports Deflation
+imports Cfun
begin
default_sort cpo
@@ -259,47 +260,4 @@
lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
by (cases x, simp_all)
-subsection {* Map function for lifted cpo *}
-
-definition
- u_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u"
-where
- "u_map = (\<Lambda> f. fup\<cdot>(up oo f))"
-
-lemma u_map_strict [simp]: "u_map\<cdot>f\<cdot>\<bottom> = \<bottom>"
-unfolding u_map_def by simp
-
-lemma u_map_up [simp]: "u_map\<cdot>f\<cdot>(up\<cdot>x) = up\<cdot>(f\<cdot>x)"
-unfolding u_map_def by simp
-
-lemma u_map_ID: "u_map\<cdot>ID = ID"
-unfolding u_map_def by (simp add: cfun_eq_iff eta_cfun)
-
-lemma u_map_map: "u_map\<cdot>f\<cdot>(u_map\<cdot>g\<cdot>p) = u_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>p"
-by (induct p) simp_all
-
-lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)"
-apply default
-apply (case_tac x, simp, simp add: ep_pair.e_inverse)
-apply (case_tac y, simp, simp add: ep_pair.e_p_below)
-done
-
-lemma deflation_u_map: "deflation d \<Longrightarrow> deflation (u_map\<cdot>d)"
-apply default
-apply (case_tac x, simp, simp add: deflation.idem)
-apply (case_tac x, simp, simp add: deflation.below)
-done
-
-lemma finite_deflation_u_map:
- assumes "finite_deflation d" shows "finite_deflation (u_map\<cdot>d)"
-proof (rule finite_deflation_intro)
- interpret d: finite_deflation d by fact
- have "deflation d" by fact
- thus "deflation (u_map\<cdot>d)" by (rule deflation_u_map)
- have "{x. u_map\<cdot>d\<cdot>x = x} \<subseteq> insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x. d\<cdot>x = x})"
- by (rule subsetI, case_tac x, simp_all)
- thus "finite {x. u_map\<cdot>d\<cdot>x = x}"
- by (rule finite_subset, simp add: d.finite_fixes)
-qed
-
end
--- a/src/HOLCF/UpperPD.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/UpperPD.thy Fri Nov 12 12:57:02 2010 +0100
@@ -76,7 +76,7 @@
"{S::'a pd_basis set. upper_le.ideal S}"
by (fast intro: upper_le.ideal_principal)
-instantiation upper_pd :: (bifinite) below
+instantiation upper_pd :: ("domain") below
begin
definition
@@ -85,11 +85,11 @@
instance ..
end
-instance upper_pd :: (bifinite) po
+instance upper_pd :: ("domain") po
using type_definition_upper_pd below_upper_pd_def
by (rule upper_le.typedef_ideal_po)
-instance upper_pd :: (bifinite) cpo
+instance upper_pd :: ("domain") cpo
using type_definition_upper_pd below_upper_pd_def
by (rule upper_le.typedef_ideal_cpo)
@@ -108,7 +108,7 @@
lemma upper_pd_minimal: "upper_principal (PDUnit compact_bot) \<sqsubseteq> ys"
by (induct ys rule: upper_pd.principal_induct, simp, simp)
-instance upper_pd :: (bifinite) pcpo
+instance upper_pd :: ("domain") pcpo
by intro_classes (fast intro: upper_pd_minimal)
lemma inst_upper_pd_pcpo: "\<bottom> = upper_principal (PDUnit compact_bot)"
@@ -428,7 +428,7 @@
by (rule finite_range_imp_finite_fixes)
qed
-subsection {* Upper powerdomain is a bifinite domain *}
+subsection {* Upper powerdomain is a domain *}
definition
upper_approx :: "nat \<Rightarrow> udom upper_pd \<rightarrow> udom upper_pd"
@@ -436,16 +436,8 @@
"upper_approx = (\<lambda>i. upper_map\<cdot>(udom_approx i))"
lemma upper_approx: "approx_chain upper_approx"
-proof (rule approx_chain.intro)
- show "chain (\<lambda>i. upper_approx i)"
- unfolding upper_approx_def by simp
- show "(\<Squnion>i. upper_approx i) = ID"
- unfolding upper_approx_def
- by (simp add: lub_distribs upper_map_ID)
- show "\<And>i. finite_deflation (upper_approx i)"
- unfolding upper_approx_def
- by (intro finite_deflation_upper_map finite_deflation_udom_approx)
-qed
+using upper_map_ID finite_deflation_upper_map
+unfolding upper_approx_def by (rule approx_chain_lemma1)
definition upper_defl :: "defl \<rightarrow> defl"
where "upper_defl = defl_fun1 upper_approx upper_map"
@@ -453,12 +445,10 @@
lemma cast_upper_defl:
"cast\<cdot>(upper_defl\<cdot>A) =
udom_emb upper_approx oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj upper_approx"
-unfolding upper_defl_def
-apply (rule cast_defl_fun1 [OF upper_approx])
-apply (erule finite_deflation_upper_map)
-done
+using upper_approx finite_deflation_upper_map
+unfolding upper_defl_def by (rule cast_defl_fun1)
-instantiation upper_pd :: (bifinite) bifinite
+instantiation upper_pd :: ("domain") liftdomain
begin
definition
@@ -470,7 +460,18 @@
definition
"defl (t::'a upper_pd itself) = upper_defl\<cdot>DEFL('a)"
-instance proof
+definition
+ "(liftemb :: 'a upper_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl (t::'a upper_pd itself) = u_defl\<cdot>DEFL('a upper_pd)"
+
+instance
+using liftemb_upper_pd_def liftprj_upper_pd_def liftdefl_upper_pd_def
+proof (rule liftdomain_class_intro)
show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)"
unfolding emb_upper_pd_def prj_upper_pd_def
using ep_pair_udom [OF upper_approx]
--- a/src/HOLCF/ex/Domain_Proofs.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/ex/Domain_Proofs.thy Fri Nov 12 12:57:02 2010 +0100
@@ -8,8 +8,6 @@
imports HOLCF
begin
-default_sort bifinite
-
(*
The definitions and proofs below are for the following recursive
@@ -19,6 +17,9 @@
and 'a bar = Bar (lazy "'a baz \<rightarrow> tr")
and 'a baz = Baz (lazy "'a foo convex_pd \<rightarrow> tr")
+TODO: add another type parameter that is strict,
+to show the different handling of LIFTDEFL vs. DEFL.
+
*)
(********************************************************************)
@@ -32,13 +33,13 @@
"defl \<rightarrow> defl \<times> defl \<times> defl \<rightarrow> defl \<times> defl \<times> defl"
where
"foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3).
- ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t2))
+ ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>t2))
, u_defl\<cdot>(cfun_defl\<cdot>t3\<cdot>DEFL(tr))
, u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>t1)\<cdot>DEFL(tr)))))"
lemma foo_bar_baz_deflF_beta:
"foo_bar_baz_deflF\<cdot>a\<cdot>t =
- ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(fst (snd t))))
+ ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>(fst (snd t))))
, u_defl\<cdot>(cfun_defl\<cdot>(snd (snd t))\<cdot>DEFL(tr))
, u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(fst t))\<cdot>DEFL(tr)))"
unfolding foo_bar_baz_deflF_def
@@ -64,7 +65,7 @@
text {* Unfold rules for each combinator. *}
lemma foo_defl_unfold:
- "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
+ "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(baz_defl\<cdot>a)\<cdot>DEFL(tr))"
@@ -82,28 +83,37 @@
text {* Use @{text pcpodef} with the appropriate type combinator. *}
-pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>DEFL('a))"
+pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>LIFTDEFL('a))"
by (rule defl_set_bottom, rule adm_defl_set)
-pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>DEFL('a))"
+pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>LIFTDEFL('a))"
by (rule defl_set_bottom, rule adm_defl_set)
-pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>DEFL('a))"
+pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>LIFTDEFL('a))"
by (rule defl_set_bottom, rule adm_defl_set)
text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
-instantiation foo :: (bifinite) bifinite
+instantiation foo :: ("domain") liftdomain
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>DEFL('a))\<cdot>y))"
+where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
definition defl_foo :: "'a foo itself \<Rightarrow> defl"
-where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>DEFL('a)"
+where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>LIFTDEFL('a)"
+
+definition
+ "(liftemb :: 'a foo u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> 'a foo u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl \<equiv> \<lambda>(t::'a foo itself). u_defl\<cdot>DEFL('a foo)"
instance
apply (rule typedef_rep_class)
@@ -112,21 +122,33 @@
apply (rule emb_foo_def)
apply (rule prj_foo_def)
apply (rule defl_foo_def)
+apply (rule liftemb_foo_def)
+apply (rule liftprj_foo_def)
+apply (rule liftdefl_foo_def)
done
end
-instantiation bar :: (bifinite) bifinite
+instantiation bar :: ("domain") liftdomain
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>DEFL('a))\<cdot>y))"
+where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
definition defl_bar :: "'a bar itself \<Rightarrow> defl"
-where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>DEFL('a)"
+where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>LIFTDEFL('a)"
+
+definition
+ "(liftemb :: 'a bar u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> 'a bar u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl \<equiv> \<lambda>(t::'a bar itself). u_defl\<cdot>DEFL('a bar)"
instance
apply (rule typedef_rep_class)
@@ -135,21 +157,33 @@
apply (rule emb_bar_def)
apply (rule prj_bar_def)
apply (rule defl_bar_def)
+apply (rule liftemb_bar_def)
+apply (rule liftprj_bar_def)
+apply (rule liftdefl_bar_def)
done
end
-instantiation baz :: (bifinite) bifinite
+instantiation baz :: ("domain") liftdomain
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>DEFL('a))\<cdot>y))"
+where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
definition defl_baz :: "'a baz itself \<Rightarrow> defl"
-where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>DEFL('a)"
+where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>LIFTDEFL('a)"
+
+definition
+ "(liftemb :: 'a baz u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> 'a baz u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "liftdefl \<equiv> \<lambda>(t::'a baz itself). u_defl\<cdot>DEFL('a baz)"
instance
apply (rule typedef_rep_class)
@@ -158,42 +192,42 @@
apply (rule emb_baz_def)
apply (rule prj_baz_def)
apply (rule defl_baz_def)
+apply (rule liftemb_baz_def)
+apply (rule liftprj_baz_def)
+apply (rule liftdefl_baz_def)
done
end
text {* Prove DEFL rules using lemma @{text typedef_DEFL}. *}
-lemma DEFL_foo: "DEFL('a foo) = foo_defl\<cdot>DEFL('a)"
+lemma DEFL_foo: "DEFL('a foo) = foo_defl\<cdot>LIFTDEFL('a)"
apply (rule typedef_DEFL)
apply (rule defl_foo_def)
done
-lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>DEFL('a)"
+lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>LIFTDEFL('a)"
apply (rule typedef_DEFL)
apply (rule defl_bar_def)
done
-lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>DEFL('a)"
+lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>LIFTDEFL('a)"
apply (rule typedef_DEFL)
apply (rule defl_baz_def)
done
text {* Prove DEFL equations using type combinator unfold lemmas. *}
-lemmas DEFL_simps =
- DEFL_ssum DEFL_sprod DEFL_u DEFL_cfun
-
lemma DEFL_foo': "DEFL('a foo) = DEFL(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
-unfolding DEFL_foo DEFL_bar DEFL_baz DEFL_simps
+unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
by (rule foo_defl_unfold)
lemma DEFL_bar': "DEFL('a bar) = DEFL(('a baz \<rightarrow> tr)\<^sub>\<bottom>)"
-unfolding DEFL_foo DEFL_bar DEFL_baz DEFL_simps
+unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
by (rule bar_defl_unfold)
lemma DEFL_baz': "DEFL('a baz) = DEFL(('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>)"
-unfolding DEFL_foo DEFL_bar DEFL_baz DEFL_simps DEFL_convex
+unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
by (rule baz_defl_unfold)
(********************************************************************)
@@ -314,7 +348,7 @@
text {* Prove isodefl rules for all map functions simultaneously. *}
lemma isodefl_foo_bar_baz:
- assumes isodefl_d: "isodefl d t"
+ assumes isodefl_d: "isodefl (u_map\<cdot>d) t"
shows
"isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and>
isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and>
@@ -332,8 +366,8 @@
isodefl_foo_abs
isodefl_bar_abs
isodefl_baz_abs
- isodefl_ssum isodefl_sprod isodefl_ID_DEFL
- isodefl_u isodefl_convex isodefl_cfun
+ domain_isodefl
+ isodefl_ID_DEFL isodefl_LIFTDEFL
isodefl_d
)
apply assumption+
@@ -349,21 +383,21 @@
apply (rule isodefl_DEFL_imp_ID)
apply (subst DEFL_foo)
apply (rule isodefl_foo)
-apply (rule isodefl_ID_DEFL)
+apply (rule isodefl_LIFTDEFL)
done
lemma bar_map_ID: "bar_map\<cdot>ID = ID"
apply (rule isodefl_DEFL_imp_ID)
apply (subst DEFL_bar)
apply (rule isodefl_bar)
-apply (rule isodefl_ID_DEFL)
+apply (rule isodefl_LIFTDEFL)
done
lemma baz_map_ID: "baz_map\<cdot>ID = ID"
apply (rule isodefl_DEFL_imp_ID)
apply (subst DEFL_baz)
apply (rule isodefl_baz)
-apply (rule isodefl_ID_DEFL)
+apply (rule isodefl_LIFTDEFL)
done
(********************************************************************)
--- a/src/HOLCF/ex/Powerdomain_ex.thy Fri Nov 12 11:36:01 2010 +0100
+++ b/src/HOLCF/ex/Powerdomain_ex.thy Fri Nov 12 12:57:02 2010 +0100
@@ -8,8 +8,6 @@
imports HOLCF
begin
-default_sort bifinite
-
subsection {* Monadic sorting example *}
domain ordering = LT | EQ | GT