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