src/HOL/HOLCF/Representable.thy

   assumes cast_liftdefl: "cast\<cdot>(liftdefl TYPE('a)) = liftemb oo liftprj"
 
 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"
-
-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)
+definition liftdefl_of :: "udom defl \<rightarrow> udom u defl"
+  where "liftdefl_of = defl_fun1 ID ID 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"
   fixes prj :: "udom \<rightarrow> 'a"
   fixes defl :: "'a itself \<Rightarrow> udom defl"
   assumes ep_pair_emb_prj: "ep_pair emb prj"
   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)"
 
 instance "domain" \<subseteq> predomain

   show "ep_pair liftemb (liftprj::udom\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>)"
     unfolding liftemb_eq liftprj_eq
     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 {*
   Constants @{const liftemb} and @{const liftprj} imply class predomain.
 *}

 
 definition
   "(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)"
     by (simp add: ep_pair.intro)
   show "cast\<cdot>DEFL(udom) = emb oo (prj :: udom \<rightarrow> udom)"

 
 definition
   "(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)"
     unfolding emb_u_def prj_u_def
     by (intro ep_pair_comp ep_pair_u predomain_ep)

 
 definition
   "(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)"
     unfolding emb_sfun_def prj_sfun_def
     by (intro ep_pair_comp ep_pair_sfun ep_pair_sfun_map ep_pair_emb_prj)

 
 definition
   "(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"
     by (rule ep_pair.intro, simp_all)
   thus "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"

 
 definition
   "(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)"
     unfolding emb_sprod_def prj_sprod_def
     by (intro ep_pair_comp ep_pair_sprod ep_pair_sprod_map ep_pair_emb_prj)

     unfolding prj_prod_def liftprj_prod_def liftprj_eq
     unfolding encode_prod_u_def decode_prod_u_def
     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
 
 lemma DEFL_prod:

 
 definition
   "(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)"
     unfolding emb_unit_def prj_unit_def
     by (simp add: ep_pair.intro)

 
 definition
   "(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)"
     unfolding emb_ssum_def prj_ssum_def
     by (intro ep_pair_comp ep_pair_ssum ep_pair_ssum_map ep_pair_emb_prj)

 
 definition
   "(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
   have "ep_pair (\<Lambda>(x::'a lift). Rep_lift x) (\<Lambda> y. Abs_lift y)"
     by (simp add: ep_pair_def)