1(* Title: HOL/HOLCF/Library/Sum_Cpo.thy 2 Author: Brian Huffman 3*) 4 5section \<open>The cpo of disjoint sums\<close> 6 7theory Sum_Cpo 8imports HOLCF 9begin 10 11subsection \<open>Ordering on sum type\<close> 12 13instantiation sum :: (below, below) below 14begin 15 16definition below_sum_def: 17 "x \<sqsubseteq> y \<equiv> case x of 18 Inl a \<Rightarrow> (case y of Inl b \<Rightarrow> a \<sqsubseteq> b | Inr b \<Rightarrow> False) | 19 Inr a \<Rightarrow> (case y of Inl b \<Rightarrow> False | Inr b \<Rightarrow> a \<sqsubseteq> b)" 20 21instance .. 22end 23 24lemma Inl_below_Inl [simp]: "Inl x \<sqsubseteq> Inl y \<longleftrightarrow> x \<sqsubseteq> y" 25unfolding below_sum_def by simp 26 27lemma Inr_below_Inr [simp]: "Inr x \<sqsubseteq> Inr y \<longleftrightarrow> x \<sqsubseteq> y" 28unfolding below_sum_def by simp 29 30lemma Inl_below_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y" 31unfolding below_sum_def by simp 32 33lemma Inr_below_Inl [simp]: "\<not> Inr x \<sqsubseteq> Inl y" 34unfolding below_sum_def by simp 35 36lemma Inl_mono: "x \<sqsubseteq> y \<Longrightarrow> Inl x \<sqsubseteq> Inl y" 37by simp 38 39lemma Inr_mono: "x \<sqsubseteq> y \<Longrightarrow> Inr x \<sqsubseteq> Inr y" 40by simp 41 42lemma Inl_belowE: "\<lbrakk>Inl a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" 43by (cases x, simp_all) 44 45lemma Inr_belowE: "\<lbrakk>Inr a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" 46by (cases x, simp_all) 47 48lemmas sum_below_elims = Inl_belowE Inr_belowE 49 50lemma sum_below_cases: 51 "\<lbrakk>x \<sqsubseteq> y; 52 \<And>a b. \<lbrakk>x = Inl a; y = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R; 53 \<And>a b. \<lbrakk>x = Inr a; y = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> 54 \<Longrightarrow> R" 55by (cases x, safe elim!: sum_below_elims, auto) 56 57subsection \<open>Sum type is a complete partial order\<close> 58 59instance sum :: (po, po) po 60proof 61 fix x :: "'a + 'b" 62 show "x \<sqsubseteq> x" 63 by (induct x, simp_all) 64next 65 fix x y :: "'a + 'b" 66 assume "x \<sqsubseteq> y" and "y \<sqsubseteq> x" thus "x = y" 67 by (induct x, auto elim!: sum_below_elims intro: below_antisym) 68next 69 fix x y z :: "'a + 'b" 70 assume "x \<sqsubseteq> y" and "y \<sqsubseteq> z" thus "x \<sqsubseteq> z" 71 by (induct x, auto elim!: sum_below_elims intro: below_trans) 72qed 73 74lemma monofun_inv_Inl: "monofun (\<lambda>p. THE a. p = Inl a)" 75by (rule monofunI, erule sum_below_cases, simp_all) 76 77lemma monofun_inv_Inr: "monofun (\<lambda>p. THE b. p = Inr b)" 78by (rule monofunI, erule sum_below_cases, simp_all) 79 80lemma sum_chain_cases: 81 assumes Y: "chain Y" 82 assumes A: "\<And>A. \<lbrakk>chain A; Y = (\<lambda>i. Inl (A i))\<rbrakk> \<Longrightarrow> R" 83 assumes B: "\<And>B. \<lbrakk>chain B; Y = (\<lambda>i. Inr (B i))\<rbrakk> \<Longrightarrow> R" 84 shows "R" 85 apply (cases "Y 0") 86 apply (rule A) 87 apply (rule ch2ch_monofun [OF monofun_inv_Inl Y]) 88 apply (rule ext) 89 apply (cut_tac j=i in chain_mono [OF Y le0], simp) 90 apply (erule Inl_belowE, simp) 91 apply (rule B) 92 apply (rule ch2ch_monofun [OF monofun_inv_Inr Y]) 93 apply (rule ext) 94 apply (cut_tac j=i in chain_mono [OF Y le0], simp) 95 apply (erule Inr_belowE, simp) 96done 97 98lemma is_lub_Inl: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inl (S i)) <<| Inl x" 99 apply (rule is_lubI) 100 apply (rule ub_rangeI) 101 apply (simp add: is_lub_rangeD1) 102 apply (frule ub_rangeD [where i=arbitrary]) 103 apply (erule Inl_belowE, simp) 104 apply (erule is_lubD2) 105 apply (rule ub_rangeI) 106 apply (drule ub_rangeD, simp) 107done 108 109lemma is_lub_Inr: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inr (S i)) <<| Inr x" 110 apply (rule is_lubI) 111 apply (rule ub_rangeI) 112 apply (simp add: is_lub_rangeD1) 113 apply (frule ub_rangeD [where i=arbitrary]) 114 apply (erule Inr_belowE, simp) 115 apply (erule is_lubD2) 116 apply (rule ub_rangeI) 117 apply (drule ub_rangeD, simp) 118done 119 120instance sum :: (cpo, cpo) cpo 121 apply intro_classes 122 apply (erule sum_chain_cases, safe) 123 apply (rule exI) 124 apply (rule is_lub_Inl) 125 apply (erule cpo_lubI) 126 apply (rule exI) 127 apply (rule is_lub_Inr) 128 apply (erule cpo_lubI) 129done 130 131subsection \<open>Continuity of \emph{Inl}, \emph{Inr}, and case function\<close> 132 133lemma cont_Inl: "cont Inl" 134by (intro contI is_lub_Inl cpo_lubI) 135 136lemma cont_Inr: "cont Inr" 137by (intro contI is_lub_Inr cpo_lubI) 138 139lemmas cont2cont_Inl [simp, cont2cont] = cont_compose [OF cont_Inl] 140lemmas cont2cont_Inr [simp, cont2cont] = cont_compose [OF cont_Inr] 141 142lemmas ch2ch_Inl [simp] = ch2ch_cont [OF cont_Inl] 143lemmas ch2ch_Inr [simp] = ch2ch_cont [OF cont_Inr] 144 145lemmas lub_Inl = cont2contlubE [OF cont_Inl, symmetric] 146lemmas lub_Inr = cont2contlubE [OF cont_Inr, symmetric] 147 148lemma cont_case_sum1: 149 assumes f: "\<And>a. cont (\<lambda>x. f x a)" 150 assumes g: "\<And>b. cont (\<lambda>x. g x b)" 151 shows "cont (\<lambda>x. case y of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)" 152by (induct y, simp add: f, simp add: g) 153 154lemma cont_case_sum2: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (case_sum f g)" 155apply (rule contI) 156apply (erule sum_chain_cases) 157apply (simp add: cont2contlubE [OF cont_Inl, symmetric] contE) 158apply (simp add: cont2contlubE [OF cont_Inr, symmetric] contE) 159done 160 161lemma cont2cont_case_sum: 162 assumes f1: "\<And>a. cont (\<lambda>x. f x a)" and f2: "\<And>x. cont (\<lambda>a. f x a)" 163 assumes g1: "\<And>b. cont (\<lambda>x. g x b)" and g2: "\<And>x. cont (\<lambda>b. g x b)" 164 assumes h: "cont (\<lambda>x. h x)" 165 shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)" 166apply (rule cont_apply [OF h]) 167apply (rule cont_case_sum2 [OF f2 g2]) 168apply (rule cont_case_sum1 [OF f1 g1]) 169done 170 171lemma cont2cont_case_sum' [simp, cont2cont]: 172 assumes f: "cont (\<lambda>p. f (fst p) (snd p))" 173 assumes g: "cont (\<lambda>p. g (fst p) (snd p))" 174 assumes h: "cont (\<lambda>x. h x)" 175 shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)" 176using assms by (simp add: cont2cont_case_sum prod_cont_iff) 177 178text \<open>Continuity of map function.\<close> 179 180lemma map_sum_eq: "map_sum f g = case_sum (\<lambda>a. Inl (f a)) (\<lambda>b. Inr (g b))" 181by (rule ext, case_tac x, simp_all) 182 183lemma cont2cont_map_sum [simp, cont2cont]: 184 assumes f: "cont (\<lambda>(x, y). f x y)" 185 assumes g: "cont (\<lambda>(x, y). g x y)" 186 assumes h: "cont (\<lambda>x. h x)" 187 shows "cont (\<lambda>x. map_sum (\<lambda>y. f x y) (\<lambda>y. g x y) (h x))" 188using assms by (simp add: map_sum_eq prod_cont_iff) 189 190subsection \<open>Compactness and chain-finiteness\<close> 191 192lemma compact_Inl: "compact a \<Longrightarrow> compact (Inl a)" 193apply (rule compactI2) 194apply (erule sum_chain_cases, safe) 195apply (simp add: lub_Inl) 196apply (erule (2) compactD2) 197apply (simp add: lub_Inr) 198done 199 200lemma compact_Inr: "compact a \<Longrightarrow> compact (Inr a)" 201apply (rule compactI2) 202apply (erule sum_chain_cases, safe) 203apply (simp add: lub_Inl) 204apply (simp add: lub_Inr) 205apply (erule (2) compactD2) 206done 207 208lemma compact_Inl_rev: "compact (Inl a) \<Longrightarrow> compact a" 209unfolding compact_def 210by (drule adm_subst [OF cont_Inl], simp) 211 212lemma compact_Inr_rev: "compact (Inr a) \<Longrightarrow> compact a" 213unfolding compact_def 214by (drule adm_subst [OF cont_Inr], simp) 215 216lemma compact_Inl_iff [simp]: "compact (Inl a) = compact a" 217by (safe elim!: compact_Inl compact_Inl_rev) 218 219lemma compact_Inr_iff [simp]: "compact (Inr a) = compact a" 220by (safe elim!: compact_Inr compact_Inr_rev) 221 222instance sum :: (chfin, chfin) chfin 223apply intro_classes 224apply (erule compact_imp_max_in_chain) 225apply (case_tac "\<Squnion>i. Y i", simp_all) 226done 227 228instance sum :: (discrete_cpo, discrete_cpo) discrete_cpo 229by intro_classes (simp add: below_sum_def split: sum.split) 230 231subsection \<open>Using sum types with fixrec\<close> 232 233definition 234 "match_Inl = (\<Lambda> x k. case x of Inl a \<Rightarrow> k\<cdot>a | Inr b \<Rightarrow> Fixrec.fail)" 235 236definition 237 "match_Inr = (\<Lambda> x k. case x of Inl a \<Rightarrow> Fixrec.fail | Inr b \<Rightarrow> k\<cdot>b)" 238 239lemma match_Inl_simps [simp]: 240 "match_Inl\<cdot>(Inl a)\<cdot>k = k\<cdot>a" 241 "match_Inl\<cdot>(Inr b)\<cdot>k = Fixrec.fail" 242unfolding match_Inl_def by simp_all 243 244lemma match_Inr_simps [simp]: 245 "match_Inr\<cdot>(Inl a)\<cdot>k = Fixrec.fail" 246 "match_Inr\<cdot>(Inr b)\<cdot>k = k\<cdot>b" 247unfolding match_Inr_def by simp_all 248 249setup \<open> 250 Fixrec.add_matchers 251 [ (@{const_name Inl}, @{const_name match_Inl}), 252 (@{const_name Inr}, @{const_name match_Inr}) ] 253\<close> 254 255subsection \<open>Disjoint sum is a predomain\<close> 256 257definition 258 "encode_sum_u = 259 (\<Lambda>(up\<cdot>x). case x of Inl a \<Rightarrow> sinl\<cdot>(up\<cdot>a) | Inr b \<Rightarrow> sinr\<cdot>(up\<cdot>b))" 260 261definition 262 "decode_sum_u = sscase\<cdot>(\<Lambda>(up\<cdot>a). up\<cdot>(Inl a))\<cdot>(\<Lambda>(up\<cdot>b). up\<cdot>(Inr b))" 263 264lemma decode_encode_sum_u [simp]: "decode_sum_u\<cdot>(encode_sum_u\<cdot>x) = x" 265unfolding decode_sum_u_def encode_sum_u_def 266by (case_tac x, simp, rename_tac y, case_tac y, simp_all) 267 268lemma encode_decode_sum_u [simp]: "encode_sum_u\<cdot>(decode_sum_u\<cdot>x) = x" 269unfolding decode_sum_u_def encode_sum_u_def 270apply (case_tac x, simp) 271apply (rename_tac a, case_tac a, simp, simp) 272apply (rename_tac b, case_tac b, simp, simp) 273done 274 275text \<open>A deflation combinator for making unpointed types\<close> 276 277definition udefl :: "udom defl \<rightarrow> udom u defl" 278 where "udefl = defl_fun1 (strictify\<cdot>up) (fup\<cdot>ID) ID" 279 280lemma ep_pair_strictify_up: 281 "ep_pair (strictify\<cdot>up) (fup\<cdot>ID)" 282apply (rule ep_pair.intro) 283apply (simp add: strictify_conv_if) 284apply (case_tac y, simp, simp add: strictify_conv_if) 285done 286 287lemma cast_udefl: 288 "cast\<cdot>(udefl\<cdot>t) = strictify\<cdot>up oo cast\<cdot>t oo fup\<cdot>ID" 289unfolding udefl_def by (simp add: cast_defl_fun1 ep_pair_strictify_up) 290 291definition sum_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl" 292 where "sum_liftdefl = (\<Lambda> a b. udefl\<cdot>(ssum_defl\<cdot>(u_liftdefl\<cdot>a)\<cdot>(u_liftdefl\<cdot>b)))" 293 294lemma u_emb_bottom: "u_emb\<cdot>\<bottom> = \<bottom>" 295by (rule pcpo_ep_pair.e_strict [unfolded pcpo_ep_pair_def, OF ep_pair_u]) 296 297(* 298definition sum_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl" 299 where "sum_liftdefl = defl_fun2 (u_map\<cdot>emb oo strictify\<cdot>up) 300 (fup\<cdot>ID oo u_map\<cdot>prj) ssum_map" 301*) 302 303instantiation sum :: (predomain, predomain) predomain 304begin 305 306definition 307 "liftemb = (strictify\<cdot>up oo ssum_emb) oo 308 (ssum_map\<cdot>(u_emb oo liftemb)\<cdot>(u_emb oo liftemb) oo encode_sum_u)" 309 310definition 311 "liftprj = (decode_sum_u oo ssum_map\<cdot>(liftprj oo u_prj)\<cdot>(liftprj oo u_prj)) 312 oo (ssum_prj oo fup\<cdot>ID)" 313 314definition 315 "liftdefl (t::('a + 'b) itself) = sum_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)" 316 317instance proof 318 show "ep_pair liftemb (liftprj :: udom u \<rightarrow> ('a + 'b) u)" 319 unfolding liftemb_sum_def liftprj_sum_def 320 by (intro ep_pair_comp ep_pair_ssum_map ep_pair_u predomain_ep 321 ep_pair_ssum ep_pair_strictify_up, simp add: ep_pair.intro) 322 show "cast\<cdot>LIFTDEFL('a + 'b) = liftemb oo (liftprj :: udom u \<rightarrow> ('a + 'b) u)" 323 unfolding liftemb_sum_def liftprj_sum_def liftdefl_sum_def 324 by (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_liftdefl 325 cast_liftdefl cfcomp1 ssum_map_map u_emb_bottom) 326qed 327 328end 329 330subsection \<open>Configuring domain package to work with sum type\<close> 331 332lemma liftdefl_sum [domain_defl_simps]: 333 "LIFTDEFL('a::predomain + 'b::predomain) = 334 sum_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)" 335by (rule liftdefl_sum_def) 336 337abbreviation map_sum' 338 where "map_sum' f g \<equiv> Abs_cfun (map_sum (Rep_cfun f) (Rep_cfun g))" 339 340lemma map_sum_ID [domain_map_ID]: "map_sum' ID ID = ID" 341by (simp add: ID_def cfun_eq_iff map_sum.identity id_def) 342 343lemma deflation_map_sum [domain_deflation]: 344 "\<lbrakk>deflation d1; deflation d2\<rbrakk> \<Longrightarrow> deflation (map_sum' d1 d2)" 345apply standard 346apply (induct_tac x, simp_all add: deflation.idem) 347apply (induct_tac x, simp_all add: deflation.below) 348done 349 350lemma encode_sum_u_map_sum: 351 "encode_sum_u\<cdot>(u_map\<cdot>(map_sum' f g)\<cdot>(decode_sum_u\<cdot>x)) 352 = ssum_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>g)\<cdot>x" 353apply (induct x, simp add: decode_sum_u_def encode_sum_u_def) 354apply (case_tac x, simp, simp add: decode_sum_u_def encode_sum_u_def) 355apply (case_tac y, simp, simp add: decode_sum_u_def encode_sum_u_def) 356done 357 358lemma isodefl_sum [domain_isodefl]: 359 fixes d :: "'a::predomain \<rightarrow> 'a" 360 assumes "isodefl' d1 t1" and "isodefl' d2 t2" 361 shows "isodefl' (map_sum' d1 d2) (sum_liftdefl\<cdot>t1\<cdot>t2)" 362using assms unfolding isodefl'_def liftemb_sum_def liftprj_sum_def 363apply (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_liftdefl) 364apply (simp add: cfcomp1 encode_sum_u_map_sum) 365apply (simp add: ssum_map_map u_emb_bottom) 366done 367 368setup \<open> 369 Domain_Take_Proofs.add_rec_type (@{type_name "sum"}, [true, true]) 370\<close> 371 372end 373