1(* Title: HOL/HOLCF/Powerdomains.thy 2 Author: Brian Huffman 3*) 4 5section \<open>Powerdomains\<close> 6 7theory Powerdomains 8imports ConvexPD Domain 9begin 10 11subsection \<open>Universal domain embeddings\<close> 12 13definition "upper_emb = udom_emb (\<lambda>i. upper_map\<cdot>(udom_approx i))" 14definition "upper_prj = udom_prj (\<lambda>i. upper_map\<cdot>(udom_approx i))" 15 16definition "lower_emb = udom_emb (\<lambda>i. lower_map\<cdot>(udom_approx i))" 17definition "lower_prj = udom_prj (\<lambda>i. lower_map\<cdot>(udom_approx i))" 18 19definition "convex_emb = udom_emb (\<lambda>i. convex_map\<cdot>(udom_approx i))" 20definition "convex_prj = udom_prj (\<lambda>i. convex_map\<cdot>(udom_approx i))" 21 22lemma ep_pair_upper: "ep_pair upper_emb upper_prj" 23 unfolding upper_emb_def upper_prj_def 24 by (simp add: ep_pair_udom approx_chain_upper_map) 25 26lemma ep_pair_lower: "ep_pair lower_emb lower_prj" 27 unfolding lower_emb_def lower_prj_def 28 by (simp add: ep_pair_udom approx_chain_lower_map) 29 30lemma ep_pair_convex: "ep_pair convex_emb convex_prj" 31 unfolding convex_emb_def convex_prj_def 32 by (simp add: ep_pair_udom approx_chain_convex_map) 33 34subsection \<open>Deflation combinators\<close> 35 36definition upper_defl :: "udom defl \<rightarrow> udom defl" 37 where "upper_defl = defl_fun1 upper_emb upper_prj upper_map" 38 39definition lower_defl :: "udom defl \<rightarrow> udom defl" 40 where "lower_defl = defl_fun1 lower_emb lower_prj lower_map" 41 42definition convex_defl :: "udom defl \<rightarrow> udom defl" 43 where "convex_defl = defl_fun1 convex_emb convex_prj convex_map" 44 45lemma cast_upper_defl: 46 "cast\<cdot>(upper_defl\<cdot>A) = upper_emb oo upper_map\<cdot>(cast\<cdot>A) oo upper_prj" 47using ep_pair_upper finite_deflation_upper_map 48unfolding upper_defl_def by (rule cast_defl_fun1) 49 50lemma cast_lower_defl: 51 "cast\<cdot>(lower_defl\<cdot>A) = lower_emb oo lower_map\<cdot>(cast\<cdot>A) oo lower_prj" 52using ep_pair_lower finite_deflation_lower_map 53unfolding lower_defl_def by (rule cast_defl_fun1) 54 55lemma cast_convex_defl: 56 "cast\<cdot>(convex_defl\<cdot>A) = convex_emb oo convex_map\<cdot>(cast\<cdot>A) oo convex_prj" 57using ep_pair_convex finite_deflation_convex_map 58unfolding convex_defl_def by (rule cast_defl_fun1) 59 60subsection \<open>Domain class instances\<close> 61 62instantiation upper_pd :: ("domain") "domain" 63begin 64 65definition 66 "emb = upper_emb oo upper_map\<cdot>emb" 67 68definition 69 "prj = upper_map\<cdot>prj oo upper_prj" 70 71definition 72 "defl (t::'a upper_pd itself) = upper_defl\<cdot>DEFL('a)" 73 74definition 75 "(liftemb :: 'a upper_pd u \<rightarrow> udom u) = u_map\<cdot>emb" 76 77definition 78 "(liftprj :: udom u \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj" 79 80definition 81 "liftdefl (t::'a upper_pd itself) = liftdefl_of\<cdot>DEFL('a upper_pd)" 82 83instance proof 84 show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)" 85 unfolding emb_upper_pd_def prj_upper_pd_def 86 by (intro ep_pair_comp ep_pair_upper ep_pair_upper_map ep_pair_emb_prj) 87next 88 show "cast\<cdot>DEFL('a upper_pd) = emb oo (prj :: udom \<rightarrow> 'a upper_pd)" 89 unfolding emb_upper_pd_def prj_upper_pd_def defl_upper_pd_def cast_upper_defl 90 by (simp add: cast_DEFL oo_def cfun_eq_iff upper_map_map) 91qed (fact liftemb_upper_pd_def liftprj_upper_pd_def liftdefl_upper_pd_def)+ 92 93end 94 95instantiation lower_pd :: ("domain") "domain" 96begin 97 98definition 99 "emb = lower_emb oo lower_map\<cdot>emb" 100 101definition 102 "prj = lower_map\<cdot>prj oo lower_prj" 103 104definition 105 "defl (t::'a lower_pd itself) = lower_defl\<cdot>DEFL('a)" 106 107definition 108 "(liftemb :: 'a lower_pd u \<rightarrow> udom u) = u_map\<cdot>emb" 109 110definition 111 "(liftprj :: udom u \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj" 112 113definition 114 "liftdefl (t::'a lower_pd itself) = liftdefl_of\<cdot>DEFL('a lower_pd)" 115 116instance proof 117 show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)" 118 unfolding emb_lower_pd_def prj_lower_pd_def 119 by (intro ep_pair_comp ep_pair_lower ep_pair_lower_map ep_pair_emb_prj) 120next 121 show "cast\<cdot>DEFL('a lower_pd) = emb oo (prj :: udom \<rightarrow> 'a lower_pd)" 122 unfolding emb_lower_pd_def prj_lower_pd_def defl_lower_pd_def cast_lower_defl 123 by (simp add: cast_DEFL oo_def cfun_eq_iff lower_map_map) 124qed (fact liftemb_lower_pd_def liftprj_lower_pd_def liftdefl_lower_pd_def)+ 125 126end 127 128instantiation convex_pd :: ("domain") "domain" 129begin 130 131definition 132 "emb = convex_emb oo convex_map\<cdot>emb" 133 134definition 135 "prj = convex_map\<cdot>prj oo convex_prj" 136 137definition 138 "defl (t::'a convex_pd itself) = convex_defl\<cdot>DEFL('a)" 139 140definition 141 "(liftemb :: 'a convex_pd u \<rightarrow> udom u) = u_map\<cdot>emb" 142 143definition 144 "(liftprj :: udom u \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj" 145 146definition 147 "liftdefl (t::'a convex_pd itself) = liftdefl_of\<cdot>DEFL('a convex_pd)" 148 149instance proof 150 show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)" 151 unfolding emb_convex_pd_def prj_convex_pd_def 152 by (intro ep_pair_comp ep_pair_convex ep_pair_convex_map ep_pair_emb_prj) 153next 154 show "cast\<cdot>DEFL('a convex_pd) = emb oo (prj :: udom \<rightarrow> 'a convex_pd)" 155 unfolding emb_convex_pd_def prj_convex_pd_def defl_convex_pd_def cast_convex_defl 156 by (simp add: cast_DEFL oo_def cfun_eq_iff convex_map_map) 157qed (fact liftemb_convex_pd_def liftprj_convex_pd_def liftdefl_convex_pd_def)+ 158 159end 160 161lemma DEFL_upper: "DEFL('a::domain upper_pd) = upper_defl\<cdot>DEFL('a)" 162by (rule defl_upper_pd_def) 163 164lemma DEFL_lower: "DEFL('a::domain lower_pd) = lower_defl\<cdot>DEFL('a)" 165by (rule defl_lower_pd_def) 166 167lemma DEFL_convex: "DEFL('a::domain convex_pd) = convex_defl\<cdot>DEFL('a)" 168by (rule defl_convex_pd_def) 169 170subsection \<open>Isomorphic deflations\<close> 171 172lemma isodefl_upper: 173 "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)" 174apply (rule isodeflI) 175apply (simp add: cast_upper_defl cast_isodefl) 176apply (simp add: emb_upper_pd_def prj_upper_pd_def) 177apply (simp add: upper_map_map) 178done 179 180lemma isodefl_lower: 181 "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>t)" 182apply (rule isodeflI) 183apply (simp add: cast_lower_defl cast_isodefl) 184apply (simp add: emb_lower_pd_def prj_lower_pd_def) 185apply (simp add: lower_map_map) 186done 187 188lemma isodefl_convex: 189 "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>t)" 190apply (rule isodeflI) 191apply (simp add: cast_convex_defl cast_isodefl) 192apply (simp add: emb_convex_pd_def prj_convex_pd_def) 193apply (simp add: convex_map_map) 194done 195 196subsection \<open>Domain package setup for powerdomains\<close> 197 198lemmas [domain_defl_simps] = DEFL_upper DEFL_lower DEFL_convex 199lemmas [domain_map_ID] = upper_map_ID lower_map_ID convex_map_ID 200lemmas [domain_isodefl] = isodefl_upper isodefl_lower isodefl_convex 201 202lemmas [domain_deflation] = 203 deflation_upper_map deflation_lower_map deflation_convex_map 204 205setup \<open> 206 fold Domain_Take_Proofs.add_rec_type 207 [(\<^type_name>\<open>upper_pd\<close>, [true]), 208 (\<^type_name>\<open>lower_pd\<close>, [true]), 209 (\<^type_name>\<open>convex_pd\<close>, [true])] 210\<close> 211 212end 213