src/HOLCF/Bifinite.thy
author haftmann
Fri Jun 19 21:08:07 2009 +0200 (2009-06-19)
changeset 31726 ffd2dc631d88
parent 31113 15cf300a742f
child 33504 b4210cc3ac97
permissions -rw-r--r--
merged
     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 instantiation "*" :: (profinite, profinite) profinite
   110 begin
   111 
   112 definition approx_prod_def:
   113   "approx = (\<lambda>n. \<Lambda> x. (approx n\<cdot>(fst x), approx n\<cdot>(snd x)))"
   114 
   115 instance proof
   116   fix i :: nat and x :: "'a \<times> 'b"
   117   show "chain (approx :: nat \<Rightarrow> 'a \<times> 'b \<rightarrow> 'a \<times> 'b)"
   118     unfolding approx_prod_def by simp
   119   show "(\<Squnion>i. approx i\<cdot>x) = x"
   120     unfolding approx_prod_def
   121     by (simp add: lub_distribs thelub_Pair)
   122   show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
   123     unfolding approx_prod_def by simp
   124   have "{x::'a \<times> 'b. approx i\<cdot>x = x} \<subseteq>
   125         {x::'a. approx i\<cdot>x = x} \<times> {x::'b. approx i\<cdot>x = x}"
   126     unfolding approx_prod_def by clarsimp
   127   thus "finite {x::'a \<times> 'b. approx i\<cdot>x = x}"
   128     by (rule finite_subset,
   129         intro finite_cartesian_product finite_fixes_approx)
   130 qed
   131 
   132 end
   133 
   134 instance "*" :: (bifinite, bifinite) bifinite ..
   135 
   136 lemma approx_Pair [simp]:
   137   "approx i\<cdot>(x, y) = (approx i\<cdot>x, approx i\<cdot>y)"
   138 unfolding approx_prod_def by simp
   139 
   140 lemma fst_approx: "fst (approx i\<cdot>p) = approx i\<cdot>(fst p)"
   141 by (induct p, simp)
   142 
   143 lemma snd_approx: "snd (approx i\<cdot>p) = approx i\<cdot>(snd p)"
   144 by (induct p, simp)
   145 
   146 
   147 subsection {* Instance for continuous function space *}
   148 
   149 lemma finite_range_cfun_lemma:
   150   assumes a: "finite (range (\<lambda>x. a\<cdot>x))"
   151   assumes b: "finite (range (\<lambda>y. b\<cdot>y))"
   152   shows "finite (range (\<lambda>f. \<Lambda> x. b\<cdot>(f\<cdot>(a\<cdot>x))))"  (is "finite (range ?h)")
   153 proof (rule finite_imageD)
   154   let ?f = "\<lambda>g. range (\<lambda>x. (a\<cdot>x, g\<cdot>x))"
   155   show "finite (?f ` range ?h)"
   156   proof (rule finite_subset)
   157     let ?B = "Pow (range (\<lambda>x. a\<cdot>x) \<times> range (\<lambda>y. b\<cdot>y))"
   158     show "?f ` range ?h \<subseteq> ?B"
   159       by clarsimp
   160     show "finite ?B"
   161       by (simp add: a b)
   162   qed
   163   show "inj_on ?f (range ?h)"
   164   proof (rule inj_onI, rule ext_cfun, clarsimp)
   165     fix x f g
   166     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))))"
   167     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))))"
   168       by (rule equalityD1)
   169     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))))"
   170       by (simp add: subset_eq)
   171     then obtain y where "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) = (a\<cdot>y, b\<cdot>(g\<cdot>(a\<cdot>y)))"
   172       by (rule rangeE)
   173     thus "b\<cdot>(f\<cdot>(a\<cdot>x)) = b\<cdot>(g\<cdot>(a\<cdot>x))"
   174       by clarsimp
   175   qed
   176 qed
   177 
   178 instantiation "->" :: (profinite, profinite) profinite
   179 begin
   180 
   181 definition
   182   approx_cfun_def:
   183     "approx = (\<lambda>n. \<Lambda> f x. approx n\<cdot>(f\<cdot>(approx n\<cdot>x)))"
   184 
   185 instance proof
   186   show "chain (approx :: nat \<Rightarrow> ('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow> 'b))"
   187     unfolding approx_cfun_def by simp
   188 next
   189   fix x :: "'a \<rightarrow> 'b"
   190   show "(\<Squnion>i. approx i\<cdot>x) = x"
   191     unfolding approx_cfun_def
   192     by (simp add: lub_distribs eta_cfun)
   193 next
   194   fix i :: nat and x :: "'a \<rightarrow> 'b"
   195   show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
   196     unfolding approx_cfun_def by simp
   197 next
   198   fix i :: nat
   199   show "finite {x::'a \<rightarrow> 'b. approx i\<cdot>x = x}"
   200     apply (rule finite_range_imp_finite_fixes)
   201     apply (simp add: approx_cfun_def)
   202     apply (intro finite_range_cfun_lemma finite_range_approx)
   203     done
   204 qed
   205 
   206 end
   207 
   208 instance "->" :: (profinite, bifinite) bifinite ..
   209 
   210 lemma approx_cfun: "approx n\<cdot>f\<cdot>x = approx n\<cdot>(f\<cdot>(approx n\<cdot>x))"
   211 by (simp add: approx_cfun_def)
   212 
   213 end