--- a/src/HOL/HOLCF/Bifinite.thy Tue Nov 30 18:40:23 2010 +0100
+++ b/src/HOL/HOLCF/Bifinite.thy Tue Nov 30 14:01:25 2010 -0800
@@ -460,13 +460,13 @@
begin
definition
- "emb = (udom_emb sfun_approx oo sfun_map\<cdot>prj\<cdot>emb) oo encode_cfun"
+ "emb = emb oo encode_cfun"
definition
- "prj = decode_cfun oo (sfun_map\<cdot>emb\<cdot>prj oo udom_prj sfun_approx)"
+ "prj = decode_cfun oo prj"
definition
- "defl (t::('a \<rightarrow> 'b) itself) = sfun_defl\<cdot>DEFL('a u)\<cdot>DEFL('b)"
+ "defl (t::('a \<rightarrow> 'b) itself) = DEFL('a u \<rightarrow>! 'b)"
definition
"(liftemb :: ('a \<rightarrow> 'b) u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
@@ -484,108 +484,18 @@
by (rule ep_pair.intro, simp_all)
thus "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
unfolding emb_cfun_def prj_cfun_def
- apply (rule ep_pair_comp)
- apply (rule ep_pair_comp)
- apply (intro ep_pair_sfun_map ep_pair_emb_prj)
- apply (rule ep_pair_udom [OF sfun_approx])
- done
+ using ep_pair_emb_prj by (rule ep_pair_comp)
show "cast\<cdot>DEFL('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
- unfolding emb_cfun_def prj_cfun_def defl_cfun_def cast_sfun_defl
- by (simp add: cast_DEFL oo_def cfun_eq_iff sfun_map_map)
+ unfolding emb_cfun_def prj_cfun_def defl_cfun_def
+ by (simp add: cast_DEFL cfcomp1)
qed
end
lemma DEFL_cfun:
- "DEFL('a::predomain \<rightarrow> 'b::domain) = sfun_defl\<cdot>DEFL('a u)\<cdot>DEFL('b)"
+ "DEFL('a::predomain \<rightarrow> 'b::domain) = DEFL('a u \<rightarrow>! 'b)"
by (rule defl_cfun_def)
-subsubsection {* Cartesian product *}
-
-text {*
- Types @{typ "('a * 'b) u"} and @{typ "'a u \<otimes> 'b u"} are isomorphic.
-*}
-
-definition
- "encode_prod_u = (\<Lambda>(up\<cdot>(x, y)). (:up\<cdot>x, up\<cdot>y:))"
-
-definition
- "decode_prod_u = (\<Lambda>(:up\<cdot>x, up\<cdot>y:). up\<cdot>(x, y))"
-
-lemma decode_encode_prod_u [simp]: "decode_prod_u\<cdot>(encode_prod_u\<cdot>x) = x"
-unfolding encode_prod_u_def decode_prod_u_def
-by (case_tac x, simp, rename_tac y, case_tac y, simp)
-
-lemma encode_decode_prod_u [simp]: "encode_prod_u\<cdot>(decode_prod_u\<cdot>y) = y"
-unfolding encode_prod_u_def decode_prod_u_def
-apply (case_tac y, simp, rename_tac a b)
-apply (case_tac a, simp, case_tac b, simp, simp)
-done
-
-instantiation prod :: (predomain, predomain) predomain
-begin
-
-definition
- "liftemb =
- (udom_emb sprod_approx oo sprod_map\<cdot>emb\<cdot>emb) oo encode_prod_u"
-
-definition
- "liftprj =
- decode_prod_u oo (sprod_map\<cdot>prj\<cdot>prj oo udom_prj sprod_approx)"
-
-definition
- "liftdefl (t::('a \<times> 'b) itself) = sprod_defl\<cdot>DEFL('a u)\<cdot>DEFL('b u)"
-
-instance proof
- have "ep_pair encode_prod_u decode_prod_u"
- by (rule ep_pair.intro, simp_all)
- thus "ep_pair liftemb (liftprj :: udom \<rightarrow> ('a \<times> 'b) u)"
- unfolding liftemb_prod_def liftprj_prod_def
- apply (rule ep_pair_comp)
- apply (rule ep_pair_comp)
- apply (intro ep_pair_sprod_map ep_pair_emb_prj)
- apply (rule ep_pair_udom [OF sprod_approx])
- done
- show "cast\<cdot>LIFTDEFL('a \<times> 'b) = liftemb oo (liftprj :: udom \<rightarrow> ('a \<times> 'b) u)"
- unfolding liftemb_prod_def liftprj_prod_def liftdefl_prod_def
- by (simp add: cast_sprod_defl cast_DEFL cfcomp1 sprod_map_map)
-qed
-
-end
-
-instantiation prod :: ("domain", "domain") "domain"
-begin
-
-definition
- "emb = udom_emb prod_approx oo cprod_map\<cdot>emb\<cdot>emb"
-
-definition
- "prj = cprod_map\<cdot>prj\<cdot>prj oo udom_prj prod_approx"
-
-definition
- "defl (t::('a \<times> 'b) itself) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
-
-instance proof
- show "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)"
- unfolding emb_prod_def prj_prod_def
- using ep_pair_udom [OF prod_approx]
- by (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj)
-next
- show "cast\<cdot>DEFL('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
- unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl
- by (simp add: cast_DEFL oo_def cfun_eq_iff cprod_map_map)
-qed
-
-end
-
-lemma DEFL_prod:
- "DEFL('a::domain \<times> 'b::domain) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
-by (rule defl_prod_def)
-
-lemma LIFTDEFL_prod:
- "LIFTDEFL('a::predomain \<times> 'b::predomain) = sprod_defl\<cdot>DEFL('a u)\<cdot>DEFL('b u)"
-by (rule liftdefl_prod_def)
-
subsubsection {* Strict product *}
instantiation sprod :: ("domain", "domain") liftdomain
@@ -628,6 +538,86 @@
"DEFL('a::domain \<otimes> 'b::domain) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
by (rule defl_sprod_def)
+subsubsection {* Cartesian product *}
+
+text {*
+ Types @{typ "('a * 'b) u"} and @{typ "'a u \<otimes> 'b u"} are isomorphic.
+*}
+
+definition
+ "encode_prod_u = (\<Lambda>(up\<cdot>(x, y)). (:up\<cdot>x, up\<cdot>y:))"
+
+definition
+ "decode_prod_u = (\<Lambda>(:up\<cdot>x, up\<cdot>y:). up\<cdot>(x, y))"
+
+lemma decode_encode_prod_u [simp]: "decode_prod_u\<cdot>(encode_prod_u\<cdot>x) = x"
+unfolding encode_prod_u_def decode_prod_u_def
+by (case_tac x, simp, rename_tac y, case_tac y, simp)
+
+lemma encode_decode_prod_u [simp]: "encode_prod_u\<cdot>(decode_prod_u\<cdot>y) = y"
+unfolding encode_prod_u_def decode_prod_u_def
+apply (case_tac y, simp, rename_tac a b)
+apply (case_tac a, simp, case_tac b, simp, simp)
+done
+
+instantiation prod :: (predomain, predomain) predomain
+begin
+
+definition
+ "liftemb = emb oo encode_prod_u"
+
+definition
+ "liftprj = decode_prod_u oo prj"
+
+definition
+ "liftdefl (t::('a \<times> 'b) itself) = DEFL('a\<^sub>\<bottom> \<otimes> 'b\<^sub>\<bottom>)"
+
+instance proof
+ have "ep_pair encode_prod_u decode_prod_u"
+ by (rule ep_pair.intro, simp_all)
+ thus "ep_pair liftemb (liftprj :: udom \<rightarrow> ('a \<times> 'b) u)"
+ unfolding liftemb_prod_def liftprj_prod_def
+ using ep_pair_emb_prj by (rule ep_pair_comp)
+ show "cast\<cdot>LIFTDEFL('a \<times> 'b) = liftemb oo (liftprj :: udom \<rightarrow> ('a \<times> 'b) u)"
+ unfolding liftemb_prod_def liftprj_prod_def liftdefl_prod_def
+ by (simp add: cast_DEFL cfcomp1)
+qed
+
+end
+
+instantiation prod :: ("domain", "domain") "domain"
+begin
+
+definition
+ "emb = udom_emb prod_approx oo cprod_map\<cdot>emb\<cdot>emb"
+
+definition
+ "prj = cprod_map\<cdot>prj\<cdot>prj oo udom_prj prod_approx"
+
+definition
+ "defl (t::('a \<times> 'b) itself) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+
+instance proof
+ show "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)"
+ unfolding emb_prod_def prj_prod_def
+ using ep_pair_udom [OF prod_approx]
+ by (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj)
+next
+ show "cast\<cdot>DEFL('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
+ unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl
+ by (simp add: cast_DEFL oo_def cfun_eq_iff cprod_map_map)
+qed
+
+end
+
+lemma DEFL_prod:
+ "DEFL('a::domain \<times> 'b::domain) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+by (rule defl_prod_def)
+
+lemma LIFTDEFL_prod:
+ "LIFTDEFL('a::predomain \<times> 'b::predomain) = DEFL('a u \<otimes> 'b u)"
+by (rule liftdefl_prod_def)
+
subsubsection {* Discrete cpo *}
definition discr_approx :: "nat \<Rightarrow> 'a::countable discr u \<rightarrow> 'a discr u"
--- a/src/HOL/HOLCF/Domain.thy Tue Nov 30 18:40:23 2010 +0100
+++ b/src/HOL/HOLCF/Domain.thy Tue Nov 30 14:01:25 2010 -0800
@@ -293,11 +293,9 @@
lemma isodefl_cprod_u:
assumes "isodefl (u_map\<cdot>d1) t1" and "isodefl (u_map\<cdot>d2) t2"
shows "isodefl (u_map\<cdot>(cprod_map\<cdot>d1\<cdot>d2)) (sprod_defl\<cdot>t1\<cdot>t2)"
-using assms unfolding isodefl_def
-apply (simp add: emb_u_def prj_u_def liftemb_prod_def liftprj_prod_def)
-apply (simp add: emb_u_def [symmetric] prj_u_def [symmetric])
-apply (simp add: cfcomp1 encode_prod_u_map cast_sprod_defl sprod_map_map)
-done
+using isodefl_sprod [OF assms] unfolding isodefl_def
+unfolding emb_u_def prj_u_def liftemb_prod_def liftprj_prod_def
+by (simp add: cfcomp1 encode_prod_u_map)
lemma encode_cfun_map:
"encode_cfun\<cdot>(cfun_map\<cdot>f\<cdot>g\<cdot>(decode_cfun\<cdot>x))
@@ -308,13 +306,10 @@
done
lemma isodefl_cfun:
- "isodefl (u_map\<cdot>d1) t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
- isodefl (cfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)"
-apply (rule isodeflI)
-apply (simp add: cast_sfun_defl cast_isodefl)
-apply (simp add: emb_cfun_def prj_cfun_def encode_cfun_map)
-apply (simp add: sfun_map_map isodefl_strict)
-done
+ assumes "isodefl (u_map\<cdot>d1) t1" and "isodefl d2 t2"
+ shows "isodefl (cfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)"
+using isodefl_sfun [OF assms] unfolding isodefl_def
+by (simp add: emb_cfun_def prj_cfun_def cfcomp1 encode_cfun_map)
subsection {* Setting up the domain package *}
--- a/src/HOL/HOLCF/Library/Sum_Cpo.thy Tue Nov 30 18:40:23 2010 +0100
+++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy Tue Nov 30 14:01:25 2010 -0800
@@ -264,27 +264,24 @@
begin
definition
- "liftemb = (udom_emb ssum_approx oo ssum_map\<cdot>emb\<cdot>emb) oo encode_sum_u"
+ "liftemb = emb oo encode_sum_u"
definition
- "liftprj =
- decode_sum_u oo (ssum_map\<cdot>prj\<cdot>prj oo udom_prj ssum_approx)"
+ "liftprj = decode_sum_u oo prj"
definition
- "liftdefl (t::('a + 'b) itself) = ssum_defl\<cdot>DEFL('a u)\<cdot>DEFL('b u)"
+ "liftdefl (t::('a + 'b) itself) = DEFL('a u \<oplus> 'b u)"
instance proof
show "ep_pair liftemb (liftprj :: udom \<rightarrow> ('a + 'b) u)"
unfolding liftemb_sum_def liftprj_sum_def
apply (rule ep_pair_comp)
apply (rule ep_pair.intro, simp, simp)
- apply (rule ep_pair_comp)
- apply (intro ep_pair_ssum_map ep_pair_emb_prj)
- apply (rule ep_pair_udom [OF ssum_approx])
+ apply (rule ep_pair_emb_prj)
done
show "cast\<cdot>LIFTDEFL('a + 'b) = liftemb oo (liftprj :: udom \<rightarrow> ('a + 'b) u)"
unfolding liftemb_sum_def liftprj_sum_def liftdefl_sum_def
- by (simp add: cast_ssum_defl cast_DEFL cfcomp1 ssum_map_map)
+ by (simp add: cast_DEFL cfcomp1)
qed
end