replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
authorhuffman
Sun Dec 19 09:52:33 2010 -0800 (2010-12-19)
changeset 41290e9c9577d88b5
parent 41289 f655912ac235
child 41291 752d81c2ce25
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
src/HOL/HOLCF/Algebraic.thy
src/HOL/HOLCF/Domain.thy
src/HOL/HOLCF/Library/Defl_Bifinite.thy
src/HOL/HOLCF/Powerdomains.thy
src/HOL/HOLCF/Representable.thy
src/HOL/HOLCF/Tools/domaindef.ML
src/HOL/HOLCF/ex/Domain_Proofs.thy
     1.1 --- a/src/HOL/HOLCF/Algebraic.thy	Sun Dec 19 06:59:01 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Algebraic.thy	Sun Dec 19 09:52:33 2010 -0800
     1.3 @@ -215,4 +215,66 @@
     1.4  lemma cast_strict2 [simp]: "cast\<cdot>A\<cdot>\<bottom> = \<bottom>"
     1.5  by (rule cast.below [THEN UU_I])
     1.6  
     1.7 +subsection {* Deflation combinators *}
     1.8 +
     1.9 +definition
    1.10 +  "defl_fun1 e p f =
    1.11 +    defl.basis_fun (\<lambda>a.
    1.12 +      defl_principal (Abs_fin_defl
    1.13 +        (e oo f\<cdot>(Rep_fin_defl a) oo p)))"
    1.14 +
    1.15 +definition
    1.16 +  "defl_fun2 e p f =
    1.17 +    defl.basis_fun (\<lambda>a.
    1.18 +      defl.basis_fun (\<lambda>b.
    1.19 +        defl_principal (Abs_fin_defl
    1.20 +          (e oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo p))))"
    1.21 +
    1.22 +lemma cast_defl_fun1:
    1.23 +  assumes ep: "ep_pair e p"
    1.24 +  assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)"
    1.25 +  shows "cast\<cdot>(defl_fun1 e p f\<cdot>A) = e oo f\<cdot>(cast\<cdot>A) oo p"
    1.26 +proof -
    1.27 +  have 1: "\<And>a. finite_deflation (e oo f\<cdot>(Rep_fin_defl a) oo p)"
    1.28 +    apply (rule ep_pair.finite_deflation_e_d_p [OF ep])
    1.29 +    apply (rule f, rule finite_deflation_Rep_fin_defl)
    1.30 +    done
    1.31 +  show ?thesis
    1.32 +    by (induct A rule: defl.principal_induct, simp)
    1.33 +       (simp only: defl_fun1_def
    1.34 +                   defl.basis_fun_principal
    1.35 +                   defl.basis_fun_mono
    1.36 +                   defl.principal_mono
    1.37 +                   Abs_fin_defl_mono [OF 1 1]
    1.38 +                   monofun_cfun below_refl
    1.39 +                   Rep_fin_defl_mono
    1.40 +                   cast_defl_principal
    1.41 +                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
    1.42 +qed
    1.43 +
    1.44 +lemma cast_defl_fun2:
    1.45 +  assumes ep: "ep_pair e p"
    1.46 +  assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow>
    1.47 +                finite_deflation (f\<cdot>a\<cdot>b)"
    1.48 +  shows "cast\<cdot>(defl_fun2 e p f\<cdot>A\<cdot>B) = e oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo p"
    1.49 +proof -
    1.50 +  have 1: "\<And>a b. finite_deflation
    1.51 +      (e oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo p)"
    1.52 +    apply (rule ep_pair.finite_deflation_e_d_p [OF ep])
    1.53 +    apply (rule f, (rule finite_deflation_Rep_fin_defl)+)
    1.54 +    done
    1.55 +  show ?thesis
    1.56 +    apply (induct A rule: defl.principal_induct, simp)
    1.57 +    apply (induct B rule: defl.principal_induct, simp)
    1.58 +    by (simp only: defl_fun2_def
    1.59 +                   defl.basis_fun_principal
    1.60 +                   defl.basis_fun_mono
    1.61 +                   defl.principal_mono
    1.62 +                   Abs_fin_defl_mono [OF 1 1]
    1.63 +                   monofun_cfun below_refl
    1.64 +                   Rep_fin_defl_mono
    1.65 +                   cast_defl_principal
    1.66 +                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
    1.67 +qed
    1.68 +
    1.69  end
     2.1 --- a/src/HOL/HOLCF/Domain.thy	Sun Dec 19 06:59:01 2010 -0800
     2.2 +++ b/src/HOL/HOLCF/Domain.thy	Sun Dec 19 09:52:33 2010 -0800
     2.3 @@ -103,8 +103,8 @@
     2.4    assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)"
     2.5    assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))"
     2.6    assumes defl: "defl \<equiv> (\<lambda> a::'a itself. t)"
     2.7 -  assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
     2.8 -  assumes liftprj: "(liftprj :: udom \<rightarrow> 'a u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
     2.9 +  assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom) \<equiv> u_emb oo u_map\<cdot>emb"
    2.10 +  assumes liftprj: "(liftprj :: udom \<rightarrow> 'a u) \<equiv> u_map\<cdot>prj oo u_prj"
    2.11    assumes liftdefl: "(liftdefl :: 'a itself \<Rightarrow> _) \<equiv> (\<lambda>t. u_defl\<cdot>DEFL('a))"
    2.12    shows "OFCLASS('a, liftdomain_class)"
    2.13  using liftemb [THEN meta_eq_to_obj_eq]
     3.1 --- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Sun Dec 19 06:59:01 2010 -0800
     3.2 +++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Sun Dec 19 09:52:33 2010 -0800
     3.3 @@ -651,10 +651,10 @@
     3.4      (\<Squnion>i. defl_principal (Abs_fin_defl (emb oo defl_approx i oo prj)))"
     3.5  
     3.6  definition
     3.7 -  "(liftemb :: 'a defl u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
     3.8 +  "(liftemb :: 'a defl u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
     3.9  
    3.10  definition
    3.11 -  "(liftprj :: udom \<rightarrow> 'a defl u) = u_map\<cdot>prj oo udom_prj u_approx"
    3.12 +  "(liftprj :: udom \<rightarrow> 'a defl u) = u_map\<cdot>prj oo u_prj"
    3.13  
    3.14  definition
    3.15    "liftdefl (t::'a defl itself) = u_defl\<cdot>DEFL('a defl)"
     4.1 --- a/src/HOL/HOLCF/Powerdomains.thy	Sun Dec 19 06:59:01 2010 -0800
     4.2 +++ b/src/HOL/HOLCF/Powerdomains.thy	Sun Dec 19 09:52:33 2010 -0800
     4.3 @@ -10,54 +10,51 @@
     4.4  
     4.5  subsection {* Universal domain embeddings *}
     4.6  
     4.7 -definition upper_approx :: "nat \<Rightarrow> udom upper_pd \<rightarrow> udom upper_pd"
     4.8 -  where "upper_approx = (\<lambda>i. upper_map\<cdot>(udom_approx i))"
     4.9 +definition "upper_emb = udom_emb (\<lambda>i. upper_map\<cdot>(udom_approx i))"
    4.10 +definition "upper_prj = udom_prj (\<lambda>i. upper_map\<cdot>(udom_approx i))"
    4.11  
    4.12 -definition lower_approx :: "nat \<Rightarrow> udom lower_pd \<rightarrow> udom lower_pd"
    4.13 -  where "lower_approx = (\<lambda>i. lower_map\<cdot>(udom_approx i))"
    4.14 +definition "lower_emb = udom_emb (\<lambda>i. lower_map\<cdot>(udom_approx i))"
    4.15 +definition "lower_prj = udom_prj (\<lambda>i. lower_map\<cdot>(udom_approx i))"
    4.16  
    4.17 -definition convex_approx :: "nat \<Rightarrow> udom convex_pd \<rightarrow> udom convex_pd"
    4.18 -  where "convex_approx = (\<lambda>i. convex_map\<cdot>(udom_approx i))"
    4.19 +definition "convex_emb = udom_emb (\<lambda>i. convex_map\<cdot>(udom_approx i))"
    4.20 +definition "convex_prj = udom_prj (\<lambda>i. convex_map\<cdot>(udom_approx i))"
    4.21  
    4.22 -lemma upper_approx: "approx_chain upper_approx"
    4.23 -  using upper_map_ID finite_deflation_upper_map
    4.24 -  unfolding upper_approx_def by (rule approx_chain_lemma1)
    4.25 +lemma ep_pair_upper: "ep_pair upper_emb upper_prj"
    4.26 +  unfolding upper_emb_def upper_prj_def
    4.27 +  by (simp add: ep_pair_udom approx_chain_upper_map)
    4.28  
    4.29 -lemma lower_approx: "approx_chain lower_approx"
    4.30 -  using lower_map_ID finite_deflation_lower_map
    4.31 -  unfolding lower_approx_def by (rule approx_chain_lemma1)
    4.32 +lemma ep_pair_lower: "ep_pair lower_emb lower_prj"
    4.33 +  unfolding lower_emb_def lower_prj_def
    4.34 +  by (simp add: ep_pair_udom approx_chain_lower_map)
    4.35  
    4.36 -lemma convex_approx: "approx_chain convex_approx"
    4.37 -  using convex_map_ID finite_deflation_convex_map
    4.38 -  unfolding convex_approx_def by (rule approx_chain_lemma1)
    4.39 +lemma ep_pair_convex: "ep_pair convex_emb convex_prj"
    4.40 +  unfolding convex_emb_def convex_prj_def
    4.41 +  by (simp add: ep_pair_udom approx_chain_convex_map)
    4.42  
    4.43  subsection {* Deflation combinators *}
    4.44  
    4.45  definition upper_defl :: "udom defl \<rightarrow> udom defl"
    4.46 -  where "upper_defl = defl_fun1 upper_approx upper_map"
    4.47 +  where "upper_defl = defl_fun1 upper_emb upper_prj upper_map"
    4.48  
    4.49  definition lower_defl :: "udom defl \<rightarrow> udom defl"
    4.50 -  where "lower_defl = defl_fun1 lower_approx lower_map"
    4.51 +  where "lower_defl = defl_fun1 lower_emb lower_prj lower_map"
    4.52  
    4.53  definition convex_defl :: "udom defl \<rightarrow> udom defl"
    4.54 -  where "convex_defl = defl_fun1 convex_approx convex_map"
    4.55 +  where "convex_defl = defl_fun1 convex_emb convex_prj convex_map"
    4.56  
    4.57  lemma cast_upper_defl:
    4.58 -  "cast\<cdot>(upper_defl\<cdot>A) =
    4.59 -    udom_emb upper_approx oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj upper_approx"
    4.60 -using upper_approx finite_deflation_upper_map
    4.61 +  "cast\<cdot>(upper_defl\<cdot>A) = upper_emb oo upper_map\<cdot>(cast\<cdot>A) oo upper_prj"
    4.62 +using ep_pair_upper finite_deflation_upper_map
    4.63  unfolding upper_defl_def by (rule cast_defl_fun1)
    4.64  
    4.65  lemma cast_lower_defl:
    4.66 -  "cast\<cdot>(lower_defl\<cdot>A) =
    4.67 -    udom_emb lower_approx oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj lower_approx"
    4.68 -using lower_approx finite_deflation_lower_map
    4.69 +  "cast\<cdot>(lower_defl\<cdot>A) = lower_emb oo lower_map\<cdot>(cast\<cdot>A) oo lower_prj"
    4.70 +using ep_pair_lower finite_deflation_lower_map
    4.71  unfolding lower_defl_def by (rule cast_defl_fun1)
    4.72  
    4.73  lemma cast_convex_defl:
    4.74 -  "cast\<cdot>(convex_defl\<cdot>A) =
    4.75 -    udom_emb convex_approx oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj convex_approx"
    4.76 -using convex_approx finite_deflation_convex_map
    4.77 +  "cast\<cdot>(convex_defl\<cdot>A) = convex_emb oo convex_map\<cdot>(cast\<cdot>A) oo convex_prj"
    4.78 +using ep_pair_convex finite_deflation_convex_map
    4.79  unfolding convex_defl_def by (rule cast_defl_fun1)
    4.80  
    4.81  subsection {* Domain class instances *}
    4.82 @@ -66,19 +63,19 @@
    4.83  begin
    4.84  
    4.85  definition
    4.86 -  "emb = udom_emb upper_approx oo upper_map\<cdot>emb"
    4.87 +  "emb = upper_emb oo upper_map\<cdot>emb"
    4.88  
    4.89  definition
    4.90 -  "prj = upper_map\<cdot>prj oo udom_prj upper_approx"
    4.91 +  "prj = upper_map\<cdot>prj oo upper_prj"
    4.92  
    4.93  definition
    4.94    "defl (t::'a upper_pd itself) = upper_defl\<cdot>DEFL('a)"
    4.95  
    4.96  definition
    4.97 -  "(liftemb :: 'a upper_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
    4.98 +  "(liftemb :: 'a upper_pd u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
    4.99  
   4.100  definition
   4.101 -  "(liftprj :: udom \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj oo udom_prj u_approx"
   4.102 +  "(liftprj :: udom \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj oo u_prj"
   4.103  
   4.104  definition
   4.105    "liftdefl (t::'a upper_pd itself) = u_defl\<cdot>DEFL('a upper_pd)"
   4.106 @@ -88,8 +85,7 @@
   4.107  proof (rule liftdomain_class_intro)
   4.108    show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)"
   4.109      unfolding emb_upper_pd_def prj_upper_pd_def
   4.110 -    using ep_pair_udom [OF upper_approx]
   4.111 -    by (intro ep_pair_comp ep_pair_upper_map ep_pair_emb_prj)
   4.112 +    by (intro ep_pair_comp ep_pair_upper ep_pair_upper_map ep_pair_emb_prj)
   4.113  next
   4.114    show "cast\<cdot>DEFL('a upper_pd) = emb oo (prj :: udom \<rightarrow> 'a upper_pd)"
   4.115      unfolding emb_upper_pd_def prj_upper_pd_def defl_upper_pd_def cast_upper_defl
   4.116 @@ -102,19 +98,19 @@
   4.117  begin
   4.118  
   4.119  definition
   4.120 -  "emb = udom_emb lower_approx oo lower_map\<cdot>emb"
   4.121 +  "emb = lower_emb oo lower_map\<cdot>emb"
   4.122  
   4.123  definition
   4.124 -  "prj = lower_map\<cdot>prj oo udom_prj lower_approx"
   4.125 +  "prj = lower_map\<cdot>prj oo lower_prj"
   4.126  
   4.127  definition
   4.128    "defl (t::'a lower_pd itself) = lower_defl\<cdot>DEFL('a)"
   4.129  
   4.130  definition
   4.131 -  "(liftemb :: 'a lower_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
   4.132 +  "(liftemb :: 'a lower_pd u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
   4.133  
   4.134  definition
   4.135 -  "(liftprj :: udom \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj oo udom_prj u_approx"
   4.136 +  "(liftprj :: udom \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj oo u_prj"
   4.137  
   4.138  definition
   4.139    "liftdefl (t::'a lower_pd itself) = u_defl\<cdot>DEFL('a lower_pd)"
   4.140 @@ -124,8 +120,7 @@
   4.141  proof (rule liftdomain_class_intro)
   4.142    show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)"
   4.143      unfolding emb_lower_pd_def prj_lower_pd_def
   4.144 -    using ep_pair_udom [OF lower_approx]
   4.145 -    by (intro ep_pair_comp ep_pair_lower_map ep_pair_emb_prj)
   4.146 +    by (intro ep_pair_comp ep_pair_lower ep_pair_lower_map ep_pair_emb_prj)
   4.147  next
   4.148    show "cast\<cdot>DEFL('a lower_pd) = emb oo (prj :: udom \<rightarrow> 'a lower_pd)"
   4.149      unfolding emb_lower_pd_def prj_lower_pd_def defl_lower_pd_def cast_lower_defl
   4.150 @@ -138,19 +133,19 @@
   4.151  begin
   4.152  
   4.153  definition
   4.154 -  "emb = udom_emb convex_approx oo convex_map\<cdot>emb"
   4.155 +  "emb = convex_emb oo convex_map\<cdot>emb"
   4.156  
   4.157  definition
   4.158 -  "prj = convex_map\<cdot>prj oo udom_prj convex_approx"
   4.159 +  "prj = convex_map\<cdot>prj oo convex_prj"
   4.160  
   4.161  definition
   4.162    "defl (t::'a convex_pd itself) = convex_defl\<cdot>DEFL('a)"
   4.163  
   4.164  definition
   4.165 -  "(liftemb :: 'a convex_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
   4.166 +  "(liftemb :: 'a convex_pd u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
   4.167  
   4.168  definition
   4.169 -  "(liftprj :: udom \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj oo udom_prj u_approx"
   4.170 +  "(liftprj :: udom \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj oo u_prj"
   4.171  
   4.172  definition
   4.173    "liftdefl (t::'a convex_pd itself) = u_defl\<cdot>DEFL('a convex_pd)"
   4.174 @@ -160,8 +155,7 @@
   4.175  proof (rule liftdomain_class_intro)
   4.176    show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)"
   4.177      unfolding emb_convex_pd_def prj_convex_pd_def
   4.178 -    using ep_pair_udom [OF convex_approx]
   4.179 -    by (intro ep_pair_comp ep_pair_convex_map ep_pair_emb_prj)
   4.180 +    by (intro ep_pair_comp ep_pair_convex ep_pair_convex_map ep_pair_emb_prj)
   4.181  next
   4.182    show "cast\<cdot>DEFL('a convex_pd) = emb oo (prj :: udom \<rightarrow> 'a convex_pd)"
   4.183      unfolding emb_convex_pd_def prj_convex_pd_def defl_convex_pd_def cast_convex_defl
     5.1 --- a/src/HOL/HOLCF/Representable.thy	Sun Dec 19 06:59:01 2010 -0800
     5.2 +++ b/src/HOL/HOLCF/Representable.thy	Sun Dec 19 09:52:33 2010 -0800
     5.3 @@ -86,180 +86,89 @@
     5.4  instance predomain \<subseteq> profinite
     5.5  by default (rule approx_chain_ep_cast [OF predomain_ep cast_liftdefl])
     5.6  
     5.7 -subsection {* Chains of approx functions *}
     5.8 -
     5.9 -definition u_approx :: "nat \<Rightarrow> udom\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
    5.10 -  where "u_approx = (\<lambda>i. u_map\<cdot>(udom_approx i))"
    5.11 +subsection {* Universal domain ep-pairs *}
    5.12  
    5.13 -definition sfun_approx :: "nat \<Rightarrow> (udom \<rightarrow>! udom) \<rightarrow> (udom \<rightarrow>! udom)"
    5.14 -  where "sfun_approx = (\<lambda>i. sfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    5.15 +definition "u_emb = udom_emb (\<lambda>i. u_map\<cdot>(udom_approx i))"
    5.16 +definition "u_prj = udom_prj (\<lambda>i. u_map\<cdot>(udom_approx i))"
    5.17  
    5.18 -definition prod_approx :: "nat \<Rightarrow> udom \<times> udom \<rightarrow> udom \<times> udom"
    5.19 -  where "prod_approx = (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    5.20 +definition "prod_emb = udom_emb (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    5.21 +definition "prod_prj = udom_prj (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    5.22  
    5.23 -definition sprod_approx :: "nat \<Rightarrow> udom \<otimes> udom \<rightarrow> udom \<otimes> udom"
    5.24 -  where "sprod_approx = (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    5.25 -
    5.26 -definition ssum_approx :: "nat \<Rightarrow> udom \<oplus> udom \<rightarrow> udom \<oplus> udom"
    5.27 -  where "ssum_approx = (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    5.28 +definition "sprod_emb = udom_emb (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    5.29 +definition "sprod_prj = udom_prj (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    5.30  
    5.31 -lemma approx_chain_lemma1:
    5.32 -  assumes "m\<cdot>ID = ID"
    5.33 -  assumes "\<And>d. finite_deflation d \<Longrightarrow> finite_deflation (m\<cdot>d)"
    5.34 -  shows "approx_chain (\<lambda>i. m\<cdot>(udom_approx i))"
    5.35 -by (rule approx_chain.intro)
    5.36 -   (simp_all add: lub_distribs finite_deflation_udom_approx assms)
    5.37 +definition "ssum_emb = udom_emb (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    5.38 +definition "ssum_prj = udom_prj (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    5.39 +
    5.40 +definition "sfun_emb = udom_emb (\<lambda>i. sfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    5.41 +definition "sfun_prj = udom_prj (\<lambda>i. sfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    5.42  
    5.43 -lemma approx_chain_lemma2:
    5.44 -  assumes "m\<cdot>ID\<cdot>ID = ID"
    5.45 -  assumes "\<And>a b. \<lbrakk>finite_deflation a; finite_deflation b\<rbrakk>
    5.46 -    \<Longrightarrow> finite_deflation (m\<cdot>a\<cdot>b)"
    5.47 -  shows "approx_chain (\<lambda>i. m\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    5.48 -by (rule approx_chain.intro)
    5.49 -   (simp_all add: lub_distribs finite_deflation_udom_approx assms)
    5.50 +lemma ep_pair_u: "ep_pair u_emb u_prj"
    5.51 +  unfolding u_emb_def u_prj_def
    5.52 +  by (simp add: ep_pair_udom approx_chain_u_map)
    5.53  
    5.54 -lemma u_approx: "approx_chain u_approx"
    5.55 -using u_map_ID finite_deflation_u_map
    5.56 -unfolding u_approx_def by (rule approx_chain_lemma1)
    5.57 +lemma ep_pair_prod: "ep_pair prod_emb prod_prj"
    5.58 +  unfolding prod_emb_def prod_prj_def
    5.59 +  by (simp add: ep_pair_udom approx_chain_cprod_map)
    5.60  
    5.61 -lemma sfun_approx: "approx_chain sfun_approx"
    5.62 -using sfun_map_ID finite_deflation_sfun_map
    5.63 -unfolding sfun_approx_def by (rule approx_chain_lemma2)
    5.64 -
    5.65 -lemma prod_approx: "approx_chain prod_approx"
    5.66 -using cprod_map_ID finite_deflation_cprod_map
    5.67 -unfolding prod_approx_def by (rule approx_chain_lemma2)
    5.68 +lemma ep_pair_sprod: "ep_pair sprod_emb sprod_prj"
    5.69 +  unfolding sprod_emb_def sprod_prj_def
    5.70 +  by (simp add: ep_pair_udom approx_chain_sprod_map)
    5.71  
    5.72 -lemma sprod_approx: "approx_chain sprod_approx"
    5.73 -using sprod_map_ID finite_deflation_sprod_map
    5.74 -unfolding sprod_approx_def by (rule approx_chain_lemma2)
    5.75 +lemma ep_pair_ssum: "ep_pair ssum_emb ssum_prj"
    5.76 +  unfolding ssum_emb_def ssum_prj_def
    5.77 +  by (simp add: ep_pair_udom approx_chain_ssum_map)
    5.78  
    5.79 -lemma ssum_approx: "approx_chain ssum_approx"
    5.80 -using ssum_map_ID finite_deflation_ssum_map
    5.81 -unfolding ssum_approx_def by (rule approx_chain_lemma2)
    5.82 +lemma ep_pair_sfun: "ep_pair sfun_emb sfun_prj"
    5.83 +  unfolding sfun_emb_def sfun_prj_def
    5.84 +  by (simp add: ep_pair_udom approx_chain_sfun_map)
    5.85  
    5.86  subsection {* Type combinators *}
    5.87  
    5.88 -default_sort bifinite
    5.89 -
    5.90 -definition
    5.91 -  defl_fun1 ::
    5.92 -    "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (udom defl \<rightarrow> udom defl)"
    5.93 -where
    5.94 -  "defl_fun1 approx f =
    5.95 -    defl.basis_fun (\<lambda>a.
    5.96 -      defl_principal (Abs_fin_defl
    5.97 -        (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)))"
    5.98 +definition u_defl :: "udom defl \<rightarrow> udom defl"
    5.99 +  where "u_defl = defl_fun1 u_emb u_prj u_map"
   5.100  
   5.101 -definition
   5.102 -  defl_fun2 ::
   5.103 -    "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a))
   5.104 -      \<Rightarrow> (udom defl \<rightarrow> udom defl \<rightarrow> udom defl)"
   5.105 -where
   5.106 -  "defl_fun2 approx f =
   5.107 -    defl.basis_fun (\<lambda>a.
   5.108 -      defl.basis_fun (\<lambda>b.
   5.109 -        defl_principal (Abs_fin_defl
   5.110 -          (udom_emb approx oo
   5.111 -            f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx))))"
   5.112 +definition prod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
   5.113 +  where "prod_defl = defl_fun2 prod_emb prod_prj cprod_map"
   5.114  
   5.115 -lemma cast_defl_fun1:
   5.116 -  assumes approx: "approx_chain approx"
   5.117 -  assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)"
   5.118 -  shows "cast\<cdot>(defl_fun1 approx f\<cdot>A) = udom_emb approx oo f\<cdot>(cast\<cdot>A) oo udom_prj approx"
   5.119 -proof -
   5.120 -  have 1: "\<And>a. finite_deflation
   5.121 -        (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)"
   5.122 -    apply (rule ep_pair.finite_deflation_e_d_p)
   5.123 -    apply (rule ep_pair_udom [OF approx])
   5.124 -    apply (rule f, rule finite_deflation_Rep_fin_defl)
   5.125 -    done
   5.126 -  show ?thesis
   5.127 -    by (induct A rule: defl.principal_induct, simp)
   5.128 -       (simp only: defl_fun1_def
   5.129 -                   defl.basis_fun_principal
   5.130 -                   defl.basis_fun_mono
   5.131 -                   defl.principal_mono
   5.132 -                   Abs_fin_defl_mono [OF 1 1]
   5.133 -                   monofun_cfun below_refl
   5.134 -                   Rep_fin_defl_mono
   5.135 -                   cast_defl_principal
   5.136 -                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
   5.137 -qed
   5.138 +definition sprod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
   5.139 +  where "sprod_defl = defl_fun2 sprod_emb sprod_prj sprod_map"
   5.140  
   5.141 -lemma cast_defl_fun2:
   5.142 -  assumes approx: "approx_chain approx"
   5.143 -  assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow>
   5.144 -                finite_deflation (f\<cdot>a\<cdot>b)"
   5.145 -  shows "cast\<cdot>(defl_fun2 approx f\<cdot>A\<cdot>B) =
   5.146 -    udom_emb approx oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj approx"
   5.147 -proof -
   5.148 -  have 1: "\<And>a b. finite_deflation (udom_emb approx oo
   5.149 -      f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx)"
   5.150 -    apply (rule ep_pair.finite_deflation_e_d_p)
   5.151 -    apply (rule ep_pair_udom [OF approx])
   5.152 -    apply (rule f, (rule finite_deflation_Rep_fin_defl)+)
   5.153 -    done
   5.154 -  show ?thesis
   5.155 -    by (induct A B rule: defl.principal_induct2, simp, simp)
   5.156 -       (simp only: defl_fun2_def
   5.157 -                   defl.basis_fun_principal
   5.158 -                   defl.basis_fun_mono
   5.159 -                   defl.principal_mono
   5.160 -                   Abs_fin_defl_mono [OF 1 1]
   5.161 -                   monofun_cfun below_refl
   5.162 -                   Rep_fin_defl_mono
   5.163 -                   cast_defl_principal
   5.164 -                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
   5.165 -qed
   5.166 -
   5.167 -definition u_defl :: "udom defl \<rightarrow> udom defl"
   5.168 -  where "u_defl = defl_fun1 u_approx u_map"
   5.169 +definition ssum_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
   5.170 +where "ssum_defl = defl_fun2 ssum_emb ssum_prj ssum_map"
   5.171  
   5.172  definition sfun_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
   5.173 -  where "sfun_defl = defl_fun2 sfun_approx sfun_map"
   5.174 -
   5.175 -definition prod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
   5.176 -  where "prod_defl = defl_fun2 prod_approx cprod_map"
   5.177 -
   5.178 -definition sprod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
   5.179 -  where "sprod_defl = defl_fun2 sprod_approx sprod_map"
   5.180 -
   5.181 -definition ssum_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
   5.182 -where "ssum_defl = defl_fun2 ssum_approx ssum_map"
   5.183 +  where "sfun_defl = defl_fun2 sfun_emb sfun_prj sfun_map"
   5.184  
   5.185  lemma cast_u_defl:
   5.186 -  "cast\<cdot>(u_defl\<cdot>A) =
   5.187 -    udom_emb u_approx oo u_map\<cdot>(cast\<cdot>A) oo udom_prj u_approx"
   5.188 -using u_approx finite_deflation_u_map
   5.189 +  "cast\<cdot>(u_defl\<cdot>A) = u_emb oo u_map\<cdot>(cast\<cdot>A) oo u_prj"
   5.190 +using ep_pair_u finite_deflation_u_map
   5.191  unfolding u_defl_def by (rule cast_defl_fun1)
   5.192  
   5.193 -lemma cast_sfun_defl:
   5.194 -  "cast\<cdot>(sfun_defl\<cdot>A\<cdot>B) =
   5.195 -    udom_emb sfun_approx oo sfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj sfun_approx"
   5.196 -using sfun_approx finite_deflation_sfun_map
   5.197 -unfolding sfun_defl_def by (rule cast_defl_fun2)
   5.198 -
   5.199  lemma cast_prod_defl:
   5.200 -  "cast\<cdot>(prod_defl\<cdot>A\<cdot>B) = udom_emb prod_approx oo
   5.201 -    cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj prod_approx"
   5.202 -using prod_approx finite_deflation_cprod_map
   5.203 +  "cast\<cdot>(prod_defl\<cdot>A\<cdot>B) =
   5.204 +    prod_emb oo cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo prod_prj"
   5.205 +using ep_pair_prod finite_deflation_cprod_map
   5.206  unfolding prod_defl_def by (rule cast_defl_fun2)
   5.207  
   5.208  lemma cast_sprod_defl:
   5.209    "cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) =
   5.210 -    udom_emb sprod_approx oo
   5.211 -      sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo
   5.212 -        udom_prj sprod_approx"
   5.213 -using sprod_approx finite_deflation_sprod_map
   5.214 +    sprod_emb oo sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo sprod_prj"
   5.215 +using ep_pair_sprod finite_deflation_sprod_map
   5.216  unfolding sprod_defl_def by (rule cast_defl_fun2)
   5.217  
   5.218  lemma cast_ssum_defl:
   5.219    "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) =
   5.220 -    udom_emb ssum_approx oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj ssum_approx"
   5.221 -using ssum_approx finite_deflation_ssum_map
   5.222 +    ssum_emb oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo ssum_prj"
   5.223 +using ep_pair_ssum finite_deflation_ssum_map
   5.224  unfolding ssum_defl_def by (rule cast_defl_fun2)
   5.225  
   5.226 +lemma cast_sfun_defl:
   5.227 +  "cast\<cdot>(sfun_defl\<cdot>A\<cdot>B) =
   5.228 +    sfun_emb oo sfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo sfun_prj"
   5.229 +using ep_pair_sfun finite_deflation_sfun_map
   5.230 +unfolding sfun_defl_def by (rule cast_defl_fun2)
   5.231 +
   5.232  subsection {* Lemma for proving domain instances *}
   5.233  
   5.234  text {*
   5.235 @@ -268,8 +177,8 @@
   5.236  *}
   5.237  
   5.238  class liftdomain = "domain" +
   5.239 -  assumes liftemb_eq: "liftemb = udom_emb u_approx oo u_map\<cdot>emb"
   5.240 -  assumes liftprj_eq: "liftprj = u_map\<cdot>prj oo udom_prj u_approx"
   5.241 +  assumes liftemb_eq: "liftemb = u_emb oo u_map\<cdot>emb"
   5.242 +  assumes liftprj_eq: "liftprj = u_map\<cdot>prj oo u_prj"
   5.243    assumes liftdefl_eq: "liftdefl TYPE('a::cpo) = u_defl\<cdot>DEFL('a)"
   5.244  
   5.245  text {* Temporarily relax type constraints. *}
   5.246 @@ -287,8 +196,8 @@
   5.247  default_sort pcpo
   5.248  
   5.249  lemma liftdomain_class_intro:
   5.250 -  assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
   5.251 -  assumes liftprj: "(liftprj :: udom \<rightarrow> 'a u) = u_map\<cdot>prj oo udom_prj u_approx"
   5.252 +  assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
   5.253 +  assumes liftprj: "(liftprj :: udom \<rightarrow> 'a u) = u_map\<cdot>prj oo u_prj"
   5.254    assumes liftdefl: "liftdefl TYPE('a) = u_defl\<cdot>DEFL('a)"
   5.255    assumes ep_pair: "ep_pair emb (prj :: udom \<rightarrow> 'a)"
   5.256    assumes cast_defl: "cast\<cdot>DEFL('a) = emb oo (prj :: udom \<rightarrow> 'a)"
   5.257 @@ -296,7 +205,7 @@
   5.258  proof
   5.259    show "ep_pair liftemb (liftprj :: udom \<rightarrow> 'a u)"
   5.260      unfolding liftemb liftprj
   5.261 -    by (intro ep_pair_comp ep_pair_u_map ep_pair ep_pair_udom u_approx)
   5.262 +    by (intro ep_pair_comp ep_pair_u_map ep_pair ep_pair_u)
   5.263    show "cast\<cdot>LIFTDEFL('a) = liftemb oo (liftprj :: udom \<rightarrow> 'a u)"
   5.264      unfolding liftemb liftprj liftdefl
   5.265      by (simp add: cfcomp1 cast_u_defl cast_defl u_map_map)
   5.266 @@ -332,10 +241,10 @@
   5.267    "defl (t::udom itself) = (\<Squnion>i. defl_principal (Abs_fin_defl (udom_approx i)))"
   5.268  
   5.269  definition
   5.270 -  "(liftemb :: udom u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
   5.271 +  "(liftemb :: udom u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
   5.272  
   5.273  definition
   5.274 -  "(liftprj :: udom \<rightarrow> udom u) = u_map\<cdot>prj oo udom_prj u_approx"
   5.275 +  "(liftprj :: udom \<rightarrow> udom u) = u_map\<cdot>prj oo u_prj"
   5.276  
   5.277  definition
   5.278    "liftdefl (t::udom itself) = u_defl\<cdot>DEFL(udom)"
   5.279 @@ -376,10 +285,10 @@
   5.280    "defl (t::'a u itself) = LIFTDEFL('a)"
   5.281  
   5.282  definition
   5.283 -  "(liftemb :: 'a u u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
   5.284 +  "(liftemb :: 'a u u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
   5.285  
   5.286  definition
   5.287 -  "(liftprj :: udom \<rightarrow> 'a u u) = u_map\<cdot>prj oo udom_prj u_approx"
   5.288 +  "(liftprj :: udom \<rightarrow> 'a u u) = u_map\<cdot>prj oo u_prj"
   5.289  
   5.290  definition
   5.291    "liftdefl (t::'a u itself) = u_defl\<cdot>DEFL('a u)"
   5.292 @@ -406,19 +315,19 @@
   5.293  begin
   5.294  
   5.295  definition
   5.296 -  "emb = udom_emb sfun_approx oo sfun_map\<cdot>prj\<cdot>emb"
   5.297 +  "emb = sfun_emb oo sfun_map\<cdot>prj\<cdot>emb"
   5.298  
   5.299  definition
   5.300 -  "prj = sfun_map\<cdot>emb\<cdot>prj oo udom_prj sfun_approx"
   5.301 +  "prj = sfun_map\<cdot>emb\<cdot>prj oo sfun_prj"
   5.302  
   5.303  definition
   5.304    "defl (t::('a \<rightarrow>! 'b) itself) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
   5.305  
   5.306  definition
   5.307 -  "(liftemb :: ('a \<rightarrow>! 'b) u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
   5.308 +  "(liftemb :: ('a \<rightarrow>! 'b) u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
   5.309  
   5.310  definition
   5.311 -  "(liftprj :: udom \<rightarrow> ('a \<rightarrow>! 'b) u) = u_map\<cdot>prj oo udom_prj u_approx"
   5.312 +  "(liftprj :: udom \<rightarrow> ('a \<rightarrow>! 'b) u) = u_map\<cdot>prj oo u_prj"
   5.313  
   5.314  definition
   5.315    "liftdefl (t::('a \<rightarrow>! 'b) itself) = u_defl\<cdot>DEFL('a \<rightarrow>! 'b)"
   5.316 @@ -428,8 +337,7 @@
   5.317  proof (rule liftdomain_class_intro)
   5.318    show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
   5.319      unfolding emb_sfun_def prj_sfun_def
   5.320 -    using ep_pair_udom [OF sfun_approx]
   5.321 -    by (intro ep_pair_comp ep_pair_sfun_map ep_pair_emb_prj)
   5.322 +    by (intro ep_pair_comp ep_pair_sfun ep_pair_sfun_map ep_pair_emb_prj)
   5.323    show "cast\<cdot>DEFL('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
   5.324      unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl
   5.325      by (simp add: cast_DEFL oo_def sfun_eq_iff sfun_map_map)
   5.326 @@ -456,10 +364,10 @@
   5.327    "defl (t::('a \<rightarrow> 'b) itself) = DEFL('a u \<rightarrow>! 'b)"
   5.328  
   5.329  definition
   5.330 -  "(liftemb :: ('a \<rightarrow> 'b) u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
   5.331 +  "(liftemb :: ('a \<rightarrow> 'b) u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
   5.332  
   5.333  definition
   5.334 -  "(liftprj :: udom \<rightarrow> ('a \<rightarrow> 'b) u) = u_map\<cdot>prj oo udom_prj u_approx"
   5.335 +  "(liftprj :: udom \<rightarrow> ('a \<rightarrow> 'b) u) = u_map\<cdot>prj oo u_prj"
   5.336  
   5.337  definition
   5.338    "liftdefl (t::('a \<rightarrow> 'b) itself) = u_defl\<cdot>DEFL('a \<rightarrow> 'b)"
   5.339 @@ -489,19 +397,19 @@
   5.340  begin
   5.341  
   5.342  definition
   5.343 -  "emb = udom_emb sprod_approx oo sprod_map\<cdot>emb\<cdot>emb"
   5.344 +  "emb = sprod_emb oo sprod_map\<cdot>emb\<cdot>emb"
   5.345  
   5.346  definition
   5.347 -  "prj = sprod_map\<cdot>prj\<cdot>prj oo udom_prj sprod_approx"
   5.348 +  "prj = sprod_map\<cdot>prj\<cdot>prj oo sprod_prj"
   5.349  
   5.350  definition
   5.351    "defl (t::('a \<otimes> 'b) itself) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
   5.352  
   5.353  definition
   5.354 -  "(liftemb :: ('a \<otimes> 'b) u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
   5.355 +  "(liftemb :: ('a \<otimes> 'b) u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
   5.356  
   5.357  definition
   5.358 -  "(liftprj :: udom \<rightarrow> ('a \<otimes> 'b) u) = u_map\<cdot>prj oo udom_prj u_approx"
   5.359 +  "(liftprj :: udom \<rightarrow> ('a \<otimes> 'b) u) = u_map\<cdot>prj oo u_prj"
   5.360  
   5.361  definition
   5.362    "liftdefl (t::('a \<otimes> 'b) itself) = u_defl\<cdot>DEFL('a \<otimes> 'b)"
   5.363 @@ -511,8 +419,7 @@
   5.364  proof (rule liftdomain_class_intro)
   5.365    show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
   5.366      unfolding emb_sprod_def prj_sprod_def
   5.367 -    using ep_pair_udom [OF sprod_approx]
   5.368 -    by (intro ep_pair_comp ep_pair_sprod_map ep_pair_emb_prj)
   5.369 +    by (intro ep_pair_comp ep_pair_sprod ep_pair_sprod_map ep_pair_emb_prj)
   5.370  next
   5.371    show "cast\<cdot>DEFL('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
   5.372      unfolding emb_sprod_def prj_sprod_def defl_sprod_def cast_sprod_defl
   5.373 @@ -556,10 +463,10 @@
   5.374  begin
   5.375  
   5.376  definition
   5.377 -  "emb = udom_emb prod_approx oo cprod_map\<cdot>emb\<cdot>emb"
   5.378 +  "emb = prod_emb oo cprod_map\<cdot>emb\<cdot>emb"
   5.379  
   5.380  definition
   5.381 -  "prj = cprod_map\<cdot>prj\<cdot>prj oo udom_prj prod_approx"
   5.382 +  "prj = cprod_map\<cdot>prj\<cdot>prj oo prod_prj"
   5.383  
   5.384  definition
   5.385    "defl (t::('a \<times> 'b) itself) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
   5.386 @@ -567,8 +474,7 @@
   5.387  instance proof
   5.388    show "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)"
   5.389      unfolding emb_prod_def prj_prod_def
   5.390 -    using ep_pair_udom [OF prod_approx]
   5.391 -    by (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj)
   5.392 +    by (intro ep_pair_comp ep_pair_prod ep_pair_cprod_map ep_pair_emb_prj)
   5.393  next
   5.394    show "cast\<cdot>DEFL('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
   5.395      unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl
   5.396 @@ -600,10 +506,10 @@
   5.397    "defl (t::unit itself) = \<bottom>"
   5.398  
   5.399  definition
   5.400 -  "(liftemb :: unit u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
   5.401 +  "(liftemb :: unit u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
   5.402  
   5.403  definition
   5.404 -  "(liftprj :: udom \<rightarrow> unit u) = u_map\<cdot>prj oo udom_prj u_approx"
   5.405 +  "(liftprj :: udom \<rightarrow> unit u) = u_map\<cdot>prj oo u_prj"
   5.406  
   5.407  definition
   5.408    "liftdefl (t::unit itself) = u_defl\<cdot>DEFL(unit)"
   5.409 @@ -668,19 +574,19 @@
   5.410  begin
   5.411  
   5.412  definition
   5.413 -  "emb = udom_emb ssum_approx oo ssum_map\<cdot>emb\<cdot>emb"
   5.414 +  "emb = ssum_emb oo ssum_map\<cdot>emb\<cdot>emb"
   5.415  
   5.416  definition
   5.417 -  "prj = ssum_map\<cdot>prj\<cdot>prj oo udom_prj ssum_approx"
   5.418 +  "prj = ssum_map\<cdot>prj\<cdot>prj oo ssum_prj"
   5.419  
   5.420  definition
   5.421    "defl (t::('a \<oplus> 'b) itself) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
   5.422  
   5.423  definition
   5.424 -  "(liftemb :: ('a \<oplus> 'b) u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
   5.425 +  "(liftemb :: ('a \<oplus> 'b) u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
   5.426  
   5.427  definition
   5.428 -  "(liftprj :: udom \<rightarrow> ('a \<oplus> 'b) u) = u_map\<cdot>prj oo udom_prj u_approx"
   5.429 +  "(liftprj :: udom \<rightarrow> ('a \<oplus> 'b) u) = u_map\<cdot>prj oo u_prj"
   5.430  
   5.431  definition
   5.432    "liftdefl (t::('a \<oplus> 'b) itself) = u_defl\<cdot>DEFL('a \<oplus> 'b)"
   5.433 @@ -690,8 +596,7 @@
   5.434  proof (rule liftdomain_class_intro)
   5.435    show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
   5.436      unfolding emb_ssum_def prj_ssum_def
   5.437 -    using ep_pair_udom [OF ssum_approx]
   5.438 -    by (intro ep_pair_comp ep_pair_ssum_map ep_pair_emb_prj)
   5.439 +    by (intro ep_pair_comp ep_pair_ssum ep_pair_ssum_map ep_pair_emb_prj)
   5.440    show "cast\<cdot>DEFL('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
   5.441      unfolding emb_ssum_def prj_ssum_def defl_ssum_def cast_ssum_defl
   5.442      by (simp add: cast_DEFL oo_def cfun_eq_iff ssum_map_map)
   5.443 @@ -718,10 +623,10 @@
   5.444    "defl (t::'a lift itself) = DEFL('a discr u)"
   5.445  
   5.446  definition
   5.447 -  "(liftemb :: 'a lift u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
   5.448 +  "(liftemb :: 'a lift u \<rightarrow> udom) = u_emb oo u_map\<cdot>emb"
   5.449  
   5.450  definition
   5.451 -  "(liftprj :: udom \<rightarrow> 'a lift u) = u_map\<cdot>prj oo udom_prj u_approx"
   5.452 +  "(liftprj :: udom \<rightarrow> 'a lift u) = u_map\<cdot>prj oo u_prj"
   5.453  
   5.454  definition
   5.455    "liftdefl (t::'a lift itself) = u_defl\<cdot>DEFL('a lift)"
     6.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML	Sun Dec 19 06:59:01 2010 -0800
     6.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML	Sun Dec 19 09:52:33 2010 -0800
     6.3 @@ -130,10 +130,10 @@
     6.4        Abs ("x", Term.itselfT newT, defl))
     6.5      val liftemb_eqn =
     6.6        Logic.mk_equals (liftemb_const newT,
     6.7 -      mk_cfcomp (@{term "udom_emb u_approx"}, mk_u_map (emb_const newT)))
     6.8 +      mk_cfcomp (@{const u_emb}, mk_u_map (emb_const newT)))
     6.9      val liftprj_eqn =
    6.10        Logic.mk_equals (liftprj_const newT,
    6.11 -      mk_cfcomp (mk_u_map (prj_const newT), @{term "udom_prj u_approx"}))
    6.12 +      mk_cfcomp (mk_u_map (prj_const newT), @{const u_prj}))
    6.13      val liftdefl_eqn =
    6.14        Logic.mk_equals (liftdefl_const newT,
    6.15          Abs ("t", Term.itselfT newT,
     7.1 --- a/src/HOL/HOLCF/ex/Domain_Proofs.thy	Sun Dec 19 06:59:01 2010 -0800
     7.2 +++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy	Sun Dec 19 09:52:33 2010 -0800
     7.3 @@ -107,10 +107,10 @@
     7.4  where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>LIFTDEFL('a)"
     7.5  
     7.6  definition
     7.7 -  "(liftemb :: 'a foo u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
     7.8 +  "(liftemb :: 'a foo u \<rightarrow> udom) \<equiv> u_emb oo u_map\<cdot>emb"
     7.9  
    7.10  definition
    7.11 -  "(liftprj :: udom \<rightarrow> 'a foo u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
    7.12 +  "(liftprj :: udom \<rightarrow> 'a foo u) \<equiv> u_map\<cdot>prj oo u_prj"
    7.13  
    7.14  definition
    7.15    "liftdefl \<equiv> \<lambda>(t::'a foo itself). u_defl\<cdot>DEFL('a foo)"
    7.16 @@ -142,10 +142,10 @@
    7.17  where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>LIFTDEFL('a)"
    7.18  
    7.19  definition
    7.20 -  "(liftemb :: 'a bar u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
    7.21 +  "(liftemb :: 'a bar u \<rightarrow> udom) \<equiv> u_emb oo u_map\<cdot>emb"
    7.22  
    7.23  definition
    7.24 -  "(liftprj :: udom \<rightarrow> 'a bar u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
    7.25 +  "(liftprj :: udom \<rightarrow> 'a bar u) \<equiv> u_map\<cdot>prj oo u_prj"
    7.26  
    7.27  definition
    7.28    "liftdefl \<equiv> \<lambda>(t::'a bar itself). u_defl\<cdot>DEFL('a bar)"
    7.29 @@ -177,10 +177,10 @@
    7.30  where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>LIFTDEFL('a)"
    7.31  
    7.32  definition
    7.33 -  "(liftemb :: 'a baz u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
    7.34 +  "(liftemb :: 'a baz u \<rightarrow> udom) \<equiv> u_emb oo u_map\<cdot>emb"
    7.35  
    7.36  definition
    7.37 -  "(liftprj :: udom \<rightarrow> 'a baz u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
    7.38 +  "(liftprj :: udom \<rightarrow> 'a baz u) \<equiv> u_map\<cdot>prj oo u_prj"
    7.39  
    7.40  definition
    7.41    "liftdefl \<equiv> \<lambda>(t::'a baz itself). u_defl\<cdot>DEFL('a baz)"