--- a/src/HOLCF/Algebraic.thy Mon Oct 11 18:03:47 2010 +0700
+++ b/src/HOLCF/Algebraic.thy Mon Oct 11 07:09:42 2010 -0700
@@ -2,10 +2,10 @@
Author: Brian Huffman
*)
-header {* Algebraic deflations and SFP domains *}
+header {* Algebraic deflations *}
theory Algebraic
-imports Universal Bifinite
+imports Universal
begin
subsection {* Type constructor for finite deflations *}
@@ -99,23 +99,10 @@
using type_definition_sfp below_sfp_def
by (rule below.typedef_ideal_cpo)
-lemma Rep_sfp_lub:
- "chain Y \<Longrightarrow> Rep_sfp (\<Squnion>i. Y i) = (\<Union>i. Rep_sfp (Y i))"
-using type_definition_sfp below_sfp_def
-by (rule below.typedef_ideal_rep_contlub)
-
-lemma ideal_Rep_sfp: "below.ideal (Rep_sfp xs)"
-by (rule Rep_sfp [unfolded mem_Collect_eq])
-
definition
sfp_principal :: "fin_defl \<Rightarrow> sfp" where
"sfp_principal t = Abs_sfp {u. u \<sqsubseteq> t}"
-lemma Rep_sfp_principal:
- "Rep_sfp (sfp_principal t) = {u. u \<sqsubseteq> t}"
-unfolding sfp_principal_def
-by (simp add: Abs_sfp_inverse below.ideal_principal)
-
lemma fin_defl_countable: "\<exists>f::fin_defl \<Rightarrow> nat. inj f"
proof
have *: "\<And>d. finite (approx_chain.place udom_approx `
@@ -144,13 +131,9 @@
qed
interpretation sfp: ideal_completion below sfp_principal Rep_sfp
-apply default
-apply (rule ideal_Rep_sfp)
-apply (erule Rep_sfp_lub)
-apply (rule Rep_sfp_principal)
-apply (simp only: below_sfp_def)
-apply (rule fin_defl_countable)
-done
+using type_definition_sfp below_sfp_def
+using sfp_principal_def fin_defl_countable
+by (rule below.typedef_ideal_completion)
text {* Algebraic deflations are pointed *}
@@ -274,232 +257,4 @@
apply (simp add: in_sfp_def)
done
-subsection {* Class of SFP domains *}
-
-text {*
- We define a SFP domain as a pcpo that is isomorphic to some
- algebraic deflation over the universal domain.
-*}
-
-class sfp = pcpo +
- fixes emb :: "'a::pcpo \<rightarrow> udom"
- fixes prj :: "udom \<rightarrow> 'a::pcpo"
- fixes sfp :: "'a itself \<Rightarrow> sfp"
- assumes ep_pair_emb_prj: "ep_pair emb prj"
- assumes cast_SFP: "cast\<cdot>(sfp TYPE('a)) = emb oo prj"
-
-syntax "_SFP" :: "type \<Rightarrow> sfp" ("(1SFP/(1'(_')))")
-translations "SFP('t)" \<rightleftharpoons> "CONST sfp TYPE('t)"
-
-interpretation sfp:
- pcpo_ep_pair "emb :: 'a::sfp \<rightarrow> udom" "prj :: udom \<rightarrow> 'a::sfp"
- unfolding pcpo_ep_pair_def
- by (rule ep_pair_emb_prj)
-
-lemmas emb_inverse = sfp.e_inverse
-lemmas emb_prj_below = sfp.e_p_below
-lemmas emb_eq_iff = sfp.e_eq_iff
-lemmas emb_strict = sfp.e_strict
-lemmas prj_strict = sfp.p_strict
-
-subsection {* SFP domains have a countable compact basis *}
-
-text {*
- Eventually it should be possible to generalize this to an unpointed
- variant of the sfp class.
-*}
-
-interpretation compact_basis:
- ideal_completion below Rep_compact_basis "approximants::'a::sfp \<Rightarrow> _"
-proof -
- obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)"
- and SFP: "SFP('a) = (\<Squnion>i. sfp_principal (Y i))"
- by (rule sfp.obtain_principal_chain)
- def approx \<equiv> "\<lambda>i. (prj oo cast\<cdot>(sfp_principal (Y i)) oo emb) :: 'a \<rightarrow> 'a"
- interpret sfp_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 SFP [symmetric] cast_SFP expand_cfun_eq)
- show "\<And>i. finite_deflation (approx i)"
- unfolding approx_def
- apply (rule sfp.finite_deflation_p_d_e)
- apply (rule finite_deflation_cast)
- apply (rule sfp.compact_principal)
- apply (rule below_trans [OF monofun_cfun_fun])
- apply (rule is_ub_thelub, simp add: Y)
- apply (simp add: lub_distribs Y SFP [symmetric] cast_SFP)
- done
- qed
- (* FIXME: why does show ?thesis fail here? *)
- show "ideal_completion below Rep_compact_basis (approximants::'a \<Rightarrow> _)" ..
-qed
-
-subsection {* Type combinators *}
-
-definition
- sfp_fun1 ::
- "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (sfp \<rightarrow> sfp)"
-where
- "sfp_fun1 approx f =
- sfp.basis_fun (\<lambda>a.
- sfp_principal (Abs_fin_defl
- (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)))"
-
-definition
- sfp_fun2 ::
- "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a))
- \<Rightarrow> (sfp \<rightarrow> sfp \<rightarrow> sfp)"
-where
- "sfp_fun2 approx f =
- sfp.basis_fun (\<lambda>a.
- sfp.basis_fun (\<lambda>b.
- sfp_principal (Abs_fin_defl
- (udom_emb approx oo
- f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx))))"
-
-lemma cast_sfp_fun1:
- assumes approx: "approx_chain approx"
- assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)"
- shows "cast\<cdot>(sfp_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: sfp.principal_induct, simp)
- (simp only: sfp_fun1_def
- sfp.basis_fun_principal
- sfp.basis_fun_mono
- sfp.principal_mono
- Abs_fin_defl_mono [OF 1 1]
- monofun_cfun below_refl
- Rep_fin_defl_mono
- cast_sfp_principal
- Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
-qed
-
-lemma cast_sfp_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>(sfp_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: sfp.principal_induct2, simp, simp)
- (simp only: sfp_fun2_def
- sfp.basis_fun_principal
- sfp.basis_fun_mono
- sfp.principal_mono
- Abs_fin_defl_mono [OF 1 1]
- monofun_cfun below_refl
- Rep_fin_defl_mono
- cast_sfp_principal
- Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
-qed
-
-subsection {* Instance for universal domain type *}
-
-instantiation udom :: sfp
-begin
-
-definition [simp]:
- "emb = (ID :: udom \<rightarrow> udom)"
-
-definition [simp]:
- "prj = (ID :: udom \<rightarrow> udom)"
-
-definition
- "sfp (t::udom itself) = (\<Squnion>i. sfp_principal (Abs_fin_defl (udom_approx i)))"
-
-instance proof
- show "ep_pair emb (prj :: udom \<rightarrow> udom)"
- by (simp add: ep_pair.intro)
-next
- show "cast\<cdot>SFP(udom) = emb oo (prj :: udom \<rightarrow> udom)"
- unfolding sfp_udom_def
- apply (subst contlub_cfun_arg)
- apply (rule chainI)
- apply (rule sfp.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_sfp_principal)
- apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
- done
-qed
-
end
-
-subsection {* Instance for continuous function space *}
-
-definition
- cfun_approx :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom)"
-where
- "cfun_approx = (\<lambda>i. cfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
-
-lemma cfun_approx: "approx_chain cfun_approx"
-proof (rule approx_chain.intro)
- show "chain (\<lambda>i. cfun_approx i)"
- unfolding cfun_approx_def by simp
- show "(\<Squnion>i. cfun_approx i) = ID"
- unfolding cfun_approx_def
- by (simp add: lub_distribs cfun_map_ID)
- show "\<And>i. finite_deflation (cfun_approx i)"
- unfolding cfun_approx_def
- by (intro finite_deflation_cfun_map finite_deflation_udom_approx)
-qed
-
-definition cfun_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
-where "cfun_sfp = sfp_fun2 cfun_approx cfun_map"
-
-lemma cast_cfun_sfp:
- "cast\<cdot>(cfun_sfp\<cdot>A\<cdot>B) =
- udom_emb cfun_approx oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj cfun_approx"
-unfolding cfun_sfp_def
-apply (rule cast_sfp_fun2 [OF cfun_approx])
-apply (erule (1) finite_deflation_cfun_map)
-done
-
-instantiation cfun :: (sfp, sfp) sfp
-begin
-
-definition
- "emb = udom_emb cfun_approx oo cfun_map\<cdot>prj\<cdot>emb"
-
-definition
- "prj = cfun_map\<cdot>emb\<cdot>prj oo udom_prj cfun_approx"
-
-definition
- "sfp (t::('a \<rightarrow> 'b) itself) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
-
-instance proof
- show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
- unfolding emb_cfun_def prj_cfun_def
- using ep_pair_udom [OF cfun_approx]
- by (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj)
-next
- show "cast\<cdot>SFP('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
- unfolding emb_cfun_def prj_cfun_def sfp_cfun_def cast_cfun_sfp
- by (simp add: cast_SFP oo_def expand_cfun_eq cfun_map_map)
-qed
-
-end
-
-lemma SFP_cfun: "SFP('a::sfp \<rightarrow> 'b::sfp) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
-by (rule sfp_cfun_def)
-
-end
--- a/src/HOLCF/Bifinite.thy Mon Oct 11 18:03:47 2010 +0700
+++ b/src/HOLCF/Bifinite.thy Mon Oct 11 07:09:42 2010 -0700
@@ -2,172 +2,559 @@
Author: Brian Huffman
*)
-header {* Bifinite domains and approximation *}
+header {* Bifinite domains *}
theory Bifinite
-imports Deflation
+imports Algebraic Cprod Sprod Ssum Up Lift One Tr
begin
-subsection {* Map operator for product type *}
+subsection {* Class of bifinite domains *}
+
+text {*
+ We define a bifinite domain as a pcpo that is isomorphic to some
+ algebraic deflation over the universal domain.
+*}
+
+class bifinite = pcpo +
+ fixes emb :: "'a::pcpo \<rightarrow> udom"
+ fixes prj :: "udom \<rightarrow> 'a::pcpo"
+ fixes sfp :: "'a itself \<Rightarrow> sfp"
+ assumes ep_pair_emb_prj: "ep_pair emb prj"
+ assumes cast_SFP: "cast\<cdot>(sfp TYPE('a)) = emb oo prj"
-definition
- cprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
-where
- "cprod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))"
+syntax "_SFP" :: "type \<Rightarrow> sfp" ("(1SFP/(1'(_')))")
+translations "SFP('t)" \<rightleftharpoons> "CONST sfp TYPE('t)"
+
+interpretation bifinite:
+ pcpo_ep_pair "emb :: 'a::bifinite \<rightarrow> udom" "prj :: udom \<rightarrow> 'a::bifinite"
+ unfolding pcpo_ep_pair_def
+ by (rule ep_pair_emb_prj)
-lemma cprod_map_Pair [simp]: "cprod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
-unfolding cprod_map_def by simp
+lemmas emb_inverse = bifinite.e_inverse
+lemmas emb_prj_below = bifinite.e_p_below
+lemmas emb_eq_iff = bifinite.e_eq_iff
+lemmas emb_strict = bifinite.e_strict
+lemmas prj_strict = bifinite.p_strict
-lemma cprod_map_ID: "cprod_map\<cdot>ID\<cdot>ID = ID"
-unfolding expand_cfun_eq by auto
+subsection {* Bifinite domains have a countable compact basis *}
-lemma cprod_map_map:
- "cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
- cprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
-by (induct p) simp
+text {*
+ Eventually it should be possible to generalize this to an unpointed
+ variant of the bifinite class.
+*}
-lemma ep_pair_cprod_map:
- assumes "ep_pair e1 p1" and "ep_pair e2 p2"
- shows "ep_pair (cprod_map\<cdot>e1\<cdot>e2) (cprod_map\<cdot>p1\<cdot>p2)"
-proof
- interpret e1p1: ep_pair e1 p1 by fact
- interpret e2p2: ep_pair e2 p2 by fact
- fix x show "cprod_map\<cdot>p1\<cdot>p2\<cdot>(cprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
- by (induct x) simp
- fix y show "cprod_map\<cdot>e1\<cdot>e2\<cdot>(cprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
- by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below)
+interpretation compact_basis:
+ ideal_completion below Rep_compact_basis "approximants::'a::bifinite \<Rightarrow> _"
+proof -
+ obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)"
+ and SFP: "SFP('a) = (\<Squnion>i. sfp_principal (Y i))"
+ by (rule sfp.obtain_principal_chain)
+ def approx \<equiv> "\<lambda>i. (prj oo cast\<cdot>(sfp_principal (Y i)) oo emb) :: 'a \<rightarrow> 'a"
+ interpret sfp_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 SFP [symmetric] cast_SFP expand_cfun_eq)
+ show "\<And>i. finite_deflation (approx i)"
+ unfolding approx_def
+ apply (rule bifinite.finite_deflation_p_d_e)
+ apply (rule finite_deflation_cast)
+ apply (rule sfp.compact_principal)
+ apply (rule below_trans [OF monofun_cfun_fun])
+ apply (rule is_ub_thelub, simp add: Y)
+ apply (simp add: lub_distribs Y SFP [symmetric] cast_SFP)
+ done
+ qed
+ (* FIXME: why does show ?thesis fail here? *)
+ show "ideal_completion below Rep_compact_basis (approximants::'a \<Rightarrow> _)" ..
qed
-lemma deflation_cprod_map:
- assumes "deflation d1" and "deflation d2"
- shows "deflation (cprod_map\<cdot>d1\<cdot>d2)"
-proof
- interpret d1: deflation d1 by fact
- interpret d2: deflation d2 by fact
- fix x
- show "cprod_map\<cdot>d1\<cdot>d2\<cdot>(cprod_map\<cdot>d1\<cdot>d2\<cdot>x) = cprod_map\<cdot>d1\<cdot>d2\<cdot>x"
- by (induct x) (simp add: d1.idem d2.idem)
- show "cprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
- by (induct x) (simp add: d1.below d2.below)
-qed
+subsection {* Type combinators *}
+
+definition
+ sfp_fun1 ::
+ "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (sfp \<rightarrow> sfp)"
+where
+ "sfp_fun1 approx f =
+ sfp.basis_fun (\<lambda>a.
+ sfp_principal (Abs_fin_defl
+ (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)))"
+
+definition
+ sfp_fun2 ::
+ "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a))
+ \<Rightarrow> (sfp \<rightarrow> sfp \<rightarrow> sfp)"
+where
+ "sfp_fun2 approx f =
+ sfp.basis_fun (\<lambda>a.
+ sfp.basis_fun (\<lambda>b.
+ sfp_principal (Abs_fin_defl
+ (udom_emb approx oo
+ f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx))))"
-lemma finite_deflation_cprod_map:
- assumes "finite_deflation d1" and "finite_deflation d2"
- shows "finite_deflation (cprod_map\<cdot>d1\<cdot>d2)"
-proof (rule finite_deflation_intro)
- interpret d1: finite_deflation d1 by fact
- interpret d2: finite_deflation d2 by fact
- have "deflation d1" and "deflation d2" by fact+
- thus "deflation (cprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_cprod_map)
- have "{p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}"
- by clarsimp
- thus "finite {p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p}"
- by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
+lemma cast_sfp_fun1:
+ assumes approx: "approx_chain approx"
+ assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)"
+ shows "cast\<cdot>(sfp_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: sfp.principal_induct, simp)
+ (simp only: sfp_fun1_def
+ sfp.basis_fun_principal
+ sfp.basis_fun_mono
+ sfp.principal_mono
+ Abs_fin_defl_mono [OF 1 1]
+ monofun_cfun below_refl
+ Rep_fin_defl_mono
+ cast_sfp_principal
+ Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
qed
-subsection {* Map operator for continuous function space *}
+lemma cast_sfp_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>(sfp_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: sfp.principal_induct2, simp, simp)
+ (simp only: sfp_fun2_def
+ sfp.basis_fun_principal
+ sfp.basis_fun_mono
+ sfp.principal_mono
+ Abs_fin_defl_mono [OF 1 1]
+ monofun_cfun below_refl
+ Rep_fin_defl_mono
+ cast_sfp_principal
+ Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
+qed
+
+subsection {* The universal domain is bifinite *}
+
+instantiation udom :: bifinite
+begin
+
+definition [simp]:
+ "emb = (ID :: udom \<rightarrow> udom)"
+
+definition [simp]:
+ "prj = (ID :: udom \<rightarrow> udom)"
definition
- cfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)"
-where
- "cfun_map = (\<Lambda> a b f x. b\<cdot>(f\<cdot>(a\<cdot>x)))"
-
-lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))"
-unfolding cfun_map_def by simp
-
-lemma cfun_map_ID: "cfun_map\<cdot>ID\<cdot>ID = ID"
-unfolding expand_cfun_eq by simp
+ "sfp (t::udom itself) = (\<Squnion>i. sfp_principal (Abs_fin_defl (udom_approx i)))"
-lemma cfun_map_map:
- "cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
- cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
-by (rule ext_cfun) simp
-
-lemma ep_pair_cfun_map:
- assumes "ep_pair e1 p1" and "ep_pair e2 p2"
- shows "ep_pair (cfun_map\<cdot>p1\<cdot>e2) (cfun_map\<cdot>e1\<cdot>p2)"
-proof
- interpret e1p1: ep_pair e1 p1 by fact
- interpret e2p2: ep_pair e2 p2 by fact
- fix f show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
- by (simp add: expand_cfun_eq)
- fix g show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
- apply (rule below_cfun_ext, simp)
- apply (rule below_trans [OF e2p2.e_p_below])
- apply (rule monofun_cfun_arg)
- apply (rule e1p1.e_p_below)
+instance proof
+ show "ep_pair emb (prj :: udom \<rightarrow> udom)"
+ by (simp add: ep_pair.intro)
+next
+ show "cast\<cdot>SFP(udom) = emb oo (prj :: udom \<rightarrow> udom)"
+ unfolding sfp_udom_def
+ apply (subst contlub_cfun_arg)
+ apply (rule chainI)
+ apply (rule sfp.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_sfp_principal)
+ apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
done
qed
-lemma deflation_cfun_map:
- assumes "deflation d1" and "deflation d2"
- shows "deflation (cfun_map\<cdot>d1\<cdot>d2)"
+end
+
+subsection {* Continuous function space is a bifinite domain *}
+
+definition
+ cfun_approx :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom)"
+where
+ "cfun_approx = (\<lambda>i. cfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+
+lemma cfun_approx: "approx_chain cfun_approx"
+proof (rule approx_chain.intro)
+ show "chain (\<lambda>i. cfun_approx i)"
+ unfolding cfun_approx_def by simp
+ show "(\<Squnion>i. cfun_approx i) = ID"
+ unfolding cfun_approx_def
+ by (simp add: lub_distribs cfun_map_ID)
+ show "\<And>i. finite_deflation (cfun_approx i)"
+ unfolding cfun_approx_def
+ by (intro finite_deflation_cfun_map finite_deflation_udom_approx)
+qed
+
+definition cfun_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
+where "cfun_sfp = sfp_fun2 cfun_approx cfun_map"
+
+lemma cast_cfun_sfp:
+ "cast\<cdot>(cfun_sfp\<cdot>A\<cdot>B) =
+ udom_emb cfun_approx oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj cfun_approx"
+unfolding cfun_sfp_def
+apply (rule cast_sfp_fun2 [OF cfun_approx])
+apply (erule (1) finite_deflation_cfun_map)
+done
+
+instantiation cfun :: (bifinite, bifinite) bifinite
+begin
+
+definition
+ "emb = udom_emb cfun_approx oo cfun_map\<cdot>prj\<cdot>emb"
+
+definition
+ "prj = cfun_map\<cdot>emb\<cdot>prj oo udom_prj cfun_approx"
+
+definition
+ "sfp (t::('a \<rightarrow> 'b) itself) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+
+instance proof
+ show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
+ unfolding emb_cfun_def prj_cfun_def
+ using ep_pair_udom [OF cfun_approx]
+ by (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj)
+next
+ show "cast\<cdot>SFP('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
+ unfolding emb_cfun_def prj_cfun_def sfp_cfun_def cast_cfun_sfp
+ by (simp add: cast_SFP oo_def expand_cfun_eq cfun_map_map)
+qed
+
+end
+
+lemma SFP_cfun:
+ "SFP('a::bifinite \<rightarrow> 'b::bifinite) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+by (rule sfp_cfun_def)
+
+subsection {* Cartesian product is a bifinite domain *}
+
+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))"
+
+lemma prod_approx: "approx_chain prod_approx"
+proof (rule approx_chain.intro)
+ show "chain (\<lambda>i. prod_approx i)"
+ unfolding prod_approx_def by simp
+ show "(\<Squnion>i. prod_approx i) = ID"
+ unfolding prod_approx_def
+ by (simp add: lub_distribs cprod_map_ID)
+ show "\<And>i. finite_deflation (prod_approx i)"
+ unfolding prod_approx_def
+ by (intro finite_deflation_cprod_map finite_deflation_udom_approx)
+qed
+
+definition prod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
+where "prod_sfp = sfp_fun2 prod_approx cprod_map"
+
+lemma cast_prod_sfp:
+ "cast\<cdot>(prod_sfp\<cdot>A\<cdot>B) = udom_emb prod_approx oo
+ cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj prod_approx"
+unfolding prod_sfp_def
+apply (rule cast_sfp_fun2 [OF prod_approx])
+apply (erule (1) finite_deflation_cprod_map)
+done
+
+instantiation prod :: (bifinite, bifinite) bifinite
+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
+ "sfp (t::('a \<times> 'b) itself) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('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>SFP('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
+ unfolding emb_prod_def prj_prod_def sfp_prod_def cast_prod_sfp
+ by (simp add: cast_SFP oo_def expand_cfun_eq cprod_map_map)
+qed
+
+end
+
+lemma SFP_prod:
+ "SFP('a::bifinite \<times> 'b::bifinite) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+by (rule sfp_prod_def)
+
+subsection {* Strict product is a bifinite domain *}
+
+definition
+ sprod_approx :: "nat \<Rightarrow> udom \<otimes> udom \<rightarrow> udom \<otimes> udom"
+where
+ "sprod_approx = (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+
+lemma sprod_approx: "approx_chain sprod_approx"
+proof (rule approx_chain.intro)
+ show "chain (\<lambda>i. sprod_approx i)"
+ unfolding sprod_approx_def by simp
+ show "(\<Squnion>i. sprod_approx i) = ID"
+ unfolding sprod_approx_def
+ by (simp add: lub_distribs sprod_map_ID)
+ show "\<And>i. finite_deflation (sprod_approx i)"
+ unfolding sprod_approx_def
+ by (intro finite_deflation_sprod_map finite_deflation_udom_approx)
+qed
+
+definition sprod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
+where "sprod_sfp = sfp_fun2 sprod_approx sprod_map"
+
+lemma cast_sprod_sfp:
+ "cast\<cdot>(sprod_sfp\<cdot>A\<cdot>B) =
+ udom_emb sprod_approx oo
+ sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo
+ udom_prj sprod_approx"
+unfolding sprod_sfp_def
+apply (rule cast_sfp_fun2 [OF sprod_approx])
+apply (erule (1) finite_deflation_sprod_map)
+done
+
+instantiation sprod :: (bifinite, bifinite) bifinite
+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
+ "sfp (t::('a \<otimes> 'b) itself) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+
+instance proof
+ 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>SFP('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
+ unfolding emb_sprod_def prj_sprod_def sfp_sprod_def cast_sprod_sfp
+ by (simp add: cast_SFP oo_def expand_cfun_eq sprod_map_map)
+qed
+
+end
+
+lemma SFP_sprod:
+ "SFP('a::bifinite \<otimes> 'b::bifinite) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+by (rule sfp_sprod_def)
+
+subsection {* Lifted cpo is a bifinite domain *}
+
+definition u_approx :: "nat \<Rightarrow> udom\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
+where "u_approx = (\<lambda>i. u_map\<cdot>(udom_approx i))"
+
+lemma u_approx: "approx_chain u_approx"
+proof (rule approx_chain.intro)
+ show "chain (\<lambda>i. u_approx i)"
+ unfolding u_approx_def by simp
+ show "(\<Squnion>i. u_approx i) = ID"
+ unfolding u_approx_def
+ by (simp add: lub_distribs u_map_ID)
+ show "\<And>i. finite_deflation (u_approx i)"
+ unfolding u_approx_def
+ by (intro finite_deflation_u_map finite_deflation_udom_approx)
+qed
+
+definition u_sfp :: "sfp \<rightarrow> sfp"
+where "u_sfp = sfp_fun1 u_approx u_map"
+
+lemma cast_u_sfp:
+ "cast\<cdot>(u_sfp\<cdot>A) =
+ udom_emb u_approx oo u_map\<cdot>(cast\<cdot>A) oo udom_prj u_approx"
+unfolding u_sfp_def
+apply (rule cast_sfp_fun1 [OF u_approx])
+apply (erule finite_deflation_u_map)
+done
+
+instantiation u :: (bifinite) bifinite
+begin
+
+definition
+ "emb = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "prj = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "sfp (t::'a u itself) = u_sfp\<cdot>SFP('a)"
+
+instance proof
+ show "ep_pair emb (prj :: udom \<rightarrow> 'a u)"
+ unfolding emb_u_def prj_u_def
+ using ep_pair_udom [OF u_approx]
+ by (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj)
+next
+ show "cast\<cdot>SFP('a u) = emb oo (prj :: udom \<rightarrow> 'a u)"
+ unfolding emb_u_def prj_u_def sfp_u_def cast_u_sfp
+ by (simp add: cast_SFP oo_def expand_cfun_eq u_map_map)
+qed
+
+end
+
+lemma SFP_u: "SFP('a::bifinite u) = u_sfp\<cdot>SFP('a)"
+by (rule sfp_u_def)
+
+subsection {* Lifted countable types are bifinite domains *}
+
+definition
+ lift_approx :: "nat \<Rightarrow> 'a::countable lift \<rightarrow> 'a lift"
+where
+ "lift_approx = (\<lambda>i. FLIFT x. if to_nat x < i then Def x else \<bottom>)"
+
+lemma chain_lift_approx [simp]: "chain lift_approx"
+ unfolding lift_approx_def
+ by (rule chainI, simp add: FLIFT_mono)
+
+lemma lub_lift_approx [simp]: "(\<Squnion>i. lift_approx i) = ID"
+apply (rule ext_cfun)
+apply (simp add: contlub_cfun_fun)
+apply (simp add: lift_approx_def)
+apply (case_tac x, simp)
+apply (rule thelubI)
+apply (rule is_lubI)
+apply (rule ub_rangeI, simp)
+apply (drule ub_rangeD)
+apply (erule rev_below_trans)
+apply simp
+apply (rule lessI)
+done
+
+lemma finite_deflation_lift_approx: "finite_deflation (lift_approx i)"
proof
- interpret d1: deflation d1 by fact
- interpret d2: deflation d2 by fact
- fix f
- show "cfun_map\<cdot>d1\<cdot>d2\<cdot>(cfun_map\<cdot>d1\<cdot>d2\<cdot>f) = cfun_map\<cdot>d1\<cdot>d2\<cdot>f"
- by (simp add: expand_cfun_eq d1.idem d2.idem)
- show "cfun_map\<cdot>d1\<cdot>d2\<cdot>f \<sqsubseteq> f"
- apply (rule below_cfun_ext, simp)
- apply (rule below_trans [OF d2.below])
- apply (rule monofun_cfun_arg)
- apply (rule d1.below)
+ fix x
+ show "lift_approx i\<cdot>x \<sqsubseteq> x"
+ unfolding lift_approx_def
+ by (cases x, simp, simp)
+ show "lift_approx i\<cdot>(lift_approx i\<cdot>x) = lift_approx i\<cdot>x"
+ unfolding lift_approx_def
+ by (cases x, simp, simp)
+ show "finite {x::'a lift. lift_approx i\<cdot>x = x}"
+ proof (rule finite_subset)
+ let ?S = "insert (\<bottom>::'a lift) (Def ` to_nat -` {..<i})"
+ show "{x::'a lift. lift_approx i\<cdot>x = x} \<subseteq> ?S"
+ unfolding lift_approx_def
+ by (rule subsetI, case_tac x, simp, simp split: split_if_asm)
+ show "finite ?S"
+ by (simp add: finite_vimageI)
+ qed
+qed
+
+lemma lift_approx: "approx_chain lift_approx"
+using chain_lift_approx lub_lift_approx finite_deflation_lift_approx
+by (rule approx_chain.intro)
+
+instantiation lift :: (countable) bifinite
+begin
+
+definition
+ "emb = udom_emb lift_approx"
+
+definition
+ "prj = udom_prj lift_approx"
+
+definition
+ "sfp (t::'a lift itself) =
+ (\<Squnion>i. sfp_principal (Abs_fin_defl (emb oo lift_approx i oo prj)))"
+
+instance proof
+ show ep: "ep_pair emb (prj :: udom \<rightarrow> 'a lift)"
+ unfolding emb_lift_def prj_lift_def
+ by (rule ep_pair_udom [OF lift_approx])
+ show "cast\<cdot>SFP('a lift) = emb oo (prj :: udom \<rightarrow> 'a lift)"
+ unfolding sfp_lift_def
+ apply (subst contlub_cfun_arg)
+ apply (rule chainI)
+ apply (rule sfp.principal_mono)
+ apply (simp add: below_fin_defl_def)
+ apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx
+ ep_pair.finite_deflation_e_d_p [OF ep])
+ apply (intro monofun_cfun below_refl)
+ apply (rule chainE)
+ apply (rule chain_lift_approx)
+ apply (subst cast_sfp_principal)
+ apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx
+ ep_pair.finite_deflation_e_d_p [OF ep] lub_distribs)
done
qed
-lemma finite_range_cfun_map:
- assumes a: "finite (range (\<lambda>x. a\<cdot>x))"
- assumes b: "finite (range (\<lambda>y. b\<cdot>y))"
- shows "finite (range (\<lambda>f. cfun_map\<cdot>a\<cdot>b\<cdot>f))" (is "finite (range ?h)")
-proof (rule finite_imageD)
- let ?f = "\<lambda>g. range (\<lambda>x. (a\<cdot>x, g\<cdot>x))"
- show "finite (?f ` range ?h)"
- proof (rule finite_subset)
- let ?B = "Pow (range (\<lambda>x. a\<cdot>x) \<times> range (\<lambda>y. b\<cdot>y))"
- show "?f ` range ?h \<subseteq> ?B"
- by clarsimp
- show "finite ?B"
- by (simp add: a b)
- qed
- show "inj_on ?f (range ?h)"
- proof (rule inj_onI, rule ext_cfun, clarsimp)
- fix x f g
- assume "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) = range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
- hence "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) \<subseteq> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
- by (rule equalityD1)
- hence "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) \<in> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
- by (simp add: subset_eq)
- then obtain y where "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) = (a\<cdot>y, b\<cdot>(g\<cdot>(a\<cdot>y)))"
- by (rule rangeE)
- thus "b\<cdot>(f\<cdot>(a\<cdot>x)) = b\<cdot>(g\<cdot>(a\<cdot>x))"
- by clarsimp
- qed
+end
+
+subsection {* Strict sum is a bifinite domain *}
+
+definition
+ ssum_approx :: "nat \<Rightarrow> udom \<oplus> udom \<rightarrow> udom \<oplus> udom"
+where
+ "ssum_approx = (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+
+lemma ssum_approx: "approx_chain ssum_approx"
+proof (rule approx_chain.intro)
+ show "chain (\<lambda>i. ssum_approx i)"
+ unfolding ssum_approx_def by simp
+ show "(\<Squnion>i. ssum_approx i) = ID"
+ unfolding ssum_approx_def
+ by (simp add: lub_distribs ssum_map_ID)
+ show "\<And>i. finite_deflation (ssum_approx i)"
+ unfolding ssum_approx_def
+ by (intro finite_deflation_ssum_map finite_deflation_udom_approx)
qed
-lemma finite_deflation_cfun_map:
- assumes "finite_deflation d1" and "finite_deflation d2"
- shows "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
-proof (rule finite_deflation_intro)
- interpret d1: finite_deflation d1 by fact
- interpret d2: finite_deflation d2 by fact
- have "deflation d1" and "deflation d2" by fact+
- thus "deflation (cfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_cfun_map)
- have "finite (range (\<lambda>f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f))"
- using d1.finite_range d2.finite_range
- by (rule finite_range_cfun_map)
- thus "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
- by (rule finite_range_imp_finite_fixes)
+definition ssum_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
+where "ssum_sfp = sfp_fun2 ssum_approx ssum_map"
+
+lemma cast_ssum_sfp:
+ "cast\<cdot>(ssum_sfp\<cdot>A\<cdot>B) =
+ udom_emb ssum_approx oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj ssum_approx"
+unfolding ssum_sfp_def
+apply (rule cast_sfp_fun2 [OF ssum_approx])
+apply (erule (1) finite_deflation_ssum_map)
+done
+
+instantiation ssum :: (bifinite, bifinite) bifinite
+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
+ "sfp (t::('a \<oplus> 'b) itself) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+
+instance proof
+ show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
+ unfolding emb_ssum_def prj_ssum_def
+ using ep_pair_udom [OF ssum_approx]
+ by (intro ep_pair_comp ep_pair_ssum_map ep_pair_emb_prj)
+next
+ show "cast\<cdot>SFP('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
+ unfolding emb_ssum_def prj_ssum_def sfp_ssum_def cast_ssum_sfp
+ by (simp add: cast_SFP oo_def expand_cfun_eq ssum_map_map)
qed
-text {* Finite deflations are compact elements of the function space *}
+end
-lemma finite_deflation_imp_compact: "finite_deflation d \<Longrightarrow> compact d"
-apply (frule finite_deflation_imp_deflation)
-apply (subgoal_tac "compact (cfun_map\<cdot>d\<cdot>d\<cdot>d)")
-apply (simp add: cfun_map_def deflation.idem eta_cfun)
-apply (rule finite_deflation.compact)
-apply (simp only: finite_deflation_cfun_map)
-done
+lemma SFP_ssum:
+ "SFP('a::bifinite \<oplus> 'b::bifinite) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+by (rule sfp_ssum_def)
end
--- a/src/HOLCF/Cfun.thy Mon Oct 11 18:03:47 2010 +0700
+++ b/src/HOLCF/Cfun.thy Mon Oct 11 07:09:42 2010 -0700
@@ -96,7 +96,6 @@
translations
"\<Lambda> _. t" => "CONST Abs_CFun (\<lambda> _. t)"
-
subsection {* Continuous function space is pointed *}
lemma UU_CFun: "\<bottom> \<in> CFun"
@@ -483,7 +482,6 @@
apply (erule minimal [THEN monofun_cfun_arg, THEN flat_eqI])
done
-
subsection {* Identity and composition *}
definition
@@ -530,6 +528,23 @@
lemma assoc_oo: "f oo (g oo h) = (f oo g) oo h"
by (rule ext_cfun, simp)
+subsection {* Map operator for continuous function space *}
+
+definition
+ cfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)"
+where
+ "cfun_map = (\<Lambda> a b f x. b\<cdot>(f\<cdot>(a\<cdot>x)))"
+
+lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))"
+unfolding cfun_map_def by simp
+
+lemma cfun_map_ID: "cfun_map\<cdot>ID\<cdot>ID = ID"
+unfolding expand_cfun_eq by simp
+
+lemma cfun_map_map:
+ "cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
+ cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
+by (rule ext_cfun) simp
subsection {* Strictified functions *}
--- a/src/HOLCF/CompactBasis.thy Mon Oct 11 18:03:47 2010 +0700
+++ b/src/HOLCF/CompactBasis.thy Mon Oct 11 07:09:42 2010 -0700
@@ -5,10 +5,10 @@
header {* A compact basis for powerdomains *}
theory CompactBasis
-imports Algebraic
+imports Bifinite
begin
-default_sort sfp
+default_sort bifinite
subsection {* A compact basis for powerdomains *}
@@ -24,7 +24,7 @@
text {* The powerdomain basis type is countable. *}
-lemma pd_basis_countable: "\<exists>f::'a::sfp pd_basis \<Rightarrow> nat. inj f"
+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 ..
@@ -108,26 +108,4 @@
by (simp add: image_Un fold1_Un2)
qed
-subsection {* Lemmas for proving if-and-only-if inequalities *}
-
-lemma chain_max_below_iff:
- assumes Y: "chain Y" shows "Y (max i j) \<sqsubseteq> x \<longleftrightarrow> Y i \<sqsubseteq> x \<and> Y j \<sqsubseteq> x"
-apply auto
-apply (erule below_trans [OF chain_mono [OF Y le_maxI1]])
-apply (erule below_trans [OF chain_mono [OF Y le_maxI2]])
-apply (simp add: max_def)
-done
-
-lemma all_ex_below_disj_iff:
- assumes "chain X" and "chain Y"
- shows "(\<forall>i. \<exists>j. X i \<sqsubseteq> Z j \<or> Y i \<sqsubseteq> Z j) \<longleftrightarrow>
- (\<forall>i. \<exists>j. X i \<sqsubseteq> Z j) \<or> (\<forall>i. \<exists>j. Y i \<sqsubseteq> Z j)"
-by (metis chain_max_below_iff assms)
-
-lemma all_ex_below_conj_iff:
- assumes "chain X" and "chain Y" and "chain Z"
- shows "(\<forall>i. \<exists>j. X i \<sqsubseteq> Z j \<and> Y i \<sqsubseteq> Z j) \<longleftrightarrow>
- (\<forall>i. \<exists>j. X i \<sqsubseteq> Z j) \<and> (\<forall>i. \<exists>j. Y i \<sqsubseteq> Z j)"
-oops
-
end
--- a/src/HOLCF/Completion.thy Mon Oct 11 18:03:47 2010 +0700
+++ b/src/HOLCF/Completion.thy Mon Oct 11 07:09:42 2010 -0700
@@ -40,17 +40,6 @@
"\<lbrakk>ideal A; x \<preceq> y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A"
unfolding ideal_def by fast
-lemma ideal_directed_finite:
- assumes A: "ideal A"
- shows "\<lbrakk>finite U; U \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. \<forall>x\<in>U. x \<preceq> z"
-apply (induct U set: finite)
-apply (simp add: idealD1 [OF A])
-apply (simp, clarify, rename_tac y)
-apply (drule (1) idealD2 [OF A])
-apply (clarify, erule_tac x=z in rev_bexI)
-apply (fast intro: r_trans)
-done
-
lemma ideal_principal: "ideal {x. x \<preceq> z}"
apply (rule idealI)
apply (rule_tac x=z in exI)
@@ -63,20 +52,6 @@
lemma ex_ideal: "\<exists>A. ideal A"
by (rule exI, rule ideal_principal)
-lemma directed_image_ideal:
- assumes A: "ideal A"
- assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y"
- shows "directed (f ` A)"
-apply (rule directedI)
-apply (cut_tac idealD1 [OF A], fast)
-apply (clarify, rename_tac a b)
-apply (drule (1) idealD2 [OF A])
-apply (clarify, rename_tac c)
-apply (rule_tac x="f c" in rev_bexI)
-apply (erule imageI)
-apply (simp add: f)
-done
-
lemma lub_image_principal:
assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y"
shows "(\<Squnion>x\<in>{x. x \<preceq> y}. f x) = f y"
@@ -227,10 +202,6 @@
"\<forall>i. Y i \<preceq> Y (Suc i) \<Longrightarrow> chain (\<lambda>i. principal (Y i))"
by (simp add: chainI principal_mono)
-lemma belowI: "(\<And>a. principal a \<sqsubseteq> x \<Longrightarrow> principal a \<sqsubseteq> u) \<Longrightarrow> x \<sqsubseteq> u"
-unfolding principal_below_iff_mem_rep
-by (simp add: below_def subset_eq)
-
lemma lub_principal_rep: "principal ` rep x <<| x"
apply (rule is_lubI)
apply (rule ub_imageI)
@@ -439,4 +410,26 @@
end
+lemma (in preorder) typedef_ideal_completion:
+ fixes Abs :: "'a set \<Rightarrow> 'b::cpo"
+ assumes type: "type_definition Rep Abs {S. ideal S}"
+ assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
+ assumes principal: "\<And>a. principal a = Abs {b. b \<preceq> a}"
+ assumes countable: "\<exists>f::'a \<Rightarrow> nat. inj f"
+ shows "ideal_completion r principal Rep"
+proof
+ interpret type_definition Rep Abs "{S. ideal S}" by fact
+ fix a b :: 'a and x y :: 'b and Y :: "nat \<Rightarrow> 'b"
+ show "ideal (Rep x)"
+ using Rep [of x] by simp
+ show "chain Y \<Longrightarrow> Rep (\<Squnion>i. Y i) = (\<Union>i. Rep (Y i))"
+ using type below by (rule typedef_ideal_rep_contlub)
+ show "Rep (principal a) = {b. b \<preceq> a}"
+ by (simp add: principal Abs_inverse ideal_principal)
+ show "Rep x \<subseteq> Rep y \<Longrightarrow> x \<sqsubseteq> y"
+ by (simp only: below)
+ show "\<exists>f::'a \<Rightarrow> nat. inj f"
+ by (rule countable)
+qed
+
end
--- a/src/HOLCF/ConvexPD.thy Mon Oct 11 18:03:47 2010 +0700
+++ b/src/HOLCF/ConvexPD.thy Mon Oct 11 07:09:42 2010 -0700
@@ -123,7 +123,7 @@
"{S::'a pd_basis set. convex_le.ideal S}"
by (fast intro: convex_le.ideal_principal)
-instantiation convex_pd :: (sfp) below
+instantiation convex_pd :: (bifinite) below
begin
definition
@@ -132,47 +132,30 @@
instance ..
end
-instance convex_pd :: (sfp) 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 :: (sfp) cpo
+instance convex_pd :: (bifinite) cpo
using type_definition_convex_pd below_convex_pd_def
by (rule convex_le.typedef_ideal_cpo)
-lemma Rep_convex_pd_lub:
- "chain Y \<Longrightarrow> Rep_convex_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_convex_pd (Y i))"
-using type_definition_convex_pd below_convex_pd_def
-by (rule convex_le.typedef_ideal_rep_contlub)
-
-lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_convex_pd xs)"
-by (rule Rep_convex_pd [unfolded mem_Collect_eq])
-
definition
convex_principal :: "'a pd_basis \<Rightarrow> 'a convex_pd" where
"convex_principal t = Abs_convex_pd {u. u \<le>\<natural> t}"
-lemma Rep_convex_principal:
- "Rep_convex_pd (convex_principal t) = {u. u \<le>\<natural> t}"
-unfolding convex_principal_def
-by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal)
-
interpretation convex_pd:
ideal_completion convex_le convex_principal Rep_convex_pd
-apply unfold_locales
-apply (rule ideal_Rep_convex_pd)
-apply (erule Rep_convex_pd_lub)
-apply (rule Rep_convex_principal)
-apply (simp only: below_convex_pd_def)
-apply (rule pd_basis_countable)
-done
+using type_definition_convex_pd below_convex_pd_def
+using convex_principal_def pd_basis_countable
+by (rule convex_le.typedef_ideal_completion)
text {* Convex powerdomain is pointed *}
lemma convex_pd_minimal: "convex_principal (PDUnit compact_bot) \<sqsubseteq> ys"
by (induct ys rule: convex_pd.principal_induct, simp, simp)
-instance convex_pd :: (sfp) 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)"
@@ -461,7 +444,7 @@
by (rule finite_range_imp_finite_fixes)
qed
-subsection {* Convex powerdomain is an SFP domain *}
+subsection {* Convex powerdomain is a bifinite domain *}
definition
convex_approx :: "nat \<Rightarrow> udom convex_pd \<rightarrow> udom convex_pd"
@@ -491,7 +474,7 @@
apply (erule finite_deflation_convex_map)
done
-instantiation convex_pd :: (sfp) sfp
+instantiation convex_pd :: (bifinite) bifinite
begin
definition
--- a/src/HOLCF/Cprod.thy Mon Oct 11 18:03:47 2010 +0700
+++ b/src/HOLCF/Cprod.thy Mon Oct 11 07:09:42 2010 -0700
@@ -5,7 +5,7 @@
header {* The cpo of cartesian products *}
theory Cprod
-imports Algebraic
+imports Deflation
begin
default_sort cpo
@@ -40,62 +40,61 @@
lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y"
by (simp add: csplit_def)
-subsection {* Cartesian product is an SFP domain *}
+subsection {* Map operator for product type *}
definition
- prod_approx :: "nat \<Rightarrow> udom \<times> udom \<rightarrow> udom \<times> udom"
+ cprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
where
- "prod_approx = (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+ "cprod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))"
+
+lemma cprod_map_Pair [simp]: "cprod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
+unfolding cprod_map_def by simp
+
+lemma cprod_map_ID: "cprod_map\<cdot>ID\<cdot>ID = ID"
+unfolding expand_cfun_eq by auto
-lemma prod_approx: "approx_chain prod_approx"
-proof (rule approx_chain.intro)
- show "chain (\<lambda>i. prod_approx i)"
- unfolding prod_approx_def by simp
- show "(\<Squnion>i. prod_approx i) = ID"
- unfolding prod_approx_def
- by (simp add: lub_distribs cprod_map_ID)
- show "\<And>i. finite_deflation (prod_approx i)"
- unfolding prod_approx_def
- by (intro finite_deflation_cprod_map finite_deflation_udom_approx)
+lemma cprod_map_map:
+ "cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
+ cprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
+by (induct p) simp
+
+lemma ep_pair_cprod_map:
+ assumes "ep_pair e1 p1" and "ep_pair e2 p2"
+ shows "ep_pair (cprod_map\<cdot>e1\<cdot>e2) (cprod_map\<cdot>p1\<cdot>p2)"
+proof
+ interpret e1p1: ep_pair e1 p1 by fact
+ interpret e2p2: ep_pair e2 p2 by fact
+ fix x show "cprod_map\<cdot>p1\<cdot>p2\<cdot>(cprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
+ by (induct x) simp
+ fix y show "cprod_map\<cdot>e1\<cdot>e2\<cdot>(cprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
+ by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below)
qed
-definition prod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
-where "prod_sfp = sfp_fun2 prod_approx cprod_map"
-
-lemma cast_prod_sfp:
- "cast\<cdot>(prod_sfp\<cdot>A\<cdot>B) = udom_emb prod_approx oo
- cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj prod_approx"
-unfolding prod_sfp_def
-apply (rule cast_sfp_fun2 [OF prod_approx])
-apply (erule (1) finite_deflation_cprod_map)
-done
-
-instantiation prod :: (sfp, sfp) sfp
-begin
+lemma deflation_cprod_map:
+ assumes "deflation d1" and "deflation d2"
+ shows "deflation (cprod_map\<cdot>d1\<cdot>d2)"
+proof
+ interpret d1: deflation d1 by fact
+ interpret d2: deflation d2 by fact
+ fix x
+ show "cprod_map\<cdot>d1\<cdot>d2\<cdot>(cprod_map\<cdot>d1\<cdot>d2\<cdot>x) = cprod_map\<cdot>d1\<cdot>d2\<cdot>x"
+ by (induct x) (simp add: d1.idem d2.idem)
+ show "cprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
+ by (induct x) (simp add: d1.below d2.below)
+qed
-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
- "sfp (t::('a \<times> 'b) itself) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('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>SFP('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
- unfolding emb_prod_def prj_prod_def sfp_prod_def cast_prod_sfp
- by (simp add: cast_SFP oo_def expand_cfun_eq cprod_map_map)
+lemma finite_deflation_cprod_map:
+ assumes "finite_deflation d1" and "finite_deflation d2"
+ shows "finite_deflation (cprod_map\<cdot>d1\<cdot>d2)"
+proof (rule finite_deflation_intro)
+ interpret d1: finite_deflation d1 by fact
+ interpret d2: finite_deflation d2 by fact
+ have "deflation d1" and "deflation d2" by fact+
+ thus "deflation (cprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_cprod_map)
+ have "{p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}"
+ by clarsimp
+ thus "finite {p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p}"
+ by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
qed
end
-
-lemma SFP_prod: "SFP('a::sfp \<times> 'b::sfp) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
-by (rule sfp_prod_def)
-
-end
--- a/src/HOLCF/Deflation.thy Mon Oct 11 18:03:47 2010 +0700
+++ b/src/HOLCF/Deflation.thy Mon Oct 11 07:09:42 2010 -0700
@@ -405,4 +405,93 @@
end
+subsection {* Map operator for continuous functions *}
+
+lemma ep_pair_cfun_map:
+ assumes "ep_pair e1 p1" and "ep_pair e2 p2"
+ shows "ep_pair (cfun_map\<cdot>p1\<cdot>e2) (cfun_map\<cdot>e1\<cdot>p2)"
+proof
+ interpret e1p1: ep_pair e1 p1 by fact
+ interpret e2p2: ep_pair e2 p2 by fact
+ fix f show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
+ by (simp add: expand_cfun_eq)
+ fix g show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
+ apply (rule below_cfun_ext, simp)
+ apply (rule below_trans [OF e2p2.e_p_below])
+ apply (rule monofun_cfun_arg)
+ apply (rule e1p1.e_p_below)
+ done
+qed
+
+lemma deflation_cfun_map:
+ assumes "deflation d1" and "deflation d2"
+ shows "deflation (cfun_map\<cdot>d1\<cdot>d2)"
+proof
+ interpret d1: deflation d1 by fact
+ interpret d2: deflation d2 by fact
+ fix f
+ show "cfun_map\<cdot>d1\<cdot>d2\<cdot>(cfun_map\<cdot>d1\<cdot>d2\<cdot>f) = cfun_map\<cdot>d1\<cdot>d2\<cdot>f"
+ by (simp add: expand_cfun_eq d1.idem d2.idem)
+ show "cfun_map\<cdot>d1\<cdot>d2\<cdot>f \<sqsubseteq> f"
+ apply (rule below_cfun_ext, simp)
+ apply (rule below_trans [OF d2.below])
+ apply (rule monofun_cfun_arg)
+ apply (rule d1.below)
+ done
+qed
+
+lemma finite_range_cfun_map:
+ assumes a: "finite (range (\<lambda>x. a\<cdot>x))"
+ assumes b: "finite (range (\<lambda>y. b\<cdot>y))"
+ shows "finite (range (\<lambda>f. cfun_map\<cdot>a\<cdot>b\<cdot>f))" (is "finite (range ?h)")
+proof (rule finite_imageD)
+ let ?f = "\<lambda>g. range (\<lambda>x. (a\<cdot>x, g\<cdot>x))"
+ show "finite (?f ` range ?h)"
+ proof (rule finite_subset)
+ let ?B = "Pow (range (\<lambda>x. a\<cdot>x) \<times> range (\<lambda>y. b\<cdot>y))"
+ show "?f ` range ?h \<subseteq> ?B"
+ by clarsimp
+ show "finite ?B"
+ by (simp add: a b)
+ qed
+ show "inj_on ?f (range ?h)"
+ proof (rule inj_onI, rule ext_cfun, clarsimp)
+ fix x f g
+ assume "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) = range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
+ hence "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) \<subseteq> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
+ by (rule equalityD1)
+ hence "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) \<in> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
+ by (simp add: subset_eq)
+ then obtain y where "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) = (a\<cdot>y, b\<cdot>(g\<cdot>(a\<cdot>y)))"
+ by (rule rangeE)
+ thus "b\<cdot>(f\<cdot>(a\<cdot>x)) = b\<cdot>(g\<cdot>(a\<cdot>x))"
+ by clarsimp
+ qed
+qed
+
+lemma finite_deflation_cfun_map:
+ assumes "finite_deflation d1" and "finite_deflation d2"
+ shows "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
+proof (rule finite_deflation_intro)
+ interpret d1: finite_deflation d1 by fact
+ interpret d2: finite_deflation d2 by fact
+ have "deflation d1" and "deflation d2" by fact+
+ thus "deflation (cfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_cfun_map)
+ have "finite (range (\<lambda>f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f))"
+ using d1.finite_range d2.finite_range
+ by (rule finite_range_cfun_map)
+ thus "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
+ by (rule finite_range_imp_finite_fixes)
+qed
+
+text {* Finite deflations are compact elements of the function space *}
+
+lemma finite_deflation_imp_compact: "finite_deflation d \<Longrightarrow> compact d"
+apply (frule finite_deflation_imp_deflation)
+apply (subgoal_tac "compact (cfun_map\<cdot>d\<cdot>d\<cdot>d)")
+apply (simp add: cfun_map_def deflation.idem eta_cfun)
+apply (rule finite_deflation.compact)
+apply (simp only: finite_deflation_cfun_map)
+done
+
end
--- a/src/HOLCF/Library/Strict_Fun.thy Mon Oct 11 18:03:47 2010 +0700
+++ b/src/HOLCF/Library/Strict_Fun.thy Mon Oct 11 07:09:42 2010 -0700
@@ -143,7 +143,7 @@
deflation_strict `deflation d1` `deflation d2`)
qed
-subsection {* Strict function space is an SFP domain *}
+subsection {* Strict function space is a bifinite domain *}
definition
sfun_approx :: "nat \<Rightarrow> (udom \<rightarrow>! udom) \<rightarrow> (udom \<rightarrow>! udom)"
@@ -173,7 +173,7 @@
apply (erule (1) finite_deflation_sfun_map)
done
-instantiation sfun :: (sfp, sfp) sfp
+instantiation sfun :: (bifinite, bifinite) bifinite
begin
definition
@@ -198,9 +198,8 @@
end
-text {* SFP of type constructor = type combinator *}
-
-lemma SFP_sfun: "SFP('a::sfp \<rightarrow>! 'b::sfp) = sfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+lemma SFP_sfun:
+ "SFP('a::bifinite \<rightarrow>! 'b::bifinite) = sfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
by (rule sfp_sfun_def)
lemma isodefl_sfun:
--- a/src/HOLCF/Lift.thy Mon Oct 11 18:03:47 2010 +0700
+++ b/src/HOLCF/Lift.thy Mon Oct 11 07:09:42 2010 -0700
@@ -170,90 +170,4 @@
lemma flift2_defined_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
by (cases x, simp_all)
-
-subsection {* Lifted countable types are SFP domains *}
-
-definition
- lift_approx :: "nat \<Rightarrow> 'a::countable lift \<rightarrow> 'a lift"
-where
- "lift_approx = (\<lambda>i. FLIFT x. if to_nat x < i then Def x else \<bottom>)"
-
-lemma chain_lift_approx [simp]: "chain lift_approx"
- unfolding lift_approx_def
- by (rule chainI, simp add: FLIFT_mono)
-
-lemma lub_lift_approx [simp]: "(\<Squnion>i. lift_approx i) = ID"
-apply (rule ext_cfun)
-apply (simp add: contlub_cfun_fun)
-apply (simp add: lift_approx_def)
-apply (case_tac x, simp)
-apply (rule thelubI)
-apply (rule is_lubI)
-apply (rule ub_rangeI, simp)
-apply (drule ub_rangeD)
-apply (erule rev_below_trans)
-apply simp
-apply (rule lessI)
-done
-
-lemma finite_deflation_lift_approx: "finite_deflation (lift_approx i)"
-proof
- fix x
- show "lift_approx i\<cdot>x \<sqsubseteq> x"
- unfolding lift_approx_def
- by (cases x, simp, simp)
- show "lift_approx i\<cdot>(lift_approx i\<cdot>x) = lift_approx i\<cdot>x"
- unfolding lift_approx_def
- by (cases x, simp, simp)
- show "finite {x::'a lift. lift_approx i\<cdot>x = x}"
- proof (rule finite_subset)
- let ?S = "insert (\<bottom>::'a lift) (Def ` to_nat -` {..<i})"
- show "{x::'a lift. lift_approx i\<cdot>x = x} \<subseteq> ?S"
- unfolding lift_approx_def
- by (rule subsetI, case_tac x, simp, simp split: split_if_asm)
- show "finite ?S"
- by (simp add: finite_vimageI)
- qed
-qed
-
-lemma lift_approx: "approx_chain lift_approx"
-using chain_lift_approx lub_lift_approx finite_deflation_lift_approx
-by (rule approx_chain.intro)
-
-instantiation lift :: (countable) sfp
-begin
-
-definition
- "emb = udom_emb lift_approx"
-
-definition
- "prj = udom_prj lift_approx"
-
-definition
- "sfp (t::'a lift itself) =
- (\<Squnion>i. sfp_principal (Abs_fin_defl (emb oo lift_approx i oo prj)))"
-
-instance proof
- show ep: "ep_pair emb (prj :: udom \<rightarrow> 'a lift)"
- unfolding emb_lift_def prj_lift_def
- by (rule ep_pair_udom [OF lift_approx])
- show "cast\<cdot>SFP('a lift) = emb oo (prj :: udom \<rightarrow> 'a lift)"
- unfolding sfp_lift_def
- apply (subst contlub_cfun_arg)
- apply (rule chainI)
- apply (rule sfp.principal_mono)
- apply (simp add: below_fin_defl_def)
- apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx
- ep_pair.finite_deflation_e_d_p [OF ep])
- apply (intro monofun_cfun below_refl)
- apply (rule chainE)
- apply (rule chain_lift_approx)
- apply (subst cast_sfp_principal)
- apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx
- ep_pair.finite_deflation_e_d_p [OF ep] lub_distribs)
- done
-qed
-
end
-
-end
--- a/src/HOLCF/LowerPD.thy Mon Oct 11 18:03:47 2010 +0700
+++ b/src/HOLCF/LowerPD.thy Mon Oct 11 07:09:42 2010 -0700
@@ -78,7 +78,7 @@
"{S::'a pd_basis set. lower_le.ideal S}"
by (fast intro: lower_le.ideal_principal)
-instantiation lower_pd :: (sfp) below
+instantiation lower_pd :: (bifinite) below
begin
definition
@@ -87,47 +87,30 @@
instance ..
end
-instance lower_pd :: (sfp) po
-by (rule lower_le.typedef_ideal_po
- [OF type_definition_lower_pd below_lower_pd_def])
-
-instance lower_pd :: (sfp) cpo
-by (rule lower_le.typedef_ideal_cpo
- [OF type_definition_lower_pd below_lower_pd_def])
+instance lower_pd :: (bifinite) po
+using type_definition_lower_pd below_lower_pd_def
+by (rule lower_le.typedef_ideal_po)
-lemma Rep_lower_pd_lub:
- "chain Y \<Longrightarrow> Rep_lower_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_lower_pd (Y i))"
-by (rule lower_le.typedef_ideal_rep_contlub
- [OF type_definition_lower_pd below_lower_pd_def])
-
-lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_lower_pd xs)"
-by (rule Rep_lower_pd [unfolded mem_Collect_eq])
+instance lower_pd :: (bifinite) cpo
+using type_definition_lower_pd below_lower_pd_def
+by (rule lower_le.typedef_ideal_cpo)
definition
lower_principal :: "'a pd_basis \<Rightarrow> 'a lower_pd" where
"lower_principal t = Abs_lower_pd {u. u \<le>\<flat> t}"
-lemma Rep_lower_principal:
- "Rep_lower_pd (lower_principal t) = {u. u \<le>\<flat> t}"
-unfolding lower_principal_def
-by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal)
-
interpretation lower_pd:
ideal_completion lower_le lower_principal Rep_lower_pd
-apply unfold_locales
-apply (rule ideal_Rep_lower_pd)
-apply (erule Rep_lower_pd_lub)
-apply (rule Rep_lower_principal)
-apply (simp only: below_lower_pd_def)
-apply (rule pd_basis_countable)
-done
+using type_definition_lower_pd below_lower_pd_def
+using lower_principal_def pd_basis_countable
+by (rule lower_le.typedef_ideal_completion)
text {* Lower powerdomain is pointed *}
lemma lower_pd_minimal: "lower_principal (PDUnit compact_bot) \<sqsubseteq> ys"
by (induct ys rule: lower_pd.principal_induct, simp, simp)
-instance lower_pd :: (sfp) 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)"
@@ -450,7 +433,7 @@
by (rule finite_range_imp_finite_fixes)
qed
-subsection {* Lower powerdomain is an SFP domain *}
+subsection {* Lower powerdomain is a bifinite domain *}
definition
lower_approx :: "nat \<Rightarrow> udom lower_pd \<rightarrow> udom lower_pd"
@@ -480,7 +463,7 @@
apply (erule finite_deflation_lower_map)
done
-instantiation lower_pd :: (sfp) sfp
+instantiation lower_pd :: (bifinite) bifinite
begin
definition
@@ -505,8 +488,6 @@
end
-text {* SFP of type constructor = type combinator *}
-
lemma SFP_lower: "SFP('a lower_pd) = lower_sfp\<cdot>SFP('a)"
by (rule sfp_lower_pd_def)
--- a/src/HOLCF/ROOT.ML Mon Oct 11 18:03:47 2010 +0700
+++ b/src/HOLCF/ROOT.ML Mon Oct 11 07:09:42 2010 -0700
@@ -4,6 +4,6 @@
HOLCF -- a semantic extension of HOL by the LCF logic.
*)
-no_document use_thys ["Nat_Bijection", "Infinite_Set", "Countable"];
+no_document use_thys ["Nat_Bijection", "Countable"];
use_thys ["HOLCF"];
--- a/src/HOLCF/Representable.thy Mon Oct 11 18:03:47 2010 +0700
+++ b/src/HOLCF/Representable.thy Mon Oct 11 07:09:42 2010 -0700
@@ -5,29 +5,29 @@
header {* Representable Types *}
theory Representable
-imports Algebraic Universal Ssum One Fixrec Domain_Aux
+imports Algebraic Bifinite Universal Ssum One Fixrec Domain_Aux
uses
("Tools/repdef.ML")
("Tools/Domain/domain_isomorphism.ML")
begin
-default_sort sfp
+default_sort bifinite
subsection {* Representations of types *}
-lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a::sfp) = cast\<cdot>SFP('a)\<cdot>x"
+lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a) = cast\<cdot>SFP('a)\<cdot>x"
by (simp add: cast_SFP)
lemma in_SFP_iff:
- "x ::: SFP('a::sfp) \<longleftrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
+ "x ::: SFP('a) \<longleftrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
by (simp add: in_sfp_def cast_SFP)
lemma prj_inverse:
- "x ::: SFP('a::sfp) \<Longrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
+ "x ::: SFP('a) \<Longrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
by (simp only: in_SFP_iff)
lemma emb_in_SFP [simp]:
- "emb\<cdot>(x::'a::sfp) ::: SFP('a)"
+ "emb\<cdot>(x::'a) ::: SFP('a)"
by (simp add: in_SFP_iff)
subsection {* Coerce operator *}
@@ -137,7 +137,7 @@
assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)"
assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))"
assumes sfp: "sfp \<equiv> (\<lambda> a::'a itself. t)"
- shows "OFCLASS('a, sfp_class)"
+ shows "OFCLASS('a, bifinite_class)"
proof
have adm: "adm (\<lambda>x. x \<in> {x. x ::: t})"
by (simp add: adm_in_sfp)
@@ -180,13 +180,13 @@
text {* Restore original typing constraints *}
setup {* Sign.add_const_constraint
- (@{const_name sfp}, SOME @{typ "'a::sfp itself \<Rightarrow> sfp"}) *}
+ (@{const_name sfp}, SOME @{typ "'a::bifinite itself \<Rightarrow> sfp"}) *}
setup {* Sign.add_const_constraint
- (@{const_name emb}, SOME @{typ "'a::sfp \<rightarrow> udom"}) *}
+ (@{const_name emb}, SOME @{typ "'a::bifinite \<rightarrow> udom"}) *}
setup {* Sign.add_const_constraint
- (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::sfp"}) *}
+ (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::bifinite"}) *}
lemma adm_mem_Collect_in_sfp: "adm (\<lambda>x. x \<in> {x. x ::: A})"
unfolding mem_Collect_eq by (rule adm_in_sfp)
@@ -196,7 +196,7 @@
subsection {* Isomorphic deflations *}
definition
- isodefl :: "('a::sfp \<rightarrow> 'a) \<Rightarrow> sfp \<Rightarrow> bool"
+ isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> sfp \<Rightarrow> bool"
where
"isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
@@ -211,7 +211,7 @@
by (drule cfun_fun_cong [where x="\<bottom>"], simp)
lemma isodefl_imp_deflation:
- fixes d :: "'a::sfp \<rightarrow> 'a"
+ fixes d :: "'a \<rightarrow> 'a"
assumes "isodefl d t" shows "deflation d"
proof
note assms [unfolded isodefl_def, simp]
--- a/src/HOLCF/Sprod.thy Mon Oct 11 18:03:47 2010 +0700
+++ b/src/HOLCF/Sprod.thy Mon Oct 11 07:09:42 2010 -0700
@@ -5,7 +5,7 @@
header {* The type of strict products *}
theory Sprod
-imports Algebraic
+imports Deflation
begin
default_sort pcpo
@@ -310,66 +310,4 @@
by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
qed
-subsection {* Strict product is an SFP domain *}
-
-definition
- sprod_approx :: "nat \<Rightarrow> udom \<otimes> udom \<rightarrow> udom \<otimes> udom"
-where
- "sprod_approx = (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
-
-lemma sprod_approx: "approx_chain sprod_approx"
-proof (rule approx_chain.intro)
- show "chain (\<lambda>i. sprod_approx i)"
- unfolding sprod_approx_def by simp
- show "(\<Squnion>i. sprod_approx i) = ID"
- unfolding sprod_approx_def
- by (simp add: lub_distribs sprod_map_ID)
- show "\<And>i. finite_deflation (sprod_approx i)"
- unfolding sprod_approx_def
- by (intro finite_deflation_sprod_map finite_deflation_udom_approx)
-qed
-
-definition sprod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
-where "sprod_sfp = sfp_fun2 sprod_approx sprod_map"
-
-lemma cast_sprod_sfp:
- "cast\<cdot>(sprod_sfp\<cdot>A\<cdot>B) =
- udom_emb sprod_approx oo
- sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo
- udom_prj sprod_approx"
-unfolding sprod_sfp_def
-apply (rule cast_sfp_fun2 [OF sprod_approx])
-apply (erule (1) finite_deflation_sprod_map)
-done
-
-instantiation sprod :: (sfp, sfp) sfp
-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
- "sfp (t::('a \<otimes> 'b) itself) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
-
-instance proof
- 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>SFP('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
- unfolding emb_sprod_def prj_sprod_def sfp_sprod_def cast_sprod_sfp
- by (simp add: cast_SFP oo_def expand_cfun_eq sprod_map_map)
-qed
-
end
-
-text {* SFP of type constructor = type combinator *}
-
-lemma SFP_sprod: "SFP('a::sfp \<otimes> 'b::sfp) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
-by (rule sfp_sprod_def)
-
-end
--- a/src/HOLCF/Ssum.thy Mon Oct 11 18:03:47 2010 +0700
+++ b/src/HOLCF/Ssum.thy Mon Oct 11 07:09:42 2010 -0700
@@ -295,64 +295,4 @@
by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
qed
-subsection {* Strict sum is an SFP domain *}
-
-definition
- ssum_approx :: "nat \<Rightarrow> udom \<oplus> udom \<rightarrow> udom \<oplus> udom"
-where
- "ssum_approx = (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
-
-lemma ssum_approx: "approx_chain ssum_approx"
-proof (rule approx_chain.intro)
- show "chain (\<lambda>i. ssum_approx i)"
- unfolding ssum_approx_def by simp
- show "(\<Squnion>i. ssum_approx i) = ID"
- unfolding ssum_approx_def
- by (simp add: lub_distribs ssum_map_ID)
- show "\<And>i. finite_deflation (ssum_approx i)"
- unfolding ssum_approx_def
- by (intro finite_deflation_ssum_map finite_deflation_udom_approx)
-qed
-
-definition ssum_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
-where "ssum_sfp = sfp_fun2 ssum_approx ssum_map"
-
-lemma cast_ssum_sfp:
- "cast\<cdot>(ssum_sfp\<cdot>A\<cdot>B) =
- udom_emb ssum_approx oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj ssum_approx"
-unfolding ssum_sfp_def
-apply (rule cast_sfp_fun2 [OF ssum_approx])
-apply (erule (1) finite_deflation_ssum_map)
-done
-
-instantiation ssum :: (sfp, sfp) sfp
-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
- "sfp (t::('a \<oplus> 'b) itself) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
-
-instance proof
- show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
- unfolding emb_ssum_def prj_ssum_def
- using ep_pair_udom [OF ssum_approx]
- by (intro ep_pair_comp ep_pair_ssum_map ep_pair_emb_prj)
-next
- show "cast\<cdot>SFP('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
- unfolding emb_ssum_def prj_ssum_def sfp_ssum_def cast_ssum_sfp
- by (simp add: cast_SFP oo_def expand_cfun_eq ssum_map_map)
-qed
-
end
-
-text {* SFP of type constructor = type combinator *}
-
-lemma SFP_ssum: "SFP('a::sfp \<oplus> 'b::sfp) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
-by (rule sfp_ssum_def)
-
-end
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Mon Oct 11 18:03:47 2010 +0700
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Mon Oct 11 07:09:42 2010 -0700
@@ -213,7 +213,7 @@
end;
fun pcpo_arg lazy = if lazy then @{sort cpo} else @{sort pcpo};
-fun rep_arg lazy = @{sort sfp};
+fun rep_arg lazy = @{sort bifinite};
val add_domain =
gen_add_domain Sign.certify_typ Domain_Axioms.add_axioms pcpo_arg;
--- a/src/HOLCF/Tools/repdef.ML Mon Oct 11 18:03:47 2010 +0700
+++ b/src/HOLCF/Tools/repdef.ML Mon Oct 11 07:09:42 2010 -0700
@@ -108,7 +108,7 @@
(*instantiate class rep*)
val lthy = thy
- |> Class.instantiation ([full_tname], lhs_tfrees, @{sort sfp});
+ |> Class.instantiation ([full_tname], lhs_tfrees, @{sort bifinite});
val ((_, (_, emb_ldef)), lthy) =
Specification.definition (NONE, (emb_bind, emb_eqn)) lthy;
val ((_, (_, prj_ldef)), lthy) =
--- a/src/HOLCF/Tutorial/New_Domain.thy Mon Oct 11 18:03:47 2010 +0700
+++ b/src/HOLCF/Tutorial/New_Domain.thy Mon Oct 11 07:09:42 2010 -0700
@@ -9,14 +9,14 @@
begin
text {*
- The definitional domain package only works with SFP domains,
- i.e. types in class @{text sfp}.
+ The definitional domain package only works with bifinite domains,
+ i.e. types in class @{text bifinite}.
*}
-default_sort sfp
+default_sort bifinite
text {*
- Provided that @{text sfp} is the default sort, the @{text new_domain}
+ Provided that @{text bifinite} is the default sort, the @{text new_domain}
package should work with any type definition supported by the old
domain package.
*}
--- a/src/HOLCF/Universal.thy Mon Oct 11 18:03:47 2010 +0700
+++ b/src/HOLCF/Universal.thy Mon Oct 11 07:09:42 2010 -0700
@@ -218,32 +218,18 @@
using type_definition_udom below_udom_def
by (rule udom.typedef_ideal_cpo)
-lemma Rep_udom_lub:
- "chain Y \<Longrightarrow> Rep_udom (\<Squnion>i. Y i) = (\<Union>i. Rep_udom (Y i))"
-using type_definition_udom below_udom_def
-by (rule udom.typedef_ideal_rep_contlub)
-
-lemma ideal_Rep_udom: "udom.ideal (Rep_udom xs)"
-by (rule Rep_udom [unfolded mem_Collect_eq])
-
definition
udom_principal :: "nat \<Rightarrow> udom" where
"udom_principal t = Abs_udom {u. ubasis_le u t}"
-lemma Rep_udom_principal:
- "Rep_udom (udom_principal t) = {u. ubasis_le u t}"
-unfolding udom_principal_def
-by (simp add: Abs_udom_inverse udom.ideal_principal)
+lemma ubasis_countable: "\<exists>f::ubasis \<Rightarrow> nat. inj f"
+by (rule exI, rule inj_on_id)
interpretation udom:
ideal_completion ubasis_le udom_principal Rep_udom
-apply unfold_locales
-apply (rule ideal_Rep_udom)
-apply (erule Rep_udom_lub)
-apply (rule Rep_udom_principal)
-apply (simp only: below_udom_def)
-apply (rule exI, rule inj_on_id)
-done
+using type_definition_udom below_udom_def
+using udom_principal_def ubasis_countable
+by (rule udom.typedef_ideal_completion)
text {* Universal domain is pointed *}
--- a/src/HOLCF/Up.thy Mon Oct 11 18:03:47 2010 +0700
+++ b/src/HOLCF/Up.thy Mon Oct 11 07:09:42 2010 -0700
@@ -5,7 +5,7 @@
header {* The type of lifted values *}
theory Up
-imports Algebraic
+imports Deflation
begin
default_sort cpo
@@ -332,62 +332,4 @@
by (rule finite_subset, simp add: d.finite_fixes)
qed
-subsection {* Lifted cpo is an SFP domain *}
-
-definition u_approx :: "nat \<Rightarrow> udom\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
-where "u_approx = (\<lambda>i. u_map\<cdot>(udom_approx i))"
-
-lemma u_approx: "approx_chain u_approx"
-proof (rule approx_chain.intro)
- show "chain (\<lambda>i. u_approx i)"
- unfolding u_approx_def by simp
- show "(\<Squnion>i. u_approx i) = ID"
- unfolding u_approx_def
- by (simp add: lub_distribs u_map_ID)
- show "\<And>i. finite_deflation (u_approx i)"
- unfolding u_approx_def
- by (intro finite_deflation_u_map finite_deflation_udom_approx)
-qed
-
-definition u_sfp :: "sfp \<rightarrow> sfp"
-where "u_sfp = sfp_fun1 u_approx u_map"
-
-lemma cast_u_sfp:
- "cast\<cdot>(u_sfp\<cdot>A) =
- udom_emb u_approx oo u_map\<cdot>(cast\<cdot>A) oo udom_prj u_approx"
-unfolding u_sfp_def
-apply (rule cast_sfp_fun1 [OF u_approx])
-apply (erule finite_deflation_u_map)
-done
-
-instantiation u :: (sfp) sfp
-begin
-
-definition
- "emb = udom_emb u_approx oo u_map\<cdot>emb"
-
-definition
- "prj = u_map\<cdot>prj oo udom_prj u_approx"
-
-definition
- "sfp (t::'a u itself) = u_sfp\<cdot>SFP('a)"
-
-instance proof
- show "ep_pair emb (prj :: udom \<rightarrow> 'a u)"
- unfolding emb_u_def prj_u_def
- using ep_pair_udom [OF u_approx]
- by (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj)
-next
- show "cast\<cdot>SFP('a u) = emb oo (prj :: udom \<rightarrow> 'a u)"
- unfolding emb_u_def prj_u_def sfp_u_def cast_u_sfp
- by (simp add: cast_SFP oo_def expand_cfun_eq u_map_map)
-qed
-
end
-
-text {* SFP of type constructor = type combinator *}
-
-lemma SFP_u: "SFP('a::sfp u) = u_sfp\<cdot>SFP('a)"
-by (rule sfp_u_def)
-
-end
--- a/src/HOLCF/UpperPD.thy Mon Oct 11 18:03:47 2010 +0700
+++ b/src/HOLCF/UpperPD.thy Mon Oct 11 07:09:42 2010 -0700
@@ -76,7 +76,7 @@
"{S::'a pd_basis set. upper_le.ideal S}"
by (fast intro: upper_le.ideal_principal)
-instantiation upper_pd :: (sfp) below
+instantiation upper_pd :: (bifinite) below
begin
definition
@@ -85,47 +85,30 @@
instance ..
end
-instance upper_pd :: (sfp) 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 :: (sfp) cpo
+instance upper_pd :: (bifinite) cpo
using type_definition_upper_pd below_upper_pd_def
by (rule upper_le.typedef_ideal_cpo)
-lemma Rep_upper_pd_lub:
- "chain Y \<Longrightarrow> Rep_upper_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_upper_pd (Y i))"
-using type_definition_upper_pd below_upper_pd_def
-by (rule upper_le.typedef_ideal_rep_contlub)
-
-lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_upper_pd xs)"
-by (rule Rep_upper_pd [unfolded mem_Collect_eq])
-
definition
upper_principal :: "'a pd_basis \<Rightarrow> 'a upper_pd" where
"upper_principal t = Abs_upper_pd {u. u \<le>\<sharp> t}"
-lemma Rep_upper_principal:
- "Rep_upper_pd (upper_principal t) = {u. u \<le>\<sharp> t}"
-unfolding upper_principal_def
-by (simp add: Abs_upper_pd_inverse upper_le.ideal_principal)
-
interpretation upper_pd:
ideal_completion upper_le upper_principal Rep_upper_pd
-apply unfold_locales
-apply (rule ideal_Rep_upper_pd)
-apply (erule Rep_upper_pd_lub)
-apply (rule Rep_upper_principal)
-apply (simp only: below_upper_pd_def)
-apply (rule pd_basis_countable)
-done
+using type_definition_upper_pd below_upper_pd_def
+using upper_principal_def pd_basis_countable
+by (rule upper_le.typedef_ideal_completion)
text {* Upper powerdomain is pointed *}
lemma upper_pd_minimal: "upper_principal (PDUnit compact_bot) \<sqsubseteq> ys"
by (induct ys rule: upper_pd.principal_induct, simp, simp)
-instance upper_pd :: (sfp) 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)"
@@ -445,7 +428,7 @@
by (rule finite_range_imp_finite_fixes)
qed
-subsection {* Upper powerdomain is an SFP domain *}
+subsection {* Upper powerdomain is a bifinite domain *}
definition
upper_approx :: "nat \<Rightarrow> udom upper_pd \<rightarrow> udom upper_pd"
@@ -475,7 +458,7 @@
apply (erule finite_deflation_upper_map)
done
-instantiation upper_pd :: (sfp) sfp
+instantiation upper_pd :: (bifinite) bifinite
begin
definition
@@ -500,8 +483,6 @@
end
-text {* SFP of type constructor = type combinator *}
-
lemma SFP_upper: "SFP('a upper_pd) = upper_sfp\<cdot>SFP('a)"
by (rule sfp_upper_pd_def)
--- a/src/HOLCF/ex/Domain_Proofs.thy Mon Oct 11 18:03:47 2010 +0700
+++ b/src/HOLCF/ex/Domain_Proofs.thy Mon Oct 11 07:09:42 2010 -0700
@@ -8,7 +8,7 @@
imports HOLCF
begin
-default_sort sfp
+default_sort bifinite
(*
@@ -93,7 +93,7 @@
text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
-instantiation foo :: (sfp) sfp
+instantiation foo :: (bifinite) bifinite
begin
definition emb_foo :: "'a foo \<rightarrow> udom"
@@ -116,7 +116,7 @@
end
-instantiation bar :: (sfp) sfp
+instantiation bar :: (bifinite) bifinite
begin
definition emb_bar :: "'a bar \<rightarrow> udom"
@@ -139,7 +139,7 @@
end
-instantiation baz :: (sfp) sfp
+instantiation baz :: (bifinite) bifinite
begin
definition emb_baz :: "'a baz \<rightarrow> udom"
--- a/src/HOLCF/ex/Powerdomain_ex.thy Mon Oct 11 18:03:47 2010 +0700
+++ b/src/HOLCF/ex/Powerdomain_ex.thy Mon Oct 11 07:09:42 2010 -0700
@@ -8,7 +8,7 @@
imports HOLCF
begin
-default_sort sfp
+default_sort bifinite
subsection {* Monadic sorting example *}