src/HOLCF/Algebraic.thy
 author huffman Mon May 11 08:28:09 2009 -0700 (2009-05-11) changeset 31095 b79d140f6d0b parent 31076 99fe356cbbc2 child 31164 f550c4cf3f3a permissions -rw-r--r--
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
```     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 text {* A pre-deflation is like a deflation, but not idempotent. *}
```
```    33
```
```    34 locale pre_deflation =
```
```    35   fixes f :: "'a \<rightarrow> 'a::cpo"
```
```    36   assumes below: "\<And>x. f\<cdot>x \<sqsubseteq> x"
```
```    37   assumes finite_range: "finite (range (\<lambda>x. f\<cdot>x))"
```
```    38 begin
```
```    39
```
```    40 lemma iterate_below: "iterate i\<cdot>f\<cdot>x \<sqsubseteq> x"
```
```    41 by (induct i, simp_all add: below_trans [OF below])
```
```    42
```
```    43 lemma iterate_fixed: "f\<cdot>x = x \<Longrightarrow> iterate i\<cdot>f\<cdot>x = x"
```
```    44 by (induct i, simp_all)
```
```    45
```
```    46 lemma antichain_iterate_app: "i \<le> j \<Longrightarrow> iterate j\<cdot>f\<cdot>x \<sqsubseteq> iterate i\<cdot>f\<cdot>x"
```
```    47 apply (erule le_Suc_induct)
```
```    48 apply (simp add: below)
```
```    49 apply (rule below_refl)
```
```    50 apply (erule (1) below_trans)
```
```    51 done
```
```    52
```
```    53 lemma finite_range_iterate_app: "finite (range (\<lambda>i. iterate i\<cdot>f\<cdot>x))"
```
```    54 proof (rule finite_subset)
```
```    55   show "range (\<lambda>i. iterate i\<cdot>f\<cdot>x) \<subseteq> insert x (range (\<lambda>x. f\<cdot>x))"
```
```    56     by (clarify, case_tac i, simp_all)
```
```    57   show "finite (insert x (range (\<lambda>x. f\<cdot>x)))"
```
```    58     by (simp add: finite_range)
```
```    59 qed
```
```    60
```
```    61 lemma eventually_constant_iterate_app:
```
```    62   "eventually_constant (\<lambda>i. iterate i\<cdot>f\<cdot>x)"
```
```    63 unfolding eventually_constant_def MOST_nat_le
```
```    64 proof -
```
```    65   let ?Y = "\<lambda>i. iterate i\<cdot>f\<cdot>x"
```
```    66   have "\<exists>j. \<forall>k. ?Y j \<sqsubseteq> ?Y k"
```
```    67     apply (rule finite_range_has_max)
```
```    68     apply (erule antichain_iterate_app)
```
```    69     apply (rule finite_range_iterate_app)
```
```    70     done
```
```    71   then obtain j where j: "\<And>k. ?Y j \<sqsubseteq> ?Y k" by fast
```
```    72   show "\<exists>z m. \<forall>n\<ge>m. ?Y n = z"
```
```    73   proof (intro exI allI impI)
```
```    74     fix k
```
```    75     assume "j \<le> k"
```
```    76     hence "?Y k \<sqsubseteq> ?Y j" by (rule antichain_iterate_app)
```
```    77     also have "?Y j \<sqsubseteq> ?Y k" by (rule j)
```
```    78     finally show "?Y k = ?Y j" .
```
```    79   qed
```
```    80 qed
```
```    81
```
```    82 lemma eventually_constant_iterate:
```
```    83   "eventually_constant (\<lambda>n. iterate n\<cdot>f)"
```
```    84 proof -
```
```    85   have "\<forall>y\<in>range (\<lambda>x. f\<cdot>x). eventually_constant (\<lambda>i. iterate i\<cdot>f\<cdot>y)"
```
```    86     by (simp add: eventually_constant_iterate_app)
```
```    87   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"
```
```    88     unfolding eventually_constant_MOST_MOST .
```
```    89   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"
```
```    90     by (simp only: MOST_finite_Ball_distrib [OF finite_range])
```
```    91   hence "MOST i. MOST j. \<forall>x. iterate j\<cdot>f\<cdot>(f\<cdot>x) = iterate i\<cdot>f\<cdot>(f\<cdot>x)"
```
```    92     by simp
```
```    93   hence "MOST i. MOST j. \<forall>x. iterate (Suc j)\<cdot>f\<cdot>x = iterate (Suc i)\<cdot>f\<cdot>x"
```
```    94     by (simp only: iterate_Suc2)
```
```    95   hence "MOST i. MOST j. iterate (Suc j)\<cdot>f = iterate (Suc i)\<cdot>f"
```
```    96     by (simp only: expand_cfun_eq)
```
```    97   hence "eventually_constant (\<lambda>i. iterate (Suc i)\<cdot>f)"
```
```    98     unfolding eventually_constant_MOST_MOST .
```
```    99   thus "eventually_constant (\<lambda>i. iterate i\<cdot>f)"
```
```   100     by (rule eventually_constant_SucD)
```
```   101 qed
```
```   102
```
```   103 abbreviation
```
```   104   d :: "'a \<rightarrow> 'a"
```
```   105 where
```
```   106   "d \<equiv> eventual (\<lambda>n. iterate n\<cdot>f)"
```
```   107
```
```   108 lemma MOST_d: "MOST n. P (iterate n\<cdot>f) \<Longrightarrow> P d"
```
```   109 using eventually_constant_iterate by (rule MOST_eventual)
```
```   110
```
```   111 lemma f_d: "f\<cdot>(d\<cdot>x) = d\<cdot>x"
```
```   112 apply (rule MOST_d)
```
```   113 apply (subst iterate_Suc [symmetric])
```
```   114 apply (rule eventually_constant_MOST_Suc_eq)
```
```   115 apply (rule eventually_constant_iterate_app)
```
```   116 done
```
```   117
```
```   118 lemma d_fixed_iff: "d\<cdot>x = x \<longleftrightarrow> f\<cdot>x = x"
```
```   119 proof
```
```   120   assume "d\<cdot>x = x"
```
```   121   with f_d [where x=x]
```
```   122   show "f\<cdot>x = x" by simp
```
```   123 next
```
```   124   assume f: "f\<cdot>x = x"
```
```   125   have "\<forall>n. iterate n\<cdot>f\<cdot>x = x"
```
```   126     by (rule allI, rule nat.induct, simp, simp add: f)
```
```   127   hence "MOST n. iterate n\<cdot>f\<cdot>x = x"
```
```   128     by (rule ALL_MOST)
```
```   129   thus "d\<cdot>x = x"
```
```   130     by (rule MOST_d)
```
```   131 qed
```
```   132
```
```   133 lemma finite_deflation_d: "finite_deflation d"
```
```   134 proof
```
```   135   fix x :: 'a
```
```   136   have "d \<in> range (\<lambda>n. iterate n\<cdot>f)"
```
```   137     using eventually_constant_iterate
```
```   138     by (rule eventual_mem_range)
```
```   139   then obtain n where n: "d = iterate n\<cdot>f" ..
```
```   140   have "iterate n\<cdot>f\<cdot>(d\<cdot>x) = d\<cdot>x"
```
```   141     using f_d by (rule iterate_fixed)
```
```   142   thus "d\<cdot>(d\<cdot>x) = d\<cdot>x"
```
```   143     by (simp add: n)
```
```   144 next
```
```   145   fix x :: 'a
```
```   146   show "d\<cdot>x \<sqsubseteq> x"
```
```   147     by (rule MOST_d, simp add: iterate_below)
```
```   148 next
```
```   149   from finite_range
```
```   150   have "finite {x. f\<cdot>x = x}"
```
```   151     by (rule finite_range_imp_finite_fixes)
```
```   152   thus "finite {x. d\<cdot>x = x}"
```
```   153     by (simp add: d_fixed_iff)
```
```   154 qed
```
```   155
```
```   156 end
```
```   157
```
```   158 lemma pre_deflation_d_f:
```
```   159   assumes "finite_deflation d"
```
```   160   assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
```
```   161   shows "pre_deflation (d oo f)"
```
```   162 proof
```
```   163   interpret d: finite_deflation d by fact
```
```   164   fix x
```
```   165   show "\<And>x. (d oo f)\<cdot>x \<sqsubseteq> x"
```
```   166     by (simp, rule below_trans [OF d.below f])
```
```   167   show "finite (range (\<lambda>x. (d oo f)\<cdot>x))"
```
```   168     by (rule finite_subset [OF _ d.finite_range], auto)
```
```   169 qed
```
```   170
```
```   171 lemma eventual_iterate_oo_fixed_iff:
```
```   172   assumes "finite_deflation d"
```
```   173   assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
```
```   174   shows "eventual (\<lambda>n. iterate n\<cdot>(d oo f))\<cdot>x = x \<longleftrightarrow> d\<cdot>x = x \<and> f\<cdot>x = x"
```
```   175 proof -
```
```   176   interpret d: finite_deflation d by fact
```
```   177   let ?e = "d oo f"
```
```   178   interpret e: pre_deflation "d oo f"
```
```   179     using `finite_deflation d` f
```
```   180     by (rule pre_deflation_d_f)
```
```   181   let ?g = "eventual (\<lambda>n. iterate n\<cdot>?e)"
```
```   182   show ?thesis
```
```   183     apply (subst e.d_fixed_iff)
```
```   184     apply simp
```
```   185     apply safe
```
```   186     apply (erule subst)
```
```   187     apply (rule d.idem)
```
```   188     apply (rule below_antisym)
```
```   189     apply (rule f)
```
```   190     apply (erule subst, rule d.below)
```
```   191     apply simp
```
```   192     done
```
```   193 qed
```
```   194
```
```   195 subsection {* Type constructor for finite deflations *}
```
```   196
```
```   197 defaultsort profinite
```
```   198
```
```   199 typedef (open) 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
```
```   200 by (fast intro: finite_deflation_approx)
```
```   201
```
```   202 instantiation fin_defl :: (profinite) below
```
```   203 begin
```
```   204
```
```   205 definition below_fin_defl_def:
```
```   206     "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep_fin_defl x \<sqsubseteq> Rep_fin_defl y"
```
```   207
```
```   208 instance ..
```
```   209 end
```
```   210
```
```   211 instance fin_defl :: (profinite) po
```
```   212 by (rule typedef_po [OF type_definition_fin_defl below_fin_defl_def])
```
```   213
```
```   214 lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)"
```
```   215 using Rep_fin_defl by simp
```
```   216
```
```   217 interpretation Rep_fin_defl: finite_deflation "Rep_fin_defl d"
```
```   218 by (rule finite_deflation_Rep_fin_defl)
```
```   219
```
```   220 lemma fin_defl_belowI:
```
```   221   "(\<And>x. Rep_fin_defl a\<cdot>x = x \<Longrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a \<sqsubseteq> b"
```
```   222 unfolding below_fin_defl_def
```
```   223 by (rule Rep_fin_defl.belowI)
```
```   224
```
```   225 lemma fin_defl_belowD:
```
```   226   "\<lbrakk>a \<sqsubseteq> b; Rep_fin_defl a\<cdot>x = x\<rbrakk> \<Longrightarrow> Rep_fin_defl b\<cdot>x = x"
```
```   227 unfolding below_fin_defl_def
```
```   228 by (rule Rep_fin_defl.belowD)
```
```   229
```
```   230 lemma fin_defl_eqI:
```
```   231   "(\<And>x. Rep_fin_defl a\<cdot>x = x \<longleftrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a = b"
```
```   232 apply (rule below_antisym)
```
```   233 apply (rule fin_defl_belowI, simp)
```
```   234 apply (rule fin_defl_belowI, simp)
```
```   235 done
```
```   236
```
```   237 lemma Abs_fin_defl_mono:
```
```   238   "\<lbrakk>finite_deflation a; finite_deflation b; a \<sqsubseteq> b\<rbrakk>
```
```   239     \<Longrightarrow> Abs_fin_defl a \<sqsubseteq> Abs_fin_defl b"
```
```   240 unfolding below_fin_defl_def
```
```   241 by (simp add: Abs_fin_defl_inverse)
```
```   242
```
```   243
```
```   244 subsection {* Take function for finite deflations *}
```
```   245
```
```   246 definition
```
```   247   fd_take :: "nat \<Rightarrow> 'a fin_defl \<Rightarrow> 'a fin_defl"
```
```   248 where
```
```   249   "fd_take i d = Abs_fin_defl (eventual (\<lambda>n. iterate n\<cdot>(approx i oo Rep_fin_defl d)))"
```
```   250
```
```   251 lemma Rep_fin_defl_fd_take:
```
```   252   "Rep_fin_defl (fd_take i d) =
```
```   253     eventual (\<lambda>n. iterate n\<cdot>(approx i oo Rep_fin_defl d))"
```
```   254 unfolding fd_take_def
```
```   255 apply (rule Abs_fin_defl_inverse [unfolded mem_Collect_eq])
```
```   256 apply (rule pre_deflation.finite_deflation_d)
```
```   257 apply (rule pre_deflation_d_f)
```
```   258 apply (rule finite_deflation_approx)
```
```   259 apply (rule Rep_fin_defl.below)
```
```   260 done
```
```   261
```
```   262 lemma fd_take_fixed_iff:
```
```   263   "Rep_fin_defl (fd_take i d)\<cdot>x = x \<longleftrightarrow>
```
```   264     approx i\<cdot>x = x \<and> Rep_fin_defl d\<cdot>x = x"
```
```   265 unfolding Rep_fin_defl_fd_take
```
```   266 by (rule eventual_iterate_oo_fixed_iff
```
```   267     [OF finite_deflation_approx Rep_fin_defl.below])
```
```   268
```
```   269 lemma fd_take_below: "fd_take n d \<sqsubseteq> d"
```
```   270 apply (rule fin_defl_belowI)
```
```   271 apply (simp add: fd_take_fixed_iff)
```
```   272 done
```
```   273
```
```   274 lemma fd_take_idem: "fd_take n (fd_take n d) = fd_take n d"
```
```   275 apply (rule fin_defl_eqI)
```
```   276 apply (simp add: fd_take_fixed_iff)
```
```   277 done
```
```   278
```
```   279 lemma fd_take_mono: "a \<sqsubseteq> b \<Longrightarrow> fd_take n a \<sqsubseteq> fd_take n b"
```
```   280 apply (rule fin_defl_belowI)
```
```   281 apply (simp add: fd_take_fixed_iff)
```
```   282 apply (simp add: fin_defl_belowD)
```
```   283 done
```
```   284
```
```   285 lemma approx_fixed_le_lemma: "\<lbrakk>i \<le> j; approx i\<cdot>x = x\<rbrakk> \<Longrightarrow> approx j\<cdot>x = x"
```
```   286 by (erule subst, simp add: min_def)
```
```   287
```
```   288 lemma fd_take_chain: "m \<le> n \<Longrightarrow> fd_take m a \<sqsubseteq> fd_take n a"
```
```   289 apply (rule fin_defl_belowI)
```
```   290 apply (simp add: fd_take_fixed_iff)
```
```   291 apply (simp add: approx_fixed_le_lemma)
```
```   292 done
```
```   293
```
```   294 lemma finite_range_fd_take: "finite (range (fd_take n))"
```
```   295 apply (rule finite_imageD [where f="\<lambda>a. {x. Rep_fin_defl a\<cdot>x = x}"])
```
```   296 apply (rule finite_subset [where B="Pow {x. approx n\<cdot>x = x}"])
```
```   297 apply (clarify, simp add: fd_take_fixed_iff)
```
```   298 apply (simp add: finite_fixes_approx)
```
```   299 apply (rule inj_onI, clarify)
```
```   300 apply (simp add: expand_set_eq fin_defl_eqI)
```
```   301 done
```
```   302
```
```   303 lemma fd_take_covers: "\<exists>n. fd_take n a = a"
```
```   304 apply (rule_tac x=
```
```   305   "Max ((\<lambda>x. LEAST n. approx n\<cdot>x = x) ` {x. Rep_fin_defl a\<cdot>x = x})" in exI)
```
```   306 apply (rule below_antisym)
```
```   307 apply (rule fd_take_below)
```
```   308 apply (rule fin_defl_belowI)
```
```   309 apply (simp add: fd_take_fixed_iff)
```
```   310 apply (rule approx_fixed_le_lemma)
```
```   311 apply (rule Max_ge)
```
```   312 apply (rule finite_imageI)
```
```   313 apply (rule Rep_fin_defl.finite_fixes)
```
```   314 apply (rule imageI)
```
```   315 apply (erule CollectI)
```
```   316 apply (rule LeastI_ex)
```
```   317 apply (rule profinite_compact_eq_approx)
```
```   318 apply (erule subst)
```
```   319 apply (rule Rep_fin_defl.compact)
```
```   320 done
```
```   321
```
```   322 interpretation fin_defl: basis_take below fd_take
```
```   323 apply default
```
```   324 apply (rule fd_take_below)
```
```   325 apply (rule fd_take_idem)
```
```   326 apply (erule fd_take_mono)
```
```   327 apply (rule fd_take_chain, simp)
```
```   328 apply (rule finite_range_fd_take)
```
```   329 apply (rule fd_take_covers)
```
```   330 done
```
```   331
```
```   332 subsection {* Defining algebraic deflations by ideal completion *}
```
```   333
```
```   334 typedef (open) 'a alg_defl =
```
```   335   "{S::'a fin_defl set. below.ideal S}"
```
```   336 by (fast intro: below.ideal_principal)
```
```   337
```
```   338 instantiation alg_defl :: (profinite) below
```
```   339 begin
```
```   340
```
```   341 definition
```
```   342   "x \<sqsubseteq> y \<longleftrightarrow> Rep_alg_defl x \<subseteq> Rep_alg_defl y"
```
```   343
```
```   344 instance ..
```
```   345 end
```
```   346
```
```   347 instance alg_defl :: (profinite) po
```
```   348 by (rule below.typedef_ideal_po
```
```   349     [OF type_definition_alg_defl below_alg_defl_def])
```
```   350
```
```   351 instance alg_defl :: (profinite) cpo
```
```   352 by (rule below.typedef_ideal_cpo
```
```   353     [OF type_definition_alg_defl below_alg_defl_def])
```
```   354
```
```   355 lemma Rep_alg_defl_lub:
```
```   356   "chain Y \<Longrightarrow> Rep_alg_defl (\<Squnion>i. Y i) = (\<Union>i. Rep_alg_defl (Y i))"
```
```   357 by (rule below.typedef_ideal_rep_contlub
```
```   358     [OF type_definition_alg_defl below_alg_defl_def])
```
```   359
```
```   360 lemma ideal_Rep_alg_defl: "below.ideal (Rep_alg_defl xs)"
```
```   361 by (rule Rep_alg_defl [unfolded mem_Collect_eq])
```
```   362
```
```   363 definition
```
```   364   alg_defl_principal :: "'a fin_defl \<Rightarrow> 'a alg_defl" where
```
```   365   "alg_defl_principal t = Abs_alg_defl {u. u \<sqsubseteq> t}"
```
```   366
```
```   367 lemma Rep_alg_defl_principal:
```
```   368   "Rep_alg_defl (alg_defl_principal t) = {u. u \<sqsubseteq> t}"
```
```   369 unfolding alg_defl_principal_def
```
```   370 by (simp add: Abs_alg_defl_inverse below.ideal_principal)
```
```   371
```
```   372 interpretation alg_defl:
```
```   373   ideal_completion below fd_take alg_defl_principal Rep_alg_defl
```
```   374 apply default
```
```   375 apply (rule ideal_Rep_alg_defl)
```
```   376 apply (erule Rep_alg_defl_lub)
```
```   377 apply (rule Rep_alg_defl_principal)
```
```   378 apply (simp only: below_alg_defl_def)
```
```   379 done
```
```   380
```
```   381 text {* Algebraic deflations are pointed *}
```
```   382
```
```   383 lemma finite_deflation_UU: "finite_deflation \<bottom>"
```
```   384 by default simp_all
```
```   385
```
```   386 lemma alg_defl_minimal:
```
```   387   "alg_defl_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x"
```
```   388 apply (induct x rule: alg_defl.principal_induct, simp)
```
```   389 apply (rule alg_defl.principal_mono)
```
```   390 apply (induct_tac a)
```
```   391 apply (rule Abs_fin_defl_mono)
```
```   392 apply (rule finite_deflation_UU)
```
```   393 apply simp
```
```   394 apply (rule minimal)
```
```   395 done
```
```   396
```
```   397 instance alg_defl :: (bifinite) pcpo
```
```   398 by intro_classes (fast intro: alg_defl_minimal)
```
```   399
```
```   400 lemma inst_alg_defl_pcpo: "\<bottom> = alg_defl_principal (Abs_fin_defl \<bottom>)"
```
```   401 by (rule alg_defl_minimal [THEN UU_I, symmetric])
```
```   402
```
```   403 text {* Algebraic deflations are profinite *}
```
```   404
```
```   405 instantiation alg_defl :: (profinite) profinite
```
```   406 begin
```
```   407
```
```   408 definition
```
```   409   approx_alg_defl_def: "approx = alg_defl.completion_approx"
```
```   410
```
```   411 instance
```
```   412 apply (intro_classes, unfold approx_alg_defl_def)
```
```   413 apply (rule alg_defl.chain_completion_approx)
```
```   414 apply (rule alg_defl.lub_completion_approx)
```
```   415 apply (rule alg_defl.completion_approx_idem)
```
```   416 apply (rule alg_defl.finite_fixes_completion_approx)
```
```   417 done
```
```   418
```
```   419 end
```
```   420
```
```   421 instance alg_defl :: (bifinite) bifinite ..
```
```   422
```
```   423 lemma approx_alg_defl_principal [simp]:
```
```   424   "approx n\<cdot>(alg_defl_principal t) = alg_defl_principal (fd_take n t)"
```
```   425 unfolding approx_alg_defl_def
```
```   426 by (rule alg_defl.completion_approx_principal)
```
```   427
```
```   428 lemma approx_eq_alg_defl_principal:
```
```   429   "\<exists>t\<in>Rep_alg_defl xs. approx n\<cdot>xs = alg_defl_principal (fd_take n t)"
```
```   430 unfolding approx_alg_defl_def
```
```   431 by (rule alg_defl.completion_approx_eq_principal)
```
```   432
```
```   433
```
```   434 subsection {* Applying algebraic deflations *}
```
```   435
```
```   436 definition
```
```   437   cast :: "'a alg_defl \<rightarrow> 'a \<rightarrow> 'a"
```
```   438 where
```
```   439   "cast = alg_defl.basis_fun Rep_fin_defl"
```
```   440
```
```   441 lemma cast_alg_defl_principal:
```
```   442   "cast\<cdot>(alg_defl_principal a) = Rep_fin_defl a"
```
```   443 unfolding cast_def
```
```   444 apply (rule alg_defl.basis_fun_principal)
```
```   445 apply (simp only: below_fin_defl_def)
```
```   446 done
```
```   447
```
```   448 lemma deflation_cast: "deflation (cast\<cdot>d)"
```
```   449 apply (induct d rule: alg_defl.principal_induct)
```
```   450 apply (rule adm_subst [OF _ adm_deflation], simp)
```
```   451 apply (simp add: cast_alg_defl_principal)
```
```   452 apply (rule finite_deflation_imp_deflation)
```
```   453 apply (rule finite_deflation_Rep_fin_defl)
```
```   454 done
```
```   455
```
```   456 lemma finite_deflation_cast:
```
```   457   "compact d \<Longrightarrow> finite_deflation (cast\<cdot>d)"
```
```   458 apply (drule alg_defl.compact_imp_principal, clarify)
```
```   459 apply (simp add: cast_alg_defl_principal)
```
```   460 apply (rule finite_deflation_Rep_fin_defl)
```
```   461 done
```
```   462
```
```   463 interpretation cast: deflation "cast\<cdot>d"
```
```   464 by (rule deflation_cast)
```
```   465
```
```   466 lemma "cast\<cdot>(\<Squnion>i. alg_defl_principal (Abs_fin_defl (approx i)))\<cdot>x = x"
```
```   467 apply (subst contlub_cfun_arg)
```
```   468 apply (rule chainI)
```
```   469 apply (rule alg_defl.principal_mono)
```
```   470 apply (rule Abs_fin_defl_mono)
```
```   471 apply (rule finite_deflation_approx)
```
```   472 apply (rule finite_deflation_approx)
```
```   473 apply (rule chainE)
```
```   474 apply (rule chain_approx)
```
```   475 apply (simp add: cast_alg_defl_principal Abs_fin_defl_inverse finite_deflation_approx)
```
```   476 done
```
```   477
```
```   478 text {* This lemma says that if we have an ep-pair from
```
```   479 a bifinite domain into a universal domain, then e oo p
```
```   480 is an algebraic deflation. *}
```
```   481
```
```   482 lemma
```
```   483   assumes "ep_pair e p"
```
```   484   constrains e :: "'a::profinite \<rightarrow> 'b::profinite"
```
```   485   shows "\<exists>d. cast\<cdot>d = e oo p"
```
```   486 proof
```
```   487   interpret ep_pair e p by fact
```
```   488   let ?a = "\<lambda>i. e oo approx i oo p"
```
```   489   have a: "\<And>i. finite_deflation (?a i)"
```
```   490     apply (rule finite_deflation_e_d_p)
```
```   491     apply (rule finite_deflation_approx)
```
```   492     done
```
```   493   let ?d = "\<Squnion>i. alg_defl_principal (Abs_fin_defl (?a i))"
```
```   494   show "cast\<cdot>?d = e oo p"
```
```   495     apply (subst contlub_cfun_arg)
```
```   496     apply (rule chainI)
```
```   497     apply (rule alg_defl.principal_mono)
```
```   498     apply (rule Abs_fin_defl_mono [OF a a])
```
```   499     apply (rule chainE, simp)
```
```   500     apply (subst cast_alg_defl_principal)
```
```   501     apply (simp add: Abs_fin_defl_inverse a)
```
```   502     apply (simp add: expand_cfun_eq lub_distribs)
```
```   503     done
```
```   504 qed
```
```   505
```
```   506 text {* This lemma says that if we have an ep-pair
```
```   507 from a cpo into a bifinite domain, and e oo p is
```
```   508 an algebraic deflation, then the cpo is bifinite. *}
```
```   509
```
```   510 lemma
```
```   511   assumes "ep_pair e p"
```
```   512   constrains e :: "'a::cpo \<rightarrow> 'b::profinite"
```
```   513   assumes d: "\<And>x. cast\<cdot>d\<cdot>x = e\<cdot>(p\<cdot>x)"
```
```   514   obtains a :: "nat \<Rightarrow> 'a \<rightarrow> 'a" where
```
```   515     "\<And>i. finite_deflation (a i)"
```
```   516     "(\<Squnion>i. a i) = ID"
```
```   517 proof
```
```   518   interpret ep_pair e p by fact
```
```   519   let ?a = "\<lambda>i. p oo cast\<cdot>(approx i\<cdot>d) oo e"
```
```   520   show "\<And>i. finite_deflation (?a i)"
```
```   521     apply (rule finite_deflation_p_d_e)
```
```   522     apply (rule finite_deflation_cast)
```
```   523     apply (rule compact_approx)
```
```   524     apply (rule below_eq_trans [OF _ d])
```
```   525     apply (rule monofun_cfun_fun)
```
```   526     apply (rule monofun_cfun_arg)
```
```   527     apply (rule approx_below)
```
```   528     done
```
```   529   show "(\<Squnion>i. ?a i) = ID"
```
```   530     apply (rule ext_cfun, simp)
```
```   531     apply (simp add: lub_distribs)
```
```   532     apply (simp add: d)
```
```   533     done
```
```   534 qed
```
```   535
```
```   536 end
```