src/HOLCF/Bifinite.thy
author Brian Huffman <brianh@cs.pdx.edu>
Tue Oct 05 17:36:45 2010 -0700 (2010-10-05)
changeset 39972 4244ff4f9649
parent 37678 0040bafffdef
child 39973 c62b4ff97bfc
permissions -rw-r--r--
add lemmas finite_deflation_imp_compact, cast_below_cast_iff
     1 (*  Title:      HOLCF/Bifinite.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 header {* Bifinite domains and approximation *}
     6 
     7 theory Bifinite
     8 imports Deflation
     9 begin
    10 
    11 subsection {* Omega-profinite and bifinite domains *}
    12 
    13 class profinite =
    14   fixes approx :: "nat \<Rightarrow> 'a \<rightarrow> 'a"
    15   assumes chain_approx [simp]: "chain approx"
    16   assumes lub_approx_app [simp]: "(\<Squnion>i. approx i\<cdot>x) = x"
    17   assumes approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
    18   assumes finite_fixes_approx: "finite {x. approx i\<cdot>x = x}"
    19 
    20 class bifinite = profinite + pcpo
    21 
    22 lemma approx_below: "approx i\<cdot>x \<sqsubseteq> x"
    23 proof -
    24   have "chain (\<lambda>i. approx i\<cdot>x)" by simp
    25   hence "approx i\<cdot>x \<sqsubseteq> (\<Squnion>i. approx i\<cdot>x)" by (rule is_ub_thelub)
    26   thus "approx i\<cdot>x \<sqsubseteq> x" by simp
    27 qed
    28 
    29 lemma finite_deflation_approx: "finite_deflation (approx i)"
    30 proof
    31   fix x :: 'a
    32   show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
    33     by (rule approx_idem)
    34   show "approx i\<cdot>x \<sqsubseteq> x"
    35     by (rule approx_below)
    36   show "finite {x. approx i\<cdot>x = x}"
    37     by (rule finite_fixes_approx)
    38 qed
    39 
    40 interpretation approx: finite_deflation "approx i"
    41 by (rule finite_deflation_approx)
    42 
    43 lemma (in deflation) deflation: "deflation d" ..
    44 
    45 lemma deflation_approx: "deflation (approx i)"
    46 by (rule approx.deflation)
    47 
    48 lemma lub_approx [simp]: "(\<Squnion>i. approx i) = (\<Lambda> x. x)"
    49 by (rule ext_cfun, simp add: contlub_cfun_fun)
    50 
    51 lemma approx_strict [simp]: "approx i\<cdot>\<bottom> = \<bottom>"
    52 by (rule UU_I, rule approx_below)
    53 
    54 lemma approx_approx1:
    55   "i \<le> j \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx i\<cdot>x"
    56 apply (rule deflation_below_comp1 [OF deflation_approx deflation_approx])
    57 apply (erule chain_mono [OF chain_approx])
    58 done
    59 
    60 lemma approx_approx2:
    61   "j \<le> i \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx j\<cdot>x"
    62 apply (rule deflation_below_comp2 [OF deflation_approx deflation_approx])
    63 apply (erule chain_mono [OF chain_approx])
    64 done
    65 
    66 lemma approx_approx [simp]:
    67   "approx i\<cdot>(approx j\<cdot>x) = approx (min i j)\<cdot>x"
    68 apply (rule_tac x=i and y=j in linorder_le_cases)
    69 apply (simp add: approx_approx1 min_def)
    70 apply (simp add: approx_approx2 min_def)
    71 done
    72 
    73 lemma finite_image_approx: "finite ((\<lambda>x. approx n\<cdot>x) ` A)"
    74 by (rule approx.finite_image)
    75 
    76 lemma finite_range_approx: "finite (range (\<lambda>x. approx i\<cdot>x))"
    77 by (rule approx.finite_range)
    78 
    79 lemma compact_approx [simp]: "compact (approx n\<cdot>x)"
    80 by (rule approx.compact)
    81 
    82 lemma profinite_compact_eq_approx: "compact x \<Longrightarrow> \<exists>i. approx i\<cdot>x = x"
    83 by (rule admD2, simp_all)
    84 
    85 lemma profinite_compact_iff: "compact x \<longleftrightarrow> (\<exists>n. approx n\<cdot>x = x)"
    86  apply (rule iffI)
    87   apply (erule profinite_compact_eq_approx)
    88  apply (erule exE)
    89  apply (erule subst)
    90  apply (rule compact_approx)
    91 done
    92 
    93 lemma approx_induct:
    94   assumes adm: "adm P" and P: "\<And>n x. P (approx n\<cdot>x)"
    95   shows "P x"
    96 proof -
    97   have "P (\<Squnion>n. approx n\<cdot>x)"
    98     by (rule admD [OF adm], simp, simp add: P)
    99   thus "P x" by simp
   100 qed
   101 
   102 lemma profinite_below_ext: "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y"
   103 apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> (\<Squnion>i. approx i\<cdot>y)", simp)
   104 apply (rule lub_mono, simp, simp, simp)
   105 done
   106 
   107 subsection {* Instance for product type *}
   108 
   109 definition
   110   cprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
   111 where
   112   "cprod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))"
   113 
   114 lemma cprod_map_Pair [simp]: "cprod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
   115 unfolding cprod_map_def by simp
   116 
   117 lemma cprod_map_ID: "cprod_map\<cdot>ID\<cdot>ID = ID"
   118 unfolding expand_cfun_eq by auto
   119 
   120 lemma cprod_map_map:
   121   "cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
   122     cprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
   123 by (induct p) simp
   124 
   125 lemma ep_pair_cprod_map:
   126   assumes "ep_pair e1 p1" and "ep_pair e2 p2"
   127   shows "ep_pair (cprod_map\<cdot>e1\<cdot>e2) (cprod_map\<cdot>p1\<cdot>p2)"
   128 proof
   129   interpret e1p1: ep_pair e1 p1 by fact
   130   interpret e2p2: ep_pair e2 p2 by fact
   131   fix x show "cprod_map\<cdot>p1\<cdot>p2\<cdot>(cprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
   132     by (induct x) simp
   133   fix y show "cprod_map\<cdot>e1\<cdot>e2\<cdot>(cprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
   134     by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below)
   135 qed
   136 
   137 lemma deflation_cprod_map:
   138   assumes "deflation d1" and "deflation d2"
   139   shows "deflation (cprod_map\<cdot>d1\<cdot>d2)"
   140 proof
   141   interpret d1: deflation d1 by fact
   142   interpret d2: deflation d2 by fact
   143   fix x
   144   show "cprod_map\<cdot>d1\<cdot>d2\<cdot>(cprod_map\<cdot>d1\<cdot>d2\<cdot>x) = cprod_map\<cdot>d1\<cdot>d2\<cdot>x"
   145     by (induct x) (simp add: d1.idem d2.idem)
   146   show "cprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
   147     by (induct x) (simp add: d1.below d2.below)
   148 qed
   149 
   150 lemma finite_deflation_cprod_map:
   151   assumes "finite_deflation d1" and "finite_deflation d2"
   152   shows "finite_deflation (cprod_map\<cdot>d1\<cdot>d2)"
   153 proof (intro finite_deflation.intro finite_deflation_axioms.intro)
   154   interpret d1: finite_deflation d1 by fact
   155   interpret d2: finite_deflation d2 by fact
   156   have "deflation d1" and "deflation d2" by fact+
   157   thus "deflation (cprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_cprod_map)
   158   have "{p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}"
   159     by clarsimp
   160   thus "finite {p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p}"
   161     by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
   162 qed
   163 
   164 instantiation prod :: (profinite, profinite) profinite
   165 begin
   166 
   167 definition
   168   approx_prod_def:
   169     "approx = (\<lambda>n. cprod_map\<cdot>(approx n)\<cdot>(approx n))"
   170 
   171 instance proof
   172   fix i :: nat and x :: "'a \<times> 'b"
   173   show "chain (approx :: nat \<Rightarrow> 'a \<times> 'b \<rightarrow> 'a \<times> 'b)"
   174     unfolding approx_prod_def by simp
   175   show "(\<Squnion>i. approx i\<cdot>x) = x"
   176     unfolding approx_prod_def cprod_map_def
   177     by (simp add: lub_distribs thelub_Pair)
   178   show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
   179     unfolding approx_prod_def cprod_map_def by simp
   180   have "{x::'a \<times> 'b. approx i\<cdot>x = x} \<subseteq>
   181         {x::'a. approx i\<cdot>x = x} \<times> {x::'b. approx i\<cdot>x = x}"
   182     unfolding approx_prod_def by clarsimp
   183   thus "finite {x::'a \<times> 'b. approx i\<cdot>x = x}"
   184     by (rule finite_subset,
   185         intro finite_cartesian_product finite_fixes_approx)
   186 qed
   187 
   188 end
   189 
   190 instance prod :: (bifinite, bifinite) bifinite ..
   191 
   192 lemma approx_Pair [simp]:
   193   "approx i\<cdot>(x, y) = (approx i\<cdot>x, approx i\<cdot>y)"
   194 unfolding approx_prod_def by simp
   195 
   196 lemma fst_approx: "fst (approx i\<cdot>p) = approx i\<cdot>(fst p)"
   197 by (induct p, simp)
   198 
   199 lemma snd_approx: "snd (approx i\<cdot>p) = approx i\<cdot>(snd p)"
   200 by (induct p, simp)
   201 
   202 
   203 subsection {* Instance for continuous function space *}
   204 
   205 definition
   206   cfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)"
   207 where
   208   "cfun_map = (\<Lambda> a b f x. b\<cdot>(f\<cdot>(a\<cdot>x)))"
   209 
   210 lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))"
   211 unfolding cfun_map_def by simp
   212 
   213 lemma cfun_map_ID: "cfun_map\<cdot>ID\<cdot>ID = ID"
   214 unfolding expand_cfun_eq by simp
   215 
   216 lemma cfun_map_map:
   217   "cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
   218     cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
   219 by (rule ext_cfun) simp
   220 
   221 lemma ep_pair_cfun_map:
   222   assumes "ep_pair e1 p1" and "ep_pair e2 p2"
   223   shows "ep_pair (cfun_map\<cdot>p1\<cdot>e2) (cfun_map\<cdot>e1\<cdot>p2)"
   224 proof
   225   interpret e1p1: ep_pair e1 p1 by fact
   226   interpret e2p2: ep_pair e2 p2 by fact
   227   fix f show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
   228     by (simp add: expand_cfun_eq)
   229   fix g show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
   230     apply (rule below_cfun_ext, simp)
   231     apply (rule below_trans [OF e2p2.e_p_below])
   232     apply (rule monofun_cfun_arg)
   233     apply (rule e1p1.e_p_below)
   234     done
   235 qed
   236 
   237 lemma deflation_cfun_map:
   238   assumes "deflation d1" and "deflation d2"
   239   shows "deflation (cfun_map\<cdot>d1\<cdot>d2)"
   240 proof
   241   interpret d1: deflation d1 by fact
   242   interpret d2: deflation d2 by fact
   243   fix f
   244   show "cfun_map\<cdot>d1\<cdot>d2\<cdot>(cfun_map\<cdot>d1\<cdot>d2\<cdot>f) = cfun_map\<cdot>d1\<cdot>d2\<cdot>f"
   245     by (simp add: expand_cfun_eq d1.idem d2.idem)
   246   show "cfun_map\<cdot>d1\<cdot>d2\<cdot>f \<sqsubseteq> f"
   247     apply (rule below_cfun_ext, simp)
   248     apply (rule below_trans [OF d2.below])
   249     apply (rule monofun_cfun_arg)
   250     apply (rule d1.below)
   251     done
   252 qed
   253 
   254 lemma finite_range_cfun_map:
   255   assumes a: "finite (range (\<lambda>x. a\<cdot>x))"
   256   assumes b: "finite (range (\<lambda>y. b\<cdot>y))"
   257   shows "finite (range (\<lambda>f. cfun_map\<cdot>a\<cdot>b\<cdot>f))"  (is "finite (range ?h)")
   258 proof (rule finite_imageD)
   259   let ?f = "\<lambda>g. range (\<lambda>x. (a\<cdot>x, g\<cdot>x))"
   260   show "finite (?f ` range ?h)"
   261   proof (rule finite_subset)
   262     let ?B = "Pow (range (\<lambda>x. a\<cdot>x) \<times> range (\<lambda>y. b\<cdot>y))"
   263     show "?f ` range ?h \<subseteq> ?B"
   264       by clarsimp
   265     show "finite ?B"
   266       by (simp add: a b)
   267   qed
   268   show "inj_on ?f (range ?h)"
   269   proof (rule inj_onI, rule ext_cfun, clarsimp)
   270     fix x f g
   271     assume "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) = range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
   272     hence "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) \<subseteq> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
   273       by (rule equalityD1)
   274     hence "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) \<in> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
   275       by (simp add: subset_eq)
   276     then obtain y where "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) = (a\<cdot>y, b\<cdot>(g\<cdot>(a\<cdot>y)))"
   277       by (rule rangeE)
   278     thus "b\<cdot>(f\<cdot>(a\<cdot>x)) = b\<cdot>(g\<cdot>(a\<cdot>x))"
   279       by clarsimp
   280   qed
   281 qed
   282 
   283 lemma finite_deflation_cfun_map:
   284   assumes "finite_deflation d1" and "finite_deflation d2"
   285   shows "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
   286 proof (intro finite_deflation.intro finite_deflation_axioms.intro)
   287   interpret d1: finite_deflation d1 by fact
   288   interpret d2: finite_deflation d2 by fact
   289   have "deflation d1" and "deflation d2" by fact+
   290   thus "deflation (cfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_cfun_map)
   291   have "finite (range (\<lambda>f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f))"
   292     using d1.finite_range d2.finite_range
   293     by (rule finite_range_cfun_map)
   294   thus "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
   295     by (rule finite_range_imp_finite_fixes)
   296 qed
   297 
   298 text {* Finite deflations are compact elements of the function space *}
   299 
   300 lemma finite_deflation_imp_compact: "finite_deflation d \<Longrightarrow> compact d"
   301 apply (frule finite_deflation_imp_deflation)
   302 apply (subgoal_tac "compact (cfun_map\<cdot>d\<cdot>d\<cdot>d)")
   303 apply (simp add: cfun_map_def deflation.idem eta_cfun)
   304 apply (rule finite_deflation.compact)
   305 apply (simp only: finite_deflation_cfun_map)
   306 done
   307 
   308 instantiation cfun :: (profinite, profinite) profinite
   309 begin
   310 
   311 definition
   312   approx_cfun_def:
   313     "approx = (\<lambda>n. cfun_map\<cdot>(approx n)\<cdot>(approx n))"
   314 
   315 instance proof
   316   show "chain (approx :: nat \<Rightarrow> ('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow> 'b))"
   317     unfolding approx_cfun_def by simp
   318 next
   319   fix x :: "'a \<rightarrow> 'b"
   320   show "(\<Squnion>i. approx i\<cdot>x) = x"
   321     unfolding approx_cfun_def cfun_map_def
   322     by (simp add: lub_distribs eta_cfun)
   323 next
   324   fix i :: nat and x :: "'a \<rightarrow> 'b"
   325   show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
   326     unfolding approx_cfun_def cfun_map_def by simp
   327 next
   328   fix i :: nat
   329   show "finite {x::'a \<rightarrow> 'b. approx i\<cdot>x = x}"
   330     unfolding approx_cfun_def
   331     by (intro finite_deflation.finite_fixes
   332               finite_deflation_cfun_map
   333               finite_deflation_approx)
   334 qed
   335 
   336 end
   337 
   338 instance cfun :: (profinite, bifinite) bifinite ..
   339 
   340 lemma approx_cfun: "approx n\<cdot>f\<cdot>x = approx n\<cdot>(f\<cdot>(approx n\<cdot>x))"
   341 by (simp add: approx_cfun_def)
   342 
   343 end