1(* Title: HOL/HOLCF/Domain.thy 2 Author: Brian Huffman 3*) 4 5section \<open>Domain package\<close> 6 7theory Domain 8imports Representable Domain_Aux 9keywords 10 "lazy" "unsafe" and 11 "domaindef" "domain" :: thy_defn and 12 "domain_isomorphism" :: thy_decl 13begin 14 15default_sort "domain" 16 17subsection \<open>Representations of types\<close> 18 19lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a) = cast\<cdot>DEFL('a)\<cdot>x" 20by (simp add: cast_DEFL) 21 22lemma emb_prj_emb: 23 fixes x :: "'a" 24 assumes "DEFL('a) \<sqsubseteq> DEFL('b)" 25 shows "emb\<cdot>(prj\<cdot>(emb\<cdot>x) :: 'b) = emb\<cdot>x" 26unfolding emb_prj 27apply (rule cast.belowD) 28apply (rule monofun_cfun_arg [OF assms]) 29apply (simp add: cast_DEFL) 30done 31 32lemma prj_emb_prj: 33 assumes "DEFL('a) \<sqsubseteq> DEFL('b)" 34 shows "prj\<cdot>(emb\<cdot>(prj\<cdot>x :: 'b)) = (prj\<cdot>x :: 'a)" 35 apply (rule emb_eq_iff [THEN iffD1]) 36 apply (simp only: emb_prj) 37 apply (rule deflation_below_comp1) 38 apply (rule deflation_cast) 39 apply (rule deflation_cast) 40 apply (rule monofun_cfun_arg [OF assms]) 41done 42 43text \<open>Isomorphism lemmas used internally by the domain package:\<close> 44 45lemma domain_abs_iso: 46 fixes abs and rep 47 assumes DEFL: "DEFL('b) = DEFL('a)" 48 assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb" 49 assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb" 50 shows "rep\<cdot>(abs\<cdot>x) = x" 51unfolding abs_def rep_def 52by (simp add: emb_prj_emb DEFL) 53 54lemma domain_rep_iso: 55 fixes abs and rep 56 assumes DEFL: "DEFL('b) = DEFL('a)" 57 assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb" 58 assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb" 59 shows "abs\<cdot>(rep\<cdot>x) = x" 60unfolding abs_def rep_def 61by (simp add: emb_prj_emb DEFL) 62 63subsection \<open>Deflations as sets\<close> 64 65definition defl_set :: "'a::bifinite defl \<Rightarrow> 'a set" 66where "defl_set A = {x. cast\<cdot>A\<cdot>x = x}" 67 68lemma adm_defl_set: "adm (\<lambda>x. x \<in> defl_set A)" 69unfolding defl_set_def by simp 70 71lemma defl_set_bottom: "\<bottom> \<in> defl_set A" 72unfolding defl_set_def by simp 73 74lemma defl_set_cast [simp]: "cast\<cdot>A\<cdot>x \<in> defl_set A" 75unfolding defl_set_def by simp 76 77lemma defl_set_subset_iff: "defl_set A \<subseteq> defl_set B \<longleftrightarrow> A \<sqsubseteq> B" 78apply (simp add: defl_set_def subset_eq cast_below_cast [symmetric]) 79apply (auto simp add: cast.belowI cast.belowD) 80done 81 82subsection \<open>Proving a subtype is representable\<close> 83 84text \<open>Temporarily relax type constraints.\<close> 85 86setup \<open> 87 fold Sign.add_const_constraint 88 [ (\<^const_name>\<open>defl\<close>, SOME \<^typ>\<open>'a::pcpo itself \<Rightarrow> udom defl\<close>) 89 , (\<^const_name>\<open>emb\<close>, SOME \<^typ>\<open>'a::pcpo \<rightarrow> udom\<close>) 90 , (\<^const_name>\<open>prj\<close>, SOME \<^typ>\<open>udom \<rightarrow> 'a::pcpo\<close>) 91 , (\<^const_name>\<open>liftdefl\<close>, SOME \<^typ>\<open>'a::pcpo itself \<Rightarrow> udom u defl\<close>) 92 , (\<^const_name>\<open>liftemb\<close>, SOME \<^typ>\<open>'a::pcpo u \<rightarrow> udom u\<close>) 93 , (\<^const_name>\<open>liftprj\<close>, SOME \<^typ>\<open>udom u \<rightarrow> 'a::pcpo u\<close>) ] 94\<close> 95 96lemma typedef_domain_class: 97 fixes Rep :: "'a::pcpo \<Rightarrow> udom" 98 fixes Abs :: "udom \<Rightarrow> 'a::pcpo" 99 fixes t :: "udom defl" 100 assumes type: "type_definition Rep Abs (defl_set t)" 101 assumes below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 102 assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)" 103 assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))" 104 assumes defl: "defl \<equiv> (\<lambda> a::'a itself. t)" 105 assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom u) \<equiv> u_map\<cdot>emb" 106 assumes liftprj: "(liftprj :: udom u \<rightarrow> 'a u) \<equiv> u_map\<cdot>prj" 107 assumes liftdefl: "(liftdefl :: 'a itself \<Rightarrow> _) \<equiv> (\<lambda>t. liftdefl_of\<cdot>DEFL('a))" 108 shows "OFCLASS('a, domain_class)" 109proof 110 have emb_beta: "\<And>x. emb\<cdot>x = Rep x" 111 unfolding emb 112 apply (rule beta_cfun) 113 apply (rule typedef_cont_Rep [OF type below adm_defl_set cont_id]) 114 done 115 have prj_beta: "\<And>y. prj\<cdot>y = Abs (cast\<cdot>t\<cdot>y)" 116 unfolding prj 117 apply (rule beta_cfun) 118 apply (rule typedef_cont_Abs [OF type below adm_defl_set]) 119 apply simp_all 120 done 121 have prj_emb: "\<And>x::'a. prj\<cdot>(emb\<cdot>x) = x" 122 using type_definition.Rep [OF type] 123 unfolding prj_beta emb_beta defl_set_def 124 by (simp add: type_definition.Rep_inverse [OF type]) 125 have emb_prj: "\<And>y. emb\<cdot>(prj\<cdot>y :: 'a) = cast\<cdot>t\<cdot>y" 126 unfolding prj_beta emb_beta 127 by (simp add: type_definition.Abs_inverse [OF type]) 128 show "ep_pair (emb :: 'a \<rightarrow> udom) prj" 129 apply standard 130 apply (simp add: prj_emb) 131 apply (simp add: emb_prj cast.below) 132 done 133 show "cast\<cdot>DEFL('a) = emb oo (prj :: udom \<rightarrow> 'a)" 134 by (rule cfun_eqI, simp add: defl emb_prj) 135qed (simp_all only: liftemb liftprj liftdefl) 136 137lemma typedef_DEFL: 138 assumes "defl \<equiv> (\<lambda>a::'a::pcpo itself. t)" 139 shows "DEFL('a::pcpo) = t" 140unfolding assms .. 141 142text \<open>Restore original typing constraints.\<close> 143 144setup \<open> 145 fold Sign.add_const_constraint 146 [(\<^const_name>\<open>defl\<close>, SOME \<^typ>\<open>'a::domain itself \<Rightarrow> udom defl\<close>), 147 (\<^const_name>\<open>emb\<close>, SOME \<^typ>\<open>'a::domain \<rightarrow> udom\<close>), 148 (\<^const_name>\<open>prj\<close>, SOME \<^typ>\<open>udom \<rightarrow> 'a::domain\<close>), 149 (\<^const_name>\<open>liftdefl\<close>, SOME \<^typ>\<open>'a::predomain itself \<Rightarrow> udom u defl\<close>), 150 (\<^const_name>\<open>liftemb\<close>, SOME \<^typ>\<open>'a::predomain u \<rightarrow> udom u\<close>), 151 (\<^const_name>\<open>liftprj\<close>, SOME \<^typ>\<open>udom u \<rightarrow> 'a::predomain u\<close>)] 152\<close> 153 154ML_file \<open>Tools/domaindef.ML\<close> 155 156subsection \<open>Isomorphic deflations\<close> 157 158definition isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> udom defl \<Rightarrow> bool" 159 where "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj" 160 161definition isodefl' :: "('a::predomain \<rightarrow> 'a) \<Rightarrow> udom u defl \<Rightarrow> bool" 162 where "isodefl' d t \<longleftrightarrow> cast\<cdot>t = liftemb oo u_map\<cdot>d oo liftprj" 163 164lemma isodeflI: "(\<And>x. cast\<cdot>t\<cdot>x = emb\<cdot>(d\<cdot>(prj\<cdot>x))) \<Longrightarrow> isodefl d t" 165unfolding isodefl_def by (simp add: cfun_eqI) 166 167lemma cast_isodefl: "isodefl d t \<Longrightarrow> cast\<cdot>t = (\<Lambda> x. emb\<cdot>(d\<cdot>(prj\<cdot>x)))" 168unfolding isodefl_def by (simp add: cfun_eqI) 169 170lemma isodefl_strict: "isodefl d t \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>" 171unfolding isodefl_def 172by (drule cfun_fun_cong [where x="\<bottom>"], simp) 173 174lemma isodefl_imp_deflation: 175 fixes d :: "'a \<rightarrow> 'a" 176 assumes "isodefl d t" shows "deflation d" 177proof 178 note assms [unfolded isodefl_def, simp] 179 fix x :: 'a 180 show "d\<cdot>(d\<cdot>x) = d\<cdot>x" 181 using cast.idem [of t "emb\<cdot>x"] by simp 182 show "d\<cdot>x \<sqsubseteq> x" 183 using cast.below [of t "emb\<cdot>x"] by simp 184qed 185 186lemma isodefl_ID_DEFL: "isodefl (ID :: 'a \<rightarrow> 'a) DEFL('a)" 187unfolding isodefl_def by (simp add: cast_DEFL) 188 189lemma isodefl_LIFTDEFL: 190 "isodefl' (ID :: 'a \<rightarrow> 'a) LIFTDEFL('a::predomain)" 191unfolding isodefl'_def by (simp add: cast_liftdefl u_map_ID) 192 193lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) DEFL('a) \<Longrightarrow> d = ID" 194unfolding isodefl_def 195apply (simp add: cast_DEFL) 196apply (simp add: cfun_eq_iff) 197apply (rule allI) 198apply (drule_tac x="emb\<cdot>x" in spec) 199apply simp 200done 201 202lemma isodefl_bottom: "isodefl \<bottom> \<bottom>" 203unfolding isodefl_def by (simp add: cfun_eq_iff) 204 205lemma adm_isodefl: 206 "cont f \<Longrightarrow> cont g \<Longrightarrow> adm (\<lambda>x. isodefl (f x) (g x))" 207unfolding isodefl_def by simp 208 209lemma isodefl_lub: 210 assumes "chain d" and "chain t" 211 assumes "\<And>i. isodefl (d i) (t i)" 212 shows "isodefl (\<Squnion>i. d i) (\<Squnion>i. t i)" 213using assms unfolding isodefl_def 214by (simp add: contlub_cfun_arg contlub_cfun_fun) 215 216lemma isodefl_fix: 217 assumes "\<And>d t. isodefl d t \<Longrightarrow> isodefl (f\<cdot>d) (g\<cdot>t)" 218 shows "isodefl (fix\<cdot>f) (fix\<cdot>g)" 219unfolding fix_def2 220apply (rule isodefl_lub, simp, simp) 221apply (induct_tac i) 222apply (simp add: isodefl_bottom) 223apply (simp add: assms) 224done 225 226lemma isodefl_abs_rep: 227 fixes abs and rep and d 228 assumes DEFL: "DEFL('b) = DEFL('a)" 229 assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb" 230 assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb" 231 shows "isodefl d t \<Longrightarrow> isodefl (abs oo d oo rep) t" 232unfolding isodefl_def 233by (simp add: cfun_eq_iff assms prj_emb_prj emb_prj_emb) 234 235lemma isodefl'_liftdefl_of: "isodefl d t \<Longrightarrow> isodefl' d (liftdefl_of\<cdot>t)" 236unfolding isodefl_def isodefl'_def 237by (simp add: cast_liftdefl_of u_map_oo liftemb_eq liftprj_eq) 238 239lemma isodefl_sfun: 240 "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow> 241 isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)" 242apply (rule isodeflI) 243apply (simp add: cast_sfun_defl cast_isodefl) 244apply (simp add: emb_sfun_def prj_sfun_def) 245apply (simp add: sfun_map_map isodefl_strict) 246done 247 248lemma isodefl_ssum: 249 "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow> 250 isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_defl\<cdot>t1\<cdot>t2)" 251apply (rule isodeflI) 252apply (simp add: cast_ssum_defl cast_isodefl) 253apply (simp add: emb_ssum_def prj_ssum_def) 254apply (simp add: ssum_map_map isodefl_strict) 255done 256 257lemma isodefl_sprod: 258 "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow> 259 isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_defl\<cdot>t1\<cdot>t2)" 260apply (rule isodeflI) 261apply (simp add: cast_sprod_defl cast_isodefl) 262apply (simp add: emb_sprod_def prj_sprod_def) 263apply (simp add: sprod_map_map isodefl_strict) 264done 265 266lemma isodefl_prod: 267 "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow> 268 isodefl (prod_map\<cdot>d1\<cdot>d2) (prod_defl\<cdot>t1\<cdot>t2)" 269apply (rule isodeflI) 270apply (simp add: cast_prod_defl cast_isodefl) 271apply (simp add: emb_prod_def prj_prod_def) 272apply (simp add: prod_map_map cfcomp1) 273done 274 275lemma isodefl_u: 276 "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)" 277apply (rule isodeflI) 278apply (simp add: cast_u_defl cast_isodefl) 279apply (simp add: emb_u_def prj_u_def liftemb_eq liftprj_eq u_map_map) 280done 281 282lemma isodefl_u_liftdefl: 283 "isodefl' d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_liftdefl\<cdot>t)" 284apply (rule isodeflI) 285apply (simp add: cast_u_liftdefl isodefl'_def) 286apply (simp add: emb_u_def prj_u_def liftemb_eq liftprj_eq) 287done 288 289lemma encode_prod_u_map: 290 "encode_prod_u\<cdot>(u_map\<cdot>(prod_map\<cdot>f\<cdot>g)\<cdot>(decode_prod_u\<cdot>x)) 291 = sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>g)\<cdot>x" 292unfolding encode_prod_u_def decode_prod_u_def 293apply (case_tac x, simp, rename_tac a b) 294apply (case_tac a, simp, case_tac b, simp, simp) 295done 296 297lemma isodefl_prod_u: 298 assumes "isodefl' d1 t1" and "isodefl' d2 t2" 299 shows "isodefl' (prod_map\<cdot>d1\<cdot>d2) (prod_liftdefl\<cdot>t1\<cdot>t2)" 300using assms unfolding isodefl'_def 301unfolding liftemb_prod_def liftprj_prod_def 302by (simp add: cast_prod_liftdefl cfcomp1 encode_prod_u_map sprod_map_map) 303 304lemma encode_cfun_map: 305 "encode_cfun\<cdot>(cfun_map\<cdot>f\<cdot>g\<cdot>(decode_cfun\<cdot>x)) 306 = sfun_map\<cdot>(u_map\<cdot>f)\<cdot>g\<cdot>x" 307unfolding encode_cfun_def decode_cfun_def 308apply (simp add: sfun_eq_iff cfun_map_def sfun_map_def) 309apply (rule cfun_eqI, rename_tac y, case_tac y, simp_all) 310done 311 312lemma isodefl_cfun: 313 assumes "isodefl (u_map\<cdot>d1) t1" and "isodefl d2 t2" 314 shows "isodefl (cfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)" 315using isodefl_sfun [OF assms] unfolding isodefl_def 316by (simp add: emb_cfun_def prj_cfun_def cfcomp1 encode_cfun_map) 317 318subsection \<open>Setting up the domain package\<close> 319 320named_theorems domain_defl_simps "theorems like DEFL('a t) = t_defl$DEFL('a)" 321 and domain_isodefl "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)" 322 323ML_file \<open>Tools/Domain/domain_isomorphism.ML\<close> 324ML_file \<open>Tools/Domain/domain_axioms.ML\<close> 325ML_file \<open>Tools/Domain/domain.ML\<close> 326 327lemmas [domain_defl_simps] = 328 DEFL_cfun DEFL_sfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u 329 liftdefl_eq LIFTDEFL_prod u_liftdefl_liftdefl_of 330 331lemmas [domain_map_ID] = 332 cfun_map_ID sfun_map_ID ssum_map_ID sprod_map_ID prod_map_ID u_map_ID 333 334lemmas [domain_isodefl] = 335 isodefl_u isodefl_sfun isodefl_ssum isodefl_sprod 336 isodefl_cfun isodefl_prod isodefl_prod_u isodefl'_liftdefl_of 337 isodefl_u_liftdefl 338 339lemmas [domain_deflation] = 340 deflation_cfun_map deflation_sfun_map deflation_ssum_map 341 deflation_sprod_map deflation_prod_map deflation_u_map 342 343setup \<open> 344 fold Domain_Take_Proofs.add_rec_type 345 [(\<^type_name>\<open>cfun\<close>, [true, true]), 346 (\<^type_name>\<open>sfun\<close>, [true, true]), 347 (\<^type_name>\<open>ssum\<close>, [true, true]), 348 (\<^type_name>\<open>sprod\<close>, [true, true]), 349 (\<^type_name>\<open>prod\<close>, [true, true]), 350 (\<^type_name>\<open>u\<close>, [true])] 351\<close> 352 353end 354