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