minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
authorhuffman
Sun Dec 19 06:59:01 2010 -0800 (2010-12-19)
changeset 41289f655912ac235
parent 41288 a19edebad961
child 41290 e9c9577d88b5
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
src/HOL/HOLCF/Compact_Basis.thy
src/HOL/HOLCF/ConvexPD.thy
src/HOL/HOLCF/LowerPD.thy
src/HOL/HOLCF/Powerdomains.thy
src/HOL/HOLCF/UpperPD.thy
     1.1 --- a/src/HOL/HOLCF/Compact_Basis.thy	Sun Dec 19 06:39:19 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Compact_Basis.thy	Sun Dec 19 06:59:01 2010 -0800
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* A compact basis for powerdomains *}
     1.5  
     1.6  theory Compact_Basis
     1.7 -imports Representable
     1.8 +imports Universal
     1.9  begin
    1.10  
    1.11  default_sort bifinite
     2.1 --- a/src/HOL/HOLCF/ConvexPD.thy	Sun Dec 19 06:39:19 2010 -0800
     2.2 +++ b/src/HOL/HOLCF/ConvexPD.thy	Sun Dec 19 06:59:01 2010 -0800
     2.3 @@ -466,7 +466,7 @@
     2.4      by (rule finite_range_imp_finite_fixes)
     2.5  qed
     2.6  
     2.7 -subsection {* Convex powerdomain is a domain *}
     2.8 +subsection {* Convex powerdomain is bifinite *}
     2.9  
    2.10  lemma approx_chain_convex_map:
    2.11    assumes "approx_chain a"
    2.12 @@ -481,66 +481,6 @@
    2.13      by (fast intro!: approx_chain_convex_map)
    2.14  qed
    2.15  
    2.16 -definition
    2.17 -  convex_approx :: "nat \<Rightarrow> udom convex_pd \<rightarrow> udom convex_pd"
    2.18 -where
    2.19 -  "convex_approx = (\<lambda>i. convex_map\<cdot>(udom_approx i))"
    2.20 -
    2.21 -lemma convex_approx: "approx_chain convex_approx"
    2.22 -using convex_map_ID finite_deflation_convex_map
    2.23 -unfolding convex_approx_def by (rule approx_chain_lemma1)
    2.24 -
    2.25 -definition convex_defl :: "udom defl \<rightarrow> udom defl"
    2.26 -where "convex_defl = defl_fun1 convex_approx convex_map"
    2.27 -
    2.28 -lemma cast_convex_defl:
    2.29 -  "cast\<cdot>(convex_defl\<cdot>A) =
    2.30 -    udom_emb convex_approx oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj convex_approx"
    2.31 -using convex_approx finite_deflation_convex_map
    2.32 -unfolding convex_defl_def by (rule cast_defl_fun1)
    2.33 -
    2.34 -instantiation convex_pd :: ("domain") liftdomain
    2.35 -begin
    2.36 -
    2.37 -definition
    2.38 -  "emb = udom_emb convex_approx oo convex_map\<cdot>emb"
    2.39 -
    2.40 -definition
    2.41 -  "prj = convex_map\<cdot>prj oo udom_prj convex_approx"
    2.42 -
    2.43 -definition
    2.44 -  "defl (t::'a convex_pd itself) = convex_defl\<cdot>DEFL('a)"
    2.45 -
    2.46 -definition
    2.47 -  "(liftemb :: 'a convex_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
    2.48 -
    2.49 -definition
    2.50 -  "(liftprj :: udom \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj oo udom_prj u_approx"
    2.51 -
    2.52 -definition
    2.53 -  "liftdefl (t::'a convex_pd itself) = u_defl\<cdot>DEFL('a convex_pd)"
    2.54 -
    2.55 -instance
    2.56 -using liftemb_convex_pd_def liftprj_convex_pd_def liftdefl_convex_pd_def
    2.57 -proof (rule liftdomain_class_intro)
    2.58 -  show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)"
    2.59 -    unfolding emb_convex_pd_def prj_convex_pd_def
    2.60 -    using ep_pair_udom [OF convex_approx]
    2.61 -    by (intro ep_pair_comp ep_pair_convex_map ep_pair_emb_prj)
    2.62 -next
    2.63 -  show "cast\<cdot>DEFL('a convex_pd) = emb oo (prj :: udom \<rightarrow> 'a convex_pd)"
    2.64 -    unfolding emb_convex_pd_def prj_convex_pd_def defl_convex_pd_def cast_convex_defl
    2.65 -    by (simp add: cast_DEFL oo_def cfun_eq_iff convex_map_map)
    2.66 -qed
    2.67 -
    2.68 -end
    2.69 -
    2.70 -text {* DEFL of type constructor = type combinator *}
    2.71 -
    2.72 -lemma DEFL_convex: "DEFL('a::domain convex_pd) = convex_defl\<cdot>DEFL('a)"
    2.73 -by (rule defl_convex_pd_def)
    2.74 -
    2.75 -
    2.76  subsection {* Join *}
    2.77  
    2.78  definition
     3.1 --- a/src/HOL/HOLCF/LowerPD.thy	Sun Dec 19 06:39:19 2010 -0800
     3.2 +++ b/src/HOL/HOLCF/LowerPD.thy	Sun Dec 19 06:59:01 2010 -0800
     3.3 @@ -458,7 +458,7 @@
     3.4      by (rule finite_range_imp_finite_fixes)
     3.5  qed
     3.6  
     3.7 -subsection {* Lower powerdomain is a domain *}
     3.8 +subsection {* Lower powerdomain is bifinite *}
     3.9  
    3.10  lemma approx_chain_lower_map:
    3.11    assumes "approx_chain a"
    3.12 @@ -473,64 +473,6 @@
    3.13      by (fast intro!: approx_chain_lower_map)
    3.14  qed
    3.15  
    3.16 -definition
    3.17 -  lower_approx :: "nat \<Rightarrow> udom lower_pd \<rightarrow> udom lower_pd"
    3.18 -where
    3.19 -  "lower_approx = (\<lambda>i. lower_map\<cdot>(udom_approx i))"
    3.20 -
    3.21 -lemma lower_approx: "approx_chain lower_approx"
    3.22 -using lower_map_ID finite_deflation_lower_map
    3.23 -unfolding lower_approx_def by (rule approx_chain_lemma1)
    3.24 -
    3.25 -definition lower_defl :: "udom defl \<rightarrow> udom defl"
    3.26 -where "lower_defl = defl_fun1 lower_approx lower_map"
    3.27 -
    3.28 -lemma cast_lower_defl:
    3.29 -  "cast\<cdot>(lower_defl\<cdot>A) =
    3.30 -    udom_emb lower_approx oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj lower_approx"
    3.31 -using lower_approx finite_deflation_lower_map
    3.32 -unfolding lower_defl_def by (rule cast_defl_fun1)
    3.33 -
    3.34 -instantiation lower_pd :: ("domain") liftdomain
    3.35 -begin
    3.36 -
    3.37 -definition
    3.38 -  "emb = udom_emb lower_approx oo lower_map\<cdot>emb"
    3.39 -
    3.40 -definition
    3.41 -  "prj = lower_map\<cdot>prj oo udom_prj lower_approx"
    3.42 -
    3.43 -definition
    3.44 -  "defl (t::'a lower_pd itself) = lower_defl\<cdot>DEFL('a)"
    3.45 -
    3.46 -definition
    3.47 -  "(liftemb :: 'a lower_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
    3.48 -
    3.49 -definition
    3.50 -  "(liftprj :: udom \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj oo udom_prj u_approx"
    3.51 -
    3.52 -definition
    3.53 -  "liftdefl (t::'a lower_pd itself) = u_defl\<cdot>DEFL('a lower_pd)"
    3.54 -
    3.55 -instance
    3.56 -using liftemb_lower_pd_def liftprj_lower_pd_def liftdefl_lower_pd_def
    3.57 -proof (rule liftdomain_class_intro)
    3.58 -  show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)"
    3.59 -    unfolding emb_lower_pd_def prj_lower_pd_def
    3.60 -    using ep_pair_udom [OF lower_approx]
    3.61 -    by (intro ep_pair_comp ep_pair_lower_map ep_pair_emb_prj)
    3.62 -next
    3.63 -  show "cast\<cdot>DEFL('a lower_pd) = emb oo (prj :: udom \<rightarrow> 'a lower_pd)"
    3.64 -    unfolding emb_lower_pd_def prj_lower_pd_def defl_lower_pd_def cast_lower_defl
    3.65 -    by (simp add: cast_DEFL oo_def cfun_eq_iff lower_map_map)
    3.66 -qed
    3.67 -
    3.68 -end
    3.69 -
    3.70 -lemma DEFL_lower: "DEFL('a::domain lower_pd) = lower_defl\<cdot>DEFL('a)"
    3.71 -by (rule defl_lower_pd_def)
    3.72 -
    3.73 -
    3.74  subsection {* Join *}
    3.75  
    3.76  definition
     4.1 --- a/src/HOL/HOLCF/Powerdomains.thy	Sun Dec 19 06:39:19 2010 -0800
     4.2 +++ b/src/HOL/HOLCF/Powerdomains.thy	Sun Dec 19 06:59:01 2010 -0800
     4.3 @@ -8,6 +8,179 @@
     4.4  imports ConvexPD Domain
     4.5  begin
     4.6  
     4.7 +subsection {* Universal domain embeddings *}
     4.8 +
     4.9 +definition upper_approx :: "nat \<Rightarrow> udom upper_pd \<rightarrow> udom upper_pd"
    4.10 +  where "upper_approx = (\<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 +
    4.15 +definition convex_approx :: "nat \<Rightarrow> udom convex_pd \<rightarrow> udom convex_pd"
    4.16 +  where "convex_approx = (\<lambda>i. convex_map\<cdot>(udom_approx i))"
    4.17 +
    4.18 +lemma upper_approx: "approx_chain upper_approx"
    4.19 +  using upper_map_ID finite_deflation_upper_map
    4.20 +  unfolding upper_approx_def by (rule approx_chain_lemma1)
    4.21 +
    4.22 +lemma lower_approx: "approx_chain lower_approx"
    4.23 +  using lower_map_ID finite_deflation_lower_map
    4.24 +  unfolding lower_approx_def by (rule approx_chain_lemma1)
    4.25 +
    4.26 +lemma convex_approx: "approx_chain convex_approx"
    4.27 +  using convex_map_ID finite_deflation_convex_map
    4.28 +  unfolding convex_approx_def by (rule approx_chain_lemma1)
    4.29 +
    4.30 +subsection {* Deflation combinators *}
    4.31 +
    4.32 +definition upper_defl :: "udom defl \<rightarrow> udom defl"
    4.33 +  where "upper_defl = defl_fun1 upper_approx upper_map"
    4.34 +
    4.35 +definition lower_defl :: "udom defl \<rightarrow> udom defl"
    4.36 +  where "lower_defl = defl_fun1 lower_approx lower_map"
    4.37 +
    4.38 +definition convex_defl :: "udom defl \<rightarrow> udom defl"
    4.39 +  where "convex_defl = defl_fun1 convex_approx convex_map"
    4.40 +
    4.41 +lemma cast_upper_defl:
    4.42 +  "cast\<cdot>(upper_defl\<cdot>A) =
    4.43 +    udom_emb upper_approx oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj upper_approx"
    4.44 +using upper_approx finite_deflation_upper_map
    4.45 +unfolding upper_defl_def by (rule cast_defl_fun1)
    4.46 +
    4.47 +lemma cast_lower_defl:
    4.48 +  "cast\<cdot>(lower_defl\<cdot>A) =
    4.49 +    udom_emb lower_approx oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj lower_approx"
    4.50 +using lower_approx finite_deflation_lower_map
    4.51 +unfolding lower_defl_def by (rule cast_defl_fun1)
    4.52 +
    4.53 +lemma cast_convex_defl:
    4.54 +  "cast\<cdot>(convex_defl\<cdot>A) =
    4.55 +    udom_emb convex_approx oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj convex_approx"
    4.56 +using convex_approx finite_deflation_convex_map
    4.57 +unfolding convex_defl_def by (rule cast_defl_fun1)
    4.58 +
    4.59 +subsection {* Domain class instances *}
    4.60 +
    4.61 +instantiation upper_pd :: ("domain") liftdomain
    4.62 +begin
    4.63 +
    4.64 +definition
    4.65 +  "emb = udom_emb upper_approx oo upper_map\<cdot>emb"
    4.66 +
    4.67 +definition
    4.68 +  "prj = upper_map\<cdot>prj oo udom_prj upper_approx"
    4.69 +
    4.70 +definition
    4.71 +  "defl (t::'a upper_pd itself) = upper_defl\<cdot>DEFL('a)"
    4.72 +
    4.73 +definition
    4.74 +  "(liftemb :: 'a upper_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
    4.75 +
    4.76 +definition
    4.77 +  "(liftprj :: udom \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj oo udom_prj u_approx"
    4.78 +
    4.79 +definition
    4.80 +  "liftdefl (t::'a upper_pd itself) = u_defl\<cdot>DEFL('a upper_pd)"
    4.81 +
    4.82 +instance
    4.83 +using liftemb_upper_pd_def liftprj_upper_pd_def liftdefl_upper_pd_def
    4.84 +proof (rule liftdomain_class_intro)
    4.85 +  show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)"
    4.86 +    unfolding emb_upper_pd_def prj_upper_pd_def
    4.87 +    using ep_pair_udom [OF upper_approx]
    4.88 +    by (intro ep_pair_comp ep_pair_upper_map ep_pair_emb_prj)
    4.89 +next
    4.90 +  show "cast\<cdot>DEFL('a upper_pd) = emb oo (prj :: udom \<rightarrow> 'a upper_pd)"
    4.91 +    unfolding emb_upper_pd_def prj_upper_pd_def defl_upper_pd_def cast_upper_defl
    4.92 +    by (simp add: cast_DEFL oo_def cfun_eq_iff upper_map_map)
    4.93 +qed
    4.94 +
    4.95 +end
    4.96 +
    4.97 +instantiation lower_pd :: ("domain") liftdomain
    4.98 +begin
    4.99 +
   4.100 +definition
   4.101 +  "emb = udom_emb lower_approx oo lower_map\<cdot>emb"
   4.102 +
   4.103 +definition
   4.104 +  "prj = lower_map\<cdot>prj oo udom_prj lower_approx"
   4.105 +
   4.106 +definition
   4.107 +  "defl (t::'a lower_pd itself) = lower_defl\<cdot>DEFL('a)"
   4.108 +
   4.109 +definition
   4.110 +  "(liftemb :: 'a lower_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
   4.111 +
   4.112 +definition
   4.113 +  "(liftprj :: udom \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj oo udom_prj u_approx"
   4.114 +
   4.115 +definition
   4.116 +  "liftdefl (t::'a lower_pd itself) = u_defl\<cdot>DEFL('a lower_pd)"
   4.117 +
   4.118 +instance
   4.119 +using liftemb_lower_pd_def liftprj_lower_pd_def liftdefl_lower_pd_def
   4.120 +proof (rule liftdomain_class_intro)
   4.121 +  show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)"
   4.122 +    unfolding emb_lower_pd_def prj_lower_pd_def
   4.123 +    using ep_pair_udom [OF lower_approx]
   4.124 +    by (intro ep_pair_comp ep_pair_lower_map ep_pair_emb_prj)
   4.125 +next
   4.126 +  show "cast\<cdot>DEFL('a lower_pd) = emb oo (prj :: udom \<rightarrow> 'a lower_pd)"
   4.127 +    unfolding emb_lower_pd_def prj_lower_pd_def defl_lower_pd_def cast_lower_defl
   4.128 +    by (simp add: cast_DEFL oo_def cfun_eq_iff lower_map_map)
   4.129 +qed
   4.130 +
   4.131 +end
   4.132 +
   4.133 +instantiation convex_pd :: ("domain") liftdomain
   4.134 +begin
   4.135 +
   4.136 +definition
   4.137 +  "emb = udom_emb convex_approx oo convex_map\<cdot>emb"
   4.138 +
   4.139 +definition
   4.140 +  "prj = convex_map\<cdot>prj oo udom_prj convex_approx"
   4.141 +
   4.142 +definition
   4.143 +  "defl (t::'a convex_pd itself) = convex_defl\<cdot>DEFL('a)"
   4.144 +
   4.145 +definition
   4.146 +  "(liftemb :: 'a convex_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
   4.147 +
   4.148 +definition
   4.149 +  "(liftprj :: udom \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj oo udom_prj u_approx"
   4.150 +
   4.151 +definition
   4.152 +  "liftdefl (t::'a convex_pd itself) = u_defl\<cdot>DEFL('a convex_pd)"
   4.153 +
   4.154 +instance
   4.155 +using liftemb_convex_pd_def liftprj_convex_pd_def liftdefl_convex_pd_def
   4.156 +proof (rule liftdomain_class_intro)
   4.157 +  show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)"
   4.158 +    unfolding emb_convex_pd_def prj_convex_pd_def
   4.159 +    using ep_pair_udom [OF convex_approx]
   4.160 +    by (intro ep_pair_comp ep_pair_convex_map ep_pair_emb_prj)
   4.161 +next
   4.162 +  show "cast\<cdot>DEFL('a convex_pd) = emb oo (prj :: udom \<rightarrow> 'a convex_pd)"
   4.163 +    unfolding emb_convex_pd_def prj_convex_pd_def defl_convex_pd_def cast_convex_defl
   4.164 +    by (simp add: cast_DEFL oo_def cfun_eq_iff convex_map_map)
   4.165 +qed
   4.166 +
   4.167 +end
   4.168 +
   4.169 +lemma DEFL_upper: "DEFL('a::domain upper_pd) = upper_defl\<cdot>DEFL('a)"
   4.170 +by (rule defl_upper_pd_def)
   4.171 +
   4.172 +lemma DEFL_lower: "DEFL('a::domain lower_pd) = lower_defl\<cdot>DEFL('a)"
   4.173 +by (rule defl_lower_pd_def)
   4.174 +
   4.175 +lemma DEFL_convex: "DEFL('a::domain convex_pd) = convex_defl\<cdot>DEFL('a)"
   4.176 +by (rule defl_convex_pd_def)
   4.177 +
   4.178 +subsection {* Isomorphic deflations *}
   4.179 +
   4.180  lemma isodefl_upper:
   4.181    "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)"
   4.182  apply (rule isodeflI)
     5.1 --- a/src/HOL/HOLCF/UpperPD.thy	Sun Dec 19 06:39:19 2010 -0800
     5.2 +++ b/src/HOL/HOLCF/UpperPD.thy	Sun Dec 19 06:59:01 2010 -0800
     5.3 @@ -453,7 +453,7 @@
     5.4      by (rule finite_range_imp_finite_fixes)
     5.5  qed
     5.6  
     5.7 -subsection {* Upper powerdomain is a domain *}
     5.8 +subsection {* Upper powerdomain is bifinite *}
     5.9  
    5.10  lemma approx_chain_upper_map:
    5.11    assumes "approx_chain a"
    5.12 @@ -468,64 +468,6 @@
    5.13      by (fast intro!: approx_chain_upper_map)
    5.14  qed
    5.15  
    5.16 -definition
    5.17 -  upper_approx :: "nat \<Rightarrow> udom upper_pd \<rightarrow> udom upper_pd"
    5.18 -where
    5.19 -  "upper_approx = (\<lambda>i. upper_map\<cdot>(udom_approx i))"
    5.20 -
    5.21 -lemma upper_approx: "approx_chain upper_approx"
    5.22 -using upper_map_ID finite_deflation_upper_map
    5.23 -unfolding upper_approx_def by (rule approx_chain_lemma1)
    5.24 -
    5.25 -definition upper_defl :: "udom defl \<rightarrow> udom defl"
    5.26 -where "upper_defl = defl_fun1 upper_approx upper_map"
    5.27 -
    5.28 -lemma cast_upper_defl:
    5.29 -  "cast\<cdot>(upper_defl\<cdot>A) =
    5.30 -    udom_emb upper_approx oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj upper_approx"
    5.31 -using upper_approx finite_deflation_upper_map
    5.32 -unfolding upper_defl_def by (rule cast_defl_fun1)
    5.33 -
    5.34 -instantiation upper_pd :: ("domain") liftdomain
    5.35 -begin
    5.36 -
    5.37 -definition
    5.38 -  "emb = udom_emb upper_approx oo upper_map\<cdot>emb"
    5.39 -
    5.40 -definition
    5.41 -  "prj = upper_map\<cdot>prj oo udom_prj upper_approx"
    5.42 -
    5.43 -definition
    5.44 -  "defl (t::'a upper_pd itself) = upper_defl\<cdot>DEFL('a)"
    5.45 -
    5.46 -definition
    5.47 -  "(liftemb :: 'a upper_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
    5.48 -
    5.49 -definition
    5.50 -  "(liftprj :: udom \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj oo udom_prj u_approx"
    5.51 -
    5.52 -definition
    5.53 -  "liftdefl (t::'a upper_pd itself) = u_defl\<cdot>DEFL('a upper_pd)"
    5.54 -
    5.55 -instance
    5.56 -using liftemb_upper_pd_def liftprj_upper_pd_def liftdefl_upper_pd_def
    5.57 -proof (rule liftdomain_class_intro)
    5.58 -  show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)"
    5.59 -    unfolding emb_upper_pd_def prj_upper_pd_def
    5.60 -    using ep_pair_udom [OF upper_approx]
    5.61 -    by (intro ep_pair_comp ep_pair_upper_map ep_pair_emb_prj)
    5.62 -next
    5.63 -  show "cast\<cdot>DEFL('a upper_pd) = emb oo (prj :: udom \<rightarrow> 'a upper_pd)"
    5.64 -    unfolding emb_upper_pd_def prj_upper_pd_def defl_upper_pd_def cast_upper_defl
    5.65 -    by (simp add: cast_DEFL oo_def cfun_eq_iff upper_map_map)
    5.66 -qed
    5.67 -
    5.68 -end
    5.69 -
    5.70 -lemma DEFL_upper: "DEFL('a::domain upper_pd) = upper_defl\<cdot>DEFL('a)"
    5.71 -by (rule defl_upper_pd_def)
    5.72 -
    5.73 -
    5.74  subsection {* Join *}
    5.75  
    5.76  definition