src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
author wenzelm
Tue Jan 05 13:48:51 2016 +0100 (2016-01-05)
changeset 62058 1cfd5d604937
parent 61766 507b39df1a57
child 62141 00bfdf4bf237
permissions -rw-r--r--
updated headers;
wenzelm@62058
     1
(*  Title:      HOL/Library/Bourbaki_Witt_Fixpoint.thy
wenzelm@62058
     2
    Author:     Andreas Lochbihler, ETH Zurich
wenzelm@62058
     3
*)
Andreas@61766
     4
Andreas@61766
     5
section \<open>The Bourbaki-Witt tower construction for transfinite iteration\<close>
Andreas@61766
     6
Andreas@61766
     7
theory Bourbaki_Witt_Fixpoint imports Main begin
Andreas@61766
     8
Andreas@61766
     9
lemma ChainsI [intro?]:
Andreas@61766
    10
  "(\<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
    11
unfolding Chains_def by blast
Andreas@61766
    12
Andreas@61766
    13
lemma in_Chains_subset: "\<lbrakk> M \<in> Chains r; M' \<subseteq> M \<rbrakk> \<Longrightarrow> M' \<in> Chains r"
Andreas@61766
    14
by(auto simp add: Chains_def)
Andreas@61766
    15
Andreas@61766
    16
lemma FieldI1: "(i, j) \<in> R \<Longrightarrow> i \<in> Field R"
Andreas@61766
    17
  unfolding Field_def by auto
Andreas@61766
    18
Andreas@61766
    19
lemma Chains_FieldD: "\<lbrakk> M \<in> Chains r; x \<in> M \<rbrakk> \<Longrightarrow> x \<in> Field r"
Andreas@61766
    20
by(auto simp add: Chains_def intro: FieldI1 FieldI2)
Andreas@61766
    21
Andreas@61766
    22
lemma partial_order_on_trans:
Andreas@61766
    23
  "\<lbrakk> partial_order_on A r; (x, y) \<in> r; (y, z) \<in> r \<rbrakk> \<Longrightarrow> (x, z) \<in> r"
Andreas@61766
    24
by(auto simp add: order_on_defs dest: transD)
Andreas@61766
    25
Andreas@61766
    26
locale bourbaki_witt_fixpoint =
Andreas@61766
    27
  fixes lub :: "'a set \<Rightarrow> 'a"
Andreas@61766
    28
  and leq :: "('a \<times> 'a) set"
Andreas@61766
    29
  and f :: "'a \<Rightarrow> 'a"
Andreas@61766
    30
  assumes po: "Partial_order leq"
Andreas@61766
    31
  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
    32
  and lub_upper: "\<lbrakk> M \<in> Chains leq; x \<in> M \<rbrakk> \<Longrightarrow> (x, lub M) \<in> leq"
Andreas@61766
    33
  and lub_in_Field: "\<lbrakk> M \<in> Chains leq; M \<noteq> {} \<rbrakk> \<Longrightarrow> lub M \<in> Field leq"
Andreas@61766
    34
  and increasing: "\<And>x. x \<in> Field leq \<Longrightarrow> (x, f x) \<in> leq"
Andreas@61766
    35
begin
Andreas@61766
    36
Andreas@61766
    37
lemma leq_trans: "\<lbrakk> (x, y) \<in> leq; (y, z) \<in> leq \<rbrakk> \<Longrightarrow> (x, z) \<in> leq"
Andreas@61766
    38
by(rule partial_order_on_trans[OF po])
Andreas@61766
    39
Andreas@61766
    40
lemma leq_refl: "x \<in> Field leq \<Longrightarrow> (x, x) \<in> leq"
Andreas@61766
    41
using po by(simp add: order_on_defs refl_on_def)
Andreas@61766
    42
Andreas@61766
    43
lemma leq_antisym: "\<lbrakk> (x, y) \<in> leq; (y, x) \<in> leq \<rbrakk> \<Longrightarrow> x = y"
Andreas@61766
    44
using po by(simp add: order_on_defs antisym_def)
Andreas@61766
    45
Andreas@61766
    46
inductive_set iterates_above :: "'a \<Rightarrow> 'a set"
Andreas@61766
    47
  for a
Andreas@61766
    48
where
Andreas@61766
    49
  base: "a \<in> iterates_above a"
Andreas@61766
    50
| step: "x \<in> iterates_above a \<Longrightarrow> f x \<in> iterates_above a"
Andreas@61766
    51
| 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
    52
Andreas@61766
    53
definition fixp_above :: "'a \<Rightarrow> 'a"
Andreas@61766
    54
where "fixp_above a = lub (iterates_above a)"
Andreas@61766
    55
Andreas@61766
    56
context 
Andreas@61766
    57
  notes leq_refl [intro!, simp]
Andreas@61766
    58
  and base [intro]
Andreas@61766
    59
  and step [intro]
Andreas@61766
    60
  and Sup [intro]
Andreas@61766
    61
  and leq_trans [trans]
Andreas@61766
    62
begin
Andreas@61766
    63
Andreas@61766
    64
lemma iterates_above_le_f: "\<lbrakk> x \<in> iterates_above a; a \<in> Field leq \<rbrakk> \<Longrightarrow> (x, f x) \<in> leq"
Andreas@61766
    65
by(induction x rule: iterates_above.induct)(blast intro: increasing FieldI2 lub_in_Field)+
Andreas@61766
    66
Andreas@61766
    67
lemma iterates_above_Field: "\<lbrakk> x \<in> iterates_above a; a \<in> Field leq \<rbrakk> \<Longrightarrow> x \<in> Field leq"
Andreas@61766
    68
by(drule (1) iterates_above_le_f)(rule FieldI1)
Andreas@61766
    69
Andreas@61766
    70
lemma iterates_above_ge:
Andreas@61766
    71
  assumes y: "y \<in> iterates_above a"
Andreas@61766
    72
  and a: "a \<in> Field leq"
Andreas@61766
    73
  shows "(a, y) \<in> leq"
Andreas@61766
    74
using y by(induction)(auto intro: a increasing iterates_above_le_f leq_trans leq_trans[OF _ lub_upper])
Andreas@61766
    75
Andreas@61766
    76
lemma iterates_above_lub:
Andreas@61766
    77
  assumes M: "M \<in> Chains leq"
Andreas@61766
    78
  and nempty: "M \<noteq> {}"
Andreas@61766
    79
  and upper: "\<And>y. y \<in> M \<Longrightarrow> \<exists>z \<in> M. (y, z) \<in> leq \<and> z \<in> iterates_above a"
Andreas@61766
    80
  shows "lub M \<in> iterates_above a"
Andreas@61766
    81
proof -
Andreas@61766
    82
  let ?M = "M \<inter> iterates_above a"
Andreas@61766
    83
  from M have M': "?M \<in> Chains leq" by(rule in_Chains_subset)simp
Andreas@61766
    84
  have "?M \<noteq> {}" using nempty by(auto dest: upper)
Andreas@61766
    85
  with M' have "lub ?M \<in> iterates_above a" by(rule Sup) blast
Andreas@61766
    86
  also have "lub ?M = lub M" using nempty
Andreas@61766
    87
    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
    88
  finally show ?thesis .
Andreas@61766
    89
qed
Andreas@61766
    90
Andreas@61766
    91
lemma iterates_above_successor:
Andreas@61766
    92
  assumes y: "y \<in> iterates_above a"
Andreas@61766
    93
  and a: "a \<in> Field leq"
Andreas@61766
    94
  shows "y = a \<or> y \<in> iterates_above (f a)"
Andreas@61766
    95
using y
Andreas@61766
    96
proof induction
Andreas@61766
    97
  case base thus ?case by simp
Andreas@61766
    98
next
Andreas@61766
    99
  case (step x) thus ?case by auto
Andreas@61766
   100
next
Andreas@61766
   101
  case (Sup M)
Andreas@61766
   102
  show ?case
Andreas@61766
   103
  proof(cases "\<exists>x. M \<subseteq> {x}")
Andreas@61766
   104
    case True
Andreas@61766
   105
    with \<open>M \<noteq> {}\<close> obtain y where M: "M = {y}" by auto
Andreas@61766
   106
    have "lub M = y"
Andreas@61766
   107
      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
   108
    with Sup.IH[of y] M show ?thesis by simp
Andreas@61766
   109
  next
Andreas@61766
   110
    case False
Andreas@61766
   111
    from Sup(1-2) have "lub M \<in> iterates_above (f a)"
Andreas@61766
   112
    proof(rule iterates_above_lub)
Andreas@61766
   113
      fix y
Andreas@61766
   114
      assume y: "y \<in> M"
Andreas@61766
   115
      from Sup.IH[OF this] show "\<exists>z\<in>M. (y, z) \<in> leq \<and> z \<in> iterates_above (f a)"
Andreas@61766
   116
      proof
Andreas@61766
   117
        assume "y = a"
Andreas@61766
   118
        from y False obtain z where z: "z \<in> M" and neq: "y \<noteq> z" by (metis insertI1 subsetI)
Andreas@61766
   119
        with Sup.IH[OF z] \<open>y = a\<close> Sup.hyps(3)[OF z]
Andreas@61766
   120
        show ?thesis by(auto dest: iterates_above_ge intro: a)
Andreas@61766
   121
      next
Andreas@61766
   122
        assume "y \<in> iterates_above (f a)"
Andreas@61766
   123
        moreover with increasing[OF a] have "y \<in> Field leq"
Andreas@61766
   124
          by(auto dest!: iterates_above_Field intro: FieldI2)
Andreas@61766
   125
        ultimately show ?thesis using y by(auto)
Andreas@61766
   126
      qed
Andreas@61766
   127
    qed
Andreas@61766
   128
    thus ?thesis by simp
Andreas@61766
   129
  qed
Andreas@61766
   130
qed
Andreas@61766
   131
Andreas@61766
   132
lemma iterates_above_Sup_aux:
Andreas@61766
   133
  assumes M: "M \<in> Chains leq" "M \<noteq> {}"
Andreas@61766
   134
  and M': "M' \<in> Chains leq" "M' \<noteq> {}"
Andreas@61766
   135
  and comp: "\<And>x. x \<in> M \<Longrightarrow> x \<in> iterates_above (lub M') \<or> lub M' \<in> iterates_above x"
Andreas@61766
   136
  shows "(lub M, lub M') \<in> leq \<or> lub M \<in> iterates_above (lub M')"
Andreas@61766
   137
proof(cases "\<exists>x \<in> M. x \<in> iterates_above (lub M')")
Andreas@61766
   138
  case True
Andreas@61766
   139
  then obtain x where x: "x \<in> M" "x \<in> iterates_above (lub M')" by blast
Andreas@61766
   140
  have lub_M': "lub M' \<in> Field leq" using M' by(rule lub_in_Field)
Andreas@61766
   141
  have "lub M \<in> iterates_above (lub M')" using M
Andreas@61766
   142
  proof(rule iterates_above_lub)
Andreas@61766
   143
    fix y
Andreas@61766
   144
    assume y: "y \<in> M"
Andreas@61766
   145
    from comp[OF y] show "\<exists>z\<in>M. (y, z) \<in> leq \<and> z \<in> iterates_above (lub M')"
Andreas@61766
   146
    proof
Andreas@61766
   147
      assume "y \<in> iterates_above (lub M')"
Andreas@61766
   148
      from this iterates_above_Field[OF this] y lub_M' show ?thesis by blast
Andreas@61766
   149
    next
Andreas@61766
   150
      assume "lub M' \<in> iterates_above y"
Andreas@61766
   151
      hence "(y, lub M') \<in> leq" using Chains_FieldD[OF M(1) y] by(rule iterates_above_ge)
Andreas@61766
   152
      also have "(lub M', x) \<in> leq" using x(2) lub_M' by(rule iterates_above_ge)
Andreas@61766
   153
      finally show ?thesis using x by blast
Andreas@61766
   154
    qed
Andreas@61766
   155
  qed
Andreas@61766
   156
  thus ?thesis ..
Andreas@61766
   157
next
Andreas@61766
   158
  case False
Andreas@61766
   159
  have "(lub M, lub M') \<in> leq" using M
Andreas@61766
   160
  proof(rule lub_least)
Andreas@61766
   161
    fix x
Andreas@61766
   162
    assume x: "x \<in> M"
Andreas@61766
   163
    from comp[OF x] x False have "lub M' \<in> iterates_above x" by auto
Andreas@61766
   164
    moreover from M(1) x have "x \<in> Field leq" by(rule Chains_FieldD)
Andreas@61766
   165
    ultimately show "(x, lub M') \<in> leq" by(rule iterates_above_ge)
Andreas@61766
   166
  qed
Andreas@61766
   167
  thus ?thesis ..
Andreas@61766
   168
qed
Andreas@61766
   169
Andreas@61766
   170
lemma iterates_above_triangle:
Andreas@61766
   171
  assumes x: "x \<in> iterates_above a"
Andreas@61766
   172
  and y: "y \<in> iterates_above a"
Andreas@61766
   173
  and a: "a \<in> Field leq"
Andreas@61766
   174
  shows "x \<in> iterates_above y \<or> y \<in> iterates_above x"
Andreas@61766
   175
using x y
Andreas@61766
   176
proof(induction arbitrary: y)
Andreas@61766
   177
  case base then show ?case by simp
Andreas@61766
   178
next
Andreas@61766
   179
  case (step x) thus ?case using a
Andreas@61766
   180
    by(auto dest: iterates_above_successor intro: iterates_above_Field)
Andreas@61766
   181
next
Andreas@61766
   182
  case x: (Sup M)
Andreas@61766
   183
  hence lub: "lub M \<in> iterates_above a" by blast
Andreas@61766
   184
  from \<open>y \<in> iterates_above a\<close> show ?case
Andreas@61766
   185
  proof(induction)
Andreas@61766
   186
    case base show ?case using lub by simp
Andreas@61766
   187
  next
Andreas@61766
   188
    case (step y) thus ?case using a
Andreas@61766
   189
      by(auto dest: iterates_above_successor intro: iterates_above_Field)
Andreas@61766
   190
  next
Andreas@61766
   191
    case y: (Sup M')
Andreas@61766
   192
    hence lub': "lub M' \<in> iterates_above a" by blast
Andreas@61766
   193
    have *: "x \<in> iterates_above (lub M') \<or> lub M' \<in> iterates_above x" if "x \<in> M" for x
Andreas@61766
   194
      using that lub' by(rule x.IH)
Andreas@61766
   195
    with x(1-2) y(1-2) have "(lub M, lub M') \<in> leq \<or> lub M \<in> iterates_above (lub M')"
Andreas@61766
   196
      by(rule iterates_above_Sup_aux)
Andreas@61766
   197
    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
   198
      by(rule iterates_above_Sup_aux)(blast dest: y.IH)
Andreas@61766
   199
    ultimately show ?case by(auto 4 3 dest: leq_antisym)
Andreas@61766
   200
  qed
Andreas@61766
   201
qed
Andreas@61766
   202
Andreas@61766
   203
lemma chain_iterates_above: 
Andreas@61766
   204
  assumes a: "a \<in> Field leq"
Andreas@61766
   205
  shows "iterates_above a \<in> Chains leq" (is "?C \<in> _")
Andreas@61766
   206
proof (rule ChainsI)
Andreas@61766
   207
  fix x y
Andreas@61766
   208
  assume "x \<in> ?C" "y \<in> ?C"
Andreas@61766
   209
  hence "x \<in> iterates_above y \<or> y \<in> iterates_above x" using a by(rule iterates_above_triangle)
Andreas@61766
   210
  moreover from \<open>x \<in> ?C\<close> a have "x \<in> Field leq" by(rule iterates_above_Field)
Andreas@61766
   211
  moreover from \<open>y \<in> ?C\<close> a have "y \<in> Field leq" by(rule iterates_above_Field)
Andreas@61766
   212
  ultimately show "(x, y) \<in> leq \<or> (y, x) \<in> leq" by(auto dest: iterates_above_ge)
Andreas@61766
   213
qed
Andreas@61766
   214
Andreas@61766
   215
lemma fixp_iterates_above: "a \<in> Field leq \<Longrightarrow> fixp_above a \<in> iterates_above a"
Andreas@61766
   216
unfolding fixp_above_def by(rule iterates_above.Sup)(blast intro: chain_iterates_above)+
Andreas@61766
   217
Andreas@61766
   218
lemma
Andreas@61766
   219
  assumes b: "b \<in> iterates_above a"
Andreas@61766
   220
  and fb: "f b = b"
Andreas@61766
   221
  and x: "x \<in> iterates_above a"
Andreas@61766
   222
  and a: "a \<in> Field leq"
Andreas@61766
   223
  shows "b \<in> iterates_above x"
Andreas@61766
   224
using x
Andreas@61766
   225
proof(induction)
Andreas@61766
   226
  case base show ?case using b by simp
Andreas@61766
   227
next
Andreas@61766
   228
  case (step x)
Andreas@61766
   229
  from step.hyps a have "x \<in> Field leq" by(rule iterates_above_Field)
Andreas@61766
   230
  from iterates_above_successor[OF step.IH this] fb
Andreas@61766
   231
  show ?case by(auto)
Andreas@61766
   232
next
Andreas@61766
   233
  case (Sup M)
Andreas@61766
   234
  oops
Andreas@61766
   235
Andreas@61766
   236
lemma fixp_above_Field: "a \<in> Field leq \<Longrightarrow> fixp_above a \<in> Field leq"
Andreas@61766
   237
using fixp_iterates_above by(rule iterates_above_Field)
Andreas@61766
   238
Andreas@61766
   239
lemma fixp_above_unfold:
Andreas@61766
   240
  assumes a: "a \<in> Field leq"
Andreas@61766
   241
  shows "fixp_above a = f (fixp_above a)" (is "?a = f ?a")
Andreas@61766
   242
proof(rule leq_antisym)
Andreas@61766
   243
  show "(?a, f ?a) \<in> leq" using fixp_above_Field[OF a] by(rule increasing)
Andreas@61766
   244
  
Andreas@61766
   245
  have "f ?a \<in> iterates_above a" using fixp_iterates_above[OF a] by(rule iterates_above.step)
Andreas@61766
   246
  with chain_iterates_above[OF a] show "(f ?a, ?a) \<in> leq" unfolding fixp_above_def by(rule lub_upper)
Andreas@61766
   247
qed
Andreas@61766
   248
Andreas@61766
   249
end
Andreas@61766
   250
Andreas@61766
   251
end
Andreas@61766
   252
Andreas@61766
   253
end