1(* Title: HOL/HOLCF/Bifinite.thy 2 Author: Brian Huffman 3*) 4 5section \<open>Profinite and bifinite cpos\<close> 6 7theory Bifinite 8 imports Map_Functions Cprod Sprod Sfun Up "HOL-Library.Countable" 9begin 10 11default_sort cpo 12 13subsection \<open>Chains of finite deflations\<close> 14 15locale approx_chain = 16 fixes approx :: "nat \<Rightarrow> 'a \<rightarrow> 'a" 17 assumes chain_approx [simp]: "chain (\<lambda>i. approx i)" 18 assumes lub_approx [simp]: "(\<Squnion>i. approx i) = ID" 19 assumes finite_deflation_approx [simp]: "\<And>i. finite_deflation (approx i)" 20begin 21 22lemma deflation_approx: "deflation (approx i)" 23using finite_deflation_approx by (rule finite_deflation_imp_deflation) 24 25lemma approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x" 26using deflation_approx by (rule deflation.idem) 27 28lemma approx_below: "approx i\<cdot>x \<sqsubseteq> x" 29using deflation_approx by (rule deflation.below) 30 31lemma finite_range_approx: "finite (range (\<lambda>x. approx i\<cdot>x))" 32apply (rule finite_deflation.finite_range) 33apply (rule finite_deflation_approx) 34done 35 36lemma compact_approx [simp]: "compact (approx n\<cdot>x)" 37apply (rule finite_deflation.compact) 38apply (rule finite_deflation_approx) 39done 40 41lemma compact_eq_approx: "compact x \<Longrightarrow> \<exists>i. approx i\<cdot>x = x" 42by (rule admD2, simp_all) 43 44end 45 46subsection \<open>Omega-profinite and bifinite domains\<close> 47 48class bifinite = pcpo + 49 assumes bifinite: "\<exists>(a::nat \<Rightarrow> 'a \<rightarrow> 'a). approx_chain a" 50 51class profinite = cpo + 52 assumes profinite: "\<exists>(a::nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>). approx_chain a" 53 54subsection \<open>Building approx chains\<close> 55 56lemma approx_chain_iso: 57 assumes a: "approx_chain a" 58 assumes [simp]: "\<And>x. f\<cdot>(g\<cdot>x) = x" 59 assumes [simp]: "\<And>y. g\<cdot>(f\<cdot>y) = y" 60 shows "approx_chain (\<lambda>i. f oo a i oo g)" 61proof - 62 have 1: "f oo g = ID" by (simp add: cfun_eqI) 63 have 2: "ep_pair f g" by (simp add: ep_pair_def) 64 from 1 2 show ?thesis 65 using a unfolding approx_chain_def 66 by (simp add: lub_APP ep_pair.finite_deflation_e_d_p) 67qed 68 69lemma approx_chain_u_map: 70 assumes "approx_chain a" 71 shows "approx_chain (\<lambda>i. u_map\<cdot>(a i))" 72 using assms unfolding approx_chain_def 73 by (simp add: lub_APP u_map_ID finite_deflation_u_map) 74 75lemma approx_chain_sfun_map: 76 assumes "approx_chain a" and "approx_chain b" 77 shows "approx_chain (\<lambda>i. sfun_map\<cdot>(a i)\<cdot>(b i))" 78 using assms unfolding approx_chain_def 79 by (simp add: lub_APP sfun_map_ID finite_deflation_sfun_map) 80 81lemma approx_chain_sprod_map: 82 assumes "approx_chain a" and "approx_chain b" 83 shows "approx_chain (\<lambda>i. sprod_map\<cdot>(a i)\<cdot>(b i))" 84 using assms unfolding approx_chain_def 85 by (simp add: lub_APP sprod_map_ID finite_deflation_sprod_map) 86 87lemma approx_chain_ssum_map: 88 assumes "approx_chain a" and "approx_chain b" 89 shows "approx_chain (\<lambda>i. ssum_map\<cdot>(a i)\<cdot>(b i))" 90 using assms unfolding approx_chain_def 91 by (simp add: lub_APP ssum_map_ID finite_deflation_ssum_map) 92 93lemma approx_chain_cfun_map: 94 assumes "approx_chain a" and "approx_chain b" 95 shows "approx_chain (\<lambda>i. cfun_map\<cdot>(a i)\<cdot>(b i))" 96 using assms unfolding approx_chain_def 97 by (simp add: lub_APP cfun_map_ID finite_deflation_cfun_map) 98 99lemma approx_chain_prod_map: 100 assumes "approx_chain a" and "approx_chain b" 101 shows "approx_chain (\<lambda>i. prod_map\<cdot>(a i)\<cdot>(b i))" 102 using assms unfolding approx_chain_def 103 by (simp add: lub_APP prod_map_ID finite_deflation_prod_map) 104 105text \<open>Approx chains for countable discrete types.\<close> 106 107definition discr_approx :: "nat \<Rightarrow> 'a::countable discr u \<rightarrow> 'a discr u" 108 where "discr_approx = (\<lambda>i. \<Lambda>(up\<cdot>x). if to_nat (undiscr x) < i then up\<cdot>x else \<bottom>)" 109 110lemma chain_discr_approx [simp]: "chain discr_approx" 111unfolding discr_approx_def 112by (rule chainI, simp add: monofun_cfun monofun_LAM) 113 114lemma lub_discr_approx [simp]: "(\<Squnion>i. discr_approx i) = ID" 115 apply (rule cfun_eqI) 116 apply (simp add: contlub_cfun_fun) 117 apply (simp add: discr_approx_def) 118 subgoal for x 119 apply (cases x) 120 apply simp 121 apply (rule lub_eqI) 122 apply (rule is_lubI) 123 apply (rule ub_rangeI, simp) 124 apply (drule ub_rangeD) 125 apply (erule rev_below_trans) 126 apply simp 127 apply (rule lessI) 128 done 129 done 130 131lemma inj_on_undiscr [simp]: "inj_on undiscr A" 132using Discr_undiscr by (rule inj_on_inverseI) 133 134lemma finite_deflation_discr_approx: "finite_deflation (discr_approx i)" 135proof 136 fix x :: "'a discr u" 137 show "discr_approx i\<cdot>x \<sqsubseteq> x" 138 unfolding discr_approx_def 139 by (cases x, simp, simp) 140 show "discr_approx i\<cdot>(discr_approx i\<cdot>x) = discr_approx i\<cdot>x" 141 unfolding discr_approx_def 142 by (cases x, simp, simp) 143 show "finite {x::'a discr u. discr_approx i\<cdot>x = x}" 144 proof (rule finite_subset) 145 let ?S = "insert (\<bottom>::'a discr u) ((\<lambda>x. up\<cdot>x) ` undiscr -` to_nat -` {..<i})" 146 show "{x::'a discr u. discr_approx i\<cdot>x = x} \<subseteq> ?S" 147 unfolding discr_approx_def 148 by (rule subsetI, case_tac x, simp, simp split: if_split_asm) 149 show "finite ?S" 150 by (simp add: finite_vimageI) 151 qed 152qed 153 154lemma discr_approx: "approx_chain discr_approx" 155using chain_discr_approx lub_discr_approx finite_deflation_discr_approx 156by (rule approx_chain.intro) 157 158subsection \<open>Class instance proofs\<close> 159 160instance bifinite \<subseteq> profinite 161proof 162 show "\<exists>(a::nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>). approx_chain a" 163 using bifinite [where 'a='a] 164 by (fast intro!: approx_chain_u_map) 165qed 166 167instance u :: (profinite) bifinite 168 by standard (rule profinite) 169 170text \<open> 171 Types \<^typ>\<open>'a \<rightarrow> 'b\<close> and \<^typ>\<open>'a u \<rightarrow>! 'b\<close> are isomorphic. 172\<close> 173 174definition "encode_cfun = (\<Lambda> f. sfun_abs\<cdot>(fup\<cdot>f))" 175 176definition "decode_cfun = (\<Lambda> g x. sfun_rep\<cdot>g\<cdot>(up\<cdot>x))" 177 178lemma decode_encode_cfun [simp]: "decode_cfun\<cdot>(encode_cfun\<cdot>x) = x" 179unfolding encode_cfun_def decode_cfun_def 180by (simp add: eta_cfun) 181 182lemma encode_decode_cfun [simp]: "encode_cfun\<cdot>(decode_cfun\<cdot>y) = y" 183unfolding encode_cfun_def decode_cfun_def 184apply (simp add: sfun_eq_iff strictify_cancel) 185apply (rule cfun_eqI, case_tac x, simp_all) 186done 187 188instance cfun :: (profinite, bifinite) bifinite 189proof 190 obtain a :: "nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>" where a: "approx_chain a" 191 using profinite .. 192 obtain b :: "nat \<Rightarrow> 'b \<rightarrow> 'b" where b: "approx_chain b" 193 using bifinite .. 194 have "approx_chain (\<lambda>i. decode_cfun oo sfun_map\<cdot>(a i)\<cdot>(b i) oo encode_cfun)" 195 using a b by (simp add: approx_chain_iso approx_chain_sfun_map) 196 thus "\<exists>(a::nat \<Rightarrow> ('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow> 'b)). approx_chain a" 197 by - (rule exI) 198qed 199 200text \<open> 201 Types \<^typ>\<open>('a * 'b) u\<close> and \<^typ>\<open>'a u \<otimes> 'b u\<close> are isomorphic. 202\<close> 203 204definition "encode_prod_u = (\<Lambda>(up\<cdot>(x, y)). (:up\<cdot>x, up\<cdot>y:))" 205 206definition "decode_prod_u = (\<Lambda>(:up\<cdot>x, up\<cdot>y:). up\<cdot>(x, y))" 207 208lemma decode_encode_prod_u [simp]: "decode_prod_u\<cdot>(encode_prod_u\<cdot>x) = x" 209 unfolding encode_prod_u_def decode_prod_u_def 210 apply (cases x) 211 apply simp 212 subgoal for y by (cases y) simp 213 done 214 215lemma encode_decode_prod_u [simp]: "encode_prod_u\<cdot>(decode_prod_u\<cdot>y) = y" 216 unfolding encode_prod_u_def decode_prod_u_def 217 apply (cases y) 218 apply simp 219 subgoal for a b 220 apply (cases a, simp) 221 apply (cases b, simp, simp) 222 done 223 done 224 225instance prod :: (profinite, profinite) profinite 226proof 227 obtain a :: "nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>" where a: "approx_chain a" 228 using profinite .. 229 obtain b :: "nat \<Rightarrow> 'b\<^sub>\<bottom> \<rightarrow> 'b\<^sub>\<bottom>" where b: "approx_chain b" 230 using profinite .. 231 have "approx_chain (\<lambda>i. decode_prod_u oo sprod_map\<cdot>(a i)\<cdot>(b i) oo encode_prod_u)" 232 using a b by (simp add: approx_chain_iso approx_chain_sprod_map) 233 thus "\<exists>(a::nat \<Rightarrow> ('a \<times> 'b)\<^sub>\<bottom> \<rightarrow> ('a \<times> 'b)\<^sub>\<bottom>). approx_chain a" 234 by - (rule exI) 235qed 236 237instance prod :: (bifinite, bifinite) bifinite 238proof 239 show "\<exists>(a::nat \<Rightarrow> ('a \<times> 'b) \<rightarrow> ('a \<times> 'b)). approx_chain a" 240 using bifinite [where 'a='a] and bifinite [where 'a='b] 241 by (fast intro!: approx_chain_prod_map) 242qed 243 244instance sfun :: (bifinite, bifinite) bifinite 245proof 246 show "\<exists>(a::nat \<Rightarrow> ('a \<rightarrow>! 'b) \<rightarrow> ('a \<rightarrow>! 'b)). approx_chain a" 247 using bifinite [where 'a='a] and bifinite [where 'a='b] 248 by (fast intro!: approx_chain_sfun_map) 249qed 250 251instance sprod :: (bifinite, bifinite) bifinite 252proof 253 show "\<exists>(a::nat \<Rightarrow> ('a \<otimes> 'b) \<rightarrow> ('a \<otimes> 'b)). approx_chain a" 254 using bifinite [where 'a='a] and bifinite [where 'a='b] 255 by (fast intro!: approx_chain_sprod_map) 256qed 257 258instance ssum :: (bifinite, bifinite) bifinite 259proof 260 show "\<exists>(a::nat \<Rightarrow> ('a \<oplus> 'b) \<rightarrow> ('a \<oplus> 'b)). approx_chain a" 261 using bifinite [where 'a='a] and bifinite [where 'a='b] 262 by (fast intro!: approx_chain_ssum_map) 263qed 264 265lemma approx_chain_unit: "approx_chain (\<bottom> :: nat \<Rightarrow> unit \<rightarrow> unit)" 266by (simp add: approx_chain_def cfun_eq_iff finite_deflation_bottom) 267 268instance unit :: bifinite 269 by standard (fast intro!: approx_chain_unit) 270 271instance discr :: (countable) profinite 272 by standard (fast intro!: discr_approx) 273 274instance lift :: (countable) bifinite 275proof 276 note [simp] = cont_Abs_lift cont_Rep_lift Rep_lift_inverse Abs_lift_inverse 277 obtain a :: "nat \<Rightarrow> ('a discr)\<^sub>\<bottom> \<rightarrow> ('a discr)\<^sub>\<bottom>" where a: "approx_chain a" 278 using profinite .. 279 hence "approx_chain (\<lambda>i. (\<Lambda> y. Abs_lift y) oo a i oo (\<Lambda> x. Rep_lift x))" 280 by (rule approx_chain_iso) simp_all 281 thus "\<exists>(a::nat \<Rightarrow> 'a lift \<rightarrow> 'a lift). approx_chain a" 282 by - (rule exI) 283qed 284 285end 286