# HG changeset patch
# User huffman
# Date 1294364438 28800
# Node ID 5bc117c382ec40f0de9ae6decc1edba7e364bf49
# Parent  480978f80eae29e8f246c84f1a532b1c70b68e02
rename constant u_defl to u_liftdefl;
add new constant u_defl :: udom defl -> udom defl

diff -r 480978f80eae -r 5bc117c382ec src/HOL/HOLCF/Domain.thy
--- a/src/HOL/HOLCF/Domain.thy	Thu Jan 06 16:52:35 2011 -0800
+++ b/src/HOL/HOLCF/Domain.thy	Thu Jan 06 17:40:38 2011 -0800
@@ -274,9 +274,16 @@
 done
 
 lemma isodefl_u:
-  "isodefl' d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
+  "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
 apply (rule isodeflI)
-apply (simp add: cast_u_defl isodefl'_def)
+apply (simp add: cast_u_defl cast_isodefl)
+apply (simp add: emb_u_def prj_u_def liftemb_eq liftprj_eq u_map_map)
+done
+
+lemma isodefl_u_liftdefl:
+  "isodefl' d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_liftdefl\<cdot>t)"
+apply (rule isodeflI)
+apply (simp add: cast_u_liftdefl isodefl'_def)
 apply (simp add: emb_u_def prj_u_def liftemb_eq liftprj_eq)
 done
 
@@ -319,7 +326,7 @@
 
 lemmas [domain_defl_simps] =
   DEFL_cfun DEFL_sfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u
-  liftdefl_eq LIFTDEFL_prod
+  liftdefl_eq LIFTDEFL_prod u_liftdefl_liftdefl_of
 
 lemmas [domain_map_ID] =
   cfun_map_ID sfun_map_ID ssum_map_ID sprod_map_ID prod_map_ID u_map_ID
@@ -327,6 +334,7 @@
 lemmas [domain_isodefl] =
   isodefl_u isodefl_sfun isodefl_ssum isodefl_sprod
   isodefl_cfun isodefl_prod isodefl_prod_u isodefl'_liftdefl_of
+  isodefl_u_liftdefl
 
 lemmas [domain_deflation] =
   deflation_cfun_map deflation_sfun_map deflation_ssum_map
diff -r 480978f80eae -r 5bc117c382ec src/HOL/HOLCF/Library/List_Predomain.thy
--- a/src/HOL/HOLCF/Library/List_Predomain.thy	Thu Jan 06 16:52:35 2011 -0800
+++ b/src/HOL/HOLCF/Library/List_Predomain.thy	Thu Jan 06 17:40:38 2011 -0800
@@ -97,7 +97,7 @@
 subsection {* Lists are a predomain *}
 
 definition list_liftdefl :: "udom u defl \<rightarrow> udom u defl"
-  where "list_liftdefl = (\<Lambda> a. udefl\<cdot>(slist_defl\<cdot>(u_defl\<cdot>a)))"
+  where "list_liftdefl = (\<Lambda> a. udefl\<cdot>(slist_defl\<cdot>(u_liftdefl\<cdot>a)))"
 
 lemma cast_slist_defl: "cast\<cdot>(slist_defl\<cdot>a) = emb oo slist_map\<cdot>(cast\<cdot>a) oo prj"
 using isodefl_slist [where fa="cast\<cdot>a" and da="a"]
@@ -122,7 +122,7 @@
       ep_pair_emb_prj predomain_ep ep_pair_u, simp add: ep_pair.intro)
   show "cast\<cdot>LIFTDEFL('a list) = liftemb oo (liftprj :: udom u \<rightarrow> ('a list) u)"
     unfolding liftemb_list_def liftprj_list_def liftdefl_list_def
-    apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_defl cast_liftdefl)
+    apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_liftdefl cast_liftdefl)
     apply (simp add: slist_map'_oo u_emb_bottom cfun_eq_iff)
     done
 qed
@@ -162,7 +162,7 @@
   assumes "isodefl' d t"
   shows "isodefl' (list_map d) (list_liftdefl\<cdot>t)"
 using assms unfolding isodefl'_def liftemb_list_def liftprj_list_def
-apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_defl)
+apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_liftdefl)
 apply (simp add: cfcomp1 encode_list_u_map)
 apply (simp add: slist_map'_slist_map' u_emb_bottom)
 done
diff -r 480978f80eae -r 5bc117c382ec src/HOL/HOLCF/Library/Sum_Cpo.thy
--- a/src/HOL/HOLCF/Library/Sum_Cpo.thy	Thu Jan 06 16:52:35 2011 -0800
+++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy	Thu Jan 06 17:40:38 2011 -0800
@@ -289,7 +289,7 @@
 unfolding udefl_def by (simp add: cast_defl_fun1 ep_pair_strictify_up)
 
 definition sum_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl"
-  where "sum_liftdefl = (\<Lambda> a b. udefl\<cdot>(ssum_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>b)))"
+  where "sum_liftdefl = (\<Lambda> a b. udefl\<cdot>(ssum_defl\<cdot>(u_liftdefl\<cdot>a)\<cdot>(u_liftdefl\<cdot>b)))"
 
 lemma u_emb_bottom: "u_emb\<cdot>\<bottom> = \<bottom>"
 by (rule pcpo_ep_pair.e_strict [unfolded pcpo_ep_pair_def, OF ep_pair_u])
@@ -321,7 +321,7 @@
       ep_pair_ssum ep_pair_strictify_up, simp add: ep_pair.intro)
   show "cast\<cdot>LIFTDEFL('a + 'b) = liftemb oo (liftprj :: udom u \<rightarrow> ('a + 'b) u)"
     unfolding liftemb_sum_def liftprj_sum_def liftdefl_sum_def
-    by (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_defl
+    by (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_liftdefl
       cast_liftdefl cfcomp1 ssum_map_map u_emb_bottom)
 qed
 
@@ -360,7 +360,7 @@
   assumes "isodefl' d1 t1" and "isodefl' d2 t2"
   shows "isodefl' (sum_map' d1 d2) (sum_liftdefl\<cdot>t1\<cdot>t2)"
 using assms unfolding isodefl'_def liftemb_sum_def liftprj_sum_def
-apply (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_defl)
+apply (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_liftdefl)
 apply (simp add: cfcomp1 encode_sum_u_sum_map)
 apply (simp add: ssum_map_map u_emb_bottom)
 done
diff -r 480978f80eae -r 5bc117c382ec src/HOL/HOLCF/Representable.thy
--- a/src/HOL/HOLCF/Representable.thy	Thu Jan 06 16:52:35 2011 -0800
+++ b/src/HOL/HOLCF/Representable.thy	Thu Jan 06 17:40:38 2011 -0800
@@ -163,8 +163,8 @@
 
 subsection {* Type combinators *}
 
-definition u_defl :: "udom u defl \<rightarrow> udom defl"
-  where "u_defl = defl_fun1 u_emb u_prj ID"
+definition u_defl :: "udom defl \<rightarrow> udom defl"
+  where "u_defl = defl_fun1 u_emb u_prj u_map"
 
 definition prod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
   where "prod_defl = defl_fun2 prod_emb prod_prj prod_map"
@@ -179,8 +179,9 @@
   where "sfun_defl = defl_fun2 sfun_emb sfun_prj sfun_map"
 
 lemma cast_u_defl:
-  "cast\<cdot>(u_defl\<cdot>A) = u_emb oo cast\<cdot>A oo u_prj"
-unfolding u_defl_def by (simp add: cast_defl_fun1 ep_pair_u)
+  "cast\<cdot>(u_defl\<cdot>A) = u_emb oo u_map\<cdot>(cast\<cdot>A) oo u_prj"
+using ep_pair_u finite_deflation_u_map
+unfolding u_defl_def by (rule cast_defl_fun1)
 
 lemma cast_prod_defl:
   "cast\<cdot>(prod_defl\<cdot>A\<cdot>B) =
@@ -206,6 +207,20 @@
 using ep_pair_sfun finite_deflation_sfun_map
 unfolding sfun_defl_def by (rule cast_defl_fun2)
 
+text {* Special deflation combinator for unpointed types. *}
+
+definition u_liftdefl :: "udom u defl \<rightarrow> udom defl"
+  where "u_liftdefl = defl_fun1 u_emb u_prj ID"
+
+lemma cast_u_liftdefl:
+  "cast\<cdot>(u_liftdefl\<cdot>A) = u_emb oo cast\<cdot>A oo u_prj"
+unfolding u_liftdefl_def by (simp add: cast_defl_fun1 ep_pair_u)
+
+lemma u_liftdefl_liftdefl_of:
+  "u_liftdefl\<cdot>(liftdefl_of\<cdot>A) = u_defl\<cdot>A"
+by (rule cast_eq_imp_eq)
+   (simp add: cast_u_liftdefl cast_liftdefl_of cast_u_defl)
+
 subsection {* Class instance proofs *}
 
 subsubsection {* Universal domain *}
@@ -262,7 +277,7 @@
   "prj = liftprj oo u_prj"
 
 definition
-  "defl (t::'a u itself) = u_defl\<cdot>LIFTDEFL('a)"
+  "defl (t::'a u itself) = u_liftdefl\<cdot>LIFTDEFL('a)"
 
 definition
   "(liftemb :: 'a u u \<rightarrow> udom u) = u_map\<cdot>emb"
@@ -279,12 +294,12 @@
     by (intro ep_pair_comp ep_pair_u predomain_ep)
   show "cast\<cdot>DEFL('a u) = emb oo (prj :: udom \<rightarrow> 'a u)"
     unfolding emb_u_def prj_u_def defl_u_def
-    by (simp add: cast_u_defl cast_liftdefl assoc_oo)
+    by (simp add: cast_u_liftdefl cast_liftdefl assoc_oo)
 qed (fact liftemb_u_def liftprj_u_def liftdefl_u_def)+
 
 end
 
-lemma DEFL_u: "DEFL('a::predomain u) = u_defl\<cdot>LIFTDEFL('a)"
+lemma DEFL_u: "DEFL('a::predomain u) = u_liftdefl\<cdot>LIFTDEFL('a)"
 by (rule defl_u_def)
 
 subsubsection {* Strict function space *}
diff -r 480978f80eae -r 5bc117c382ec src/HOL/HOLCF/ex/Domain_Proofs.thy
--- a/src/HOL/HOLCF/ex/Domain_Proofs.thy	Thu Jan 06 16:52:35 2011 -0800
+++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy	Thu Jan 06 17:40:38 2011 -0800
@@ -30,15 +30,15 @@
     "udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl"
 where
   "foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3). 
-    ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>a))\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>t2)))
-    , u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>t3))\<cdot>DEFL(tr)))
-    , u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(convex_defl\<cdot>t1)))\<cdot>DEFL(tr))))))"
+    ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t2))
+    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>t3)\<cdot>DEFL(tr))
+    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>t1))\<cdot>DEFL(tr)))))"
 
 lemma foo_bar_baz_deflF_beta:
   "foo_bar_baz_deflF\<cdot>a\<cdot>t =
-    ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>a))\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(fst (snd t)))))
-    , u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(snd (snd t))))\<cdot>DEFL(tr)))
-    , u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(convex_defl\<cdot>(fst t))))\<cdot>DEFL(tr))))"
+    ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(fst (snd t))))
+    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(snd (snd t)))\<cdot>DEFL(tr))
+    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(fst t)))\<cdot>DEFL(tr)))"
 unfolding foo_bar_baz_deflF_def
 by (simp add: split_def)
 
@@ -62,13 +62,13 @@
 text {* Unfold rules for each combinator. *}
 
 lemma foo_defl_unfold:
-  "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>a))\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(bar_defl\<cdot>a))))"
+  "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
 unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
 
-lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(baz_defl\<cdot>a)))\<cdot>DEFL(tr)))"
+lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(baz_defl\<cdot>a))\<cdot>DEFL(tr))"
 unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
 
-lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a))))\<cdot>DEFL(tr)))"
+lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a)))\<cdot>DEFL(tr))"
 unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
 
 text "The automation for the previous steps will be quite similar to