# HG changeset patch
# User huffman
# Date 1258647720 28800
# Node ID 7e434813752f181efc52a4dbdabfd6030259a246
# Parent  685bbf418cb77b87398b1278cacb34d2c02d0089
change naming convention for deflation combinators

diff -r 685bbf418cb7 -r 7e434813752f src/HOLCF/Representable.thy
--- a/src/HOLCF/Representable.thy	Thu Nov 19 08:08:57 2009 -0800
+++ b/src/HOLCF/Representable.thy	Thu Nov 19 08:22:00 2009 -0800
@@ -690,14 +690,14 @@
           Abs_fin_defl (udom_emb oo
             f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj))))"
 
-definition "cfun_typ = TypeRep_fun2 cfun_map"
-definition "ssum_typ = TypeRep_fun2 ssum_map"
-definition "sprod_typ = TypeRep_fun2 sprod_map"
-definition "cprod_typ = TypeRep_fun2 cprod_map"
-definition "u_typ = TypeRep_fun1 u_map"
-definition "upper_typ = TypeRep_fun1 upper_map"
-definition "lower_typ = TypeRep_fun1 lower_map"
-definition "convex_typ = TypeRep_fun1 convex_map"
+definition "cfun_defl = TypeRep_fun2 cfun_map"
+definition "ssum_defl = TypeRep_fun2 ssum_map"
+definition "sprod_defl = TypeRep_fun2 sprod_map"
+definition "cprod_defl = TypeRep_fun2 cprod_map"
+definition "u_defl = TypeRep_fun1 u_map"
+definition "upper_defl = TypeRep_fun1 upper_map"
+definition "lower_defl = TypeRep_fun1 lower_map"
+definition "convex_defl = TypeRep_fun1 convex_map"
 
 lemma Rep_fin_defl_mono: "a \<sqsubseteq> b \<Longrightarrow> Rep_fin_defl a \<sqsubseteq> Rep_fin_defl b"
 unfolding below_fin_defl_def .
@@ -746,124 +746,124 @@
                    Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
 qed
 
-lemma cast_cfun_typ:
-  "cast\<cdot>(cfun_typ\<cdot>A\<cdot>B) = udom_emb oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
-unfolding cfun_typ_def
+lemma cast_cfun_defl:
+  "cast\<cdot>(cfun_defl\<cdot>A\<cdot>B) = udom_emb oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
+unfolding cfun_defl_def
 apply (rule cast_TypeRep_fun2)
 apply (erule (1) finite_deflation_cfun_map)
 done
 
-lemma cast_ssum_typ:
-  "cast\<cdot>(ssum_typ\<cdot>A\<cdot>B) = udom_emb oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
-unfolding ssum_typ_def
+lemma cast_ssum_defl:
+  "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) = udom_emb oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
+unfolding ssum_defl_def
 apply (rule cast_TypeRep_fun2)
 apply (erule (1) finite_deflation_ssum_map)
 done
 
-lemma cast_sprod_typ:
-  "cast\<cdot>(sprod_typ\<cdot>A\<cdot>B) = udom_emb oo sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
-unfolding sprod_typ_def
+lemma cast_sprod_defl:
+  "cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) = udom_emb oo sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
+unfolding sprod_defl_def
 apply (rule cast_TypeRep_fun2)
 apply (erule (1) finite_deflation_sprod_map)
 done
 
-lemma cast_cprod_typ:
-  "cast\<cdot>(cprod_typ\<cdot>A\<cdot>B) = udom_emb oo cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
-unfolding cprod_typ_def
+lemma cast_cprod_defl:
+  "cast\<cdot>(cprod_defl\<cdot>A\<cdot>B) = udom_emb oo cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
+unfolding cprod_defl_def
 apply (rule cast_TypeRep_fun2)
 apply (erule (1) finite_deflation_cprod_map)
 done
 
-lemma cast_u_typ:
-  "cast\<cdot>(u_typ\<cdot>A) = udom_emb oo u_map\<cdot>(cast\<cdot>A) oo udom_prj"
-unfolding u_typ_def
+lemma cast_u_defl:
+  "cast\<cdot>(u_defl\<cdot>A) = udom_emb oo u_map\<cdot>(cast\<cdot>A) oo udom_prj"
+unfolding u_defl_def
 apply (rule cast_TypeRep_fun1)
 apply (erule finite_deflation_u_map)
 done
 
-lemma cast_upper_typ:
-  "cast\<cdot>(upper_typ\<cdot>A) = udom_emb oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj"
-unfolding upper_typ_def
+lemma cast_upper_defl:
+  "cast\<cdot>(upper_defl\<cdot>A) = udom_emb oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj"
+unfolding upper_defl_def
 apply (rule cast_TypeRep_fun1)
 apply (erule finite_deflation_upper_map)
 done
 
-lemma cast_lower_typ:
-  "cast\<cdot>(lower_typ\<cdot>A) = udom_emb oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj"
-unfolding lower_typ_def
+lemma cast_lower_defl:
+  "cast\<cdot>(lower_defl\<cdot>A) = udom_emb oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj"
+unfolding lower_defl_def
 apply (rule cast_TypeRep_fun1)
 apply (erule finite_deflation_lower_map)
 done
 
-lemma cast_convex_typ:
-  "cast\<cdot>(convex_typ\<cdot>A) = udom_emb oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj"
-unfolding convex_typ_def
+lemma cast_convex_defl:
+  "cast\<cdot>(convex_defl\<cdot>A) = udom_emb oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj"
+unfolding convex_defl_def
 apply (rule cast_TypeRep_fun1)
 apply (erule finite_deflation_convex_map)
 done
 
 text {* REP of type constructor = type combinator *}
 
-lemma REP_cfun: "REP('a \<rightarrow> 'b) = cfun_typ\<cdot>REP('a)\<cdot>REP('b)"
+lemma REP_cfun: "REP('a \<rightarrow> 'b) = cfun_defl\<cdot>REP('a)\<cdot>REP('b)"
 apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_cfun_typ)
+apply (simp add: cast_REP cast_cfun_defl)
 apply (simp add: cfun_map_def)
 apply (simp only: prj_cfun_def emb_cfun_def)
 apply (simp add: expand_cfun_eq ep_pair.e_eq_iff [OF ep_pair_udom])
 done
 
 
-lemma REP_ssum: "REP('a \<oplus> 'b) = ssum_typ\<cdot>REP('a)\<cdot>REP('b)"
+lemma REP_ssum: "REP('a \<oplus> 'b) = ssum_defl\<cdot>REP('a)\<cdot>REP('b)"
 apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_ssum_typ)
+apply (simp add: cast_REP cast_ssum_defl)
 apply (simp add: prj_ssum_def)
 apply (simp add: emb_ssum_def)
 apply (simp add: ssum_map_map cfcomp1)
 done
 
-lemma REP_sprod: "REP('a \<otimes> 'b) = sprod_typ\<cdot>REP('a)\<cdot>REP('b)"
+lemma REP_sprod: "REP('a \<otimes> 'b) = sprod_defl\<cdot>REP('a)\<cdot>REP('b)"
 apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_sprod_typ)
+apply (simp add: cast_REP cast_sprod_defl)
 apply (simp add: prj_sprod_def)
 apply (simp add: emb_sprod_def)
 apply (simp add: sprod_map_map cfcomp1)
 done
 
-lemma REP_cprod: "REP('a \<times> 'b) = cprod_typ\<cdot>REP('a)\<cdot>REP('b)"
+lemma REP_cprod: "REP('a \<times> 'b) = cprod_defl\<cdot>REP('a)\<cdot>REP('b)"
 apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_cprod_typ)
+apply (simp add: cast_REP cast_cprod_defl)
 apply (simp add: prj_cprod_def)
 apply (simp add: emb_cprod_def)
 apply (simp add: cprod_map_map cfcomp1)
 done
 
-lemma REP_up: "REP('a u) = u_typ\<cdot>REP('a)"
+lemma REP_up: "REP('a u) = u_defl\<cdot>REP('a)"
 apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_u_typ)
+apply (simp add: cast_REP cast_u_defl)
 apply (simp add: prj_u_def)
 apply (simp add: emb_u_def)
 apply (simp add: u_map_map cfcomp1)
 done
 
-lemma REP_upper: "REP('a upper_pd) = upper_typ\<cdot>REP('a)"
+lemma REP_upper: "REP('a upper_pd) = upper_defl\<cdot>REP('a)"
 apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_upper_typ)
+apply (simp add: cast_REP cast_upper_defl)
 apply (simp add: prj_upper_pd_def)
 apply (simp add: emb_upper_pd_def)
 apply (simp add: upper_map_map cfcomp1)
 done
 
-lemma REP_lower: "REP('a lower_pd) = lower_typ\<cdot>REP('a)"
+lemma REP_lower: "REP('a lower_pd) = lower_defl\<cdot>REP('a)"
 apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_lower_typ)
+apply (simp add: cast_REP cast_lower_defl)
 apply (simp add: prj_lower_pd_def)
 apply (simp add: emb_lower_pd_def)
 apply (simp add: lower_map_map cfcomp1)
 done
 
-lemma REP_convex: "REP('a convex_pd) = convex_typ\<cdot>REP('a)"
+lemma REP_convex: "REP('a convex_pd) = convex_defl\<cdot>REP('a)"
 apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_convex_typ)
+apply (simp add: cast_REP cast_convex_defl)
 apply (simp add: prj_convex_pd_def)
 apply (simp add: emb_convex_pd_def)
 apply (simp add: convex_map_map cfcomp1)
@@ -963,59 +963,59 @@
 
 lemma isodefl_cfun:
   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
-    isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_typ\<cdot>t1\<cdot>t2)"
+    isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_defl\<cdot>t1\<cdot>t2)"
 apply (rule isodeflI)
-apply (simp add: cast_cfun_typ cast_isodefl)
+apply (simp add: cast_cfun_defl cast_isodefl)
 apply (simp add: emb_cfun_def prj_cfun_def)
 apply (simp add: cfun_map_map cfcomp1)
 done
 
 lemma isodefl_ssum:
   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
-    isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_typ\<cdot>t1\<cdot>t2)"
+    isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_defl\<cdot>t1\<cdot>t2)"
 apply (rule isodeflI)
-apply (simp add: cast_ssum_typ cast_isodefl)
+apply (simp add: cast_ssum_defl cast_isodefl)
 apply (simp add: emb_ssum_def prj_ssum_def)
 apply (simp add: ssum_map_map isodefl_strict)
 done
 
 lemma isodefl_sprod:
   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
-    isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_typ\<cdot>t1\<cdot>t2)"
+    isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_defl\<cdot>t1\<cdot>t2)"
 apply (rule isodeflI)
-apply (simp add: cast_sprod_typ cast_isodefl)
+apply (simp add: cast_sprod_defl cast_isodefl)
 apply (simp add: emb_sprod_def prj_sprod_def)
 apply (simp add: sprod_map_map isodefl_strict)
 done
 
 lemma isodefl_u:
-  "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_typ\<cdot>t)"
+  "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
 apply (rule isodeflI)
-apply (simp add: cast_u_typ cast_isodefl)
+apply (simp add: cast_u_defl cast_isodefl)
 apply (simp add: emb_u_def prj_u_def)
 apply (simp add: u_map_map)
 done
 
 lemma isodefl_upper:
-  "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_typ\<cdot>t)"
+  "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)"
 apply (rule isodeflI)
-apply (simp add: cast_upper_typ cast_isodefl)
+apply (simp add: cast_upper_defl cast_isodefl)
 apply (simp add: emb_upper_pd_def prj_upper_pd_def)
 apply (simp add: upper_map_map)
 done
 
 lemma isodefl_lower:
-  "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_typ\<cdot>t)"
+  "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>t)"
 apply (rule isodeflI)
-apply (simp add: cast_lower_typ cast_isodefl)
+apply (simp add: cast_lower_defl cast_isodefl)
 apply (simp add: emb_lower_pd_def prj_lower_pd_def)
 apply (simp add: lower_map_map)
 done
 
 lemma isodefl_convex:
-  "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_typ\<cdot>t)"
+  "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>t)"
 apply (rule isodeflI)
-apply (simp add: cast_convex_typ cast_isodefl)
+apply (simp add: cast_convex_defl cast_isodefl)
 apply (simp add: emb_convex_pd_def prj_convex_pd_def)
 apply (simp add: convex_map_map)
 done
diff -r 685bbf418cb7 -r 7e434813752f src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Nov 19 08:08:57 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Nov 19 08:22:00 2009 -0800
@@ -197,14 +197,14 @@
 
 (* FIXME: use theory data for this *)
 val defl_tab : term Symtab.table =
-    Symtab.make [(@{type_name "->"}, @{term "cfun_typ"}),
-                 (@{type_name "++"}, @{term "ssum_typ"}),
-                 (@{type_name "**"}, @{term "sprod_typ"}),
-                 (@{type_name "*"}, @{term "cprod_typ"}),
-                 (@{type_name "u"}, @{term "u_typ"}),
-                 (@{type_name "upper_pd"}, @{term "upper_typ"}),
-                 (@{type_name "lower_pd"}, @{term "lower_typ"}),
-                 (@{type_name "convex_pd"}, @{term "convex_typ"})];
+    Symtab.make [(@{type_name "->"}, @{term "cfun_defl"}),
+                 (@{type_name "++"}, @{term "ssum_defl"}),
+                 (@{type_name "**"}, @{term "sprod_defl"}),
+                 (@{type_name "*"}, @{term "cprod_defl"}),
+                 (@{type_name "u"}, @{term "u_defl"}),
+                 (@{type_name "upper_pd"}, @{term "upper_defl"}),
+                 (@{type_name "lower_pd"}, @{term "lower_defl"}),
+                 (@{type_name "convex_pd"}, @{term "convex_defl"})];
 
 fun defl_of_typ
     (tab : term Symtab.table)
@@ -306,20 +306,20 @@
       end) doms;
     val dom_binds = map (fn (_, tbind, _, _) => tbind) doms;
 
-    (* declare type combinator constants *)
-    fun declare_typ_const (vs, tbind, mx, rhs) thy =
+    (* declare deflation combinator constants *)
+    fun declare_defl_const (vs, tbind, mx, rhs) thy =
       let
-        val typ_type = Library.foldr cfunT (map (K deflT) vs, deflT);
-        val typ_bind = Binding.suffix_name "_typ" tbind;
+        val defl_type = Library.foldr cfunT (map (K deflT) vs, deflT);
+        val defl_bind = Binding.suffix_name "_defl" tbind;
       in
-        Sign.declare_const ((typ_bind, typ_type), NoSyn) thy
+        Sign.declare_const ((defl_bind, defl_type), NoSyn) thy
       end;
-    val (typ_consts, thy) = fold_map declare_typ_const doms thy;
+    val (defl_consts, thy) = fold_map declare_defl_const doms thy;
 
     (* defining equations for type combinators *)
     val defl_tab1 = defl_tab; (* FIXME: use theory data *)
     val defl_tab2 =
-      Symtab.make (map (fst o dest_Type o fst) dom_eqns ~~ typ_consts);
+      Symtab.make (map (fst o dest_Type o fst) dom_eqns ~~ defl_consts);
     val defl_tab' = Symtab.merge (K true) (defl_tab1, defl_tab2);
     fun free a = Free (Library.unprefix "'" a, deflT);
     fun mk_defl_spec (lhsT, rhsT) =
@@ -327,22 +327,22 @@
               defl_of_typ defl_tab' free rhsT);
     val defl_specs = map mk_defl_spec dom_eqns;
 
-    (* register recursive definition of type combinators *)
-    val typ_binds = map (Binding.suffix_name "_typ") dom_binds;
-    val (typ_unfold_thms, thy) = add_fixdefs (typ_binds ~~ defl_specs) thy;
+    (* register recursive definition of deflation combinators *)
+    val defl_binds = map (Binding.suffix_name "_defl") dom_binds;
+    val (defl_unfold_thms, thy) = add_fixdefs (defl_binds ~~ defl_specs) thy;
 
     (* define types using deflation combinators *)
-    fun make_repdef ((vs, tbind, mx, _), typ_const) thy =
+    fun make_repdef ((vs, tbind, mx, _), defl_const) thy =
       let
         fun tfree a = TFree (a, the (AList.lookup (op =) sorts a))
         val reps = map (mk_Rep_of o tfree) vs;
-        val defl = Library.foldl mk_capply (typ_const, reps);
+        val defl = Library.foldl mk_capply (defl_const, reps);
         val ((_, _, _, {REP, ...}), thy) =
           Repdef.add_repdef false NONE (tbind, vs, mx) defl NONE thy;
       in
         (REP, thy)
       end;
-    val (REP_thms, thy) = fold_map make_repdef (doms ~~ typ_consts) thy;
+    val (REP_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy;
 
     (* FIXME: use theory data for this *)
     val REP_simps = REP_thms @
@@ -355,7 +355,7 @@
         val goal = mk_eqs (mk_Rep_of lhsT, mk_Rep_of rhsT);
         val tac =
           simp_tac (HOL_basic_ss addsimps REP_simps) 1
-          THEN resolve_tac typ_unfold_thms 1;
+          THEN resolve_tac defl_unfold_thms 1;
       in
         Goal.prove_global thy [] [] goal (K tac)
       end;
diff -r 685bbf418cb7 -r 7e434813752f src/HOLCF/ex/Domain_Proofs.thy
--- a/src/HOLCF/ex/Domain_Proofs.thy	Thu Nov 19 08:08:57 2009 -0800
+++ b/src/HOLCF/ex/Domain_Proofs.thy	Thu Nov 19 08:22:00 2009 -0800
@@ -28,47 +28,47 @@
 text {* Start with the one-step non-recursive version *}
 
 definition
-  foo_bar_baz_typF ::
+  foo_bar_baz_deflF ::
     "TypeRep \<rightarrow> TypeRep \<times> TypeRep \<times> TypeRep \<rightarrow> TypeRep \<times> TypeRep \<times> TypeRep"
 where
-  "foo_bar_baz_typF = (\<Lambda> a. Abs_CFun (\<lambda>(t1, t2, t3). 
-    ( ssum_typ\<cdot>REP(one)\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>t2))
-    , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>t3)
-    , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>t1)))))"
+  "foo_bar_baz_deflF = (\<Lambda> a. Abs_CFun (\<lambda>(t1, t2, t3). 
+    ( ssum_defl\<cdot>REP(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t2))
+    , sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t3)
+    , sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(convex_defl\<cdot>t1)))))"
 
-lemma foo_bar_baz_typF_beta:
-  "foo_bar_baz_typF\<cdot>a\<cdot>t =
-    ( ssum_typ\<cdot>REP(one)\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(fst (snd t))))
-    , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(snd (snd t)))
-    , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>(fst t))))"
-unfolding foo_bar_baz_typF_def
+lemma foo_bar_baz_deflF_beta:
+  "foo_bar_baz_deflF\<cdot>a\<cdot>t =
+    ( ssum_defl\<cdot>REP(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(fst (snd t))))
+    , sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(snd (snd t)))
+    , sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(fst t))))"
+unfolding foo_bar_baz_deflF_def
 by (simp add: split_def)
 
 text {* Individual type combinators are projected from the fixed point. *}
 
-definition foo_typ :: "TypeRep \<rightarrow> TypeRep"
-where "foo_typ = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_typF\<cdot>a)))"
+definition foo_defl :: "TypeRep \<rightarrow> TypeRep"
+where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
 
-definition bar_typ :: "TypeRep \<rightarrow> TypeRep"
-where "bar_typ = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_typF\<cdot>a))))"
+definition bar_defl :: "TypeRep \<rightarrow> TypeRep"
+where "bar_defl = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
 
-definition baz_typ :: "TypeRep \<rightarrow> TypeRep"
-where "baz_typ = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_typF\<cdot>a))))"
+definition baz_defl :: "TypeRep \<rightarrow> TypeRep"
+where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
 
 text {* Unfold rules for each combinator. *}
 
-lemma foo_typ_unfold:
-  "foo_typ\<cdot>a = ssum_typ\<cdot>REP(one)\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(bar_typ\<cdot>a)))"
-unfolding foo_typ_def bar_typ_def baz_typ_def
-by (subst fix_eq, simp add: foo_bar_baz_typF_beta)
+lemma foo_defl_unfold:
+  "foo_defl\<cdot>a = ssum_defl\<cdot>REP(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
+unfolding foo_defl_def bar_defl_def baz_defl_def
+by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
 
-lemma bar_typ_unfold: "bar_typ\<cdot>a = sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(baz_typ\<cdot>a))"
-unfolding foo_typ_def bar_typ_def baz_typ_def
-by (subst fix_eq, simp add: foo_bar_baz_typF_beta)
+lemma bar_defl_unfold: "bar_defl\<cdot>a = sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(baz_defl\<cdot>a))"
+unfolding foo_defl_def bar_defl_def baz_defl_def
+by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
 
-lemma baz_typ_unfold: "baz_typ\<cdot>a = sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>(foo_typ\<cdot>a)))"
-unfolding foo_typ_def bar_typ_def baz_typ_def
-by (subst fix_eq, simp add: foo_bar_baz_typF_beta)
+lemma baz_defl_unfold: "baz_defl\<cdot>a = sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a)))"
+unfolding foo_defl_def bar_defl_def baz_defl_def
+by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
 
 text "The automation for the previous steps will be quite similar to
 how the fixrec package works."
@@ -79,13 +79,13 @@
 
 text {* Use @{text pcpodef} with the appropriate type combinator. *}
 
-pcpodef (open) 'a foo = "{x. x ::: foo_typ\<cdot>REP('a)}"
+pcpodef (open) 'a foo = "{x. x ::: foo_defl\<cdot>REP('a)}"
 by (simp_all add: adm_in_deflation)
 
-pcpodef (open) 'a bar = "{x. x ::: bar_typ\<cdot>REP('a)}"
+pcpodef (open) 'a bar = "{x. x ::: bar_defl\<cdot>REP('a)}"
 by (simp_all add: adm_in_deflation)
 
-pcpodef (open) 'a baz = "{x. x ::: baz_typ\<cdot>REP('a)}"
+pcpodef (open) 'a baz = "{x. x ::: baz_defl\<cdot>REP('a)}"
 by (simp_all add: adm_in_deflation)
 
 text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
@@ -97,10 +97,10 @@
 where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)"
 
 definition prj_foo :: "udom \<rightarrow> 'a foo"
-where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_typ\<cdot>REP('a))\<cdot>y))"
+where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>REP('a))\<cdot>y))"
 
 definition approx_foo :: "nat \<Rightarrow> 'a foo \<rightarrow> 'a foo"
-where "approx_foo \<equiv> repdef_approx Rep_foo Abs_foo (foo_typ\<cdot>REP('a))"
+where "approx_foo \<equiv> repdef_approx Rep_foo Abs_foo (foo_defl\<cdot>REP('a))"
 
 instance
 apply (rule typedef_rep_class)
@@ -120,10 +120,10 @@
 where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)"
 
 definition prj_bar :: "udom \<rightarrow> 'a bar"
-where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_typ\<cdot>REP('a))\<cdot>y))"
+where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>REP('a))\<cdot>y))"
 
 definition approx_bar :: "nat \<Rightarrow> 'a bar \<rightarrow> 'a bar"
-where "approx_bar \<equiv> repdef_approx Rep_bar Abs_bar (bar_typ\<cdot>REP('a))"
+where "approx_bar \<equiv> repdef_approx Rep_bar Abs_bar (bar_defl\<cdot>REP('a))"
 
 instance
 apply (rule typedef_rep_class)
@@ -143,10 +143,10 @@
 where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)"
 
 definition prj_baz :: "udom \<rightarrow> 'a baz"
-where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_typ\<cdot>REP('a))\<cdot>y))"
+where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>REP('a))\<cdot>y))"
 
 definition approx_baz :: "nat \<Rightarrow> 'a baz \<rightarrow> 'a baz"
-where "approx_baz \<equiv> repdef_approx Rep_baz Abs_baz (baz_typ\<cdot>REP('a))"
+where "approx_baz \<equiv> repdef_approx Rep_baz Abs_baz (baz_defl\<cdot>REP('a))"
 
 instance
 apply (rule typedef_rep_class)
@@ -161,7 +161,7 @@
 
 text {* Prove REP rules using lemma @{text typedef_REP}. *}
 
-lemma REP_foo: "REP('a foo) = foo_typ\<cdot>REP('a)"
+lemma REP_foo: "REP('a foo) = foo_defl\<cdot>REP('a)"
 apply (rule typedef_REP)
 apply (rule type_definition_foo)
 apply (rule below_foo_def)
@@ -169,7 +169,7 @@
 apply (rule prj_foo_def)
 done
 
-lemma REP_bar: "REP('a bar) = bar_typ\<cdot>REP('a)"
+lemma REP_bar: "REP('a bar) = bar_defl\<cdot>REP('a)"
 apply (rule typedef_REP)
 apply (rule type_definition_bar)
 apply (rule below_bar_def)
@@ -177,7 +177,7 @@
 apply (rule prj_bar_def)
 done
 
-lemma REP_baz: "REP('a baz) = baz_typ\<cdot>REP('a)"
+lemma REP_baz: "REP('a baz) = baz_defl\<cdot>REP('a)"
 apply (rule typedef_REP)
 apply (rule type_definition_baz)
 apply (rule below_baz_def)
@@ -189,15 +189,15 @@
 
 lemma REP_foo': "REP('a foo) = REP(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
 unfolding REP_foo REP_bar REP_baz REP_simps
-by (rule foo_typ_unfold)
+by (rule foo_defl_unfold)
 
 lemma REP_bar': "REP('a bar) = REP('a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom>)"
 unfolding REP_foo REP_bar REP_baz REP_simps
-by (rule bar_typ_unfold)
+by (rule bar_defl_unfold)
 
 lemma REP_baz': "REP('a baz) = REP('a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom>)"
 unfolding REP_foo REP_bar REP_baz REP_simps
-by (rule baz_typ_unfold)
+by (rule baz_defl_unfold)
 
 (********************************************************************)
 
@@ -318,17 +318,17 @@
 lemma isodefl_foo_bar_baz:
   assumes isodefl_d: "isodefl d t"
   shows
-  "isodefl (foo_map\<cdot>d) (foo_typ\<cdot>t) \<and>
-  isodefl (bar_map\<cdot>d) (bar_typ\<cdot>t) \<and>
-  isodefl (baz_map\<cdot>d) (baz_typ\<cdot>t)"
+  "isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and>
+  isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and>
+  isodefl (baz_map\<cdot>d) (baz_defl\<cdot>t)"
  apply (simp add: foo_map_def bar_map_def baz_map_def)
- apply (simp add: foo_typ_def bar_typ_def baz_typ_def)
+ apply (simp add: foo_defl_def bar_defl_def baz_defl_def)
  apply (rule parallel_fix_ind
-  [where F="foo_bar_baz_typF\<cdot>t" and G="foo_bar_baz_mapF\<cdot>d"])
+  [where F="foo_bar_baz_deflF\<cdot>t" and G="foo_bar_baz_mapF\<cdot>d"])
    apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id)
   apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms)
  apply (simp only: foo_bar_baz_mapF_beta
-                   foo_bar_baz_typF_beta
+                   foo_bar_baz_deflF_beta
                    fst_conv snd_conv)
  apply (elim conjE)
  apply (intro