src/HOLCF/Library/Defl_Bifinite.thy
author huffman
Tue Nov 09 16:37:13 2010 -0800 (2010-11-09)
changeset 40491 6de5839e2fb3
parent 40002 c5b5f7a3a3b1
child 40494 db8a09daba7b
permissions -rw-r--r--
add 'predomain' class: unpointed version of bifinite
     1 (*  Title:      HOLCF/Library/Defl_Bifinite.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 header {* Algebraic deflations are a bifinite domain *}
     6 
     7 theory Defl_Bifinite
     8 imports HOLCF Infinite_Set
     9 begin
    10 
    11 subsection {* Lemmas about MOST *}
    12 
    13 default_sort type
    14 
    15 lemma MOST_INFM:
    16   assumes inf: "infinite (UNIV::'a set)"
    17   shows "MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x"
    18   unfolding Alm_all_def Inf_many_def
    19   apply (auto simp add: Collect_neg_eq)
    20   apply (drule (1) finite_UnI)
    21   apply (simp add: Compl_partition2 inf)
    22   done
    23 
    24 lemma MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
    25 by (rule MOST_inj [OF _ inj_Suc])
    26 
    27 lemma MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
    28 unfolding MOST_nat
    29 apply (clarify, rule_tac x="Suc m" in exI, clarify)
    30 apply (erule Suc_lessE, simp)
    31 done
    32 
    33 lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
    34 by (rule iffI [OF MOST_SucD MOST_SucI])
    35 
    36 lemma INFM_finite_Bex_distrib:
    37   "finite A \<Longrightarrow> (INFM y. \<exists>x\<in>A. P x y) \<longleftrightarrow> (\<exists>x\<in>A. INFM y. P x y)"
    38 by (induct set: finite, simp, simp add: INFM_disj_distrib)
    39 
    40 lemma MOST_finite_Ball_distrib:
    41   "finite A \<Longrightarrow> (MOST y. \<forall>x\<in>A. P x y) \<longleftrightarrow> (\<forall>x\<in>A. MOST y. P x y)"
    42 by (induct set: finite, simp, simp add: MOST_conj_distrib)
    43 
    44 lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
    45 unfolding MOST_nat_le by fast
    46 
    47 subsection {* Eventually constant sequences *}
    48 
    49 definition
    50   eventually_constant :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool"
    51 where
    52   "eventually_constant S = (\<exists>x. MOST i. S i = x)"
    53 
    54 lemma eventually_constant_MOST_MOST:
    55   "eventually_constant S \<longleftrightarrow> (MOST m. MOST n. S n = S m)"
    56 unfolding eventually_constant_def MOST_nat
    57 apply safe
    58 apply (rule_tac x=m in exI, clarify)
    59 apply (rule_tac x=m in exI, clarify)
    60 apply simp
    61 apply fast
    62 done
    63 
    64 lemma eventually_constantI: "MOST i. S i = x \<Longrightarrow> eventually_constant S"
    65 unfolding eventually_constant_def by fast
    66 
    67 lemma eventually_constant_comp:
    68   "eventually_constant (\<lambda>i. S i) \<Longrightarrow> eventually_constant (\<lambda>i. f (S i))"
    69 unfolding eventually_constant_def
    70 apply (erule exE, rule_tac x="f x" in exI)
    71 apply (erule MOST_mono, simp)
    72 done
    73 
    74 lemma eventually_constant_Suc_iff:
    75   "eventually_constant (\<lambda>i. S (Suc i)) \<longleftrightarrow> eventually_constant (\<lambda>i. S i)"
    76 unfolding eventually_constant_def
    77 by (subst MOST_Suc_iff, rule refl)
    78 
    79 lemma eventually_constant_SucD:
    80   "eventually_constant (\<lambda>i. S (Suc i)) \<Longrightarrow> eventually_constant (\<lambda>i. S i)"
    81 by (rule eventually_constant_Suc_iff [THEN iffD1])
    82 
    83 subsection {* Limits of eventually constant sequences *}
    84 
    85 definition
    86   eventual :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a" where
    87   "eventual S = (THE x. MOST i. S i = x)"
    88 
    89 lemma eventual_eqI: "MOST i. S i = x \<Longrightarrow> eventual S = x"
    90 unfolding eventual_def
    91 apply (rule the_equality, assumption)
    92 apply (rename_tac y)
    93 apply (subgoal_tac "MOST i::nat. y = x", simp)
    94 apply (erule MOST_rev_mp)
    95 apply (erule MOST_rev_mp)
    96 apply simp
    97 done
    98 
    99 lemma MOST_eq_eventual:
   100   "eventually_constant S \<Longrightarrow> MOST i. S i = eventual S"
   101 unfolding eventually_constant_def
   102 by (erule exE, simp add: eventual_eqI)
   103 
   104 lemma eventual_mem_range:
   105   "eventually_constant S \<Longrightarrow> eventual S \<in> range S"
   106 apply (drule MOST_eq_eventual)
   107 apply (simp only: MOST_nat_le, clarify)
   108 apply (drule spec, drule mp, rule order_refl)
   109 apply (erule range_eqI [OF sym])
   110 done
   111 
   112 lemma eventually_constant_MOST_iff:
   113   assumes S: "eventually_constant S"
   114   shows "(MOST n. P (S n)) \<longleftrightarrow> P (eventual S)"
   115 apply (subgoal_tac "(MOST n. P (S n)) \<longleftrightarrow> (MOST n::nat. P (eventual S))")
   116 apply simp
   117 apply (rule iffI)
   118 apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]])
   119 apply (erule MOST_mono, force)
   120 apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]])
   121 apply (erule MOST_mono, simp)
   122 done
   123 
   124 lemma MOST_eventual:
   125   "\<lbrakk>eventually_constant S; MOST n. P (S n)\<rbrakk> \<Longrightarrow> P (eventual S)"
   126 proof -
   127   assume "eventually_constant S"
   128   hence "MOST n. S n = eventual S"
   129     by (rule MOST_eq_eventual)
   130   moreover assume "MOST n. P (S n)"
   131   ultimately have "MOST n. S n = eventual S \<and> P (S n)"
   132     by (rule MOST_conj_distrib [THEN iffD2, OF conjI])
   133   hence "MOST n::nat. P (eventual S)"
   134     by (rule MOST_mono) auto
   135   thus ?thesis by simp
   136 qed
   137 
   138 lemma eventually_constant_MOST_Suc_eq:
   139   "eventually_constant S \<Longrightarrow> MOST n. S (Suc n) = S n"
   140 apply (drule MOST_eq_eventual)
   141 apply (frule MOST_Suc_iff [THEN iffD2])
   142 apply (erule MOST_rev_mp)
   143 apply (erule MOST_rev_mp)
   144 apply simp
   145 done
   146 
   147 lemma eventual_comp:
   148   "eventually_constant S \<Longrightarrow> eventual (\<lambda>i. f (S i)) = f (eventual (\<lambda>i. S i))"
   149 apply (rule eventual_eqI)
   150 apply (rule MOST_mono)
   151 apply (erule MOST_eq_eventual)
   152 apply simp
   153 done
   154 
   155 subsection {* Constructing finite deflations by iteration *}
   156 
   157 default_sort cpo
   158 
   159 lemma le_Suc_induct:
   160   assumes le: "i \<le> j"
   161   assumes step: "\<And>i. P i (Suc i)"
   162   assumes refl: "\<And>i. P i i"
   163   assumes trans: "\<And>i j k. \<lbrakk>P i j; P j k\<rbrakk> \<Longrightarrow> P i k"
   164   shows "P i j"
   165 proof (cases "i = j")
   166   assume "i = j"
   167   thus "P i j" by (simp add: refl)
   168 next
   169   assume "i \<noteq> j"
   170   with le have "i < j" by simp
   171   thus "P i j" using step trans by (rule less_Suc_induct)
   172 qed
   173 
   174 definition
   175   eventual_iterate :: "('a \<rightarrow> 'a::cpo) \<Rightarrow> ('a \<rightarrow> 'a)"
   176 where
   177   "eventual_iterate f = eventual (\<lambda>n. iterate n\<cdot>f)"
   178 
   179 text {* A pre-deflation is like a deflation, but not idempotent. *}
   180 
   181 locale pre_deflation =
   182   fixes f :: "'a \<rightarrow> 'a::cpo"
   183   assumes below: "\<And>x. f\<cdot>x \<sqsubseteq> x"
   184   assumes finite_range: "finite (range (\<lambda>x. f\<cdot>x))"
   185 begin
   186 
   187 lemma iterate_below: "iterate i\<cdot>f\<cdot>x \<sqsubseteq> x"
   188 by (induct i, simp_all add: below_trans [OF below])
   189 
   190 lemma iterate_fixed: "f\<cdot>x = x \<Longrightarrow> iterate i\<cdot>f\<cdot>x = x"
   191 by (induct i, simp_all)
   192 
   193 lemma antichain_iterate_app: "i \<le> j \<Longrightarrow> iterate j\<cdot>f\<cdot>x \<sqsubseteq> iterate i\<cdot>f\<cdot>x"
   194 apply (erule le_Suc_induct)
   195 apply (simp add: below)
   196 apply (rule below_refl)
   197 apply (erule (1) below_trans)
   198 done
   199 
   200 lemma finite_range_iterate_app: "finite (range (\<lambda>i. iterate i\<cdot>f\<cdot>x))"
   201 proof (rule finite_subset)
   202   show "range (\<lambda>i. iterate i\<cdot>f\<cdot>x) \<subseteq> insert x (range (\<lambda>x. f\<cdot>x))"
   203     by (clarify, case_tac i, simp_all)
   204   show "finite (insert x (range (\<lambda>x. f\<cdot>x)))"
   205     by (simp add: finite_range)
   206 qed
   207 
   208 lemma eventually_constant_iterate_app:
   209   "eventually_constant (\<lambda>i. iterate i\<cdot>f\<cdot>x)"
   210 unfolding eventually_constant_def MOST_nat_le
   211 proof -
   212   let ?Y = "\<lambda>i. iterate i\<cdot>f\<cdot>x"
   213   have "\<exists>j. \<forall>k. ?Y j \<sqsubseteq> ?Y k"
   214     apply (rule finite_range_has_max)
   215     apply (erule antichain_iterate_app)
   216     apply (rule finite_range_iterate_app)
   217     done
   218   then obtain j where j: "\<And>k. ?Y j \<sqsubseteq> ?Y k" by fast
   219   show "\<exists>z m. \<forall>n\<ge>m. ?Y n = z"
   220   proof (intro exI allI impI)
   221     fix k
   222     assume "j \<le> k"
   223     hence "?Y k \<sqsubseteq> ?Y j" by (rule antichain_iterate_app)
   224     also have "?Y j \<sqsubseteq> ?Y k" by (rule j)
   225     finally show "?Y k = ?Y j" .
   226   qed
   227 qed
   228 
   229 lemma eventually_constant_iterate:
   230   "eventually_constant (\<lambda>n. iterate n\<cdot>f)"
   231 proof -
   232   have "\<forall>y\<in>range (\<lambda>x. f\<cdot>x). eventually_constant (\<lambda>i. iterate i\<cdot>f\<cdot>y)"
   233     by (simp add: eventually_constant_iterate_app)
   234   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"
   235     unfolding eventually_constant_MOST_MOST .
   236   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"
   237     by (simp only: MOST_finite_Ball_distrib [OF finite_range])
   238   hence "MOST i. MOST j. \<forall>x. iterate j\<cdot>f\<cdot>(f\<cdot>x) = iterate i\<cdot>f\<cdot>(f\<cdot>x)"
   239     by simp
   240   hence "MOST i. MOST j. \<forall>x. iterate (Suc j)\<cdot>f\<cdot>x = iterate (Suc i)\<cdot>f\<cdot>x"
   241     by (simp only: iterate_Suc2)
   242   hence "MOST i. MOST j. iterate (Suc j)\<cdot>f = iterate (Suc i)\<cdot>f"
   243     by (simp only: cfun_eq_iff)
   244   hence "eventually_constant (\<lambda>i. iterate (Suc i)\<cdot>f)"
   245     unfolding eventually_constant_MOST_MOST .
   246   thus "eventually_constant (\<lambda>i. iterate i\<cdot>f)"
   247     by (rule eventually_constant_SucD)
   248 qed
   249 
   250 abbreviation
   251   d :: "'a \<rightarrow> 'a"
   252 where
   253   "d \<equiv> eventual_iterate f"
   254 
   255 lemma MOST_d: "MOST n. P (iterate n\<cdot>f) \<Longrightarrow> P d"
   256 unfolding eventual_iterate_def
   257 using eventually_constant_iterate by (rule MOST_eventual)
   258 
   259 lemma f_d: "f\<cdot>(d\<cdot>x) = d\<cdot>x"
   260 apply (rule MOST_d)
   261 apply (subst iterate_Suc [symmetric])
   262 apply (rule eventually_constant_MOST_Suc_eq)
   263 apply (rule eventually_constant_iterate_app)
   264 done
   265 
   266 lemma d_fixed_iff: "d\<cdot>x = x \<longleftrightarrow> f\<cdot>x = x"
   267 proof
   268   assume "d\<cdot>x = x"
   269   with f_d [where x=x]
   270   show "f\<cdot>x = x" by simp
   271 next
   272   assume f: "f\<cdot>x = x"
   273   have "\<forall>n. iterate n\<cdot>f\<cdot>x = x"
   274     by (rule allI, rule nat.induct, simp, simp add: f)
   275   hence "MOST n. iterate n\<cdot>f\<cdot>x = x"
   276     by (rule ALL_MOST)
   277   thus "d\<cdot>x = x"
   278     by (rule MOST_d)
   279 qed
   280 
   281 lemma finite_deflation_d: "finite_deflation d"
   282 proof
   283   fix x :: 'a
   284   have "d \<in> range (\<lambda>n. iterate n\<cdot>f)"
   285     unfolding eventual_iterate_def
   286     using eventually_constant_iterate
   287     by (rule eventual_mem_range)
   288   then obtain n where n: "d = iterate n\<cdot>f" ..
   289   have "iterate n\<cdot>f\<cdot>(d\<cdot>x) = d\<cdot>x"
   290     using f_d by (rule iterate_fixed)
   291   thus "d\<cdot>(d\<cdot>x) = d\<cdot>x"
   292     by (simp add: n)
   293 next
   294   fix x :: 'a
   295   show "d\<cdot>x \<sqsubseteq> x"
   296     by (rule MOST_d, simp add: iterate_below)
   297 next
   298   from finite_range
   299   have "finite {x. f\<cdot>x = x}"
   300     by (rule finite_range_imp_finite_fixes)
   301   thus "finite {x. d\<cdot>x = x}"
   302     by (simp add: d_fixed_iff)
   303 qed
   304 
   305 lemma deflation_d: "deflation d"
   306 using finite_deflation_d
   307 by (rule finite_deflation_imp_deflation)
   308 
   309 end
   310 
   311 lemma finite_deflation_eventual_iterate:
   312   "pre_deflation d \<Longrightarrow> finite_deflation (eventual_iterate d)"
   313 by (rule pre_deflation.finite_deflation_d)
   314 
   315 lemma pre_deflation_oo:
   316   assumes "finite_deflation d"
   317   assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
   318   shows "pre_deflation (d oo f)"
   319 proof
   320   interpret d: finite_deflation d by fact
   321   fix x
   322   show "\<And>x. (d oo f)\<cdot>x \<sqsubseteq> x"
   323     by (simp, rule below_trans [OF d.below f])
   324   show "finite (range (\<lambda>x. (d oo f)\<cdot>x))"
   325     by (rule finite_subset [OF _ d.finite_range], auto)
   326 qed
   327 
   328 lemma eventual_iterate_oo_fixed_iff:
   329   assumes "finite_deflation d"
   330   assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
   331   shows "eventual_iterate (d oo f)\<cdot>x = x \<longleftrightarrow> d\<cdot>x = x \<and> f\<cdot>x = x"
   332 proof -
   333   interpret d: finite_deflation d by fact
   334   let ?e = "d oo f"
   335   interpret e: pre_deflation "d oo f"
   336     using `finite_deflation d` f
   337     by (rule pre_deflation_oo)
   338   let ?g = "eventual (\<lambda>n. iterate n\<cdot>?e)"
   339   show ?thesis
   340     apply (subst e.d_fixed_iff)
   341     apply simp
   342     apply safe
   343     apply (erule subst)
   344     apply (rule d.idem)
   345     apply (rule below_antisym)
   346     apply (rule f)
   347     apply (erule subst, rule d.below)
   348     apply simp
   349     done
   350 qed
   351 
   352 lemma eventual_mono:
   353   assumes A: "eventually_constant A"
   354   assumes B: "eventually_constant B"
   355   assumes below: "\<And>n. A n \<sqsubseteq> B n"
   356   shows "eventual A \<sqsubseteq> eventual B"
   357 proof -
   358   from A have "MOST n. A n = eventual A"
   359     by (rule MOST_eq_eventual)
   360   then have "MOST n. eventual A \<sqsubseteq> B n"
   361     by (rule MOST_mono) (erule subst, rule below)
   362   with B show "eventual A \<sqsubseteq> eventual B"
   363     by (rule MOST_eventual)
   364 qed
   365 
   366 lemma eventual_iterate_mono:
   367   assumes f: "pre_deflation f" and g: "pre_deflation g" and "f \<sqsubseteq> g"
   368   shows "eventual_iterate f \<sqsubseteq> eventual_iterate g"
   369 unfolding eventual_iterate_def
   370 apply (rule eventual_mono)
   371 apply (rule pre_deflation.eventually_constant_iterate [OF f])
   372 apply (rule pre_deflation.eventually_constant_iterate [OF g])
   373 apply (rule monofun_cfun_arg [OF `f \<sqsubseteq> g`])
   374 done
   375 
   376 lemma cont2cont_eventual_iterate_oo:
   377   assumes d: "finite_deflation d"
   378   assumes cont: "cont f" and below: "\<And>x y. f x\<cdot>y \<sqsubseteq> y"
   379   shows "cont (\<lambda>x. eventual_iterate (d oo f x))"
   380     (is "cont ?e")
   381 proof (rule contI2)
   382   show "monofun ?e"
   383     apply (rule monofunI)
   384     apply (rule eventual_iterate_mono)
   385     apply (rule pre_deflation_oo [OF d below])
   386     apply (rule pre_deflation_oo [OF d below])
   387     apply (rule monofun_cfun_arg)
   388     apply (erule cont2monofunE [OF cont])
   389     done
   390 next
   391   fix Y :: "nat \<Rightarrow> 'b"
   392   assume Y: "chain Y"
   393   with cont have fY: "chain (\<lambda>i. f (Y i))"
   394     by (rule ch2ch_cont)
   395   assume eY: "chain (\<lambda>i. ?e (Y i))"
   396   have lub_below: "\<And>x. f (\<Squnion>i. Y i)\<cdot>x \<sqsubseteq> x"
   397     by (rule admD [OF _ Y], simp add: cont, rule below)
   398   have "deflation (?e (\<Squnion>i. Y i))"
   399     apply (rule pre_deflation.deflation_d)
   400     apply (rule pre_deflation_oo [OF d lub_below])
   401     done
   402   then show "?e (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. ?e (Y i))"
   403   proof (rule deflation.belowI)
   404     fix x :: 'a
   405     assume "?e (\<Squnion>i. Y i)\<cdot>x = x"
   406     hence "d\<cdot>x = x" and "f (\<Squnion>i. Y i)\<cdot>x = x"
   407       by (simp_all add: eventual_iterate_oo_fixed_iff [OF d lub_below])
   408     hence "(\<Squnion>i. f (Y i)\<cdot>x) = x"
   409       apply (simp only: cont2contlubE [OF cont Y])
   410       apply (simp only: contlub_cfun_fun [OF fY])
   411       done
   412     have "compact (d\<cdot>x)"
   413       using d by (rule finite_deflation.compact)
   414     then have "compact x"
   415       using `d\<cdot>x = x` by simp
   416     then have "compact (\<Squnion>i. f (Y i)\<cdot>x)"
   417       using `(\<Squnion>i. f (Y i)\<cdot>x) = x` by simp
   418     then have "\<exists>n. max_in_chain n (\<lambda>i. f (Y i)\<cdot>x)"
   419       by - (rule compact_imp_max_in_chain, simp add: fY, assumption)
   420     then obtain n where n: "max_in_chain n (\<lambda>i. f (Y i)\<cdot>x)" ..
   421     then have "f (Y n)\<cdot>x = x"
   422       using `(\<Squnion>i. f (Y i)\<cdot>x) = x` fY by (simp add: maxinch_is_thelub)
   423     with `d\<cdot>x = x` have "?e (Y n)\<cdot>x = x"
   424       by (simp add: eventual_iterate_oo_fixed_iff [OF d below])
   425     moreover have "?e (Y n)\<cdot>x \<sqsubseteq> (\<Squnion>i. ?e (Y i)\<cdot>x)"
   426       by (rule is_ub_thelub, simp add: eY)
   427     ultimately have "x \<sqsubseteq> (\<Squnion>i. ?e (Y i))\<cdot>x"
   428       by (simp add: contlub_cfun_fun eY)
   429     also have "(\<Squnion>i. ?e (Y i))\<cdot>x \<sqsubseteq> x"
   430       apply (rule deflation.below)
   431       apply (rule admD [OF adm_deflation eY])
   432       apply (rule pre_deflation.deflation_d)
   433       apply (rule pre_deflation_oo [OF d below])
   434       done
   435     finally show "(\<Squnion>i. ?e (Y i))\<cdot>x = x" ..
   436   qed
   437 qed
   438 
   439 subsection {* Take function for finite deflations *}
   440 
   441 definition
   442   defl_take :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<Rightarrow> (udom \<rightarrow> udom)"
   443 where
   444   "defl_take i d = eventual_iterate (udom_approx i oo d)"
   445 
   446 lemma finite_deflation_defl_take:
   447   "deflation d \<Longrightarrow> finite_deflation (defl_take i d)"
   448 unfolding defl_take_def
   449 apply (rule pre_deflation.finite_deflation_d)
   450 apply (rule pre_deflation_oo)
   451 apply (rule finite_deflation_udom_approx)
   452 apply (erule deflation.below)
   453 done
   454 
   455 lemma deflation_defl_take:
   456   "deflation d \<Longrightarrow> deflation (defl_take i d)"
   457 apply (rule finite_deflation_imp_deflation)
   458 apply (erule finite_deflation_defl_take)
   459 done
   460 
   461 lemma defl_take_fixed_iff:
   462   "deflation d \<Longrightarrow> defl_take i d\<cdot>x = x \<longleftrightarrow> udom_approx i\<cdot>x = x \<and> d\<cdot>x = x"
   463 unfolding defl_take_def
   464 apply (rule eventual_iterate_oo_fixed_iff)
   465 apply (rule finite_deflation_udom_approx)
   466 apply (erule deflation.below)
   467 done
   468 
   469 lemma defl_take_below:
   470   "\<lbrakk>a \<sqsubseteq> b; deflation a; deflation b\<rbrakk> \<Longrightarrow> defl_take i a \<sqsubseteq> defl_take i b"
   471 apply (rule deflation.belowI)
   472 apply (erule deflation_defl_take)
   473 apply (simp add: defl_take_fixed_iff)
   474 apply (erule (1) deflation.belowD)
   475 apply (erule conjunct2)
   476 done
   477 
   478 lemma cont2cont_defl_take:
   479   assumes cont: "cont f" and below: "\<And>x y. f x\<cdot>y \<sqsubseteq> y"
   480   shows "cont (\<lambda>x. defl_take i (f x))"
   481 unfolding defl_take_def
   482 using finite_deflation_udom_approx assms
   483 by (rule cont2cont_eventual_iterate_oo)
   484 
   485 definition
   486   fd_take :: "nat \<Rightarrow> fin_defl \<Rightarrow> fin_defl"
   487 where
   488   "fd_take i d = Abs_fin_defl (defl_take i (Rep_fin_defl d))"
   489 
   490 lemma Rep_fin_defl_fd_take:
   491   "Rep_fin_defl (fd_take i d) = defl_take i (Rep_fin_defl d)"
   492 unfolding fd_take_def
   493 apply (rule Abs_fin_defl_inverse [unfolded mem_Collect_eq])
   494 apply (rule finite_deflation_defl_take)
   495 apply (rule deflation_Rep_fin_defl)
   496 done
   497 
   498 lemma fd_take_fixed_iff:
   499   "Rep_fin_defl (fd_take i d)\<cdot>x = x \<longleftrightarrow>
   500     udom_approx i\<cdot>x = x \<and> Rep_fin_defl d\<cdot>x = x"
   501 unfolding Rep_fin_defl_fd_take
   502 apply (rule defl_take_fixed_iff)
   503 apply (rule deflation_Rep_fin_defl)
   504 done
   505 
   506 lemma fd_take_below: "fd_take n d \<sqsubseteq> d"
   507 apply (rule fin_defl_belowI)
   508 apply (simp add: fd_take_fixed_iff)
   509 done
   510 
   511 lemma fd_take_idem: "fd_take n (fd_take n d) = fd_take n d"
   512 apply (rule fin_defl_eqI)
   513 apply (simp add: fd_take_fixed_iff)
   514 done
   515 
   516 lemma fd_take_mono: "a \<sqsubseteq> b \<Longrightarrow> fd_take n a \<sqsubseteq> fd_take n b"
   517 apply (rule fin_defl_belowI)
   518 apply (simp add: fd_take_fixed_iff)
   519 apply (simp add: fin_defl_belowD)
   520 done
   521 
   522 lemma approx_fixed_le_lemma: "\<lbrakk>i \<le> j; udom_approx i\<cdot>x = x\<rbrakk> \<Longrightarrow> udom_approx j\<cdot>x = x"
   523 apply (rule deflation.belowD)
   524 apply (rule finite_deflation_imp_deflation)
   525 apply (rule finite_deflation_udom_approx)
   526 apply (erule chain_mono [OF chain_udom_approx])
   527 apply assumption
   528 done
   529 
   530 lemma fd_take_chain: "m \<le> n \<Longrightarrow> fd_take m a \<sqsubseteq> fd_take n a"
   531 apply (rule fin_defl_belowI)
   532 apply (simp add: fd_take_fixed_iff)
   533 apply (simp add: approx_fixed_le_lemma)
   534 done
   535 
   536 lemma finite_range_fd_take: "finite (range (fd_take n))"
   537 apply (rule finite_imageD [where f="\<lambda>a. {x. Rep_fin_defl a\<cdot>x = x}"])
   538 apply (rule finite_subset [where B="Pow {x. udom_approx n\<cdot>x = x}"])
   539 apply (clarify, simp add: fd_take_fixed_iff)
   540 apply (simp add: finite_deflation.finite_fixes [OF finite_deflation_udom_approx])
   541 apply (rule inj_onI, clarify)
   542 apply (simp add: set_eq_iff fin_defl_eqI)
   543 done
   544 
   545 lemma fd_take_covers: "\<exists>n. fd_take n a = a"
   546 apply (rule_tac x=
   547   "Max ((\<lambda>x. LEAST n. udom_approx n\<cdot>x = x) ` {x. Rep_fin_defl a\<cdot>x = x})" in exI)
   548 apply (rule below_antisym)
   549 apply (rule fd_take_below)
   550 apply (rule fin_defl_belowI)
   551 apply (simp add: fd_take_fixed_iff)
   552 apply (rule approx_fixed_le_lemma)
   553 apply (rule Max_ge)
   554 apply (rule finite_imageI)
   555 apply (rule Rep_fin_defl.finite_fixes)
   556 apply (rule imageI)
   557 apply (erule CollectI)
   558 apply (rule LeastI_ex)
   559 apply (rule approx_chain.compact_eq_approx [OF udom_approx])
   560 apply (erule subst)
   561 apply (rule Rep_fin_defl.compact)
   562 done
   563 
   564 subsection {* Chain of approx functions on algebraic deflations *}
   565 
   566 definition
   567   defl_approx :: "nat \<Rightarrow> defl \<rightarrow> defl"
   568 where
   569   "defl_approx = (\<lambda>i. defl.basis_fun (\<lambda>d. defl_principal (fd_take i d)))"
   570 
   571 lemma defl_approx_principal:
   572   "defl_approx i\<cdot>(defl_principal d) = defl_principal (fd_take i d)"
   573 unfolding defl_approx_def
   574 by (simp add: defl.basis_fun_principal fd_take_mono)
   575 
   576 lemma defl_approx: "approx_chain defl_approx"
   577 proof
   578   show chain: "chain defl_approx"
   579     unfolding defl_approx_def
   580     by (simp add: chainI defl.basis_fun_mono fd_take_mono fd_take_chain)
   581   show idem: "\<And>i x. defl_approx i\<cdot>(defl_approx i\<cdot>x) = defl_approx i\<cdot>x"
   582     apply (induct_tac x rule: defl.principal_induct, simp)
   583     apply (simp add: defl_approx_principal fd_take_idem)
   584     done
   585   show below: "\<And>i x. defl_approx i\<cdot>x \<sqsubseteq> x"
   586     apply (induct_tac x rule: defl.principal_induct, simp)
   587     apply (simp add: defl_approx_principal fd_take_below)
   588     done
   589   show lub: "(\<Squnion>i. defl_approx i) = ID"
   590     apply (rule cfun_eqI, rule below_antisym)
   591     apply (simp add: contlub_cfun_fun chain lub_below_iff chain below)
   592     apply (induct_tac x rule: defl.principal_induct, simp)
   593     apply (simp add: contlub_cfun_fun chain)
   594     apply (simp add: compact_below_lub_iff defl.compact_principal chain)
   595     apply (simp add: defl_approx_principal)
   596     apply (subgoal_tac "\<exists>i. fd_take i a = a", metis below_refl)
   597     apply (rule fd_take_covers)
   598     done
   599   show "\<And>i. finite {x. defl_approx i\<cdot>x = x}"
   600     apply (rule finite_range_imp_finite_fixes)
   601     apply (rule_tac B="defl_principal ` range (fd_take i)" in rev_finite_subset)
   602     apply (simp add: finite_range_fd_take)
   603     apply (clarsimp, rename_tac x)
   604     apply (induct_tac x rule: defl.principal_induct)
   605     apply (simp add: adm_mem_finite finite_range_fd_take)
   606     apply (simp add: defl_approx_principal)
   607     done
   608 qed
   609 
   610 subsection {* Algebraic deflations are a bifinite domain *}
   611 
   612 instantiation defl :: bifinite
   613 begin
   614 
   615 definition
   616   "emb = udom_emb defl_approx"
   617 
   618 definition
   619   "prj = udom_prj defl_approx"
   620 
   621 definition
   622   "defl (t::defl itself) =
   623     (\<Squnion>i. defl_principal (Abs_fin_defl (emb oo defl_approx i oo prj)))"
   624 
   625 definition
   626   "(liftemb :: defl u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
   627 
   628 definition
   629   "(liftprj :: udom \<rightarrow> defl u) = u_map\<cdot>prj oo udom_prj u_approx"
   630 
   631 definition
   632   "liftdefl (t::defl itself) = u_defl\<cdot>DEFL(defl)"
   633 
   634 instance
   635 using liftemb_defl_def liftprj_defl_def liftdefl_defl_def
   636 proof (rule bifinite_class_intro)
   637   show ep: "ep_pair emb (prj :: udom \<rightarrow> defl)"
   638     unfolding emb_defl_def prj_defl_def
   639     by (rule ep_pair_udom [OF defl_approx])
   640   show "cast\<cdot>DEFL(defl) = emb oo (prj :: udom \<rightarrow> defl)"
   641     unfolding defl_defl_def
   642     apply (subst contlub_cfun_arg)
   643     apply (rule chainI)
   644     apply (rule defl.principal_mono)
   645     apply (simp add: below_fin_defl_def)
   646     apply (simp add: Abs_fin_defl_inverse approx_chain.finite_deflation_approx [OF defl_approx]
   647                      ep_pair.finite_deflation_e_d_p [OF ep])
   648     apply (intro monofun_cfun below_refl)
   649     apply (rule chainE)
   650     apply (rule approx_chain.chain_approx [OF defl_approx])
   651     apply (subst cast_defl_principal)
   652     apply (simp add: Abs_fin_defl_inverse approx_chain.finite_deflation_approx [OF defl_approx]
   653                      ep_pair.finite_deflation_e_d_p [OF ep])
   654     apply (simp add: lub_distribs approx_chain.chain_approx [OF defl_approx]
   655                      approx_chain.lub_approx [OF defl_approx])
   656     done
   657 qed
   658 
   659 end
   660 
   661 end