src/HOL/Library/Order_Continuity.thy
author wenzelm
Wed Jun 17 11:03:05 2015 +0200 (2015-06-17)
changeset 60500 903bb1495239
parent 60427 b4b672f09270
child 60614 e39e6881985c
permissions -rw-r--r--
isabelle update_cartouches;
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@60172
    40
  sup_continuous :: "('a::complete_lattice \<Rightarrow> 'a::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@56020
    47
  fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
hoelzl@60172
    48
  assumes [simp]: "sup_continuous F" shows "mono F"
nipkow@21312
    49
proof
hoelzl@56020
    50
  fix A B :: "'a" assume [simp]: "A \<le> B"
hoelzl@56020
    51
  have "F B = F (SUP n::nat. if n = 0 then A else B)"
hoelzl@56020
    52
    by (simp add: sup_absorb2 SUP_nat_binary)
hoelzl@56020
    53
  also have "\<dots> = (SUP n::nat. if n = 0 then F A else F B)"
hoelzl@60172
    54
    by (auto simp: sup_continuousD mono_def intro!: SUP_cong)
hoelzl@56020
    55
  finally show "F A \<le> F B"
hoelzl@56020
    56
    by (simp add: SUP_nat_binary le_iff_sup)
nipkow@21312
    57
qed
nipkow@21312
    58
hoelzl@60172
    59
lemma sup_continuous_lfp:
hoelzl@60172
    60
  assumes "sup_continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
hoelzl@56020
    61
proof (rule antisym)
wenzelm@60500
    62
  note mono = sup_continuous_mono[OF \<open>sup_continuous F\<close>]
hoelzl@56020
    63
  show "?U \<le> lfp F"
hoelzl@56020
    64
  proof (rule SUP_least)
hoelzl@56020
    65
    fix i show "(F ^^ i) bot \<le> lfp F"
nipkow@21312
    66
    proof (induct i)
nipkow@21312
    67
      case (Suc i)
hoelzl@56020
    68
      have "(F ^^ Suc i) bot = F ((F ^^ i) bot)" by simp
hoelzl@56020
    69
      also have "\<dots> \<le> F (lfp F)" by (rule monoD[OF mono Suc])
hoelzl@56020
    70
      also have "\<dots> = lfp F" by (simp add: lfp_unfold[OF mono, symmetric])
nipkow@21312
    71
      finally show ?case .
hoelzl@56020
    72
    qed simp
hoelzl@56020
    73
  qed
hoelzl@56020
    74
  show "lfp F \<le> ?U"
nipkow@21312
    75
  proof (rule lfp_lowerbound)
hoelzl@56020
    76
    have "mono (\<lambda>i::nat. (F ^^ i) bot)"
nipkow@21312
    77
    proof -
hoelzl@56020
    78
      { fix i::nat have "(F ^^ i) bot \<le> (F ^^ (Suc i)) bot"
wenzelm@32960
    79
        proof (induct i)
wenzelm@32960
    80
          case 0 show ?case by simp
wenzelm@32960
    81
        next
wenzelm@32960
    82
          case Suc thus ?case using monoD[OF mono Suc] by auto
wenzelm@32960
    83
        qed }
hoelzl@56020
    84
      thus ?thesis by (auto simp add: mono_iff_le_Suc)
nipkow@21312
    85
    qed
hoelzl@60172
    86
    hence "F ?U = (SUP i. (F ^^ Suc i) bot)"
wenzelm@60500
    87
      using \<open>sup_continuous F\<close> by (simp add: sup_continuous_def)
hoelzl@60172
    88
    also have "\<dots> \<le> ?U"
hoelzl@60172
    89
      by (fast intro: SUP_least SUP_upper)
nipkow@21312
    90
    finally show "F ?U \<le> ?U" .
nipkow@21312
    91
  qed
nipkow@21312
    92
qed
nipkow@21312
    93
hoelzl@60427
    94
lemma lfp_transfer:
hoelzl@60427
    95
  assumes \<alpha>: "sup_continuous \<alpha>" and f: "sup_continuous f" and g: "sup_continuous g"
hoelzl@60427
    96
  assumes [simp]: "\<alpha> bot = bot" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
hoelzl@60427
    97
  shows "\<alpha> (lfp f) = lfp g"
hoelzl@60427
    98
proof -
hoelzl@60427
    99
  have "\<alpha> (lfp f) = (SUP i. \<alpha> ((f^^i) bot))"
hoelzl@60427
   100
    unfolding sup_continuous_lfp[OF f] by (intro f \<alpha> sup_continuousD mono_funpow sup_continuous_mono)
hoelzl@60427
   101
  moreover have "\<alpha> ((f^^i) bot) = (g^^i) bot" for i
hoelzl@60427
   102
    by (induction i; simp)
hoelzl@60427
   103
  ultimately show ?thesis
hoelzl@60427
   104
    unfolding sup_continuous_lfp[OF g] by simp
hoelzl@60427
   105
qed
hoelzl@60427
   106
wenzelm@19736
   107
definition
hoelzl@60172
   108
  inf_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
hoelzl@60172
   109
  "inf_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
oheimb@11351
   110
hoelzl@60172
   111
lemma inf_continuousD: "inf_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
hoelzl@60172
   112
  by (auto simp: inf_continuous_def)
oheimb@11351
   113
hoelzl@60172
   114
lemma inf_continuous_mono:
hoelzl@56020
   115
  fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
hoelzl@60172
   116
  assumes [simp]: "inf_continuous F" shows "mono F"
hoelzl@56020
   117
proof
hoelzl@56020
   118
  fix A B :: "'a" assume [simp]: "A \<le> B"
hoelzl@56020
   119
  have "F A = F (INF n::nat. if n = 0 then B else A)"
hoelzl@56020
   120
    by (simp add: inf_absorb2 INF_nat_binary)
hoelzl@56020
   121
  also have "\<dots> = (INF n::nat. if n = 0 then F B else F A)"
hoelzl@60172
   122
    by (auto simp: inf_continuousD antimono_def intro!: INF_cong)
hoelzl@56020
   123
  finally show "F A \<le> F B"
hoelzl@56020
   124
    by (simp add: INF_nat_binary le_iff_inf inf_commute)
hoelzl@56020
   125
qed
oheimb@11351
   126
hoelzl@60172
   127
lemma inf_continuous_gfp:
hoelzl@60172
   128
  assumes "inf_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U")
hoelzl@56020
   129
proof (rule antisym)
wenzelm@60500
   130
  note mono = inf_continuous_mono[OF \<open>inf_continuous F\<close>]
hoelzl@56020
   131
  show "gfp F \<le> ?U"
hoelzl@56020
   132
  proof (rule INF_greatest)
hoelzl@56020
   133
    fix i show "gfp F \<le> (F ^^ i) top"
hoelzl@56020
   134
    proof (induct i)
hoelzl@56020
   135
      case (Suc i)
hoelzl@56020
   136
      have "gfp F = F (gfp F)" by (simp add: gfp_unfold[OF mono, symmetric])
hoelzl@56020
   137
      also have "\<dots> \<le> F ((F ^^ i) top)" by (rule monoD[OF mono Suc])
hoelzl@56020
   138
      also have "\<dots> = (F ^^ Suc i) top" by simp
hoelzl@56020
   139
      finally show ?case .
hoelzl@56020
   140
    qed simp
hoelzl@56020
   141
  qed
hoelzl@56020
   142
  show "?U \<le> gfp F"
hoelzl@56020
   143
  proof (rule gfp_upperbound)
hoelzl@56020
   144
    have *: "antimono (\<lambda>i::nat. (F ^^ i) top)"
hoelzl@56020
   145
    proof -
hoelzl@56020
   146
      { fix i::nat have "(F ^^ Suc i) top \<le> (F ^^ i) top"
hoelzl@56020
   147
        proof (induct i)
hoelzl@56020
   148
          case 0 show ?case by simp
hoelzl@56020
   149
        next
hoelzl@56020
   150
          case Suc thus ?case using monoD[OF mono Suc] by auto
hoelzl@56020
   151
        qed }
hoelzl@56020
   152
      thus ?thesis by (auto simp add: antimono_iff_le_Suc)
hoelzl@56020
   153
    qed
hoelzl@56020
   154
    have "?U \<le> (INF i. (F ^^ Suc i) top)"
hoelzl@56020
   155
      by (fast intro: INF_greatest INF_lower)
hoelzl@56020
   156
    also have "\<dots> \<le> F ?U"
wenzelm@60500
   157
      by (simp add: inf_continuousD \<open>inf_continuous F\<close> *)
hoelzl@56020
   158
    finally show "?U \<le> F ?U" .
hoelzl@56020
   159
  qed
hoelzl@56020
   160
qed
oheimb@11351
   161
hoelzl@60427
   162
lemma gfp_transfer:
hoelzl@60427
   163
  assumes \<alpha>: "inf_continuous \<alpha>" and f: "inf_continuous f" and g: "inf_continuous g"
hoelzl@60427
   164
  assumes [simp]: "\<alpha> top = top" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
hoelzl@60427
   165
  shows "\<alpha> (gfp f) = gfp g"
hoelzl@60427
   166
proof -
hoelzl@60427
   167
  have "\<alpha> (gfp f) = (INF i. \<alpha> ((f^^i) top))"
hoelzl@60427
   168
    unfolding inf_continuous_gfp[OF f] by (intro f \<alpha> inf_continuousD antimono_funpow inf_continuous_mono)
hoelzl@60427
   169
  moreover have "\<alpha> ((f^^i) top) = (g^^i) top" for i
hoelzl@60427
   170
    by (induction i; simp)
hoelzl@60427
   171
  ultimately show ?thesis
hoelzl@60427
   172
    unfolding inf_continuous_gfp[OF g] by simp
hoelzl@60427
   173
qed
hoelzl@60427
   174
oheimb@11351
   175
end