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