src/HOL/Library/Order_Continuity.thy
author hoelzl
Mon May 04 17:35:31 2015 +0200 (2015-05-04)
changeset 60172 423273355b55
parent 58881 b9556a055632
child 60427 b4b672f09270
permissions -rw-r--r--
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
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@58881
     5
section {* Continuity and iterations (of set transformers) *}
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@22367
    37
subsection {* Continuity for complete lattices *}
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)
hoelzl@60172
    62
  note mono = sup_continuous_mono[OF `sup_continuous F`]
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)"
hoelzl@60172
    87
      using `sup_continuous F` 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
wenzelm@19736
    94
definition
hoelzl@60172
    95
  inf_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
hoelzl@60172
    96
  "inf_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
oheimb@11351
    97
hoelzl@60172
    98
lemma inf_continuousD: "inf_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
hoelzl@60172
    99
  by (auto simp: inf_continuous_def)
oheimb@11351
   100
hoelzl@60172
   101
lemma inf_continuous_mono:
hoelzl@56020
   102
  fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
hoelzl@60172
   103
  assumes [simp]: "inf_continuous F" shows "mono F"
hoelzl@56020
   104
proof
hoelzl@56020
   105
  fix A B :: "'a" assume [simp]: "A \<le> B"
hoelzl@56020
   106
  have "F A = F (INF n::nat. if n = 0 then B else A)"
hoelzl@56020
   107
    by (simp add: inf_absorb2 INF_nat_binary)
hoelzl@56020
   108
  also have "\<dots> = (INF n::nat. if n = 0 then F B else F A)"
hoelzl@60172
   109
    by (auto simp: inf_continuousD antimono_def intro!: INF_cong)
hoelzl@56020
   110
  finally show "F A \<le> F B"
hoelzl@56020
   111
    by (simp add: INF_nat_binary le_iff_inf inf_commute)
hoelzl@56020
   112
qed
oheimb@11351
   113
hoelzl@60172
   114
lemma inf_continuous_gfp:
hoelzl@60172
   115
  assumes "inf_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U")
hoelzl@56020
   116
proof (rule antisym)
hoelzl@60172
   117
  note mono = inf_continuous_mono[OF `inf_continuous F`]
hoelzl@56020
   118
  show "gfp F \<le> ?U"
hoelzl@56020
   119
  proof (rule INF_greatest)
hoelzl@56020
   120
    fix i show "gfp F \<le> (F ^^ i) top"
hoelzl@56020
   121
    proof (induct i)
hoelzl@56020
   122
      case (Suc i)
hoelzl@56020
   123
      have "gfp F = F (gfp F)" by (simp add: gfp_unfold[OF mono, symmetric])
hoelzl@56020
   124
      also have "\<dots> \<le> F ((F ^^ i) top)" by (rule monoD[OF mono Suc])
hoelzl@56020
   125
      also have "\<dots> = (F ^^ Suc i) top" by simp
hoelzl@56020
   126
      finally show ?case .
hoelzl@56020
   127
    qed simp
hoelzl@56020
   128
  qed
hoelzl@56020
   129
  show "?U \<le> gfp F"
hoelzl@56020
   130
  proof (rule gfp_upperbound)
hoelzl@56020
   131
    have *: "antimono (\<lambda>i::nat. (F ^^ i) top)"
hoelzl@56020
   132
    proof -
hoelzl@56020
   133
      { fix i::nat have "(F ^^ Suc i) top \<le> (F ^^ i) top"
hoelzl@56020
   134
        proof (induct i)
hoelzl@56020
   135
          case 0 show ?case by simp
hoelzl@56020
   136
        next
hoelzl@56020
   137
          case Suc thus ?case using monoD[OF mono Suc] by auto
hoelzl@56020
   138
        qed }
hoelzl@56020
   139
      thus ?thesis by (auto simp add: antimono_iff_le_Suc)
hoelzl@56020
   140
    qed
hoelzl@56020
   141
    have "?U \<le> (INF i. (F ^^ Suc i) top)"
hoelzl@56020
   142
      by (fast intro: INF_greatest INF_lower)
hoelzl@56020
   143
    also have "\<dots> \<le> F ?U"
hoelzl@60172
   144
      by (simp add: inf_continuousD `inf_continuous F` *)
hoelzl@56020
   145
    finally show "?U \<le> F ?U" .
hoelzl@56020
   146
  qed
hoelzl@56020
   147
qed
oheimb@11351
   148
oheimb@11351
   149
end