--- a/NEWS Sun Dec 19 19:03:49 2010 +0100
+++ b/NEWS Sun Dec 19 17:39:20 2010 -0800
@@ -487,12 +487,12 @@
Accordingly, users of the definitional package must remove any
'default_sort rep' declarations. INCOMPATIBILITY.
-* The old type classes 'profinite' and 'bifinite', along with the
-overloaded constant 'approx' have been removed. INCOMPATIBILITY.
-
-* The type 'udom alg_defl' has been replaced by the non-parameterized
-type 'defl'. HOLCF no longer defines an embedding of type defl into
-udom by default; the instance proof defl :: domain is now available in
+* The 'bifinite' class no longer fixes a constant 'approx'; the class
+now just asserts that such a function exists. INCOMPATIBILITY.
+
+* The type 'alg_defl' has been renamed to 'defl'. HOLCF no longer
+defines an embedding of type 'a defl into udom by default; instances
+of 'bifinite' and 'domain' classes are available in
HOLCF/Library/Defl_Bifinite.thy.
* The syntax 'REP('a)' has been replaced with 'DEFL('a)'.
--- a/src/HOL/HOLCF/Algebraic.thy Sun Dec 19 19:03:49 2010 +0100
+++ b/src/HOL/HOLCF/Algebraic.thy Sun Dec 19 17:39:20 2010 -0800
@@ -8,21 +8,23 @@
imports Universal Map_Functions
begin
+default_sort bifinite
+
subsection {* Type constructor for finite deflations *}
-typedef (open) fin_defl = "{d::udom \<rightarrow> udom. finite_deflation d}"
+typedef (open) 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
by (fast intro: finite_deflation_UU)
-instantiation fin_defl :: below
+instantiation fin_defl :: (bifinite) below
begin
definition below_fin_defl_def:
- "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep_fin_defl x \<sqsubseteq> Rep_fin_defl y"
+ "below \<equiv> \<lambda>x y. Rep_fin_defl x \<sqsubseteq> Rep_fin_defl y"
instance ..
end
-instance fin_defl :: po
+instance fin_defl :: (bifinite) po
using type_definition_fin_defl below_fin_defl_def
by (rule typedef_po)
@@ -72,10 +74,10 @@
subsection {* Defining algebraic deflations by ideal completion *}
-typedef (open) defl = "{S::fin_defl set. below.ideal S}"
+typedef (open) 'a defl = "{S::'a fin_defl set. below.ideal S}"
by (rule below.ex_ideal)
-instantiation defl :: below
+instantiation defl :: (bifinite) below
begin
definition
@@ -84,22 +86,23 @@
instance ..
end
-instance defl :: po
+instance defl :: (bifinite) po
using type_definition_defl below_defl_def
by (rule below.typedef_ideal_po)
-instance defl :: cpo
+instance defl :: (bifinite) cpo
using type_definition_defl below_defl_def
by (rule below.typedef_ideal_cpo)
definition
- defl_principal :: "fin_defl \<Rightarrow> defl" where
+ defl_principal :: "'a fin_defl \<Rightarrow> 'a defl" where
"defl_principal t = Abs_defl {u. u \<sqsubseteq> t}"
-lemma fin_defl_countable: "\<exists>f::fin_defl \<Rightarrow> nat. inj f"
-proof
- have *: "\<And>d. finite (approx_chain.place udom_approx `
- Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x})"
+lemma fin_defl_countable: "\<exists>f::'a fin_defl \<Rightarrow> nat. inj f"
+proof -
+ obtain f :: "'a compact_basis \<Rightarrow> nat" where inj_f: "inj f"
+ using compact_basis.countable ..
+ have *: "\<And>d. finite (f ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x})"
apply (rule finite_imageI)
apply (rule finite_vimageI)
apply (rule Rep_fin_defl.finite_fixes)
@@ -107,11 +110,11 @@
done
have range_eq: "range Rep_compact_basis = {x. compact x}"
using type_definition_compact_basis by (rule type_definition.Rep_range)
- show "inj (\<lambda>d. set_encode
- (approx_chain.place udom_approx ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x}))"
+ have "inj (\<lambda>d. set_encode
+ (f ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x}))"
apply (rule inj_onI)
apply (simp only: set_encode_eq *)
- apply (simp only: inj_image_eq_iff approx_chain.inj_place [OF udom_approx])
+ apply (simp only: inj_image_eq_iff inj_f)
apply (drule_tac f="image Rep_compact_basis" in arg_cong)
apply (simp del: vimage_Collect_eq add: range_eq set_eq_iff)
apply (rule Rep_fin_defl_inject [THEN iffD1])
@@ -121,6 +124,7 @@
apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
apply (drule_tac x=z in spec, simp)
done
+ thus ?thesis by - (rule exI)
qed
interpretation defl: ideal_completion below defl_principal Rep_defl
@@ -137,7 +141,7 @@
apply (simp add: Abs_fin_defl_inverse finite_deflation_UU)
done
-instance defl :: pcpo
+instance defl :: (bifinite) pcpo
by intro_classes (fast intro: defl_minimal)
lemma inst_defl_pcpo: "\<bottom> = defl_principal (Abs_fin_defl \<bottom>)"
@@ -146,7 +150,7 @@
subsection {* Applying algebraic deflations *}
definition
- cast :: "defl \<rightarrow> udom \<rightarrow> udom"
+ cast :: "'a defl \<rightarrow> 'a \<rightarrow> 'a"
where
"cast = defl.basis_fun Rep_fin_defl"
@@ -211,4 +215,66 @@
lemma cast_strict2 [simp]: "cast\<cdot>A\<cdot>\<bottom> = \<bottom>"
by (rule cast.below [THEN UU_I])
+subsection {* Deflation combinators *}
+
+definition
+ "defl_fun1 e p f =
+ defl.basis_fun (\<lambda>a.
+ defl_principal (Abs_fin_defl
+ (e oo f\<cdot>(Rep_fin_defl a) oo p)))"
+
+definition
+ "defl_fun2 e p f =
+ defl.basis_fun (\<lambda>a.
+ defl.basis_fun (\<lambda>b.
+ defl_principal (Abs_fin_defl
+ (e oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo p))))"
+
+lemma cast_defl_fun1:
+ assumes ep: "ep_pair e p"
+ assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)"
+ shows "cast\<cdot>(defl_fun1 e p f\<cdot>A) = e oo f\<cdot>(cast\<cdot>A) oo p"
+proof -
+ have 1: "\<And>a. finite_deflation (e oo f\<cdot>(Rep_fin_defl a) oo p)"
+ apply (rule ep_pair.finite_deflation_e_d_p [OF ep])
+ apply (rule f, rule finite_deflation_Rep_fin_defl)
+ done
+ show ?thesis
+ by (induct A rule: defl.principal_induct, simp)
+ (simp only: defl_fun1_def
+ defl.basis_fun_principal
+ defl.basis_fun_mono
+ defl.principal_mono
+ Abs_fin_defl_mono [OF 1 1]
+ monofun_cfun below_refl
+ Rep_fin_defl_mono
+ cast_defl_principal
+ Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
+qed
+
+lemma cast_defl_fun2:
+ assumes ep: "ep_pair e p"
+ assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow>
+ finite_deflation (f\<cdot>a\<cdot>b)"
+ shows "cast\<cdot>(defl_fun2 e p f\<cdot>A\<cdot>B) = e oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo p"
+proof -
+ have 1: "\<And>a b. finite_deflation
+ (e oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo p)"
+ apply (rule ep_pair.finite_deflation_e_d_p [OF ep])
+ apply (rule f, (rule finite_deflation_Rep_fin_defl)+)
+ done
+ show ?thesis
+ apply (induct A rule: defl.principal_induct, simp)
+ apply (induct B rule: defl.principal_induct, simp)
+ by (simp only: defl_fun2_def
+ defl.basis_fun_principal
+ defl.basis_fun_mono
+ defl.principal_mono
+ Abs_fin_defl_mono [OF 1 1]
+ monofun_cfun below_refl
+ Rep_fin_defl_mono
+ cast_defl_principal
+ Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
+qed
+
end
--- a/src/HOL/HOLCF/Bifinite.thy Sun Dec 19 19:03:49 2010 +0100
+++ b/src/HOL/HOLCF/Bifinite.thy Sun Dec 19 17:39:20 2010 -0800
@@ -2,659 +2,107 @@
Author: Brian Huffman
*)
-header {* Bifinite domains *}
+header {* Profinite and bifinite cpos *}
theory Bifinite
-imports Algebraic Map_Functions Countable
+imports Map_Functions Countable
+begin
+
+default_sort cpo
+
+subsection {* Chains of finite deflations *}
+
+locale approx_chain =
+ fixes approx :: "nat \<Rightarrow> 'a \<rightarrow> 'a"
+ assumes chain_approx [simp]: "chain (\<lambda>i. approx i)"
+ assumes lub_approx [simp]: "(\<Squnion>i. approx i) = ID"
+ assumes finite_deflation_approx [simp]: "\<And>i. finite_deflation (approx i)"
begin
-subsection {* Class of bifinite domains *}
-
-text {*
- 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 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"
-
-syntax "_DEFL" :: "type \<Rightarrow> defl" ("(1DEFL/(1'(_')))")
-translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)"
-
-interpretation "domain": pcpo_ep_pair emb prj
- unfolding pcpo_ep_pair_def
- by (rule ep_pair_emb_prj)
-
-lemmas emb_inverse = domain.e_inverse
-lemmas emb_prj_below = domain.e_p_below
-lemmas emb_eq_iff = domain.e_eq_iff
-lemmas emb_strict = domain.e_strict
-lemmas prj_strict = domain.p_strict
-
-subsection {* Domains have a countable compact basis *}
-
-text {*
- Eventually it should be possible to generalize this to an unpointed
- variant of the domain class.
-*}
-
-interpretation compact_basis:
- 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))"
- by (rule defl.obtain_principal_chain)
- def approx \<equiv> "\<lambda>i. (prj oo cast\<cdot>(defl_principal (Y i)) oo emb) :: 'a \<rightarrow> 'a"
- interpret defl_approx: approx_chain approx
- proof (rule approx_chain.intro)
- show "chain (\<lambda>i. approx i)"
- unfolding approx_def by (simp add: Y)
- show "(\<Squnion>i. approx i) = ID"
- unfolding approx_def
- 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 domain.finite_deflation_p_d_e)
- apply (rule finite_deflation_cast)
- apply (rule defl.compact_principal)
- apply (rule below_trans [OF monofun_cfun_fun])
- apply (rule is_ub_thelub, simp add: Y)
- apply (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL)
- done
- qed
- (* FIXME: why does show ?thesis fail here? *)
- show "ideal_completion below Rep_compact_basis (approximants::'a \<Rightarrow> _)" ..
-qed
+lemma deflation_approx: "deflation (approx i)"
+using finite_deflation_approx by (rule finite_deflation_imp_deflation)
-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 sfun_approx :: "nat \<Rightarrow> (udom \<rightarrow>! udom) \<rightarrow> (udom \<rightarrow>! udom)"
- where "sfun_approx = (\<lambda>i. sfun_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 approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
+using deflation_approx by (rule deflation.idem)
-lemma sfun_approx: "approx_chain sfun_approx"
-using sfun_map_ID finite_deflation_sfun_map
-unfolding sfun_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
- defl_fun1 ::
- "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (defl \<rightarrow> defl)"
-where
- "defl_fun1 approx f =
- defl.basis_fun (\<lambda>a.
- defl_principal (Abs_fin_defl
- (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)))"
-
-definition
- defl_fun2 ::
- "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a))
- \<Rightarrow> (defl \<rightarrow> defl \<rightarrow> defl)"
-where
- "defl_fun2 approx f =
- defl.basis_fun (\<lambda>a.
- defl.basis_fun (\<lambda>b.
- defl_principal (Abs_fin_defl
- (udom_emb approx oo
- f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx))))"
+lemma approx_below: "approx i\<cdot>x \<sqsubseteq> x"
+using deflation_approx by (rule deflation.below)
-lemma cast_defl_fun1:
- assumes approx: "approx_chain approx"
- assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)"
- shows "cast\<cdot>(defl_fun1 approx f\<cdot>A) = udom_emb approx oo f\<cdot>(cast\<cdot>A) oo udom_prj approx"
-proof -
- have 1: "\<And>a. finite_deflation
- (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)"
- apply (rule ep_pair.finite_deflation_e_d_p)
- apply (rule approx_chain.ep_pair_udom [OF approx])
- apply (rule f, rule finite_deflation_Rep_fin_defl)
- done
- show ?thesis
- by (induct A rule: defl.principal_induct, simp)
- (simp only: defl_fun1_def
- defl.basis_fun_principal
- defl.basis_fun_mono
- defl.principal_mono
- Abs_fin_defl_mono [OF 1 1]
- monofun_cfun below_refl
- Rep_fin_defl_mono
- cast_defl_principal
- Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
-qed
-
-lemma cast_defl_fun2:
- assumes approx: "approx_chain approx"
- assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow>
- finite_deflation (f\<cdot>a\<cdot>b)"
- shows "cast\<cdot>(defl_fun2 approx f\<cdot>A\<cdot>B) =
- udom_emb approx oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj approx"
-proof -
- have 1: "\<And>a b. finite_deflation (udom_emb approx oo
- f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx)"
- apply (rule ep_pair.finite_deflation_e_d_p)
- apply (rule ep_pair_udom [OF approx])
- apply (rule f, (rule finite_deflation_Rep_fin_defl)+)
- done
- show ?thesis
- by (induct A B rule: defl.principal_induct2, simp, simp)
- (simp only: defl_fun2_def
- defl.basis_fun_principal
- defl.basis_fun_mono
- defl.principal_mono
- Abs_fin_defl_mono [OF 1 1]
- monofun_cfun below_refl
- Rep_fin_defl_mono
- cast_defl_principal
- Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
-qed
-
-definition u_defl :: "defl \<rightarrow> defl"
- where "u_defl = defl_fun1 u_approx u_map"
-
-definition sfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
- where "sfun_defl = defl_fun2 sfun_approx sfun_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_sfun_defl:
- "cast\<cdot>(sfun_defl\<cdot>A\<cdot>B) =
- udom_emb sfun_approx oo sfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj sfun_approx"
-using sfun_approx finite_deflation_sfun_map
-unfolding sfun_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)
+lemma finite_range_approx: "finite (range (\<lambda>x. approx i\<cdot>x))"
+apply (rule finite_deflation.finite_range)
+apply (rule finite_deflation_approx)
+done
-subsection {* Lemma for proving domain instances *}
-
-text {*
- A class of domains where @{const liftemb}, @{const liftprj},
- and @{const liftdefl} are all defined in the standard way.
-*}
-
-class liftdomain = "domain" +
- assumes liftemb_eq: "liftemb = 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. *}
+lemma compact_approx: "compact (approx n\<cdot>x)"
+apply (rule finite_deflation.compact)
+apply (rule finite_deflation_approx)
+done
-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]:
- "emb = (ID :: udom \<rightarrow> udom)"
-
-definition [simp]:
- "prj = (ID :: udom \<rightarrow> udom)"
-
-definition
- "defl (t::udom itself) = (\<Squnion>i. defl_principal (Abs_fin_defl (udom_approx i)))"
-
-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)
- show "cast\<cdot>DEFL(udom) = emb oo (prj :: udom \<rightarrow> udom)"
- unfolding defl_udom_def
- apply (subst contlub_cfun_arg)
- apply (rule chainI)
- apply (rule defl.principal_mono)
- apply (simp add: below_fin_defl_def)
- apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
- apply (rule chainE)
- apply (rule chain_udom_approx)
- apply (subst cast_defl_principal)
- apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
- done
-qed
+lemma compact_eq_approx: "compact x \<Longrightarrow> \<exists>i. approx i\<cdot>x = x"
+by (rule admD2, simp_all)
end
-subsubsection {* Lifted cpo *}
-
-instantiation u :: (predomain) liftdomain
-begin
-
-definition
- "emb = liftemb"
-
-definition
- "prj = liftprj"
+subsection {* Omega-profinite and bifinite domains *}
-definition
- "defl (t::'a u itself) = LIFTDEFL('a)"
-
-definition
- "(liftemb :: 'a u u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
-
-definition
- "(liftprj :: udom \<rightarrow> 'a u u) = u_map\<cdot>prj oo udom_prj u_approx"
-
-definition
- "liftdefl (t::'a u itself) = u_defl\<cdot>DEFL('a u)"
+class bifinite = pcpo +
+ assumes bifinite: "\<exists>(a::nat \<Rightarrow> 'a \<rightarrow> 'a). approx_chain a"
-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
-
-end
-
-lemma DEFL_u: "DEFL('a::predomain u) = LIFTDEFL('a)"
-by (rule defl_u_def)
-
-subsubsection {* Strict function space *}
+class profinite = cpo +
+ assumes profinite: "\<exists>(a::nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>). approx_chain a"
-instantiation sfun :: ("domain", "domain") liftdomain
-begin
-
-definition
- "emb = udom_emb sfun_approx oo sfun_map\<cdot>prj\<cdot>emb"
-
-definition
- "prj = sfun_map\<cdot>emb\<cdot>prj oo udom_prj sfun_approx"
-
-definition
- "defl (t::('a \<rightarrow>! 'b) itself) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
-
-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)"
+subsection {* Building approx chains *}
-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]
- by (intro ep_pair_comp ep_pair_sfun_map ep_pair_emb_prj)
- show "cast\<cdot>DEFL('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
- unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl
- by (simp add: cast_DEFL oo_def sfun_eq_iff sfun_map_map)
-qed
-
-end
-
-lemma DEFL_sfun:
- "DEFL('a::domain \<rightarrow>! 'b::domain) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
-by (rule defl_sfun_def)
-
-subsubsection {* Continuous function space *}
-
-text {*
- Types @{typ "'a \<rightarrow> 'b"} and @{typ "'a u \<rightarrow>! 'b"} are isomorphic.
-*}
-
-definition
- "encode_cfun = (\<Lambda> f. sfun_abs\<cdot>(fup\<cdot>f))"
-
-definition
- "decode_cfun = (\<Lambda> g x. sfun_rep\<cdot>g\<cdot>(up\<cdot>x))"
-
-lemma decode_encode_cfun [simp]: "decode_cfun\<cdot>(encode_cfun\<cdot>x) = x"
-unfolding encode_cfun_def decode_cfun_def
-by (simp add: eta_cfun)
-
-lemma encode_decode_cfun [simp]: "encode_cfun\<cdot>(decode_cfun\<cdot>y) = y"
-unfolding encode_cfun_def decode_cfun_def
-apply (simp add: sfun_eq_iff strictify_cancel)
-apply (rule cfun_eqI, case_tac x, simp_all)
-done
-
-instantiation cfun :: (predomain, "domain") liftdomain
-begin
-
-definition
- "emb = emb oo encode_cfun"
-
-definition
- "prj = decode_cfun oo prj"
-
-definition
- "defl (t::('a \<rightarrow> 'b) itself) = DEFL('a u \<rightarrow>! 'b)"
-
-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)
- have "ep_pair encode_cfun decode_cfun"
- by (rule ep_pair.intro, simp_all)
- thus "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
- unfolding emb_cfun_def prj_cfun_def
- using ep_pair_emb_prj by (rule ep_pair_comp)
- show "cast\<cdot>DEFL('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
- unfolding emb_cfun_def prj_cfun_def defl_cfun_def
- by (simp add: cast_DEFL cfcomp1)
+lemma approx_chain_iso:
+ assumes a: "approx_chain a"
+ assumes [simp]: "\<And>x. f\<cdot>(g\<cdot>x) = x"
+ assumes [simp]: "\<And>y. g\<cdot>(f\<cdot>y) = y"
+ shows "approx_chain (\<lambda>i. f oo a i oo g)"
+proof -
+ have 1: "f oo g = ID" by (simp add: cfun_eqI)
+ have 2: "ep_pair f g" by (simp add: ep_pair_def)
+ from 1 2 show ?thesis
+ using a unfolding approx_chain_def
+ by (simp add: lub_APP ep_pair.finite_deflation_e_d_p)
qed
-end
-
-lemma DEFL_cfun:
- "DEFL('a::predomain \<rightarrow> 'b::domain) = DEFL('a u \<rightarrow>! 'b)"
-by (rule defl_cfun_def)
-
-subsubsection {* Strict product *}
-
-instantiation sprod :: ("domain", "domain") liftdomain
-begin
-
-definition
- "emb = udom_emb sprod_approx oo sprod_map\<cdot>emb\<cdot>emb"
-
-definition
- "prj = sprod_map\<cdot>prj\<cdot>prj oo udom_prj sprod_approx"
-
-definition
- "defl (t::('a \<otimes> 'b) itself) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
-
-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)"
+lemma approx_chain_u_map:
+ assumes "approx_chain a"
+ shows "approx_chain (\<lambda>i. u_map\<cdot>(a i))"
+ using assms unfolding approx_chain_def
+ by (simp add: lub_APP u_map_ID finite_deflation_u_map)
-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]
- by (intro ep_pair_comp ep_pair_sprod_map ep_pair_emb_prj)
-next
- show "cast\<cdot>DEFL('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
- unfolding emb_sprod_def prj_sprod_def defl_sprod_def cast_sprod_defl
- by (simp add: cast_DEFL oo_def cfun_eq_iff sprod_map_map)
-qed
-
-end
-
-lemma DEFL_sprod:
- "DEFL('a::domain \<otimes> 'b::domain) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
-by (rule defl_sprod_def)
-
-subsubsection {* Cartesian product *}
-
-text {*
- Types @{typ "('a * 'b) u"} and @{typ "'a u \<otimes> 'b u"} are isomorphic.
-*}
+lemma approx_chain_sfun_map:
+ assumes "approx_chain a" and "approx_chain b"
+ shows "approx_chain (\<lambda>i. sfun_map\<cdot>(a i)\<cdot>(b i))"
+ using assms unfolding approx_chain_def
+ by (simp add: lub_APP sfun_map_ID finite_deflation_sfun_map)
-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
- "liftemb = emb oo encode_prod_u"
-
-definition
- "liftprj = decode_prod_u oo prj"
-
-definition
- "liftdefl (t::('a \<times> 'b) itself) = DEFL('a\<^sub>\<bottom> \<otimes> 'b\<^sub>\<bottom>)"
+lemma approx_chain_sprod_map:
+ assumes "approx_chain a" and "approx_chain b"
+ shows "approx_chain (\<lambda>i. sprod_map\<cdot>(a i)\<cdot>(b i))"
+ using assms unfolding approx_chain_def
+ by (simp add: lub_APP sprod_map_ID finite_deflation_sprod_map)
-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
- using ep_pair_emb_prj by (rule ep_pair_comp)
- show "cast\<cdot>LIFTDEFL('a \<times> 'b) = liftemb oo (liftprj :: udom \<rightarrow> ('a \<times> 'b) u)"
- unfolding liftemb_prod_def liftprj_prod_def liftdefl_prod_def
- by (simp add: cast_DEFL cfcomp1)
-qed
-
-end
-
-instantiation prod :: ("domain", "domain") "domain"
-begin
-
-definition
- "emb = udom_emb prod_approx oo cprod_map\<cdot>emb\<cdot>emb"
-
-definition
- "prj = cprod_map\<cdot>prj\<cdot>prj oo udom_prj prod_approx"
-
-definition
- "defl (t::('a \<times> 'b) itself) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
-
-instance proof
- show "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)"
- unfolding emb_prod_def prj_prod_def
- using ep_pair_udom [OF prod_approx]
- by (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj)
-next
- show "cast\<cdot>DEFL('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
- unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl
- by (simp add: cast_DEFL oo_def cfun_eq_iff cprod_map_map)
-qed
-
-end
-
-lemma DEFL_prod:
- "DEFL('a::domain \<times> 'b::domain) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
-by (rule defl_prod_def)
+lemma approx_chain_ssum_map:
+ assumes "approx_chain a" and "approx_chain b"
+ shows "approx_chain (\<lambda>i. ssum_map\<cdot>(a i)\<cdot>(b i))"
+ using assms unfolding approx_chain_def
+ by (simp add: lub_APP ssum_map_ID finite_deflation_ssum_map)
-lemma LIFTDEFL_prod:
- "LIFTDEFL('a::predomain \<times> 'b::predomain) = DEFL('a u \<otimes> 'b u)"
-by (rule liftdefl_prod_def)
-
-subsubsection {* Unit type *}
-
-instantiation unit :: liftdomain
-begin
-
-definition
- "emb = (\<bottom> :: unit \<rightarrow> udom)"
-
-definition
- "prj = (\<bottom> :: udom \<rightarrow> unit)"
-
-definition
- "defl (t::unit itself) = \<bottom>"
-
-definition
- "(liftemb :: unit u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+lemma approx_chain_cfun_map:
+ assumes "approx_chain a" and "approx_chain b"
+ shows "approx_chain (\<lambda>i. cfun_map\<cdot>(a i)\<cdot>(b i))"
+ using assms unfolding approx_chain_def
+ by (simp add: lub_APP cfun_map_ID finite_deflation_cfun_map)
-definition
- "(liftprj :: udom \<rightarrow> unit u) = u_map\<cdot>prj oo udom_prj u_approx"
-
-definition
- "liftdefl (t::unit itself) = u_defl\<cdot>DEFL(unit)"
+lemma approx_chain_cprod_map:
+ assumes "approx_chain a" and "approx_chain b"
+ shows "approx_chain (\<lambda>i. cprod_map\<cdot>(a i)\<cdot>(b i))"
+ using assms unfolding approx_chain_def
+ by (simp add: lub_APP cprod_map_ID finite_deflation_cprod_map)
-instance
-using liftemb_unit_def liftprj_unit_def liftdefl_unit_def
-proof (rule liftdomain_class_intro)
- show "ep_pair emb (prj :: udom \<rightarrow> unit)"
- unfolding emb_unit_def prj_unit_def
- by (simp add: ep_pair.intro)
-next
- show "cast\<cdot>DEFL(unit) = emb oo (prj :: udom \<rightarrow> unit)"
- unfolding emb_unit_def prj_unit_def defl_unit_def by simp
-qed
-
-end
-
-subsubsection {* Discrete cpo *}
+text {* Approx chains for countable discrete types. *}
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>)"
@@ -704,123 +152,124 @@
using chain_discr_approx lub_discr_approx finite_deflation_discr_approx
by (rule approx_chain.intro)
-instantiation discr :: (countable) predomain
-begin
+subsection {* Class instance proofs *}
+
+instance bifinite \<subseteq> profinite
+proof
+ show "\<exists>(a::nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>). approx_chain a"
+ using bifinite [where 'a='a]
+ by (fast intro!: approx_chain_u_map)
+qed
+
+instance u :: (profinite) bifinite
+ by default (rule profinite)
-definition
- "liftemb = udom_emb discr_approx"
+text {*
+ Types @{typ "'a \<rightarrow> 'b"} and @{typ "'a u \<rightarrow>! 'b"} are isomorphic.
+*}
+
+definition "encode_cfun = (\<Lambda> f. sfun_abs\<cdot>(fup\<cdot>f))"
+
+definition "decode_cfun = (\<Lambda> g x. sfun_rep\<cdot>g\<cdot>(up\<cdot>x))"
+
+lemma decode_encode_cfun [simp]: "decode_cfun\<cdot>(encode_cfun\<cdot>x) = x"
+unfolding encode_cfun_def decode_cfun_def
+by (simp add: eta_cfun)
-definition
- "liftprj = udom_prj discr_approx"
+lemma encode_decode_cfun [simp]: "encode_cfun\<cdot>(decode_cfun\<cdot>y) = y"
+unfolding encode_cfun_def decode_cfun_def
+apply (simp add: sfun_eq_iff strictify_cancel)
+apply (rule cfun_eqI, case_tac x, simp_all)
+done
-definition
- "liftdefl (t::'a discr itself) =
- (\<Squnion>i. defl_principal (Abs_fin_defl (liftemb oo discr_approx i oo liftprj)))"
+instance cfun :: (profinite, bifinite) bifinite
+proof
+ obtain a :: "nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>" where a: "approx_chain a"
+ using profinite ..
+ obtain b :: "nat \<Rightarrow> 'b \<rightarrow> 'b" where b: "approx_chain b"
+ using bifinite ..
+ have "approx_chain (\<lambda>i. decode_cfun oo sfun_map\<cdot>(a i)\<cdot>(b i) oo encode_cfun)"
+ using a b by (simp add: approx_chain_iso approx_chain_sfun_map)
+ thus "\<exists>(a::nat \<Rightarrow> ('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow> 'b)). approx_chain a"
+ by - (rule exI)
+qed
+
+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)
-instance proof
- 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
- 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_discr_approx)
- apply (subst cast_defl_principal)
- apply (simp add: Abs_fin_defl_inverse
- ep_pair.finite_deflation_e_d_p [OF ep_pair_udom [OF discr_approx]]
- approx_chain.finite_deflation_approx [OF discr_approx])
- apply (simp add: lub_distribs)
- done
+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
+
+instance prod :: (profinite, profinite) profinite
+proof
+ obtain a :: "nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>" where a: "approx_chain a"
+ using profinite ..
+ obtain b :: "nat \<Rightarrow> 'b\<^sub>\<bottom> \<rightarrow> 'b\<^sub>\<bottom>" where b: "approx_chain b"
+ using profinite ..
+ have "approx_chain (\<lambda>i. decode_prod_u oo sprod_map\<cdot>(a i)\<cdot>(b i) oo encode_prod_u)"
+ using a b by (simp add: approx_chain_iso approx_chain_sprod_map)
+ thus "\<exists>(a::nat \<Rightarrow> ('a \<times> 'b)\<^sub>\<bottom> \<rightarrow> ('a \<times> 'b)\<^sub>\<bottom>). approx_chain a"
+ by - (rule exI)
+qed
+
+instance prod :: (bifinite, bifinite) bifinite
+proof
+ show "\<exists>(a::nat \<Rightarrow> ('a \<times> 'b) \<rightarrow> ('a \<times> 'b)). approx_chain a"
+ using bifinite [where 'a='a] and bifinite [where 'a='b]
+ by (fast intro!: approx_chain_cprod_map)
+qed
+
+instance sfun :: (bifinite, bifinite) bifinite
+proof
+ show "\<exists>(a::nat \<Rightarrow> ('a \<rightarrow>! 'b) \<rightarrow> ('a \<rightarrow>! 'b)). approx_chain a"
+ using bifinite [where 'a='a] and bifinite [where 'a='b]
+ by (fast intro!: approx_chain_sfun_map)
+qed
+
+instance sprod :: (bifinite, bifinite) bifinite
+proof
+ show "\<exists>(a::nat \<Rightarrow> ('a \<otimes> 'b) \<rightarrow> ('a \<otimes> 'b)). approx_chain a"
+ using bifinite [where 'a='a] and bifinite [where 'a='b]
+ by (fast intro!: approx_chain_sprod_map)
+qed
+
+instance ssum :: (bifinite, bifinite) bifinite
+proof
+ show "\<exists>(a::nat \<Rightarrow> ('a \<oplus> 'b) \<rightarrow> ('a \<oplus> 'b)). approx_chain a"
+ using bifinite [where 'a='a] and bifinite [where 'a='b]
+ by (fast intro!: approx_chain_ssum_map)
+qed
+
+lemma approx_chain_unit: "approx_chain (\<bottom> :: nat \<Rightarrow> unit \<rightarrow> unit)"
+by (simp add: approx_chain_def cfun_eq_iff finite_deflation_UU)
+
+instance unit :: bifinite
+ by default (fast intro!: approx_chain_unit)
+
+instance discr :: (countable) profinite
+ by default (fast intro!: discr_approx)
+
+instance lift :: (countable) bifinite
+proof
+ note [simp] = cont_Abs_lift cont_Rep_lift Rep_lift_inverse Abs_lift_inverse
+ obtain a :: "nat \<Rightarrow> ('a discr)\<^sub>\<bottom> \<rightarrow> ('a discr)\<^sub>\<bottom>" where a: "approx_chain a"
+ using profinite ..
+ hence "approx_chain (\<lambda>i. (\<Lambda> y. Abs_lift y) oo a i oo (\<Lambda> x. Rep_lift x))"
+ by (rule approx_chain_iso) simp_all
+ thus "\<exists>(a::nat \<Rightarrow> 'a lift \<rightarrow> 'a lift). approx_chain a"
+ by - (rule exI)
qed
end
-
-subsubsection {* Strict sum *}
-
-instantiation ssum :: ("domain", "domain") liftdomain
-begin
-
-definition
- "emb = udom_emb ssum_approx oo ssum_map\<cdot>emb\<cdot>emb"
-
-definition
- "prj = ssum_map\<cdot>prj\<cdot>prj oo udom_prj ssum_approx"
-
-definition
- "defl (t::('a \<oplus> 'b) itself) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
-
-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)
- show "cast\<cdot>DEFL('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
- unfolding emb_ssum_def prj_ssum_def defl_ssum_def cast_ssum_defl
- by (simp add: cast_DEFL oo_def cfun_eq_iff ssum_map_map)
-qed
-
-end
-
-lemma DEFL_ssum:
- "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/HOL/HOLCF/CompactBasis.thy Sun Dec 19 19:03:49 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-(* Title: HOLCF/CompactBasis.thy
- Author: Brian Huffman
-*)
-
-header {* A compact basis for powerdomains *}
-
-theory CompactBasis
-imports Bifinite
-begin
-
-default_sort "domain"
-
-subsection {* A compact basis for powerdomains *}
-
-typedef 'a pd_basis =
- "{S::'a compact_basis set. finite S \<and> S \<noteq> {}}"
-by (rule_tac x="{arbitrary}" in exI, simp)
-
-lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)"
-by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
-
-lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}"
-by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
-
-text {* The powerdomain basis type is countable. *}
-
-lemma pd_basis_countable: "\<exists>f::'a pd_basis \<Rightarrow> nat. inj f"
-proof -
- obtain g :: "'a compact_basis \<Rightarrow> nat" where "inj g"
- using compact_basis.countable ..
- hence image_g_eq: "\<And>A B. g ` A = g ` B \<longleftrightarrow> A = B"
- by (rule inj_image_eq_iff)
- have "inj (\<lambda>t. set_encode (g ` Rep_pd_basis t))"
- by (simp add: inj_on_def set_encode_eq image_g_eq Rep_pd_basis_inject)
- thus ?thesis by - (rule exI)
- (* FIXME: why doesn't ".." or "by (rule exI)" work? *)
-qed
-
-subsection {* Unit and plus constructors *}
-
-definition
- PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where
- "PDUnit = (\<lambda>x. Abs_pd_basis {x})"
-
-definition
- PDPlus :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
- "PDPlus t u = Abs_pd_basis (Rep_pd_basis t \<union> Rep_pd_basis u)"
-
-lemma Rep_PDUnit:
- "Rep_pd_basis (PDUnit x) = {x}"
-unfolding PDUnit_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
-
-lemma Rep_PDPlus:
- "Rep_pd_basis (PDPlus u v) = Rep_pd_basis u \<union> Rep_pd_basis v"
-unfolding PDPlus_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
-
-lemma PDUnit_inject [simp]: "(PDUnit a = PDUnit b) = (a = b)"
-unfolding Rep_pd_basis_inject [symmetric] Rep_PDUnit by simp
-
-lemma PDPlus_assoc: "PDPlus (PDPlus t u) v = PDPlus t (PDPlus u v)"
-unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_assoc)
-
-lemma PDPlus_commute: "PDPlus t u = PDPlus u t"
-unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_commute)
-
-lemma PDPlus_absorb: "PDPlus t t = t"
-unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_absorb)
-
-lemma pd_basis_induct1:
- assumes PDUnit: "\<And>a. P (PDUnit a)"
- assumes PDPlus: "\<And>a t. P t \<Longrightarrow> P (PDPlus (PDUnit a) t)"
- shows "P x"
-apply (induct x, unfold pd_basis_def, clarify)
-apply (erule (1) finite_ne_induct)
-apply (cut_tac a=x in PDUnit)
-apply (simp add: PDUnit_def)
-apply (drule_tac a=x in PDPlus)
-apply (simp add: PDUnit_def PDPlus_def
- Abs_pd_basis_inverse [unfolded pd_basis_def])
-done
-
-lemma pd_basis_induct:
- assumes PDUnit: "\<And>a. P (PDUnit a)"
- assumes PDPlus: "\<And>t u. \<lbrakk>P t; P u\<rbrakk> \<Longrightarrow> P (PDPlus t u)"
- shows "P x"
-apply (induct x rule: pd_basis_induct1)
-apply (rule PDUnit, erule PDPlus [OF PDUnit])
-done
-
-subsection {* Fold operator *}
-
-definition
- fold_pd ::
- "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b"
- where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
-
-lemma fold_pd_PDUnit:
- assumes "class.ab_semigroup_idem_mult f"
- shows "fold_pd g f (PDUnit x) = g x"
-unfolding fold_pd_def Rep_PDUnit by simp
-
-lemma fold_pd_PDPlus:
- assumes "class.ab_semigroup_idem_mult f"
- shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
-proof -
- interpret ab_semigroup_idem_mult f by fact
- show ?thesis unfolding fold_pd_def Rep_PDPlus
- by (simp add: image_Un fold1_Un2)
-qed
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/Compact_Basis.thy Sun Dec 19 17:39:20 2010 -0800
@@ -0,0 +1,111 @@
+(* Title: HOLCF/Compact_Basis.thy
+ Author: Brian Huffman
+*)
+
+header {* A compact basis for powerdomains *}
+
+theory Compact_Basis
+imports Universal
+begin
+
+default_sort bifinite
+
+subsection {* A compact basis for powerdomains *}
+
+typedef 'a pd_basis =
+ "{S::'a compact_basis set. finite S \<and> S \<noteq> {}}"
+by (rule_tac x="{arbitrary}" in exI, simp)
+
+lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)"
+by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
+
+lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}"
+by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
+
+text {* The powerdomain basis type is countable. *}
+
+lemma pd_basis_countable: "\<exists>f::'a pd_basis \<Rightarrow> nat. inj f"
+proof -
+ obtain g :: "'a compact_basis \<Rightarrow> nat" where "inj g"
+ using compact_basis.countable ..
+ hence image_g_eq: "\<And>A B. g ` A = g ` B \<longleftrightarrow> A = B"
+ by (rule inj_image_eq_iff)
+ have "inj (\<lambda>t. set_encode (g ` Rep_pd_basis t))"
+ by (simp add: inj_on_def set_encode_eq image_g_eq Rep_pd_basis_inject)
+ thus ?thesis by - (rule exI)
+ (* FIXME: why doesn't ".." or "by (rule exI)" work? *)
+qed
+
+subsection {* Unit and plus constructors *}
+
+definition
+ PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where
+ "PDUnit = (\<lambda>x. Abs_pd_basis {x})"
+
+definition
+ PDPlus :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
+ "PDPlus t u = Abs_pd_basis (Rep_pd_basis t \<union> Rep_pd_basis u)"
+
+lemma Rep_PDUnit:
+ "Rep_pd_basis (PDUnit x) = {x}"
+unfolding PDUnit_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
+
+lemma Rep_PDPlus:
+ "Rep_pd_basis (PDPlus u v) = Rep_pd_basis u \<union> Rep_pd_basis v"
+unfolding PDPlus_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
+
+lemma PDUnit_inject [simp]: "(PDUnit a = PDUnit b) = (a = b)"
+unfolding Rep_pd_basis_inject [symmetric] Rep_PDUnit by simp
+
+lemma PDPlus_assoc: "PDPlus (PDPlus t u) v = PDPlus t (PDPlus u v)"
+unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_assoc)
+
+lemma PDPlus_commute: "PDPlus t u = PDPlus u t"
+unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_commute)
+
+lemma PDPlus_absorb: "PDPlus t t = t"
+unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_absorb)
+
+lemma pd_basis_induct1:
+ assumes PDUnit: "\<And>a. P (PDUnit a)"
+ assumes PDPlus: "\<And>a t. P t \<Longrightarrow> P (PDPlus (PDUnit a) t)"
+ shows "P x"
+apply (induct x, unfold pd_basis_def, clarify)
+apply (erule (1) finite_ne_induct)
+apply (cut_tac a=x in PDUnit)
+apply (simp add: PDUnit_def)
+apply (drule_tac a=x in PDPlus)
+apply (simp add: PDUnit_def PDPlus_def
+ Abs_pd_basis_inverse [unfolded pd_basis_def])
+done
+
+lemma pd_basis_induct:
+ assumes PDUnit: "\<And>a. P (PDUnit a)"
+ assumes PDPlus: "\<And>t u. \<lbrakk>P t; P u\<rbrakk> \<Longrightarrow> P (PDPlus t u)"
+ shows "P x"
+apply (induct x rule: pd_basis_induct1)
+apply (rule PDUnit, erule PDPlus [OF PDUnit])
+done
+
+subsection {* Fold operator *}
+
+definition
+ fold_pd ::
+ "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b"
+ where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
+
+lemma fold_pd_PDUnit:
+ assumes "class.ab_semigroup_idem_mult f"
+ shows "fold_pd g f (PDUnit x) = g x"
+unfolding fold_pd_def Rep_PDUnit by simp
+
+lemma fold_pd_PDPlus:
+ assumes "class.ab_semigroup_idem_mult f"
+ shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
+proof -
+ interpret ab_semigroup_idem_mult f by fact
+ show ?thesis unfolding fold_pd_def Rep_PDPlus
+ by (simp add: image_Un fold1_Un2)
+qed
+
+end
--- a/src/HOL/HOLCF/ConvexPD.thy Sun Dec 19 19:03:49 2010 +0100
+++ b/src/HOL/HOLCF/ConvexPD.thy Sun Dec 19 17:39:20 2010 -0800
@@ -125,7 +125,7 @@
type_notation (xsymbols) convex_pd ("('(_')\<natural>)")
-instantiation convex_pd :: ("domain") below
+instantiation convex_pd :: (bifinite) below
begin
definition
@@ -134,11 +134,11 @@
instance ..
end
-instance convex_pd :: ("domain") po
+instance convex_pd :: (bifinite) po
using type_definition_convex_pd below_convex_pd_def
by (rule convex_le.typedef_ideal_po)
-instance convex_pd :: ("domain") cpo
+instance convex_pd :: (bifinite) cpo
using type_definition_convex_pd below_convex_pd_def
by (rule convex_le.typedef_ideal_cpo)
@@ -157,7 +157,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 :: ("domain") pcpo
+instance convex_pd :: (bifinite) pcpo
by intro_classes (fast intro: convex_pd_minimal)
lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)"
@@ -466,68 +466,21 @@
by (rule finite_range_imp_finite_fixes)
qed
-subsection {* Convex powerdomain is a domain *}
-
-definition
- convex_approx :: "nat \<Rightarrow> udom convex_pd \<rightarrow> udom convex_pd"
-where
- "convex_approx = (\<lambda>i. convex_map\<cdot>(udom_approx i))"
-
-lemma convex_approx: "approx_chain convex_approx"
-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"
-
-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"
-using convex_approx finite_deflation_convex_map
-unfolding convex_defl_def by (rule cast_defl_fun1)
-
-instantiation convex_pd :: ("domain") liftdomain
-begin
-
-definition
- "emb = udom_emb convex_approx oo convex_map\<cdot>emb"
-
-definition
- "prj = convex_map\<cdot>prj oo udom_prj convex_approx"
+subsection {* Convex powerdomain is bifinite *}
-definition
- "defl (t::'a convex_pd itself) = convex_defl\<cdot>DEFL('a)"
-
-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)"
+lemma approx_chain_convex_map:
+ assumes "approx_chain a"
+ shows "approx_chain (\<lambda>i. convex_map\<cdot>(a i))"
+ using assms unfolding approx_chain_def
+ by (simp add: lub_APP convex_map_ID finite_deflation_convex_map)
-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]
- by (intro ep_pair_comp ep_pair_convex_map ep_pair_emb_prj)
-next
- show "cast\<cdot>DEFL('a convex_pd) = emb oo (prj :: udom \<rightarrow> 'a convex_pd)"
- unfolding emb_convex_pd_def prj_convex_pd_def defl_convex_pd_def cast_convex_defl
- by (simp add: cast_DEFL oo_def cfun_eq_iff convex_map_map)
+instance convex_pd :: (bifinite) bifinite
+proof
+ show "\<exists>(a::nat \<Rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd). approx_chain a"
+ using bifinite [where 'a='a]
+ by (fast intro!: approx_chain_convex_map)
qed
-end
-
-text {* DEFL of type constructor = type combinator *}
-
-lemma DEFL_convex: "DEFL('a convex_pd) = convex_defl\<cdot>DEFL('a)"
-by (rule defl_convex_pd_def)
-
-
subsection {* Join *}
definition
--- a/src/HOL/HOLCF/Domain.thy Sun Dec 19 19:03:49 2010 +0100
+++ b/src/HOL/HOLCF/Domain.thy Sun Dec 19 17:39:20 2010 -0800
@@ -5,7 +5,7 @@
header {* Domain package *}
theory Domain
-imports Bifinite Domain_Aux
+imports Representable Domain_Aux
uses
("Tools/domaindef.ML")
("Tools/Domain/domain_isomorphism.ML")
@@ -63,7 +63,7 @@
subsection {* Deflations as sets *}
-definition defl_set :: "defl \<Rightarrow> udom set"
+definition defl_set :: "'a::bifinite defl \<Rightarrow> 'a set"
where "defl_set A = {x. cast\<cdot>A\<cdot>x = x}"
lemma adm_defl_set: "adm (\<lambda>x. x \<in> defl_set A)"
@@ -86,30 +86,28 @@
setup {*
fold Sign.add_const_constraint
- [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"})
+ [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> udom defl"})
, (@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"})
, (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::pcpo"})
- , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"})
- , (@{const_name liftemb}, SOME @{typ "'a::pcpo u \<rightarrow> udom"})
- , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::pcpo u"}) ]
+ , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \<Rightarrow> udom u defl"})
+ , (@{const_name liftemb}, SOME @{typ "'a::pcpo u \<rightarrow> udom u"})
+ , (@{const_name liftprj}, SOME @{typ "udom u \<rightarrow> 'a::pcpo u"}) ]
*}
-lemma typedef_liftdomain_class:
+lemma typedef_domain_class:
fixes Rep :: "'a::pcpo \<Rightarrow> udom"
fixes Abs :: "udom \<Rightarrow> 'a::pcpo"
- fixes t :: defl
+ fixes t :: "udom 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)
+ assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom u) \<equiv> u_map\<cdot>emb"
+ assumes liftprj: "(liftprj :: udom u \<rightarrow> 'a u) \<equiv> u_map\<cdot>prj"
+ assumes liftdefl: "(liftdefl :: 'a itself \<Rightarrow> _) \<equiv> (\<lambda>t. pdefl\<cdot>DEFL('a))"
+ shows "OFCLASS('a, domain_class)"
+proof
have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
unfolding emb
apply (rule beta_cfun)
@@ -135,9 +133,7 @@
done
show "cast\<cdot>DEFL('a) = emb oo (prj :: udom \<rightarrow> 'a)"
by (rule cfun_eqI, simp add: defl emb_prj)
- show "LIFTDEFL('a) = u_defl\<cdot>DEFL('a)"
- unfolding liftdefl ..
-qed
+qed (simp_all only: liftemb liftprj liftdefl)
lemma typedef_DEFL:
assumes "defl \<equiv> (\<lambda>a::'a::pcpo itself. t)"
@@ -148,22 +144,23 @@
setup {*
fold Sign.add_const_constraint
- [ (@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> defl"})
+ [ (@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> udom defl"})
, (@{const_name emb}, SOME @{typ "'a::domain \<rightarrow> udom"})
, (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::domain"})
- , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> defl"})
- , (@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom"})
- , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::predomain u"}) ]
+ , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> udom u defl"})
+ , (@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom u"})
+ , (@{const_name liftprj}, SOME @{typ "udom u \<rightarrow> 'a::predomain u"}) ]
*}
use "Tools/domaindef.ML"
subsection {* Isomorphic deflations *}
-definition
- isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> defl \<Rightarrow> bool"
-where
- "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
+definition isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> udom defl \<Rightarrow> bool"
+ where "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
+
+definition isodefl' :: "('a::predomain \<rightarrow> 'a) \<Rightarrow> udom u defl \<Rightarrow> bool"
+ where "isodefl' d t \<longleftrightarrow> cast\<cdot>t = liftemb oo u_map\<cdot>d oo liftprj"
lemma isodeflI: "(\<And>x. cast\<cdot>t\<cdot>x = emb\<cdot>(d\<cdot>(prj\<cdot>x))) \<Longrightarrow> isodefl d t"
unfolding isodefl_def by (simp add: cfun_eqI)
@@ -191,9 +188,8 @@
unfolding isodefl_def by (simp add: cast_DEFL)
lemma isodefl_LIFTDEFL:
- "isodefl (u_map\<cdot>(ID :: 'a \<rightarrow> 'a)) LIFTDEFL('a::predomain)"
-unfolding u_map_ID DEFL_u [symmetric]
-by (rule isodefl_ID_DEFL)
+ "isodefl' (ID :: 'a \<rightarrow> 'a) LIFTDEFL('a::predomain)"
+unfolding isodefl'_def by (simp add: cast_liftdefl u_map_ID)
lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) DEFL('a) \<Longrightarrow> d = ID"
unfolding isodefl_def
@@ -237,6 +233,10 @@
unfolding isodefl_def
by (simp add: cfun_eq_iff assms prj_emb_prj emb_prj_emb)
+lemma isodefl'_pdefl: "isodefl d t \<Longrightarrow> isodefl' d (pdefl\<cdot>t)"
+unfolding isodefl_def isodefl'_def
+by (simp add: cast_pdefl u_map_oo liftemb_eq liftprj_eq)
+
lemma isodefl_sfun:
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)"
@@ -274,12 +274,10 @@
done
lemma isodefl_u:
- fixes d :: "'a::liftdomain \<rightarrow> 'a"
- shows "isodefl (d :: 'a \<rightarrow> 'a) t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
+ "isodefl' d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
apply (rule isodeflI)
-apply (simp add: cast_u_defl cast_isodefl)
+apply (simp add: cast_u_defl isodefl'_def)
apply (simp add: emb_u_def prj_u_def liftemb_eq liftprj_eq)
-apply (simp add: u_map_map)
done
lemma encode_prod_u_map:
@@ -291,11 +289,11 @@
done
lemma isodefl_cprod_u:
- assumes "isodefl (u_map\<cdot>d1) t1" and "isodefl (u_map\<cdot>d2) t2"
- shows "isodefl (u_map\<cdot>(cprod_map\<cdot>d1\<cdot>d2)) (sprod_defl\<cdot>t1\<cdot>t2)"
-using isodefl_sprod [OF assms] unfolding isodefl_def
-unfolding emb_u_def prj_u_def liftemb_prod_def liftprj_prod_def
-by (simp add: cfcomp1 encode_prod_u_map)
+ assumes "isodefl' d1 t1" and "isodefl' d2 t2"
+ shows "isodefl' (cprod_map\<cdot>d1\<cdot>d2) (prod_liftdefl\<cdot>t1\<cdot>t2)"
+using assms unfolding isodefl'_def
+unfolding liftemb_prod_def liftprj_prod_def
+by (simp add: cast_prod_liftdefl cfcomp1 encode_prod_u_map sprod_map_map)
lemma encode_cfun_map:
"encode_cfun\<cdot>(cfun_map\<cdot>f\<cdot>g\<cdot>(decode_cfun\<cdot>x))
@@ -328,7 +326,7 @@
lemmas [domain_isodefl] =
isodefl_u isodefl_sfun isodefl_ssum isodefl_sprod
- isodefl_cfun isodefl_cprod isodefl_cprod_u
+ isodefl_cfun isodefl_cprod isodefl_cprod_u isodefl'_pdefl
lemmas [domain_deflation] =
deflation_cfun_map deflation_sfun_map deflation_ssum_map
--- a/src/HOL/HOLCF/IsaMakefile Sun Dec 19 19:03:49 2010 +0100
+++ b/src/HOL/HOLCF/IsaMakefile Sun Dec 19 17:39:20 2010 -0800
@@ -39,7 +39,7 @@
Algebraic.thy \
Bifinite.thy \
Cfun.thy \
- CompactBasis.thy \
+ Compact_Basis.thy \
Completion.thy \
Cont.thy \
ConvexPD.thy \
@@ -62,6 +62,7 @@
Porder.thy \
Powerdomains.thy \
Product_Cpo.thy \
+ Representable.thy \
Sfun.thy \
Sprod.thy \
Ssum.thy \
--- a/src/HOL/HOLCF/Library/Bool_Discrete.thy Sun Dec 19 19:03:49 2010 +0100
+++ b/src/HOL/HOLCF/Library/Bool_Discrete.thy Sun Dec 19 17:39:20 2010 -0800
@@ -29,23 +29,23 @@
begin
definition
- "(liftemb :: bool u \<rightarrow> udom) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
+ "(liftemb :: bool u \<rightarrow> udom u) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
definition
- "(liftprj :: udom \<rightarrow> bool u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
+ "(liftprj :: udom u \<rightarrow> bool u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
definition
"liftdefl \<equiv> (\<lambda>(t::bool itself). LIFTDEFL(bool discr))"
instance proof
- show "ep_pair liftemb (liftprj :: udom \<rightarrow> bool u)"
+ show "ep_pair liftemb (liftprj :: udom u \<rightarrow> bool u)"
unfolding liftemb_bool_def liftprj_bool_def
apply (rule ep_pair_comp)
apply (rule ep_pair_u_map)
apply (simp add: ep_pair.intro)
apply (rule predomain_ep)
done
- show "cast\<cdot>LIFTDEFL(bool) = liftemb oo (liftprj :: udom \<rightarrow> bool u)"
+ show "cast\<cdot>LIFTDEFL(bool) = liftemb oo (liftprj :: udom u \<rightarrow> bool u)"
unfolding liftemb_bool_def liftprj_bool_def liftdefl_bool_def
apply (simp add: cast_liftdefl cfcomp1 u_map_map)
apply (simp add: ID_def [symmetric] u_map_ID)
--- a/src/HOL/HOLCF/Library/Char_Discrete.thy Sun Dec 19 19:03:49 2010 +0100
+++ b/src/HOL/HOLCF/Library/Char_Discrete.thy Sun Dec 19 17:39:20 2010 -0800
@@ -29,23 +29,23 @@
begin
definition
- "(liftemb :: nibble u \<rightarrow> udom) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
+ "(liftemb :: nibble u \<rightarrow> udom u) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
definition
- "(liftprj :: udom \<rightarrow> nibble u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
+ "(liftprj :: udom u \<rightarrow> nibble u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
definition
"liftdefl \<equiv> (\<lambda>(t::nibble itself). LIFTDEFL(nibble discr))"
instance proof
- show "ep_pair liftemb (liftprj :: udom \<rightarrow> nibble u)"
+ show "ep_pair liftemb (liftprj :: udom u \<rightarrow> nibble u)"
unfolding liftemb_nibble_def liftprj_nibble_def
apply (rule ep_pair_comp)
apply (rule ep_pair_u_map)
apply (simp add: ep_pair.intro)
apply (rule predomain_ep)
done
- show "cast\<cdot>LIFTDEFL(nibble) = liftemb oo (liftprj :: udom \<rightarrow> nibble u)"
+ show "cast\<cdot>LIFTDEFL(nibble) = liftemb oo (liftprj :: udom u \<rightarrow> nibble u)"
unfolding liftemb_nibble_def liftprj_nibble_def liftdefl_nibble_def
apply (simp add: cast_liftdefl cfcomp1 u_map_map)
apply (simp add: ID_def [symmetric] u_map_ID)
@@ -75,23 +75,23 @@
begin
definition
- "(liftemb :: char u \<rightarrow> udom) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
+ "(liftemb :: char u \<rightarrow> udom u) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
definition
- "(liftprj :: udom \<rightarrow> char u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
+ "(liftprj :: udom u \<rightarrow> char u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
definition
"liftdefl \<equiv> (\<lambda>(t::char itself). LIFTDEFL(char discr))"
instance proof
- show "ep_pair liftemb (liftprj :: udom \<rightarrow> char u)"
+ show "ep_pair liftemb (liftprj :: udom u \<rightarrow> char u)"
unfolding liftemb_char_def liftprj_char_def
apply (rule ep_pair_comp)
apply (rule ep_pair_u_map)
apply (simp add: ep_pair.intro)
apply (rule predomain_ep)
done
- show "cast\<cdot>LIFTDEFL(char) = liftemb oo (liftprj :: udom \<rightarrow> char u)"
+ show "cast\<cdot>LIFTDEFL(char) = liftemb oo (liftprj :: udom u \<rightarrow> char u)"
unfolding liftemb_char_def liftprj_char_def liftdefl_char_def
apply (simp add: cast_liftdefl cfcomp1 u_map_map)
apply (simp add: ID_def [symmetric] u_map_ID)
--- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy Sun Dec 19 19:03:49 2010 +0100
+++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy Sun Dec 19 17:39:20 2010 -0800
@@ -438,17 +438,20 @@
subsection {* Take function for finite deflations *}
+context bifinite_approx_chain
+begin
+
definition
- defl_take :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<Rightarrow> (udom \<rightarrow> udom)"
+ defl_take :: "nat \<Rightarrow> ('a \<rightarrow> 'a) \<Rightarrow> ('a \<rightarrow> 'a)"
where
- "defl_take i d = eventual_iterate (udom_approx i oo d)"
+ "defl_take i d = eventual_iterate (approx i oo d)"
lemma finite_deflation_defl_take:
"deflation d \<Longrightarrow> finite_deflation (defl_take i d)"
unfolding defl_take_def
apply (rule pre_deflation.finite_deflation_d)
apply (rule pre_deflation_oo)
-apply (rule finite_deflation_udom_approx)
+apply (rule finite_deflation_approx)
apply (erule deflation.below)
done
@@ -459,10 +462,10 @@
done
lemma defl_take_fixed_iff:
- "deflation d \<Longrightarrow> defl_take i d\<cdot>x = x \<longleftrightarrow> udom_approx i\<cdot>x = x \<and> d\<cdot>x = x"
+ "deflation d \<Longrightarrow> defl_take i d\<cdot>x = x \<longleftrightarrow> approx i\<cdot>x = x \<and> d\<cdot>x = x"
unfolding defl_take_def
apply (rule eventual_iterate_oo_fixed_iff)
-apply (rule finite_deflation_udom_approx)
+apply (rule finite_deflation_approx)
apply (erule deflation.below)
done
@@ -479,11 +482,11 @@
assumes cont: "cont f" and below: "\<And>x y. f x\<cdot>y \<sqsubseteq> y"
shows "cont (\<lambda>x. defl_take i (f x))"
unfolding defl_take_def
-using finite_deflation_udom_approx assms
+using finite_deflation_approx assms
by (rule cont2cont_eventual_iterate_oo)
definition
- fd_take :: "nat \<Rightarrow> fin_defl \<Rightarrow> fin_defl"
+ fd_take :: "nat \<Rightarrow> 'a fin_defl \<Rightarrow> 'a fin_defl"
where
"fd_take i d = Abs_fin_defl (defl_take i (Rep_fin_defl d))"
@@ -497,7 +500,7 @@
lemma fd_take_fixed_iff:
"Rep_fin_defl (fd_take i d)\<cdot>x = x \<longleftrightarrow>
- udom_approx i\<cdot>x = x \<and> Rep_fin_defl d\<cdot>x = x"
+ approx i\<cdot>x = x \<and> Rep_fin_defl d\<cdot>x = x"
unfolding Rep_fin_defl_fd_take
apply (rule defl_take_fixed_iff)
apply (rule deflation_Rep_fin_defl)
@@ -519,11 +522,11 @@
apply (simp add: fin_defl_belowD)
done
-lemma approx_fixed_le_lemma: "\<lbrakk>i \<le> j; udom_approx i\<cdot>x = x\<rbrakk> \<Longrightarrow> udom_approx j\<cdot>x = x"
+lemma approx_fixed_le_lemma: "\<lbrakk>i \<le> j; approx i\<cdot>x = x\<rbrakk> \<Longrightarrow> approx j\<cdot>x = x"
apply (rule deflation.belowD)
apply (rule finite_deflation_imp_deflation)
-apply (rule finite_deflation_udom_approx)
-apply (erule chain_mono [OF chain_udom_approx])
+apply (rule finite_deflation_approx)
+apply (erule chain_mono [OF chain_approx])
apply assumption
done
@@ -535,16 +538,16 @@
lemma finite_range_fd_take: "finite (range (fd_take n))"
apply (rule finite_imageD [where f="\<lambda>a. {x. Rep_fin_defl a\<cdot>x = x}"])
-apply (rule finite_subset [where B="Pow {x. udom_approx n\<cdot>x = x}"])
+apply (rule finite_subset [where B="Pow {x. approx n\<cdot>x = x}"])
apply (clarify, simp add: fd_take_fixed_iff)
-apply (simp add: finite_deflation.finite_fixes [OF finite_deflation_udom_approx])
+apply (simp add: finite_deflation.finite_fixes [OF finite_deflation_approx])
apply (rule inj_onI, clarify)
apply (simp add: set_eq_iff fin_defl_eqI)
done
lemma fd_take_covers: "\<exists>n. fd_take n a = a"
apply (rule_tac x=
- "Max ((\<lambda>x. LEAST n. udom_approx n\<cdot>x = x) ` {x. Rep_fin_defl a\<cdot>x = x})" in exI)
+ "Max ((\<lambda>x. LEAST n. approx n\<cdot>x = x) ` {x. Rep_fin_defl a\<cdot>x = x})" in exI)
apply (rule below_antisym)
apply (rule fd_take_below)
apply (rule fin_defl_belowI)
@@ -556,7 +559,7 @@
apply (rule imageI)
apply (erule CollectI)
apply (rule LeastI_ex)
-apply (rule approx_chain.compact_eq_approx [OF udom_approx])
+apply (rule compact_eq_approx)
apply (erule subst)
apply (rule Rep_fin_defl.compact)
done
@@ -564,7 +567,7 @@
subsection {* Chain of approx functions on algebraic deflations *}
definition
- defl_approx :: "nat \<Rightarrow> defl \<rightarrow> defl"
+ defl_approx :: "nat \<Rightarrow> 'a defl \<rightarrow> 'a defl"
where
"defl_approx = (\<lambda>i. defl.basis_fun (\<lambda>d. defl_principal (fd_take i d)))"
@@ -607,9 +610,34 @@
done
qed
+end
+
subsection {* Algebraic deflations are a bifinite domain *}
-instantiation defl :: liftdomain
+instance defl :: (bifinite) bifinite
+proof
+ obtain a :: "nat \<Rightarrow> 'a \<rightarrow> 'a" where "approx_chain a"
+ using bifinite ..
+ hence "bifinite_approx_chain a"
+ unfolding bifinite_approx_chain_def .
+ thus "\<exists>(a::nat \<Rightarrow> 'a defl \<rightarrow> 'a defl). approx_chain a"
+ by (fast intro: bifinite_approx_chain.defl_approx)
+qed
+
+subsection {* Algebraic deflations are representable *}
+
+definition defl_approx :: "nat \<Rightarrow> 'a::bifinite defl \<rightarrow> 'a defl"
+ where "defl_approx = bifinite_approx_chain.defl_approx
+ (SOME a. approx_chain a)"
+
+lemma defl_approx: "approx_chain defl_approx"
+unfolding defl_approx_def
+apply (rule bifinite_approx_chain.defl_approx)
+apply (unfold bifinite_approx_chain_def)
+apply (rule someI_ex [OF bifinite])
+done
+
+instantiation defl :: (bifinite) "domain"
begin
definition
@@ -619,25 +647,23 @@
"prj = udom_prj defl_approx"
definition
- "defl (t::defl itself) =
+ "defl (t::'a defl itself) =
(\<Squnion>i. defl_principal (Abs_fin_defl (emb oo defl_approx i oo prj)))"
definition
- "(liftemb :: defl u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+ "(liftemb :: 'a defl u \<rightarrow> udom u) = u_map\<cdot>emb"
definition
- "(liftprj :: udom \<rightarrow> defl u) = u_map\<cdot>prj oo udom_prj u_approx"
+ "(liftprj :: udom u \<rightarrow> 'a defl u) = u_map\<cdot>prj"
definition
- "liftdefl (t::defl itself) = u_defl\<cdot>DEFL(defl)"
+ "liftdefl (t::'a defl itself) = pdefl\<cdot>DEFL('a 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)"
+instance proof
+ show ep: "ep_pair emb (prj :: udom \<rightarrow> 'a defl)"
unfolding emb_defl_def prj_defl_def
by (rule ep_pair_udom [OF defl_approx])
- show "cast\<cdot>DEFL(defl) = emb oo (prj :: udom \<rightarrow> defl)"
+ show "cast\<cdot>DEFL('a defl) = emb oo (prj :: udom \<rightarrow> 'a defl)"
unfolding defl_defl_def
apply (subst contlub_cfun_arg)
apply (rule chainI)
@@ -654,7 +680,7 @@
apply (simp add: lub_distribs approx_chain.chain_approx [OF defl_approx]
approx_chain.lub_approx [OF defl_approx])
done
-qed
+qed (fact liftemb_defl_def liftprj_defl_def liftdefl_defl_def)+
end
--- a/src/HOL/HOLCF/Library/Int_Discrete.thy Sun Dec 19 19:03:49 2010 +0100
+++ b/src/HOL/HOLCF/Library/Int_Discrete.thy Sun Dec 19 17:39:20 2010 -0800
@@ -29,23 +29,23 @@
begin
definition
- "(liftemb :: int u \<rightarrow> udom) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
+ "(liftemb :: int u \<rightarrow> udom u) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
definition
- "(liftprj :: udom \<rightarrow> int u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
+ "(liftprj :: udom u \<rightarrow> int u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
definition
"liftdefl \<equiv> (\<lambda>(t::int itself). LIFTDEFL(int discr))"
instance proof
- show "ep_pair liftemb (liftprj :: udom \<rightarrow> int u)"
+ show "ep_pair liftemb (liftprj :: udom u \<rightarrow> int u)"
unfolding liftemb_int_def liftprj_int_def
apply (rule ep_pair_comp)
apply (rule ep_pair_u_map)
apply (simp add: ep_pair.intro)
apply (rule predomain_ep)
done
- show "cast\<cdot>LIFTDEFL(int) = liftemb oo (liftprj :: udom \<rightarrow> int u)"
+ show "cast\<cdot>LIFTDEFL(int) = liftemb oo (liftprj :: udom u \<rightarrow> int u)"
unfolding liftemb_int_def liftprj_int_def liftdefl_int_def
apply (simp add: cast_liftdefl cfcomp1 u_map_map)
apply (simp add: ID_def [symmetric] u_map_ID)
--- a/src/HOL/HOLCF/Library/List_Predomain.thy Sun Dec 19 19:03:49 2010 +0100
+++ b/src/HOL/HOLCF/Library/List_Predomain.thy Sun Dec 19 17:39:20 2010 -0800
@@ -5,13 +5,61 @@
header {* Predomain class instance for HOL list type *}
theory List_Predomain
-imports List_Cpo
+imports List_Cpo Sum_Cpo
begin
subsection {* Strict list type *}
domain 'a slist = SNil | SCons "'a" "'a slist"
+text {* Polymorphic map function for strict lists. *}
+
+text {* FIXME: The domain package should generate this! *}
+
+fixrec slist_map' :: "('a \<rightarrow> 'b) \<rightarrow> 'a slist \<rightarrow> 'b slist"
+ where "slist_map'\<cdot>f\<cdot>SNil = SNil"
+ | "\<lbrakk>x \<noteq> \<bottom>; xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow>
+ slist_map'\<cdot>f\<cdot>(SCons\<cdot>x\<cdot>xs) = SCons\<cdot>(f\<cdot>x)\<cdot>(slist_map'\<cdot>f\<cdot>xs)"
+
+lemma slist_map'_strict [simp]: "slist_map'\<cdot>f\<cdot>\<bottom> = \<bottom>"
+by fixrec_simp
+
+lemma slist_map_conv [simp]: "slist_map = slist_map'"
+apply (rule cfun_eqI, rule cfun_eqI, rename_tac f xs)
+apply (induct_tac xs, simp_all)
+apply (subst slist_map_unfold, simp)
+apply (subst slist_map_unfold, simp add: SNil_def)
+apply (subst slist_map_unfold, simp add: SCons_def)
+done
+
+lemma slist_map'_slist_map':
+ "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> slist_map'\<cdot>f\<cdot>(slist_map'\<cdot>g\<cdot>xs) = slist_map'\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
+apply (induct xs, simp, simp)
+apply (case_tac "g\<cdot>a = \<bottom>", simp, simp)
+apply (case_tac "slist_map'\<cdot>g\<cdot>xs = \<bottom>", simp, simp)
+done
+
+lemma slist_map'_oo:
+ "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> slist_map'\<cdot>(f oo g) = slist_map'\<cdot>f oo slist_map'\<cdot>g"
+by (simp add: cfcomp1 slist_map'_slist_map' eta_cfun)
+
+lemma slist_map'_ID: "slist_map'\<cdot>ID = ID"
+by (rule cfun_eqI, induct_tac x, simp_all)
+
+lemma ep_pair_slist_map':
+ "ep_pair e p \<Longrightarrow> ep_pair (slist_map'\<cdot>e) (slist_map'\<cdot>p)"
+apply (rule ep_pair.intro)
+apply (subst slist_map'_slist_map')
+apply (erule pcpo_ep_pair.p_strict [unfolded pcpo_ep_pair_def])
+apply (simp add: ep_pair.e_inverse ID_def [symmetric] slist_map'_ID)
+apply (subst slist_map'_slist_map')
+apply (erule pcpo_ep_pair.e_strict [unfolded pcpo_ep_pair_def])
+apply (rule below_eq_trans [OF _ ID1])
+apply (subst slist_map'_ID [symmetric])
+apply (intro monofun_cfun below_refl)
+apply (simp add: cfun_below_iff ep_pair.e_p_below)
+done
+
text {*
Types @{typ "'a list u"}. and @{typ "'a u slist"} are isomorphic.
*}
@@ -48,34 +96,52 @@
subsection {* Lists are a predomain *}
+definition udefl :: "udom defl \<rightarrow> udom u defl"
+ where "udefl = defl_fun1 (strictify\<cdot>up) (fup\<cdot>ID) ID"
+
+lemma cast_udefl:
+ "cast\<cdot>(udefl\<cdot>t) = strictify\<cdot>up oo cast\<cdot>t oo fup\<cdot>ID"
+unfolding udefl_def by (simp add: cast_defl_fun1 ep_pair_strictify_up)
+
+definition list_liftdefl :: "udom u defl \<rightarrow> udom u defl"
+ where "list_liftdefl = (\<Lambda> a. udefl\<cdot>(slist_defl\<cdot>(u_defl\<cdot>a)))"
+
+lemma cast_slist_defl: "cast\<cdot>(slist_defl\<cdot>a) = emb oo slist_map\<cdot>(cast\<cdot>a) oo prj"
+using isodefl_slist [where fa="cast\<cdot>a" and da="a"]
+unfolding isodefl_def by simp
+
+lemma u_emb_bottom: "u_emb\<cdot>\<bottom> = \<bottom>"
+by (rule pcpo_ep_pair.e_strict [unfolded pcpo_ep_pair_def, OF ep_pair_u])
+
instantiation list :: (predomain) predomain
begin
definition
- "liftemb = emb oo encode_list_u"
+ "liftemb = (strictify\<cdot>up oo emb oo slist_map'\<cdot>u_emb) oo slist_map'\<cdot>liftemb oo encode_list_u"
definition
- "liftprj = decode_list_u oo prj"
+ "liftprj = (decode_list_u oo slist_map'\<cdot>liftprj) oo (slist_map'\<cdot>u_prj oo prj) oo fup\<cdot>ID"
definition
- "liftdefl (t::('a list) itself) = DEFL(('a\<^sub>\<bottom>) slist)"
+ "liftdefl (t::('a list) itself) = list_liftdefl\<cdot>LIFTDEFL('a)"
instance proof
- have "ep_pair encode_list_u decode_list_u"
- by (rule ep_pair.intro, simp_all)
- thus "ep_pair liftemb (liftprj :: udom \<rightarrow> ('a list) u)"
+ show "ep_pair liftemb (liftprj :: udom u \<rightarrow> ('a list) u)"
unfolding liftemb_list_def liftprj_list_def
- using ep_pair_emb_prj by (rule ep_pair_comp)
- show "cast\<cdot>LIFTDEFL('a list) = liftemb oo (liftprj :: udom \<rightarrow> ('a list) u)"
+ by (intro ep_pair_comp ep_pair_slist_map' ep_pair_strictify_up
+ ep_pair_emb_prj predomain_ep ep_pair_u, simp add: ep_pair.intro)
+ show "cast\<cdot>LIFTDEFL('a list) = liftemb oo (liftprj :: udom u \<rightarrow> ('a list) u)"
unfolding liftemb_list_def liftprj_list_def liftdefl_list_def
- by (simp add: cfcomp1 cast_DEFL)
+ apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_defl cast_liftdefl)
+ apply (simp add: slist_map'_oo u_emb_bottom cfun_eq_iff)
+ done
qed
end
lemma liftdefl_list [domain_defl_simps]:
- "LIFTDEFL('a::predomain list) = slist_defl\<cdot>LIFTDEFL('a)"
-unfolding liftdefl_list_def by (simp add: domain_defl_simps)
+ "LIFTDEFL('a::predomain list) = list_liftdefl\<cdot>LIFTDEFL('a)"
+by (rule liftdefl_list_def)
subsection {* Continuous map operation for lists *}
@@ -105,21 +171,21 @@
lemma encode_list_u_map:
"encode_list_u\<cdot>(u_map\<cdot>(list_map\<cdot>f)\<cdot>(decode_list_u\<cdot>xs))
= slist_map\<cdot>(u_map\<cdot>f)\<cdot>xs"
-apply (induct xs)
-apply (simp, subst slist_map_unfold, simp)
-apply (simp, subst slist_map_unfold, simp add: SNil_def)
+apply (induct xs, simp, simp)
apply (case_tac a, simp, rename_tac b)
apply (case_tac "decode_list_u\<cdot>xs")
-apply (drule_tac f="encode_list_u" in cfun_arg_cong, simp)
-by (simp, subst slist_map_unfold, simp add: SCons_def)
+apply (drule_tac f="encode_list_u" in cfun_arg_cong, simp, simp)
+done
lemma isodefl_list_u [domain_isodefl]:
fixes d :: "'a::predomain \<rightarrow> 'a"
- assumes "isodefl (u_map\<cdot>d) t"
- shows "isodefl (u_map\<cdot>(list_map\<cdot>d)) (slist_defl\<cdot>t)"
-using assms [THEN isodefl_slist] unfolding isodefl_def
-unfolding emb_u_def prj_u_def liftemb_list_def liftprj_list_def
-by (simp add: cfcomp1 encode_list_u_map)
+ assumes "isodefl' d t"
+ shows "isodefl' (list_map\<cdot>d) (list_liftdefl\<cdot>t)"
+using assms unfolding isodefl'_def liftemb_list_def liftprj_list_def
+apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_defl)
+apply (simp add: cfcomp1 encode_list_u_map)
+apply (simp add: slist_map'_slist_map' u_emb_bottom)
+done
setup {*
Domain_Take_Proofs.add_rec_type (@{type_name "list"}, [true])
--- a/src/HOL/HOLCF/Library/Nat_Discrete.thy Sun Dec 19 19:03:49 2010 +0100
+++ b/src/HOL/HOLCF/Library/Nat_Discrete.thy Sun Dec 19 17:39:20 2010 -0800
@@ -29,23 +29,23 @@
begin
definition
- "(liftemb :: nat u \<rightarrow> udom) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
+ "(liftemb :: nat u \<rightarrow> udom u) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
definition
- "(liftprj :: udom \<rightarrow> nat u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
+ "(liftprj :: udom u \<rightarrow> nat u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
definition
"liftdefl \<equiv> (\<lambda>(t::nat itself). LIFTDEFL(nat discr))"
instance proof
- show "ep_pair liftemb (liftprj :: udom \<rightarrow> nat u)"
+ show "ep_pair liftemb (liftprj :: udom u \<rightarrow> nat u)"
unfolding liftemb_nat_def liftprj_nat_def
apply (rule ep_pair_comp)
apply (rule ep_pair_u_map)
apply (simp add: ep_pair.intro)
apply (rule predomain_ep)
done
- show "cast\<cdot>LIFTDEFL(nat) = liftemb oo (liftprj :: udom \<rightarrow> nat u)"
+ show "cast\<cdot>LIFTDEFL(nat) = liftemb oo (liftprj :: udom u \<rightarrow> nat u)"
unfolding liftemb_nat_def liftprj_nat_def liftdefl_nat_def
apply (simp add: cast_liftdefl cfcomp1 u_map_map)
apply (simp add: ID_def [symmetric] u_map_ID)
--- a/src/HOL/HOLCF/Library/Option_Cpo.thy Sun Dec 19 19:03:49 2010 +0100
+++ b/src/HOL/HOLCF/Library/Option_Cpo.thy Sun Dec 19 17:39:20 2010 -0800
@@ -5,7 +5,7 @@
header {* Cpo class instance for HOL option type *}
theory Option_Cpo
-imports HOLCF
+imports HOLCF Sum_Cpo
begin
subsection {* Ordering on option type *}
@@ -209,45 +209,40 @@
subsection {* Option type is a predomain *}
definition
- "encode_option_u =
- (\<Lambda>(up\<cdot>x). case x of None \<Rightarrow> sinl\<cdot>ONE | Some a \<Rightarrow> sinr\<cdot>(up\<cdot>a))"
+ "encode_option = (\<Lambda> x. case x of None \<Rightarrow> Inl () | Some a \<Rightarrow> Inr a)"
definition
- "decode_option_u = sscase\<cdot>(\<Lambda> ONE. up\<cdot>None)\<cdot>(\<Lambda>(up\<cdot>a). up\<cdot>(Some a))"
-
-lemma decode_encode_option_u [simp]: "decode_option_u\<cdot>(encode_option_u\<cdot>x) = x"
-unfolding decode_option_u_def encode_option_u_def
-by (case_tac x, simp, rename_tac y, case_tac y, simp_all)
+ "decode_option = (\<Lambda> x. case x of Inl (u::unit) \<Rightarrow> None | Inr a \<Rightarrow> Some a)"
-lemma encode_decode_option_u [simp]: "encode_option_u\<cdot>(decode_option_u\<cdot>x) = x"
-unfolding decode_option_u_def encode_option_u_def
-apply (case_tac x, simp)
-apply (rename_tac a, case_tac a rule: oneE, simp, simp)
-apply (rename_tac b, case_tac b, simp, simp)
-done
+lemma decode_encode_option [simp]: "decode_option\<cdot>(encode_option\<cdot>x) = x"
+unfolding decode_option_def encode_option_def
+by (cases x, simp_all)
+
+lemma encode_decode_option [simp]: "encode_option\<cdot>(decode_option\<cdot>x) = x"
+unfolding decode_option_def encode_option_def
+by (cases x, simp_all)
instantiation option :: (predomain) predomain
begin
definition
- "liftemb = emb oo encode_option_u"
+ "liftemb = liftemb oo u_map\<cdot>encode_option"
definition
- "liftprj = decode_option_u oo prj"
+ "liftprj = u_map\<cdot>decode_option oo liftprj"
definition
- "liftdefl (t::('a option) itself) = DEFL(one \<oplus> 'a u)"
+ "liftdefl (t::('a option) itself) = LIFTDEFL(unit + 'a)"
instance proof
- show "ep_pair liftemb (liftprj :: udom \<rightarrow> ('a option) u)"
+ show "ep_pair liftemb (liftprj :: udom u \<rightarrow> ('a option) u)"
unfolding liftemb_option_def liftprj_option_def
- apply (rule ep_pair_comp)
+ apply (intro ep_pair_comp ep_pair_u_map predomain_ep)
apply (rule ep_pair.intro, simp, simp)
- apply (rule ep_pair_emb_prj)
done
- show "cast\<cdot>LIFTDEFL('a option) = liftemb oo (liftprj :: udom \<rightarrow> ('a option) u)"
+ show "cast\<cdot>LIFTDEFL('a option) = liftemb oo (liftprj :: udom u \<rightarrow> ('a option) u)"
unfolding liftemb_option_def liftprj_option_def liftdefl_option_def
- by (simp add: cast_DEFL cfcomp1)
+ by (simp add: cast_liftdefl cfcomp1 u_map_map ID_def [symmetric] u_map_ID)
qed
end
--- a/src/HOL/HOLCF/Library/Sum_Cpo.thy Sun Dec 19 19:03:49 2010 +0100
+++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy Sun Dec 19 17:39:20 2010 -0800
@@ -260,28 +260,43 @@
apply (rename_tac b, case_tac b, simp, simp)
done
+lemma ep_pair_strictify_up:
+ "ep_pair (strictify\<cdot>up) (fup\<cdot>ID)"
+apply (rule ep_pair.intro)
+apply (simp add: strictify_conv_if)
+apply (case_tac y, simp, simp add: strictify_conv_if)
+done
+
+definition sum_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl"
+ where "sum_liftdefl = defl_fun2 (u_map\<cdot>emb oo strictify\<cdot>up)
+ (fup\<cdot>ID oo u_map\<cdot>prj) ssum_map"
+
instantiation sum :: (predomain, predomain) predomain
begin
definition
- "liftemb = emb oo encode_sum_u"
+ "liftemb = (u_map\<cdot>emb oo strictify\<cdot>up) oo
+ (ssum_map\<cdot>liftemb\<cdot>liftemb oo encode_sum_u)"
definition
- "liftprj = decode_sum_u oo prj"
+ "liftprj = (decode_sum_u oo ssum_map\<cdot>liftprj\<cdot>liftprj) oo
+ (fup\<cdot>ID oo u_map\<cdot>prj)"
definition
- "liftdefl (t::('a + 'b) itself) = DEFL('a u \<oplus> 'b u)"
+ "liftdefl (t::('a + 'b) itself) = sum_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
instance proof
- show "ep_pair liftemb (liftprj :: udom \<rightarrow> ('a + 'b) u)"
+ show "ep_pair liftemb (liftprj :: udom u \<rightarrow> ('a + 'b) u)"
unfolding liftemb_sum_def liftprj_sum_def
- apply (rule ep_pair_comp)
- apply (rule ep_pair.intro, simp, simp)
- apply (rule ep_pair_emb_prj)
- done
- show "cast\<cdot>LIFTDEFL('a + 'b) = liftemb oo (liftprj :: udom \<rightarrow> ('a + 'b) u)"
+ by (intro ep_pair_comp ep_pair_ssum_map ep_pair_u_map ep_pair_emb_prj
+ ep_pair_strictify_up predomain_ep, simp add: ep_pair.intro)
+ show "cast\<cdot>LIFTDEFL('a + 'b) = liftemb oo (liftprj :: udom u \<rightarrow> ('a + 'b) u)"
unfolding liftemb_sum_def liftprj_sum_def liftdefl_sum_def
- by (simp add: cast_DEFL cfcomp1)
+ apply (subst sum_liftdefl_def, subst cast_defl_fun2)
+ apply (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj
+ ep_pair_strictify_up)
+ apply (erule (1) finite_deflation_ssum_map)
+ by (simp add: cast_liftdefl cfcomp1 ssum_map_map)
qed
end
--- a/src/HOL/HOLCF/LowerPD.thy Sun Dec 19 19:03:49 2010 +0100
+++ b/src/HOL/HOLCF/LowerPD.thy Sun Dec 19 17:39:20 2010 -0800
@@ -5,7 +5,7 @@
header {* Lower powerdomain *}
theory LowerPD
-imports CompactBasis
+imports Compact_Basis
begin
subsection {* Basis preorder *}
@@ -80,7 +80,7 @@
type_notation (xsymbols) lower_pd ("('(_')\<flat>)")
-instantiation lower_pd :: ("domain") below
+instantiation lower_pd :: (bifinite) below
begin
definition
@@ -89,11 +89,11 @@
instance ..
end
-instance lower_pd :: ("domain") po
+instance lower_pd :: (bifinite) po
using type_definition_lower_pd below_lower_pd_def
by (rule lower_le.typedef_ideal_po)
-instance lower_pd :: ("domain") cpo
+instance lower_pd :: (bifinite) cpo
using type_definition_lower_pd below_lower_pd_def
by (rule lower_le.typedef_ideal_cpo)
@@ -112,7 +112,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 :: ("domain") pcpo
+instance lower_pd :: (bifinite) pcpo
by intro_classes (fast intro: lower_pd_minimal)
lemma inst_lower_pd_pcpo: "\<bottom> = lower_principal (PDUnit compact_bot)"
@@ -458,66 +458,21 @@
by (rule finite_range_imp_finite_fixes)
qed
-subsection {* Lower powerdomain is a domain *}
-
-definition
- lower_approx :: "nat \<Rightarrow> udom lower_pd \<rightarrow> udom lower_pd"
-where
- "lower_approx = (\<lambda>i. lower_map\<cdot>(udom_approx i))"
-
-lemma lower_approx: "approx_chain lower_approx"
-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"
-
-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"
-using lower_approx finite_deflation_lower_map
-unfolding lower_defl_def by (rule cast_defl_fun1)
-
-instantiation lower_pd :: ("domain") liftdomain
-begin
-
-definition
- "emb = udom_emb lower_approx oo lower_map\<cdot>emb"
-
-definition
- "prj = lower_map\<cdot>prj oo udom_prj lower_approx"
+subsection {* Lower powerdomain is bifinite *}
-definition
- "defl (t::'a lower_pd itself) = lower_defl\<cdot>DEFL('a)"
-
-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)"
+lemma approx_chain_lower_map:
+ assumes "approx_chain a"
+ shows "approx_chain (\<lambda>i. lower_map\<cdot>(a i))"
+ using assms unfolding approx_chain_def
+ by (simp add: lub_APP lower_map_ID finite_deflation_lower_map)
-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]
- by (intro ep_pair_comp ep_pair_lower_map ep_pair_emb_prj)
-next
- show "cast\<cdot>DEFL('a lower_pd) = emb oo (prj :: udom \<rightarrow> 'a lower_pd)"
- unfolding emb_lower_pd_def prj_lower_pd_def defl_lower_pd_def cast_lower_defl
- by (simp add: cast_DEFL oo_def cfun_eq_iff lower_map_map)
+instance lower_pd :: (bifinite) bifinite
+proof
+ show "\<exists>(a::nat \<Rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd). approx_chain a"
+ using bifinite [where 'a='a]
+ by (fast intro!: approx_chain_lower_map)
qed
-end
-
-lemma DEFL_lower: "DEFL('a lower_pd) = lower_defl\<cdot>DEFL('a)"
-by (rule defl_lower_pd_def)
-
-
subsection {* Join *}
definition
--- a/src/HOL/HOLCF/Map_Functions.thy Sun Dec 19 19:03:49 2010 +0100
+++ b/src/HOL/HOLCF/Map_Functions.thy Sun Dec 19 17:39:20 2010 -0800
@@ -191,6 +191,9 @@
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 u_map_oo: "u_map\<cdot>(f oo g) = u_map\<cdot>f oo u_map\<cdot>g"
+by (simp add: cfcomp1 u_map_map eta_cfun)
+
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)
--- a/src/HOL/HOLCF/Powerdomains.thy Sun Dec 19 19:03:49 2010 +0100
+++ b/src/HOL/HOLCF/Powerdomains.thy Sun Dec 19 17:39:20 2010 -0800
@@ -8,6 +8,167 @@
imports ConvexPD Domain
begin
+subsection {* Universal domain embeddings *}
+
+definition "upper_emb = udom_emb (\<lambda>i. upper_map\<cdot>(udom_approx i))"
+definition "upper_prj = udom_prj (\<lambda>i. upper_map\<cdot>(udom_approx i))"
+
+definition "lower_emb = udom_emb (\<lambda>i. lower_map\<cdot>(udom_approx i))"
+definition "lower_prj = udom_prj (\<lambda>i. lower_map\<cdot>(udom_approx i))"
+
+definition "convex_emb = udom_emb (\<lambda>i. convex_map\<cdot>(udom_approx i))"
+definition "convex_prj = udom_prj (\<lambda>i. convex_map\<cdot>(udom_approx i))"
+
+lemma ep_pair_upper: "ep_pair upper_emb upper_prj"
+ unfolding upper_emb_def upper_prj_def
+ by (simp add: ep_pair_udom approx_chain_upper_map)
+
+lemma ep_pair_lower: "ep_pair lower_emb lower_prj"
+ unfolding lower_emb_def lower_prj_def
+ by (simp add: ep_pair_udom approx_chain_lower_map)
+
+lemma ep_pair_convex: "ep_pair convex_emb convex_prj"
+ unfolding convex_emb_def convex_prj_def
+ by (simp add: ep_pair_udom approx_chain_convex_map)
+
+subsection {* Deflation combinators *}
+
+definition upper_defl :: "udom defl \<rightarrow> udom defl"
+ where "upper_defl = defl_fun1 upper_emb upper_prj upper_map"
+
+definition lower_defl :: "udom defl \<rightarrow> udom defl"
+ where "lower_defl = defl_fun1 lower_emb lower_prj lower_map"
+
+definition convex_defl :: "udom defl \<rightarrow> udom defl"
+ where "convex_defl = defl_fun1 convex_emb convex_prj convex_map"
+
+lemma cast_upper_defl:
+ "cast\<cdot>(upper_defl\<cdot>A) = upper_emb oo upper_map\<cdot>(cast\<cdot>A) oo upper_prj"
+using ep_pair_upper finite_deflation_upper_map
+unfolding upper_defl_def by (rule cast_defl_fun1)
+
+lemma cast_lower_defl:
+ "cast\<cdot>(lower_defl\<cdot>A) = lower_emb oo lower_map\<cdot>(cast\<cdot>A) oo lower_prj"
+using ep_pair_lower finite_deflation_lower_map
+unfolding lower_defl_def by (rule cast_defl_fun1)
+
+lemma cast_convex_defl:
+ "cast\<cdot>(convex_defl\<cdot>A) = convex_emb oo convex_map\<cdot>(cast\<cdot>A) oo convex_prj"
+using ep_pair_convex finite_deflation_convex_map
+unfolding convex_defl_def by (rule cast_defl_fun1)
+
+subsection {* Domain class instances *}
+
+instantiation upper_pd :: ("domain") "domain"
+begin
+
+definition
+ "emb = upper_emb oo upper_map\<cdot>emb"
+
+definition
+ "prj = upper_map\<cdot>prj oo upper_prj"
+
+definition
+ "defl (t::'a upper_pd itself) = upper_defl\<cdot>DEFL('a)"
+
+definition
+ "(liftemb :: 'a upper_pd u \<rightarrow> udom u) = u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom u \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj"
+
+definition
+ "liftdefl (t::'a upper_pd itself) = pdefl\<cdot>DEFL('a upper_pd)"
+
+instance proof
+ show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)"
+ unfolding emb_upper_pd_def prj_upper_pd_def
+ by (intro ep_pair_comp ep_pair_upper ep_pair_upper_map ep_pair_emb_prj)
+next
+ show "cast\<cdot>DEFL('a upper_pd) = emb oo (prj :: udom \<rightarrow> 'a upper_pd)"
+ unfolding emb_upper_pd_def prj_upper_pd_def defl_upper_pd_def cast_upper_defl
+ by (simp add: cast_DEFL oo_def cfun_eq_iff upper_map_map)
+qed (fact liftemb_upper_pd_def liftprj_upper_pd_def liftdefl_upper_pd_def)+
+
+end
+
+instantiation lower_pd :: ("domain") "domain"
+begin
+
+definition
+ "emb = lower_emb oo lower_map\<cdot>emb"
+
+definition
+ "prj = lower_map\<cdot>prj oo lower_prj"
+
+definition
+ "defl (t::'a lower_pd itself) = lower_defl\<cdot>DEFL('a)"
+
+definition
+ "(liftemb :: 'a lower_pd u \<rightarrow> udom u) = u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom u \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj"
+
+definition
+ "liftdefl (t::'a lower_pd itself) = pdefl\<cdot>DEFL('a lower_pd)"
+
+instance proof
+ show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)"
+ unfolding emb_lower_pd_def prj_lower_pd_def
+ by (intro ep_pair_comp ep_pair_lower ep_pair_lower_map ep_pair_emb_prj)
+next
+ show "cast\<cdot>DEFL('a lower_pd) = emb oo (prj :: udom \<rightarrow> 'a lower_pd)"
+ unfolding emb_lower_pd_def prj_lower_pd_def defl_lower_pd_def cast_lower_defl
+ by (simp add: cast_DEFL oo_def cfun_eq_iff lower_map_map)
+qed (fact liftemb_lower_pd_def liftprj_lower_pd_def liftdefl_lower_pd_def)+
+
+end
+
+instantiation convex_pd :: ("domain") "domain"
+begin
+
+definition
+ "emb = convex_emb oo convex_map\<cdot>emb"
+
+definition
+ "prj = convex_map\<cdot>prj oo convex_prj"
+
+definition
+ "defl (t::'a convex_pd itself) = convex_defl\<cdot>DEFL('a)"
+
+definition
+ "(liftemb :: 'a convex_pd u \<rightarrow> udom u) = u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom u \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj"
+
+definition
+ "liftdefl (t::'a convex_pd itself) = pdefl\<cdot>DEFL('a convex_pd)"
+
+instance proof
+ show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)"
+ unfolding emb_convex_pd_def prj_convex_pd_def
+ by (intro ep_pair_comp ep_pair_convex ep_pair_convex_map ep_pair_emb_prj)
+next
+ show "cast\<cdot>DEFL('a convex_pd) = emb oo (prj :: udom \<rightarrow> 'a convex_pd)"
+ unfolding emb_convex_pd_def prj_convex_pd_def defl_convex_pd_def cast_convex_defl
+ by (simp add: cast_DEFL oo_def cfun_eq_iff convex_map_map)
+qed (fact liftemb_convex_pd_def liftprj_convex_pd_def liftdefl_convex_pd_def)+
+
+end
+
+lemma DEFL_upper: "DEFL('a::domain upper_pd) = upper_defl\<cdot>DEFL('a)"
+by (rule defl_upper_pd_def)
+
+lemma DEFL_lower: "DEFL('a::domain lower_pd) = lower_defl\<cdot>DEFL('a)"
+by (rule defl_lower_pd_def)
+
+lemma DEFL_convex: "DEFL('a::domain convex_pd) = convex_defl\<cdot>DEFL('a)"
+by (rule defl_convex_pd_def)
+
+subsection {* Isomorphic deflations *}
+
lemma isodefl_upper:
"isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)"
apply (rule isodeflI)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/Representable.thy Sun Dec 19 17:39:20 2010 -0800
@@ -0,0 +1,647 @@
+(* Title: HOLCF/Representable.thy
+ Author: Brian Huffman
+*)
+
+header {* Representable domains *}
+
+theory Representable
+imports Algebraic Map_Functions Countable
+begin
+
+default_sort cpo
+
+subsection {* Class of representable domains *}
+
+text {*
+ We define a ``domain'' as a pcpo that is isomorphic to some
+ algebraic deflation over the universal domain; this is equivalent
+ to being omega-bifinite.
+
+ A predomain is a cpo that, when lifted, becomes a domain.
+ Predomains are represented by deflations over a lifted universal
+ domain type.
+*}
+
+class predomain_syn = cpo +
+ fixes liftemb :: "'a\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
+ fixes liftprj :: "udom\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>"
+ fixes liftdefl :: "'a itself \<Rightarrow> udom u defl"
+
+class predomain = predomain_syn +
+ assumes predomain_ep: "ep_pair liftemb liftprj"
+ assumes cast_liftdefl: "cast\<cdot>(liftdefl TYPE('a)) = liftemb oo liftprj"
+
+syntax "_LIFTDEFL" :: "type \<Rightarrow> logic" ("(1LIFTDEFL/(1'(_')))")
+translations "LIFTDEFL('t)" \<rightleftharpoons> "CONST liftdefl TYPE('t)"
+
+definition pdefl :: "udom defl \<rightarrow> udom u defl"
+ where "pdefl = defl_fun1 ID ID u_map"
+
+lemma cast_pdefl: "cast\<cdot>(pdefl\<cdot>t) = u_map\<cdot>(cast\<cdot>t)"
+by (simp add: pdefl_def cast_defl_fun1 ep_pair_def finite_deflation_u_map)
+
+class "domain" = predomain_syn + pcpo +
+ fixes emb :: "'a \<rightarrow> udom"
+ fixes prj :: "udom \<rightarrow> 'a"
+ fixes defl :: "'a itself \<Rightarrow> udom defl"
+ assumes ep_pair_emb_prj: "ep_pair emb prj"
+ assumes cast_DEFL: "cast\<cdot>(defl TYPE('a)) = emb oo prj"
+ assumes liftemb_eq: "liftemb = u_map\<cdot>emb"
+ assumes liftprj_eq: "liftprj = u_map\<cdot>prj"
+ assumes liftdefl_eq: "liftdefl TYPE('a) = pdefl\<cdot>(defl TYPE('a))"
+
+syntax "_DEFL" :: "type \<Rightarrow> logic" ("(1DEFL/(1'(_')))")
+translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)"
+
+instance "domain" \<subseteq> predomain
+proof
+ show "ep_pair liftemb (liftprj::udom\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>)"
+ unfolding liftemb_eq liftprj_eq
+ by (intro ep_pair_u_map ep_pair_emb_prj)
+ show "cast\<cdot>LIFTDEFL('a) = liftemb oo (liftprj::udom\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>)"
+ unfolding liftemb_eq liftprj_eq liftdefl_eq
+ by (simp add: cast_pdefl cast_DEFL u_map_oo)
+qed
+
+text {*
+ Constants @{const liftemb} and @{const liftprj} imply class predomain.
+*}
+
+setup {*
+ fold Sign.add_const_constraint
+ [(@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom u"}),
+ (@{const_name liftprj}, SOME @{typ "udom u \<rightarrow> 'a::predomain u"}),
+ (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> udom u defl"})]
+*}
+
+interpretation predomain: pcpo_ep_pair liftemb liftprj
+ unfolding pcpo_ep_pair_def by (rule predomain_ep)
+
+interpretation "domain": pcpo_ep_pair emb prj
+ unfolding pcpo_ep_pair_def by (rule ep_pair_emb_prj)
+
+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 {* Domains are bifinite *}
+
+lemma approx_chain_ep_cast:
+ assumes ep: "ep_pair (e::'a::pcpo \<rightarrow> 'b::bifinite) (p::'b \<rightarrow> 'a)"
+ assumes cast_t: "cast\<cdot>t = e oo p"
+ shows "\<exists>(a::nat \<Rightarrow> 'a::pcpo \<rightarrow> 'a). approx_chain a"
+proof -
+ interpret ep_pair e p by fact
+ obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)"
+ and t: "t = (\<Squnion>i. defl_principal (Y i))"
+ by (rule defl.obtain_principal_chain)
+ def approx \<equiv> "\<lambda>i. (p oo cast\<cdot>(defl_principal (Y i)) oo e) :: 'a \<rightarrow> 'a"
+ have "approx_chain approx"
+ proof (rule approx_chain.intro)
+ show "chain (\<lambda>i. approx i)"
+ unfolding approx_def by (simp add: Y)
+ show "(\<Squnion>i. approx i) = ID"
+ unfolding approx_def
+ by (simp add: lub_distribs Y t [symmetric] cast_t cfun_eq_iff)
+ show "\<And>i. finite_deflation (approx i)"
+ unfolding approx_def
+ apply (rule finite_deflation_p_d_e)
+ apply (rule finite_deflation_cast)
+ apply (rule defl.compact_principal)
+ apply (rule below_trans [OF monofun_cfun_fun])
+ apply (rule is_ub_thelub, simp add: Y)
+ apply (simp add: lub_distribs Y t [symmetric] cast_t)
+ done
+ qed
+ thus "\<exists>(a::nat \<Rightarrow> 'a \<rightarrow> 'a). approx_chain a" by - (rule exI)
+qed
+
+instance "domain" \<subseteq> bifinite
+by default (rule approx_chain_ep_cast [OF ep_pair_emb_prj cast_DEFL])
+
+instance predomain \<subseteq> profinite
+by default (rule approx_chain_ep_cast [OF predomain_ep cast_liftdefl])
+
+subsection {* Universal domain ep-pairs *}
+
+definition "u_emb = udom_emb (\<lambda>i. u_map\<cdot>(udom_approx i))"
+definition "u_prj = udom_prj (\<lambda>i. u_map\<cdot>(udom_approx i))"
+
+definition "prod_emb = udom_emb (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+definition "prod_prj = udom_prj (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+
+definition "sprod_emb = udom_emb (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+definition "sprod_prj = udom_prj (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+
+definition "ssum_emb = udom_emb (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+definition "ssum_prj = udom_prj (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+
+definition "sfun_emb = udom_emb (\<lambda>i. sfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+definition "sfun_prj = udom_prj (\<lambda>i. sfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+
+lemma ep_pair_u: "ep_pair u_emb u_prj"
+ unfolding u_emb_def u_prj_def
+ by (simp add: ep_pair_udom approx_chain_u_map)
+
+lemma ep_pair_prod: "ep_pair prod_emb prod_prj"
+ unfolding prod_emb_def prod_prj_def
+ by (simp add: ep_pair_udom approx_chain_cprod_map)
+
+lemma ep_pair_sprod: "ep_pair sprod_emb sprod_prj"
+ unfolding sprod_emb_def sprod_prj_def
+ by (simp add: ep_pair_udom approx_chain_sprod_map)
+
+lemma ep_pair_ssum: "ep_pair ssum_emb ssum_prj"
+ unfolding ssum_emb_def ssum_prj_def
+ by (simp add: ep_pair_udom approx_chain_ssum_map)
+
+lemma ep_pair_sfun: "ep_pair sfun_emb sfun_prj"
+ unfolding sfun_emb_def sfun_prj_def
+ by (simp add: ep_pair_udom approx_chain_sfun_map)
+
+subsection {* Type combinators *}
+
+definition u_defl :: "udom u defl \<rightarrow> udom defl"
+ where "u_defl = defl_fun1 u_emb u_prj ID"
+
+definition prod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
+ where "prod_defl = defl_fun2 prod_emb prod_prj cprod_map"
+
+definition sprod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
+ where "sprod_defl = defl_fun2 sprod_emb sprod_prj sprod_map"
+
+definition ssum_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
+where "ssum_defl = defl_fun2 ssum_emb ssum_prj ssum_map"
+
+definition sfun_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
+ where "sfun_defl = defl_fun2 sfun_emb sfun_prj sfun_map"
+
+lemma cast_u_defl:
+ "cast\<cdot>(u_defl\<cdot>A) = u_emb oo cast\<cdot>A oo u_prj"
+unfolding u_defl_def by (simp add: cast_defl_fun1 ep_pair_u)
+
+lemma cast_prod_defl:
+ "cast\<cdot>(prod_defl\<cdot>A\<cdot>B) =
+ prod_emb oo cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo prod_prj"
+using ep_pair_prod 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) =
+ sprod_emb oo sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo sprod_prj"
+using ep_pair_sprod finite_deflation_sprod_map
+unfolding sprod_defl_def by (rule cast_defl_fun2)
+
+lemma cast_ssum_defl:
+ "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) =
+ ssum_emb oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo ssum_prj"
+using ep_pair_ssum finite_deflation_ssum_map
+unfolding ssum_defl_def by (rule cast_defl_fun2)
+
+lemma cast_sfun_defl:
+ "cast\<cdot>(sfun_defl\<cdot>A\<cdot>B) =
+ sfun_emb oo sfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo sfun_prj"
+using ep_pair_sfun finite_deflation_sfun_map
+unfolding sfun_defl_def by (rule cast_defl_fun2)
+
+subsection {* Class instance proofs *}
+
+subsubsection {* Universal domain *}
+
+instantiation udom :: "domain"
+begin
+
+definition [simp]:
+ "emb = (ID :: udom \<rightarrow> udom)"
+
+definition [simp]:
+ "prj = (ID :: udom \<rightarrow> udom)"
+
+definition
+ "defl (t::udom itself) = (\<Squnion>i. defl_principal (Abs_fin_defl (udom_approx i)))"
+
+definition
+ "(liftemb :: udom u \<rightarrow> udom u) = u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom u \<rightarrow> udom u) = u_map\<cdot>prj"
+
+definition
+ "liftdefl (t::udom itself) = pdefl\<cdot>DEFL(udom)"
+
+instance proof
+ show "ep_pair emb (prj :: udom \<rightarrow> udom)"
+ by (simp add: ep_pair.intro)
+ show "cast\<cdot>DEFL(udom) = emb oo (prj :: udom \<rightarrow> udom)"
+ unfolding defl_udom_def
+ apply (subst contlub_cfun_arg)
+ apply (rule chainI)
+ apply (rule defl.principal_mono)
+ apply (simp add: below_fin_defl_def)
+ apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
+ apply (rule chainE)
+ apply (rule chain_udom_approx)
+ apply (subst cast_defl_principal)
+ apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
+ done
+qed (fact liftemb_udom_def liftprj_udom_def liftdefl_udom_def)+
+
+end
+
+subsubsection {* Lifted cpo *}
+
+instantiation u :: (predomain) "domain"
+begin
+
+definition
+ "emb = u_emb oo liftemb"
+
+definition
+ "prj = liftprj oo u_prj"
+
+definition
+ "defl (t::'a u itself) = u_defl\<cdot>LIFTDEFL('a)"
+
+definition
+ "(liftemb :: 'a u u \<rightarrow> udom u) = u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom u \<rightarrow> 'a u u) = u_map\<cdot>prj"
+
+definition
+ "liftdefl (t::'a u itself) = pdefl\<cdot>DEFL('a u)"
+
+instance proof
+ show "ep_pair emb (prj :: udom \<rightarrow> 'a u)"
+ unfolding emb_u_def prj_u_def
+ by (intro ep_pair_comp ep_pair_u predomain_ep)
+ show "cast\<cdot>DEFL('a u) = emb oo (prj :: udom \<rightarrow> 'a u)"
+ unfolding emb_u_def prj_u_def defl_u_def
+ by (simp add: cast_u_defl cast_liftdefl assoc_oo)
+qed (fact liftemb_u_def liftprj_u_def liftdefl_u_def)+
+
+end
+
+lemma DEFL_u: "DEFL('a::predomain u) = u_defl\<cdot>LIFTDEFL('a)"
+by (rule defl_u_def)
+
+subsubsection {* Strict function space *}
+
+instantiation sfun :: ("domain", "domain") "domain"
+begin
+
+definition
+ "emb = sfun_emb oo sfun_map\<cdot>prj\<cdot>emb"
+
+definition
+ "prj = sfun_map\<cdot>emb\<cdot>prj oo sfun_prj"
+
+definition
+ "defl (t::('a \<rightarrow>! 'b) itself) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+
+definition
+ "(liftemb :: ('a \<rightarrow>! 'b) u \<rightarrow> udom u) = u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom u \<rightarrow> ('a \<rightarrow>! 'b) u) = u_map\<cdot>prj"
+
+definition
+ "liftdefl (t::('a \<rightarrow>! 'b) itself) = pdefl\<cdot>DEFL('a \<rightarrow>! 'b)"
+
+instance proof
+ show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
+ unfolding emb_sfun_def prj_sfun_def
+ by (intro ep_pair_comp ep_pair_sfun ep_pair_sfun_map ep_pair_emb_prj)
+ show "cast\<cdot>DEFL('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
+ unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl
+ by (simp add: cast_DEFL oo_def sfun_eq_iff sfun_map_map)
+qed (fact liftemb_sfun_def liftprj_sfun_def liftdefl_sfun_def)+
+
+end
+
+lemma DEFL_sfun:
+ "DEFL('a::domain \<rightarrow>! 'b::domain) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+by (rule defl_sfun_def)
+
+subsubsection {* Continuous function space *}
+
+instantiation cfun :: (predomain, "domain") "domain"
+begin
+
+definition
+ "emb = emb oo encode_cfun"
+
+definition
+ "prj = decode_cfun oo prj"
+
+definition
+ "defl (t::('a \<rightarrow> 'b) itself) = DEFL('a u \<rightarrow>! 'b)"
+
+definition
+ "(liftemb :: ('a \<rightarrow> 'b) u \<rightarrow> udom u) = u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom u \<rightarrow> ('a \<rightarrow> 'b) u) = u_map\<cdot>prj"
+
+definition
+ "liftdefl (t::('a \<rightarrow> 'b) itself) = pdefl\<cdot>DEFL('a \<rightarrow> 'b)"
+
+instance proof
+ have "ep_pair encode_cfun decode_cfun"
+ by (rule ep_pair.intro, simp_all)
+ thus "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
+ unfolding emb_cfun_def prj_cfun_def
+ using ep_pair_emb_prj by (rule ep_pair_comp)
+ show "cast\<cdot>DEFL('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
+ unfolding emb_cfun_def prj_cfun_def defl_cfun_def
+ by (simp add: cast_DEFL cfcomp1)
+qed (fact liftemb_cfun_def liftprj_cfun_def liftdefl_cfun_def)+
+
+end
+
+lemma DEFL_cfun:
+ "DEFL('a::predomain \<rightarrow> 'b::domain) = DEFL('a u \<rightarrow>! 'b)"
+by (rule defl_cfun_def)
+
+subsubsection {* Strict product *}
+
+instantiation sprod :: ("domain", "domain") "domain"
+begin
+
+definition
+ "emb = sprod_emb oo sprod_map\<cdot>emb\<cdot>emb"
+
+definition
+ "prj = sprod_map\<cdot>prj\<cdot>prj oo sprod_prj"
+
+definition
+ "defl (t::('a \<otimes> 'b) itself) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+
+definition
+ "(liftemb :: ('a \<otimes> 'b) u \<rightarrow> udom u) = u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom u \<rightarrow> ('a \<otimes> 'b) u) = u_map\<cdot>prj"
+
+definition
+ "liftdefl (t::('a \<otimes> 'b) itself) = pdefl\<cdot>DEFL('a \<otimes> 'b)"
+
+instance proof
+ show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
+ unfolding emb_sprod_def prj_sprod_def
+ by (intro ep_pair_comp ep_pair_sprod ep_pair_sprod_map ep_pair_emb_prj)
+ show "cast\<cdot>DEFL('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
+ unfolding emb_sprod_def prj_sprod_def defl_sprod_def cast_sprod_defl
+ by (simp add: cast_DEFL oo_def cfun_eq_iff sprod_map_map)
+qed (fact liftemb_sprod_def liftprj_sprod_def liftdefl_sprod_def)+
+
+end
+
+lemma DEFL_sprod:
+ "DEFL('a::domain \<otimes> 'b::domain) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+by (rule defl_sprod_def)
+
+subsubsection {* Cartesian product *}
+
+definition prod_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl"
+ where "prod_liftdefl = defl_fun2 (u_map\<cdot>prod_emb oo decode_prod_u)
+ (encode_prod_u oo u_map\<cdot>prod_prj) sprod_map"
+
+lemma cast_prod_liftdefl:
+ "cast\<cdot>(prod_liftdefl\<cdot>a\<cdot>b) =
+ (u_map\<cdot>prod_emb oo decode_prod_u) oo sprod_map\<cdot>(cast\<cdot>a)\<cdot>(cast\<cdot>b) oo
+ (encode_prod_u oo u_map\<cdot>prod_prj)"
+unfolding prod_liftdefl_def
+apply (rule cast_defl_fun2)
+apply (intro ep_pair_comp ep_pair_u_map ep_pair_prod)
+apply (simp add: ep_pair.intro)
+apply (erule (1) finite_deflation_sprod_map)
+done
+
+instantiation prod :: (predomain, predomain) predomain
+begin
+
+definition
+ "liftemb = (u_map\<cdot>prod_emb oo decode_prod_u) oo
+ (sprod_map\<cdot>liftemb\<cdot>liftemb oo encode_prod_u)"
+
+definition
+ "liftprj = (decode_prod_u oo sprod_map\<cdot>liftprj\<cdot>liftprj) oo
+ (encode_prod_u oo u_map\<cdot>prod_prj)"
+
+definition
+ "liftdefl (t::('a \<times> 'b) itself) = prod_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
+
+instance proof
+ show "ep_pair liftemb (liftprj :: udom u \<rightarrow> ('a \<times> 'b) u)"
+ unfolding liftemb_prod_def liftprj_prod_def
+ by (intro ep_pair_comp ep_pair_sprod_map ep_pair_u_map
+ ep_pair_prod predomain_ep, simp_all add: ep_pair.intro)
+ show "cast\<cdot>LIFTDEFL('a \<times> 'b) = liftemb oo (liftprj :: udom u \<rightarrow> ('a \<times> 'b) u)"
+ unfolding liftemb_prod_def liftprj_prod_def liftdefl_prod_def
+ by (simp add: cast_prod_liftdefl cast_liftdefl cfcomp1 sprod_map_map)
+qed
+
+end
+
+instantiation prod :: ("domain", "domain") "domain"
+begin
+
+definition
+ "emb = prod_emb oo cprod_map\<cdot>emb\<cdot>emb"
+
+definition
+ "prj = cprod_map\<cdot>prj\<cdot>prj oo prod_prj"
+
+definition
+ "defl (t::('a \<times> 'b) itself) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+
+instance proof
+ show 1: "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)"
+ unfolding emb_prod_def prj_prod_def
+ by (intro ep_pair_comp ep_pair_prod ep_pair_cprod_map ep_pair_emb_prj)
+ show 2: "cast\<cdot>DEFL('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
+ unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl
+ by (simp add: cast_DEFL oo_def cfun_eq_iff cprod_map_map)
+ show 3: "liftemb = u_map\<cdot>(emb :: 'a \<times> 'b \<rightarrow> udom)"
+ unfolding emb_prod_def liftemb_prod_def liftemb_eq
+ unfolding encode_prod_u_def decode_prod_u_def
+ by (rule cfun_eqI, case_tac x, simp, clarsimp)
+ show 4: "liftprj = u_map\<cdot>(prj :: udom \<rightarrow> 'a \<times> 'b)"
+ unfolding prj_prod_def liftprj_prod_def liftprj_eq
+ unfolding encode_prod_u_def decode_prod_u_def
+ apply (rule cfun_eqI, case_tac x, simp)
+ apply (rename_tac y, case_tac "prod_prj\<cdot>y", simp)
+ done
+ show 5: "LIFTDEFL('a \<times> 'b) = pdefl\<cdot>DEFL('a \<times> 'b)"
+ by (rule cast_eq_imp_eq)
+ (simp add: cast_liftdefl cast_pdefl cast_DEFL 2 3 4 u_map_oo)
+qed
+
+end
+
+lemma DEFL_prod:
+ "DEFL('a::domain \<times> 'b::domain) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+by (rule defl_prod_def)
+
+lemma LIFTDEFL_prod:
+ "LIFTDEFL('a::predomain \<times> 'b::predomain) =
+ prod_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
+by (rule liftdefl_prod_def)
+
+subsubsection {* Unit type *}
+
+instantiation unit :: "domain"
+begin
+
+definition
+ "emb = (\<bottom> :: unit \<rightarrow> udom)"
+
+definition
+ "prj = (\<bottom> :: udom \<rightarrow> unit)"
+
+definition
+ "defl (t::unit itself) = \<bottom>"
+
+definition
+ "(liftemb :: unit u \<rightarrow> udom u) = u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom u \<rightarrow> unit u) = u_map\<cdot>prj"
+
+definition
+ "liftdefl (t::unit itself) = pdefl\<cdot>DEFL(unit)"
+
+instance proof
+ show "ep_pair emb (prj :: udom \<rightarrow> unit)"
+ unfolding emb_unit_def prj_unit_def
+ by (simp add: ep_pair.intro)
+ show "cast\<cdot>DEFL(unit) = emb oo (prj :: udom \<rightarrow> unit)"
+ unfolding emb_unit_def prj_unit_def defl_unit_def by simp
+qed (fact liftemb_unit_def liftprj_unit_def liftdefl_unit_def)+
+
+end
+
+subsubsection {* Discrete cpo *}
+
+instantiation discr :: (countable) predomain
+begin
+
+definition
+ "(liftemb :: 'a discr u \<rightarrow> udom u) = strictify\<cdot>up oo udom_emb discr_approx"
+
+definition
+ "(liftprj :: udom u \<rightarrow> 'a discr u) = udom_prj discr_approx oo fup\<cdot>ID"
+
+definition
+ "liftdefl (t::'a discr itself) =
+ (\<Squnion>i. defl_principal (Abs_fin_defl (liftemb oo discr_approx i oo (liftprj::udom u \<rightarrow> 'a discr u))))"
+
+instance proof
+ show 1: "ep_pair liftemb (liftprj :: udom u \<rightarrow> 'a discr u)"
+ unfolding liftemb_discr_def liftprj_discr_def
+ apply (intro ep_pair_comp ep_pair_udom [OF discr_approx])
+ apply (rule ep_pair.intro)
+ apply (simp add: strictify_conv_if)
+ apply (case_tac y, simp, simp add: strictify_conv_if)
+ done
+ show "cast\<cdot>LIFTDEFL('a discr) = liftemb oo (liftprj :: udom u \<rightarrow> 'a discr u)"
+ unfolding liftdefl_discr_def
+ apply (subst contlub_cfun_arg)
+ apply (rule chainI)
+ apply (rule defl.principal_mono)
+ apply (simp add: below_fin_defl_def)
+ apply (simp add: Abs_fin_defl_inverse
+ ep_pair.finite_deflation_e_d_p [OF 1]
+ approx_chain.finite_deflation_approx [OF discr_approx])
+ apply (intro monofun_cfun below_refl)
+ apply (rule chainE)
+ apply (rule chain_discr_approx)
+ apply (subst cast_defl_principal)
+ apply (simp add: Abs_fin_defl_inverse
+ ep_pair.finite_deflation_e_d_p [OF 1]
+ approx_chain.finite_deflation_approx [OF discr_approx])
+ apply (simp add: lub_distribs)
+ done
+qed
+
+end
+
+subsubsection {* Strict sum *}
+
+instantiation ssum :: ("domain", "domain") "domain"
+begin
+
+definition
+ "emb = ssum_emb oo ssum_map\<cdot>emb\<cdot>emb"
+
+definition
+ "prj = ssum_map\<cdot>prj\<cdot>prj oo ssum_prj"
+
+definition
+ "defl (t::('a \<oplus> 'b) itself) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+
+definition
+ "(liftemb :: ('a \<oplus> 'b) u \<rightarrow> udom u) = u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom u \<rightarrow> ('a \<oplus> 'b) u) = u_map\<cdot>prj"
+
+definition
+ "liftdefl (t::('a \<oplus> 'b) itself) = pdefl\<cdot>DEFL('a \<oplus> 'b)"
+
+instance proof
+ show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
+ unfolding emb_ssum_def prj_ssum_def
+ by (intro ep_pair_comp ep_pair_ssum ep_pair_ssum_map ep_pair_emb_prj)
+ show "cast\<cdot>DEFL('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
+ unfolding emb_ssum_def prj_ssum_def defl_ssum_def cast_ssum_defl
+ by (simp add: cast_DEFL oo_def cfun_eq_iff ssum_map_map)
+qed (fact liftemb_ssum_def liftprj_ssum_def liftdefl_ssum_def)+
+
+end
+
+lemma DEFL_ssum:
+ "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) "domain"
+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 u) = u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom u \<rightarrow> 'a lift u) = u_map\<cdot>prj"
+
+definition
+ "liftdefl (t::'a lift itself) = pdefl\<cdot>DEFL('a lift)"
+
+instance proof
+ note [simp] = cont_Rep_lift cont_Abs_lift Rep_lift_inverse Abs_lift_inverse
+ have "ep_pair (\<Lambda>(x::'a lift). Rep_lift x) (\<Lambda> y. Abs_lift y)"
+ by (simp add: ep_pair_def)
+ 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 (fact liftemb_lift_def liftprj_lift_def liftdefl_lift_def)+
+
+end
+
+end
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Dec 19 19:03:49 2010 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Dec 19 17:39:20 2010 -0800
@@ -68,7 +68,8 @@
infixr -->>
val udomT = @{typ udom}
-val deflT = @{typ "defl"}
+val deflT = @{typ "udom defl"}
+val udeflT = @{typ "udom u defl"}
fun mk_DEFL T =
Const (@{const_name defl}, Term.itselfT T --> deflT) $ Logic.mk_type T
@@ -77,7 +78,7 @@
| dest_DEFL t = raise TERM ("dest_DEFL", [t])
fun mk_LIFTDEFL T =
- Const (@{const_name liftdefl}, Term.itselfT T --> deflT) $ Logic.mk_type T
+ Const (@{const_name liftdefl}, Term.itselfT T --> udeflT) $ Logic.mk_type T
fun dest_LIFTDEFL (Const (@{const_name liftdefl}, _) $ t) = Logic.dest_type t
| dest_LIFTDEFL t = raise TERM ("dest_LIFTDEFL", [t])
@@ -100,6 +101,9 @@
fun isodefl_const T =
Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT)
+fun isodefl'_const T =
+ Const (@{const_name isodefl'}, (T ->> T) --> udeflT --> HOLogic.boolT)
+
fun mk_deflation t =
Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t
@@ -218,7 +222,7 @@
| _ => NONE) handle TERM _ => NONE
fun proc2 t =
(case dest_LIFTDEFL t of
- TFree (a, _) => SOME (Free ("p" ^ Library.unprefix "'" a, deflT))
+ TFree (a, _) => SOME (Free ("p" ^ Library.unprefix "'" a, udeflT))
| _ => NONE) handle TERM _ => NONE
in
Pattern.rewrite_term thy (rules @ rules') [proc1, proc2] (mk_DEFL T)
@@ -492,7 +496,7 @@
let
val defl_bind = Binding.suffix_name "_defl" tbind
val defl_type =
- map Term.itselfT typeTs ---> map (K deflT) defl_args -->> deflT
+ map Term.itselfT typeTs ---> map fastype_of defl_args -->> deflT
in
Sign.declare_const ((defl_bind, defl_type), NoSyn) thy
end
@@ -614,11 +618,11 @@
let
fun unprime a = Library.unprefix "'" a
fun mk_d T = Free ("d" ^ unprime (fst (dest_TFree T)), deflT)
- fun mk_p T = Free ("p" ^ unprime (fst (dest_TFree T)), deflT)
+ fun mk_p T = Free ("p" ^ unprime (fst (dest_TFree T)), udeflT)
fun mk_f T = Free ("f" ^ unprime (fst (dest_TFree T)), T ->> T)
fun mk_assm t =
case try dest_LIFTDEFL t of
- SOME T => mk_trp (isodefl_const (mk_upT T) $ mk_u_map (mk_f T) $ mk_p T)
+ SOME T => mk_trp (isodefl'_const T $ mk_f T $ mk_p T)
| NONE =>
let val T = dest_DEFL t
in mk_trp (isodefl_const T $ mk_f T $ mk_d T) end
--- a/src/HOL/HOLCF/Tools/domaindef.ML Sun Dec 19 19:03:49 2010 +0100
+++ b/src/HOL/HOLCF/Tools/domaindef.ML Sun Dec 19 17:39:20 2010 -0800
@@ -49,13 +49,14 @@
(* building types and terms *)
val udomT = @{typ udom}
-val deflT = @{typ defl}
+val deflT = @{typ "udom defl"}
+val udeflT = @{typ "udom u defl"}
fun emb_const T = Const (@{const_name emb}, T ->> udomT)
fun prj_const T = Const (@{const_name prj}, udomT ->> T)
fun defl_const T = Const (@{const_name defl}, Term.itselfT T --> deflT)
-fun liftemb_const T = Const (@{const_name liftemb}, mk_upT T ->> udomT)
-fun liftprj_const T = Const (@{const_name liftprj}, udomT ->> mk_upT T)
-fun liftdefl_const T = Const (@{const_name liftdefl}, Term.itselfT T --> deflT)
+fun liftemb_const T = Const (@{const_name liftemb}, mk_upT T ->> mk_upT udomT)
+fun liftprj_const T = Const (@{const_name liftprj}, mk_upT udomT ->> mk_upT T)
+fun liftdefl_const T = Const (@{const_name liftdefl}, Term.itselfT T --> udeflT)
fun mk_u_map t =
let
@@ -68,7 +69,7 @@
fun mk_cast (t, x) =
capply_const (udomT, udomT)
- $ (capply_const (deflT, udomT ->> udomT) $ @{const cast} $ t)
+ $ (capply_const (deflT, udomT ->> udomT) $ @{term "cast :: udom defl -> udom -> udom"} $ t)
$ x
(* manipulating theorems *)
@@ -98,7 +99,7 @@
val tmp_ctxt = tmp_ctxt |> Variable.declare_constraints defl
val deflT = Term.fastype_of defl
- val _ = if deflT = @{typ "defl"} then ()
+ val _ = if deflT = @{typ "udom defl"} then ()
else error ("Not type defl: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT))
(*lhs*)
@@ -112,7 +113,7 @@
|> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
(*set*)
- val set = @{const defl_set} $ defl
+ val set = @{term "defl_set :: udom defl => udom => bool"} $ defl
(*pcpodef*)
val tac1 = rtac @{thm defl_set_bottom} 1
@@ -129,15 +130,13 @@
val defl_eqn = Logic.mk_equals (defl_const newT,
Abs ("x", Term.itselfT newT, defl))
val liftemb_eqn =
- Logic.mk_equals (liftemb_const newT,
- mk_cfcomp (@{term "udom_emb u_approx"}, mk_u_map (emb_const newT)))
+ Logic.mk_equals (liftemb_const newT, mk_u_map (emb_const newT))
val liftprj_eqn =
- Logic.mk_equals (liftprj_const newT,
- mk_cfcomp (mk_u_map (prj_const newT), @{term "udom_prj u_approx"}))
+ Logic.mk_equals (liftprj_const newT, mk_u_map (prj_const newT))
val liftdefl_eqn =
Logic.mk_equals (liftdefl_const newT,
Abs ("t", Term.itselfT newT,
- mk_capply (@{const u_defl}, defl_const newT $ Logic.mk_type newT)))
+ mk_capply (@{const pdefl}, defl_const newT $ Logic.mk_type newT)))
val name_def = Binding.suffix_name "_def" name
val emb_bind = (Binding.prefix_name "emb_" name_def, [])
@@ -149,7 +148,7 @@
(*instantiate class rep*)
val lthy = thy
- |> Class.instantiation ([full_tname], lhs_tfrees, @{sort liftdomain})
+ |> Class.instantiation ([full_tname], lhs_tfrees, @{sort domain})
val ((_, (_, emb_ldef)), lthy) =
Specification.definition (NONE, (emb_bind, emb_eqn)) lthy
val ((_, (_, prj_ldef)), lthy) =
@@ -178,7 +177,7 @@
liftemb_def, liftprj_def, liftdefl_def]
val thy = lthy
|> Class.prove_instantiation_instance
- (K (Tactic.rtac (@{thm typedef_liftdomain_class} OF typedef_thms) 1))
+ (K (Tactic.rtac (@{thm typedef_domain_class} OF typedef_thms) 1))
|> Local_Theory.exit_global
(*other theorems*)
--- a/src/HOL/HOLCF/Universal.thy Sun Dec 19 19:03:49 2010 +0100
+++ b/src/HOL/HOLCF/Universal.thy Sun Dec 19 17:39:20 2010 -0800
@@ -5,7 +5,7 @@
header {* A universal bifinite domain *}
theory Universal
-imports Completion Deflation Nat_Bijection
+imports Bifinite Completion Nat_Bijection
begin
subsection {* Basis for universal domain *}
@@ -287,11 +287,8 @@
text {* We use a locale to parameterize the construction over a chain
of approx functions on the type to be embedded. *}
-locale approx_chain =
- fixes approx :: "nat \<Rightarrow> 'a::pcpo \<rightarrow> 'a"
- assumes chain_approx [simp]: "chain (\<lambda>i. approx i)"
- assumes lub_approx [simp]: "(\<Squnion>i. approx i) = ID"
- assumes finite_deflation_approx: "\<And>i. finite_deflation (approx i)"
+locale bifinite_approx_chain = approx_chain +
+ constrains approx :: "nat \<Rightarrow> 'a::bifinite \<rightarrow> 'a"
begin
subsubsection {* Choosing a maximal element from a finite set *}
@@ -408,30 +405,6 @@
apply (simp add: choose_pos.simps)
done
-subsubsection {* Properties of approx function *}
-
-lemma deflation_approx: "deflation (approx i)"
-using finite_deflation_approx by (rule finite_deflation_imp_deflation)
-
-lemma approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
-using deflation_approx by (rule deflation.idem)
-
-lemma approx_below: "approx i\<cdot>x \<sqsubseteq> x"
-using deflation_approx by (rule deflation.below)
-
-lemma finite_range_approx: "finite (range (\<lambda>x. approx i\<cdot>x))"
-apply (rule finite_deflation.finite_range)
-apply (rule finite_deflation_approx)
-done
-
-lemma compact_approx: "compact (approx n\<cdot>x)"
-apply (rule finite_deflation.compact)
-apply (rule finite_deflation_approx)
-done
-
-lemma compact_eq_approx: "compact x \<Longrightarrow> \<exists>i. approx i\<cdot>x = x"
-by (rule admD2, simp_all)
-
subsubsection {* Compact basis take function *}
primrec
@@ -804,11 +777,8 @@
apply (rule ubasis_until_less)
done
-end
-
-sublocale approx_chain \<subseteq> compact_basis!:
- ideal_completion below Rep_compact_basis
- "approximants :: 'a \<Rightarrow> 'a compact_basis set"
+lemma ideal_completion:
+ "ideal_completion below Rep_compact_basis (approximants :: 'a \<Rightarrow> _)"
proof
fix w :: "'a"
show "below.ideal (approximants w)"
@@ -873,9 +843,23 @@
by (rule exI, rule inj_place)
qed
+end
+
+interpretation compact_basis!:
+ ideal_completion below Rep_compact_basis
+ "approximants :: 'a::bifinite \<Rightarrow> 'a compact_basis set"
+proof -
+ obtain a :: "nat \<Rightarrow> 'a \<rightarrow> 'a" where "approx_chain a"
+ using bifinite ..
+ hence "bifinite_approx_chain a"
+ unfolding bifinite_approx_chain_def .
+ thus "ideal_completion below Rep_compact_basis (approximants :: 'a \<Rightarrow> _)"
+ by (rule bifinite_approx_chain.ideal_completion)
+qed
+
subsubsection {* EP-pair from any bifinite domain into \emph{udom} *}
-context approx_chain begin
+context bifinite_approx_chain begin
definition
udom_emb :: "'a \<rightarrow> udom"
@@ -915,10 +899,11 @@
end
-abbreviation "udom_emb \<equiv> approx_chain.udom_emb"
-abbreviation "udom_prj \<equiv> approx_chain.udom_prj"
+abbreviation "udom_emb \<equiv> bifinite_approx_chain.udom_emb"
+abbreviation "udom_prj \<equiv> bifinite_approx_chain.udom_prj"
-lemmas ep_pair_udom = approx_chain.ep_pair_udom
+lemmas ep_pair_udom =
+ bifinite_approx_chain.ep_pair_udom [unfolded bifinite_approx_chain_def]
subsection {* Chain of approx functions for type \emph{udom} *}
@@ -1001,7 +986,7 @@
apply (simp add: ubasis_until_same ubasis_le_refl)
done
-lemma udom_approx: "approx_chain udom_approx"
+lemma udom_approx [simp]: "approx_chain udom_approx"
proof
show "chain (\<lambda>i. udom_approx i)"
by (rule chain_udom_approx)
@@ -1009,6 +994,9 @@
by (rule lub_udom_approx)
qed
+instance udom :: bifinite
+ by default (fast intro: udom_approx)
+
hide_const (open) node
end
--- a/src/HOL/HOLCF/UpperPD.thy Sun Dec 19 19:03:49 2010 +0100
+++ b/src/HOL/HOLCF/UpperPD.thy Sun Dec 19 17:39:20 2010 -0800
@@ -5,7 +5,7 @@
header {* Upper powerdomain *}
theory UpperPD
-imports CompactBasis
+imports Compact_Basis
begin
subsection {* Basis preorder *}
@@ -78,7 +78,7 @@
type_notation (xsymbols) upper_pd ("('(_')\<sharp>)")
-instantiation upper_pd :: ("domain") below
+instantiation upper_pd :: (bifinite) below
begin
definition
@@ -87,11 +87,11 @@
instance ..
end
-instance upper_pd :: ("domain") po
+instance upper_pd :: (bifinite) po
using type_definition_upper_pd below_upper_pd_def
by (rule upper_le.typedef_ideal_po)
-instance upper_pd :: ("domain") cpo
+instance upper_pd :: (bifinite) cpo
using type_definition_upper_pd below_upper_pd_def
by (rule upper_le.typedef_ideal_cpo)
@@ -110,7 +110,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 :: ("domain") pcpo
+instance upper_pd :: (bifinite) pcpo
by intro_classes (fast intro: upper_pd_minimal)
lemma inst_upper_pd_pcpo: "\<bottom> = upper_principal (PDUnit compact_bot)"
@@ -453,66 +453,21 @@
by (rule finite_range_imp_finite_fixes)
qed
-subsection {* Upper powerdomain is a domain *}
-
-definition
- upper_approx :: "nat \<Rightarrow> udom upper_pd \<rightarrow> udom upper_pd"
-where
- "upper_approx = (\<lambda>i. upper_map\<cdot>(udom_approx i))"
-
-lemma upper_approx: "approx_chain upper_approx"
-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"
-
-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"
-using upper_approx finite_deflation_upper_map
-unfolding upper_defl_def by (rule cast_defl_fun1)
-
-instantiation upper_pd :: ("domain") liftdomain
-begin
-
-definition
- "emb = udom_emb upper_approx oo upper_map\<cdot>emb"
-
-definition
- "prj = upper_map\<cdot>prj oo udom_prj upper_approx"
+subsection {* Upper powerdomain is bifinite *}
-definition
- "defl (t::'a upper_pd itself) = upper_defl\<cdot>DEFL('a)"
-
-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)"
+lemma approx_chain_upper_map:
+ assumes "approx_chain a"
+ shows "approx_chain (\<lambda>i. upper_map\<cdot>(a i))"
+ using assms unfolding approx_chain_def
+ by (simp add: lub_APP upper_map_ID finite_deflation_upper_map)
-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]
- by (intro ep_pair_comp ep_pair_upper_map ep_pair_emb_prj)
-next
- show "cast\<cdot>DEFL('a upper_pd) = emb oo (prj :: udom \<rightarrow> 'a upper_pd)"
- unfolding emb_upper_pd_def prj_upper_pd_def defl_upper_pd_def cast_upper_defl
- by (simp add: cast_DEFL oo_def cfun_eq_iff upper_map_map)
+instance upper_pd :: (bifinite) bifinite
+proof
+ show "\<exists>(a::nat \<Rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd). approx_chain a"
+ using bifinite [where 'a='a]
+ by (fast intro!: approx_chain_upper_map)
qed
-end
-
-lemma DEFL_upper: "DEFL('a upper_pd) = upper_defl\<cdot>DEFL('a)"
-by (rule defl_upper_pd_def)
-
-
subsection {* Join *}
definition
--- a/src/HOL/HOLCF/ex/Domain_Proofs.thy Sun Dec 19 19:03:49 2010 +0100
+++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy Sun Dec 19 17:39:20 2010 -0800
@@ -17,9 +17,6 @@
and 'a bar = Bar (lazy "'a baz \<rightarrow> tr")
and 'a baz = Baz (lazy "'a foo convex_pd \<rightarrow> tr")
-TODO: add another type parameter that is strict,
-to show the different handling of LIFTDEFL vs. DEFL.
-
*)
(********************************************************************)
@@ -30,30 +27,30 @@
definition
foo_bar_baz_deflF ::
- "defl \<rightarrow> defl \<times> defl \<times> defl \<rightarrow> defl \<times> defl \<times> defl"
+ "udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl"
where
"foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3).
- ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>t2))
- , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>t3)\<cdot>DEFL(tr))
- , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>t1))\<cdot>DEFL(tr)))))"
+ ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>a))\<cdot>(u_defl\<cdot>(pdefl\<cdot>t2)))
+ , u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>t3))\<cdot>DEFL(tr)))
+ , u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>(convex_defl\<cdot>t1)))\<cdot>DEFL(tr))))))"
lemma foo_bar_baz_deflF_beta:
"foo_bar_baz_deflF\<cdot>a\<cdot>t =
- ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>(fst (snd t))))
- , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(snd (snd t)))\<cdot>DEFL(tr))
- , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(fst t)))\<cdot>DEFL(tr)))"
+ ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>a))\<cdot>(u_defl\<cdot>(pdefl\<cdot>(fst (snd t)))))
+ , u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>(snd (snd t))))\<cdot>DEFL(tr)))
+ , u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>(convex_defl\<cdot>(fst t))))\<cdot>DEFL(tr))))"
unfolding foo_bar_baz_deflF_def
by (simp add: split_def)
text {* Individual type combinators are projected from the fixed point. *}
-definition foo_defl :: "defl \<rightarrow> defl"
+definition foo_defl :: "udom defl \<rightarrow> udom defl"
where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
-definition bar_defl :: "defl \<rightarrow> defl"
+definition bar_defl :: "udom defl \<rightarrow> udom defl"
where "bar_defl = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
-definition baz_defl :: "defl \<rightarrow> defl"
+definition baz_defl :: "udom defl \<rightarrow> udom defl"
where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
lemma defl_apply_thms:
@@ -65,13 +62,13 @@
text {* Unfold rules for each combinator. *}
lemma foo_defl_unfold:
- "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
+ "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>a))\<cdot>(u_defl\<cdot>(pdefl\<cdot>(bar_defl\<cdot>a))))"
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
-lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(baz_defl\<cdot>a))\<cdot>DEFL(tr))"
+lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>(baz_defl\<cdot>a)))\<cdot>DEFL(tr)))"
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
-lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a)))\<cdot>DEFL(tr))"
+lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a))))\<cdot>DEFL(tr)))"
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
text "The automation for the previous steps will be quite similar to
@@ -83,40 +80,40 @@
text {* Use @{text pcpodef} with the appropriate type combinator. *}
-pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>LIFTDEFL('a))"
+pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>DEFL('a))"
by (rule defl_set_bottom, rule adm_defl_set)
-pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>LIFTDEFL('a))"
+pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>DEFL('a))"
by (rule defl_set_bottom, rule adm_defl_set)
-pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>LIFTDEFL('a))"
+pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>DEFL('a))"
by (rule defl_set_bottom, rule adm_defl_set)
text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
-instantiation foo :: ("domain") liftdomain
+instantiation foo :: ("domain") "domain"
begin
definition emb_foo :: "'a foo \<rightarrow> udom"
where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)"
definition prj_foo :: "udom \<rightarrow> 'a foo"
-where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
+where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>DEFL('a))\<cdot>y))"
-definition defl_foo :: "'a foo itself \<Rightarrow> defl"
-where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>LIFTDEFL('a)"
+definition defl_foo :: "'a foo itself \<Rightarrow> udom defl"
+where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>DEFL('a)"
definition
- "(liftemb :: 'a foo u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
+ "(liftemb :: 'a foo u \<rightarrow> udom u) \<equiv> u_map\<cdot>emb"
definition
- "(liftprj :: udom \<rightarrow> 'a foo u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
+ "(liftprj :: udom u \<rightarrow> 'a foo u) \<equiv> u_map\<cdot>prj"
definition
- "liftdefl \<equiv> \<lambda>(t::'a foo itself). u_defl\<cdot>DEFL('a foo)"
+ "liftdefl \<equiv> \<lambda>(t::'a foo itself). pdefl\<cdot>DEFL('a foo)"
instance
-apply (rule typedef_liftdomain_class)
+apply (rule typedef_domain_class)
apply (rule type_definition_foo)
apply (rule below_foo_def)
apply (rule emb_foo_def)
@@ -129,29 +126,29 @@
end
-instantiation bar :: ("domain") liftdomain
+instantiation bar :: ("domain") "domain"
begin
definition emb_bar :: "'a bar \<rightarrow> udom"
where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)"
definition prj_bar :: "udom \<rightarrow> 'a bar"
-where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
+where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>DEFL('a))\<cdot>y))"
-definition defl_bar :: "'a bar itself \<Rightarrow> defl"
-where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>LIFTDEFL('a)"
+definition defl_bar :: "'a bar itself \<Rightarrow> udom defl"
+where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>DEFL('a)"
definition
- "(liftemb :: 'a bar u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
+ "(liftemb :: 'a bar u \<rightarrow> udom u) \<equiv> u_map\<cdot>emb"
definition
- "(liftprj :: udom \<rightarrow> 'a bar u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
+ "(liftprj :: udom u \<rightarrow> 'a bar u) \<equiv> u_map\<cdot>prj"
definition
- "liftdefl \<equiv> \<lambda>(t::'a bar itself). u_defl\<cdot>DEFL('a bar)"
+ "liftdefl \<equiv> \<lambda>(t::'a bar itself). pdefl\<cdot>DEFL('a bar)"
instance
-apply (rule typedef_liftdomain_class)
+apply (rule typedef_domain_class)
apply (rule type_definition_bar)
apply (rule below_bar_def)
apply (rule emb_bar_def)
@@ -164,29 +161,29 @@
end
-instantiation baz :: ("domain") liftdomain
+instantiation baz :: ("domain") "domain"
begin
definition emb_baz :: "'a baz \<rightarrow> udom"
where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)"
definition prj_baz :: "udom \<rightarrow> 'a baz"
-where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
+where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>DEFL('a))\<cdot>y))"
-definition defl_baz :: "'a baz itself \<Rightarrow> defl"
-where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>LIFTDEFL('a)"
+definition defl_baz :: "'a baz itself \<Rightarrow> udom defl"
+where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>DEFL('a)"
definition
- "(liftemb :: 'a baz u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
+ "(liftemb :: 'a baz u \<rightarrow> udom u) \<equiv> u_map\<cdot>emb"
definition
- "(liftprj :: udom \<rightarrow> 'a baz u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
+ "(liftprj :: udom u \<rightarrow> 'a baz u) \<equiv> u_map\<cdot>prj"
definition
- "liftdefl \<equiv> \<lambda>(t::'a baz itself). u_defl\<cdot>DEFL('a baz)"
+ "liftdefl \<equiv> \<lambda>(t::'a baz itself). pdefl\<cdot>DEFL('a baz)"
instance
-apply (rule typedef_liftdomain_class)
+apply (rule typedef_domain_class)
apply (rule type_definition_baz)
apply (rule below_baz_def)
apply (rule emb_baz_def)
@@ -201,17 +198,17 @@
text {* Prove DEFL rules using lemma @{text typedef_DEFL}. *}
-lemma DEFL_foo: "DEFL('a foo) = foo_defl\<cdot>LIFTDEFL('a)"
+lemma DEFL_foo: "DEFL('a foo) = foo_defl\<cdot>DEFL('a)"
apply (rule typedef_DEFL)
apply (rule defl_foo_def)
done
-lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>LIFTDEFL('a)"
+lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>DEFL('a)"
apply (rule typedef_DEFL)
apply (rule defl_bar_def)
done
-lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>LIFTDEFL('a)"
+lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>DEFL('a)"
apply (rule typedef_DEFL)
apply (rule defl_baz_def)
done
@@ -348,7 +345,7 @@
text {* Prove isodefl rules for all map functions simultaneously. *}
lemma isodefl_foo_bar_baz:
- assumes isodefl_d: "isodefl (u_map\<cdot>d) t"
+ assumes isodefl_d: "isodefl d t"
shows
"isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and>
isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and>
@@ -383,21 +380,21 @@
apply (rule isodefl_DEFL_imp_ID)
apply (subst DEFL_foo)
apply (rule isodefl_foo)
-apply (rule isodefl_LIFTDEFL)
+apply (rule isodefl_ID_DEFL)
done
lemma bar_map_ID: "bar_map\<cdot>ID = ID"
apply (rule isodefl_DEFL_imp_ID)
apply (subst DEFL_bar)
apply (rule isodefl_bar)
-apply (rule isodefl_LIFTDEFL)
+apply (rule isodefl_ID_DEFL)
done
lemma baz_map_ID: "baz_map\<cdot>ID = ID"
apply (rule isodefl_DEFL_imp_ID)
apply (subst DEFL_baz)
apply (rule isodefl_baz)
-apply (rule isodefl_LIFTDEFL)
+apply (rule isodefl_ID_DEFL)
done
(********************************************************************)
--- a/src/HOL/IsaMakefile Sun Dec 19 19:03:49 2010 +0100
+++ b/src/HOL/IsaMakefile Sun Dec 19 17:39:20 2010 -0800
@@ -1406,7 +1406,7 @@
HOLCF/Algebraic.thy \
HOLCF/Bifinite.thy \
HOLCF/Cfun.thy \
- HOLCF/CompactBasis.thy \
+ HOLCF/Compact_Basis.thy \
HOLCF/Completion.thy \
HOLCF/Cont.thy \
HOLCF/ConvexPD.thy \
@@ -1429,6 +1429,7 @@
HOLCF/Porder.thy \
HOLCF/Powerdomains.thy \
HOLCF/Product_Cpo.thy \
+ HOLCF/Representable.thy \
HOLCF/Sfun.thy \
HOLCF/Sprod.thy \
HOLCF/Ssum.thy \