src/HOL/Library/Order_Continuity.thy
author hoelzl
Tue Jun 30 13:30:04 2015 +0200 (2015-06-30)
changeset 60614 e39e6881985c
parent 60500 903bb1495239
child 60636 ee18efe9b246
permissions -rw-r--r--
generalized inf and sup_continuous; added intro rules
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
wenzelm@46508
     8
imports 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
wenzelm@60500
    37
subsection \<open>Continuity for complete lattices\<close>
nipkow@21312
    38
wenzelm@22367
    39
definition
hoelzl@60614
    40
  sup_continuous :: "('a::complete_lattice \<Rightarrow> 'b::complete_lattice) \<Rightarrow> bool" where
hoelzl@60172
    41
  "sup_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. mono M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
wenzelm@22367
    42
hoelzl@60172
    43
lemma sup_continuousD: "sup_continuous F \<Longrightarrow> mono M \<Longrightarrow> F (SUP i::nat. M i) = (SUP i. F (M i))"
hoelzl@60172
    44
  by (auto simp: sup_continuous_def)
nipkow@21312
    45
hoelzl@60172
    46
lemma sup_continuous_mono:
hoelzl@60172
    47
  assumes [simp]: "sup_continuous F" shows "mono F"
nipkow@21312
    48
proof
hoelzl@56020
    49
  fix A B :: "'a" assume [simp]: "A \<le> B"
hoelzl@56020
    50
  have "F B = F (SUP n::nat. if n = 0 then A else B)"
hoelzl@56020
    51
    by (simp add: sup_absorb2 SUP_nat_binary)
hoelzl@56020
    52
  also have "\<dots> = (SUP n::nat. if n = 0 then F A else F B)"
hoelzl@60172
    53
    by (auto simp: sup_continuousD mono_def intro!: SUP_cong)
hoelzl@56020
    54
  finally show "F A \<le> F B"
hoelzl@56020
    55
    by (simp add: SUP_nat_binary le_iff_sup)
nipkow@21312
    56
qed
nipkow@21312
    57
hoelzl@60614
    58
lemma sup_continuous_intros:
hoelzl@60614
    59
  shows sup_continuous_const: "sup_continuous (\<lambda>x. c)"
hoelzl@60614
    60
    and sup_continuous_id: "sup_continuous (\<lambda>x. x)"
hoelzl@60614
    61
    and sup_continuous_apply: "sup_continuous (\<lambda>f. f x)"
hoelzl@60614
    62
    and sup_continuous_fun: "(\<And>s. sup_continuous (\<lambda>x. P x s)) \<Longrightarrow> sup_continuous P"
hoelzl@60614
    63
 by (auto simp: sup_continuous_def)
hoelzl@60614
    64
hoelzl@60614
    65
lemma sup_continuous_compose:
hoelzl@60614
    66
  assumes f: "sup_continuous f" and g: "sup_continuous g"
hoelzl@60614
    67
  shows "sup_continuous (\<lambda>x. f (g x))"
hoelzl@60614
    68
  unfolding sup_continuous_def
hoelzl@60614
    69
proof safe
hoelzl@60614
    70
  fix M :: "nat \<Rightarrow> 'c" assume "mono M"
hoelzl@60614
    71
  moreover then have "mono (\<lambda>i. g (M i))"
hoelzl@60614
    72
    using sup_continuous_mono[OF g] by (auto simp: mono_def)
hoelzl@60614
    73
  ultimately show "f (g (SUPREMUM UNIV M)) = (SUP i. f (g (M i)))"
hoelzl@60614
    74
    by (auto simp: sup_continuous_def g[THEN sup_continuousD] f[THEN sup_continuousD])
hoelzl@60614
    75
qed
hoelzl@60614
    76
hoelzl@60172
    77
lemma sup_continuous_lfp:
hoelzl@60172
    78
  assumes "sup_continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
hoelzl@56020
    79
proof (rule antisym)
wenzelm@60500
    80
  note mono = sup_continuous_mono[OF \<open>sup_continuous F\<close>]
hoelzl@56020
    81
  show "?U \<le> lfp F"
hoelzl@56020
    82
  proof (rule SUP_least)
hoelzl@56020
    83
    fix i show "(F ^^ i) bot \<le> lfp F"
nipkow@21312
    84
    proof (induct i)
nipkow@21312
    85
      case (Suc i)
hoelzl@56020
    86
      have "(F ^^ Suc i) bot = F ((F ^^ i) bot)" by simp
hoelzl@56020
    87
      also have "\<dots> \<le> F (lfp F)" by (rule monoD[OF mono Suc])
hoelzl@56020
    88
      also have "\<dots> = lfp F" by (simp add: lfp_unfold[OF mono, symmetric])
nipkow@21312
    89
      finally show ?case .
hoelzl@56020
    90
    qed simp
hoelzl@56020
    91
  qed
hoelzl@56020
    92
  show "lfp F \<le> ?U"
nipkow@21312
    93
  proof (rule lfp_lowerbound)
hoelzl@56020
    94
    have "mono (\<lambda>i::nat. (F ^^ i) bot)"
nipkow@21312
    95
    proof -
hoelzl@56020
    96
      { fix i::nat have "(F ^^ i) bot \<le> (F ^^ (Suc i)) bot"
wenzelm@32960
    97
        proof (induct i)
wenzelm@32960
    98
          case 0 show ?case by simp
wenzelm@32960
    99
        next
wenzelm@32960
   100
          case Suc thus ?case using monoD[OF mono Suc] by auto
wenzelm@32960
   101
        qed }
hoelzl@56020
   102
      thus ?thesis by (auto simp add: mono_iff_le_Suc)
nipkow@21312
   103
    qed
hoelzl@60172
   104
    hence "F ?U = (SUP i. (F ^^ Suc i) bot)"
wenzelm@60500
   105
      using \<open>sup_continuous F\<close> by (simp add: sup_continuous_def)
hoelzl@60172
   106
    also have "\<dots> \<le> ?U"
hoelzl@60172
   107
      by (fast intro: SUP_least SUP_upper)
nipkow@21312
   108
    finally show "F ?U \<le> ?U" .
nipkow@21312
   109
  qed
nipkow@21312
   110
qed
nipkow@21312
   111
hoelzl@60427
   112
lemma lfp_transfer:
hoelzl@60427
   113
  assumes \<alpha>: "sup_continuous \<alpha>" and f: "sup_continuous f" and g: "sup_continuous g"
hoelzl@60427
   114
  assumes [simp]: "\<alpha> bot = bot" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
hoelzl@60427
   115
  shows "\<alpha> (lfp f) = lfp g"
hoelzl@60427
   116
proof -
hoelzl@60427
   117
  have "\<alpha> (lfp f) = (SUP i. \<alpha> ((f^^i) bot))"
hoelzl@60427
   118
    unfolding sup_continuous_lfp[OF f] by (intro f \<alpha> sup_continuousD mono_funpow sup_continuous_mono)
hoelzl@60427
   119
  moreover have "\<alpha> ((f^^i) bot) = (g^^i) bot" for i
hoelzl@60427
   120
    by (induction i; simp)
hoelzl@60427
   121
  ultimately show ?thesis
hoelzl@60427
   122
    unfolding sup_continuous_lfp[OF g] by simp
hoelzl@60427
   123
qed
hoelzl@60427
   124
wenzelm@19736
   125
definition
hoelzl@60614
   126
  inf_continuous :: "('a::complete_lattice \<Rightarrow> 'b::complete_lattice) \<Rightarrow> bool" where
hoelzl@60172
   127
  "inf_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
oheimb@11351
   128
hoelzl@60172
   129
lemma inf_continuousD: "inf_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
hoelzl@60172
   130
  by (auto simp: inf_continuous_def)
oheimb@11351
   131
hoelzl@60172
   132
lemma inf_continuous_mono:
hoelzl@60172
   133
  assumes [simp]: "inf_continuous F" shows "mono F"
hoelzl@56020
   134
proof
hoelzl@56020
   135
  fix A B :: "'a" assume [simp]: "A \<le> B"
hoelzl@56020
   136
  have "F A = F (INF n::nat. if n = 0 then B else A)"
hoelzl@56020
   137
    by (simp add: inf_absorb2 INF_nat_binary)
hoelzl@56020
   138
  also have "\<dots> = (INF n::nat. if n = 0 then F B else F A)"
hoelzl@60172
   139
    by (auto simp: inf_continuousD antimono_def intro!: INF_cong)
hoelzl@56020
   140
  finally show "F A \<le> F B"
hoelzl@56020
   141
    by (simp add: INF_nat_binary le_iff_inf inf_commute)
hoelzl@56020
   142
qed
oheimb@11351
   143
hoelzl@60614
   144
lemma inf_continuous_intros:
hoelzl@60614
   145
  shows inf_continuous_const: "inf_continuous (\<lambda>x. c)"
hoelzl@60614
   146
    and inf_continuous_id: "inf_continuous (\<lambda>x. x)"
hoelzl@60614
   147
    and inf_continuous_apply: "inf_continuous (\<lambda>f. f x)"
hoelzl@60614
   148
    and inf_continuous_fun: "(\<And>s. inf_continuous (\<lambda>x. P x s)) \<Longrightarrow> inf_continuous P"
hoelzl@60614
   149
 by (auto simp: inf_continuous_def)
hoelzl@60614
   150
hoelzl@60614
   151
lemma inf_continuous_compose:
hoelzl@60614
   152
  assumes f: "inf_continuous f" and g: "inf_continuous g"
hoelzl@60614
   153
  shows "inf_continuous (\<lambda>x. f (g x))"
hoelzl@60614
   154
  unfolding inf_continuous_def
hoelzl@60614
   155
proof safe
hoelzl@60614
   156
  fix M :: "nat \<Rightarrow> 'c" assume "antimono M"
hoelzl@60614
   157
  moreover then have "antimono (\<lambda>i. g (M i))"
hoelzl@60614
   158
    using inf_continuous_mono[OF g] by (auto simp: mono_def antimono_def)
hoelzl@60614
   159
  ultimately show "f (g (INFIMUM UNIV M)) = (INF i. f (g (M i)))"
hoelzl@60614
   160
    by (auto simp: inf_continuous_def g[THEN inf_continuousD] f[THEN inf_continuousD])
hoelzl@60614
   161
qed
hoelzl@60614
   162
hoelzl@60172
   163
lemma inf_continuous_gfp:
hoelzl@60172
   164
  assumes "inf_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U")
hoelzl@56020
   165
proof (rule antisym)
wenzelm@60500
   166
  note mono = inf_continuous_mono[OF \<open>inf_continuous F\<close>]
hoelzl@56020
   167
  show "gfp F \<le> ?U"
hoelzl@56020
   168
  proof (rule INF_greatest)
hoelzl@56020
   169
    fix i show "gfp F \<le> (F ^^ i) top"
hoelzl@56020
   170
    proof (induct i)
hoelzl@56020
   171
      case (Suc i)
hoelzl@56020
   172
      have "gfp F = F (gfp F)" by (simp add: gfp_unfold[OF mono, symmetric])
hoelzl@56020
   173
      also have "\<dots> \<le> F ((F ^^ i) top)" by (rule monoD[OF mono Suc])
hoelzl@56020
   174
      also have "\<dots> = (F ^^ Suc i) top" by simp
hoelzl@56020
   175
      finally show ?case .
hoelzl@56020
   176
    qed simp
hoelzl@56020
   177
  qed
hoelzl@56020
   178
  show "?U \<le> gfp F"
hoelzl@56020
   179
  proof (rule gfp_upperbound)
hoelzl@56020
   180
    have *: "antimono (\<lambda>i::nat. (F ^^ i) top)"
hoelzl@56020
   181
    proof -
hoelzl@56020
   182
      { fix i::nat have "(F ^^ Suc i) top \<le> (F ^^ i) top"
hoelzl@56020
   183
        proof (induct i)
hoelzl@56020
   184
          case 0 show ?case by simp
hoelzl@56020
   185
        next
hoelzl@56020
   186
          case Suc thus ?case using monoD[OF mono Suc] by auto
hoelzl@56020
   187
        qed }
hoelzl@56020
   188
      thus ?thesis by (auto simp add: antimono_iff_le_Suc)
hoelzl@56020
   189
    qed
hoelzl@56020
   190
    have "?U \<le> (INF i. (F ^^ Suc i) top)"
hoelzl@56020
   191
      by (fast intro: INF_greatest INF_lower)
hoelzl@56020
   192
    also have "\<dots> \<le> F ?U"
wenzelm@60500
   193
      by (simp add: inf_continuousD \<open>inf_continuous F\<close> *)
hoelzl@56020
   194
    finally show "?U \<le> F ?U" .
hoelzl@56020
   195
  qed
hoelzl@56020
   196
qed
oheimb@11351
   197
hoelzl@60427
   198
lemma gfp_transfer:
hoelzl@60427
   199
  assumes \<alpha>: "inf_continuous \<alpha>" and f: "inf_continuous f" and g: "inf_continuous g"
hoelzl@60427
   200
  assumes [simp]: "\<alpha> top = top" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
hoelzl@60427
   201
  shows "\<alpha> (gfp f) = gfp g"
hoelzl@60427
   202
proof -
hoelzl@60427
   203
  have "\<alpha> (gfp f) = (INF i. \<alpha> ((f^^i) top))"
hoelzl@60427
   204
    unfolding inf_continuous_gfp[OF f] by (intro f \<alpha> inf_continuousD antimono_funpow inf_continuous_mono)
hoelzl@60427
   205
  moreover have "\<alpha> ((f^^i) top) = (g^^i) top" for i
hoelzl@60427
   206
    by (induction i; simp)
hoelzl@60427
   207
  ultimately show ?thesis
hoelzl@60427
   208
    unfolding inf_continuous_gfp[OF g] by simp
hoelzl@60427
   209
qed
hoelzl@60427
   210
oheimb@11351
   211
end