# HG changeset patch
# User huffman
# Date 1294361555 28800
# Node ID 480978f80eae29e8f246c84f1a532b1c70b68e02
# Parent  12585dfb86fef51f18493607049666ed32599b40
rename constant pdefl to liftdefl_of

diff -r 12585dfb86fe -r 480978f80eae src/HOL/HOLCF/Domain.thy
--- a/src/HOL/HOLCF/Domain.thy	Thu Jan 06 21:06:18 2011 +0100
+++ b/src/HOL/HOLCF/Domain.thy	Thu Jan 06 16:52:35 2011 -0800
@@ -105,7 +105,7 @@
   assumes defl: "defl \<equiv> (\<lambda> a::'a itself. t)"
   assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom u) \<equiv> u_map\<cdot>emb"
   assumes liftprj: "(liftprj :: udom u \<rightarrow> 'a u) \<equiv> u_map\<cdot>prj"
-  assumes liftdefl: "(liftdefl :: 'a itself \<Rightarrow> _) \<equiv> (\<lambda>t. pdefl\<cdot>DEFL('a))"
+  assumes liftdefl: "(liftdefl :: 'a itself \<Rightarrow> _) \<equiv> (\<lambda>t. liftdefl_of\<cdot>DEFL('a))"
   shows "OFCLASS('a, domain_class)"
 proof
   have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
@@ -233,9 +233,9 @@
 unfolding isodefl_def
 by (simp add: cfun_eq_iff assms prj_emb_prj emb_prj_emb)
 
-lemma isodefl'_pdefl: "isodefl d t \<Longrightarrow> isodefl' d (pdefl\<cdot>t)"
+lemma isodefl'_liftdefl_of: "isodefl d t \<Longrightarrow> isodefl' d (liftdefl_of\<cdot>t)"
 unfolding isodefl_def isodefl'_def
-by (simp add: cast_pdefl u_map_oo liftemb_eq liftprj_eq)
+by (simp add: cast_liftdefl_of u_map_oo liftemb_eq liftprj_eq)
 
 lemma isodefl_sfun:
   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
@@ -326,7 +326,7 @@
 
 lemmas [domain_isodefl] =
   isodefl_u isodefl_sfun isodefl_ssum isodefl_sprod
-  isodefl_cfun isodefl_prod isodefl_prod_u isodefl'_pdefl
+  isodefl_cfun isodefl_prod isodefl_prod_u isodefl'_liftdefl_of
 
 lemmas [domain_deflation] =
   deflation_cfun_map deflation_sfun_map deflation_ssum_map
diff -r 12585dfb86fe -r 480978f80eae src/HOL/HOLCF/Library/Defl_Bifinite.thy
--- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Thu Jan 06 21:06:18 2011 +0100
+++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Thu Jan 06 16:52:35 2011 -0800
@@ -657,7 +657,7 @@
   "(liftprj :: udom u \<rightarrow> 'a defl u) = u_map\<cdot>prj"
 
 definition
-  "liftdefl (t::'a defl itself) = pdefl\<cdot>DEFL('a defl)"
+  "liftdefl (t::'a defl itself) = liftdefl_of\<cdot>DEFL('a defl)"
 
 instance proof
   show ep: "ep_pair emb (prj :: udom \<rightarrow> 'a defl)"
diff -r 12585dfb86fe -r 480978f80eae src/HOL/HOLCF/Library/Option_Cpo.thy
--- a/src/HOL/HOLCF/Library/Option_Cpo.thy	Thu Jan 06 21:06:18 2011 +0100
+++ b/src/HOL/HOLCF/Library/Option_Cpo.thy	Thu Jan 06 16:52:35 2011 -0800
@@ -280,7 +280,7 @@
 
 lemma isodefl_option [domain_isodefl]:
   assumes "isodefl' d t"
-  shows "isodefl' (option_map d) (sum_liftdefl\<cdot>(pdefl\<cdot>DEFL(unit))\<cdot>t)"
+  shows "isodefl' (option_map d) (sum_liftdefl\<cdot>(liftdefl_of\<cdot>DEFL(unit))\<cdot>t)"
 using isodefl_sum [OF isodefl_LIFTDEFL [where 'a=unit] assms]
 unfolding isodefl'_def liftemb_option_def liftprj_option_def liftdefl_eq
 by (simp add: cfcomp1 u_map_map encode_option_option_map)
diff -r 12585dfb86fe -r 480978f80eae src/HOL/HOLCF/Powerdomains.thy
--- a/src/HOL/HOLCF/Powerdomains.thy	Thu Jan 06 21:06:18 2011 +0100
+++ b/src/HOL/HOLCF/Powerdomains.thy	Thu Jan 06 16:52:35 2011 -0800
@@ -78,7 +78,7 @@
   "(liftprj :: udom u \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj"
 
 definition
-  "liftdefl (t::'a upper_pd itself) = pdefl\<cdot>DEFL('a upper_pd)"
+  "liftdefl (t::'a upper_pd itself) = liftdefl_of\<cdot>DEFL('a upper_pd)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)"
@@ -111,7 +111,7 @@
   "(liftprj :: udom u \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj"
 
 definition
-  "liftdefl (t::'a lower_pd itself) = pdefl\<cdot>DEFL('a lower_pd)"
+  "liftdefl (t::'a lower_pd itself) = liftdefl_of\<cdot>DEFL('a lower_pd)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)"
@@ -144,7 +144,7 @@
   "(liftprj :: udom u \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj"
 
 definition
-  "liftdefl (t::'a convex_pd itself) = pdefl\<cdot>DEFL('a convex_pd)"
+  "liftdefl (t::'a convex_pd itself) = liftdefl_of\<cdot>DEFL('a convex_pd)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)"
diff -r 12585dfb86fe -r 480978f80eae src/HOL/HOLCF/Representable.thy
--- a/src/HOL/HOLCF/Representable.thy	Thu Jan 06 21:06:18 2011 +0100
+++ b/src/HOL/HOLCF/Representable.thy	Thu Jan 06 16:52:35 2011 -0800
@@ -34,11 +34,11 @@
 syntax "_LIFTDEFL" :: "type \<Rightarrow> logic"  ("(1LIFTDEFL/(1'(_')))")
 translations "LIFTDEFL('t)" \<rightleftharpoons> "CONST liftdefl TYPE('t)"
 
-definition pdefl :: "udom defl \<rightarrow> udom u defl"
-  where "pdefl = defl_fun1 ID ID u_map"
+definition liftdefl_of :: "udom defl \<rightarrow> udom u defl"
+  where "liftdefl_of = defl_fun1 ID ID u_map"
 
-lemma cast_pdefl: "cast\<cdot>(pdefl\<cdot>t) = u_map\<cdot>(cast\<cdot>t)"
-by (simp add: pdefl_def cast_defl_fun1 ep_pair_def finite_deflation_u_map)
+lemma cast_liftdefl_of: "cast\<cdot>(liftdefl_of\<cdot>t) = u_map\<cdot>(cast\<cdot>t)"
+by (simp add: liftdefl_of_def cast_defl_fun1 ep_pair_def finite_deflation_u_map)
 
 class "domain" = predomain_syn + pcpo +
   fixes emb :: "'a \<rightarrow> udom"
@@ -48,7 +48,7 @@
   assumes cast_DEFL: "cast\<cdot>(defl TYPE('a)) = emb oo prj"
   assumes liftemb_eq: "liftemb = u_map\<cdot>emb"
   assumes liftprj_eq: "liftprj = u_map\<cdot>prj"
-  assumes liftdefl_eq: "liftdefl TYPE('a) = pdefl\<cdot>(defl TYPE('a))"
+  assumes liftdefl_eq: "liftdefl TYPE('a) = liftdefl_of\<cdot>(defl TYPE('a))"
 
 syntax "_DEFL" :: "type \<Rightarrow> logic"  ("(1DEFL/(1'(_')))")
 translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)"
@@ -60,7 +60,7 @@
     by (intro ep_pair_u_map ep_pair_emb_prj)
   show "cast\<cdot>LIFTDEFL('a) = liftemb oo (liftprj::udom\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>)"
     unfolding liftemb_eq liftprj_eq liftdefl_eq
-    by (simp add: cast_pdefl cast_DEFL u_map_oo)
+    by (simp add: cast_liftdefl_of cast_DEFL u_map_oo)
 qed
 
 text {*
@@ -229,7 +229,7 @@
   "(liftprj :: udom u \<rightarrow> udom u) = u_map\<cdot>prj"
 
 definition
-  "liftdefl (t::udom itself) = pdefl\<cdot>DEFL(udom)"
+  "liftdefl (t::udom itself) = liftdefl_of\<cdot>DEFL(udom)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> udom)"
@@ -271,7 +271,7 @@
   "(liftprj :: udom u \<rightarrow> 'a u u) = u_map\<cdot>prj"
 
 definition
-  "liftdefl (t::'a u itself) = pdefl\<cdot>DEFL('a u)"
+  "liftdefl (t::'a u itself) = liftdefl_of\<cdot>DEFL('a u)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> 'a u)"
@@ -308,7 +308,7 @@
   "(liftprj :: udom u \<rightarrow> ('a \<rightarrow>! 'b) u) = u_map\<cdot>prj"
 
 definition
-  "liftdefl (t::('a \<rightarrow>! 'b) itself) = pdefl\<cdot>DEFL('a \<rightarrow>! 'b)"
+  "liftdefl (t::('a \<rightarrow>! 'b) itself) = liftdefl_of\<cdot>DEFL('a \<rightarrow>! 'b)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
@@ -346,7 +346,7 @@
   "(liftprj :: udom u \<rightarrow> ('a \<rightarrow> 'b) u) = u_map\<cdot>prj"
 
 definition
-  "liftdefl (t::('a \<rightarrow> 'b) itself) = pdefl\<cdot>DEFL('a \<rightarrow> 'b)"
+  "liftdefl (t::('a \<rightarrow> 'b) itself) = liftdefl_of\<cdot>DEFL('a \<rightarrow> 'b)"
 
 instance proof
   have "ep_pair encode_cfun decode_cfun"
@@ -386,7 +386,7 @@
   "(liftprj :: udom u \<rightarrow> ('a \<otimes> 'b) u) = u_map\<cdot>prj"
 
 definition
-  "liftdefl (t::('a \<otimes> 'b) itself) = pdefl\<cdot>DEFL('a \<otimes> 'b)"
+  "liftdefl (t::('a \<otimes> 'b) itself) = liftdefl_of\<cdot>DEFL('a \<otimes> 'b)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
@@ -475,9 +475,9 @@
     apply (rule cfun_eqI, case_tac x, simp)
     apply (rename_tac y, case_tac "prod_prj\<cdot>y", simp)
     done
-  show 5: "LIFTDEFL('a \<times> 'b) = pdefl\<cdot>DEFL('a \<times> 'b)"
+  show 5: "LIFTDEFL('a \<times> 'b) = liftdefl_of\<cdot>DEFL('a \<times> 'b)"
     by (rule cast_eq_imp_eq)
-      (simp add: cast_liftdefl cast_pdefl cast_DEFL 2 3 4 u_map_oo)
+      (simp add: cast_liftdefl cast_liftdefl_of cast_DEFL 2 3 4 u_map_oo)
 qed
 
 end
@@ -512,7 +512,7 @@
   "(liftprj :: udom u \<rightarrow> unit u) = u_map\<cdot>prj"
 
 definition
-  "liftdefl (t::unit itself) = pdefl\<cdot>DEFL(unit)"
+  "liftdefl (t::unit itself) = liftdefl_of\<cdot>DEFL(unit)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> unit)"
@@ -590,7 +590,7 @@
   "(liftprj :: udom u \<rightarrow> ('a \<oplus> 'b) u) = u_map\<cdot>prj"
 
 definition
-  "liftdefl (t::('a \<oplus> 'b) itself) = pdefl\<cdot>DEFL('a \<oplus> 'b)"
+  "liftdefl (t::('a \<oplus> 'b) itself) = liftdefl_of\<cdot>DEFL('a \<oplus> 'b)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
@@ -628,7 +628,7 @@
   "(liftprj :: udom u \<rightarrow> 'a lift u) = u_map\<cdot>prj"
 
 definition
-  "liftdefl (t::'a lift itself) = pdefl\<cdot>DEFL('a lift)"
+  "liftdefl (t::'a lift itself) = liftdefl_of\<cdot>DEFL('a lift)"
 
 instance proof
   note [simp] = cont_Rep_lift cont_Abs_lift Rep_lift_inverse Abs_lift_inverse
diff -r 12585dfb86fe -r 480978f80eae src/HOL/HOLCF/Tools/domaindef.ML
--- a/src/HOL/HOLCF/Tools/domaindef.ML	Thu Jan 06 21:06:18 2011 +0100
+++ b/src/HOL/HOLCF/Tools/domaindef.ML	Thu Jan 06 16:52:35 2011 -0800
@@ -136,7 +136,7 @@
     val liftdefl_eqn =
       Logic.mk_equals (liftdefl_const newT,
         Abs ("t", Term.itselfT newT,
-          mk_capply (@{const pdefl}, defl_const newT $ Logic.mk_type newT)))
+          mk_capply (@{const liftdefl_of}, defl_const newT $ Logic.mk_type newT)))
 
     val name_def = Binding.suffix_name "_def" name
     val emb_bind = (Binding.prefix_name "emb_" name_def, [])
diff -r 12585dfb86fe -r 480978f80eae src/HOL/HOLCF/ex/Domain_Proofs.thy
--- a/src/HOL/HOLCF/ex/Domain_Proofs.thy	Thu Jan 06 21:06:18 2011 +0100
+++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy	Thu Jan 06 16:52:35 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>(pdefl\<cdot>a))\<cdot>(u_defl\<cdot>(pdefl\<cdot>t2)))
-    , u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>t3))\<cdot>DEFL(tr)))
-    , u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>(convex_defl\<cdot>t1)))\<cdot>DEFL(tr))))))"
+    ( 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))))))"
 
 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>(pdefl\<cdot>a))\<cdot>(u_defl\<cdot>(pdefl\<cdot>(fst (snd t)))))
-    , u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>(snd (snd t))))\<cdot>DEFL(tr)))
-    , u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>(convex_defl\<cdot>(fst t))))\<cdot>DEFL(tr))))"
+    ( 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))))"
 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>(pdefl\<cdot>a))\<cdot>(u_defl\<cdot>(pdefl\<cdot>(bar_defl\<cdot>a))))"
+  "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))))"
 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>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>(baz_defl\<cdot>a)))\<cdot>DEFL(tr)))"
+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)))"
 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>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a))))\<cdot>DEFL(tr)))"
+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)))"
 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
@@ -110,7 +110,7 @@
   "(liftprj :: udom u \<rightarrow> 'a foo u) \<equiv> u_map\<cdot>prj"
 
 definition
-  "liftdefl \<equiv> \<lambda>(t::'a foo itself). pdefl\<cdot>DEFL('a foo)"
+  "liftdefl \<equiv> \<lambda>(t::'a foo itself). liftdefl_of\<cdot>DEFL('a foo)"
 
 instance
 apply (rule typedef_domain_class)
@@ -145,7 +145,7 @@
   "(liftprj :: udom u \<rightarrow> 'a bar u) \<equiv> u_map\<cdot>prj"
 
 definition
-  "liftdefl \<equiv> \<lambda>(t::'a bar itself). pdefl\<cdot>DEFL('a bar)"
+  "liftdefl \<equiv> \<lambda>(t::'a bar itself). liftdefl_of\<cdot>DEFL('a bar)"
 
 instance
 apply (rule typedef_domain_class)
@@ -180,7 +180,7 @@
   "(liftprj :: udom u \<rightarrow> 'a baz u) \<equiv> u_map\<cdot>prj"
 
 definition
-  "liftdefl \<equiv> \<lambda>(t::'a baz itself). pdefl\<cdot>DEFL('a baz)"
+  "liftdefl \<equiv> \<lambda>(t::'a baz itself). liftdefl_of\<cdot>DEFL('a baz)"
 
 instance
 apply (rule typedef_domain_class)