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