add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
authorhuffman
Mon Oct 11 09:54:04 2010 -0700 (2010-10-11)
changeset 39999e3948547b541
parent 39989 ad60d7311f43
child 40000 9c6ad000dc89
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
src/HOLCF/IsaMakefile
src/HOLCF/Library/Defl_Bifinite.thy
src/HOLCF/Library/HOLCF_Library.thy
     1.1 --- a/src/HOLCF/IsaMakefile	Mon Oct 11 08:32:09 2010 -0700
     1.2 +++ b/src/HOLCF/IsaMakefile	Mon Oct 11 09:54:04 2010 -0700
     1.3 @@ -102,6 +102,7 @@
     1.4  HOLCF-Library: HOLCF $(LOG)/HOLCF-Library.gz
     1.5  
     1.6  $(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \
     1.7 +  Library/Defl_Bifinite.thy \
     1.8    Library/List_Cpo.thy \
     1.9    Library/Stream.thy \
    1.10    Library/Strict_Fun.thy \
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOLCF/Library/Defl_Bifinite.thy	Mon Oct 11 09:54:04 2010 -0700
     2.3 @@ -0,0 +1,650 @@
     2.4 +(*  Title:      HOLCF/Library/Defl_Bifinite.thy
     2.5 +    Author:     Brian Huffman
     2.6 +*)
     2.7 +
     2.8 +header {* Algebraic deflations are a bifinite domain *}
     2.9 +
    2.10 +theory Defl_Bifinite
    2.11 +imports HOLCF Infinite_Set
    2.12 +begin
    2.13 +
    2.14 +subsection {* Lemmas about MOST *}
    2.15 +
    2.16 +default_sort type
    2.17 +
    2.18 +lemma MOST_INFM:
    2.19 +  assumes inf: "infinite (UNIV::'a set)"
    2.20 +  shows "MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x"
    2.21 +  unfolding Alm_all_def Inf_many_def
    2.22 +  apply (auto simp add: Collect_neg_eq)
    2.23 +  apply (drule (1) finite_UnI)
    2.24 +  apply (simp add: Compl_partition2 inf)
    2.25 +  done
    2.26 +
    2.27 +lemma MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
    2.28 +by (rule MOST_inj [OF _ inj_Suc])
    2.29 +
    2.30 +lemma MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
    2.31 +unfolding MOST_nat
    2.32 +apply (clarify, rule_tac x="Suc m" in exI, clarify)
    2.33 +apply (erule Suc_lessE, simp)
    2.34 +done
    2.35 +
    2.36 +lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
    2.37 +by (rule iffI [OF MOST_SucD MOST_SucI])
    2.38 +
    2.39 +lemma INFM_finite_Bex_distrib:
    2.40 +  "finite A \<Longrightarrow> (INFM y. \<exists>x\<in>A. P x y) \<longleftrightarrow> (\<exists>x\<in>A. INFM y. P x y)"
    2.41 +by (induct set: finite, simp, simp add: INFM_disj_distrib)
    2.42 +
    2.43 +lemma MOST_finite_Ball_distrib:
    2.44 +  "finite A \<Longrightarrow> (MOST y. \<forall>x\<in>A. P x y) \<longleftrightarrow> (\<forall>x\<in>A. MOST y. P x y)"
    2.45 +by (induct set: finite, simp, simp add: MOST_conj_distrib)
    2.46 +
    2.47 +lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
    2.48 +unfolding MOST_nat_le by fast
    2.49 +
    2.50 +subsection {* Eventually constant sequences *}
    2.51 +
    2.52 +definition
    2.53 +  eventually_constant :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool"
    2.54 +where
    2.55 +  "eventually_constant S = (\<exists>x. MOST i. S i = x)"
    2.56 +
    2.57 +lemma eventually_constant_MOST_MOST:
    2.58 +  "eventually_constant S \<longleftrightarrow> (MOST m. MOST n. S n = S m)"
    2.59 +unfolding eventually_constant_def MOST_nat
    2.60 +apply safe
    2.61 +apply (rule_tac x=m in exI, clarify)
    2.62 +apply (rule_tac x=m in exI, clarify)
    2.63 +apply simp
    2.64 +apply fast
    2.65 +done
    2.66 +
    2.67 +lemma eventually_constantI: "MOST i. S i = x \<Longrightarrow> eventually_constant S"
    2.68 +unfolding eventually_constant_def by fast
    2.69 +
    2.70 +lemma eventually_constant_comp:
    2.71 +  "eventually_constant (\<lambda>i. S i) \<Longrightarrow> eventually_constant (\<lambda>i. f (S i))"
    2.72 +unfolding eventually_constant_def
    2.73 +apply (erule exE, rule_tac x="f x" in exI)
    2.74 +apply (erule MOST_mono, simp)
    2.75 +done
    2.76 +
    2.77 +lemma eventually_constant_Suc_iff:
    2.78 +  "eventually_constant (\<lambda>i. S (Suc i)) \<longleftrightarrow> eventually_constant (\<lambda>i. S i)"
    2.79 +unfolding eventually_constant_def
    2.80 +by (subst MOST_Suc_iff, rule refl)
    2.81 +
    2.82 +lemma eventually_constant_SucD:
    2.83 +  "eventually_constant (\<lambda>i. S (Suc i)) \<Longrightarrow> eventually_constant (\<lambda>i. S i)"
    2.84 +by (rule eventually_constant_Suc_iff [THEN iffD1])
    2.85 +
    2.86 +subsection {* Limits of eventually constant sequences *}
    2.87 +
    2.88 +definition
    2.89 +  eventual :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a" where
    2.90 +  "eventual S = (THE x. MOST i. S i = x)"
    2.91 +
    2.92 +lemma eventual_eqI: "MOST i. S i = x \<Longrightarrow> eventual S = x"
    2.93 +unfolding eventual_def
    2.94 +apply (rule the_equality, assumption)
    2.95 +apply (rename_tac y)
    2.96 +apply (subgoal_tac "MOST i::nat. y = x", simp)
    2.97 +apply (erule MOST_rev_mp)
    2.98 +apply (erule MOST_rev_mp)
    2.99 +apply simp
   2.100 +done
   2.101 +
   2.102 +lemma MOST_eq_eventual:
   2.103 +  "eventually_constant S \<Longrightarrow> MOST i. S i = eventual S"
   2.104 +unfolding eventually_constant_def
   2.105 +by (erule exE, simp add: eventual_eqI)
   2.106 +
   2.107 +lemma eventual_mem_range:
   2.108 +  "eventually_constant S \<Longrightarrow> eventual S \<in> range S"
   2.109 +apply (drule MOST_eq_eventual)
   2.110 +apply (simp only: MOST_nat_le, clarify)
   2.111 +apply (drule spec, drule mp, rule order_refl)
   2.112 +apply (erule range_eqI [OF sym])
   2.113 +done
   2.114 +
   2.115 +lemma eventually_constant_MOST_iff:
   2.116 +  assumes S: "eventually_constant S"
   2.117 +  shows "(MOST n. P (S n)) \<longleftrightarrow> P (eventual S)"
   2.118 +apply (subgoal_tac "(MOST n. P (S n)) \<longleftrightarrow> (MOST n::nat. P (eventual S))")
   2.119 +apply simp
   2.120 +apply (rule iffI)
   2.121 +apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]])
   2.122 +apply (erule MOST_mono, force)
   2.123 +apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]])
   2.124 +apply (erule MOST_mono, simp)
   2.125 +done
   2.126 +
   2.127 +lemma MOST_eventual:
   2.128 +  "\<lbrakk>eventually_constant S; MOST n. P (S n)\<rbrakk> \<Longrightarrow> P (eventual S)"
   2.129 +proof -
   2.130 +  assume "eventually_constant S"
   2.131 +  hence "MOST n. S n = eventual S"
   2.132 +    by (rule MOST_eq_eventual)
   2.133 +  moreover assume "MOST n. P (S n)"
   2.134 +  ultimately have "MOST n. S n = eventual S \<and> P (S n)"
   2.135 +    by (rule MOST_conj_distrib [THEN iffD2, OF conjI])
   2.136 +  hence "MOST n::nat. P (eventual S)"
   2.137 +    by (rule MOST_mono) auto
   2.138 +  thus ?thesis by simp
   2.139 +qed
   2.140 +
   2.141 +lemma eventually_constant_MOST_Suc_eq:
   2.142 +  "eventually_constant S \<Longrightarrow> MOST n. S (Suc n) = S n"
   2.143 +apply (drule MOST_eq_eventual)
   2.144 +apply (frule MOST_Suc_iff [THEN iffD2])
   2.145 +apply (erule MOST_rev_mp)
   2.146 +apply (erule MOST_rev_mp)
   2.147 +apply simp
   2.148 +done
   2.149 +
   2.150 +lemma eventual_comp:
   2.151 +  "eventually_constant S \<Longrightarrow> eventual (\<lambda>i. f (S i)) = f (eventual (\<lambda>i. S i))"
   2.152 +apply (rule eventual_eqI)
   2.153 +apply (rule MOST_mono)
   2.154 +apply (erule MOST_eq_eventual)
   2.155 +apply simp
   2.156 +done
   2.157 +
   2.158 +subsection {* Constructing finite deflations by iteration *}
   2.159 +
   2.160 +default_sort cpo
   2.161 +
   2.162 +lemma le_Suc_induct:
   2.163 +  assumes le: "i \<le> j"
   2.164 +  assumes step: "\<And>i. P i (Suc i)"
   2.165 +  assumes refl: "\<And>i. P i i"
   2.166 +  assumes trans: "\<And>i j k. \<lbrakk>P i j; P j k\<rbrakk> \<Longrightarrow> P i k"
   2.167 +  shows "P i j"
   2.168 +proof (cases "i = j")
   2.169 +  assume "i = j"
   2.170 +  thus "P i j" by (simp add: refl)
   2.171 +next
   2.172 +  assume "i \<noteq> j"
   2.173 +  with le have "i < j" by simp
   2.174 +  thus "P i j" using step trans by (rule less_Suc_induct)
   2.175 +qed
   2.176 +
   2.177 +definition
   2.178 +  eventual_iterate :: "('a \<rightarrow> 'a::cpo) \<Rightarrow> ('a \<rightarrow> 'a)"
   2.179 +where
   2.180 +  "eventual_iterate f = eventual (\<lambda>n. iterate n\<cdot>f)"
   2.181 +
   2.182 +text {* A pre-deflation is like a deflation, but not idempotent. *}
   2.183 +
   2.184 +locale pre_deflation =
   2.185 +  fixes f :: "'a \<rightarrow> 'a::cpo"
   2.186 +  assumes below: "\<And>x. f\<cdot>x \<sqsubseteq> x"
   2.187 +  assumes finite_range: "finite (range (\<lambda>x. f\<cdot>x))"
   2.188 +begin
   2.189 +
   2.190 +lemma iterate_below: "iterate i\<cdot>f\<cdot>x \<sqsubseteq> x"
   2.191 +by (induct i, simp_all add: below_trans [OF below])
   2.192 +
   2.193 +lemma iterate_fixed: "f\<cdot>x = x \<Longrightarrow> iterate i\<cdot>f\<cdot>x = x"
   2.194 +by (induct i, simp_all)
   2.195 +
   2.196 +lemma antichain_iterate_app: "i \<le> j \<Longrightarrow> iterate j\<cdot>f\<cdot>x \<sqsubseteq> iterate i\<cdot>f\<cdot>x"
   2.197 +apply (erule le_Suc_induct)
   2.198 +apply (simp add: below)
   2.199 +apply (rule below_refl)
   2.200 +apply (erule (1) below_trans)
   2.201 +done
   2.202 +
   2.203 +lemma finite_range_iterate_app: "finite (range (\<lambda>i. iterate i\<cdot>f\<cdot>x))"
   2.204 +proof (rule finite_subset)
   2.205 +  show "range (\<lambda>i. iterate i\<cdot>f\<cdot>x) \<subseteq> insert x (range (\<lambda>x. f\<cdot>x))"
   2.206 +    by (clarify, case_tac i, simp_all)
   2.207 +  show "finite (insert x (range (\<lambda>x. f\<cdot>x)))"
   2.208 +    by (simp add: finite_range)
   2.209 +qed
   2.210 +
   2.211 +lemma eventually_constant_iterate_app:
   2.212 +  "eventually_constant (\<lambda>i. iterate i\<cdot>f\<cdot>x)"
   2.213 +unfolding eventually_constant_def MOST_nat_le
   2.214 +proof -
   2.215 +  let ?Y = "\<lambda>i. iterate i\<cdot>f\<cdot>x"
   2.216 +  have "\<exists>j. \<forall>k. ?Y j \<sqsubseteq> ?Y k"
   2.217 +    apply (rule finite_range_has_max)
   2.218 +    apply (erule antichain_iterate_app)
   2.219 +    apply (rule finite_range_iterate_app)
   2.220 +    done
   2.221 +  then obtain j where j: "\<And>k. ?Y j \<sqsubseteq> ?Y k" by fast
   2.222 +  show "\<exists>z m. \<forall>n\<ge>m. ?Y n = z"
   2.223 +  proof (intro exI allI impI)
   2.224 +    fix k
   2.225 +    assume "j \<le> k"
   2.226 +    hence "?Y k \<sqsubseteq> ?Y j" by (rule antichain_iterate_app)
   2.227 +    also have "?Y j \<sqsubseteq> ?Y k" by (rule j)
   2.228 +    finally show "?Y k = ?Y j" .
   2.229 +  qed
   2.230 +qed
   2.231 +
   2.232 +lemma eventually_constant_iterate:
   2.233 +  "eventually_constant (\<lambda>n. iterate n\<cdot>f)"
   2.234 +proof -
   2.235 +  have "\<forall>y\<in>range (\<lambda>x. f\<cdot>x). eventually_constant (\<lambda>i. iterate i\<cdot>f\<cdot>y)"
   2.236 +    by (simp add: eventually_constant_iterate_app)
   2.237 +  hence "\<forall>y\<in>range (\<lambda>x. f\<cdot>x). MOST i. MOST j. iterate j\<cdot>f\<cdot>y = iterate i\<cdot>f\<cdot>y"
   2.238 +    unfolding eventually_constant_MOST_MOST .
   2.239 +  hence "MOST i. MOST j. \<forall>y\<in>range (\<lambda>x. f\<cdot>x). iterate j\<cdot>f\<cdot>y = iterate i\<cdot>f\<cdot>y"
   2.240 +    by (simp only: MOST_finite_Ball_distrib [OF finite_range])
   2.241 +  hence "MOST i. MOST j. \<forall>x. iterate j\<cdot>f\<cdot>(f\<cdot>x) = iterate i\<cdot>f\<cdot>(f\<cdot>x)"
   2.242 +    by simp
   2.243 +  hence "MOST i. MOST j. \<forall>x. iterate (Suc j)\<cdot>f\<cdot>x = iterate (Suc i)\<cdot>f\<cdot>x"
   2.244 +    by (simp only: iterate_Suc2)
   2.245 +  hence "MOST i. MOST j. iterate (Suc j)\<cdot>f = iterate (Suc i)\<cdot>f"
   2.246 +    by (simp only: expand_cfun_eq)
   2.247 +  hence "eventually_constant (\<lambda>i. iterate (Suc i)\<cdot>f)"
   2.248 +    unfolding eventually_constant_MOST_MOST .
   2.249 +  thus "eventually_constant (\<lambda>i. iterate i\<cdot>f)"
   2.250 +    by (rule eventually_constant_SucD)
   2.251 +qed
   2.252 +
   2.253 +abbreviation
   2.254 +  d :: "'a \<rightarrow> 'a"
   2.255 +where
   2.256 +  "d \<equiv> eventual_iterate f"
   2.257 +
   2.258 +lemma MOST_d: "MOST n. P (iterate n\<cdot>f) \<Longrightarrow> P d"
   2.259 +unfolding eventual_iterate_def
   2.260 +using eventually_constant_iterate by (rule MOST_eventual)
   2.261 +
   2.262 +lemma f_d: "f\<cdot>(d\<cdot>x) = d\<cdot>x"
   2.263 +apply (rule MOST_d)
   2.264 +apply (subst iterate_Suc [symmetric])
   2.265 +apply (rule eventually_constant_MOST_Suc_eq)
   2.266 +apply (rule eventually_constant_iterate_app)
   2.267 +done
   2.268 +
   2.269 +lemma d_fixed_iff: "d\<cdot>x = x \<longleftrightarrow> f\<cdot>x = x"
   2.270 +proof
   2.271 +  assume "d\<cdot>x = x"
   2.272 +  with f_d [where x=x]
   2.273 +  show "f\<cdot>x = x" by simp
   2.274 +next
   2.275 +  assume f: "f\<cdot>x = x"
   2.276 +  have "\<forall>n. iterate n\<cdot>f\<cdot>x = x"
   2.277 +    by (rule allI, rule nat.induct, simp, simp add: f)
   2.278 +  hence "MOST n. iterate n\<cdot>f\<cdot>x = x"
   2.279 +    by (rule ALL_MOST)
   2.280 +  thus "d\<cdot>x = x"
   2.281 +    by (rule MOST_d)
   2.282 +qed
   2.283 +
   2.284 +lemma finite_deflation_d: "finite_deflation d"
   2.285 +proof
   2.286 +  fix x :: 'a
   2.287 +  have "d \<in> range (\<lambda>n. iterate n\<cdot>f)"
   2.288 +    unfolding eventual_iterate_def
   2.289 +    using eventually_constant_iterate
   2.290 +    by (rule eventual_mem_range)
   2.291 +  then obtain n where n: "d = iterate n\<cdot>f" ..
   2.292 +  have "iterate n\<cdot>f\<cdot>(d\<cdot>x) = d\<cdot>x"
   2.293 +    using f_d by (rule iterate_fixed)
   2.294 +  thus "d\<cdot>(d\<cdot>x) = d\<cdot>x"
   2.295 +    by (simp add: n)
   2.296 +next
   2.297 +  fix x :: 'a
   2.298 +  show "d\<cdot>x \<sqsubseteq> x"
   2.299 +    by (rule MOST_d, simp add: iterate_below)
   2.300 +next
   2.301 +  from finite_range
   2.302 +  have "finite {x. f\<cdot>x = x}"
   2.303 +    by (rule finite_range_imp_finite_fixes)
   2.304 +  thus "finite {x. d\<cdot>x = x}"
   2.305 +    by (simp add: d_fixed_iff)
   2.306 +qed
   2.307 +
   2.308 +lemma deflation_d: "deflation d"
   2.309 +using finite_deflation_d
   2.310 +by (rule finite_deflation_imp_deflation)
   2.311 +
   2.312 +end
   2.313 +
   2.314 +lemma finite_deflation_eventual_iterate:
   2.315 +  "pre_deflation d \<Longrightarrow> finite_deflation (eventual_iterate d)"
   2.316 +by (rule pre_deflation.finite_deflation_d)
   2.317 +
   2.318 +lemma pre_deflation_oo:
   2.319 +  assumes "finite_deflation d"
   2.320 +  assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
   2.321 +  shows "pre_deflation (d oo f)"
   2.322 +proof
   2.323 +  interpret d: finite_deflation d by fact
   2.324 +  fix x
   2.325 +  show "\<And>x. (d oo f)\<cdot>x \<sqsubseteq> x"
   2.326 +    by (simp, rule below_trans [OF d.below f])
   2.327 +  show "finite (range (\<lambda>x. (d oo f)\<cdot>x))"
   2.328 +    by (rule finite_subset [OF _ d.finite_range], auto)
   2.329 +qed
   2.330 +
   2.331 +lemma eventual_iterate_oo_fixed_iff:
   2.332 +  assumes "finite_deflation d"
   2.333 +  assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
   2.334 +  shows "eventual_iterate (d oo f)\<cdot>x = x \<longleftrightarrow> d\<cdot>x = x \<and> f\<cdot>x = x"
   2.335 +proof -
   2.336 +  interpret d: finite_deflation d by fact
   2.337 +  let ?e = "d oo f"
   2.338 +  interpret e: pre_deflation "d oo f"
   2.339 +    using `finite_deflation d` f
   2.340 +    by (rule pre_deflation_oo)
   2.341 +  let ?g = "eventual (\<lambda>n. iterate n\<cdot>?e)"
   2.342 +  show ?thesis
   2.343 +    apply (subst e.d_fixed_iff)
   2.344 +    apply simp
   2.345 +    apply safe
   2.346 +    apply (erule subst)
   2.347 +    apply (rule d.idem)
   2.348 +    apply (rule below_antisym)
   2.349 +    apply (rule f)
   2.350 +    apply (erule subst, rule d.below)
   2.351 +    apply simp
   2.352 +    done
   2.353 +qed
   2.354 +
   2.355 +lemma eventual_mono:
   2.356 +  assumes A: "eventually_constant A"
   2.357 +  assumes B: "eventually_constant B"
   2.358 +  assumes below: "\<And>n. A n \<sqsubseteq> B n"
   2.359 +  shows "eventual A \<sqsubseteq> eventual B"
   2.360 +proof -
   2.361 +  from A have "MOST n. A n = eventual A"
   2.362 +    by (rule MOST_eq_eventual)
   2.363 +  then have "MOST n. eventual A \<sqsubseteq> B n"
   2.364 +    by (rule MOST_mono) (erule subst, rule below)
   2.365 +  with B show "eventual A \<sqsubseteq> eventual B"
   2.366 +    by (rule MOST_eventual)
   2.367 +qed
   2.368 +
   2.369 +lemma eventual_iterate_mono:
   2.370 +  assumes f: "pre_deflation f" and g: "pre_deflation g" and "f \<sqsubseteq> g"
   2.371 +  shows "eventual_iterate f \<sqsubseteq> eventual_iterate g"
   2.372 +unfolding eventual_iterate_def
   2.373 +apply (rule eventual_mono)
   2.374 +apply (rule pre_deflation.eventually_constant_iterate [OF f])
   2.375 +apply (rule pre_deflation.eventually_constant_iterate [OF g])
   2.376 +apply (rule monofun_cfun_arg [OF `f \<sqsubseteq> g`])
   2.377 +done
   2.378 +
   2.379 +lemma cont2cont_eventual_iterate_oo:
   2.380 +  assumes d: "finite_deflation d"
   2.381 +  assumes cont: "cont f" and below: "\<And>x y. f x\<cdot>y \<sqsubseteq> y"
   2.382 +  shows "cont (\<lambda>x. eventual_iterate (d oo f x))"
   2.383 +    (is "cont ?e")
   2.384 +proof (rule contI2)
   2.385 +  show "monofun ?e"
   2.386 +    apply (rule monofunI)
   2.387 +    apply (rule eventual_iterate_mono)
   2.388 +    apply (rule pre_deflation_oo [OF d below])
   2.389 +    apply (rule pre_deflation_oo [OF d below])
   2.390 +    apply (rule monofun_cfun_arg)
   2.391 +    apply (erule cont2monofunE [OF cont])
   2.392 +    done
   2.393 +next
   2.394 +  fix Y :: "nat \<Rightarrow> 'b"
   2.395 +  assume Y: "chain Y"
   2.396 +  with cont have fY: "chain (\<lambda>i. f (Y i))"
   2.397 +    by (rule ch2ch_cont)
   2.398 +  assume eY: "chain (\<lambda>i. ?e (Y i))"
   2.399 +  have lub_below: "\<And>x. f (\<Squnion>i. Y i)\<cdot>x \<sqsubseteq> x"
   2.400 +    by (rule admD [OF _ Y], simp add: cont, rule below)
   2.401 +  have "deflation (?e (\<Squnion>i. Y i))"
   2.402 +    apply (rule pre_deflation.deflation_d)
   2.403 +    apply (rule pre_deflation_oo [OF d lub_below])
   2.404 +    done
   2.405 +  then show "?e (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. ?e (Y i))"
   2.406 +  proof (rule deflation.belowI)
   2.407 +    fix x :: 'a
   2.408 +    assume "?e (\<Squnion>i. Y i)\<cdot>x = x"
   2.409 +    hence "d\<cdot>x = x" and "f (\<Squnion>i. Y i)\<cdot>x = x"
   2.410 +      by (simp_all add: eventual_iterate_oo_fixed_iff [OF d lub_below])
   2.411 +    hence "(\<Squnion>i. f (Y i)\<cdot>x) = x"
   2.412 +      apply (simp only: cont2contlubE [OF cont Y])
   2.413 +      apply (simp only: contlub_cfun_fun [OF fY])
   2.414 +      done
   2.415 +    have "compact (d\<cdot>x)"
   2.416 +      using d by (rule finite_deflation.compact)
   2.417 +    then have "compact x"
   2.418 +      using `d\<cdot>x = x` by simp
   2.419 +    then have "compact (\<Squnion>i. f (Y i)\<cdot>x)"
   2.420 +      using `(\<Squnion>i. f (Y i)\<cdot>x) = x` by simp
   2.421 +    then have "\<exists>n. max_in_chain n (\<lambda>i. f (Y i)\<cdot>x)"
   2.422 +      by - (rule compact_imp_max_in_chain, simp add: fY, assumption)
   2.423 +    then obtain n where n: "max_in_chain n (\<lambda>i. f (Y i)\<cdot>x)" ..
   2.424 +    then have "f (Y n)\<cdot>x = x"
   2.425 +      using `(\<Squnion>i. f (Y i)\<cdot>x) = x` fY by (simp add: maxinch_is_thelub)
   2.426 +    with `d\<cdot>x = x` have "?e (Y n)\<cdot>x = x"
   2.427 +      by (simp add: eventual_iterate_oo_fixed_iff [OF d below])
   2.428 +    moreover have "?e (Y n)\<cdot>x \<sqsubseteq> (\<Squnion>i. ?e (Y i)\<cdot>x)"
   2.429 +      by (rule is_ub_thelub, simp add: eY)
   2.430 +    ultimately have "x \<sqsubseteq> (\<Squnion>i. ?e (Y i))\<cdot>x"
   2.431 +      by (simp add: contlub_cfun_fun eY)
   2.432 +    also have "(\<Squnion>i. ?e (Y i))\<cdot>x \<sqsubseteq> x"
   2.433 +      apply (rule deflation.below)
   2.434 +      apply (rule admD [OF adm_deflation eY])
   2.435 +      apply (rule pre_deflation.deflation_d)
   2.436 +      apply (rule pre_deflation_oo [OF d below])
   2.437 +      done
   2.438 +    finally show "(\<Squnion>i. ?e (Y i))\<cdot>x = x" ..
   2.439 +  qed
   2.440 +qed
   2.441 +
   2.442 +subsection {* Take function for finite deflations *}
   2.443 +
   2.444 +definition
   2.445 +  defl_take :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<Rightarrow> (udom \<rightarrow> udom)"
   2.446 +where
   2.447 +  "defl_take i d = eventual_iterate (udom_approx i oo d)"
   2.448 +
   2.449 +lemma finite_deflation_defl_take:
   2.450 +  "deflation d \<Longrightarrow> finite_deflation (defl_take i d)"
   2.451 +unfolding defl_take_def
   2.452 +apply (rule pre_deflation.finite_deflation_d)
   2.453 +apply (rule pre_deflation_oo)
   2.454 +apply (rule finite_deflation_udom_approx)
   2.455 +apply (erule deflation.below)
   2.456 +done
   2.457 +
   2.458 +lemma deflation_defl_take:
   2.459 +  "deflation d \<Longrightarrow> deflation (defl_take i d)"
   2.460 +apply (rule finite_deflation_imp_deflation)
   2.461 +apply (erule finite_deflation_defl_take)
   2.462 +done
   2.463 +
   2.464 +lemma defl_take_fixed_iff:
   2.465 +  "deflation d \<Longrightarrow> defl_take i d\<cdot>x = x \<longleftrightarrow> udom_approx i\<cdot>x = x \<and> d\<cdot>x = x"
   2.466 +unfolding defl_take_def
   2.467 +apply (rule eventual_iterate_oo_fixed_iff)
   2.468 +apply (rule finite_deflation_udom_approx)
   2.469 +apply (erule deflation.below)
   2.470 +done
   2.471 +
   2.472 +lemma defl_take_below:
   2.473 +  "\<lbrakk>a \<sqsubseteq> b; deflation a; deflation b\<rbrakk> \<Longrightarrow> defl_take i a \<sqsubseteq> defl_take i b"
   2.474 +apply (rule deflation.belowI)
   2.475 +apply (erule deflation_defl_take)
   2.476 +apply (simp add: defl_take_fixed_iff)
   2.477 +apply (erule (1) deflation.belowD)
   2.478 +apply (erule conjunct2)
   2.479 +done
   2.480 +
   2.481 +lemma cont2cont_defl_take:
   2.482 +  assumes cont: "cont f" and below: "\<And>x y. f x\<cdot>y \<sqsubseteq> y"
   2.483 +  shows "cont (\<lambda>x. defl_take i (f x))"
   2.484 +unfolding defl_take_def
   2.485 +using finite_deflation_udom_approx assms
   2.486 +by (rule cont2cont_eventual_iterate_oo)
   2.487 +
   2.488 +definition
   2.489 +  fd_take :: "nat \<Rightarrow> fin_defl \<Rightarrow> fin_defl"
   2.490 +where
   2.491 +  "fd_take i d = Abs_fin_defl (defl_take i (Rep_fin_defl d))"
   2.492 +
   2.493 +lemma Rep_fin_defl_fd_take:
   2.494 +  "Rep_fin_defl (fd_take i d) = defl_take i (Rep_fin_defl d)"
   2.495 +unfolding fd_take_def
   2.496 +apply (rule Abs_fin_defl_inverse [unfolded mem_Collect_eq])
   2.497 +apply (rule finite_deflation_defl_take)
   2.498 +apply (rule deflation_Rep_fin_defl)
   2.499 +done
   2.500 +
   2.501 +lemma fd_take_fixed_iff:
   2.502 +  "Rep_fin_defl (fd_take i d)\<cdot>x = x \<longleftrightarrow>
   2.503 +    udom_approx i\<cdot>x = x \<and> Rep_fin_defl d\<cdot>x = x"
   2.504 +unfolding Rep_fin_defl_fd_take
   2.505 +apply (rule defl_take_fixed_iff)
   2.506 +apply (rule deflation_Rep_fin_defl)
   2.507 +done
   2.508 +
   2.509 +lemma fd_take_below: "fd_take n d \<sqsubseteq> d"
   2.510 +apply (rule fin_defl_belowI)
   2.511 +apply (simp add: fd_take_fixed_iff)
   2.512 +done
   2.513 +
   2.514 +lemma fd_take_idem: "fd_take n (fd_take n d) = fd_take n d"
   2.515 +apply (rule fin_defl_eqI)
   2.516 +apply (simp add: fd_take_fixed_iff)
   2.517 +done
   2.518 +
   2.519 +lemma fd_take_mono: "a \<sqsubseteq> b \<Longrightarrow> fd_take n a \<sqsubseteq> fd_take n b"
   2.520 +apply (rule fin_defl_belowI)
   2.521 +apply (simp add: fd_take_fixed_iff)
   2.522 +apply (simp add: fin_defl_belowD)
   2.523 +done
   2.524 +
   2.525 +lemma approx_fixed_le_lemma: "\<lbrakk>i \<le> j; udom_approx i\<cdot>x = x\<rbrakk> \<Longrightarrow> udom_approx j\<cdot>x = x"
   2.526 +apply (rule deflation.belowD)
   2.527 +apply (rule finite_deflation_imp_deflation)
   2.528 +apply (rule finite_deflation_udom_approx)
   2.529 +apply (erule chain_mono [OF chain_udom_approx])
   2.530 +apply assumption
   2.531 +done
   2.532 +
   2.533 +lemma fd_take_chain: "m \<le> n \<Longrightarrow> fd_take m a \<sqsubseteq> fd_take n a"
   2.534 +apply (rule fin_defl_belowI)
   2.535 +apply (simp add: fd_take_fixed_iff)
   2.536 +apply (simp add: approx_fixed_le_lemma)
   2.537 +done
   2.538 +
   2.539 +lemma finite_range_fd_take: "finite (range (fd_take n))"
   2.540 +apply (rule finite_imageD [where f="\<lambda>a. {x. Rep_fin_defl a\<cdot>x = x}"])
   2.541 +apply (rule finite_subset [where B="Pow {x. udom_approx n\<cdot>x = x}"])
   2.542 +apply (clarify, simp add: fd_take_fixed_iff)
   2.543 +apply (simp add: finite_deflation.finite_fixes [OF finite_deflation_udom_approx])
   2.544 +apply (rule inj_onI, clarify)
   2.545 +apply (simp add: set_eq_iff fin_defl_eqI)
   2.546 +done
   2.547 +
   2.548 +lemma fd_take_covers: "\<exists>n. fd_take n a = a"
   2.549 +apply (rule_tac x=
   2.550 +  "Max ((\<lambda>x. LEAST n. udom_approx n\<cdot>x = x) ` {x. Rep_fin_defl a\<cdot>x = x})" in exI)
   2.551 +apply (rule below_antisym)
   2.552 +apply (rule fd_take_below)
   2.553 +apply (rule fin_defl_belowI)
   2.554 +apply (simp add: fd_take_fixed_iff)
   2.555 +apply (rule approx_fixed_le_lemma)
   2.556 +apply (rule Max_ge)
   2.557 +apply (rule finite_imageI)
   2.558 +apply (rule Rep_fin_defl.finite_fixes)
   2.559 +apply (rule imageI)
   2.560 +apply (erule CollectI)
   2.561 +apply (rule LeastI_ex)
   2.562 +apply (rule approx_chain.compact_eq_approx [OF udom_approx])
   2.563 +apply (erule subst)
   2.564 +apply (rule Rep_fin_defl.compact)
   2.565 +done
   2.566 +
   2.567 +subsection {* Chain of approx functions on algebraic deflations *}
   2.568 +
   2.569 +definition
   2.570 +  defl_approx :: "nat \<Rightarrow> defl \<rightarrow> defl"
   2.571 +where
   2.572 +  "defl_approx = (\<lambda>i. defl.basis_fun (\<lambda>d. defl_principal (fd_take i d)))"
   2.573 +
   2.574 +lemma defl_approx_principal:
   2.575 +  "defl_approx i\<cdot>(defl_principal d) = defl_principal (fd_take i d)"
   2.576 +unfolding defl_approx_def
   2.577 +by (simp add: defl.basis_fun_principal fd_take_mono)
   2.578 +
   2.579 +lemma defl_approx: "approx_chain defl_approx"
   2.580 +proof
   2.581 +  show chain: "chain defl_approx"
   2.582 +    unfolding defl_approx_def
   2.583 +    by (simp add: chainI defl.basis_fun_mono fd_take_mono fd_take_chain)
   2.584 +  show idem: "\<And>i x. defl_approx i\<cdot>(defl_approx i\<cdot>x) = defl_approx i\<cdot>x"
   2.585 +    apply (induct_tac x rule: defl.principal_induct, simp)
   2.586 +    apply (simp add: defl_approx_principal fd_take_idem)
   2.587 +    done
   2.588 +  show below: "\<And>i x. defl_approx i\<cdot>x \<sqsubseteq> x"
   2.589 +    apply (induct_tac x rule: defl.principal_induct, simp)
   2.590 +    apply (simp add: defl_approx_principal fd_take_below)
   2.591 +    done
   2.592 +  show lub: "(\<Squnion>i. defl_approx i) = ID"
   2.593 +    apply (rule ext_cfun, rule below_antisym)
   2.594 +    apply (simp add: contlub_cfun_fun chain lub_below_iff chain below)
   2.595 +    apply (induct_tac x rule: defl.principal_induct, simp)
   2.596 +    apply (simp add: contlub_cfun_fun chain)
   2.597 +    apply (simp add: compact_below_lub_iff defl.compact_principal chain)
   2.598 +    apply (simp add: defl_approx_principal)
   2.599 +    apply (subgoal_tac "\<exists>i. fd_take i a = a", metis below_refl)
   2.600 +    apply (rule fd_take_covers)
   2.601 +    done
   2.602 +  show "\<And>i. finite {x. defl_approx i\<cdot>x = x}"
   2.603 +    apply (rule finite_range_imp_finite_fixes)
   2.604 +    apply (rule_tac B="defl_principal ` range (fd_take i)" in rev_finite_subset)
   2.605 +    apply (simp add: finite_range_fd_take)
   2.606 +    apply (clarsimp, rename_tac x)
   2.607 +    apply (induct_tac x rule: defl.principal_induct)
   2.608 +    apply (simp add: adm_mem_finite finite_range_fd_take)
   2.609 +    apply (simp add: defl_approx_principal)
   2.610 +    done
   2.611 +qed
   2.612 +
   2.613 +subsection {* Algebraic deflations are a bifinite domain *}
   2.614 +
   2.615 +instantiation defl :: bifinite
   2.616 +begin
   2.617 +
   2.618 +definition
   2.619 +  "emb = udom_emb defl_approx"
   2.620 +
   2.621 +definition
   2.622 +  "prj = udom_prj defl_approx"
   2.623 +
   2.624 +definition
   2.625 +  "defl (t::defl itself) =
   2.626 +    (\<Squnion>i. defl_principal (Abs_fin_defl (emb oo defl_approx i oo prj)))"
   2.627 +
   2.628 +instance proof
   2.629 +  show ep: "ep_pair emb (prj :: udom \<rightarrow> defl)"
   2.630 +    unfolding emb_defl_def prj_defl_def
   2.631 +    by (rule ep_pair_udom [OF defl_approx])
   2.632 +  show "cast\<cdot>DEFL(defl) = emb oo (prj :: udom \<rightarrow> defl)"
   2.633 +    unfolding defl_defl_def
   2.634 +    apply (subst contlub_cfun_arg)
   2.635 +    apply (rule chainI)
   2.636 +    apply (rule defl.principal_mono)
   2.637 +    apply (simp add: below_fin_defl_def)
   2.638 +    apply (simp add: Abs_fin_defl_inverse approx_chain.finite_deflation_approx [OF defl_approx]
   2.639 +                     ep_pair.finite_deflation_e_d_p [OF ep])
   2.640 +    apply (intro monofun_cfun below_refl)
   2.641 +    apply (rule chainE)
   2.642 +    apply (rule approx_chain.chain_approx [OF defl_approx])
   2.643 +    apply (subst cast_defl_principal)
   2.644 +    apply (simp add: Abs_fin_defl_inverse approx_chain.finite_deflation_approx [OF defl_approx]
   2.645 +                     ep_pair.finite_deflation_e_d_p [OF ep])
   2.646 +    apply (simp add: lub_distribs approx_chain.chain_approx [OF defl_approx]
   2.647 +                     approx_chain.lub_approx [OF defl_approx])
   2.648 +    done
   2.649 +qed
   2.650 +
   2.651 +end
   2.652 +
   2.653 +end
     3.1 --- a/src/HOLCF/Library/HOLCF_Library.thy	Mon Oct 11 08:32:09 2010 -0700
     3.2 +++ b/src/HOLCF/Library/HOLCF_Library.thy	Mon Oct 11 09:54:04 2010 -0700
     3.3 @@ -1,5 +1,6 @@
     3.4  theory HOLCF_Library
     3.5  imports
     3.6 +  Defl_Bifinite
     3.7    List_Cpo
     3.8    Stream
     3.9    Strict_Fun