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