src/HOL/Library/Order_Continuity.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (3 months ago)
changeset 69946 494934c30f38
parent 69872 bb16c0bb7520
permissions -rw-r--r--
improved code equations taken over from AFP
hoelzl@56020
     1
(*  Title:      HOL/Library/Order_Continuity.thy
hoelzl@62373
     2
    Author:     David von Oheimb, TU München
hoelzl@62373
     3
    Author:     Johannes Hölzl, TU München
oheimb@11351
     4
*)
oheimb@11351
     5
hoelzl@62373
     6
section \<open>Continuity and iterations\<close>
oheimb@11351
     7
hoelzl@56020
     8
theory Order_Continuity
hoelzl@62373
     9
imports Complex_Main Countable_Complete_Lattices
nipkow@15131
    10
begin
oheimb@11351
    11
hoelzl@56020
    12
(* TODO: Generalize theory to chain-complete partial orders *)
hoelzl@56020
    13
hoelzl@56020
    14
lemma SUP_nat_binary:
haftmann@69661
    15
  "(sup A (SUP x\<in>Collect ((<) (0::nat)). B)) = (sup A B::'a::countable_complete_lattice)"
haftmann@69661
    16
  apply (subst image_constant)
haftmann@69661
    17
   apply auto
hoelzl@56020
    18
  done
hoelzl@56020
    19
hoelzl@56020
    20
lemma INF_nat_binary:
haftmann@69661
    21
  "inf A (INF x\<in>Collect ((<) (0::nat)). B) = (inf A B::'a::countable_complete_lattice)"
haftmann@69661
    22
  apply (subst image_constant)
haftmann@69661
    23
   apply auto
hoelzl@56020
    24
  done
hoelzl@56020
    25
hoelzl@60172
    26
text \<open>
wenzelm@61585
    27
  The name \<open>continuous\<close> is already taken in \<open>Complex_Main\<close>, so we use
wenzelm@61585
    28
  \<open>sup_continuous\<close> and \<open>inf_continuous\<close>. These names appear sometimes in literature
hoelzl@60172
    29
  and have the advantage that these names are duals.
hoelzl@60172
    30
\<close>
hoelzl@60172
    31
hoelzl@60636
    32
named_theorems order_continuous_intros
hoelzl@60636
    33
wenzelm@60500
    34
subsection \<open>Continuity for complete lattices\<close>
nipkow@21312
    35
wenzelm@22367
    36
definition
hoelzl@62373
    37
  sup_continuous :: "('a::countable_complete_lattice \<Rightarrow> 'b::countable_complete_lattice) \<Rightarrow> bool"
hoelzl@62373
    38
where
hoelzl@60172
    39
  "sup_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. mono M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
wenzelm@22367
    40
hoelzl@60172
    41
lemma sup_continuousD: "sup_continuous F \<Longrightarrow> mono M \<Longrightarrow> F (SUP i::nat. M i) = (SUP i. F (M i))"
hoelzl@60172
    42
  by (auto simp: sup_continuous_def)
nipkow@21312
    43
hoelzl@60172
    44
lemma sup_continuous_mono:
haftmann@69661
    45
  "mono F" if "sup_continuous F"
nipkow@21312
    46
proof
haftmann@69661
    47
  fix A B :: "'a"
haftmann@69661
    48
  assume "A \<le> B"
haftmann@69661
    49
  let ?f = "\<lambda>n::nat. if n = 0 then A else B"
haftmann@69661
    50
  from \<open>A \<le> B\<close> have "incseq ?f"
haftmann@69661
    51
    by (auto intro: monoI)
haftmann@69661
    52
  with \<open>sup_continuous F\<close> have *: "F (SUP i. ?f i) = (SUP i. F (?f i))"
haftmann@69661
    53
    by (auto dest: sup_continuousD)
haftmann@69661
    54
  from \<open>A \<le> B\<close> have "B = sup A B"
haftmann@69661
    55
    by (simp add: le_iff_sup)
haftmann@69661
    56
  then have "F B = F (sup A B)"
haftmann@69661
    57
    by simp
haftmann@69661
    58
  also have "\<dots> = sup (F A) (F B)"
haftmann@69661
    59
    using * by (simp add: if_distrib SUP_nat_binary cong del: SUP_cong)
hoelzl@56020
    60
  finally show "F A \<le> F B"
haftmann@69661
    61
    by (simp add: le_iff_sup)
nipkow@21312
    62
qed
nipkow@21312
    63
hoelzl@60636
    64
lemma [order_continuous_intros]:
hoelzl@60614
    65
  shows sup_continuous_const: "sup_continuous (\<lambda>x. c)"
hoelzl@60614
    66
    and sup_continuous_id: "sup_continuous (\<lambda>x. x)"
hoelzl@60614
    67
    and sup_continuous_apply: "sup_continuous (\<lambda>f. f x)"
hoelzl@60614
    68
    and sup_continuous_fun: "(\<And>s. sup_continuous (\<lambda>x. P x s)) \<Longrightarrow> sup_continuous P"
hoelzl@60636
    69
    and sup_continuous_If: "sup_continuous F \<Longrightarrow> sup_continuous G \<Longrightarrow> sup_continuous (\<lambda>f. if C then F f else G f)"
haftmann@69861
    70
  by (auto simp: sup_continuous_def image_comp)
hoelzl@60614
    71
hoelzl@60614
    72
lemma sup_continuous_compose:
hoelzl@60614
    73
  assumes f: "sup_continuous f" and g: "sup_continuous g"
hoelzl@60614
    74
  shows "sup_continuous (\<lambda>x. f (g x))"
hoelzl@60614
    75
  unfolding sup_continuous_def
hoelzl@60614
    76
proof safe
wenzelm@63540
    77
  fix M :: "nat \<Rightarrow> 'c"
wenzelm@63540
    78
  assume M: "mono M"
wenzelm@63540
    79
  then have "mono (\<lambda>i. g (M i))"
hoelzl@60614
    80
    using sup_continuous_mono[OF g] by (auto simp: mono_def)
haftmann@69313
    81
  with M show "f (g (Sup (M ` UNIV))) = (SUP i. f (g (M i)))"
hoelzl@60614
    82
    by (auto simp: sup_continuous_def g[THEN sup_continuousD] f[THEN sup_continuousD])
hoelzl@60614
    83
qed
hoelzl@60614
    84
hoelzl@60636
    85
lemma sup_continuous_sup[order_continuous_intros]:
hoelzl@60636
    86
  "sup_continuous f \<Longrightarrow> sup_continuous g \<Longrightarrow> sup_continuous (\<lambda>x. sup (f x) (g x))"
hoelzl@62373
    87
  by (simp add: sup_continuous_def ccSUP_sup_distrib)
hoelzl@60636
    88
hoelzl@60636
    89
lemma sup_continuous_inf[order_continuous_intros]:
hoelzl@62373
    90
  fixes P Q :: "'a :: countable_complete_lattice \<Rightarrow> 'b :: countable_complete_distrib_lattice"
hoelzl@60636
    91
  assumes P: "sup_continuous P" and Q: "sup_continuous Q"
hoelzl@60636
    92
  shows "sup_continuous (\<lambda>x. inf (P x) (Q x))"
hoelzl@60636
    93
  unfolding sup_continuous_def
hoelzl@60636
    94
proof (safe intro!: antisym)
hoelzl@60636
    95
  fix M :: "nat \<Rightarrow> 'a" assume M: "incseq M"
hoelzl@60636
    96
  have "inf (P (SUP i. M i)) (Q (SUP i. M i)) \<le> (SUP j i. inf (P (M i)) (Q (M j)))"
hoelzl@62373
    97
    by (simp add: sup_continuousD[OF P M] sup_continuousD[OF Q M] inf_ccSUP ccSUP_inf)
hoelzl@60636
    98
  also have "\<dots> \<le> (SUP i. inf (P (M i)) (Q (M i)))"
hoelzl@62373
    99
  proof (intro ccSUP_least)
hoelzl@60636
   100
    fix i j from M assms[THEN sup_continuous_mono] show "inf (P (M i)) (Q (M j)) \<le> (SUP i. inf (P (M i)) (Q (M i)))"
hoelzl@62373
   101
      by (intro ccSUP_upper2[of _ "sup i j"] inf_mono) (auto simp: mono_def)
hoelzl@62373
   102
  qed auto
hoelzl@60636
   103
  finally show "inf (P (SUP i. M i)) (Q (SUP i. M i)) \<le> (SUP i. inf (P (M i)) (Q (M i)))" .
hoelzl@62373
   104
hoelzl@60636
   105
  show "(SUP i. inf (P (M i)) (Q (M i))) \<le> inf (P (SUP i. M i)) (Q (SUP i. M i))"
hoelzl@62373
   106
    unfolding sup_continuousD[OF P M] sup_continuousD[OF Q M] by (intro ccSUP_least inf_mono ccSUP_upper) auto
hoelzl@60636
   107
qed
hoelzl@60636
   108
hoelzl@60636
   109
lemma sup_continuous_and[order_continuous_intros]:
hoelzl@60636
   110
  "sup_continuous P \<Longrightarrow> sup_continuous Q \<Longrightarrow> sup_continuous (\<lambda>x. P x \<and> Q x)"
hoelzl@60636
   111
  using sup_continuous_inf[of P Q] by simp
hoelzl@60636
   112
hoelzl@60636
   113
lemma sup_continuous_or[order_continuous_intros]:
hoelzl@60636
   114
  "sup_continuous P \<Longrightarrow> sup_continuous Q \<Longrightarrow> sup_continuous (\<lambda>x. P x \<or> Q x)"
hoelzl@60636
   115
  by (auto simp: sup_continuous_def)
hoelzl@60636
   116
hoelzl@60172
   117
lemma sup_continuous_lfp:
hoelzl@60172
   118
  assumes "sup_continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
hoelzl@56020
   119
proof (rule antisym)
wenzelm@60500
   120
  note mono = sup_continuous_mono[OF \<open>sup_continuous F\<close>]
hoelzl@56020
   121
  show "?U \<le> lfp F"
hoelzl@56020
   122
  proof (rule SUP_least)
hoelzl@56020
   123
    fix i show "(F ^^ i) bot \<le> lfp F"
nipkow@21312
   124
    proof (induct i)
nipkow@21312
   125
      case (Suc i)
hoelzl@56020
   126
      have "(F ^^ Suc i) bot = F ((F ^^ i) bot)" by simp
hoelzl@56020
   127
      also have "\<dots> \<le> F (lfp F)" by (rule monoD[OF mono Suc])
wenzelm@63979
   128
      also have "\<dots> = lfp F" by (simp add: lfp_fixpoint[OF mono])
nipkow@21312
   129
      finally show ?case .
hoelzl@56020
   130
    qed simp
hoelzl@56020
   131
  qed
hoelzl@56020
   132
  show "lfp F \<le> ?U"
nipkow@21312
   133
  proof (rule lfp_lowerbound)
hoelzl@56020
   134
    have "mono (\<lambda>i::nat. (F ^^ i) bot)"
nipkow@21312
   135
    proof -
hoelzl@56020
   136
      { fix i::nat have "(F ^^ i) bot \<le> (F ^^ (Suc i)) bot"
wenzelm@32960
   137
        proof (induct i)
wenzelm@32960
   138
          case 0 show ?case by simp
wenzelm@32960
   139
        next
wenzelm@32960
   140
          case Suc thus ?case using monoD[OF mono Suc] by auto
wenzelm@32960
   141
        qed }
hoelzl@56020
   142
      thus ?thesis by (auto simp add: mono_iff_le_Suc)
nipkow@21312
   143
    qed
hoelzl@60172
   144
    hence "F ?U = (SUP i. (F ^^ Suc i) bot)"
wenzelm@60500
   145
      using \<open>sup_continuous F\<close> by (simp add: sup_continuous_def)
hoelzl@60172
   146
    also have "\<dots> \<le> ?U"
hoelzl@60172
   147
      by (fast intro: SUP_least SUP_upper)
nipkow@21312
   148
    finally show "F ?U \<le> ?U" .
nipkow@21312
   149
  qed
nipkow@21312
   150
qed
nipkow@21312
   151
hoelzl@60636
   152
lemma lfp_transfer_bounded:
hoelzl@60636
   153
  assumes P: "P bot" "\<And>x. P x \<Longrightarrow> P (f x)" "\<And>M. (\<And>i. P (M i)) \<Longrightarrow> P (SUP i::nat. M i)"
hoelzl@60636
   154
  assumes \<alpha>: "\<And>M. mono M \<Longrightarrow> (\<And>i::nat. P (M i)) \<Longrightarrow> \<alpha> (SUP i. M i) = (SUP i. \<alpha> (M i))"
hoelzl@60636
   155
  assumes f: "sup_continuous f" and g: "sup_continuous g"
hoelzl@60714
   156
  assumes [simp]: "\<And>x. P x \<Longrightarrow> x \<le> lfp f \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)"
hoelzl@60636
   157
  assumes g_bound: "\<And>x. \<alpha> bot \<le> g x"
hoelzl@60636
   158
  shows "\<alpha> (lfp f) = lfp g"
hoelzl@60636
   159
proof (rule antisym)
hoelzl@60636
   160
  note mono_g = sup_continuous_mono[OF g]
hoelzl@60714
   161
  note mono_f = sup_continuous_mono[OF f]
hoelzl@60636
   162
  have lfp_bound: "\<alpha> bot \<le> lfp g"
hoelzl@60636
   163
    by (subst lfp_unfold[OF mono_g]) (rule g_bound)
hoelzl@60636
   164
hoelzl@60636
   165
  have P_pow: "P ((f ^^ i) bot)" for i
hoelzl@60636
   166
    by (induction i) (auto intro!: P)
hoelzl@60636
   167
  have incseq_pow: "mono (\<lambda>i. (f ^^ i) bot)"
hoelzl@60636
   168
    unfolding mono_iff_le_Suc
hoelzl@60636
   169
  proof
hoelzl@60636
   170
    fix i show "(f ^^ i) bot \<le> (f ^^ (Suc i)) bot"
hoelzl@60636
   171
    proof (induct i)
hoelzl@60636
   172
      case Suc thus ?case using monoD[OF sup_continuous_mono[OF f] Suc] by auto
hoelzl@60636
   173
    qed (simp add: le_fun_def)
hoelzl@60636
   174
  qed
hoelzl@60636
   175
  have P_lfp: "P (lfp f)"
hoelzl@60636
   176
    using P_pow unfolding sup_continuous_lfp[OF f] by (auto intro!: P)
hoelzl@60636
   177
hoelzl@60714
   178
  have iter_le_lfp: "(f ^^ n) bot \<le> lfp f" for n
hoelzl@60714
   179
    apply (induction n)
hoelzl@60714
   180
    apply simp
hoelzl@60714
   181
    apply (subst lfp_unfold[OF mono_f])
hoelzl@60714
   182
    apply (auto intro!: monoD[OF mono_f])
hoelzl@60714
   183
    done
hoelzl@60714
   184
hoelzl@60636
   185
  have "\<alpha> (lfp f) = (SUP i. \<alpha> ((f^^i) bot))"
hoelzl@60636
   186
    unfolding sup_continuous_lfp[OF f] using incseq_pow P_pow by (rule \<alpha>)
hoelzl@60636
   187
  also have "\<dots> \<le> lfp g"
hoelzl@60636
   188
  proof (rule SUP_least)
hoelzl@60636
   189
    fix i show "\<alpha> ((f^^i) bot) \<le> lfp g"
hoelzl@60636
   190
    proof (induction i)
hoelzl@60636
   191
      case (Suc n) then show ?case
hoelzl@60714
   192
        by (subst lfp_unfold[OF mono_g]) (simp add: monoD[OF mono_g] P_pow iter_le_lfp)
hoelzl@60636
   193
    qed (simp add: lfp_bound)
hoelzl@60636
   194
  qed
hoelzl@60636
   195
  finally show "\<alpha> (lfp f) \<le> lfp g" .
hoelzl@60636
   196
hoelzl@60636
   197
  show "lfp g \<le> \<alpha> (lfp f)"
hoelzl@60636
   198
  proof (induction rule: lfp_ordinal_induct[OF mono_g])
hoelzl@60636
   199
    case (1 S) then show ?case
hoelzl@60636
   200
      by (subst lfp_unfold[OF sup_continuous_mono[OF f]])
hoelzl@60636
   201
         (simp add: monoD[OF mono_g] P_lfp)
hoelzl@60636
   202
  qed (auto intro: Sup_least)
hoelzl@60636
   203
qed
hoelzl@60636
   204
hoelzl@60714
   205
lemma lfp_transfer:
hoelzl@60714
   206
  "sup_continuous \<alpha> \<Longrightarrow> sup_continuous f \<Longrightarrow> sup_continuous g \<Longrightarrow>
hoelzl@60714
   207
    (\<And>x. \<alpha> bot \<le> g x) \<Longrightarrow> (\<And>x. x \<le> lfp f \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)) \<Longrightarrow> \<alpha> (lfp f) = lfp g"
hoelzl@60714
   208
  by (rule lfp_transfer_bounded[where P=top]) (auto dest: sup_continuousD)
hoelzl@60714
   209
wenzelm@19736
   210
definition
hoelzl@62373
   211
  inf_continuous :: "('a::countable_complete_lattice \<Rightarrow> 'b::countable_complete_lattice) \<Rightarrow> bool"
hoelzl@62373
   212
where
hoelzl@60172
   213
  "inf_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
oheimb@11351
   214
hoelzl@60172
   215
lemma inf_continuousD: "inf_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
hoelzl@60172
   216
  by (auto simp: inf_continuous_def)
oheimb@11351
   217
hoelzl@60172
   218
lemma inf_continuous_mono:
haftmann@69661
   219
  "mono F" if "inf_continuous F"
hoelzl@56020
   220
proof
haftmann@69661
   221
  fix A B :: "'a"
haftmann@69661
   222
  assume "A \<le> B"
haftmann@69661
   223
  let ?f = "\<lambda>n::nat. if n = 0 then B else A"
haftmann@69661
   224
  from \<open>A \<le> B\<close> have "decseq ?f"
haftmann@69661
   225
    by (auto intro: antimonoI)
haftmann@69661
   226
  with \<open>inf_continuous F\<close> have *: "F (INF i. ?f i) = (INF i. F (?f i))"
haftmann@69661
   227
    by (auto dest: inf_continuousD)
haftmann@69661
   228
  from \<open>A \<le> B\<close> have "A = inf B A"
haftmann@69661
   229
    by (simp add: inf.absorb_iff2)
haftmann@69661
   230
  then have "F A = F (inf B A)"
haftmann@69661
   231
    by simp
haftmann@69661
   232
  also have "\<dots> = inf (F B) (F A)"
haftmann@69661
   233
    using * by (simp add: if_distrib INF_nat_binary cong del: INF_cong)
hoelzl@56020
   234
  finally show "F A \<le> F B"
haftmann@69661
   235
    by (simp add: inf.absorb_iff2)
hoelzl@56020
   236
qed
oheimb@11351
   237
hoelzl@60636
   238
lemma [order_continuous_intros]:
hoelzl@60614
   239
  shows inf_continuous_const: "inf_continuous (\<lambda>x. c)"
hoelzl@60614
   240
    and inf_continuous_id: "inf_continuous (\<lambda>x. x)"
hoelzl@60614
   241
    and inf_continuous_apply: "inf_continuous (\<lambda>f. f x)"
hoelzl@60614
   242
    and inf_continuous_fun: "(\<And>s. inf_continuous (\<lambda>x. P x s)) \<Longrightarrow> inf_continuous P"
hoelzl@60636
   243
    and inf_continuous_If: "inf_continuous F \<Longrightarrow> inf_continuous G \<Longrightarrow> inf_continuous (\<lambda>f. if C then F f else G f)"
haftmann@69861
   244
  by (auto simp: inf_continuous_def image_comp)
hoelzl@60636
   245
hoelzl@60636
   246
lemma inf_continuous_inf[order_continuous_intros]:
hoelzl@60636
   247
  "inf_continuous f \<Longrightarrow> inf_continuous g \<Longrightarrow> inf_continuous (\<lambda>x. inf (f x) (g x))"
hoelzl@62373
   248
  by (simp add: inf_continuous_def ccINF_inf_distrib)
hoelzl@60636
   249
hoelzl@60636
   250
lemma inf_continuous_sup[order_continuous_intros]:
hoelzl@62373
   251
  fixes P Q :: "'a :: countable_complete_lattice \<Rightarrow> 'b :: countable_complete_distrib_lattice"
hoelzl@60636
   252
  assumes P: "inf_continuous P" and Q: "inf_continuous Q"
hoelzl@60636
   253
  shows "inf_continuous (\<lambda>x. sup (P x) (Q x))"
hoelzl@60636
   254
  unfolding inf_continuous_def
hoelzl@60636
   255
proof (safe intro!: antisym)
hoelzl@60636
   256
  fix M :: "nat \<Rightarrow> 'a" assume M: "decseq M"
hoelzl@60636
   257
  show "sup (P (INF i. M i)) (Q (INF i. M i)) \<le> (INF i. sup (P (M i)) (Q (M i)))"
hoelzl@62373
   258
    unfolding inf_continuousD[OF P M] inf_continuousD[OF Q M] by (intro ccINF_greatest sup_mono ccINF_lower) auto
hoelzl@60636
   259
hoelzl@60636
   260
  have "(INF i. sup (P (M i)) (Q (M i))) \<le> (INF j i. sup (P (M i)) (Q (M j)))"
hoelzl@62373
   261
  proof (intro ccINF_greatest)
hoelzl@60636
   262
    fix i j from M assms[THEN inf_continuous_mono] show "sup (P (M i)) (Q (M j)) \<ge> (INF i. sup (P (M i)) (Q (M i)))"
hoelzl@62373
   263
      by (intro ccINF_lower2[of _ "sup i j"] sup_mono) (auto simp: mono_def antimono_def)
hoelzl@62373
   264
  qed auto
hoelzl@60636
   265
  also have "\<dots> \<le> sup (P (INF i. M i)) (Q (INF i. M i))"
hoelzl@62373
   266
    by (simp add: inf_continuousD[OF P M] inf_continuousD[OF Q M] ccINF_sup sup_ccINF)
hoelzl@60636
   267
  finally show "sup (P (INF i. M i)) (Q (INF i. M i)) \<ge> (INF i. sup (P (M i)) (Q (M i)))" .
hoelzl@60636
   268
qed
hoelzl@60636
   269
hoelzl@60636
   270
lemma inf_continuous_and[order_continuous_intros]:
hoelzl@60636
   271
  "inf_continuous P \<Longrightarrow> inf_continuous Q \<Longrightarrow> inf_continuous (\<lambda>x. P x \<and> Q x)"
hoelzl@60636
   272
  using inf_continuous_inf[of P Q] by simp
hoelzl@60636
   273
hoelzl@60636
   274
lemma inf_continuous_or[order_continuous_intros]:
hoelzl@60636
   275
  "inf_continuous P \<Longrightarrow> inf_continuous Q \<Longrightarrow> inf_continuous (\<lambda>x. P x \<or> Q x)"
hoelzl@60636
   276
  using inf_continuous_sup[of P Q] by simp
hoelzl@60614
   277
hoelzl@60614
   278
lemma inf_continuous_compose:
hoelzl@60614
   279
  assumes f: "inf_continuous f" and g: "inf_continuous g"
hoelzl@60614
   280
  shows "inf_continuous (\<lambda>x. f (g x))"
hoelzl@60614
   281
  unfolding inf_continuous_def
hoelzl@60614
   282
proof safe
wenzelm@63540
   283
  fix M :: "nat \<Rightarrow> 'c"
wenzelm@63540
   284
  assume M: "antimono M"
wenzelm@63540
   285
  then have "antimono (\<lambda>i. g (M i))"
hoelzl@60614
   286
    using inf_continuous_mono[OF g] by (auto simp: mono_def antimono_def)
haftmann@69313
   287
  with M show "f (g (Inf (M ` UNIV))) = (INF i. f (g (M i)))"
hoelzl@60614
   288
    by (auto simp: inf_continuous_def g[THEN inf_continuousD] f[THEN inf_continuousD])
hoelzl@60614
   289
qed
hoelzl@60614
   290
hoelzl@60172
   291
lemma inf_continuous_gfp:
hoelzl@60172
   292
  assumes "inf_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U")
hoelzl@56020
   293
proof (rule antisym)
wenzelm@60500
   294
  note mono = inf_continuous_mono[OF \<open>inf_continuous F\<close>]
hoelzl@56020
   295
  show "gfp F \<le> ?U"
hoelzl@56020
   296
  proof (rule INF_greatest)
hoelzl@56020
   297
    fix i show "gfp F \<le> (F ^^ i) top"
hoelzl@56020
   298
    proof (induct i)
hoelzl@56020
   299
      case (Suc i)
wenzelm@63979
   300
      have "gfp F = F (gfp F)" by (simp add: gfp_fixpoint[OF mono])
hoelzl@56020
   301
      also have "\<dots> \<le> F ((F ^^ i) top)" by (rule monoD[OF mono Suc])
hoelzl@56020
   302
      also have "\<dots> = (F ^^ Suc i) top" by simp
hoelzl@56020
   303
      finally show ?case .
hoelzl@56020
   304
    qed simp
hoelzl@56020
   305
  qed
hoelzl@56020
   306
  show "?U \<le> gfp F"
hoelzl@56020
   307
  proof (rule gfp_upperbound)
hoelzl@56020
   308
    have *: "antimono (\<lambda>i::nat. (F ^^ i) top)"
hoelzl@56020
   309
    proof -
hoelzl@56020
   310
      { fix i::nat have "(F ^^ Suc i) top \<le> (F ^^ i) top"
hoelzl@56020
   311
        proof (induct i)
hoelzl@56020
   312
          case 0 show ?case by simp
hoelzl@56020
   313
        next
hoelzl@56020
   314
          case Suc thus ?case using monoD[OF mono Suc] by auto
hoelzl@56020
   315
        qed }
hoelzl@56020
   316
      thus ?thesis by (auto simp add: antimono_iff_le_Suc)
hoelzl@56020
   317
    qed
hoelzl@56020
   318
    have "?U \<le> (INF i. (F ^^ Suc i) top)"
hoelzl@56020
   319
      by (fast intro: INF_greatest INF_lower)
hoelzl@56020
   320
    also have "\<dots> \<le> F ?U"
wenzelm@60500
   321
      by (simp add: inf_continuousD \<open>inf_continuous F\<close> *)
hoelzl@56020
   322
    finally show "?U \<le> F ?U" .
hoelzl@56020
   323
  qed
hoelzl@56020
   324
qed
oheimb@11351
   325
hoelzl@60427
   326
lemma gfp_transfer:
hoelzl@60427
   327
  assumes \<alpha>: "inf_continuous \<alpha>" and f: "inf_continuous f" and g: "inf_continuous g"
hoelzl@60427
   328
  assumes [simp]: "\<alpha> top = top" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
hoelzl@60427
   329
  shows "\<alpha> (gfp f) = gfp g"
hoelzl@60427
   330
proof -
hoelzl@60427
   331
  have "\<alpha> (gfp f) = (INF i. \<alpha> ((f^^i) top))"
hoelzl@60427
   332
    unfolding inf_continuous_gfp[OF f] by (intro f \<alpha> inf_continuousD antimono_funpow inf_continuous_mono)
hoelzl@60427
   333
  moreover have "\<alpha> ((f^^i) top) = (g^^i) top" for i
hoelzl@60427
   334
    by (induction i; simp)
hoelzl@60427
   335
  ultimately show ?thesis
hoelzl@60427
   336
    unfolding inf_continuous_gfp[OF g] by simp
hoelzl@60427
   337
qed
hoelzl@60427
   338
hoelzl@60636
   339
lemma gfp_transfer_bounded:
hoelzl@60636
   340
  assumes P: "P (f top)" "\<And>x. P x \<Longrightarrow> P (f x)" "\<And>M. antimono M \<Longrightarrow> (\<And>i. P (M i)) \<Longrightarrow> P (INF i::nat. M i)"
hoelzl@60636
   341
  assumes \<alpha>: "\<And>M. antimono M \<Longrightarrow> (\<And>i::nat. P (M i)) \<Longrightarrow> \<alpha> (INF i. M i) = (INF i. \<alpha> (M i))"
hoelzl@60636
   342
  assumes f: "inf_continuous f" and g: "inf_continuous g"
hoelzl@60636
   343
  assumes [simp]: "\<And>x. P x \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)"
hoelzl@60636
   344
  assumes g_bound: "\<And>x. g x \<le> \<alpha> (f top)"
hoelzl@60636
   345
  shows "\<alpha> (gfp f) = gfp g"
hoelzl@60636
   346
proof (rule antisym)
hoelzl@60636
   347
  note mono_g = inf_continuous_mono[OF g]
hoelzl@60636
   348
hoelzl@60636
   349
  have P_pow: "P ((f ^^ i) (f top))" for i
hoelzl@60636
   350
    by (induction i) (auto intro!: P)
hoelzl@60636
   351
hoelzl@60636
   352
  have antimono_pow: "antimono (\<lambda>i. (f ^^ i) top)"
hoelzl@60636
   353
    unfolding antimono_iff_le_Suc
hoelzl@60636
   354
  proof
hoelzl@60636
   355
    fix i show "(f ^^ Suc i) top \<le> (f ^^ i) top"
hoelzl@60636
   356
    proof (induct i)
hoelzl@60636
   357
      case Suc thus ?case using monoD[OF inf_continuous_mono[OF f] Suc] by auto
hoelzl@60636
   358
    qed (simp add: le_fun_def)
hoelzl@60636
   359
  qed
hoelzl@60636
   360
  have antimono_pow2: "antimono (\<lambda>i. (f ^^ i) (f top))"
hoelzl@60636
   361
  proof
hoelzl@60636
   362
    show "x \<le> y \<Longrightarrow> (f ^^ y) (f top) \<le> (f ^^ x) (f top)" for x y
hoelzl@60636
   363
      using antimono_pow[THEN antimonoD, of "Suc x" "Suc y"]
hoelzl@60636
   364
      unfolding funpow_Suc_right by simp
hoelzl@60636
   365
  qed
hoelzl@62373
   366
hoelzl@60636
   367
  have gfp_f: "gfp f = (INF i. (f ^^ i) (f top))"
hoelzl@60636
   368
    unfolding inf_continuous_gfp[OF f]
hoelzl@60636
   369
  proof (rule INF_eq)
hoelzl@60636
   370
    show "\<exists>j\<in>UNIV. (f ^^ j) (f top) \<le> (f ^^ i) top" for i
hoelzl@60636
   371
      by (intro bexI[of _ "i - 1"]) (auto simp: diff_Suc funpow_Suc_right simp del: funpow.simps(2) split: nat.split)
hoelzl@60636
   372
    show "\<exists>j\<in>UNIV. (f ^^ j) top \<le> (f ^^ i) (f top)" for i
hoelzl@60636
   373
      by (intro bexI[of _ "Suc i"]) (auto simp: funpow_Suc_right simp del: funpow.simps(2))
hoelzl@60636
   374
  qed
hoelzl@60636
   375
hoelzl@60636
   376
  have P_lfp: "P (gfp f)"
hoelzl@60636
   377
    unfolding gfp_f by (auto intro!: P P_pow antimono_pow2)
hoelzl@60636
   378
hoelzl@60636
   379
  have "\<alpha> (gfp f) = (INF i. \<alpha> ((f^^i) (f top)))"
hoelzl@60636
   380
    unfolding gfp_f by (rule \<alpha>) (auto intro!: P_pow antimono_pow2)
hoelzl@60636
   381
  also have "\<dots> \<ge> gfp g"
hoelzl@60636
   382
  proof (rule INF_greatest)
hoelzl@60636
   383
    fix i show "gfp g \<le> \<alpha> ((f^^i) (f top))"
hoelzl@60636
   384
    proof (induction i)
hoelzl@60636
   385
      case (Suc n) then show ?case
hoelzl@60636
   386
        by (subst gfp_unfold[OF mono_g]) (simp add: monoD[OF mono_g] P_pow)
hoelzl@60636
   387
    next
hoelzl@60636
   388
      case 0
hoelzl@60636
   389
      have "gfp g \<le> \<alpha> (f top)"
hoelzl@60636
   390
        by (subst gfp_unfold[OF mono_g]) (rule g_bound)
hoelzl@60636
   391
      then show ?case
hoelzl@60636
   392
        by simp
hoelzl@60636
   393
    qed
hoelzl@60636
   394
  qed
hoelzl@60636
   395
  finally show "gfp g \<le> \<alpha> (gfp f)" .
hoelzl@60636
   396
hoelzl@60636
   397
  show "\<alpha> (gfp f) \<le> gfp g"
hoelzl@60636
   398
  proof (induction rule: gfp_ordinal_induct[OF mono_g])
hoelzl@60636
   399
    case (1 S) then show ?case
hoelzl@60636
   400
      by (subst gfp_unfold[OF inf_continuous_mono[OF f]])
hoelzl@60636
   401
         (simp add: monoD[OF mono_g] P_lfp)
hoelzl@60636
   402
  qed (auto intro: Inf_greatest)
hoelzl@60636
   403
qed
hoelzl@60636
   404
hoelzl@62373
   405
subsubsection \<open>Least fixed points in countable complete lattices\<close>
hoelzl@62373
   406
hoelzl@62373
   407
definition (in countable_complete_lattice) cclfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
hoelzl@62374
   408
  where "cclfp f = (SUP i. (f ^^ i) bot)"
hoelzl@62373
   409
hoelzl@62373
   410
lemma cclfp_unfold:
hoelzl@62373
   411
  assumes "sup_continuous F" shows "cclfp F = F (cclfp F)"
hoelzl@62373
   412
proof -
hoelzl@62374
   413
  have "cclfp F = (SUP i. F ((F ^^ i) bot))"
haftmann@69861
   414
    unfolding cclfp_def
haftmann@69861
   415
    by (subst UNIV_nat_eq) (simp add: image_comp)
hoelzl@62373
   416
  also have "\<dots> = F (cclfp F)"
hoelzl@62373
   417
    unfolding cclfp_def
hoelzl@62373
   418
    by (intro sup_continuousD[symmetric] assms mono_funpow sup_continuous_mono)
hoelzl@62373
   419
  finally show ?thesis .
hoelzl@62373
   420
qed
hoelzl@62373
   421
hoelzl@62373
   422
lemma cclfp_lowerbound: assumes f: "mono f" and A: "f A \<le> A" shows "cclfp f \<le> A"
hoelzl@62373
   423
  unfolding cclfp_def
hoelzl@62373
   424
proof (intro ccSUP_least)
hoelzl@62374
   425
  fix i show "(f ^^ i) bot \<le> A"
hoelzl@62373
   426
  proof (induction i)
hoelzl@62373
   427
    case (Suc i) from monoD[OF f this] A show ?case
hoelzl@62373
   428
      by auto
hoelzl@62373
   429
  qed simp
hoelzl@62373
   430
qed simp
hoelzl@62373
   431
hoelzl@62373
   432
lemma cclfp_transfer:
hoelzl@62373
   433
  assumes "sup_continuous \<alpha>" "mono f"
hoelzl@62374
   434
  assumes "\<alpha> bot = bot" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
hoelzl@62373
   435
  shows "\<alpha> (cclfp f) = cclfp g"
hoelzl@62373
   436
proof -
hoelzl@62374
   437
  have "\<alpha> (cclfp f) = (SUP i. \<alpha> ((f ^^ i) bot))"
hoelzl@62373
   438
    unfolding cclfp_def by (intro sup_continuousD assms mono_funpow sup_continuous_mono)
hoelzl@62374
   439
  moreover have "\<alpha> ((f ^^ i) bot) = (g ^^ i) bot" for i
hoelzl@62373
   440
    by (induction i) (simp_all add: assms)
hoelzl@62373
   441
  ultimately show ?thesis
hoelzl@62373
   442
    by (simp add: cclfp_def)
hoelzl@62373
   443
qed
hoelzl@62373
   444
oheimb@11351
   445
end