src/HOLCF/Bifinite.thy
author huffman
Mon Jan 14 21:15:20 2008 +0100 (2008-01-14)
changeset 25909 6b96b9392873
parent 25903 5e59af604d4f
child 25922 cb04d05e95fb
permissions -rw-r--r--
add class bifinite_cpo for possibly-unpointed bifinite domains
     1 (*  Title:      HOLCF/Bifinite.thy
     2     ID:         $Id$
     3     Author:     Brian Huffman
     4 *)
     5 
     6 header {* Bifinite domains and approximation *}
     7 
     8 theory Bifinite
     9 imports Cfun
    10 begin
    11 
    12 subsection {* Bifinite domains *}
    13 
    14 axclass approx < cpo
    15 
    16 consts approx :: "nat \<Rightarrow> 'a::approx \<rightarrow> 'a"
    17 
    18 axclass bifinite_cpo < approx
    19   chain_approx_app: "chain (\<lambda>i. approx i\<cdot>x)"
    20   lub_approx_app [simp]: "(\<Squnion>i. approx i\<cdot>x) = x"
    21   approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
    22   finite_fixes_approx: "finite {x. approx i\<cdot>x = x}"
    23 
    24 axclass bifinite < bifinite_cpo, pcpo
    25 
    26 lemma finite_range_imp_finite_fixes:
    27   "finite {x. \<exists>y. x = f y} \<Longrightarrow> finite {x. f x = x}"
    28 apply (subgoal_tac "{x. f x = x} \<subseteq> {x. \<exists>y. x = f y}")
    29 apply (erule (1) finite_subset)
    30 apply (clarify, erule subst, rule exI, rule refl)
    31 done
    32 
    33 lemma chain_approx [simp]:
    34   "chain (approx :: nat \<Rightarrow> 'a::bifinite_cpo \<rightarrow> 'a)"
    35 apply (rule chainI)
    36 apply (rule less_cfun_ext)
    37 apply (rule chainE)
    38 apply (rule chain_approx_app)
    39 done
    40 
    41 lemma lub_approx [simp]: "(\<Squnion>i. approx i) = (\<Lambda>(x::'a::bifinite_cpo). x)"
    42 by (rule ext_cfun, simp add: contlub_cfun_fun)
    43 
    44 lemma approx_less: "approx i\<cdot>x \<sqsubseteq> (x::'a::bifinite_cpo)"
    45 apply (subgoal_tac "approx i\<cdot>x \<sqsubseteq> (\<Squnion>i. approx i\<cdot>x)", simp)
    46 apply (rule is_ub_thelub, simp)
    47 done
    48 
    49 lemma approx_strict [simp]: "approx i\<cdot>(\<bottom>::'a::bifinite) = \<bottom>"
    50 by (rule UU_I, rule approx_less)
    51 
    52 lemma approx_approx1:
    53   "i \<le> j \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx i\<cdot>(x::'a::bifinite_cpo)"
    54 apply (rule antisym_less)
    55 apply (rule monofun_cfun_arg [OF approx_less])
    56 apply (rule sq_ord_eq_less_trans [OF approx_idem [symmetric]])
    57 apply (rule monofun_cfun_arg)
    58 apply (rule monofun_cfun_fun)
    59 apply (erule chain_mono3 [OF chain_approx])
    60 done
    61 
    62 lemma approx_approx2:
    63   "j \<le> i \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx j\<cdot>(x::'a::bifinite_cpo)"
    64 apply (rule antisym_less)
    65 apply (rule approx_less)
    66 apply (rule sq_ord_eq_less_trans [OF approx_idem [symmetric]])
    67 apply (rule monofun_cfun_fun)
    68 apply (erule chain_mono3 [OF chain_approx])
    69 done
    70 
    71 lemma approx_approx [simp]:
    72   "approx i\<cdot>(approx j\<cdot>x) = approx (min i j)\<cdot>(x::'a::bifinite_cpo)"
    73 apply (rule_tac x=i and y=j in linorder_le_cases)
    74 apply (simp add: approx_approx1 min_def)
    75 apply (simp add: approx_approx2 min_def)
    76 done
    77 
    78 lemma idem_fixes_eq_range:
    79   "\<forall>x. f (f x) = f x \<Longrightarrow> {x. f x = x} = {y. \<exists>x. y = f x}"
    80 by (auto simp add: eq_sym_conv)
    81 
    82 lemma finite_approx: "finite {y::'a::bifinite_cpo. \<exists>x. y = approx n\<cdot>x}"
    83 using finite_fixes_approx by (simp add: idem_fixes_eq_range)
    84 
    85 lemma finite_range_approx:
    86   "finite (range (\<lambda>x::'a::bifinite_cpo. approx n\<cdot>x))"
    87 by (simp add: image_def finite_approx)
    88 
    89 lemma compact_approx [simp]:
    90   fixes x :: "'a::bifinite_cpo"
    91   shows "compact (approx n\<cdot>x)"
    92 proof (rule compactI2)
    93   fix Y::"nat \<Rightarrow> 'a"
    94   assume Y: "chain Y"
    95   have "finite_chain (\<lambda>i. approx n\<cdot>(Y i))"
    96   proof (rule finite_range_imp_finch)
    97     show "chain (\<lambda>i. approx n\<cdot>(Y i))"
    98       using Y by simp
    99     have "range (\<lambda>i. approx n\<cdot>(Y i)) \<subseteq> {x. approx n\<cdot>x = x}"
   100       by clarsimp
   101     thus "finite (range (\<lambda>i. approx n\<cdot>(Y i)))"
   102       using finite_fixes_approx by (rule finite_subset)
   103   qed
   104   hence "\<exists>j. (\<Squnion>i. approx n\<cdot>(Y i)) = approx n\<cdot>(Y j)"
   105     by (simp add: finite_chain_def maxinch_is_thelub Y)
   106   then obtain j where j: "(\<Squnion>i. approx n\<cdot>(Y i)) = approx n\<cdot>(Y j)" ..
   107 
   108   assume "approx n\<cdot>x \<sqsubseteq> (\<Squnion>i. Y i)"
   109   hence "approx n\<cdot>(approx n\<cdot>x) \<sqsubseteq> approx n\<cdot>(\<Squnion>i. Y i)"
   110     by (rule monofun_cfun_arg)
   111   hence "approx n\<cdot>x \<sqsubseteq> (\<Squnion>i. approx n\<cdot>(Y i))"
   112     by (simp add: contlub_cfun_arg Y)
   113   hence "approx n\<cdot>x \<sqsubseteq> approx n\<cdot>(Y j)"
   114     using j by simp
   115   hence "approx n\<cdot>x \<sqsubseteq> Y j"
   116     using approx_less by (rule trans_less)
   117   thus "\<exists>j. approx n\<cdot>x \<sqsubseteq> Y j" ..
   118 qed
   119 
   120 lemma bifinite_compact_eq_approx:
   121   fixes x :: "'a::bifinite_cpo"
   122   assumes x: "compact x"
   123   shows "\<exists>i. approx i\<cdot>x = x"
   124 proof -
   125   have chain: "chain (\<lambda>i. approx i\<cdot>x)" by simp
   126   have less: "x \<sqsubseteq> (\<Squnion>i. approx i\<cdot>x)" by simp
   127   obtain i where i: "x \<sqsubseteq> approx i\<cdot>x"
   128     using compactD2 [OF x chain less] ..
   129   with approx_less have "approx i\<cdot>x = x"
   130     by (rule antisym_less)
   131   thus "\<exists>i. approx i\<cdot>x = x" ..
   132 qed
   133 
   134 lemma bifinite_compact_iff:
   135   "compact (x::'a::bifinite_cpo) = (\<exists>n. approx n\<cdot>x = x)"
   136  apply (rule iffI)
   137   apply (erule bifinite_compact_eq_approx)
   138  apply (erule exE)
   139  apply (erule subst)
   140  apply (rule compact_approx)
   141 done
   142 
   143 lemma approx_induct:
   144   assumes adm: "adm P" and P: "\<And>n x. P (approx n\<cdot>x)"
   145   shows "P (x::'a::bifinite)"
   146 proof -
   147   have "P (\<Squnion>n. approx n\<cdot>x)"
   148     by (rule admD [OF adm], simp, simp add: P)
   149   thus "P x" by simp
   150 qed
   151 
   152 lemma bifinite_less_ext:
   153   fixes x y :: "'a::bifinite_cpo"
   154   shows "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y"
   155 apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> (\<Squnion>i. approx i\<cdot>y)", simp)
   156 apply (rule lub_mono [rule_format], simp, simp, simp)
   157 done
   158 
   159 subsection {* Instance for continuous function space *}
   160 
   161 lemma finite_range_lemma:
   162   fixes h :: "'a::cpo \<rightarrow> 'b::cpo"
   163   fixes k :: "'c::cpo \<rightarrow> 'd::cpo"
   164   shows "\<lbrakk>finite {y. \<exists>x. y = h\<cdot>x}; finite {y. \<exists>x. y = k\<cdot>x}\<rbrakk>
   165     \<Longrightarrow> finite {g. \<exists>f. g = (\<Lambda> x. k\<cdot>(f\<cdot>(h\<cdot>x)))}"
   166  apply (rule_tac f="\<lambda>g. {(h\<cdot>x, y) |x y. y = g\<cdot>x}" in finite_imageD)
   167   apply (rule_tac B="Pow ({y. \<exists>x. y = h\<cdot>x} \<times> {y. \<exists>x. y = k\<cdot>x})"
   168            in finite_subset)
   169    apply (rule image_subsetI)
   170    apply (clarsimp, fast)
   171   apply simp
   172  apply (rule inj_onI)
   173  apply (clarsimp simp add: expand_set_eq)
   174  apply (rule ext_cfun, simp)
   175  apply (drule_tac x="h\<cdot>x" in spec)
   176  apply (drule_tac x="k\<cdot>(f\<cdot>(h\<cdot>x))" in spec)
   177  apply (drule iffD1, fast)
   178  apply clarsimp
   179 done
   180 
   181 instance "->" :: (bifinite_cpo, bifinite_cpo) approx ..
   182 
   183 defs (overloaded)
   184   approx_cfun_def:
   185     "approx \<equiv> \<lambda>n. \<Lambda> f x. approx n\<cdot>(f\<cdot>(approx n\<cdot>x))"
   186 
   187 instance "->" :: (bifinite_cpo, bifinite_cpo) bifinite_cpo
   188  apply (intro_classes, unfold approx_cfun_def)
   189     apply simp
   190    apply (simp add: lub_distribs eta_cfun)
   191   apply simp
   192  apply simp
   193  apply (rule finite_range_imp_finite_fixes)
   194  apply (intro finite_range_lemma finite_approx)
   195 done
   196 
   197 instance "->" :: (bifinite_cpo, bifinite) bifinite ..
   198 
   199 lemma approx_cfun: "approx n\<cdot>f\<cdot>x = approx n\<cdot>(f\<cdot>(approx n\<cdot>x))"
   200 by (simp add: approx_cfun_def)
   201 
   202 end