# HG changeset patch # User huffman # Date 1292770741 28800 # Node ID f655912ac235e3df4ee757a78e942e4e6e8cfca9 # Parent a19edebad961195260abbe62ceb29cb4899fa843 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy diff -r a19edebad961 -r f655912ac235 src/HOL/HOLCF/Compact_Basis.thy --- a/src/HOL/HOLCF/Compact_Basis.thy Sun Dec 19 06:39:19 2010 -0800 +++ b/src/HOL/HOLCF/Compact_Basis.thy Sun Dec 19 06:59:01 2010 -0800 @@ -5,7 +5,7 @@ header {* A compact basis for powerdomains *} theory Compact_Basis -imports Representable +imports Universal begin default_sort bifinite diff -r a19edebad961 -r f655912ac235 src/HOL/HOLCF/ConvexPD.thy --- a/src/HOL/HOLCF/ConvexPD.thy Sun Dec 19 06:39:19 2010 -0800 +++ b/src/HOL/HOLCF/ConvexPD.thy Sun Dec 19 06:59:01 2010 -0800 @@ -466,7 +466,7 @@ by (rule finite_range_imp_finite_fixes) qed -subsection {* Convex powerdomain is a domain *} +subsection {* Convex powerdomain is bifinite *} lemma approx_chain_convex_map: assumes "approx_chain a" @@ -481,66 +481,6 @@ by (fast intro!: approx_chain_convex_map) qed -definition - convex_approx :: "nat \ udom convex_pd \ udom convex_pd" -where - "convex_approx = (\i. convex_map\(udom_approx i))" - -lemma convex_approx: "approx_chain convex_approx" -using convex_map_ID finite_deflation_convex_map -unfolding convex_approx_def by (rule approx_chain_lemma1) - -definition convex_defl :: "udom defl \ udom defl" -where "convex_defl = defl_fun1 convex_approx convex_map" - -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 -unfolding convex_defl_def by (rule cast_defl_fun1) - -instantiation convex_pd :: ("domain") liftdomain -begin - -definition - "emb = udom_emb convex_approx oo convex_map\emb" - -definition - "prj = convex_map\prj oo udom_prj convex_approx" - -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" - -definition - "(liftprj :: udom \ 'a convex_pd u) = u_map\prj oo udom_prj u_approx" - -definition - "liftdefl (t::'a convex_pd itself) = u_defl\DEFL('a convex_pd)" - -instance -using liftemb_convex_pd_def liftprj_convex_pd_def liftdefl_convex_pd_def -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) -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 - by (simp add: cast_DEFL oo_def cfun_eq_iff convex_map_map) -qed - -end - -text {* DEFL of type constructor = type combinator *} - -lemma DEFL_convex: "DEFL('a::domain convex_pd) = convex_defl\DEFL('a)" -by (rule defl_convex_pd_def) - - subsection {* Join *} definition diff -r a19edebad961 -r f655912ac235 src/HOL/HOLCF/LowerPD.thy --- a/src/HOL/HOLCF/LowerPD.thy Sun Dec 19 06:39:19 2010 -0800 +++ b/src/HOL/HOLCF/LowerPD.thy Sun Dec 19 06:59:01 2010 -0800 @@ -458,7 +458,7 @@ by (rule finite_range_imp_finite_fixes) qed -subsection {* Lower powerdomain is a domain *} +subsection {* Lower powerdomain is bifinite *} lemma approx_chain_lower_map: assumes "approx_chain a" @@ -473,64 +473,6 @@ by (fast intro!: approx_chain_lower_map) qed -definition - lower_approx :: "nat \ udom lower_pd \ udom lower_pd" -where - "lower_approx = (\i. lower_map\(udom_approx i))" - -lemma lower_approx: "approx_chain lower_approx" -using lower_map_ID finite_deflation_lower_map -unfolding lower_approx_def by (rule approx_chain_lemma1) - -definition lower_defl :: "udom defl \ udom defl" -where "lower_defl = defl_fun1 lower_approx lower_map" - -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 -unfolding lower_defl_def by (rule cast_defl_fun1) - -instantiation lower_pd :: ("domain") liftdomain -begin - -definition - "emb = udom_emb lower_approx oo lower_map\emb" - -definition - "prj = lower_map\prj oo udom_prj lower_approx" - -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" - -definition - "(liftprj :: udom \ 'a lower_pd u) = u_map\prj oo udom_prj u_approx" - -definition - "liftdefl (t::'a lower_pd itself) = u_defl\DEFL('a lower_pd)" - -instance -using liftemb_lower_pd_def liftprj_lower_pd_def liftdefl_lower_pd_def -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) -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 - by (simp add: cast_DEFL oo_def cfun_eq_iff lower_map_map) -qed - -end - -lemma DEFL_lower: "DEFL('a::domain lower_pd) = lower_defl\DEFL('a)" -by (rule defl_lower_pd_def) - - subsection {* Join *} definition diff -r a19edebad961 -r f655912ac235 src/HOL/HOLCF/Powerdomains.thy --- a/src/HOL/HOLCF/Powerdomains.thy Sun Dec 19 06:39:19 2010 -0800 +++ b/src/HOL/HOLCF/Powerdomains.thy Sun Dec 19 06:59:01 2010 -0800 @@ -8,6 +8,179 @@ imports ConvexPD Domain begin +subsection {* Universal domain embeddings *} + +definition upper_approx :: "nat \ udom upper_pd \ udom upper_pd" + where "upper_approx = (\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 convex_approx :: "nat \ udom convex_pd \ udom convex_pd" + where "convex_approx = (\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 lower_approx: "approx_chain lower_approx" + using lower_map_ID finite_deflation_lower_map + unfolding lower_approx_def by (rule approx_chain_lemma1) + +lemma convex_approx: "approx_chain convex_approx" + using convex_map_ID finite_deflation_convex_map + unfolding convex_approx_def by (rule approx_chain_lemma1) + +subsection {* Deflation combinators *} + +definition upper_defl :: "udom defl \ udom defl" + where "upper_defl = defl_fun1 upper_approx upper_map" + +definition lower_defl :: "udom defl \ udom defl" + where "lower_defl = defl_fun1 lower_approx lower_map" + +definition convex_defl :: "udom defl \ udom defl" + where "convex_defl = defl_fun1 convex_approx 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 +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 +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 +unfolding convex_defl_def by (rule cast_defl_fun1) + +subsection {* Domain class instances *} + +instantiation upper_pd :: ("domain") liftdomain +begin + +definition + "emb = udom_emb upper_approx oo upper_map\emb" + +definition + "prj = upper_map\prj oo udom_prj upper_approx" + +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" + +definition + "(liftprj :: udom \ 'a upper_pd u) = u_map\prj oo udom_prj u_approx" + +definition + "liftdefl (t::'a upper_pd itself) = u_defl\DEFL('a upper_pd)" + +instance +using liftemb_upper_pd_def liftprj_upper_pd_def liftdefl_upper_pd_def +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) +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 + by (simp add: cast_DEFL oo_def cfun_eq_iff upper_map_map) +qed + +end + +instantiation lower_pd :: ("domain") liftdomain +begin + +definition + "emb = udom_emb lower_approx oo lower_map\emb" + +definition + "prj = lower_map\prj oo udom_prj lower_approx" + +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" + +definition + "(liftprj :: udom \ 'a lower_pd u) = u_map\prj oo udom_prj u_approx" + +definition + "liftdefl (t::'a lower_pd itself) = u_defl\DEFL('a lower_pd)" + +instance +using liftemb_lower_pd_def liftprj_lower_pd_def liftdefl_lower_pd_def +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) +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 + by (simp add: cast_DEFL oo_def cfun_eq_iff lower_map_map) +qed + +end + +instantiation convex_pd :: ("domain") liftdomain +begin + +definition + "emb = udom_emb convex_approx oo convex_map\emb" + +definition + "prj = convex_map\prj oo udom_prj convex_approx" + +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" + +definition + "(liftprj :: udom \ 'a convex_pd u) = u_map\prj oo udom_prj u_approx" + +definition + "liftdefl (t::'a convex_pd itself) = u_defl\DEFL('a convex_pd)" + +instance +using liftemb_convex_pd_def liftprj_convex_pd_def liftdefl_convex_pd_def +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) +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 + by (simp add: cast_DEFL oo_def cfun_eq_iff convex_map_map) +qed + +end + +lemma DEFL_upper: "DEFL('a::domain upper_pd) = upper_defl\DEFL('a)" +by (rule defl_upper_pd_def) + +lemma DEFL_lower: "DEFL('a::domain lower_pd) = lower_defl\DEFL('a)" +by (rule defl_lower_pd_def) + +lemma DEFL_convex: "DEFL('a::domain convex_pd) = convex_defl\DEFL('a)" +by (rule defl_convex_pd_def) + +subsection {* Isomorphic deflations *} + lemma isodefl_upper: "isodefl d t \ isodefl (upper_map\d) (upper_defl\t)" apply (rule isodeflI) diff -r a19edebad961 -r f655912ac235 src/HOL/HOLCF/UpperPD.thy --- a/src/HOL/HOLCF/UpperPD.thy Sun Dec 19 06:39:19 2010 -0800 +++ b/src/HOL/HOLCF/UpperPD.thy Sun Dec 19 06:59:01 2010 -0800 @@ -453,7 +453,7 @@ by (rule finite_range_imp_finite_fixes) qed -subsection {* Upper powerdomain is a domain *} +subsection {* Upper powerdomain is bifinite *} lemma approx_chain_upper_map: assumes "approx_chain a" @@ -468,64 +468,6 @@ by (fast intro!: approx_chain_upper_map) qed -definition - upper_approx :: "nat \ udom upper_pd \ udom upper_pd" -where - "upper_approx = (\i. upper_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) - -definition upper_defl :: "udom defl \ udom defl" -where "upper_defl = defl_fun1 upper_approx upper_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 -unfolding upper_defl_def by (rule cast_defl_fun1) - -instantiation upper_pd :: ("domain") liftdomain -begin - -definition - "emb = udom_emb upper_approx oo upper_map\emb" - -definition - "prj = upper_map\prj oo udom_prj upper_approx" - -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" - -definition - "(liftprj :: udom \ 'a upper_pd u) = u_map\prj oo udom_prj u_approx" - -definition - "liftdefl (t::'a upper_pd itself) = u_defl\DEFL('a upper_pd)" - -instance -using liftemb_upper_pd_def liftprj_upper_pd_def liftdefl_upper_pd_def -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) -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 - by (simp add: cast_DEFL oo_def cfun_eq_iff upper_map_map) -qed - -end - -lemma DEFL_upper: "DEFL('a::domain upper_pd) = upper_defl\DEFL('a)" -by (rule defl_upper_pd_def) - - subsection {* Join *} definition