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