src/HOLCF/Library/Defl_Bifinite.thy
author huffman
Tue Nov 09 16:37:13 2010 -0800 (2010-11-09)
changeset 40491 6de5839e2fb3
parent 40002 c5b5f7a3a3b1
child 40494 db8a09daba7b
permissions -rw-r--r--
add 'predomain' class: unpointed version of bifinite
huffman@39999
     1
(*  Title:      HOLCF/Library/Defl_Bifinite.thy
huffman@39999
     2
    Author:     Brian Huffman
huffman@39999
     3
*)
huffman@39999
     4
huffman@39999
     5
header {* Algebraic deflations are a bifinite domain *}
huffman@39999
     6
huffman@39999
     7
theory Defl_Bifinite
huffman@39999
     8
imports HOLCF Infinite_Set
huffman@39999
     9
begin
huffman@39999
    10
huffman@39999
    11
subsection {* Lemmas about MOST *}
huffman@39999
    12
huffman@39999
    13
default_sort type
huffman@39999
    14
huffman@39999
    15
lemma MOST_INFM:
huffman@39999
    16
  assumes inf: "infinite (UNIV::'a set)"
huffman@39999
    17
  shows "MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x"
huffman@39999
    18
  unfolding Alm_all_def Inf_many_def
huffman@39999
    19
  apply (auto simp add: Collect_neg_eq)
huffman@39999
    20
  apply (drule (1) finite_UnI)
huffman@39999
    21
  apply (simp add: Compl_partition2 inf)
huffman@39999
    22
  done
huffman@39999
    23
huffman@39999
    24
lemma MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
huffman@39999
    25
by (rule MOST_inj [OF _ inj_Suc])
huffman@39999
    26
huffman@39999
    27
lemma MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
huffman@39999
    28
unfolding MOST_nat
huffman@39999
    29
apply (clarify, rule_tac x="Suc m" in exI, clarify)
huffman@39999
    30
apply (erule Suc_lessE, simp)
huffman@39999
    31
done
huffman@39999
    32
huffman@39999
    33
lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
huffman@39999
    34
by (rule iffI [OF MOST_SucD MOST_SucI])
huffman@39999
    35
huffman@39999
    36
lemma INFM_finite_Bex_distrib:
huffman@39999
    37
  "finite A \<Longrightarrow> (INFM y. \<exists>x\<in>A. P x y) \<longleftrightarrow> (\<exists>x\<in>A. INFM y. P x y)"
huffman@39999
    38
by (induct set: finite, simp, simp add: INFM_disj_distrib)
huffman@39999
    39
huffman@39999
    40
lemma MOST_finite_Ball_distrib:
huffman@39999
    41
  "finite A \<Longrightarrow> (MOST y. \<forall>x\<in>A. P x y) \<longleftrightarrow> (\<forall>x\<in>A. MOST y. P x y)"
huffman@39999
    42
by (induct set: finite, simp, simp add: MOST_conj_distrib)
huffman@39999
    43
huffman@39999
    44
lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
huffman@39999
    45
unfolding MOST_nat_le by fast
huffman@39999
    46
huffman@39999
    47
subsection {* Eventually constant sequences *}
huffman@39999
    48
huffman@39999
    49
definition
huffman@39999
    50
  eventually_constant :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool"
huffman@39999
    51
where
huffman@39999
    52
  "eventually_constant S = (\<exists>x. MOST i. S i = x)"
huffman@39999
    53
huffman@39999
    54
lemma eventually_constant_MOST_MOST:
huffman@39999
    55
  "eventually_constant S \<longleftrightarrow> (MOST m. MOST n. S n = S m)"
huffman@39999
    56
unfolding eventually_constant_def MOST_nat
huffman@39999
    57
apply safe
huffman@39999
    58
apply (rule_tac x=m in exI, clarify)
huffman@39999
    59
apply (rule_tac x=m in exI, clarify)
huffman@39999
    60
apply simp
huffman@39999
    61
apply fast
huffman@39999
    62
done
huffman@39999
    63
huffman@39999
    64
lemma eventually_constantI: "MOST i. S i = x \<Longrightarrow> eventually_constant S"
huffman@39999
    65
unfolding eventually_constant_def by fast
huffman@39999
    66
huffman@39999
    67
lemma eventually_constant_comp:
huffman@39999
    68
  "eventually_constant (\<lambda>i. S i) \<Longrightarrow> eventually_constant (\<lambda>i. f (S i))"
huffman@39999
    69
unfolding eventually_constant_def
huffman@39999
    70
apply (erule exE, rule_tac x="f x" in exI)
huffman@39999
    71
apply (erule MOST_mono, simp)
huffman@39999
    72
done
huffman@39999
    73
huffman@39999
    74
lemma eventually_constant_Suc_iff:
huffman@39999
    75
  "eventually_constant (\<lambda>i. S (Suc i)) \<longleftrightarrow> eventually_constant (\<lambda>i. S i)"
huffman@39999
    76
unfolding eventually_constant_def
huffman@39999
    77
by (subst MOST_Suc_iff, rule refl)
huffman@39999
    78
huffman@39999
    79
lemma eventually_constant_SucD:
huffman@39999
    80
  "eventually_constant (\<lambda>i. S (Suc i)) \<Longrightarrow> eventually_constant (\<lambda>i. S i)"
huffman@39999
    81
by (rule eventually_constant_Suc_iff [THEN iffD1])
huffman@39999
    82
huffman@39999
    83
subsection {* Limits of eventually constant sequences *}
huffman@39999
    84
huffman@39999
    85
definition
huffman@39999
    86
  eventual :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a" where
huffman@39999
    87
  "eventual S = (THE x. MOST i. S i = x)"
huffman@39999
    88
huffman@39999
    89
lemma eventual_eqI: "MOST i. S i = x \<Longrightarrow> eventual S = x"
huffman@39999
    90
unfolding eventual_def
huffman@39999
    91
apply (rule the_equality, assumption)
huffman@39999
    92
apply (rename_tac y)
huffman@39999
    93
apply (subgoal_tac "MOST i::nat. y = x", simp)
huffman@39999
    94
apply (erule MOST_rev_mp)
huffman@39999
    95
apply (erule MOST_rev_mp)
huffman@39999
    96
apply simp
huffman@39999
    97
done
huffman@39999
    98
huffman@39999
    99
lemma MOST_eq_eventual:
huffman@39999
   100
  "eventually_constant S \<Longrightarrow> MOST i. S i = eventual S"
huffman@39999
   101
unfolding eventually_constant_def
huffman@39999
   102
by (erule exE, simp add: eventual_eqI)
huffman@39999
   103
huffman@39999
   104
lemma eventual_mem_range:
huffman@39999
   105
  "eventually_constant S \<Longrightarrow> eventual S \<in> range S"
huffman@39999
   106
apply (drule MOST_eq_eventual)
huffman@39999
   107
apply (simp only: MOST_nat_le, clarify)
huffman@39999
   108
apply (drule spec, drule mp, rule order_refl)
huffman@39999
   109
apply (erule range_eqI [OF sym])
huffman@39999
   110
done
huffman@39999
   111
huffman@39999
   112
lemma eventually_constant_MOST_iff:
huffman@39999
   113
  assumes S: "eventually_constant S"
huffman@39999
   114
  shows "(MOST n. P (S n)) \<longleftrightarrow> P (eventual S)"
huffman@39999
   115
apply (subgoal_tac "(MOST n. P (S n)) \<longleftrightarrow> (MOST n::nat. P (eventual S))")
huffman@39999
   116
apply simp
huffman@39999
   117
apply (rule iffI)
huffman@39999
   118
apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]])
huffman@39999
   119
apply (erule MOST_mono, force)
huffman@39999
   120
apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]])
huffman@39999
   121
apply (erule MOST_mono, simp)
huffman@39999
   122
done
huffman@39999
   123
huffman@39999
   124
lemma MOST_eventual:
huffman@39999
   125
  "\<lbrakk>eventually_constant S; MOST n. P (S n)\<rbrakk> \<Longrightarrow> P (eventual S)"
huffman@39999
   126
proof -
huffman@39999
   127
  assume "eventually_constant S"
huffman@39999
   128
  hence "MOST n. S n = eventual S"
huffman@39999
   129
    by (rule MOST_eq_eventual)
huffman@39999
   130
  moreover assume "MOST n. P (S n)"
huffman@39999
   131
  ultimately have "MOST n. S n = eventual S \<and> P (S n)"
huffman@39999
   132
    by (rule MOST_conj_distrib [THEN iffD2, OF conjI])
huffman@39999
   133
  hence "MOST n::nat. P (eventual S)"
huffman@39999
   134
    by (rule MOST_mono) auto
huffman@39999
   135
  thus ?thesis by simp
huffman@39999
   136
qed
huffman@39999
   137
huffman@39999
   138
lemma eventually_constant_MOST_Suc_eq:
huffman@39999
   139
  "eventually_constant S \<Longrightarrow> MOST n. S (Suc n) = S n"
huffman@39999
   140
apply (drule MOST_eq_eventual)
huffman@39999
   141
apply (frule MOST_Suc_iff [THEN iffD2])
huffman@39999
   142
apply (erule MOST_rev_mp)
huffman@39999
   143
apply (erule MOST_rev_mp)
huffman@39999
   144
apply simp
huffman@39999
   145
done
huffman@39999
   146
huffman@39999
   147
lemma eventual_comp:
huffman@39999
   148
  "eventually_constant S \<Longrightarrow> eventual (\<lambda>i. f (S i)) = f (eventual (\<lambda>i. S i))"
huffman@39999
   149
apply (rule eventual_eqI)
huffman@39999
   150
apply (rule MOST_mono)
huffman@39999
   151
apply (erule MOST_eq_eventual)
huffman@39999
   152
apply simp
huffman@39999
   153
done
huffman@39999
   154
huffman@39999
   155
subsection {* Constructing finite deflations by iteration *}
huffman@39999
   156
huffman@39999
   157
default_sort cpo
huffman@39999
   158
huffman@39999
   159
lemma le_Suc_induct:
huffman@39999
   160
  assumes le: "i \<le> j"
huffman@39999
   161
  assumes step: "\<And>i. P i (Suc i)"
huffman@39999
   162
  assumes refl: "\<And>i. P i i"
huffman@39999
   163
  assumes trans: "\<And>i j k. \<lbrakk>P i j; P j k\<rbrakk> \<Longrightarrow> P i k"
huffman@39999
   164
  shows "P i j"
huffman@39999
   165
proof (cases "i = j")
huffman@39999
   166
  assume "i = j"
huffman@39999
   167
  thus "P i j" by (simp add: refl)
huffman@39999
   168
next
huffman@39999
   169
  assume "i \<noteq> j"
huffman@39999
   170
  with le have "i < j" by simp
huffman@39999
   171
  thus "P i j" using step trans by (rule less_Suc_induct)
huffman@39999
   172
qed
huffman@39999
   173
huffman@39999
   174
definition
huffman@39999
   175
  eventual_iterate :: "('a \<rightarrow> 'a::cpo) \<Rightarrow> ('a \<rightarrow> 'a)"
huffman@39999
   176
where
huffman@39999
   177
  "eventual_iterate f = eventual (\<lambda>n. iterate n\<cdot>f)"
huffman@39999
   178
huffman@39999
   179
text {* A pre-deflation is like a deflation, but not idempotent. *}
huffman@39999
   180
huffman@39999
   181
locale pre_deflation =
huffman@39999
   182
  fixes f :: "'a \<rightarrow> 'a::cpo"
huffman@39999
   183
  assumes below: "\<And>x. f\<cdot>x \<sqsubseteq> x"
huffman@39999
   184
  assumes finite_range: "finite (range (\<lambda>x. f\<cdot>x))"
huffman@39999
   185
begin
huffman@39999
   186
huffman@39999
   187
lemma iterate_below: "iterate i\<cdot>f\<cdot>x \<sqsubseteq> x"
huffman@39999
   188
by (induct i, simp_all add: below_trans [OF below])
huffman@39999
   189
huffman@39999
   190
lemma iterate_fixed: "f\<cdot>x = x \<Longrightarrow> iterate i\<cdot>f\<cdot>x = x"
huffman@39999
   191
by (induct i, simp_all)
huffman@39999
   192
huffman@39999
   193
lemma antichain_iterate_app: "i \<le> j \<Longrightarrow> iterate j\<cdot>f\<cdot>x \<sqsubseteq> iterate i\<cdot>f\<cdot>x"
huffman@39999
   194
apply (erule le_Suc_induct)
huffman@39999
   195
apply (simp add: below)
huffman@39999
   196
apply (rule below_refl)
huffman@39999
   197
apply (erule (1) below_trans)
huffman@39999
   198
done
huffman@39999
   199
huffman@39999
   200
lemma finite_range_iterate_app: "finite (range (\<lambda>i. iterate i\<cdot>f\<cdot>x))"
huffman@39999
   201
proof (rule finite_subset)
huffman@39999
   202
  show "range (\<lambda>i. iterate i\<cdot>f\<cdot>x) \<subseteq> insert x (range (\<lambda>x. f\<cdot>x))"
huffman@39999
   203
    by (clarify, case_tac i, simp_all)
huffman@39999
   204
  show "finite (insert x (range (\<lambda>x. f\<cdot>x)))"
huffman@39999
   205
    by (simp add: finite_range)
huffman@39999
   206
qed
huffman@39999
   207
huffman@39999
   208
lemma eventually_constant_iterate_app:
huffman@39999
   209
  "eventually_constant (\<lambda>i. iterate i\<cdot>f\<cdot>x)"
huffman@39999
   210
unfolding eventually_constant_def MOST_nat_le
huffman@39999
   211
proof -
huffman@39999
   212
  let ?Y = "\<lambda>i. iterate i\<cdot>f\<cdot>x"
huffman@39999
   213
  have "\<exists>j. \<forall>k. ?Y j \<sqsubseteq> ?Y k"
huffman@39999
   214
    apply (rule finite_range_has_max)
huffman@39999
   215
    apply (erule antichain_iterate_app)
huffman@39999
   216
    apply (rule finite_range_iterate_app)
huffman@39999
   217
    done
huffman@39999
   218
  then obtain j where j: "\<And>k. ?Y j \<sqsubseteq> ?Y k" by fast
huffman@39999
   219
  show "\<exists>z m. \<forall>n\<ge>m. ?Y n = z"
huffman@39999
   220
  proof (intro exI allI impI)
huffman@39999
   221
    fix k
huffman@39999
   222
    assume "j \<le> k"
huffman@39999
   223
    hence "?Y k \<sqsubseteq> ?Y j" by (rule antichain_iterate_app)
huffman@39999
   224
    also have "?Y j \<sqsubseteq> ?Y k" by (rule j)
huffman@39999
   225
    finally show "?Y k = ?Y j" .
huffman@39999
   226
  qed
huffman@39999
   227
qed
huffman@39999
   228
huffman@39999
   229
lemma eventually_constant_iterate:
huffman@39999
   230
  "eventually_constant (\<lambda>n. iterate n\<cdot>f)"
huffman@39999
   231
proof -
huffman@39999
   232
  have "\<forall>y\<in>range (\<lambda>x. f\<cdot>x). eventually_constant (\<lambda>i. iterate i\<cdot>f\<cdot>y)"
huffman@39999
   233
    by (simp add: eventually_constant_iterate_app)
huffman@39999
   234
  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@39999
   235
    unfolding eventually_constant_MOST_MOST .
huffman@39999
   236
  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@39999
   237
    by (simp only: MOST_finite_Ball_distrib [OF finite_range])
huffman@39999
   238
  hence "MOST i. MOST j. \<forall>x. iterate j\<cdot>f\<cdot>(f\<cdot>x) = iterate i\<cdot>f\<cdot>(f\<cdot>x)"
huffman@39999
   239
    by simp
huffman@39999
   240
  hence "MOST i. MOST j. \<forall>x. iterate (Suc j)\<cdot>f\<cdot>x = iterate (Suc i)\<cdot>f\<cdot>x"
huffman@39999
   241
    by (simp only: iterate_Suc2)
huffman@39999
   242
  hence "MOST i. MOST j. iterate (Suc j)\<cdot>f = iterate (Suc i)\<cdot>f"
huffman@40002
   243
    by (simp only: cfun_eq_iff)
huffman@39999
   244
  hence "eventually_constant (\<lambda>i. iterate (Suc i)\<cdot>f)"
huffman@39999
   245
    unfolding eventually_constant_MOST_MOST .
huffman@39999
   246
  thus "eventually_constant (\<lambda>i. iterate i\<cdot>f)"
huffman@39999
   247
    by (rule eventually_constant_SucD)
huffman@39999
   248
qed
huffman@39999
   249
huffman@39999
   250
abbreviation
huffman@39999
   251
  d :: "'a \<rightarrow> 'a"
huffman@39999
   252
where
huffman@39999
   253
  "d \<equiv> eventual_iterate f"
huffman@39999
   254
huffman@39999
   255
lemma MOST_d: "MOST n. P (iterate n\<cdot>f) \<Longrightarrow> P d"
huffman@39999
   256
unfolding eventual_iterate_def
huffman@39999
   257
using eventually_constant_iterate by (rule MOST_eventual)
huffman@39999
   258
huffman@39999
   259
lemma f_d: "f\<cdot>(d\<cdot>x) = d\<cdot>x"
huffman@39999
   260
apply (rule MOST_d)
huffman@39999
   261
apply (subst iterate_Suc [symmetric])
huffman@39999
   262
apply (rule eventually_constant_MOST_Suc_eq)
huffman@39999
   263
apply (rule eventually_constant_iterate_app)
huffman@39999
   264
done
huffman@39999
   265
huffman@39999
   266
lemma d_fixed_iff: "d\<cdot>x = x \<longleftrightarrow> f\<cdot>x = x"
huffman@39999
   267
proof
huffman@39999
   268
  assume "d\<cdot>x = x"
huffman@39999
   269
  with f_d [where x=x]
huffman@39999
   270
  show "f\<cdot>x = x" by simp
huffman@39999
   271
next
huffman@39999
   272
  assume f: "f\<cdot>x = x"
huffman@39999
   273
  have "\<forall>n. iterate n\<cdot>f\<cdot>x = x"
huffman@39999
   274
    by (rule allI, rule nat.induct, simp, simp add: f)
huffman@39999
   275
  hence "MOST n. iterate n\<cdot>f\<cdot>x = x"
huffman@39999
   276
    by (rule ALL_MOST)
huffman@39999
   277
  thus "d\<cdot>x = x"
huffman@39999
   278
    by (rule MOST_d)
huffman@39999
   279
qed
huffman@39999
   280
huffman@39999
   281
lemma finite_deflation_d: "finite_deflation d"
huffman@39999
   282
proof
huffman@39999
   283
  fix x :: 'a
huffman@39999
   284
  have "d \<in> range (\<lambda>n. iterate n\<cdot>f)"
huffman@39999
   285
    unfolding eventual_iterate_def
huffman@39999
   286
    using eventually_constant_iterate
huffman@39999
   287
    by (rule eventual_mem_range)
huffman@39999
   288
  then obtain n where n: "d = iterate n\<cdot>f" ..
huffman@39999
   289
  have "iterate n\<cdot>f\<cdot>(d\<cdot>x) = d\<cdot>x"
huffman@39999
   290
    using f_d by (rule iterate_fixed)
huffman@39999
   291
  thus "d\<cdot>(d\<cdot>x) = d\<cdot>x"
huffman@39999
   292
    by (simp add: n)
huffman@39999
   293
next
huffman@39999
   294
  fix x :: 'a
huffman@39999
   295
  show "d\<cdot>x \<sqsubseteq> x"
huffman@39999
   296
    by (rule MOST_d, simp add: iterate_below)
huffman@39999
   297
next
huffman@39999
   298
  from finite_range
huffman@39999
   299
  have "finite {x. f\<cdot>x = x}"
huffman@39999
   300
    by (rule finite_range_imp_finite_fixes)
huffman@39999
   301
  thus "finite {x. d\<cdot>x = x}"
huffman@39999
   302
    by (simp add: d_fixed_iff)
huffman@39999
   303
qed
huffman@39999
   304
huffman@39999
   305
lemma deflation_d: "deflation d"
huffman@39999
   306
using finite_deflation_d
huffman@39999
   307
by (rule finite_deflation_imp_deflation)
huffman@39999
   308
huffman@39999
   309
end
huffman@39999
   310
huffman@39999
   311
lemma finite_deflation_eventual_iterate:
huffman@39999
   312
  "pre_deflation d \<Longrightarrow> finite_deflation (eventual_iterate d)"
huffman@39999
   313
by (rule pre_deflation.finite_deflation_d)
huffman@39999
   314
huffman@39999
   315
lemma pre_deflation_oo:
huffman@39999
   316
  assumes "finite_deflation d"
huffman@39999
   317
  assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
huffman@39999
   318
  shows "pre_deflation (d oo f)"
huffman@39999
   319
proof
huffman@39999
   320
  interpret d: finite_deflation d by fact
huffman@39999
   321
  fix x
huffman@39999
   322
  show "\<And>x. (d oo f)\<cdot>x \<sqsubseteq> x"
huffman@39999
   323
    by (simp, rule below_trans [OF d.below f])
huffman@39999
   324
  show "finite (range (\<lambda>x. (d oo f)\<cdot>x))"
huffman@39999
   325
    by (rule finite_subset [OF _ d.finite_range], auto)
huffman@39999
   326
qed
huffman@39999
   327
huffman@39999
   328
lemma eventual_iterate_oo_fixed_iff:
huffman@39999
   329
  assumes "finite_deflation d"
huffman@39999
   330
  assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
huffman@39999
   331
  shows "eventual_iterate (d oo f)\<cdot>x = x \<longleftrightarrow> d\<cdot>x = x \<and> f\<cdot>x = x"
huffman@39999
   332
proof -
huffman@39999
   333
  interpret d: finite_deflation d by fact
huffman@39999
   334
  let ?e = "d oo f"
huffman@39999
   335
  interpret e: pre_deflation "d oo f"
huffman@39999
   336
    using `finite_deflation d` f
huffman@39999
   337
    by (rule pre_deflation_oo)
huffman@39999
   338
  let ?g = "eventual (\<lambda>n. iterate n\<cdot>?e)"
huffman@39999
   339
  show ?thesis
huffman@39999
   340
    apply (subst e.d_fixed_iff)
huffman@39999
   341
    apply simp
huffman@39999
   342
    apply safe
huffman@39999
   343
    apply (erule subst)
huffman@39999
   344
    apply (rule d.idem)
huffman@39999
   345
    apply (rule below_antisym)
huffman@39999
   346
    apply (rule f)
huffman@39999
   347
    apply (erule subst, rule d.below)
huffman@39999
   348
    apply simp
huffman@39999
   349
    done
huffman@39999
   350
qed
huffman@39999
   351
huffman@39999
   352
lemma eventual_mono:
huffman@39999
   353
  assumes A: "eventually_constant A"
huffman@39999
   354
  assumes B: "eventually_constant B"
huffman@39999
   355
  assumes below: "\<And>n. A n \<sqsubseteq> B n"
huffman@39999
   356
  shows "eventual A \<sqsubseteq> eventual B"
huffman@39999
   357
proof -
huffman@39999
   358
  from A have "MOST n. A n = eventual A"
huffman@39999
   359
    by (rule MOST_eq_eventual)
huffman@39999
   360
  then have "MOST n. eventual A \<sqsubseteq> B n"
huffman@39999
   361
    by (rule MOST_mono) (erule subst, rule below)
huffman@39999
   362
  with B show "eventual A \<sqsubseteq> eventual B"
huffman@39999
   363
    by (rule MOST_eventual)
huffman@39999
   364
qed
huffman@39999
   365
huffman@39999
   366
lemma eventual_iterate_mono:
huffman@39999
   367
  assumes f: "pre_deflation f" and g: "pre_deflation g" and "f \<sqsubseteq> g"
huffman@39999
   368
  shows "eventual_iterate f \<sqsubseteq> eventual_iterate g"
huffman@39999
   369
unfolding eventual_iterate_def
huffman@39999
   370
apply (rule eventual_mono)
huffman@39999
   371
apply (rule pre_deflation.eventually_constant_iterate [OF f])
huffman@39999
   372
apply (rule pre_deflation.eventually_constant_iterate [OF g])
huffman@39999
   373
apply (rule monofun_cfun_arg [OF `f \<sqsubseteq> g`])
huffman@39999
   374
done
huffman@39999
   375
huffman@39999
   376
lemma cont2cont_eventual_iterate_oo:
huffman@39999
   377
  assumes d: "finite_deflation d"
huffman@39999
   378
  assumes cont: "cont f" and below: "\<And>x y. f x\<cdot>y \<sqsubseteq> y"
huffman@39999
   379
  shows "cont (\<lambda>x. eventual_iterate (d oo f x))"
huffman@39999
   380
    (is "cont ?e")
huffman@39999
   381
proof (rule contI2)
huffman@39999
   382
  show "monofun ?e"
huffman@39999
   383
    apply (rule monofunI)
huffman@39999
   384
    apply (rule eventual_iterate_mono)
huffman@39999
   385
    apply (rule pre_deflation_oo [OF d below])
huffman@39999
   386
    apply (rule pre_deflation_oo [OF d below])
huffman@39999
   387
    apply (rule monofun_cfun_arg)
huffman@39999
   388
    apply (erule cont2monofunE [OF cont])
huffman@39999
   389
    done
huffman@39999
   390
next
huffman@39999
   391
  fix Y :: "nat \<Rightarrow> 'b"
huffman@39999
   392
  assume Y: "chain Y"
huffman@39999
   393
  with cont have fY: "chain (\<lambda>i. f (Y i))"
huffman@39999
   394
    by (rule ch2ch_cont)
huffman@39999
   395
  assume eY: "chain (\<lambda>i. ?e (Y i))"
huffman@39999
   396
  have lub_below: "\<And>x. f (\<Squnion>i. Y i)\<cdot>x \<sqsubseteq> x"
huffman@39999
   397
    by (rule admD [OF _ Y], simp add: cont, rule below)
huffman@39999
   398
  have "deflation (?e (\<Squnion>i. Y i))"
huffman@39999
   399
    apply (rule pre_deflation.deflation_d)
huffman@39999
   400
    apply (rule pre_deflation_oo [OF d lub_below])
huffman@39999
   401
    done
huffman@39999
   402
  then show "?e (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. ?e (Y i))"
huffman@39999
   403
  proof (rule deflation.belowI)
huffman@39999
   404
    fix x :: 'a
huffman@39999
   405
    assume "?e (\<Squnion>i. Y i)\<cdot>x = x"
huffman@39999
   406
    hence "d\<cdot>x = x" and "f (\<Squnion>i. Y i)\<cdot>x = x"
huffman@39999
   407
      by (simp_all add: eventual_iterate_oo_fixed_iff [OF d lub_below])
huffman@39999
   408
    hence "(\<Squnion>i. f (Y i)\<cdot>x) = x"
huffman@39999
   409
      apply (simp only: cont2contlubE [OF cont Y])
huffman@39999
   410
      apply (simp only: contlub_cfun_fun [OF fY])
huffman@39999
   411
      done
huffman@39999
   412
    have "compact (d\<cdot>x)"
huffman@39999
   413
      using d by (rule finite_deflation.compact)
huffman@39999
   414
    then have "compact x"
huffman@39999
   415
      using `d\<cdot>x = x` by simp
huffman@39999
   416
    then have "compact (\<Squnion>i. f (Y i)\<cdot>x)"
huffman@39999
   417
      using `(\<Squnion>i. f (Y i)\<cdot>x) = x` by simp
huffman@39999
   418
    then have "\<exists>n. max_in_chain n (\<lambda>i. f (Y i)\<cdot>x)"
huffman@39999
   419
      by - (rule compact_imp_max_in_chain, simp add: fY, assumption)
huffman@39999
   420
    then obtain n where n: "max_in_chain n (\<lambda>i. f (Y i)\<cdot>x)" ..
huffman@39999
   421
    then have "f (Y n)\<cdot>x = x"
huffman@39999
   422
      using `(\<Squnion>i. f (Y i)\<cdot>x) = x` fY by (simp add: maxinch_is_thelub)
huffman@39999
   423
    with `d\<cdot>x = x` have "?e (Y n)\<cdot>x = x"
huffman@39999
   424
      by (simp add: eventual_iterate_oo_fixed_iff [OF d below])
huffman@39999
   425
    moreover have "?e (Y n)\<cdot>x \<sqsubseteq> (\<Squnion>i. ?e (Y i)\<cdot>x)"
huffman@39999
   426
      by (rule is_ub_thelub, simp add: eY)
huffman@39999
   427
    ultimately have "x \<sqsubseteq> (\<Squnion>i. ?e (Y i))\<cdot>x"
huffman@39999
   428
      by (simp add: contlub_cfun_fun eY)
huffman@39999
   429
    also have "(\<Squnion>i. ?e (Y i))\<cdot>x \<sqsubseteq> x"
huffman@39999
   430
      apply (rule deflation.below)
huffman@39999
   431
      apply (rule admD [OF adm_deflation eY])
huffman@39999
   432
      apply (rule pre_deflation.deflation_d)
huffman@39999
   433
      apply (rule pre_deflation_oo [OF d below])
huffman@39999
   434
      done
huffman@39999
   435
    finally show "(\<Squnion>i. ?e (Y i))\<cdot>x = x" ..
huffman@39999
   436
  qed
huffman@39999
   437
qed
huffman@39999
   438
huffman@39999
   439
subsection {* Take function for finite deflations *}
huffman@39999
   440
huffman@39999
   441
definition
huffman@39999
   442
  defl_take :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<Rightarrow> (udom \<rightarrow> udom)"
huffman@39999
   443
where
huffman@39999
   444
  "defl_take i d = eventual_iterate (udom_approx i oo d)"
huffman@39999
   445
huffman@39999
   446
lemma finite_deflation_defl_take:
huffman@39999
   447
  "deflation d \<Longrightarrow> finite_deflation (defl_take i d)"
huffman@39999
   448
unfolding defl_take_def
huffman@39999
   449
apply (rule pre_deflation.finite_deflation_d)
huffman@39999
   450
apply (rule pre_deflation_oo)
huffman@39999
   451
apply (rule finite_deflation_udom_approx)
huffman@39999
   452
apply (erule deflation.below)
huffman@39999
   453
done
huffman@39999
   454
huffman@39999
   455
lemma deflation_defl_take:
huffman@39999
   456
  "deflation d \<Longrightarrow> deflation (defl_take i d)"
huffman@39999
   457
apply (rule finite_deflation_imp_deflation)
huffman@39999
   458
apply (erule finite_deflation_defl_take)
huffman@39999
   459
done
huffman@39999
   460
huffman@39999
   461
lemma defl_take_fixed_iff:
huffman@39999
   462
  "deflation d \<Longrightarrow> defl_take i d\<cdot>x = x \<longleftrightarrow> udom_approx i\<cdot>x = x \<and> d\<cdot>x = x"
huffman@39999
   463
unfolding defl_take_def
huffman@39999
   464
apply (rule eventual_iterate_oo_fixed_iff)
huffman@39999
   465
apply (rule finite_deflation_udom_approx)
huffman@39999
   466
apply (erule deflation.below)
huffman@39999
   467
done
huffman@39999
   468
huffman@39999
   469
lemma defl_take_below:
huffman@39999
   470
  "\<lbrakk>a \<sqsubseteq> b; deflation a; deflation b\<rbrakk> \<Longrightarrow> defl_take i a \<sqsubseteq> defl_take i b"
huffman@39999
   471
apply (rule deflation.belowI)
huffman@39999
   472
apply (erule deflation_defl_take)
huffman@39999
   473
apply (simp add: defl_take_fixed_iff)
huffman@39999
   474
apply (erule (1) deflation.belowD)
huffman@39999
   475
apply (erule conjunct2)
huffman@39999
   476
done
huffman@39999
   477
huffman@39999
   478
lemma cont2cont_defl_take:
huffman@39999
   479
  assumes cont: "cont f" and below: "\<And>x y. f x\<cdot>y \<sqsubseteq> y"
huffman@39999
   480
  shows "cont (\<lambda>x. defl_take i (f x))"
huffman@39999
   481
unfolding defl_take_def
huffman@39999
   482
using finite_deflation_udom_approx assms
huffman@39999
   483
by (rule cont2cont_eventual_iterate_oo)
huffman@39999
   484
huffman@39999
   485
definition
huffman@39999
   486
  fd_take :: "nat \<Rightarrow> fin_defl \<Rightarrow> fin_defl"
huffman@39999
   487
where
huffman@39999
   488
  "fd_take i d = Abs_fin_defl (defl_take i (Rep_fin_defl d))"
huffman@39999
   489
huffman@39999
   490
lemma Rep_fin_defl_fd_take:
huffman@39999
   491
  "Rep_fin_defl (fd_take i d) = defl_take i (Rep_fin_defl d)"
huffman@39999
   492
unfolding fd_take_def
huffman@39999
   493
apply (rule Abs_fin_defl_inverse [unfolded mem_Collect_eq])
huffman@39999
   494
apply (rule finite_deflation_defl_take)
huffman@39999
   495
apply (rule deflation_Rep_fin_defl)
huffman@39999
   496
done
huffman@39999
   497
huffman@39999
   498
lemma fd_take_fixed_iff:
huffman@39999
   499
  "Rep_fin_defl (fd_take i d)\<cdot>x = x \<longleftrightarrow>
huffman@39999
   500
    udom_approx i\<cdot>x = x \<and> Rep_fin_defl d\<cdot>x = x"
huffman@39999
   501
unfolding Rep_fin_defl_fd_take
huffman@39999
   502
apply (rule defl_take_fixed_iff)
huffman@39999
   503
apply (rule deflation_Rep_fin_defl)
huffman@39999
   504
done
huffman@39999
   505
huffman@39999
   506
lemma fd_take_below: "fd_take n d \<sqsubseteq> d"
huffman@39999
   507
apply (rule fin_defl_belowI)
huffman@39999
   508
apply (simp add: fd_take_fixed_iff)
huffman@39999
   509
done
huffman@39999
   510
huffman@39999
   511
lemma fd_take_idem: "fd_take n (fd_take n d) = fd_take n d"
huffman@39999
   512
apply (rule fin_defl_eqI)
huffman@39999
   513
apply (simp add: fd_take_fixed_iff)
huffman@39999
   514
done
huffman@39999
   515
huffman@39999
   516
lemma fd_take_mono: "a \<sqsubseteq> b \<Longrightarrow> fd_take n a \<sqsubseteq> fd_take n b"
huffman@39999
   517
apply (rule fin_defl_belowI)
huffman@39999
   518
apply (simp add: fd_take_fixed_iff)
huffman@39999
   519
apply (simp add: fin_defl_belowD)
huffman@39999
   520
done
huffman@39999
   521
huffman@39999
   522
lemma approx_fixed_le_lemma: "\<lbrakk>i \<le> j; udom_approx i\<cdot>x = x\<rbrakk> \<Longrightarrow> udom_approx j\<cdot>x = x"
huffman@39999
   523
apply (rule deflation.belowD)
huffman@39999
   524
apply (rule finite_deflation_imp_deflation)
huffman@39999
   525
apply (rule finite_deflation_udom_approx)
huffman@39999
   526
apply (erule chain_mono [OF chain_udom_approx])
huffman@39999
   527
apply assumption
huffman@39999
   528
done
huffman@39999
   529
huffman@39999
   530
lemma fd_take_chain: "m \<le> n \<Longrightarrow> fd_take m a \<sqsubseteq> fd_take n a"
huffman@39999
   531
apply (rule fin_defl_belowI)
huffman@39999
   532
apply (simp add: fd_take_fixed_iff)
huffman@39999
   533
apply (simp add: approx_fixed_le_lemma)
huffman@39999
   534
done
huffman@39999
   535
huffman@39999
   536
lemma finite_range_fd_take: "finite (range (fd_take n))"
huffman@39999
   537
apply (rule finite_imageD [where f="\<lambda>a. {x. Rep_fin_defl a\<cdot>x = x}"])
huffman@39999
   538
apply (rule finite_subset [where B="Pow {x. udom_approx n\<cdot>x = x}"])
huffman@39999
   539
apply (clarify, simp add: fd_take_fixed_iff)
huffman@39999
   540
apply (simp add: finite_deflation.finite_fixes [OF finite_deflation_udom_approx])
huffman@39999
   541
apply (rule inj_onI, clarify)
huffman@39999
   542
apply (simp add: set_eq_iff fin_defl_eqI)
huffman@39999
   543
done
huffman@39999
   544
huffman@39999
   545
lemma fd_take_covers: "\<exists>n. fd_take n a = a"
huffman@39999
   546
apply (rule_tac x=
huffman@39999
   547
  "Max ((\<lambda>x. LEAST n. udom_approx n\<cdot>x = x) ` {x. Rep_fin_defl a\<cdot>x = x})" in exI)
huffman@39999
   548
apply (rule below_antisym)
huffman@39999
   549
apply (rule fd_take_below)
huffman@39999
   550
apply (rule fin_defl_belowI)
huffman@39999
   551
apply (simp add: fd_take_fixed_iff)
huffman@39999
   552
apply (rule approx_fixed_le_lemma)
huffman@39999
   553
apply (rule Max_ge)
huffman@39999
   554
apply (rule finite_imageI)
huffman@39999
   555
apply (rule Rep_fin_defl.finite_fixes)
huffman@39999
   556
apply (rule imageI)
huffman@39999
   557
apply (erule CollectI)
huffman@39999
   558
apply (rule LeastI_ex)
huffman@39999
   559
apply (rule approx_chain.compact_eq_approx [OF udom_approx])
huffman@39999
   560
apply (erule subst)
huffman@39999
   561
apply (rule Rep_fin_defl.compact)
huffman@39999
   562
done
huffman@39999
   563
huffman@39999
   564
subsection {* Chain of approx functions on algebraic deflations *}
huffman@39999
   565
huffman@39999
   566
definition
huffman@39999
   567
  defl_approx :: "nat \<Rightarrow> defl \<rightarrow> defl"
huffman@39999
   568
where
huffman@39999
   569
  "defl_approx = (\<lambda>i. defl.basis_fun (\<lambda>d. defl_principal (fd_take i d)))"
huffman@39999
   570
huffman@39999
   571
lemma defl_approx_principal:
huffman@39999
   572
  "defl_approx i\<cdot>(defl_principal d) = defl_principal (fd_take i d)"
huffman@39999
   573
unfolding defl_approx_def
huffman@39999
   574
by (simp add: defl.basis_fun_principal fd_take_mono)
huffman@39999
   575
huffman@39999
   576
lemma defl_approx: "approx_chain defl_approx"
huffman@39999
   577
proof
huffman@39999
   578
  show chain: "chain defl_approx"
huffman@39999
   579
    unfolding defl_approx_def
huffman@39999
   580
    by (simp add: chainI defl.basis_fun_mono fd_take_mono fd_take_chain)
huffman@39999
   581
  show idem: "\<And>i x. defl_approx i\<cdot>(defl_approx i\<cdot>x) = defl_approx i\<cdot>x"
huffman@39999
   582
    apply (induct_tac x rule: defl.principal_induct, simp)
huffman@39999
   583
    apply (simp add: defl_approx_principal fd_take_idem)
huffman@39999
   584
    done
huffman@39999
   585
  show below: "\<And>i x. defl_approx i\<cdot>x \<sqsubseteq> x"
huffman@39999
   586
    apply (induct_tac x rule: defl.principal_induct, simp)
huffman@39999
   587
    apply (simp add: defl_approx_principal fd_take_below)
huffman@39999
   588
    done
huffman@39999
   589
  show lub: "(\<Squnion>i. defl_approx i) = ID"
huffman@40002
   590
    apply (rule cfun_eqI, rule below_antisym)
huffman@39999
   591
    apply (simp add: contlub_cfun_fun chain lub_below_iff chain below)
huffman@39999
   592
    apply (induct_tac x rule: defl.principal_induct, simp)
huffman@39999
   593
    apply (simp add: contlub_cfun_fun chain)
huffman@39999
   594
    apply (simp add: compact_below_lub_iff defl.compact_principal chain)
huffman@39999
   595
    apply (simp add: defl_approx_principal)
huffman@39999
   596
    apply (subgoal_tac "\<exists>i. fd_take i a = a", metis below_refl)
huffman@39999
   597
    apply (rule fd_take_covers)
huffman@39999
   598
    done
huffman@39999
   599
  show "\<And>i. finite {x. defl_approx i\<cdot>x = x}"
huffman@39999
   600
    apply (rule finite_range_imp_finite_fixes)
huffman@39999
   601
    apply (rule_tac B="defl_principal ` range (fd_take i)" in rev_finite_subset)
huffman@39999
   602
    apply (simp add: finite_range_fd_take)
huffman@39999
   603
    apply (clarsimp, rename_tac x)
huffman@39999
   604
    apply (induct_tac x rule: defl.principal_induct)
huffman@39999
   605
    apply (simp add: adm_mem_finite finite_range_fd_take)
huffman@39999
   606
    apply (simp add: defl_approx_principal)
huffman@39999
   607
    done
huffman@39999
   608
qed
huffman@39999
   609
huffman@39999
   610
subsection {* Algebraic deflations are a bifinite domain *}
huffman@39999
   611
huffman@39999
   612
instantiation defl :: bifinite
huffman@39999
   613
begin
huffman@39999
   614
huffman@39999
   615
definition
huffman@39999
   616
  "emb = udom_emb defl_approx"
huffman@39999
   617
huffman@39999
   618
definition
huffman@39999
   619
  "prj = udom_prj defl_approx"
huffman@39999
   620
huffman@39999
   621
definition
huffman@39999
   622
  "defl (t::defl itself) =
huffman@39999
   623
    (\<Squnion>i. defl_principal (Abs_fin_defl (emb oo defl_approx i oo prj)))"
huffman@39999
   624
huffman@40491
   625
definition
huffman@40491
   626
  "(liftemb :: defl u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
huffman@40491
   627
huffman@40491
   628
definition
huffman@40491
   629
  "(liftprj :: udom \<rightarrow> defl u) = u_map\<cdot>prj oo udom_prj u_approx"
huffman@40491
   630
huffman@40491
   631
definition
huffman@40491
   632
  "liftdefl (t::defl itself) = u_defl\<cdot>DEFL(defl)"
huffman@40491
   633
huffman@40491
   634
instance
huffman@40491
   635
using liftemb_defl_def liftprj_defl_def liftdefl_defl_def
huffman@40491
   636
proof (rule bifinite_class_intro)
huffman@39999
   637
  show ep: "ep_pair emb (prj :: udom \<rightarrow> defl)"
huffman@39999
   638
    unfolding emb_defl_def prj_defl_def
huffman@39999
   639
    by (rule ep_pair_udom [OF defl_approx])
huffman@39999
   640
  show "cast\<cdot>DEFL(defl) = emb oo (prj :: udom \<rightarrow> defl)"
huffman@39999
   641
    unfolding defl_defl_def
huffman@39999
   642
    apply (subst contlub_cfun_arg)
huffman@39999
   643
    apply (rule chainI)
huffman@39999
   644
    apply (rule defl.principal_mono)
huffman@39999
   645
    apply (simp add: below_fin_defl_def)
huffman@39999
   646
    apply (simp add: Abs_fin_defl_inverse approx_chain.finite_deflation_approx [OF defl_approx]
huffman@39999
   647
                     ep_pair.finite_deflation_e_d_p [OF ep])
huffman@39999
   648
    apply (intro monofun_cfun below_refl)
huffman@39999
   649
    apply (rule chainE)
huffman@39999
   650
    apply (rule approx_chain.chain_approx [OF defl_approx])
huffman@39999
   651
    apply (subst cast_defl_principal)
huffman@39999
   652
    apply (simp add: Abs_fin_defl_inverse approx_chain.finite_deflation_approx [OF defl_approx]
huffman@39999
   653
                     ep_pair.finite_deflation_e_d_p [OF ep])
huffman@39999
   654
    apply (simp add: lub_distribs approx_chain.chain_approx [OF defl_approx]
huffman@39999
   655
                     approx_chain.lub_approx [OF defl_approx])
huffman@39999
   656
    done
huffman@39999
   657
qed
huffman@39999
   658
huffman@39999
   659
end
huffman@39999
   660
huffman@39999
   661
end