src/HOL/Library/Order_Continuity.thy
author hoelzl
Mon Mar 10 20:04:40 2014 +0100 (2014-03-10)
changeset 56020 f92479477c52
parent 54257 src/HOL/Library/Continuity.thy@5c7a3b6b05a9
child 58881 b9556a055632
permissions -rw-r--r--
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
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@14706
     5
header {* 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
wenzelm@22367
    31
subsection {* Continuity for complete lattices *}
nipkow@21312
    32
wenzelm@22367
    33
definition
hoelzl@56020
    34
  continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
hoelzl@56020
    35
  "continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. mono M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
wenzelm@22367
    36
hoelzl@56020
    37
lemma continuousD: "continuous F \<Longrightarrow> mono M \<Longrightarrow> F (SUP i::nat. M i) = (SUP i. F (M i))"
hoelzl@56020
    38
  by (auto simp: continuous_def)
nipkow@21312
    39
hoelzl@56020
    40
lemma continuous_mono:
hoelzl@56020
    41
  fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
hoelzl@56020
    42
  assumes [simp]: "continuous F" shows "mono F"
nipkow@21312
    43
proof
hoelzl@56020
    44
  fix A B :: "'a" assume [simp]: "A \<le> B"
hoelzl@56020
    45
  have "F B = F (SUP n::nat. if n = 0 then A else B)"
hoelzl@56020
    46
    by (simp add: sup_absorb2 SUP_nat_binary)
hoelzl@56020
    47
  also have "\<dots> = (SUP n::nat. if n = 0 then F A else F B)"
hoelzl@56020
    48
    by (auto simp: continuousD mono_def intro!: SUP_cong)
hoelzl@56020
    49
  finally show "F A \<le> F B"
hoelzl@56020
    50
    by (simp add: SUP_nat_binary le_iff_sup)
nipkow@21312
    51
qed
nipkow@21312
    52
nipkow@21312
    53
lemma continuous_lfp:
hoelzl@56020
    54
  assumes "continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
hoelzl@56020
    55
proof (rule antisym)
nipkow@21312
    56
  note mono = continuous_mono[OF `continuous F`]
hoelzl@56020
    57
  show "?U \<le> lfp F"
hoelzl@56020
    58
  proof (rule SUP_least)
hoelzl@56020
    59
    fix i show "(F ^^ i) bot \<le> lfp F"
nipkow@21312
    60
    proof (induct i)
nipkow@21312
    61
      case (Suc i)
hoelzl@56020
    62
      have "(F ^^ Suc i) bot = F ((F ^^ i) bot)" by simp
hoelzl@56020
    63
      also have "\<dots> \<le> F (lfp F)" by (rule monoD[OF mono Suc])
hoelzl@56020
    64
      also have "\<dots> = lfp F" by (simp add: lfp_unfold[OF mono, symmetric])
nipkow@21312
    65
      finally show ?case .
hoelzl@56020
    66
    qed simp
hoelzl@56020
    67
  qed
hoelzl@56020
    68
  show "lfp F \<le> ?U"
nipkow@21312
    69
  proof (rule lfp_lowerbound)
hoelzl@56020
    70
    have "mono (\<lambda>i::nat. (F ^^ i) bot)"
nipkow@21312
    71
    proof -
hoelzl@56020
    72
      { fix i::nat have "(F ^^ i) bot \<le> (F ^^ (Suc i)) bot"
wenzelm@32960
    73
        proof (induct i)
wenzelm@32960
    74
          case 0 show ?case by simp
wenzelm@32960
    75
        next
wenzelm@32960
    76
          case Suc thus ?case using monoD[OF mono Suc] by auto
wenzelm@32960
    77
        qed }
hoelzl@56020
    78
      thus ?thesis by (auto simp add: mono_iff_le_Suc)
nipkow@21312
    79
    qed
hoelzl@56020
    80
    hence "F ?U = (SUP i. (F ^^ Suc i) bot)" using `continuous F` by (simp add: continuous_def)
hoelzl@56020
    81
    also have "\<dots> \<le> ?U" by (fast intro: SUP_least SUP_upper)
nipkow@21312
    82
    finally show "F ?U \<le> ?U" .
nipkow@21312
    83
  qed
nipkow@21312
    84
qed
nipkow@21312
    85
wenzelm@19736
    86
definition
hoelzl@56020
    87
  down_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
hoelzl@56020
    88
  "down_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
oheimb@11351
    89
hoelzl@56020
    90
lemma down_continuousD: "down_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
hoelzl@56020
    91
  by (auto simp: down_continuous_def)
oheimb@11351
    92
hoelzl@56020
    93
lemma down_continuous_mono:
hoelzl@56020
    94
  fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
hoelzl@56020
    95
  assumes [simp]: "down_continuous F" shows "mono F"
hoelzl@56020
    96
proof
hoelzl@56020
    97
  fix A B :: "'a" assume [simp]: "A \<le> B"
hoelzl@56020
    98
  have "F A = F (INF n::nat. if n = 0 then B else A)"
hoelzl@56020
    99
    by (simp add: inf_absorb2 INF_nat_binary)
hoelzl@56020
   100
  also have "\<dots> = (INF n::nat. if n = 0 then F B else F A)"
hoelzl@56020
   101
    by (auto simp: down_continuousD antimono_def intro!: INF_cong)
hoelzl@56020
   102
  finally show "F A \<le> F B"
hoelzl@56020
   103
    by (simp add: INF_nat_binary le_iff_inf inf_commute)
hoelzl@56020
   104
qed
oheimb@11351
   105
hoelzl@56020
   106
lemma down_continuous_gfp:
hoelzl@56020
   107
  assumes "down_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U")
hoelzl@56020
   108
proof (rule antisym)
hoelzl@56020
   109
  note mono = down_continuous_mono[OF `down_continuous F`]
hoelzl@56020
   110
  show "gfp F \<le> ?U"
hoelzl@56020
   111
  proof (rule INF_greatest)
hoelzl@56020
   112
    fix i show "gfp F \<le> (F ^^ i) top"
hoelzl@56020
   113
    proof (induct i)
hoelzl@56020
   114
      case (Suc i)
hoelzl@56020
   115
      have "gfp F = F (gfp F)" by (simp add: gfp_unfold[OF mono, symmetric])
hoelzl@56020
   116
      also have "\<dots> \<le> F ((F ^^ i) top)" by (rule monoD[OF mono Suc])
hoelzl@56020
   117
      also have "\<dots> = (F ^^ Suc i) top" by simp
hoelzl@56020
   118
      finally show ?case .
hoelzl@56020
   119
    qed simp
hoelzl@56020
   120
  qed
hoelzl@56020
   121
  show "?U \<le> gfp F"
hoelzl@56020
   122
  proof (rule gfp_upperbound)
hoelzl@56020
   123
    have *: "antimono (\<lambda>i::nat. (F ^^ i) top)"
hoelzl@56020
   124
    proof -
hoelzl@56020
   125
      { fix i::nat have "(F ^^ Suc i) top \<le> (F ^^ i) top"
hoelzl@56020
   126
        proof (induct i)
hoelzl@56020
   127
          case 0 show ?case by simp
hoelzl@56020
   128
        next
hoelzl@56020
   129
          case Suc thus ?case using monoD[OF mono Suc] by auto
hoelzl@56020
   130
        qed }
hoelzl@56020
   131
      thus ?thesis by (auto simp add: antimono_iff_le_Suc)
hoelzl@56020
   132
    qed
hoelzl@56020
   133
    have "?U \<le> (INF i. (F ^^ Suc i) top)"
hoelzl@56020
   134
      by (fast intro: INF_greatest INF_lower)
hoelzl@56020
   135
    also have "\<dots> \<le> F ?U"
hoelzl@56020
   136
      by (simp add: down_continuousD `down_continuous F` *)
hoelzl@56020
   137
    finally show "?U \<le> F ?U" .
hoelzl@56020
   138
  qed
hoelzl@56020
   139
qed
oheimb@11351
   140
oheimb@11351
   141
end