src/HOLCF/Bifinite.thy
 author huffman Fri Jun 20 22:51:50 2008 +0200 (2008-06-20) changeset 27309 c74270fd72a8 parent 27186 416d66c36d8f child 27310 d0229bc6c461 permissions -rw-r--r--
clean up and rename some profinite lemmas
```     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 {* Omega-profinite and bifinite domains *}
```
```    13
```
```    14 class profinite = cpo +
```
```    15   fixes approx :: "nat \<Rightarrow> 'a \<rightarrow> 'a"
```
```    16   assumes chain_approx_app: "chain (\<lambda>i. approx i\<cdot>x)"
```
```    17   assumes lub_approx_app [simp]: "(\<Squnion>i. approx i\<cdot>x) = x"
```
```    18   assumes approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
```
```    19   assumes finite_fixes_approx: "finite {x. approx i\<cdot>x = x}"
```
```    20
```
```    21 class bifinite = profinite + pcpo
```
```    22
```
```    23 lemma finite_range_imp_finite_fixes:
```
```    24   "finite {x. \<exists>y. x = f y} \<Longrightarrow> finite {x. f x = x}"
```
```    25 apply (subgoal_tac "{x. f x = x} \<subseteq> {x. \<exists>y. x = f y}")
```
```    26 apply (erule (1) finite_subset)
```
```    27 apply (clarify, erule subst, rule exI, rule refl)
```
```    28 done
```
```    29
```
```    30 lemma chain_approx [simp]: "chain approx"
```
```    31 apply (rule chainI)
```
```    32 apply (rule less_cfun_ext)
```
```    33 apply (rule chainE)
```
```    34 apply (rule chain_approx_app)
```
```    35 done
```
```    36
```
```    37 lemma lub_approx [simp]: "(\<Squnion>i. approx i) = (\<Lambda> x. x)"
```
```    38 by (rule ext_cfun, simp add: contlub_cfun_fun)
```
```    39
```
```    40 lemma approx_less: "approx i\<cdot>x \<sqsubseteq> x"
```
```    41 apply (subgoal_tac "approx i\<cdot>x \<sqsubseteq> (\<Squnion>i. approx i\<cdot>x)", simp)
```
```    42 apply (rule is_ub_thelub, simp)
```
```    43 done
```
```    44
```
```    45 lemma approx_strict [simp]: "approx i\<cdot>\<bottom> = \<bottom>"
```
```    46 by (rule UU_I, rule approx_less)
```
```    47
```
```    48 lemma approx_approx1:
```
```    49   "i \<le> j \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx i\<cdot>x"
```
```    50 apply (rule antisym_less)
```
```    51 apply (rule monofun_cfun_arg [OF approx_less])
```
```    52 apply (rule sq_ord_eq_less_trans [OF approx_idem [symmetric]])
```
```    53 apply (rule monofun_cfun_arg)
```
```    54 apply (rule monofun_cfun_fun)
```
```    55 apply (erule chain_mono [OF chain_approx])
```
```    56 done
```
```    57
```
```    58 lemma approx_approx2:
```
```    59   "j \<le> i \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx j\<cdot>x"
```
```    60 apply (rule antisym_less)
```
```    61 apply (rule approx_less)
```
```    62 apply (rule sq_ord_eq_less_trans [OF approx_idem [symmetric]])
```
```    63 apply (rule monofun_cfun_fun)
```
```    64 apply (erule chain_mono [OF chain_approx])
```
```    65 done
```
```    66
```
```    67 lemma approx_approx [simp]:
```
```    68   "approx i\<cdot>(approx j\<cdot>x) = approx (min i j)\<cdot>x"
```
```    69 apply (rule_tac x=i and y=j in linorder_le_cases)
```
```    70 apply (simp add: approx_approx1 min_def)
```
```    71 apply (simp add: approx_approx2 min_def)
```
```    72 done
```
```    73
```
```    74 lemma idem_fixes_eq_range:
```
```    75   "\<forall>x. f (f x) = f x \<Longrightarrow> {x. f x = x} = {y. \<exists>x. y = f x}"
```
```    76 by (auto simp add: eq_sym_conv)
```
```    77
```
```    78 lemma finite_approx: "finite {y. \<exists>x. y = approx n\<cdot>x}"
```
```    79 using finite_fixes_approx by (simp add: idem_fixes_eq_range)
```
```    80
```
```    81 lemma finite_image_approx: "finite ((\<lambda>x. approx n\<cdot>x) ` A)"
```
```    82 by (rule finite_subset [OF _ finite_fixes_approx [where i=n]]) auto
```
```    83
```
```    84 lemma finite_range_approx: "finite (range (\<lambda>x. approx n\<cdot>x))"
```
```    85 by (rule finite_image_approx)
```
```    86
```
```    87 lemma compact_approx [simp]: "compact (approx n\<cdot>x)"
```
```    88 proof (rule compactI2)
```
```    89   fix Y::"nat \<Rightarrow> 'a"
```
```    90   assume Y: "chain Y"
```
```    91   have "finite_chain (\<lambda>i. approx n\<cdot>(Y i))"
```
```    92   proof (rule finite_range_imp_finch)
```
```    93     show "chain (\<lambda>i. approx n\<cdot>(Y i))"
```
```    94       using Y by simp
```
```    95     have "range (\<lambda>i. approx n\<cdot>(Y i)) \<subseteq> {x. approx n\<cdot>x = x}"
```
```    96       by clarsimp
```
```    97     thus "finite (range (\<lambda>i. approx n\<cdot>(Y i)))"
```
```    98       using finite_fixes_approx by (rule finite_subset)
```
```    99   qed
```
```   100   hence "\<exists>j. (\<Squnion>i. approx n\<cdot>(Y i)) = approx n\<cdot>(Y j)"
```
```   101     by (simp add: finite_chain_def maxinch_is_thelub Y)
```
```   102   then obtain j where j: "(\<Squnion>i. approx n\<cdot>(Y i)) = approx n\<cdot>(Y j)" ..
```
```   103
```
```   104   assume "approx n\<cdot>x \<sqsubseteq> (\<Squnion>i. Y i)"
```
```   105   hence "approx n\<cdot>(approx n\<cdot>x) \<sqsubseteq> approx n\<cdot>(\<Squnion>i. Y i)"
```
```   106     by (rule monofun_cfun_arg)
```
```   107   hence "approx n\<cdot>x \<sqsubseteq> (\<Squnion>i. approx n\<cdot>(Y i))"
```
```   108     by (simp add: contlub_cfun_arg Y)
```
```   109   hence "approx n\<cdot>x \<sqsubseteq> approx n\<cdot>(Y j)"
```
```   110     using j by simp
```
```   111   hence "approx n\<cdot>x \<sqsubseteq> Y j"
```
```   112     using approx_less by (rule trans_less)
```
```   113   thus "\<exists>j. approx n\<cdot>x \<sqsubseteq> Y j" ..
```
```   114 qed
```
```   115
```
```   116 lemma profinite_compact_eq_approx: "compact x \<Longrightarrow> \<exists>i. approx i\<cdot>x = x"
```
```   117 by (rule admD2) simp_all
```
```   118
```
```   119 lemma profinite_compact_iff: "compact x \<longleftrightarrow> (\<exists>n. approx n\<cdot>x = x)"
```
```   120  apply (rule iffI)
```
```   121   apply (erule profinite_compact_eq_approx)
```
```   122  apply (erule exE)
```
```   123  apply (erule subst)
```
```   124  apply (rule compact_approx)
```
```   125 done
```
```   126
```
```   127 lemma approx_induct:
```
```   128   assumes adm: "adm P" and P: "\<And>n x. P (approx n\<cdot>x)"
```
```   129   shows "P x"
```
```   130 proof -
```
```   131   have "P (\<Squnion>n. approx n\<cdot>x)"
```
```   132     by (rule admD [OF adm], simp, simp add: P)
```
```   133   thus "P x" by simp
```
```   134 qed
```
```   135
```
```   136 lemma profinite_less_ext: "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y"
```
```   137 apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> (\<Squnion>i. approx i\<cdot>y)", simp)
```
```   138 apply (rule lub_mono, simp, simp, simp)
```
```   139 done
```
```   140
```
```   141 subsection {* Instance for continuous function space *}
```
```   142
```
```   143 lemma finite_range_lemma:
```
```   144   fixes h :: "'a::cpo \<rightarrow> 'b::cpo"
```
```   145   fixes k :: "'c::cpo \<rightarrow> 'd::cpo"
```
```   146   shows "\<lbrakk>finite {y. \<exists>x. y = h\<cdot>x}; finite {y. \<exists>x. y = k\<cdot>x}\<rbrakk>
```
```   147     \<Longrightarrow> finite {g. \<exists>f. g = (\<Lambda> x. k\<cdot>(f\<cdot>(h\<cdot>x)))}"
```
```   148  apply (rule_tac f="\<lambda>g. {(h\<cdot>x, y) |x y. y = g\<cdot>x}" in finite_imageD)
```
```   149   apply (rule_tac B="Pow ({y. \<exists>x. y = h\<cdot>x} \<times> {y. \<exists>x. y = k\<cdot>x})"
```
```   150            in finite_subset)
```
```   151    apply (rule image_subsetI)
```
```   152    apply (clarsimp, fast)
```
```   153   apply simp
```
```   154  apply (rule inj_onI)
```
```   155  apply (clarsimp simp add: expand_set_eq)
```
```   156  apply (rule ext_cfun, simp)
```
```   157  apply (drule_tac x="h\<cdot>x" in spec)
```
```   158  apply (drule_tac x="k\<cdot>(f\<cdot>(h\<cdot>x))" in spec)
```
```   159  apply (drule iffD1, fast)
```
```   160  apply clarsimp
```
```   161 done
```
```   162
```
```   163 instantiation "->" :: (profinite, profinite) profinite
```
```   164 begin
```
```   165
```
```   166 definition
```
```   167   approx_cfun_def:
```
```   168     "approx = (\<lambda>n. \<Lambda> f x. approx n\<cdot>(f\<cdot>(approx n\<cdot>x)))"
```
```   169
```
```   170 instance
```
```   171  apply (intro_classes, unfold approx_cfun_def)
```
```   172     apply simp
```
```   173    apply (simp add: lub_distribs eta_cfun)
```
```   174   apply simp
```
```   175  apply simp
```
```   176  apply (rule finite_range_imp_finite_fixes)
```
```   177  apply (intro finite_range_lemma finite_approx)
```
```   178 done
```
```   179
```
```   180 end
```
```   181
```
```   182 instance "->" :: (profinite, bifinite) bifinite ..
```
```   183
```
```   184 lemma approx_cfun: "approx n\<cdot>f\<cdot>x = approx n\<cdot>(f\<cdot>(approx n\<cdot>x))"
```
```   185 by (simp add: approx_cfun_def)
```
```   186
```
```   187 end
```