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