src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
author Andreas Lochbihler
Fri Jul 29 09:49:23 2016 +0200 (2016-07-29)
changeset 63561 fba08009ff3e
parent 63540 f8652d0534fa
child 63562 6f7a9d48a828
permissions -rw-r--r--
add lemmas contributed by Peter Gammie
wenzelm@62058
     1
(*  Title:      HOL/Library/Bourbaki_Witt_Fixpoint.thy
wenzelm@62058
     2
    Author:     Andreas Lochbihler, ETH Zurich
Andreas@62141
     3
Andreas@62141
     4
  Follows G. Smolka, S. Schäfer and C. Doczkal: Transfinite Constructions in
Andreas@62141
     5
  Classical Type Theory. ITP 2015
wenzelm@62058
     6
*)
Andreas@61766
     7
Andreas@61766
     8
section \<open>The Bourbaki-Witt tower construction for transfinite iteration\<close>
Andreas@61766
     9
wenzelm@63540
    10
theory Bourbaki_Witt_Fixpoint
Andreas@63561
    11
  imports While_Combinator
wenzelm@63540
    12
begin
Andreas@61766
    13
Andreas@61766
    14
lemma ChainsI [intro?]:
Andreas@61766
    15
  "(\<And>a b. \<lbrakk> a \<in> Y; b \<in> Y \<rbrakk> \<Longrightarrow> (a, b) \<in> r \<or> (b, a) \<in> r) \<Longrightarrow> Y \<in> Chains r"
Andreas@61766
    16
unfolding Chains_def by blast
Andreas@61766
    17
Andreas@61766
    18
lemma in_Chains_subset: "\<lbrakk> M \<in> Chains r; M' \<subseteq> M \<rbrakk> \<Longrightarrow> M' \<in> Chains r"
Andreas@61766
    19
by(auto simp add: Chains_def)
Andreas@61766
    20
Andreas@63561
    21
lemma in_ChainsD: "\<lbrakk> M \<in> Chains r; x \<in> M; y \<in> M \<rbrakk> \<Longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r"
Andreas@63561
    22
unfolding Chains_def by fast
Andreas@61766
    23
Andreas@61766
    24
lemma Chains_FieldD: "\<lbrakk> M \<in> Chains r; x \<in> M \<rbrakk> \<Longrightarrow> x \<in> Field r"
Andreas@61766
    25
by(auto simp add: Chains_def intro: FieldI1 FieldI2)
Andreas@61766
    26
Andreas@62622
    27
lemma in_Chains_conv_chain: "M \<in> Chains r \<longleftrightarrow> Complete_Partial_Order.chain (\<lambda>x y. (x, y) \<in> r) M"
Andreas@62622
    28
by(simp add: Chains_def chain_def)
Andreas@62622
    29
Andreas@61766
    30
lemma partial_order_on_trans:
Andreas@61766
    31
  "\<lbrakk> partial_order_on A r; (x, y) \<in> r; (y, z) \<in> r \<rbrakk> \<Longrightarrow> (x, z) \<in> r"
Andreas@61766
    32
by(auto simp add: order_on_defs dest: transD)
Andreas@61766
    33
Andreas@61766
    34
locale bourbaki_witt_fixpoint =
Andreas@61766
    35
  fixes lub :: "'a set \<Rightarrow> 'a"
Andreas@61766
    36
  and leq :: "('a \<times> 'a) set"
Andreas@61766
    37
  and f :: "'a \<Rightarrow> 'a"
Andreas@61766
    38
  assumes po: "Partial_order leq"
Andreas@61766
    39
  and lub_least: "\<lbrakk> M \<in> Chains leq; M \<noteq> {}; \<And>x. x \<in> M \<Longrightarrow> (x, z) \<in> leq \<rbrakk> \<Longrightarrow> (lub M, z) \<in> leq"
Andreas@61766
    40
  and lub_upper: "\<lbrakk> M \<in> Chains leq; x \<in> M \<rbrakk> \<Longrightarrow> (x, lub M) \<in> leq"
Andreas@61766
    41
  and lub_in_Field: "\<lbrakk> M \<in> Chains leq; M \<noteq> {} \<rbrakk> \<Longrightarrow> lub M \<in> Field leq"
Andreas@61766
    42
  and increasing: "\<And>x. x \<in> Field leq \<Longrightarrow> (x, f x) \<in> leq"
Andreas@61766
    43
begin
Andreas@61766
    44
Andreas@61766
    45
lemma leq_trans: "\<lbrakk> (x, y) \<in> leq; (y, z) \<in> leq \<rbrakk> \<Longrightarrow> (x, z) \<in> leq"
Andreas@61766
    46
by(rule partial_order_on_trans[OF po])
Andreas@61766
    47
Andreas@61766
    48
lemma leq_refl: "x \<in> Field leq \<Longrightarrow> (x, x) \<in> leq"
Andreas@61766
    49
using po by(simp add: order_on_defs refl_on_def)
Andreas@61766
    50
Andreas@61766
    51
lemma leq_antisym: "\<lbrakk> (x, y) \<in> leq; (y, x) \<in> leq \<rbrakk> \<Longrightarrow> x = y"
Andreas@61766
    52
using po by(simp add: order_on_defs antisym_def)
Andreas@61766
    53
Andreas@61766
    54
inductive_set iterates_above :: "'a \<Rightarrow> 'a set"
Andreas@61766
    55
  for a
Andreas@61766
    56
where
Andreas@61766
    57
  base: "a \<in> iterates_above a"
Andreas@61766
    58
| step: "x \<in> iterates_above a \<Longrightarrow> f x \<in> iterates_above a"
Andreas@61766
    59
| Sup: "\<lbrakk> M \<in> Chains leq; M \<noteq> {}; \<And>x. x \<in> M \<Longrightarrow> x \<in> iterates_above a \<rbrakk> \<Longrightarrow> lub M \<in> iterates_above a"
Andreas@61766
    60
Andreas@61766
    61
definition fixp_above :: "'a \<Rightarrow> 'a"
Andreas@62647
    62
where "fixp_above a = (if a \<in> Field leq then lub (iterates_above a) else a)"
Andreas@62647
    63
Andreas@62647
    64
lemma fixp_above_outside: "a \<notin> Field leq \<Longrightarrow> fixp_above a = a"
Andreas@62647
    65
by(simp add: fixp_above_def)
Andreas@62647
    66
Andreas@62647
    67
lemma fixp_above_inside: "a \<in> Field leq \<Longrightarrow> fixp_above a = lub (iterates_above a)"
Andreas@62647
    68
by(simp add: fixp_above_def)
Andreas@61766
    69
Andreas@61766
    70
context 
Andreas@61766
    71
  notes leq_refl [intro!, simp]
Andreas@61766
    72
  and base [intro]
Andreas@61766
    73
  and step [intro]
Andreas@61766
    74
  and Sup [intro]
Andreas@61766
    75
  and leq_trans [trans]
Andreas@61766
    76
begin
Andreas@61766
    77
Andreas@61766
    78
lemma iterates_above_le_f: "\<lbrakk> x \<in> iterates_above a; a \<in> Field leq \<rbrakk> \<Longrightarrow> (x, f x) \<in> leq"
Andreas@61766
    79
by(induction x rule: iterates_above.induct)(blast intro: increasing FieldI2 lub_in_Field)+
Andreas@61766
    80
Andreas@61766
    81
lemma iterates_above_Field: "\<lbrakk> x \<in> iterates_above a; a \<in> Field leq \<rbrakk> \<Longrightarrow> x \<in> Field leq"
Andreas@61766
    82
by(drule (1) iterates_above_le_f)(rule FieldI1)
Andreas@61766
    83
Andreas@61766
    84
lemma iterates_above_ge:
Andreas@61766
    85
  assumes y: "y \<in> iterates_above a"
Andreas@61766
    86
  and a: "a \<in> Field leq"
Andreas@61766
    87
  shows "(a, y) \<in> leq"
Andreas@61766
    88
using y by(induction)(auto intro: a increasing iterates_above_le_f leq_trans leq_trans[OF _ lub_upper])
Andreas@61766
    89
Andreas@61766
    90
lemma iterates_above_lub:
Andreas@61766
    91
  assumes M: "M \<in> Chains leq"
Andreas@61766
    92
  and nempty: "M \<noteq> {}"
Andreas@61766
    93
  and upper: "\<And>y. y \<in> M \<Longrightarrow> \<exists>z \<in> M. (y, z) \<in> leq \<and> z \<in> iterates_above a"
Andreas@61766
    94
  shows "lub M \<in> iterates_above a"
Andreas@61766
    95
proof -
Andreas@61766
    96
  let ?M = "M \<inter> iterates_above a"
Andreas@61766
    97
  from M have M': "?M \<in> Chains leq" by(rule in_Chains_subset)simp
Andreas@61766
    98
  have "?M \<noteq> {}" using nempty by(auto dest: upper)
Andreas@61766
    99
  with M' have "lub ?M \<in> iterates_above a" by(rule Sup) blast
Andreas@61766
   100
  also have "lub ?M = lub M" using nempty
Andreas@61766
   101
    by(intro leq_antisym)(blast intro!: lub_least[OF M] lub_least[OF M'] intro: lub_upper[OF M'] lub_upper[OF M] leq_trans dest: upper)+
Andreas@61766
   102
  finally show ?thesis .
Andreas@61766
   103
qed
Andreas@61766
   104
Andreas@61766
   105
lemma iterates_above_successor:
Andreas@61766
   106
  assumes y: "y \<in> iterates_above a"
Andreas@61766
   107
  and a: "a \<in> Field leq"
Andreas@61766
   108
  shows "y = a \<or> y \<in> iterates_above (f a)"
Andreas@61766
   109
using y
Andreas@61766
   110
proof induction
Andreas@61766
   111
  case base thus ?case by simp
Andreas@61766
   112
next
Andreas@61766
   113
  case (step x) thus ?case by auto
Andreas@61766
   114
next
Andreas@61766
   115
  case (Sup M)
Andreas@61766
   116
  show ?case
Andreas@61766
   117
  proof(cases "\<exists>x. M \<subseteq> {x}")
Andreas@61766
   118
    case True
Andreas@61766
   119
    with \<open>M \<noteq> {}\<close> obtain y where M: "M = {y}" by auto
Andreas@61766
   120
    have "lub M = y"
Andreas@61766
   121
      by(rule leq_antisym)(auto intro!: lub_upper Sup lub_least ChainsI simp add: a M Sup.hyps(3)[of y, THEN iterates_above_Field] dest: iterates_above_Field)
Andreas@61766
   122
    with Sup.IH[of y] M show ?thesis by simp
Andreas@61766
   123
  next
Andreas@61766
   124
    case False
Andreas@61766
   125
    from Sup(1-2) have "lub M \<in> iterates_above (f a)"
Andreas@61766
   126
    proof(rule iterates_above_lub)
Andreas@61766
   127
      fix y
Andreas@61766
   128
      assume y: "y \<in> M"
Andreas@61766
   129
      from Sup.IH[OF this] show "\<exists>z\<in>M. (y, z) \<in> leq \<and> z \<in> iterates_above (f a)"
Andreas@61766
   130
      proof
Andreas@61766
   131
        assume "y = a"
Andreas@61766
   132
        from y False obtain z where z: "z \<in> M" and neq: "y \<noteq> z" by (metis insertI1 subsetI)
Andreas@61766
   133
        with Sup.IH[OF z] \<open>y = a\<close> Sup.hyps(3)[OF z]
Andreas@61766
   134
        show ?thesis by(auto dest: iterates_above_ge intro: a)
Andreas@61766
   135
      next
wenzelm@63540
   136
        assume *: "y \<in> iterates_above (f a)"
wenzelm@63540
   137
        with increasing[OF a] have "y \<in> Field leq"
Andreas@61766
   138
          by(auto dest!: iterates_above_Field intro: FieldI2)
wenzelm@63540
   139
        with * show ?thesis using y by auto
Andreas@61766
   140
      qed
Andreas@61766
   141
    qed
Andreas@61766
   142
    thus ?thesis by simp
Andreas@61766
   143
  qed
Andreas@61766
   144
qed
Andreas@61766
   145
Andreas@61766
   146
lemma iterates_above_Sup_aux:
Andreas@61766
   147
  assumes M: "M \<in> Chains leq" "M \<noteq> {}"
Andreas@61766
   148
  and M': "M' \<in> Chains leq" "M' \<noteq> {}"
Andreas@61766
   149
  and comp: "\<And>x. x \<in> M \<Longrightarrow> x \<in> iterates_above (lub M') \<or> lub M' \<in> iterates_above x"
Andreas@61766
   150
  shows "(lub M, lub M') \<in> leq \<or> lub M \<in> iterates_above (lub M')"
Andreas@61766
   151
proof(cases "\<exists>x \<in> M. x \<in> iterates_above (lub M')")
Andreas@61766
   152
  case True
Andreas@61766
   153
  then obtain x where x: "x \<in> M" "x \<in> iterates_above (lub M')" by blast
Andreas@61766
   154
  have lub_M': "lub M' \<in> Field leq" using M' by(rule lub_in_Field)
Andreas@61766
   155
  have "lub M \<in> iterates_above (lub M')" using M
Andreas@61766
   156
  proof(rule iterates_above_lub)
Andreas@61766
   157
    fix y
Andreas@61766
   158
    assume y: "y \<in> M"
Andreas@61766
   159
    from comp[OF y] show "\<exists>z\<in>M. (y, z) \<in> leq \<and> z \<in> iterates_above (lub M')"
Andreas@61766
   160
    proof
Andreas@61766
   161
      assume "y \<in> iterates_above (lub M')"
Andreas@61766
   162
      from this iterates_above_Field[OF this] y lub_M' show ?thesis by blast
Andreas@61766
   163
    next
Andreas@61766
   164
      assume "lub M' \<in> iterates_above y"
Andreas@61766
   165
      hence "(y, lub M') \<in> leq" using Chains_FieldD[OF M(1) y] by(rule iterates_above_ge)
Andreas@61766
   166
      also have "(lub M', x) \<in> leq" using x(2) lub_M' by(rule iterates_above_ge)
Andreas@61766
   167
      finally show ?thesis using x by blast
Andreas@61766
   168
    qed
Andreas@61766
   169
  qed
Andreas@61766
   170
  thus ?thesis ..
Andreas@61766
   171
next
Andreas@61766
   172
  case False
Andreas@61766
   173
  have "(lub M, lub M') \<in> leq" using M
Andreas@61766
   174
  proof(rule lub_least)
Andreas@61766
   175
    fix x
Andreas@61766
   176
    assume x: "x \<in> M"
Andreas@61766
   177
    from comp[OF x] x False have "lub M' \<in> iterates_above x" by auto
Andreas@61766
   178
    moreover from M(1) x have "x \<in> Field leq" by(rule Chains_FieldD)
Andreas@61766
   179
    ultimately show "(x, lub M') \<in> leq" by(rule iterates_above_ge)
Andreas@61766
   180
  qed
Andreas@61766
   181
  thus ?thesis ..
Andreas@61766
   182
qed
Andreas@61766
   183
Andreas@61766
   184
lemma iterates_above_triangle:
Andreas@61766
   185
  assumes x: "x \<in> iterates_above a"
Andreas@61766
   186
  and y: "y \<in> iterates_above a"
Andreas@61766
   187
  and a: "a \<in> Field leq"
Andreas@61766
   188
  shows "x \<in> iterates_above y \<or> y \<in> iterates_above x"
Andreas@61766
   189
using x y
Andreas@61766
   190
proof(induction arbitrary: y)
Andreas@61766
   191
  case base then show ?case by simp
Andreas@61766
   192
next
Andreas@61766
   193
  case (step x) thus ?case using a
Andreas@61766
   194
    by(auto dest: iterates_above_successor intro: iterates_above_Field)
Andreas@61766
   195
next
Andreas@61766
   196
  case x: (Sup M)
Andreas@61766
   197
  hence lub: "lub M \<in> iterates_above a" by blast
Andreas@61766
   198
  from \<open>y \<in> iterates_above a\<close> show ?case
Andreas@61766
   199
  proof(induction)
Andreas@61766
   200
    case base show ?case using lub by simp
Andreas@61766
   201
  next
Andreas@61766
   202
    case (step y) thus ?case using a
Andreas@61766
   203
      by(auto dest: iterates_above_successor intro: iterates_above_Field)
Andreas@61766
   204
  next
Andreas@61766
   205
    case y: (Sup M')
Andreas@61766
   206
    hence lub': "lub M' \<in> iterates_above a" by blast
Andreas@61766
   207
    have *: "x \<in> iterates_above (lub M') \<or> lub M' \<in> iterates_above x" if "x \<in> M" for x
Andreas@61766
   208
      using that lub' by(rule x.IH)
Andreas@61766
   209
    with x(1-2) y(1-2) have "(lub M, lub M') \<in> leq \<or> lub M \<in> iterates_above (lub M')"
Andreas@61766
   210
      by(rule iterates_above_Sup_aux)
Andreas@61766
   211
    moreover from y(1-2) x(1-2) have "(lub M', lub M) \<in> leq \<or> lub M' \<in> iterates_above (lub M)"
Andreas@61766
   212
      by(rule iterates_above_Sup_aux)(blast dest: y.IH)
Andreas@61766
   213
    ultimately show ?case by(auto 4 3 dest: leq_antisym)
Andreas@61766
   214
  qed
Andreas@61766
   215
qed
Andreas@61766
   216
Andreas@61766
   217
lemma chain_iterates_above: 
Andreas@61766
   218
  assumes a: "a \<in> Field leq"
Andreas@61766
   219
  shows "iterates_above a \<in> Chains leq" (is "?C \<in> _")
Andreas@61766
   220
proof (rule ChainsI)
Andreas@61766
   221
  fix x y
Andreas@61766
   222
  assume "x \<in> ?C" "y \<in> ?C"
Andreas@61766
   223
  hence "x \<in> iterates_above y \<or> y \<in> iterates_above x" using a by(rule iterates_above_triangle)
Andreas@61766
   224
  moreover from \<open>x \<in> ?C\<close> a have "x \<in> Field leq" by(rule iterates_above_Field)
Andreas@61766
   225
  moreover from \<open>y \<in> ?C\<close> a have "y \<in> Field leq" by(rule iterates_above_Field)
Andreas@61766
   226
  ultimately show "(x, y) \<in> leq \<or> (y, x) \<in> leq" by(auto dest: iterates_above_ge)
Andreas@61766
   227
qed
Andreas@61766
   228
Andreas@62647
   229
lemma fixp_iterates_above: "fixp_above a \<in> iterates_above a"
Andreas@62647
   230
by(auto intro: chain_iterates_above simp add: fixp_above_def)
Andreas@61766
   231
Andreas@61766
   232
lemma fixp_above_Field: "a \<in> Field leq \<Longrightarrow> fixp_above a \<in> Field leq"
Andreas@61766
   233
using fixp_iterates_above by(rule iterates_above_Field)
Andreas@61766
   234
Andreas@61766
   235
lemma fixp_above_unfold:
Andreas@61766
   236
  assumes a: "a \<in> Field leq"
Andreas@61766
   237
  shows "fixp_above a = f (fixp_above a)" (is "?a = f ?a")
Andreas@61766
   238
proof(rule leq_antisym)
Andreas@61766
   239
  show "(?a, f ?a) \<in> leq" using fixp_above_Field[OF a] by(rule increasing)
Andreas@61766
   240
  
Andreas@62647
   241
  have "f ?a \<in> iterates_above a" using fixp_iterates_above by(rule iterates_above.step)
Andreas@62647
   242
  with chain_iterates_above[OF a] show "(f ?a, ?a) \<in> leq"
Andreas@62647
   243
    by(simp add: fixp_above_inside assms lub_upper)
Andreas@61766
   244
qed
Andreas@61766
   245
Andreas@61766
   246
end
Andreas@61766
   247
Andreas@63561
   248
lemma fixp_above_induct [case_names adm base step]:
Andreas@62622
   249
  assumes adm: "ccpo.admissible lub (\<lambda>x y. (x, y) \<in> leq) P"
Andreas@62622
   250
  and base: "P a"
Andreas@62622
   251
  and step: "\<And>x. P x \<Longrightarrow> P (f x)"
Andreas@62622
   252
  shows "P (fixp_above a)"
Andreas@62647
   253
proof(cases "a \<in> Field leq")
Andreas@62647
   254
  case True
Andreas@62647
   255
  from adm chain_iterates_above[OF True]
Andreas@62647
   256
  show ?thesis unfolding fixp_above_inside[OF True] in_Chains_conv_chain
Andreas@62647
   257
  proof(rule ccpo.admissibleD)
Andreas@62647
   258
    have "a \<in> iterates_above a" ..
Andreas@62647
   259
    then show "iterates_above a \<noteq> {}" by(auto)
Andreas@62647
   260
    show "P x" if "x \<in> iterates_above a" for x using that
Andreas@62647
   261
      by induction(auto intro: base step simp add: in_Chains_conv_chain dest: ccpo.admissibleD[OF adm])
Andreas@62647
   262
  qed
Andreas@62647
   263
qed(simp add: fixp_above_outside base)
Andreas@62622
   264
Andreas@61766
   265
end
Andreas@61766
   266
Andreas@63561
   267
subsection \<open>Connect with the while combinator for executability on chain-finite lattices.\<close>
Andreas@63561
   268
Andreas@63561
   269
context bourbaki_witt_fixpoint begin
Andreas@63561
   270
Andreas@63561
   271
lemma in_Chains_finite: -- \<open>Translation from @{thm in_chain_finite}. }\<close>
Andreas@63561
   272
  assumes "M \<in> Chains leq"
Andreas@63561
   273
  and "M \<noteq> {}"
Andreas@63561
   274
  and "finite M"
Andreas@63561
   275
  shows "lub M \<in> M"
Andreas@63561
   276
using assms(3,1,2)
Andreas@63561
   277
proof induction
Andreas@63561
   278
  case empty thus ?case by simp
Andreas@63561
   279
next
Andreas@63561
   280
  case (insert x M)
Andreas@63561
   281
  note chain = \<open>insert x M \<in> Chains leq\<close>
Andreas@63561
   282
  show ?case
Andreas@63561
   283
  proof(cases "M = {}")
Andreas@63561
   284
    case True thus ?thesis
Andreas@63561
   285
      using chain in_ChainsD leq_antisym lub_least lub_upper by fastforce
Andreas@63561
   286
  next
Andreas@63561
   287
    case False
Andreas@63561
   288
    from chain have chain': "M \<in> Chains leq"
Andreas@63561
   289
      using in_Chains_subset subset_insertI by blast
Andreas@63561
   290
    hence "lub M \<in> M" using False by(rule insert.IH)
Andreas@63561
   291
    show ?thesis
Andreas@63561
   292
    proof(cases "(x, lub M) \<in> leq")
Andreas@63561
   293
      case True
Andreas@63561
   294
      have "(lub (insert x M), lub M) \<in> leq" using chain
Andreas@63561
   295
        by (rule lub_least) (auto simp: True intro: lub_upper[OF chain'])
Andreas@63561
   296
      with False have "lub (insert x M) = lub M"
Andreas@63561
   297
        using lub_upper[OF chain] lub_least[OF chain'] by (blast intro: leq_antisym)
Andreas@63561
   298
      with \<open>lub M \<in> M\<close> show ?thesis by simp
Andreas@63561
   299
    next
Andreas@63561
   300
      case False
Andreas@63561
   301
      with in_ChainsD[OF chain, of x "lub M"] \<open>lub M \<in> M\<close>
Andreas@63561
   302
      have "lub (insert x M) = x"
Andreas@63561
   303
        by - (rule leq_antisym, (blast intro: FieldI2 chain chain' insert.prems(2) leq_refl leq_trans lub_least lub_upper)+)
Andreas@63561
   304
      thus ?thesis by simp
Andreas@63561
   305
    qed
Andreas@63561
   306
  qed
Andreas@63561
   307
qed
Andreas@63561
   308
Andreas@63561
   309
lemma fun_pow_iterates_above: "(f ^^ k) a \<in> iterates_above a"
Andreas@63561
   310
using iterates_above.base iterates_above.step by (induct k) simp_all
Andreas@63561
   311
Andreas@63561
   312
lemma chfin_iterates_above_fun_pow:
Andreas@63561
   313
  assumes "x \<in> iterates_above a"
Andreas@63561
   314
  assumes "\<forall>M \<in> Chains leq. finite M"
Andreas@63561
   315
  shows "\<exists>j. x = (f ^^ j) a"
Andreas@63561
   316
using assms(1)
Andreas@63561
   317
proof induct
Andreas@63561
   318
  case base then show ?case by (simp add: exI[where x=0])
Andreas@63561
   319
next
Andreas@63561
   320
  case (step x) then obtain j where "x = (f ^^ j) a" by blast
Andreas@63561
   321
  with step(1) show ?case by (simp add: exI[where x="Suc j"])
Andreas@63561
   322
next
Andreas@63561
   323
  case (Sup M) with in_Chains_finite assms(2) show ?case by blast
Andreas@63561
   324
qed
Andreas@63561
   325
Andreas@63561
   326
lemma Chain_finite_iterates_above_fun_pow_iff:
Andreas@63561
   327
  assumes "\<forall>M \<in> Chains leq. finite M"
Andreas@63561
   328
  shows "x \<in> iterates_above a \<longleftrightarrow> (\<exists>j. x = (f ^^ j) a)"
Andreas@63561
   329
using chfin_iterates_above_fun_pow fun_pow_iterates_above assms by blast
Andreas@63561
   330
Andreas@63561
   331
lemma fixp_above_Kleene_iter_ex:
Andreas@63561
   332
  assumes "(\<forall>M \<in> Chains leq. finite M)"
Andreas@63561
   333
  obtains k where "fixp_above a = (f ^^ k) a"
Andreas@63561
   334
using assms by atomize_elim (simp add: chfin_iterates_above_fun_pow fixp_iterates_above)
Andreas@63561
   335
Andreas@63561
   336
context fixes a assumes a: "a \<in> Field leq" begin
Andreas@63561
   337
Andreas@63561
   338
lemma funpow_Field_leq: "(f ^^ k) a \<in> Field leq"
Andreas@63561
   339
using a by (induct k) (auto intro: increasing FieldI2)
Andreas@63561
   340
Andreas@63561
   341
lemma funpow_prefix: "j < k \<Longrightarrow> ((f ^^ j) a, (f ^^ k) a) \<in> leq"
Andreas@63561
   342
proof(induct k)
Andreas@63561
   343
  case (Suc k)
Andreas@63561
   344
  with leq_trans[OF _ increasing[OF funpow_Field_leq]] funpow_Field_leq increasing a
Andreas@63561
   345
  show ?case by simp (metis less_antisym)
Andreas@63561
   346
qed simp
Andreas@63561
   347
Andreas@63561
   348
lemma funpow_suffix: "(f ^^ Suc k) a = (f ^^ k) a \<Longrightarrow> ((f ^^ (j + k)) a, (f ^^ k) a) \<in> leq"
Andreas@63561
   349
using funpow_Field_leq
Andreas@63561
   350
by (induct j) (simp_all del: funpow.simps add: funpow_Suc_right funpow_add leq_refl)
Andreas@63561
   351
Andreas@63561
   352
lemma funpow_stability: "(f ^^ Suc k) a = (f ^^ k) a \<Longrightarrow> ((f ^^ j) a, (f ^^ k) a) \<in> leq"
Andreas@63561
   353
using funpow_prefix funpow_suffix[where j="j - k" and k=k] by (cases "j < k") simp_all
Andreas@63561
   354
Andreas@63561
   355
lemma funpow_in_Chains: "{(f ^^ k) a |k. True} \<in> Chains leq"
Andreas@63561
   356
using chain_iterates_above[OF a] fun_pow_iterates_above
Andreas@63561
   357
by (blast intro: ChainsI dest: in_ChainsD)
Andreas@63561
   358
Andreas@63561
   359
lemma fixp_above_Kleene_iter:
Andreas@63561
   360
  assumes "\<forall>M \<in> Chains leq. finite M" (* convenient but surely not necessary *)
Andreas@63561
   361
  assumes "(f ^^ Suc k) a = (f ^^ k) a"
Andreas@63561
   362
  shows "fixp_above a = (f ^^ k) a"
Andreas@63561
   363
proof(rule leq_antisym)
Andreas@63561
   364
  show "(fixp_above a, (f ^^ k) a) \<in> leq" using assms a
Andreas@63561
   365
    by(auto simp add: fixp_above_def chain_iterates_above Chain_finite_iterates_above_fun_pow_iff funpow_stability[OF assms(2)] intro!: lub_least intro: iterates_above.base)
Andreas@63561
   366
  show "((f ^^ k) a, fixp_above a) \<in> leq" using a
Andreas@63561
   367
    by(auto simp add: fixp_above_def chain_iterates_above fun_pow_iterates_above intro!: lub_upper)
Andreas@63561
   368
qed
Andreas@63561
   369
Andreas@63561
   370
context assumes chfin: "\<forall>M \<in> Chains leq. finite M" begin
Andreas@63561
   371
Andreas@63561
   372
lemma Chain_finite_wf: "wf {(f ((f ^^ k) a), (f ^^ k) a) |k. f ((f ^^ k) a) \<noteq> (f ^^ k) a}"
Andreas@63561
   373
apply(rule wf_measure[where f="\<lambda>b. card {(f ^^ j) a |j. (b, (f ^^ j) a) \<in> leq}", THEN wf_subset])
Andreas@63561
   374
apply(auto simp: set_eq_iff intro!: psubset_card_mono[OF finite_subset[OF _ bspec[OF chfin funpow_in_Chains]]])
Andreas@63561
   375
apply(metis funpow_Field_leq increasing leq_antisym leq_trans leq_refl)+
Andreas@63561
   376
done
Andreas@63561
   377
Andreas@63561
   378
lemma while_option_finite_increasing: "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f a = Some P"
Andreas@63561
   379
by(rule wf_rel_while_option_Some[OF Chain_finite_wf, where P="\<lambda>A. (\<exists>k. A = (f ^^ k) a) \<and> (A, f A) \<in> leq" and s="a"])
Andreas@63561
   380
  (auto simp: a increasing chfin FieldI2 chfin_iterates_above_fun_pow fun_pow_iterates_above iterates_above.step intro: exI[where x=0])
Andreas@63561
   381
Andreas@63561
   382
lemma fixp_above_the_while_option: "fixp_above a = the (while_option (\<lambda>A. f A \<noteq> A) f a)"
Andreas@63561
   383
proof -
Andreas@63561
   384
  obtain P where "while_option (\<lambda>A. f A \<noteq> A) f a = Some P"
Andreas@63561
   385
    using while_option_finite_increasing by blast
Andreas@63561
   386
  with while_option_stop2[OF this] fixp_above_Kleene_iter[OF chfin]
Andreas@63561
   387
  show ?thesis by fastforce
Andreas@63561
   388
qed
Andreas@63561
   389
Andreas@63561
   390
lemma fixp_above_conv_while: "fixp_above a = while (\<lambda>A. f A \<noteq> A) f a"
Andreas@63561
   391
unfolding while_def by (rule fixp_above_the_while_option)
Andreas@63561
   392
nipkow@62390
   393
end
Andreas@63561
   394
Andreas@63561
   395
end
Andreas@63561
   396
Andreas@63561
   397
end
Andreas@63561
   398
Andreas@63561
   399
lemma bourbaki_witt_fixpoint_complete_latticeI:
Andreas@63561
   400
  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
Andreas@63561
   401
  assumes "\<And>x. x \<le> f x"
Andreas@63561
   402
  shows "bourbaki_witt_fixpoint Sup {(x, y). x \<le> y} f"
Andreas@63561
   403
by unfold_locales (auto simp: assms Sup_upper order_on_defs Field_def intro: refl_onI transI antisymI Sup_least)
Andreas@63561
   404
Andreas@63561
   405
end