# HG changeset patch # User huffman # Date 1292781153 28800 # Node ID e9c9577d88b5f2a418690c74ef2b96e8da074047 # Parent f655912ac235e3df4ee757a78e942e4e6e8cfca9 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings diff -r f655912ac235 -r e9c9577d88b5 src/HOL/HOLCF/Algebraic.thy --- a/src/HOL/HOLCF/Algebraic.thy Sun Dec 19 06:59:01 2010 -0800 +++ b/src/HOL/HOLCF/Algebraic.thy Sun Dec 19 09:52:33 2010 -0800 @@ -215,4 +215,66 @@ lemma cast_strict2 [simp]: "cast\A\\ = \" by (rule cast.below [THEN UU_I]) +subsection {* Deflation combinators *} + +definition + "defl_fun1 e p f = + defl.basis_fun (\a. + defl_principal (Abs_fin_defl + (e oo f\(Rep_fin_defl a) oo p)))" + +definition + "defl_fun2 e p f = + defl.basis_fun (\a. + defl.basis_fun (\b. + defl_principal (Abs_fin_defl + (e oo f\(Rep_fin_defl a)\(Rep_fin_defl b) oo p))))" + +lemma cast_defl_fun1: + assumes ep: "ep_pair e p" + assumes f: "\a. finite_deflation a \ finite_deflation (f\a)" + shows "cast\(defl_fun1 e p f\A) = e oo f\(cast\A) oo p" +proof - + have 1: "\a. finite_deflation (e oo f\(Rep_fin_defl a) oo p)" + apply (rule ep_pair.finite_deflation_e_d_p [OF ep]) + apply (rule f, rule finite_deflation_Rep_fin_defl) + done + show ?thesis + by (induct A rule: defl.principal_induct, simp) + (simp only: defl_fun1_def + defl.basis_fun_principal + defl.basis_fun_mono + defl.principal_mono + Abs_fin_defl_mono [OF 1 1] + monofun_cfun below_refl + Rep_fin_defl_mono + cast_defl_principal + Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1]) +qed + +lemma cast_defl_fun2: + assumes ep: "ep_pair e p" + assumes f: "\a b. finite_deflation a \ finite_deflation b \ + finite_deflation (f\a\b)" + shows "cast\(defl_fun2 e p f\A\B) = e oo f\(cast\A)\(cast\B) oo p" +proof - + have 1: "\a b. finite_deflation + (e oo f\(Rep_fin_defl a)\(Rep_fin_defl b) oo p)" + apply (rule ep_pair.finite_deflation_e_d_p [OF ep]) + apply (rule f, (rule finite_deflation_Rep_fin_defl)+) + done + show ?thesis + apply (induct A rule: defl.principal_induct, simp) + apply (induct B rule: defl.principal_induct, simp) + by (simp only: defl_fun2_def + defl.basis_fun_principal + defl.basis_fun_mono + defl.principal_mono + Abs_fin_defl_mono [OF 1 1] + monofun_cfun below_refl + Rep_fin_defl_mono + cast_defl_principal + Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1]) +qed + end diff -r f655912ac235 -r e9c9577d88b5 src/HOL/HOLCF/Domain.thy --- a/src/HOL/HOLCF/Domain.thy Sun Dec 19 06:59:01 2010 -0800 +++ b/src/HOL/HOLCF/Domain.thy Sun Dec 19 09:52:33 2010 -0800 @@ -103,8 +103,8 @@ assumes emb: "emb \ (\ x. Rep x)" assumes prj: "prj \ (\ x. Abs (cast\t\x))" assumes defl: "defl \ (\ a::'a itself. t)" - assumes liftemb: "(liftemb :: 'a u \ udom) \ udom_emb u_approx oo u_map\emb" - assumes liftprj: "(liftprj :: udom \ 'a u) \ u_map\prj oo udom_prj u_approx" + assumes liftemb: "(liftemb :: 'a u \ udom) \ u_emb oo u_map\emb" + assumes liftprj: "(liftprj :: udom \ 'a u) \ u_map\prj oo u_prj" assumes liftdefl: "(liftdefl :: 'a itself \ _) \ (\t. u_defl\DEFL('a))" shows "OFCLASS('a, liftdomain_class)" using liftemb [THEN meta_eq_to_obj_eq] diff -r f655912ac235 -r e9c9577d88b5 src/HOL/HOLCF/Library/Defl_Bifinite.thy --- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy Sun Dec 19 06:59:01 2010 -0800 +++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy Sun Dec 19 09:52:33 2010 -0800 @@ -651,10 +651,10 @@ (\i. defl_principal (Abs_fin_defl (emb oo defl_approx i oo prj)))" definition - "(liftemb :: 'a defl u \ udom) = udom_emb u_approx oo u_map\emb" + "(liftemb :: 'a defl u \ udom) = u_emb oo u_map\emb" definition - "(liftprj :: udom \ 'a defl u) = u_map\prj oo udom_prj u_approx" + "(liftprj :: udom \ 'a defl u) = u_map\prj oo u_prj" definition "liftdefl (t::'a defl itself) = u_defl\DEFL('a defl)" diff -r f655912ac235 -r e9c9577d88b5 src/HOL/HOLCF/Powerdomains.thy --- a/src/HOL/HOLCF/Powerdomains.thy Sun Dec 19 06:59:01 2010 -0800 +++ b/src/HOL/HOLCF/Powerdomains.thy Sun Dec 19 09:52:33 2010 -0800 @@ -10,54 +10,51 @@ subsection {* Universal domain embeddings *} -definition upper_approx :: "nat \ udom upper_pd \ udom upper_pd" - where "upper_approx = (\i. upper_map\(udom_approx i))" +definition "upper_emb = udom_emb (\i. upper_map\(udom_approx i))" +definition "upper_prj = udom_prj (\i. upper_map\(udom_approx i))" -definition lower_approx :: "nat \ udom lower_pd \ udom lower_pd" - where "lower_approx = (\i. lower_map\(udom_approx i))" +definition "lower_emb = udom_emb (\i. lower_map\(udom_approx i))" +definition "lower_prj = udom_prj (\i. lower_map\(udom_approx i))" -definition convex_approx :: "nat \ udom convex_pd \ udom convex_pd" - where "convex_approx = (\i. convex_map\(udom_approx i))" +definition "convex_emb = udom_emb (\i. convex_map\(udom_approx i))" +definition "convex_prj = udom_prj (\i. convex_map\(udom_approx i))" -lemma upper_approx: "approx_chain upper_approx" - using upper_map_ID finite_deflation_upper_map - unfolding upper_approx_def by (rule approx_chain_lemma1) +lemma ep_pair_upper: "ep_pair upper_emb upper_prj" + unfolding upper_emb_def upper_prj_def + by (simp add: ep_pair_udom approx_chain_upper_map) -lemma lower_approx: "approx_chain lower_approx" - using lower_map_ID finite_deflation_lower_map - unfolding lower_approx_def by (rule approx_chain_lemma1) +lemma ep_pair_lower: "ep_pair lower_emb lower_prj" + unfolding lower_emb_def lower_prj_def + by (simp add: ep_pair_udom approx_chain_lower_map) -lemma convex_approx: "approx_chain convex_approx" - using convex_map_ID finite_deflation_convex_map - unfolding convex_approx_def by (rule approx_chain_lemma1) +lemma ep_pair_convex: "ep_pair convex_emb convex_prj" + unfolding convex_emb_def convex_prj_def + by (simp add: ep_pair_udom approx_chain_convex_map) subsection {* Deflation combinators *} definition upper_defl :: "udom defl \ udom defl" - where "upper_defl = defl_fun1 upper_approx upper_map" + where "upper_defl = defl_fun1 upper_emb upper_prj upper_map" definition lower_defl :: "udom defl \ udom defl" - where "lower_defl = defl_fun1 lower_approx lower_map" + where "lower_defl = defl_fun1 lower_emb lower_prj lower_map" definition convex_defl :: "udom defl \ udom defl" - where "convex_defl = defl_fun1 convex_approx convex_map" + where "convex_defl = defl_fun1 convex_emb convex_prj convex_map" lemma cast_upper_defl: - "cast\(upper_defl\A) = - udom_emb upper_approx oo upper_map\(cast\A) oo udom_prj upper_approx" -using upper_approx finite_deflation_upper_map + "cast\(upper_defl\A) = upper_emb oo upper_map\(cast\A) oo upper_prj" +using ep_pair_upper finite_deflation_upper_map unfolding upper_defl_def by (rule cast_defl_fun1) lemma cast_lower_defl: - "cast\(lower_defl\A) = - udom_emb lower_approx oo lower_map\(cast\A) oo udom_prj lower_approx" -using lower_approx finite_deflation_lower_map + "cast\(lower_defl\A) = lower_emb oo lower_map\(cast\A) oo lower_prj" +using ep_pair_lower finite_deflation_lower_map unfolding lower_defl_def by (rule cast_defl_fun1) lemma cast_convex_defl: - "cast\(convex_defl\A) = - udom_emb convex_approx oo convex_map\(cast\A) oo udom_prj convex_approx" -using convex_approx finite_deflation_convex_map + "cast\(convex_defl\A) = convex_emb oo convex_map\(cast\A) oo convex_prj" +using ep_pair_convex finite_deflation_convex_map unfolding convex_defl_def by (rule cast_defl_fun1) subsection {* Domain class instances *} @@ -66,19 +63,19 @@ begin definition - "emb = udom_emb upper_approx oo upper_map\emb" + "emb = upper_emb oo upper_map\emb" definition - "prj = upper_map\prj oo udom_prj upper_approx" + "prj = upper_map\prj oo upper_prj" definition "defl (t::'a upper_pd itself) = upper_defl\DEFL('a)" definition - "(liftemb :: 'a upper_pd u \ udom) = udom_emb u_approx oo u_map\emb" + "(liftemb :: 'a upper_pd u \ udom) = u_emb oo u_map\emb" definition - "(liftprj :: udom \ 'a upper_pd u) = u_map\prj oo udom_prj u_approx" + "(liftprj :: udom \ 'a upper_pd u) = u_map\prj oo u_prj" definition "liftdefl (t::'a upper_pd itself) = u_defl\DEFL('a upper_pd)" @@ -88,8 +85,7 @@ proof (rule liftdomain_class_intro) show "ep_pair emb (prj :: udom \ 'a upper_pd)" unfolding emb_upper_pd_def prj_upper_pd_def - using ep_pair_udom [OF upper_approx] - by (intro ep_pair_comp ep_pair_upper_map ep_pair_emb_prj) + by (intro ep_pair_comp ep_pair_upper ep_pair_upper_map ep_pair_emb_prj) next show "cast\DEFL('a upper_pd) = emb oo (prj :: udom \ 'a upper_pd)" unfolding emb_upper_pd_def prj_upper_pd_def defl_upper_pd_def cast_upper_defl @@ -102,19 +98,19 @@ begin definition - "emb = udom_emb lower_approx oo lower_map\emb" + "emb = lower_emb oo lower_map\emb" definition - "prj = lower_map\prj oo udom_prj lower_approx" + "prj = lower_map\prj oo lower_prj" definition "defl (t::'a lower_pd itself) = lower_defl\DEFL('a)" definition - "(liftemb :: 'a lower_pd u \ udom) = udom_emb u_approx oo u_map\emb" + "(liftemb :: 'a lower_pd u \ udom) = u_emb oo u_map\emb" definition - "(liftprj :: udom \ 'a lower_pd u) = u_map\prj oo udom_prj u_approx" + "(liftprj :: udom \ 'a lower_pd u) = u_map\prj oo u_prj" definition "liftdefl (t::'a lower_pd itself) = u_defl\DEFL('a lower_pd)" @@ -124,8 +120,7 @@ proof (rule liftdomain_class_intro) show "ep_pair emb (prj :: udom \ 'a lower_pd)" unfolding emb_lower_pd_def prj_lower_pd_def - using ep_pair_udom [OF lower_approx] - by (intro ep_pair_comp ep_pair_lower_map ep_pair_emb_prj) + by (intro ep_pair_comp ep_pair_lower ep_pair_lower_map ep_pair_emb_prj) next show "cast\DEFL('a lower_pd) = emb oo (prj :: udom \ 'a lower_pd)" unfolding emb_lower_pd_def prj_lower_pd_def defl_lower_pd_def cast_lower_defl @@ -138,19 +133,19 @@ begin definition - "emb = udom_emb convex_approx oo convex_map\emb" + "emb = convex_emb oo convex_map\emb" definition - "prj = convex_map\prj oo udom_prj convex_approx" + "prj = convex_map\prj oo convex_prj" definition "defl (t::'a convex_pd itself) = convex_defl\DEFL('a)" definition - "(liftemb :: 'a convex_pd u \ udom) = udom_emb u_approx oo u_map\emb" + "(liftemb :: 'a convex_pd u \ udom) = u_emb oo u_map\emb" definition - "(liftprj :: udom \ 'a convex_pd u) = u_map\prj oo udom_prj u_approx" + "(liftprj :: udom \ 'a convex_pd u) = u_map\prj oo u_prj" definition "liftdefl (t::'a convex_pd itself) = u_defl\DEFL('a convex_pd)" @@ -160,8 +155,7 @@ proof (rule liftdomain_class_intro) show "ep_pair emb (prj :: udom \ 'a convex_pd)" unfolding emb_convex_pd_def prj_convex_pd_def - using ep_pair_udom [OF convex_approx] - by (intro ep_pair_comp ep_pair_convex_map ep_pair_emb_prj) + by (intro ep_pair_comp ep_pair_convex ep_pair_convex_map ep_pair_emb_prj) next show "cast\DEFL('a convex_pd) = emb oo (prj :: udom \ 'a convex_pd)" unfolding emb_convex_pd_def prj_convex_pd_def defl_convex_pd_def cast_convex_defl diff -r f655912ac235 -r e9c9577d88b5 src/HOL/HOLCF/Representable.thy --- a/src/HOL/HOLCF/Representable.thy Sun Dec 19 06:59:01 2010 -0800 +++ b/src/HOL/HOLCF/Representable.thy Sun Dec 19 09:52:33 2010 -0800 @@ -86,180 +86,89 @@ instance predomain \ profinite by default (rule approx_chain_ep_cast [OF predomain_ep cast_liftdefl]) -subsection {* Chains of approx functions *} - -definition u_approx :: "nat \ udom\<^sub>\ \ udom\<^sub>\" - where "u_approx = (\i. u_map\(udom_approx i))" +subsection {* Universal domain ep-pairs *} -definition sfun_approx :: "nat \ (udom \! udom) \ (udom \! udom)" - where "sfun_approx = (\i. sfun_map\(udom_approx i)\(udom_approx i))" +definition "u_emb = udom_emb (\i. u_map\(udom_approx i))" +definition "u_prj = udom_prj (\i. u_map\(udom_approx i))" -definition prod_approx :: "nat \ udom \ udom \ udom \ udom" - where "prod_approx = (\i. cprod_map\(udom_approx i)\(udom_approx i))" +definition "prod_emb = udom_emb (\i. cprod_map\(udom_approx i)\(udom_approx i))" +definition "prod_prj = udom_prj (\i. cprod_map\(udom_approx i)\(udom_approx i))" -definition sprod_approx :: "nat \ udom \ udom \ udom \ udom" - where "sprod_approx = (\i. sprod_map\(udom_approx i)\(udom_approx i))" - -definition ssum_approx :: "nat \ udom \ udom \ udom \ udom" - where "ssum_approx = (\i. ssum_map\(udom_approx i)\(udom_approx i))" +definition "sprod_emb = udom_emb (\i. sprod_map\(udom_approx i)\(udom_approx i))" +definition "sprod_prj = udom_prj (\i. sprod_map\(udom_approx i)\(udom_approx i))" -lemma approx_chain_lemma1: - assumes "m\ID = ID" - assumes "\d. finite_deflation d \ finite_deflation (m\d)" - shows "approx_chain (\i. m\(udom_approx i))" -by (rule approx_chain.intro) - (simp_all add: lub_distribs finite_deflation_udom_approx assms) +definition "ssum_emb = udom_emb (\i. ssum_map\(udom_approx i)\(udom_approx i))" +definition "ssum_prj = udom_prj (\i. ssum_map\(udom_approx i)\(udom_approx i))" + +definition "sfun_emb = udom_emb (\i. sfun_map\(udom_approx i)\(udom_approx i))" +definition "sfun_prj = udom_prj (\i. sfun_map\(udom_approx i)\(udom_approx i))" -lemma approx_chain_lemma2: - assumes "m\ID\ID = ID" - assumes "\a b. \finite_deflation a; finite_deflation b\ - \ finite_deflation (m\a\b)" - shows "approx_chain (\i. m\(udom_approx i)\(udom_approx i))" -by (rule approx_chain.intro) - (simp_all add: lub_distribs finite_deflation_udom_approx assms) +lemma ep_pair_u: "ep_pair u_emb u_prj" + unfolding u_emb_def u_prj_def + by (simp add: ep_pair_udom approx_chain_u_map) -lemma u_approx: "approx_chain u_approx" -using u_map_ID finite_deflation_u_map -unfolding u_approx_def by (rule approx_chain_lemma1) +lemma ep_pair_prod: "ep_pair prod_emb prod_prj" + unfolding prod_emb_def prod_prj_def + by (simp add: ep_pair_udom approx_chain_cprod_map) -lemma sfun_approx: "approx_chain sfun_approx" -using sfun_map_ID finite_deflation_sfun_map -unfolding sfun_approx_def by (rule approx_chain_lemma2) - -lemma prod_approx: "approx_chain prod_approx" -using cprod_map_ID finite_deflation_cprod_map -unfolding prod_approx_def by (rule approx_chain_lemma2) +lemma ep_pair_sprod: "ep_pair sprod_emb sprod_prj" + unfolding sprod_emb_def sprod_prj_def + by (simp add: ep_pair_udom approx_chain_sprod_map) -lemma sprod_approx: "approx_chain sprod_approx" -using sprod_map_ID finite_deflation_sprod_map -unfolding sprod_approx_def by (rule approx_chain_lemma2) +lemma ep_pair_ssum: "ep_pair ssum_emb ssum_prj" + unfolding ssum_emb_def ssum_prj_def + by (simp add: ep_pair_udom approx_chain_ssum_map) -lemma ssum_approx: "approx_chain ssum_approx" -using ssum_map_ID finite_deflation_ssum_map -unfolding ssum_approx_def by (rule approx_chain_lemma2) +lemma ep_pair_sfun: "ep_pair sfun_emb sfun_prj" + unfolding sfun_emb_def sfun_prj_def + by (simp add: ep_pair_udom approx_chain_sfun_map) subsection {* Type combinators *} -default_sort bifinite - -definition - defl_fun1 :: - "(nat \ 'a \ 'a) \ ((udom \ udom) \ ('a \ 'a)) \ (udom defl \ udom defl)" -where - "defl_fun1 approx f = - defl.basis_fun (\a. - defl_principal (Abs_fin_defl - (udom_emb approx oo f\(Rep_fin_defl a) oo udom_prj approx)))" +definition u_defl :: "udom defl \ udom defl" + where "u_defl = defl_fun1 u_emb u_prj u_map" -definition - defl_fun2 :: - "(nat \ 'a \ 'a) \ ((udom \ udom) \ (udom \ udom) \ ('a \ 'a)) - \ (udom defl \ udom defl \ udom defl)" -where - "defl_fun2 approx f = - defl.basis_fun (\a. - defl.basis_fun (\b. - defl_principal (Abs_fin_defl - (udom_emb approx oo - f\(Rep_fin_defl a)\(Rep_fin_defl b) oo udom_prj approx))))" +definition prod_defl :: "udom defl \ udom defl \ udom defl" + where "prod_defl = defl_fun2 prod_emb prod_prj cprod_map" -lemma cast_defl_fun1: - assumes approx: "approx_chain approx" - assumes f: "\a. finite_deflation a \ finite_deflation (f\a)" - shows "cast\(defl_fun1 approx f\A) = udom_emb approx oo f\(cast\A) oo udom_prj approx" -proof - - have 1: "\a. finite_deflation - (udom_emb approx oo f\(Rep_fin_defl a) oo udom_prj approx)" - apply (rule ep_pair.finite_deflation_e_d_p) - apply (rule ep_pair_udom [OF approx]) - apply (rule f, rule finite_deflation_Rep_fin_defl) - done - show ?thesis - by (induct A rule: defl.principal_induct, simp) - (simp only: defl_fun1_def - defl.basis_fun_principal - defl.basis_fun_mono - defl.principal_mono - Abs_fin_defl_mono [OF 1 1] - monofun_cfun below_refl - Rep_fin_defl_mono - cast_defl_principal - Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1]) -qed +definition sprod_defl :: "udom defl \ udom defl \ udom defl" + where "sprod_defl = defl_fun2 sprod_emb sprod_prj sprod_map" -lemma cast_defl_fun2: - assumes approx: "approx_chain approx" - assumes f: "\a b. finite_deflation a \ finite_deflation b \ - finite_deflation (f\a\b)" - shows "cast\(defl_fun2 approx f\A\B) = - udom_emb approx oo f\(cast\A)\(cast\B) oo udom_prj approx" -proof - - have 1: "\a b. finite_deflation (udom_emb approx oo - f\(Rep_fin_defl a)\(Rep_fin_defl b) oo udom_prj approx)" - apply (rule ep_pair.finite_deflation_e_d_p) - apply (rule ep_pair_udom [OF approx]) - apply (rule f, (rule finite_deflation_Rep_fin_defl)+) - done - show ?thesis - by (induct A B rule: defl.principal_induct2, simp, simp) - (simp only: defl_fun2_def - defl.basis_fun_principal - defl.basis_fun_mono - defl.principal_mono - Abs_fin_defl_mono [OF 1 1] - monofun_cfun below_refl - Rep_fin_defl_mono - cast_defl_principal - Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1]) -qed - -definition u_defl :: "udom defl \ udom defl" - where "u_defl = defl_fun1 u_approx u_map" +definition ssum_defl :: "udom defl \ udom defl \ udom defl" +where "ssum_defl = defl_fun2 ssum_emb ssum_prj ssum_map" definition sfun_defl :: "udom defl \ udom defl \ udom defl" - where "sfun_defl = defl_fun2 sfun_approx sfun_map" - -definition prod_defl :: "udom defl \ udom defl \ udom defl" - where "prod_defl = defl_fun2 prod_approx cprod_map" - -definition sprod_defl :: "udom defl \ udom defl \ udom defl" - where "sprod_defl = defl_fun2 sprod_approx sprod_map" - -definition ssum_defl :: "udom defl \ udom defl \ udom defl" -where "ssum_defl = defl_fun2 ssum_approx ssum_map" + where "sfun_defl = defl_fun2 sfun_emb sfun_prj sfun_map" lemma cast_u_defl: - "cast\(u_defl\A) = - udom_emb u_approx oo u_map\(cast\A) oo udom_prj u_approx" -using u_approx finite_deflation_u_map + "cast\(u_defl\A) = u_emb oo u_map\(cast\A) oo u_prj" +using ep_pair_u finite_deflation_u_map unfolding u_defl_def by (rule cast_defl_fun1) -lemma cast_sfun_defl: - "cast\(sfun_defl\A\B) = - udom_emb sfun_approx oo sfun_map\(cast\A)\(cast\B) oo udom_prj sfun_approx" -using sfun_approx finite_deflation_sfun_map -unfolding sfun_defl_def by (rule cast_defl_fun2) - lemma cast_prod_defl: - "cast\(prod_defl\A\B) = udom_emb prod_approx oo - cprod_map\(cast\A)\(cast\B) oo udom_prj prod_approx" -using prod_approx finite_deflation_cprod_map + "cast\(prod_defl\A\B) = + prod_emb oo cprod_map\(cast\A)\(cast\B) oo prod_prj" +using ep_pair_prod finite_deflation_cprod_map unfolding prod_defl_def by (rule cast_defl_fun2) lemma cast_sprod_defl: "cast\(sprod_defl\A\B) = - udom_emb sprod_approx oo - sprod_map\(cast\A)\(cast\B) oo - udom_prj sprod_approx" -using sprod_approx finite_deflation_sprod_map + sprod_emb oo sprod_map\(cast\A)\(cast\B) oo sprod_prj" +using ep_pair_sprod finite_deflation_sprod_map unfolding sprod_defl_def by (rule cast_defl_fun2) lemma cast_ssum_defl: "cast\(ssum_defl\A\B) = - udom_emb ssum_approx oo ssum_map\(cast\A)\(cast\B) oo udom_prj ssum_approx" -using ssum_approx finite_deflation_ssum_map + ssum_emb oo ssum_map\(cast\A)\(cast\B) oo ssum_prj" +using ep_pair_ssum finite_deflation_ssum_map unfolding ssum_defl_def by (rule cast_defl_fun2) +lemma cast_sfun_defl: + "cast\(sfun_defl\A\B) = + sfun_emb oo sfun_map\(cast\A)\(cast\B) oo sfun_prj" +using ep_pair_sfun finite_deflation_sfun_map +unfolding sfun_defl_def by (rule cast_defl_fun2) + subsection {* Lemma for proving domain instances *} text {* @@ -268,8 +177,8 @@ *} class liftdomain = "domain" + - assumes liftemb_eq: "liftemb = udom_emb u_approx oo u_map\emb" - assumes liftprj_eq: "liftprj = u_map\prj oo udom_prj u_approx" + assumes liftemb_eq: "liftemb = u_emb oo u_map\emb" + assumes liftprj_eq: "liftprj = u_map\prj oo u_prj" assumes liftdefl_eq: "liftdefl TYPE('a::cpo) = u_defl\DEFL('a)" text {* Temporarily relax type constraints. *} @@ -287,8 +196,8 @@ default_sort pcpo lemma liftdomain_class_intro: - assumes liftemb: "(liftemb :: 'a u \ udom) = udom_emb u_approx oo u_map\emb" - assumes liftprj: "(liftprj :: udom \ 'a u) = u_map\prj oo udom_prj u_approx" + assumes liftemb: "(liftemb :: 'a u \ udom) = u_emb oo u_map\emb" + assumes liftprj: "(liftprj :: udom \ 'a u) = u_map\prj oo u_prj" assumes liftdefl: "liftdefl TYPE('a) = u_defl\DEFL('a)" assumes ep_pair: "ep_pair emb (prj :: udom \ 'a)" assumes cast_defl: "cast\DEFL('a) = emb oo (prj :: udom \ 'a)" @@ -296,7 +205,7 @@ proof show "ep_pair liftemb (liftprj :: udom \ 'a u)" unfolding liftemb liftprj - by (intro ep_pair_comp ep_pair_u_map ep_pair ep_pair_udom u_approx) + by (intro ep_pair_comp ep_pair_u_map ep_pair ep_pair_u) show "cast\LIFTDEFL('a) = liftemb oo (liftprj :: udom \ 'a u)" unfolding liftemb liftprj liftdefl by (simp add: cfcomp1 cast_u_defl cast_defl u_map_map) @@ -332,10 +241,10 @@ "defl (t::udom itself) = (\i. defl_principal (Abs_fin_defl (udom_approx i)))" definition - "(liftemb :: udom u \ udom) = udom_emb u_approx oo u_map\emb" + "(liftemb :: udom u \ udom) = u_emb oo u_map\emb" definition - "(liftprj :: udom \ udom u) = u_map\prj oo udom_prj u_approx" + "(liftprj :: udom \