author huffman Sun Dec 19 09:52:33 2010 -0800 (2010-12-19) changeset 41290 e9c9577d88b5 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 file | annotate | diff | revisions src/HOL/HOLCF/Domain.thy file | annotate | diff | revisions src/HOL/HOLCF/Library/Defl_Bifinite.thy file | annotate | diff | revisions src/HOL/HOLCF/Powerdomains.thy file | annotate | diff | revisions src/HOL/HOLCF/Representable.thy file | annotate | diff | revisions src/HOL/HOLCF/Tools/domaindef.ML file | annotate | diff | revisions src/HOL/HOLCF/ex/Domain_Proofs.thy file | annotate | diff | revisions
```     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)"
```