src/HOL/HOLCF/Bifinite.thy
 author kuncar Fri Dec 09 18:07:04 2011 +0100 (2011-12-09) changeset 45802 b16f976db515 parent 42151 4da4fc77664b child 58880 0baae4311a9f permissions -rw-r--r--
Quotient_Info stores only relation maps
```     1 (*  Title:      HOL/HOLCF/Bifinite.thy
```
```     2     Author:     Brian Huffman
```
```     3 *)
```
```     4
```
```     5 header {* Profinite and bifinite cpos *}
```
```     6
```
```     7 theory Bifinite
```
```     8 imports Map_Functions "~~/src/HOL/Library/Countable"
```
```     9 begin
```
```    10
```
```    11 default_sort cpo
```
```    12
```
```    13 subsection {* Chains of finite deflations *}
```
```    14
```
```    15 locale 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)"
```
```    20 begin
```
```    21
```
```    22 lemma deflation_approx: "deflation (approx i)"
```
```    23 using finite_deflation_approx by (rule finite_deflation_imp_deflation)
```
```    24
```
```    25 lemma approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
```
```    26 using deflation_approx by (rule deflation.idem)
```
```    27
```
```    28 lemma approx_below: "approx i\<cdot>x \<sqsubseteq> x"
```
```    29 using deflation_approx by (rule deflation.below)
```
```    30
```
```    31 lemma finite_range_approx: "finite (range (\<lambda>x. approx i\<cdot>x))"
```
```    32 apply (rule finite_deflation.finite_range)
```
```    33 apply (rule finite_deflation_approx)
```
```    34 done
```
```    35
```
```    36 lemma compact_approx [simp]: "compact (approx n\<cdot>x)"
```
```    37 apply (rule finite_deflation.compact)
```
```    38 apply (rule finite_deflation_approx)
```
```    39 done
```
```    40
```
```    41 lemma compact_eq_approx: "compact x \<Longrightarrow> \<exists>i. approx i\<cdot>x = x"
```
```    42 by (rule admD2, simp_all)
```
```    43
```
```    44 end
```
```    45
```
```    46 subsection {* Omega-profinite and bifinite domains *}
```
```    47
```
```    48 class bifinite = pcpo +
```
```    49   assumes bifinite: "\<exists>(a::nat \<Rightarrow> 'a \<rightarrow> 'a). approx_chain a"
```
```    50
```
```    51 class profinite = cpo +
```
```    52   assumes profinite: "\<exists>(a::nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>). approx_chain a"
```
```    53
```
```    54 subsection {* Building approx chains *}
```
```    55
```
```    56 lemma 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)"
```
```    61 proof -
```
```    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)
```
```    67 qed
```
```    68
```
```    69 lemma 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
```
```    75 lemma 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
```
```    81 lemma 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
```
```    87 lemma 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
```
```    93 lemma 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
```
```    99 lemma 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
```
```   105 text {* Approx chains for countable discrete types. *}
```
```   106
```
```   107 definition 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
```
```   110 lemma chain_discr_approx [simp]: "chain discr_approx"
```
```   111 unfolding discr_approx_def
```
```   112 by (rule chainI, simp add: monofun_cfun monofun_LAM)
```
```   113
```
```   114 lemma 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 apply (case_tac x, simp)
```
```   119 apply (rule lub_eqI)
```
```   120 apply (rule is_lubI)
```
```   121 apply (rule ub_rangeI, simp)
```
```   122 apply (drule ub_rangeD)
```
```   123 apply (erule rev_below_trans)
```
```   124 apply simp
```
```   125 apply (rule lessI)
```
```   126 done
```
```   127
```
```   128 lemma inj_on_undiscr [simp]: "inj_on undiscr A"
```
```   129 using Discr_undiscr by (rule inj_on_inverseI)
```
```   130
```
```   131 lemma finite_deflation_discr_approx: "finite_deflation (discr_approx i)"
```
```   132 proof
```
```   133   fix x :: "'a discr u"
```
```   134   show "discr_approx i\<cdot>x \<sqsubseteq> x"
```
```   135     unfolding discr_approx_def
```
```   136     by (cases x, simp, simp)
```
```   137   show "discr_approx i\<cdot>(discr_approx i\<cdot>x) = discr_approx i\<cdot>x"
```
```   138     unfolding discr_approx_def
```
```   139     by (cases x, simp, simp)
```
```   140   show "finite {x::'a discr u. discr_approx i\<cdot>x = x}"
```
```   141   proof (rule finite_subset)
```
```   142     let ?S = "insert (\<bottom>::'a discr u) ((\<lambda>x. up\<cdot>x) ` undiscr -` to_nat -` {..<i})"
```
```   143     show "{x::'a discr u. discr_approx i\<cdot>x = x} \<subseteq> ?S"
```
```   144       unfolding discr_approx_def
```
```   145       by (rule subsetI, case_tac x, simp, simp split: split_if_asm)
```
```   146     show "finite ?S"
```
```   147       by (simp add: finite_vimageI)
```
```   148   qed
```
```   149 qed
```
```   150
```
```   151 lemma discr_approx: "approx_chain discr_approx"
```
```   152 using chain_discr_approx lub_discr_approx finite_deflation_discr_approx
```
```   153 by (rule approx_chain.intro)
```
```   154
```
```   155 subsection {* Class instance proofs *}
```
```   156
```
```   157 instance bifinite \<subseteq> profinite
```
```   158 proof
```
```   159   show "\<exists>(a::nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>). approx_chain a"
```
```   160     using bifinite [where 'a='a]
```
```   161     by (fast intro!: approx_chain_u_map)
```
```   162 qed
```
```   163
```
```   164 instance u :: (profinite) bifinite
```
```   165   by default (rule profinite)
```
```   166
```
```   167 text {*
```
```   168   Types @{typ "'a \<rightarrow> 'b"} and @{typ "'a u \<rightarrow>! 'b"} are isomorphic.
```
```   169 *}
```
```   170
```
```   171 definition "encode_cfun = (\<Lambda> f. sfun_abs\<cdot>(fup\<cdot>f))"
```
```   172
```
```   173 definition "decode_cfun = (\<Lambda> g x. sfun_rep\<cdot>g\<cdot>(up\<cdot>x))"
```
```   174
```
```   175 lemma decode_encode_cfun [simp]: "decode_cfun\<cdot>(encode_cfun\<cdot>x) = x"
```
```   176 unfolding encode_cfun_def decode_cfun_def
```
```   177 by (simp add: eta_cfun)
```
```   178
```
```   179 lemma encode_decode_cfun [simp]: "encode_cfun\<cdot>(decode_cfun\<cdot>y) = y"
```
```   180 unfolding encode_cfun_def decode_cfun_def
```
```   181 apply (simp add: sfun_eq_iff strictify_cancel)
```
```   182 apply (rule cfun_eqI, case_tac x, simp_all)
```
```   183 done
```
```   184
```
```   185 instance cfun :: (profinite, bifinite) bifinite
```
```   186 proof
```
```   187   obtain a :: "nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>" where a: "approx_chain a"
```
```   188     using profinite ..
```
```   189   obtain b :: "nat \<Rightarrow> 'b \<rightarrow> 'b" where b: "approx_chain b"
```
```   190     using bifinite ..
```
```   191   have "approx_chain (\<lambda>i. decode_cfun oo sfun_map\<cdot>(a i)\<cdot>(b i) oo encode_cfun)"
```
```   192     using a b by (simp add: approx_chain_iso approx_chain_sfun_map)
```
```   193   thus "\<exists>(a::nat \<Rightarrow> ('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow> 'b)). approx_chain a"
```
```   194     by - (rule exI)
```
```   195 qed
```
```   196
```
```   197 text {*
```
```   198   Types @{typ "('a * 'b) u"} and @{typ "'a u \<otimes> 'b u"} are isomorphic.
```
```   199 *}
```
```   200
```
```   201 definition "encode_prod_u = (\<Lambda>(up\<cdot>(x, y)). (:up\<cdot>x, up\<cdot>y:))"
```
```   202
```
```   203 definition "decode_prod_u = (\<Lambda>(:up\<cdot>x, up\<cdot>y:). up\<cdot>(x, y))"
```
```   204
```
```   205 lemma decode_encode_prod_u [simp]: "decode_prod_u\<cdot>(encode_prod_u\<cdot>x) = x"
```
```   206 unfolding encode_prod_u_def decode_prod_u_def
```
```   207 by (case_tac x, simp, rename_tac y, case_tac y, simp)
```
```   208
```
```   209 lemma encode_decode_prod_u [simp]: "encode_prod_u\<cdot>(decode_prod_u\<cdot>y) = y"
```
```   210 unfolding encode_prod_u_def decode_prod_u_def
```
```   211 apply (case_tac y, simp, rename_tac a b)
```
```   212 apply (case_tac a, simp, case_tac b, simp, simp)
```
```   213 done
```
```   214
```
```   215 instance prod :: (profinite, profinite) profinite
```
```   216 proof
```
```   217   obtain a :: "nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>" where a: "approx_chain a"
```
```   218     using profinite ..
```
```   219   obtain b :: "nat \<Rightarrow> 'b\<^sub>\<bottom> \<rightarrow> 'b\<^sub>\<bottom>" where b: "approx_chain b"
```
```   220     using profinite ..
```
```   221   have "approx_chain (\<lambda>i. decode_prod_u oo sprod_map\<cdot>(a i)\<cdot>(b i) oo encode_prod_u)"
```
```   222     using a b by (simp add: approx_chain_iso approx_chain_sprod_map)
```
```   223   thus "\<exists>(a::nat \<Rightarrow> ('a \<times> 'b)\<^sub>\<bottom> \<rightarrow> ('a \<times> 'b)\<^sub>\<bottom>). approx_chain a"
```
```   224     by - (rule exI)
```
```   225 qed
```
```   226
```
```   227 instance prod :: (bifinite, bifinite) bifinite
```
```   228 proof
```
```   229   show "\<exists>(a::nat \<Rightarrow> ('a \<times> 'b) \<rightarrow> ('a \<times> 'b)). approx_chain a"
```
```   230     using bifinite [where 'a='a] and bifinite [where 'a='b]
```
```   231     by (fast intro!: approx_chain_prod_map)
```
```   232 qed
```
```   233
```
```   234 instance sfun :: (bifinite, bifinite) bifinite
```
```   235 proof
```
```   236   show "\<exists>(a::nat \<Rightarrow> ('a \<rightarrow>! 'b) \<rightarrow> ('a \<rightarrow>! 'b)). approx_chain a"
```
```   237     using bifinite [where 'a='a] and bifinite [where 'a='b]
```
```   238     by (fast intro!: approx_chain_sfun_map)
```
```   239 qed
```
```   240
```
```   241 instance sprod :: (bifinite, bifinite) bifinite
```
```   242 proof
```
```   243   show "\<exists>(a::nat \<Rightarrow> ('a \<otimes> 'b) \<rightarrow> ('a \<otimes> 'b)). approx_chain a"
```
```   244     using bifinite [where 'a='a] and bifinite [where 'a='b]
```
```   245     by (fast intro!: approx_chain_sprod_map)
```
```   246 qed
```
```   247
```
```   248 instance ssum :: (bifinite, bifinite) bifinite
```
```   249 proof
```
```   250   show "\<exists>(a::nat \<Rightarrow> ('a \<oplus> 'b) \<rightarrow> ('a \<oplus> 'b)). approx_chain a"
```
```   251     using bifinite [where 'a='a] and bifinite [where 'a='b]
```
```   252     by (fast intro!: approx_chain_ssum_map)
```
```   253 qed
```
```   254
```
```   255 lemma approx_chain_unit: "approx_chain (\<bottom> :: nat \<Rightarrow> unit \<rightarrow> unit)"
```
```   256 by (simp add: approx_chain_def cfun_eq_iff finite_deflation_bottom)
```
```   257
```
```   258 instance unit :: bifinite
```
```   259   by default (fast intro!: approx_chain_unit)
```
```   260
```
```   261 instance discr :: (countable) profinite
```
```   262   by default (fast intro!: discr_approx)
```
```   263
```
```   264 instance lift :: (countable) bifinite
```
```   265 proof
```
```   266   note [simp] = cont_Abs_lift cont_Rep_lift Rep_lift_inverse Abs_lift_inverse
```
```   267   obtain a :: "nat \<Rightarrow> ('a discr)\<^sub>\<bottom> \<rightarrow> ('a discr)\<^sub>\<bottom>" where a: "approx_chain a"
```
```   268     using profinite ..
```
```   269   hence "approx_chain (\<lambda>i. (\<Lambda> y. Abs_lift y) oo a i oo (\<Lambda> x. Rep_lift x))"
```
```   270     by (rule approx_chain_iso) simp_all
```
```   271   thus "\<exists>(a::nat \<Rightarrow> 'a lift \<rightarrow> 'a lift). approx_chain a"
```
```   272     by - (rule exI)
```
```   273 qed
```
```   274
```
```   275 end
```