src/HOLCF/Algebraic.thy
 author haftmann Fri Jun 19 21:08:07 2009 +0200 (2009-06-19) changeset 31726 ffd2dc631d88 parent 31164 f550c4cf3f3a child 33586 0e745228d605 permissions -rw-r--r--
merged
```     1 (*  Title:      HOLCF/Algebraic.thy
```
```     2     Author:     Brian Huffman
```
```     3 *)
```
```     4
```
```     5 header {* Algebraic deflations *}
```
```     6
```
```     7 theory Algebraic
```
```     8 imports Completion Fix Eventual
```
```     9 begin
```
```    10
```
```    11 subsection {* Constructing finite deflations by iteration *}
```
```    12
```
```    13 lemma finite_deflation_imp_deflation:
```
```    14   "finite_deflation d \<Longrightarrow> deflation d"
```
```    15 unfolding finite_deflation_def by simp
```
```    16
```
```    17 lemma le_Suc_induct:
```
```    18   assumes le: "i \<le> j"
```
```    19   assumes step: "\<And>i. P i (Suc i)"
```
```    20   assumes refl: "\<And>i. P i i"
```
```    21   assumes trans: "\<And>i j k. \<lbrakk>P i j; P j k\<rbrakk> \<Longrightarrow> P i k"
```
```    22   shows "P i j"
```
```    23 proof (cases "i = j")
```
```    24   assume "i = j"
```
```    25   thus "P i j" by (simp add: refl)
```
```    26 next
```
```    27   assume "i \<noteq> j"
```
```    28   with le have "i < j" by simp
```
```    29   thus "P i j" using step trans by (rule less_Suc_induct)
```
```    30 qed
```
```    31
```
```    32 definition
```
```    33   eventual_iterate :: "('a \<rightarrow> 'a::cpo) \<Rightarrow> ('a \<rightarrow> 'a)"
```
```    34 where
```
```    35   "eventual_iterate f = eventual (\<lambda>n. iterate n\<cdot>f)"
```
```    36
```
```    37 text {* A pre-deflation is like a deflation, but not idempotent. *}
```
```    38
```
```    39 locale pre_deflation =
```
```    40   fixes f :: "'a \<rightarrow> 'a::cpo"
```
```    41   assumes below: "\<And>x. f\<cdot>x \<sqsubseteq> x"
```
```    42   assumes finite_range: "finite (range (\<lambda>x. f\<cdot>x))"
```
```    43 begin
```
```    44
```
```    45 lemma iterate_below: "iterate i\<cdot>f\<cdot>x \<sqsubseteq> x"
```
```    46 by (induct i, simp_all add: below_trans [OF below])
```
```    47
```
```    48 lemma iterate_fixed: "f\<cdot>x = x \<Longrightarrow> iterate i\<cdot>f\<cdot>x = x"
```
```    49 by (induct i, simp_all)
```
```    50
```
```    51 lemma antichain_iterate_app: "i \<le> j \<Longrightarrow> iterate j\<cdot>f\<cdot>x \<sqsubseteq> iterate i\<cdot>f\<cdot>x"
```
```    52 apply (erule le_Suc_induct)
```
```    53 apply (simp add: below)
```
```    54 apply (rule below_refl)
```
```    55 apply (erule (1) below_trans)
```
```    56 done
```
```    57
```
```    58 lemma finite_range_iterate_app: "finite (range (\<lambda>i. iterate i\<cdot>f\<cdot>x))"
```
```    59 proof (rule finite_subset)
```
```    60   show "range (\<lambda>i. iterate i\<cdot>f\<cdot>x) \<subseteq> insert x (range (\<lambda>x. f\<cdot>x))"
```
```    61     by (clarify, case_tac i, simp_all)
```
```    62   show "finite (insert x (range (\<lambda>x. f\<cdot>x)))"
```
```    63     by (simp add: finite_range)
```
```    64 qed
```
```    65
```
```    66 lemma eventually_constant_iterate_app:
```
```    67   "eventually_constant (\<lambda>i. iterate i\<cdot>f\<cdot>x)"
```
```    68 unfolding eventually_constant_def MOST_nat_le
```
```    69 proof -
```
```    70   let ?Y = "\<lambda>i. iterate i\<cdot>f\<cdot>x"
```
```    71   have "\<exists>j. \<forall>k. ?Y j \<sqsubseteq> ?Y k"
```
```    72     apply (rule finite_range_has_max)
```
```    73     apply (erule antichain_iterate_app)
```
```    74     apply (rule finite_range_iterate_app)
```
```    75     done
```
```    76   then obtain j where j: "\<And>k. ?Y j \<sqsubseteq> ?Y k" by fast
```
```    77   show "\<exists>z m. \<forall>n\<ge>m. ?Y n = z"
```
```    78   proof (intro exI allI impI)
```
```    79     fix k
```
```    80     assume "j \<le> k"
```
```    81     hence "?Y k \<sqsubseteq> ?Y j" by (rule antichain_iterate_app)
```
```    82     also have "?Y j \<sqsubseteq> ?Y k" by (rule j)
```
```    83     finally show "?Y k = ?Y j" .
```
```    84   qed
```
```    85 qed
```
```    86
```
```    87 lemma eventually_constant_iterate:
```
```    88   "eventually_constant (\<lambda>n. iterate n\<cdot>f)"
```
```    89 proof -
```
```    90   have "\<forall>y\<in>range (\<lambda>x. f\<cdot>x). eventually_constant (\<lambda>i. iterate i\<cdot>f\<cdot>y)"
```
```    91     by (simp add: eventually_constant_iterate_app)
```
```    92   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"
```
```    93     unfolding eventually_constant_MOST_MOST .
```
```    94   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"
```
```    95     by (simp only: MOST_finite_Ball_distrib [OF finite_range])
```
```    96   hence "MOST i. MOST j. \<forall>x. iterate j\<cdot>f\<cdot>(f\<cdot>x) = iterate i\<cdot>f\<cdot>(f\<cdot>x)"
```
```    97     by simp
```
```    98   hence "MOST i. MOST j. \<forall>x. iterate (Suc j)\<cdot>f\<cdot>x = iterate (Suc i)\<cdot>f\<cdot>x"
```
```    99     by (simp only: iterate_Suc2)
```
```   100   hence "MOST i. MOST j. iterate (Suc j)\<cdot>f = iterate (Suc i)\<cdot>f"
```
```   101     by (simp only: expand_cfun_eq)
```
```   102   hence "eventually_constant (\<lambda>i. iterate (Suc i)\<cdot>f)"
```
```   103     unfolding eventually_constant_MOST_MOST .
```
```   104   thus "eventually_constant (\<lambda>i. iterate i\<cdot>f)"
```
```   105     by (rule eventually_constant_SucD)
```
```   106 qed
```
```   107
```
```   108 abbreviation
```
```   109   d :: "'a \<rightarrow> 'a"
```
```   110 where
```
```   111   "d \<equiv> eventual_iterate f"
```
```   112
```
```   113 lemma MOST_d: "MOST n. P (iterate n\<cdot>f) \<Longrightarrow> P d"
```
```   114 unfolding eventual_iterate_def
```
```   115 using eventually_constant_iterate by (rule MOST_eventual)
```
```   116
```
```   117 lemma f_d: "f\<cdot>(d\<cdot>x) = d\<cdot>x"
```
```   118 apply (rule MOST_d)
```
```   119 apply (subst iterate_Suc [symmetric])
```
```   120 apply (rule eventually_constant_MOST_Suc_eq)
```
```   121 apply (rule eventually_constant_iterate_app)
```
```   122 done
```
```   123
```
```   124 lemma d_fixed_iff: "d\<cdot>x = x \<longleftrightarrow> f\<cdot>x = x"
```
```   125 proof
```
```   126   assume "d\<cdot>x = x"
```
```   127   with f_d [where x=x]
```
```   128   show "f\<cdot>x = x" by simp
```
```   129 next
```
```   130   assume f: "f\<cdot>x = x"
```
```   131   have "\<forall>n. iterate n\<cdot>f\<cdot>x = x"
```
```   132     by (rule allI, rule nat.induct, simp, simp add: f)
```
```   133   hence "MOST n. iterate n\<cdot>f\<cdot>x = x"
```
```   134     by (rule ALL_MOST)
```
```   135   thus "d\<cdot>x = x"
```
```   136     by (rule MOST_d)
```
```   137 qed
```
```   138
```
```   139 lemma finite_deflation_d: "finite_deflation d"
```
```   140 proof
```
```   141   fix x :: 'a
```
```   142   have "d \<in> range (\<lambda>n. iterate n\<cdot>f)"
```
```   143     unfolding eventual_iterate_def
```
```   144     using eventually_constant_iterate
```
```   145     by (rule eventual_mem_range)
```
```   146   then obtain n where n: "d = iterate n\<cdot>f" ..
```
```   147   have "iterate n\<cdot>f\<cdot>(d\<cdot>x) = d\<cdot>x"
```
```   148     using f_d by (rule iterate_fixed)
```
```   149   thus "d\<cdot>(d\<cdot>x) = d\<cdot>x"
```
```   150     by (simp add: n)
```
```   151 next
```
```   152   fix x :: 'a
```
```   153   show "d\<cdot>x \<sqsubseteq> x"
```
```   154     by (rule MOST_d, simp add: iterate_below)
```
```   155 next
```
```   156   from finite_range
```
```   157   have "finite {x. f\<cdot>x = x}"
```
```   158     by (rule finite_range_imp_finite_fixes)
```
```   159   thus "finite {x. d\<cdot>x = x}"
```
```   160     by (simp add: d_fixed_iff)
```
```   161 qed
```
```   162
```
```   163 lemma deflation_d: "deflation d"
```
```   164 using finite_deflation_d
```
```   165 by (rule finite_deflation_imp_deflation)
```
```   166
```
```   167 end
```
```   168
```
```   169 lemma finite_deflation_eventual_iterate:
```
```   170   "pre_deflation d \<Longrightarrow> finite_deflation (eventual_iterate d)"
```
```   171 by (rule pre_deflation.finite_deflation_d)
```
```   172
```
```   173 lemma pre_deflation_oo:
```
```   174   assumes "finite_deflation d"
```
```   175   assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
```
```   176   shows "pre_deflation (d oo f)"
```
```   177 proof
```
```   178   interpret d: finite_deflation d by fact
```
```   179   fix x
```
```   180   show "\<And>x. (d oo f)\<cdot>x \<sqsubseteq> x"
```
```   181     by (simp, rule below_trans [OF d.below f])
```
```   182   show "finite (range (\<lambda>x. (d oo f)\<cdot>x))"
```
```   183     by (rule finite_subset [OF _ d.finite_range], auto)
```
```   184 qed
```
```   185
```
```   186 lemma eventual_iterate_oo_fixed_iff:
```
```   187   assumes "finite_deflation d"
```
```   188   assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
```
```   189   shows "eventual_iterate (d oo f)\<cdot>x = x \<longleftrightarrow> d\<cdot>x = x \<and> f\<cdot>x = x"
```
```   190 proof -
```
```   191   interpret d: finite_deflation d by fact
```
```   192   let ?e = "d oo f"
```
```   193   interpret e: pre_deflation "d oo f"
```
```   194     using `finite_deflation d` f
```
```   195     by (rule pre_deflation_oo)
```
```   196   let ?g = "eventual (\<lambda>n. iterate n\<cdot>?e)"
```
```   197   show ?thesis
```
```   198     apply (subst e.d_fixed_iff)
```
```   199     apply simp
```
```   200     apply safe
```
```   201     apply (erule subst)
```
```   202     apply (rule d.idem)
```
```   203     apply (rule below_antisym)
```
```   204     apply (rule f)
```
```   205     apply (erule subst, rule d.below)
```
```   206     apply simp
```
```   207     done
```
```   208 qed
```
```   209
```
```   210 lemma eventual_mono:
```
```   211   assumes A: "eventually_constant A"
```
```   212   assumes B: "eventually_constant B"
```
```   213   assumes below: "\<And>n. A n \<sqsubseteq> B n"
```
```   214   shows "eventual A \<sqsubseteq> eventual B"
```
```   215 proof -
```
```   216   from A have "MOST n. A n = eventual A"
```
```   217     by (rule MOST_eq_eventual)
```
```   218   then have "MOST n. eventual A \<sqsubseteq> B n"
```
```   219     by (rule MOST_mono) (erule subst, rule below)
```
```   220   with B show "eventual A \<sqsubseteq> eventual B"
```
```   221     by (rule MOST_eventual)
```
```   222 qed
```
```   223
```
```   224 lemma eventual_iterate_mono:
```
```   225   assumes f: "pre_deflation f" and g: "pre_deflation g" and "f \<sqsubseteq> g"
```
```   226   shows "eventual_iterate f \<sqsubseteq> eventual_iterate g"
```
```   227 unfolding eventual_iterate_def
```
```   228 apply (rule eventual_mono)
```
```   229 apply (rule pre_deflation.eventually_constant_iterate [OF f])
```
```   230 apply (rule pre_deflation.eventually_constant_iterate [OF g])
```
```   231 apply (rule monofun_cfun_arg [OF `f \<sqsubseteq> g`])
```
```   232 done
```
```   233
```
```   234 lemma cont2cont_eventual_iterate_oo:
```
```   235   assumes d: "finite_deflation d"
```
```   236   assumes cont: "cont f" and below: "\<And>x y. f x\<cdot>y \<sqsubseteq> y"
```
```   237   shows "cont (\<lambda>x. eventual_iterate (d oo f x))"
```
```   238     (is "cont ?e")
```
```   239 proof (rule contI2)
```
```   240   show "monofun ?e"
```
```   241     apply (rule monofunI)
```
```   242     apply (rule eventual_iterate_mono)
```
```   243     apply (rule pre_deflation_oo [OF d below])
```
```   244     apply (rule pre_deflation_oo [OF d below])
```
```   245     apply (rule monofun_cfun_arg)
```
```   246     apply (erule cont2monofunE [OF cont])
```
```   247     done
```
```   248 next
```
```   249   fix Y :: "nat \<Rightarrow> 'b"
```
```   250   assume Y: "chain Y"
```
```   251   with cont have fY: "chain (\<lambda>i. f (Y i))"
```
```   252     by (rule ch2ch_cont)
```
```   253   assume eY: "chain (\<lambda>i. ?e (Y i))"
```
```   254   have lub_below: "\<And>x. f (\<Squnion>i. Y i)\<cdot>x \<sqsubseteq> x"
```
```   255     by (rule admD [OF _ Y], simp add: cont, rule below)
```
```   256   have "deflation (?e (\<Squnion>i. Y i))"
```
```   257     apply (rule pre_deflation.deflation_d)
```
```   258     apply (rule pre_deflation_oo [OF d lub_below])
```
```   259     done
```
```   260   then show "?e (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. ?e (Y i))"
```
```   261   proof (rule deflation.belowI)
```
```   262     fix x :: 'a
```
```   263     assume "?e (\<Squnion>i. Y i)\<cdot>x = x"
```
```   264     hence "d\<cdot>x = x" and "f (\<Squnion>i. Y i)\<cdot>x = x"
```
```   265       by (simp_all add: eventual_iterate_oo_fixed_iff [OF d lub_below])
```
```   266     hence "(\<Squnion>i. f (Y i)\<cdot>x) = x"
```
```   267       apply (simp only: cont2contlubE [OF cont Y])
```
```   268       apply (simp only: contlub_cfun_fun [OF fY])
```
```   269       done
```
```   270     have "compact (d\<cdot>x)"
```
```   271       using d by (rule finite_deflation.compact)
```
```   272     then have "compact x"
```
```   273       using `d\<cdot>x = x` by simp
```
```   274     then have "compact (\<Squnion>i. f (Y i)\<cdot>x)"
```
```   275       using `(\<Squnion>i. f (Y i)\<cdot>x) = x` by simp
```
```   276     then have "\<exists>n. max_in_chain n (\<lambda>i. f (Y i)\<cdot>x)"
```
```   277       by - (rule compact_imp_max_in_chain, simp add: fY, assumption)
```
```   278     then obtain n where n: "max_in_chain n (\<lambda>i. f (Y i)\<cdot>x)" ..
```
```   279     then have "f (Y n)\<cdot>x = x"
```
```   280       using `(\<Squnion>i. f (Y i)\<cdot>x) = x` fY by (simp add: maxinch_is_thelub)
```
```   281     with `d\<cdot>x = x` have "?e (Y n)\<cdot>x = x"
```
```   282       by (simp add: eventual_iterate_oo_fixed_iff [OF d below])
```
```   283     moreover have "?e (Y n)\<cdot>x \<sqsubseteq> (\<Squnion>i. ?e (Y i)\<cdot>x)"
```
```   284       by (rule is_ub_thelub, simp add: eY)
```
```   285     ultimately have "x \<sqsubseteq> (\<Squnion>i. ?e (Y i))\<cdot>x"
```
```   286       by (simp add: contlub_cfun_fun eY)
```
```   287     also have "(\<Squnion>i. ?e (Y i))\<cdot>x \<sqsubseteq> x"
```
```   288       apply (rule deflation.below)
```
```   289       apply (rule admD [OF adm_deflation eY])
```
```   290       apply (rule pre_deflation.deflation_d)
```
```   291       apply (rule pre_deflation_oo [OF d below])
```
```   292       done
```
```   293     finally show "(\<Squnion>i. ?e (Y i))\<cdot>x = x" ..
```
```   294   qed
```
```   295 qed
```
```   296
```
```   297
```
```   298 subsection {* Type constructor for finite deflations *}
```
```   299
```
```   300 defaultsort profinite
```
```   301
```
```   302 typedef (open) 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
```
```   303 by (fast intro: finite_deflation_approx)
```
```   304
```
```   305 instantiation fin_defl :: (profinite) below
```
```   306 begin
```
```   307
```
```   308 definition below_fin_defl_def:
```
```   309     "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep_fin_defl x \<sqsubseteq> Rep_fin_defl y"
```
```   310
```
```   311 instance ..
```
```   312 end
```
```   313
```
```   314 instance fin_defl :: (profinite) po
```
```   315 by (rule typedef_po [OF type_definition_fin_defl below_fin_defl_def])
```
```   316
```
```   317 lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)"
```
```   318 using Rep_fin_defl by simp
```
```   319
```
```   320 lemma deflation_Rep_fin_defl: "deflation (Rep_fin_defl d)"
```
```   321 using finite_deflation_Rep_fin_defl
```
```   322 by (rule finite_deflation_imp_deflation)
```
```   323
```
```   324 interpretation Rep_fin_defl: finite_deflation "Rep_fin_defl d"
```
```   325 by (rule finite_deflation_Rep_fin_defl)
```
```   326
```
```   327 lemma fin_defl_belowI:
```
```   328   "(\<And>x. Rep_fin_defl a\<cdot>x = x \<Longrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a \<sqsubseteq> b"
```
```   329 unfolding below_fin_defl_def
```
```   330 by (rule Rep_fin_defl.belowI)
```
```   331
```
```   332 lemma fin_defl_belowD:
```
```   333   "\<lbrakk>a \<sqsubseteq> b; Rep_fin_defl a\<cdot>x = x\<rbrakk> \<Longrightarrow> Rep_fin_defl b\<cdot>x = x"
```
```   334 unfolding below_fin_defl_def
```
```   335 by (rule Rep_fin_defl.belowD)
```
```   336
```
```   337 lemma fin_defl_eqI:
```
```   338   "(\<And>x. Rep_fin_defl a\<cdot>x = x \<longleftrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a = b"
```
```   339 apply (rule below_antisym)
```
```   340 apply (rule fin_defl_belowI, simp)
```
```   341 apply (rule fin_defl_belowI, simp)
```
```   342 done
```
```   343
```
```   344 lemma Abs_fin_defl_mono:
```
```   345   "\<lbrakk>finite_deflation a; finite_deflation b; a \<sqsubseteq> b\<rbrakk>
```
```   346     \<Longrightarrow> Abs_fin_defl a \<sqsubseteq> Abs_fin_defl b"
```
```   347 unfolding below_fin_defl_def
```
```   348 by (simp add: Abs_fin_defl_inverse)
```
```   349
```
```   350
```
```   351 subsection {* Take function for finite deflations *}
```
```   352
```
```   353 definition
```
```   354   defl_approx :: "nat \<Rightarrow> ('a \<rightarrow> 'a) \<Rightarrow> ('a \<rightarrow> 'a)"
```
```   355 where
```
```   356   "defl_approx i d = eventual_iterate (approx i oo d)"
```
```   357
```
```   358 lemma finite_deflation_defl_approx:
```
```   359   "deflation d \<Longrightarrow> finite_deflation (defl_approx i d)"
```
```   360 unfolding defl_approx_def
```
```   361 apply (rule pre_deflation.finite_deflation_d)
```
```   362 apply (rule pre_deflation_oo)
```
```   363 apply (rule finite_deflation_approx)
```
```   364 apply (erule deflation.below)
```
```   365 done
```
```   366
```
```   367 lemma deflation_defl_approx:
```
```   368   "deflation d \<Longrightarrow> deflation (defl_approx i d)"
```
```   369 apply (rule finite_deflation_imp_deflation)
```
```   370 apply (erule finite_deflation_defl_approx)
```
```   371 done
```
```   372
```
```   373 lemma defl_approx_fixed_iff:
```
```   374   "deflation d \<Longrightarrow> defl_approx i d\<cdot>x = x \<longleftrightarrow> approx i\<cdot>x = x \<and> d\<cdot>x = x"
```
```   375 unfolding defl_approx_def
```
```   376 apply (rule eventual_iterate_oo_fixed_iff)
```
```   377 apply (rule finite_deflation_approx)
```
```   378 apply (erule deflation.below)
```
```   379 done
```
```   380
```
```   381 lemma defl_approx_below:
```
```   382   "\<lbrakk>a \<sqsubseteq> b; deflation a; deflation b\<rbrakk> \<Longrightarrow> defl_approx i a \<sqsubseteq> defl_approx i b"
```
```   383 apply (rule deflation.belowI)
```
```   384 apply (erule deflation_defl_approx)
```
```   385 apply (simp add: defl_approx_fixed_iff)
```
```   386 apply (erule (1) deflation.belowD)
```
```   387 apply (erule conjunct2)
```
```   388 done
```
```   389
```
```   390 lemma cont2cont_defl_approx:
```
```   391   assumes cont: "cont f" and below: "\<And>x y. f x\<cdot>y \<sqsubseteq> y"
```
```   392   shows "cont (\<lambda>x. defl_approx i (f x))"
```
```   393 unfolding defl_approx_def
```
```   394 using finite_deflation_approx assms
```
```   395 by (rule cont2cont_eventual_iterate_oo)
```
```   396
```
```   397 definition
```
```   398   fd_take :: "nat \<Rightarrow> 'a fin_defl \<Rightarrow> 'a fin_defl"
```
```   399 where
```
```   400   "fd_take i d = Abs_fin_defl (defl_approx i (Rep_fin_defl d))"
```
```   401
```
```   402 lemma Rep_fin_defl_fd_take:
```
```   403   "Rep_fin_defl (fd_take i d) = defl_approx i (Rep_fin_defl d)"
```
```   404 unfolding fd_take_def
```
```   405 apply (rule Abs_fin_defl_inverse [unfolded mem_Collect_eq])
```
```   406 apply (rule finite_deflation_defl_approx)
```
```   407 apply (rule deflation_Rep_fin_defl)
```
```   408 done
```
```   409
```
```   410 lemma fd_take_fixed_iff:
```
```   411   "Rep_fin_defl (fd_take i d)\<cdot>x = x \<longleftrightarrow>
```
```   412     approx i\<cdot>x = x \<and> Rep_fin_defl d\<cdot>x = x"
```
```   413 unfolding Rep_fin_defl_fd_take
```
```   414 apply (rule defl_approx_fixed_iff)
```
```   415 apply (rule deflation_Rep_fin_defl)
```
```   416 done
```
```   417
```
```   418 lemma fd_take_below: "fd_take n d \<sqsubseteq> d"
```
```   419 apply (rule fin_defl_belowI)
```
```   420 apply (simp add: fd_take_fixed_iff)
```
```   421 done
```
```   422
```
```   423 lemma fd_take_idem: "fd_take n (fd_take n d) = fd_take n d"
```
```   424 apply (rule fin_defl_eqI)
```
```   425 apply (simp add: fd_take_fixed_iff)
```
```   426 done
```
```   427
```
```   428 lemma fd_take_mono: "a \<sqsubseteq> b \<Longrightarrow> fd_take n a \<sqsubseteq> fd_take n b"
```
```   429 apply (rule fin_defl_belowI)
```
```   430 apply (simp add: fd_take_fixed_iff)
```
```   431 apply (simp add: fin_defl_belowD)
```
```   432 done
```
```   433
```
```   434 lemma approx_fixed_le_lemma: "\<lbrakk>i \<le> j; approx i\<cdot>x = x\<rbrakk> \<Longrightarrow> approx j\<cdot>x = x"
```
```   435 by (erule subst, simp add: min_def)
```
```   436
```
```   437 lemma fd_take_chain: "m \<le> n \<Longrightarrow> fd_take m a \<sqsubseteq> fd_take n a"
```
```   438 apply (rule fin_defl_belowI)
```
```   439 apply (simp add: fd_take_fixed_iff)
```
```   440 apply (simp add: approx_fixed_le_lemma)
```
```   441 done
```
```   442
```
```   443 lemma finite_range_fd_take: "finite (range (fd_take n))"
```
```   444 apply (rule finite_imageD [where f="\<lambda>a. {x. Rep_fin_defl a\<cdot>x = x}"])
```
```   445 apply (rule finite_subset [where B="Pow {x. approx n\<cdot>x = x}"])
```
```   446 apply (clarify, simp add: fd_take_fixed_iff)
```
```   447 apply (simp add: finite_fixes_approx)
```
```   448 apply (rule inj_onI, clarify)
```
```   449 apply (simp add: expand_set_eq fin_defl_eqI)
```
```   450 done
```
```   451
```
```   452 lemma fd_take_covers: "\<exists>n. fd_take n a = a"
```
```   453 apply (rule_tac x=
```
```   454   "Max ((\<lambda>x. LEAST n. approx n\<cdot>x = x) ` {x. Rep_fin_defl a\<cdot>x = x})" in exI)
```
```   455 apply (rule below_antisym)
```
```   456 apply (rule fd_take_below)
```
```   457 apply (rule fin_defl_belowI)
```
```   458 apply (simp add: fd_take_fixed_iff)
```
```   459 apply (rule approx_fixed_le_lemma)
```
```   460 apply (rule Max_ge)
```
```   461 apply (rule finite_imageI)
```
```   462 apply (rule Rep_fin_defl.finite_fixes)
```
```   463 apply (rule imageI)
```
```   464 apply (erule CollectI)
```
```   465 apply (rule LeastI_ex)
```
```   466 apply (rule profinite_compact_eq_approx)
```
```   467 apply (erule subst)
```
```   468 apply (rule Rep_fin_defl.compact)
```
```   469 done
```
```   470
```
```   471 interpretation fin_defl: basis_take below fd_take
```
```   472 apply default
```
```   473 apply (rule fd_take_below)
```
```   474 apply (rule fd_take_idem)
```
```   475 apply (erule fd_take_mono)
```
```   476 apply (rule fd_take_chain, simp)
```
```   477 apply (rule finite_range_fd_take)
```
```   478 apply (rule fd_take_covers)
```
```   479 done
```
```   480
```
```   481 subsection {* Defining algebraic deflations by ideal completion *}
```
```   482
```
```   483 typedef (open) 'a alg_defl =
```
```   484   "{S::'a fin_defl set. below.ideal S}"
```
```   485 by (fast intro: below.ideal_principal)
```
```   486
```
```   487 instantiation alg_defl :: (profinite) below
```
```   488 begin
```
```   489
```
```   490 definition
```
```   491   "x \<sqsubseteq> y \<longleftrightarrow> Rep_alg_defl x \<subseteq> Rep_alg_defl y"
```
```   492
```
```   493 instance ..
```
```   494 end
```
```   495
```
```   496 instance alg_defl :: (profinite) po
```
```   497 by (rule below.typedef_ideal_po
```
```   498     [OF type_definition_alg_defl below_alg_defl_def])
```
```   499
```
```   500 instance alg_defl :: (profinite) cpo
```
```   501 by (rule below.typedef_ideal_cpo
```
```   502     [OF type_definition_alg_defl below_alg_defl_def])
```
```   503
```
```   504 lemma Rep_alg_defl_lub:
```
```   505   "chain Y \<Longrightarrow> Rep_alg_defl (\<Squnion>i. Y i) = (\<Union>i. Rep_alg_defl (Y i))"
```
```   506 by (rule below.typedef_ideal_rep_contlub
```
```   507     [OF type_definition_alg_defl below_alg_defl_def])
```
```   508
```
```   509 lemma ideal_Rep_alg_defl: "below.ideal (Rep_alg_defl xs)"
```
```   510 by (rule Rep_alg_defl [unfolded mem_Collect_eq])
```
```   511
```
```   512 definition
```
```   513   alg_defl_principal :: "'a fin_defl \<Rightarrow> 'a alg_defl" where
```
```   514   "alg_defl_principal t = Abs_alg_defl {u. u \<sqsubseteq> t}"
```
```   515
```
```   516 lemma Rep_alg_defl_principal:
```
```   517   "Rep_alg_defl (alg_defl_principal t) = {u. u \<sqsubseteq> t}"
```
```   518 unfolding alg_defl_principal_def
```
```   519 by (simp add: Abs_alg_defl_inverse below.ideal_principal)
```
```   520
```
```   521 interpretation alg_defl:
```
```   522   ideal_completion below fd_take alg_defl_principal Rep_alg_defl
```
```   523 apply default
```
```   524 apply (rule ideal_Rep_alg_defl)
```
```   525 apply (erule Rep_alg_defl_lub)
```
```   526 apply (rule Rep_alg_defl_principal)
```
```   527 apply (simp only: below_alg_defl_def)
```
```   528 done
```
```   529
```
```   530 text {* Algebraic deflations are pointed *}
```
```   531
```
```   532 lemma finite_deflation_UU: "finite_deflation \<bottom>"
```
```   533 by default simp_all
```
```   534
```
```   535 lemma alg_defl_minimal:
```
```   536   "alg_defl_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x"
```
```   537 apply (induct x rule: alg_defl.principal_induct, simp)
```
```   538 apply (rule alg_defl.principal_mono)
```
```   539 apply (induct_tac a)
```
```   540 apply (rule Abs_fin_defl_mono)
```
```   541 apply (rule finite_deflation_UU)
```
```   542 apply simp
```
```   543 apply (rule minimal)
```
```   544 done
```
```   545
```
```   546 instance alg_defl :: (bifinite) pcpo
```
```   547 by intro_classes (fast intro: alg_defl_minimal)
```
```   548
```
```   549 lemma inst_alg_defl_pcpo: "\<bottom> = alg_defl_principal (Abs_fin_defl \<bottom>)"
```
```   550 by (rule alg_defl_minimal [THEN UU_I, symmetric])
```
```   551
```
```   552 text {* Algebraic deflations are profinite *}
```
```   553
```
```   554 instantiation alg_defl :: (profinite) profinite
```
```   555 begin
```
```   556
```
```   557 definition
```
```   558   approx_alg_defl_def: "approx = alg_defl.completion_approx"
```
```   559
```
```   560 instance
```
```   561 apply (intro_classes, unfold approx_alg_defl_def)
```
```   562 apply (rule alg_defl.chain_completion_approx)
```
```   563 apply (rule alg_defl.lub_completion_approx)
```
```   564 apply (rule alg_defl.completion_approx_idem)
```
```   565 apply (rule alg_defl.finite_fixes_completion_approx)
```
```   566 done
```
```   567
```
```   568 end
```
```   569
```
```   570 instance alg_defl :: (bifinite) bifinite ..
```
```   571
```
```   572 lemma approx_alg_defl_principal [simp]:
```
```   573   "approx n\<cdot>(alg_defl_principal t) = alg_defl_principal (fd_take n t)"
```
```   574 unfolding approx_alg_defl_def
```
```   575 by (rule alg_defl.completion_approx_principal)
```
```   576
```
```   577 lemma approx_eq_alg_defl_principal:
```
```   578   "\<exists>t\<in>Rep_alg_defl xs. approx n\<cdot>xs = alg_defl_principal (fd_take n t)"
```
```   579 unfolding approx_alg_defl_def
```
```   580 by (rule alg_defl.completion_approx_eq_principal)
```
```   581
```
```   582
```
```   583 subsection {* Applying algebraic deflations *}
```
```   584
```
```   585 definition
```
```   586   cast :: "'a alg_defl \<rightarrow> 'a \<rightarrow> 'a"
```
```   587 where
```
```   588   "cast = alg_defl.basis_fun Rep_fin_defl"
```
```   589
```
```   590 lemma cast_alg_defl_principal:
```
```   591   "cast\<cdot>(alg_defl_principal a) = Rep_fin_defl a"
```
```   592 unfolding cast_def
```
```   593 apply (rule alg_defl.basis_fun_principal)
```
```   594 apply (simp only: below_fin_defl_def)
```
```   595 done
```
```   596
```
```   597 lemma deflation_cast: "deflation (cast\<cdot>d)"
```
```   598 apply (induct d rule: alg_defl.principal_induct)
```
```   599 apply (rule adm_subst [OF _ adm_deflation], simp)
```
```   600 apply (simp add: cast_alg_defl_principal)
```
```   601 apply (rule finite_deflation_imp_deflation)
```
```   602 apply (rule finite_deflation_Rep_fin_defl)
```
```   603 done
```
```   604
```
```   605 lemma finite_deflation_cast:
```
```   606   "compact d \<Longrightarrow> finite_deflation (cast\<cdot>d)"
```
```   607 apply (drule alg_defl.compact_imp_principal, clarify)
```
```   608 apply (simp add: cast_alg_defl_principal)
```
```   609 apply (rule finite_deflation_Rep_fin_defl)
```
```   610 done
```
```   611
```
```   612 interpretation cast: deflation "cast\<cdot>d"
```
```   613 by (rule deflation_cast)
```
```   614
```
```   615 lemma cast_approx: "cast\<cdot>(approx n\<cdot>A) = defl_approx n (cast\<cdot>A)"
```
```   616 apply (rule alg_defl.principal_induct)
```
```   617 apply (rule adm_eq)
```
```   618 apply simp
```
```   619 apply (simp add: cont2cont_defl_approx cast.below)
```
```   620 apply (simp only: approx_alg_defl_principal)
```
```   621 apply (simp only: cast_alg_defl_principal)
```
```   622 apply (simp only: Rep_fin_defl_fd_take)
```
```   623 done
```
```   624
```
```   625 lemma cast_approx_fixed_iff:
```
```   626   "cast\<cdot>(approx i\<cdot>A)\<cdot>x = x \<longleftrightarrow> approx i\<cdot>x = x \<and> cast\<cdot>A\<cdot>x = x"
```
```   627 apply (simp only: cast_approx)
```
```   628 apply (rule defl_approx_fixed_iff)
```
```   629 apply (rule deflation_cast)
```
```   630 done
```
```   631
```
```   632 lemma defl_approx_cast: "defl_approx i (cast\<cdot>A) = cast\<cdot>(approx i\<cdot>A)"
```
```   633 by (rule cast_approx [symmetric])
```
```   634
```
```   635 lemma cast_below_imp_below: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<Longrightarrow> A \<sqsubseteq> B"
```
```   636 apply (rule profinite_below_ext)
```
```   637 apply (drule_tac i=i in defl_approx_below)
```
```   638 apply (rule deflation_cast)
```
```   639 apply (rule deflation_cast)
```
```   640 apply (simp only: defl_approx_cast)
```
```   641 apply (cut_tac x="approx i\<cdot>A" in alg_defl.compact_imp_principal)
```
```   642 apply (rule compact_approx)
```
```   643 apply (cut_tac x="approx i\<cdot>B" in alg_defl.compact_imp_principal)
```
```   644 apply (rule compact_approx)
```
```   645 apply clarsimp
```
```   646 apply (simp add: cast_alg_defl_principal)
```
```   647 apply (simp add: below_fin_defl_def)
```
```   648 done
```
```   649
```
```   650 lemma "cast\<cdot>(\<Squnion>i. alg_defl_principal (Abs_fin_defl (approx i)))\<cdot>x = x"
```
```   651 apply (subst contlub_cfun_arg)
```
```   652 apply (rule chainI)
```
```   653 apply (rule alg_defl.principal_mono)
```
```   654 apply (rule Abs_fin_defl_mono)
```
```   655 apply (rule finite_deflation_approx)
```
```   656 apply (rule finite_deflation_approx)
```
```   657 apply (rule chainE)
```
```   658 apply (rule chain_approx)
```
```   659 apply (simp add: cast_alg_defl_principal Abs_fin_defl_inverse finite_deflation_approx)
```
```   660 done
```
```   661
```
```   662 text {* This lemma says that if we have an ep-pair from
```
```   663 a bifinite domain into a universal domain, then e oo p
```
```   664 is an algebraic deflation. *}
```
```   665
```
```   666 lemma
```
```   667   assumes "ep_pair e p"
```
```   668   constrains e :: "'a::profinite \<rightarrow> 'b::profinite"
```
```   669   shows "\<exists>d. cast\<cdot>d = e oo p"
```
```   670 proof
```
```   671   interpret ep_pair e p by fact
```
```   672   let ?a = "\<lambda>i. e oo approx i oo p"
```
```   673   have a: "\<And>i. finite_deflation (?a i)"
```
```   674     apply (rule finite_deflation_e_d_p)
```
```   675     apply (rule finite_deflation_approx)
```
```   676     done
```
```   677   let ?d = "\<Squnion>i. alg_defl_principal (Abs_fin_defl (?a i))"
```
```   678   show "cast\<cdot>?d = e oo p"
```
```   679     apply (subst contlub_cfun_arg)
```
```   680     apply (rule chainI)
```
```   681     apply (rule alg_defl.principal_mono)
```
```   682     apply (rule Abs_fin_defl_mono [OF a a])
```
```   683     apply (rule chainE, simp)
```
```   684     apply (subst cast_alg_defl_principal)
```
```   685     apply (simp add: Abs_fin_defl_inverse a)
```
```   686     apply (simp add: expand_cfun_eq lub_distribs)
```
```   687     done
```
```   688 qed
```
```   689
```
```   690 text {* This lemma says that if we have an ep-pair
```
```   691 from a cpo into a bifinite domain, and e oo p is
```
```   692 an algebraic deflation, then the cpo is bifinite. *}
```
```   693
```
```   694 lemma
```
```   695   assumes "ep_pair e p"
```
```   696   constrains e :: "'a::cpo \<rightarrow> 'b::profinite"
```
```   697   assumes d: "\<And>x. cast\<cdot>d\<cdot>x = e\<cdot>(p\<cdot>x)"
```
```   698   obtains a :: "nat \<Rightarrow> 'a \<rightarrow> 'a" where
```
```   699     "\<And>i. finite_deflation (a i)"
```
```   700     "(\<Squnion>i. a i) = ID"
```
```   701 proof
```
```   702   interpret ep_pair e p by fact
```
```   703   let ?a = "\<lambda>i. p oo cast\<cdot>(approx i\<cdot>d) oo e"
```
```   704   show "\<And>i. finite_deflation (?a i)"
```
```   705     apply (rule finite_deflation_p_d_e)
```
```   706     apply (rule finite_deflation_cast)
```
```   707     apply (rule compact_approx)
```
```   708     apply (rule below_eq_trans [OF _ d])
```
```   709     apply (rule monofun_cfun_fun)
```
```   710     apply (rule monofun_cfun_arg)
```
```   711     apply (rule approx_below)
```
```   712     done
```
```   713   show "(\<Squnion>i. ?a i) = ID"
```
```   714     apply (rule ext_cfun, simp)
```
```   715     apply (simp add: lub_distribs)
```
```   716     apply (simp add: d)
```
```   717     done
```
```   718 qed
```
```   719
```
```   720 end
```