# HG changeset patch
# User huffman
# Date 1291154485 28800
# Node ID 158d18502378099ebba59788d1c2a3a77f73ca3e
# Parent  a3af470a55d29db2952d136352af50a9add50c05
simplify predomain instances

diff -r a3af470a55d2 -r 158d18502378 src/HOL/HOLCF/Bifinite.thy
--- 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"
diff -r a3af470a55d2 -r 158d18502378 src/HOL/HOLCF/Domain.thy
--- 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 *}
 
diff -r a3af470a55d2 -r 158d18502378 src/HOL/HOLCF/Library/Sum_Cpo.thy
--- 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