--- a/src/HOLCF/Bifinite.thy Thu Nov 05 11:36:30 2009 -0800
+++ b/src/HOLCF/Bifinite.thy Thu Nov 05 11:47:00 2009 -0800
@@ -106,21 +106,69 @@
subsection {* Instance for product type *}
+definition
+ cprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
+where
+ "cprod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))"
+
+lemma cprod_map_Pair [simp]: "cprod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
+unfolding cprod_map_def by simp
+
+lemma ep_pair_cprod_map:
+ assumes "ep_pair e1 p1" and "ep_pair e2 p2"
+ shows "ep_pair (cprod_map\<cdot>e1\<cdot>e2) (cprod_map\<cdot>p1\<cdot>p2)"
+proof
+ interpret e1p1: ep_pair e1 p1 by fact
+ interpret e2p2: ep_pair e2 p2 by fact
+ fix x show "cprod_map\<cdot>p1\<cdot>p2\<cdot>(cprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
+ by (induct x) simp
+ fix y show "cprod_map\<cdot>e1\<cdot>e2\<cdot>(cprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
+ by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below)
+qed
+
+lemma deflation_cprod_map:
+ assumes "deflation d1" and "deflation d2"
+ shows "deflation (cprod_map\<cdot>d1\<cdot>d2)"
+proof
+ interpret d1: deflation d1 by fact
+ interpret d2: deflation d2 by fact
+ fix x
+ show "cprod_map\<cdot>d1\<cdot>d2\<cdot>(cprod_map\<cdot>d1\<cdot>d2\<cdot>x) = cprod_map\<cdot>d1\<cdot>d2\<cdot>x"
+ by (induct x) (simp add: d1.idem d2.idem)
+ show "cprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
+ by (induct x) (simp add: d1.below d2.below)
+qed
+
+lemma finite_deflation_cprod_map:
+ assumes "finite_deflation d1" and "finite_deflation d2"
+ shows "finite_deflation (cprod_map\<cdot>d1\<cdot>d2)"
+proof (intro finite_deflation.intro finite_deflation_axioms.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
+
instantiation "*" :: (profinite, profinite) profinite
begin
-definition approx_prod_def:
- "approx = (\<lambda>n. \<Lambda> x. (approx n\<cdot>(fst x), approx n\<cdot>(snd x)))"
+definition
+ approx_prod_def:
+ "approx = (\<lambda>n. cprod_map\<cdot>(approx n)\<cdot>(approx n))"
instance proof
fix i :: nat and x :: "'a \<times> 'b"
show "chain (approx :: nat \<Rightarrow> 'a \<times> 'b \<rightarrow> 'a \<times> 'b)"
unfolding approx_prod_def by simp
show "(\<Squnion>i. approx i\<cdot>x) = x"
- unfolding approx_prod_def
+ unfolding approx_prod_def cprod_map_def
by (simp add: lub_distribs thelub_Pair)
show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
- unfolding approx_prod_def by simp
+ unfolding approx_prod_def cprod_map_def by simp
have "{x::'a \<times> 'b. approx i\<cdot>x = x} \<subseteq>
{x::'a. approx i\<cdot>x = x} \<times> {x::'b. approx i\<cdot>x = x}"
unfolding approx_prod_def by clarsimp
@@ -146,10 +194,51 @@
subsection {* Instance for continuous function space *}
-lemma finite_range_cfun_lemma:
+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 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. \<Lambda> x. b\<cdot>(f\<cdot>(a\<cdot>x))))" (is "finite (range ?h)")
+ 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)"
@@ -175,12 +264,27 @@
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 (intro finite_deflation.intro finite_deflation_axioms.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
+
instantiation "->" :: (profinite, profinite) profinite
begin
definition
approx_cfun_def:
- "approx = (\<lambda>n. \<Lambda> f x. approx n\<cdot>(f\<cdot>(approx n\<cdot>x)))"
+ "approx = (\<lambda>n. cfun_map\<cdot>(approx n)\<cdot>(approx n))"
instance proof
show "chain (approx :: nat \<Rightarrow> ('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow> 'b))"
@@ -188,19 +292,19 @@
next
fix x :: "'a \<rightarrow> 'b"
show "(\<Squnion>i. approx i\<cdot>x) = x"
- unfolding approx_cfun_def
+ unfolding approx_cfun_def cfun_map_def
by (simp add: lub_distribs eta_cfun)
next
fix i :: nat and x :: "'a \<rightarrow> 'b"
show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
- unfolding approx_cfun_def by simp
+ unfolding approx_cfun_def cfun_map_def by simp
next
fix i :: nat
show "finite {x::'a \<rightarrow> 'b. approx i\<cdot>x = x}"
- apply (rule finite_range_imp_finite_fixes)
- apply (simp add: approx_cfun_def)
- apply (intro finite_range_cfun_lemma finite_range_approx)
- done
+ unfolding approx_cfun_def
+ by (intro finite_deflation.finite_fixes
+ finite_deflation_cfun_map
+ finite_deflation_approx)
qed
end
--- a/src/HOLCF/Domain.thy Thu Nov 05 11:36:30 2009 -0800
+++ b/src/HOLCF/Domain.thy Thu Nov 05 11:47:00 2009 -0800
@@ -204,61 +204,11 @@
subsection {* Combinators for building copy functions *}
-definition
- cfun_fun :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)"
-where
- "cfun_fun = (\<Lambda> f g p. g oo p oo f)"
-
-definition
- ssum_fun :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd"
-where
- "ssum_fun = (\<Lambda> f g. sscase\<cdot>(sinl oo f)\<cdot>(sinr oo g))"
-
-definition
- sprod_fun :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<otimes> 'c \<rightarrow> 'b \<otimes> 'd"
-where
- "sprod_fun = (\<Lambda> f g. ssplit\<cdot>(\<Lambda> x y. (:f\<cdot>x, g\<cdot>y:)))"
-
-definition
- cprod_fun :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
-where
- "cprod_fun = (\<Lambda> f g. csplit\<cdot>(\<Lambda> x y. (f\<cdot>x, g\<cdot>y)))"
-
-definition
- u_fun :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u"
-where
- "u_fun = (\<Lambda> f. fup\<cdot>(up oo f))"
-
-lemma cfun_fun_strict: "b\<cdot>\<bottom> = \<bottom> \<Longrightarrow> cfun_fun\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>"
-unfolding cfun_fun_def expand_cfun_eq by simp
+lemmas domain_map_stricts =
+ ssum_map_strict sprod_map_strict u_map_strict
-lemma ssum_fun_strict: "ssum_fun\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>"
-unfolding ssum_fun_def by simp
-
-lemma sprod_fun_strict: "sprod_fun\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>"
-unfolding sprod_fun_def by simp
-
-lemma u_fun_strict: "u_fun\<cdot>a\<cdot>\<bottom> = \<bottom>"
-unfolding u_fun_def by simp
-
-lemma ssum_fun_sinl: "x \<noteq> \<bottom> \<Longrightarrow> ssum_fun\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"
-by (simp add: ssum_fun_def)
-
-lemma ssum_fun_sinr: "x \<noteq> \<bottom> \<Longrightarrow> ssum_fun\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
-by (simp add: ssum_fun_def)
-
-lemma sprod_fun_spair:
- "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_fun\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
-by (simp add: sprod_fun_def)
-
-lemma u_fun_up: "u_fun\<cdot>a\<cdot>(up\<cdot>x) = up\<cdot>(a\<cdot>x)"
-by (simp add: u_fun_def)
-
-lemmas domain_fun_stricts =
- ssum_fun_strict sprod_fun_strict u_fun_strict
-
-lemmas domain_fun_simps =
- ssum_fun_sinl ssum_fun_sinr sprod_fun_spair u_fun_up
+lemmas domain_map_simps =
+ ssum_map_sinl ssum_map_sinr sprod_map_spair u_map_up
subsection {* Installing the domain package *}
--- a/src/HOLCF/Sprod.thy Thu Nov 05 11:36:30 2009 -0800
+++ b/src/HOLCF/Sprod.thy Thu Nov 05 11:47:00 2009 -0800
@@ -131,6 +131,9 @@
lemma inst_sprod_pcpo2: "UU = (:UU,UU:)"
by simp
+lemma sprodE2: "(\<And>x y. p = (:x, y:) \<Longrightarrow> Q) \<Longrightarrow> Q"
+by (cases p, simp only: inst_sprod_pcpo2, simp)
+
subsection {* Properties of @{term sfst} and @{term ssnd} *}
lemma sfst_strict [simp]: "sfst\<cdot>\<bottom> = \<bottom>"
@@ -228,6 +231,68 @@
done
qed
+subsection {* Map function for strict products *}
+
+definition
+ sprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<otimes> 'c \<rightarrow> 'b \<otimes> 'd"
+where
+ "sprod_map = (\<Lambda> f g. ssplit\<cdot>(\<Lambda> x y. (:f\<cdot>x, g\<cdot>y:)))"
+
+lemma sprod_map_strict [simp]: "sprod_map\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>"
+unfolding sprod_map_def by simp
+
+lemma sprod_map_spair [simp]:
+ "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
+by (simp add: sprod_map_def)
+
+lemma ep_pair_sprod_map:
+ assumes "ep_pair e1 p1" and "ep_pair e2 p2"
+ shows "ep_pair (sprod_map\<cdot>e1\<cdot>e2) (sprod_map\<cdot>p1\<cdot>p2)"
+proof
+ interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact
+ interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact
+ fix x show "sprod_map\<cdot>p1\<cdot>p2\<cdot>(sprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
+ by (induct x) simp_all
+ fix y show "sprod_map\<cdot>e1\<cdot>e2\<cdot>(sprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
+ apply (induct y, simp)
+ apply (case_tac "p1\<cdot>x = \<bottom>", simp, case_tac "p2\<cdot>y = \<bottom>", simp)
+ apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below)
+ done
+qed
+
+lemma deflation_sprod_map:
+ assumes "deflation d1" and "deflation d2"
+ shows "deflation (sprod_map\<cdot>d1\<cdot>d2)"
+proof
+ interpret d1: deflation d1 by fact
+ interpret d2: deflation d2 by fact
+ fix x
+ show "sprod_map\<cdot>d1\<cdot>d2\<cdot>(sprod_map\<cdot>d1\<cdot>d2\<cdot>x) = sprod_map\<cdot>d1\<cdot>d2\<cdot>x"
+ apply (induct x, simp)
+ apply (case_tac "d1\<cdot>x = \<bottom>", simp, case_tac "d2\<cdot>y = \<bottom>", simp)
+ apply (simp add: d1.idem d2.idem)
+ done
+ show "sprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
+ apply (induct x, simp)
+ apply (simp add: monofun_cfun d1.below d2.below)
+ done
+qed
+
+lemma finite_deflation_sprod_map:
+ assumes "finite_deflation d1" and "finite_deflation d2"
+ shows "finite_deflation (sprod_map\<cdot>d1\<cdot>d2)"
+proof (intro finite_deflation.intro finite_deflation_axioms.intro)
+ interpret d1: finite_deflation d1 by fact
+ interpret d2: finite_deflation d2 by fact
+ have "deflation d1" and "deflation d2" by fact+
+ thus "deflation (sprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_sprod_map)
+ have "{x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq> insert \<bottom>
+ ((\<lambda>(x, y). (:x, y:)) ` ({x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}))"
+ by (rule subsetI, case_tac x, auto simp add: spair_eq_iff)
+ thus "finite {x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x}"
+ by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
+qed
+
subsection {* Strict product is a bifinite domain *}
instantiation "**" :: (bifinite, bifinite) bifinite
@@ -235,35 +300,30 @@
definition
approx_sprod_def:
- "approx = (\<lambda>n. \<Lambda>(:x, y:). (:approx n\<cdot>x, approx n\<cdot>y:))"
+ "approx = (\<lambda>n. sprod_map\<cdot>(approx n)\<cdot>(approx n))"
instance proof
fix i :: nat and x :: "'a \<otimes> 'b"
show "chain (approx :: nat \<Rightarrow> 'a \<otimes> 'b \<rightarrow> 'a \<otimes> 'b)"
unfolding approx_sprod_def by simp
show "(\<Squnion>i. approx i\<cdot>x) = x"
- unfolding approx_sprod_def
+ unfolding approx_sprod_def sprod_map_def
by (simp add: lub_distribs eta_cfun)
show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
- unfolding approx_sprod_def
+ unfolding approx_sprod_def sprod_map_def
by (simp add: ssplit_def strictify_conv_if)
- have "Rep_Sprod ` {x::'a \<otimes> 'b. approx i\<cdot>x = x} \<subseteq> {x. approx i\<cdot>x = x}"
+ show "finite {x::'a \<otimes> 'b. approx i\<cdot>x = x}"
unfolding approx_sprod_def
- apply (clarify, case_tac x)
- apply (simp add: Rep_Sprod_strict)
- apply (simp add: Rep_Sprod_spair spair_eq_iff)
- done
- hence "finite (Rep_Sprod ` {x::'a \<otimes> 'b. approx i\<cdot>x = x})"
- using finite_fixes_approx by (rule finite_subset)
- thus "finite {x::'a \<otimes> 'b. approx i\<cdot>x = x}"
- by (rule finite_imageD, simp add: inj_on_def Rep_Sprod_inject)
+ by (intro finite_deflation.finite_fixes
+ finite_deflation_sprod_map
+ finite_deflation_approx)
qed
end
lemma approx_spair [simp]:
"approx i\<cdot>(:x, y:) = (:approx i\<cdot>x, approx i\<cdot>y:)"
-unfolding approx_sprod_def
+unfolding approx_sprod_def sprod_map_def
by (simp add: ssplit_def strictify_conv_if)
end
--- a/src/HOLCF/Ssum.thy Thu Nov 05 11:36:30 2009 -0800
+++ b/src/HOLCF/Ssum.thy Thu Nov 05 11:47:00 2009 -0800
@@ -210,6 +210,72 @@
apply (case_tac y, simp_all add: flat_below_iff)
done
+subsection {* Map function for strict sums *}
+
+definition
+ ssum_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd"
+where
+ "ssum_map = (\<Lambda> f g. sscase\<cdot>(sinl oo f)\<cdot>(sinr oo g))"
+
+lemma ssum_map_strict [simp]: "ssum_map\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
+unfolding ssum_map_def by simp
+
+lemma ssum_map_sinl [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"
+unfolding ssum_map_def by simp
+
+lemma ssum_map_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
+unfolding ssum_map_def by simp
+
+lemma ep_pair_ssum_map:
+ assumes "ep_pair e1 p1" and "ep_pair e2 p2"
+ shows "ep_pair (ssum_map\<cdot>e1\<cdot>e2) (ssum_map\<cdot>p1\<cdot>p2)"
+proof
+ interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact
+ interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact
+ fix x show "ssum_map\<cdot>p1\<cdot>p2\<cdot>(ssum_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
+ by (induct x) simp_all
+ fix y show "ssum_map\<cdot>e1\<cdot>e2\<cdot>(ssum_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
+ apply (induct y, simp)
+ apply (case_tac "p1\<cdot>x = \<bottom>", simp, simp add: e1p1.e_p_below)
+ apply (case_tac "p2\<cdot>y = \<bottom>", simp, simp add: e2p2.e_p_below)
+ done
+qed
+
+lemma deflation_ssum_map:
+ assumes "deflation d1" and "deflation d2"
+ shows "deflation (ssum_map\<cdot>d1\<cdot>d2)"
+proof
+ interpret d1: deflation d1 by fact
+ interpret d2: deflation d2 by fact
+ fix x
+ show "ssum_map\<cdot>d1\<cdot>d2\<cdot>(ssum_map\<cdot>d1\<cdot>d2\<cdot>x) = ssum_map\<cdot>d1\<cdot>d2\<cdot>x"
+ apply (induct x, simp)
+ apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.idem)
+ apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.idem)
+ done
+ show "ssum_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
+ apply (induct x, simp)
+ apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.below)
+ apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.below)
+ done
+qed
+
+lemma finite_deflation_ssum_map:
+ assumes "finite_deflation d1" and "finite_deflation d2"
+ shows "finite_deflation (ssum_map\<cdot>d1\<cdot>d2)"
+proof (intro finite_deflation.intro finite_deflation_axioms.intro)
+ interpret d1: finite_deflation d1 by fact
+ interpret d2: finite_deflation d2 by fact
+ have "deflation d1" and "deflation d2" by fact+
+ thus "deflation (ssum_map\<cdot>d1\<cdot>d2)" by (rule deflation_ssum_map)
+ have "{x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq>
+ (\<lambda>x. sinl\<cdot>x) ` {x. d1\<cdot>x = x} \<union>
+ (\<lambda>x. sinr\<cdot>x) ` {x. d2\<cdot>x = x} \<union> {\<bottom>}"
+ by (rule subsetI, case_tac x, simp_all)
+ thus "finite {x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x}"
+ by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
+qed
+
subsection {* Strict sum is a bifinite domain *}
instantiation "++" :: (bifinite, bifinite) bifinite
@@ -217,7 +283,7 @@
definition
approx_ssum_def:
- "approx = (\<lambda>n. sscase\<cdot>(\<Lambda> x. sinl\<cdot>(approx n\<cdot>x))\<cdot>(\<Lambda> y. sinr\<cdot>(approx n\<cdot>y)))"
+ "approx = (\<lambda>n. ssum_map\<cdot>(approx n)\<cdot>(approx n))"
lemma approx_sinl [simp]: "approx i\<cdot>(sinl\<cdot>x) = sinl\<cdot>(approx i\<cdot>x)"
unfolding approx_ssum_def by (cases "x = \<bottom>") simp_all
@@ -231,16 +297,14 @@
unfolding approx_ssum_def by simp
show "(\<Squnion>i. approx i\<cdot>x) = x"
unfolding approx_ssum_def
- by (simp add: lub_distribs eta_cfun)
+ by (cases x, simp_all add: lub_distribs)
show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
by (cases x, simp add: approx_ssum_def, simp, simp)
- have "{x::'a \<oplus> 'b. approx i\<cdot>x = x} \<subseteq>
- (\<lambda>x. sinl\<cdot>x) ` {x. approx i\<cdot>x = x} \<union>
- (\<lambda>x. sinr\<cdot>x) ` {x. approx i\<cdot>x = x}"
- by (rule subsetI, case_tac x rule: ssumE2, simp, simp)
- thus "finite {x::'a \<oplus> 'b. approx i\<cdot>x = x}"
- by (rule finite_subset,
- intro finite_UnI finite_imageI finite_fixes_approx)
+ show "finite {x::'a \<oplus> 'b. approx i\<cdot>x = x}"
+ unfolding approx_ssum_def
+ by (intro finite_deflation.finite_fixes
+ finite_deflation_ssum_map
+ finite_deflation_approx)
qed
end
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML Thu Nov 05 11:36:30 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Thu Nov 05 11:47:00 2009 -0800
@@ -28,11 +28,11 @@
(* FIXME: use theory data for this *)
val copy_tab : string Symtab.table =
- Symtab.make [(@{type_name "->"}, @{const_name "cfun_fun"}),
- (@{type_name "++"}, @{const_name "ssum_fun"}),
- (@{type_name "**"}, @{const_name "sprod_fun"}),
- (@{type_name "*"}, @{const_name "cprod_fun"}),
- (@{type_name "u"}, @{const_name "u_fun"})];
+ Symtab.make [(@{type_name "->"}, @{const_name "cfun_map"}),
+ (@{type_name "++"}, @{const_name "ssum_map"}),
+ (@{type_name "**"}, @{const_name "sprod_map"}),
+ (@{type_name "*"}, @{const_name "cprod_map"}),
+ (@{type_name "u"}, @{const_name "u_map"})];
fun copy_of_dtyp r dt = if DatatypeAux.is_rec_type dt then copy r dt else ID
and copy r (DatatypeAux.DtRec i) = r i
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Nov 05 11:36:30 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Nov 05 11:47:00 2009 -0800
@@ -589,7 +589,7 @@
let
val _ = trace " Proving copy_strict...";
val goal = mk_trp (strict (dc_copy `% "f"));
- val rules = [abs_strict, rep_strict] @ @{thms domain_fun_stricts};
+ val rules = [abs_strict, rep_strict] @ @{thms domain_map_stricts};
val tacs = [asm_simp_tac (HOLCF_ss addsimps rules) 1];
in pg [ax_copy_def] goal (K tacs) end;
@@ -604,9 +604,9 @@
val rhs = con_app2 con one_rhs args;
val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
val args' = filter_out (fn a => is_rec a orelse is_lazy a) args;
- val stricts = abs_strict :: rep_strict :: @{thms domain_fun_stricts};
+ val stricts = abs_strict :: rep_strict :: @{thms domain_map_stricts};
fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args';
- val rules = [ax_abs_iso] @ @{thms domain_fun_simps};
+ val rules = [ax_abs_iso] @ @{thms domain_map_simps};
val tacs2 = [asm_simp_tac (HOLCF_ss addsimps rules) 1];
in pg (ax_copy_def::con_appls) goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
in
--- a/src/HOLCF/Up.thy Thu Nov 05 11:36:30 2009 -0800
+++ b/src/HOLCF/Up.thy Thu Nov 05 11:47:00 2009 -0800
@@ -290,6 +290,43 @@
lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
by (cases x, simp_all)
+subsection {* Map function for lifted cpo *}
+
+definition
+ u_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u"
+where
+ "u_map = (\<Lambda> f. fup\<cdot>(up oo f))"
+
+lemma u_map_strict [simp]: "u_map\<cdot>f\<cdot>\<bottom> = \<bottom>"
+unfolding u_map_def by simp
+
+lemma u_map_up [simp]: "u_map\<cdot>f\<cdot>(up\<cdot>x) = up\<cdot>(f\<cdot>x)"
+unfolding u_map_def by simp
+
+lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)"
+apply default
+apply (case_tac x, simp, simp add: ep_pair.e_inverse)
+apply (case_tac y, simp, simp add: ep_pair.e_p_below)
+done
+
+lemma deflation_u_map: "deflation d \<Longrightarrow> deflation (u_map\<cdot>d)"
+apply default
+apply (case_tac x, simp, simp add: deflation.idem)
+apply (case_tac x, simp, simp add: deflation.below)
+done
+
+lemma finite_deflation_u_map:
+ assumes "finite_deflation d" shows "finite_deflation (u_map\<cdot>d)"
+proof (intro finite_deflation.intro finite_deflation_axioms.intro)
+ interpret d: finite_deflation d by fact
+ have "deflation d" by fact
+ thus "deflation (u_map\<cdot>d)" by (rule deflation_u_map)
+ have "{x. u_map\<cdot>d\<cdot>x = x} \<subseteq> insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x. d\<cdot>x = x})"
+ by (rule subsetI, case_tac x, simp_all)
+ thus "finite {x. u_map\<cdot>d\<cdot>x = x}"
+ by (rule finite_subset, simp add: d.finite_fixes)
+qed
+
subsection {* Lifted cpo is a bifinite domain *}
instantiation u :: (profinite) bifinite
@@ -297,7 +334,7 @@
definition
approx_up_def:
- "approx = (\<lambda>n. fup\<cdot>(\<Lambda> x. up\<cdot>(approx n\<cdot>x)))"
+ "approx = (\<lambda>n. u_map\<cdot>(approx n))"
instance proof
fix i :: nat and x :: "'a u"
@@ -305,16 +342,15 @@
unfolding approx_up_def by simp
show "(\<Squnion>i. approx i\<cdot>x) = x"
unfolding approx_up_def
- by (simp add: lub_distribs eta_cfun)
+ by (induct x, simp, simp add: lub_distribs)
show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
unfolding approx_up_def
- by (induct x, simp, simp)
- have "{x::'a u. approx i\<cdot>x = x} \<subseteq>
- insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x::'a. approx i\<cdot>x = x})"
+ by (induct x) simp_all
+ show "finite {x::'a u. approx i\<cdot>x = x}"
unfolding approx_up_def
- by (rule subsetI, case_tac x, simp_all)
- thus "finite {x::'a u. approx i\<cdot>x = x}"
- by (rule finite_subset, simp add: finite_fixes_approx)
+ by (intro finite_deflation.finite_fixes
+ finite_deflation_u_map
+ finite_deflation_approx)
qed
end