src/HOL/Library/Lub_Glb.thy
author Manuel Eberl <eberlm@in.tum.de>
Mon Mar 26 16:14:16 2018 +0200 (19 months ago)
changeset 67951 655aa11359dc
parent 67613 ce654b0e6d69
child 68356 46d5a9f428e1
permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
wenzelm@58810
     1
(*  Title:      HOL/Library/Lub_Glb.thy
hoelzl@54263
     2
    Author:     Jacques D. Fleuriot, University of Cambridge
hoelzl@54263
     3
    Author:     Amine Chaieb, University of Cambridge *)
hoelzl@54263
     4
wenzelm@60500
     5
section \<open>Definitions of Least Upper Bounds and Greatest Lower Bounds\<close>
hoelzl@54263
     6
wenzelm@58810
     7
theory Lub_Glb
hoelzl@54263
     8
imports Complex_Main
hoelzl@54263
     9
begin
hoelzl@54263
    10
wenzelm@60500
    11
text \<open>Thanks to suggestions by James Margetson\<close>
hoelzl@54263
    12
hoelzl@54263
    13
definition setle :: "'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"  (infixl "*<=" 70)
wenzelm@67613
    14
  where "S *<= x = (\<forall>y\<in>S. y \<le> x)"
hoelzl@54263
    15
hoelzl@54263
    16
definition setge :: "'a::ord \<Rightarrow> 'a set \<Rightarrow> bool"  (infixl "<=*" 70)
wenzelm@67613
    17
  where "x <=* S = (\<forall>y\<in>S. x \<le> y)"
hoelzl@54263
    18
hoelzl@54263
    19
wenzelm@61585
    20
subsection \<open>Rules for the Relations \<open>*<=\<close> and \<open><=*\<close>\<close>
hoelzl@54263
    21
wenzelm@67613
    22
lemma setleI: "\<forall>y\<in>S. y \<le> x \<Longrightarrow> S *<= x"
hoelzl@54263
    23
  by (simp add: setle_def)
chaieb@29838
    24
wenzelm@67613
    25
lemma setleD: "S *<= x \<Longrightarrow> y\<in>S \<Longrightarrow> y \<le> x"
hoelzl@54263
    26
  by (simp add: setle_def)
hoelzl@54263
    27
wenzelm@67613
    28
lemma setgeI: "\<forall>y\<in>S. x \<le> y \<Longrightarrow> x <=* S"
hoelzl@54263
    29
  by (simp add: setge_def)
hoelzl@54263
    30
wenzelm@67613
    31
lemma setgeD: "x <=* S \<Longrightarrow> y\<in>S \<Longrightarrow> x \<le> y"
hoelzl@54263
    32
  by (simp add: setge_def)
hoelzl@54263
    33
hoelzl@54263
    34
hoelzl@54263
    35
definition leastP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
hoelzl@54263
    36
  where "leastP P x = (P x \<and> x <=* Collect P)"
hoelzl@54263
    37
hoelzl@54263
    38
definition isUb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
wenzelm@67613
    39
  where "isUb R S x = (S *<= x \<and> x \<in> R)"
hoelzl@54263
    40
hoelzl@54263
    41
definition isLub :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
hoelzl@54263
    42
  where "isLub R S x = leastP (isUb R S) x"
hoelzl@54263
    43
hoelzl@54263
    44
definition ubs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
hoelzl@54263
    45
  where "ubs R S = Collect (isUb R S)"
hoelzl@54263
    46
hoelzl@54263
    47
wenzelm@60500
    48
subsection \<open>Rules about the Operators @{term leastP}, @{term ub} and @{term lub}\<close>
hoelzl@54263
    49
hoelzl@54263
    50
lemma leastPD1: "leastP P x \<Longrightarrow> P x"
hoelzl@54263
    51
  by (simp add: leastP_def)
chaieb@29838
    52
hoelzl@54263
    53
lemma leastPD2: "leastP P x \<Longrightarrow> x <=* Collect P"
hoelzl@54263
    54
  by (simp add: leastP_def)
hoelzl@54263
    55
wenzelm@67613
    56
lemma leastPD3: "leastP P x \<Longrightarrow> y \<in> Collect P \<Longrightarrow> x \<le> y"
hoelzl@54263
    57
  by (blast dest!: leastPD2 setgeD)
hoelzl@54263
    58
hoelzl@54263
    59
lemma isLubD1: "isLub R S x \<Longrightarrow> S *<= x"
hoelzl@54263
    60
  by (simp add: isLub_def isUb_def leastP_def)
hoelzl@54263
    61
wenzelm@67613
    62
lemma isLubD1a: "isLub R S x \<Longrightarrow> x \<in> R"
hoelzl@54263
    63
  by (simp add: isLub_def isUb_def leastP_def)
hoelzl@54263
    64
hoelzl@54263
    65
lemma isLub_isUb: "isLub R S x \<Longrightarrow> isUb R S x"
hoelzl@54263
    66
  unfolding isUb_def by (blast dest: isLubD1 isLubD1a)
hoelzl@54263
    67
wenzelm@67613
    68
lemma isLubD2: "isLub R S x \<Longrightarrow> y \<in> S \<Longrightarrow> y \<le> x"
hoelzl@54263
    69
  by (blast dest!: isLubD1 setleD)
hoelzl@54263
    70
hoelzl@54263
    71
lemma isLubD3: "isLub R S x \<Longrightarrow> leastP (isUb R S) x"
hoelzl@54263
    72
  by (simp add: isLub_def)
hoelzl@54263
    73
hoelzl@54263
    74
lemma isLubI1: "leastP(isUb R S) x \<Longrightarrow> isLub R S x"
hoelzl@54263
    75
  by (simp add: isLub_def)
hoelzl@54263
    76
hoelzl@54263
    77
lemma isLubI2: "isUb R S x \<Longrightarrow> x <=* Collect (isUb R S) \<Longrightarrow> isLub R S x"
hoelzl@54263
    78
  by (simp add: isLub_def leastP_def)
hoelzl@54263
    79
wenzelm@67613
    80
lemma isUbD: "isUb R S x \<Longrightarrow> y \<in> S \<Longrightarrow> y \<le> x"
hoelzl@54263
    81
  by (simp add: isUb_def setle_def)
hoelzl@54263
    82
hoelzl@54263
    83
lemma isUbD2: "isUb R S x \<Longrightarrow> S *<= x"
hoelzl@54263
    84
  by (simp add: isUb_def)
hoelzl@54263
    85
wenzelm@67613
    86
lemma isUbD2a: "isUb R S x \<Longrightarrow> x \<in> R"
hoelzl@54263
    87
  by (simp add: isUb_def)
hoelzl@54263
    88
wenzelm@67613
    89
lemma isUbI: "S *<= x \<Longrightarrow> x \<in> R \<Longrightarrow> isUb R S x"
hoelzl@54263
    90
  by (simp add: isUb_def)
hoelzl@54263
    91
hoelzl@54263
    92
lemma isLub_le_isUb: "isLub R S x \<Longrightarrow> isUb R S y \<Longrightarrow> x \<le> y"
hoelzl@54263
    93
  unfolding isLub_def by (blast intro!: leastPD3)
hoelzl@54263
    94
hoelzl@54263
    95
lemma isLub_ubs: "isLub R S x \<Longrightarrow> x <=* ubs R S"
hoelzl@54263
    96
  unfolding ubs_def isLub_def by (rule leastPD2)
hoelzl@54263
    97
hoelzl@54263
    98
lemma isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::'a::linorder)"
hoelzl@54263
    99
  apply (frule isLub_isUb)
hoelzl@54263
   100
  apply (frule_tac x = y in isLub_isUb)
hoelzl@54263
   101
  apply (blast intro!: order_antisym dest!: isLub_le_isUb)
hoelzl@54263
   102
  done
hoelzl@54263
   103
hoelzl@54263
   104
lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u"
hoelzl@54263
   105
  by (simp add: isUbI setleI)
hoelzl@54263
   106
chaieb@29838
   107
wenzelm@46509
   108
definition greatestP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
wenzelm@46509
   109
  where "greatestP P x = (P x \<and> Collect P *<=  x)"
chaieb@29838
   110
wenzelm@46509
   111
definition isLb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
wenzelm@67613
   112
  where "isLb R S x = (x <=* S \<and> x \<in> R)"
chaieb@29838
   113
wenzelm@46509
   114
definition isGlb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
wenzelm@46509
   115
  where "isGlb R S x = greatestP (isLb R S) x"
chaieb@29838
   116
wenzelm@46509
   117
definition lbs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
wenzelm@46509
   118
  where "lbs R S = Collect (isLb R S)"
wenzelm@46509
   119
chaieb@29838
   120
wenzelm@60500
   121
subsection \<open>Rules about the Operators @{term greatestP}, @{term isLb} and @{term isGlb}\<close>
chaieb@29838
   122
hoelzl@54263
   123
lemma greatestPD1: "greatestP P x \<Longrightarrow> P x"
wenzelm@46509
   124
  by (simp add: greatestP_def)
chaieb@29838
   125
wenzelm@46509
   126
lemma greatestPD2: "greatestP P x \<Longrightarrow> Collect P *<= x"
wenzelm@46509
   127
  by (simp add: greatestP_def)
chaieb@29838
   128
wenzelm@67613
   129
lemma greatestPD3: "greatestP P x \<Longrightarrow> y \<in> Collect P \<Longrightarrow> x \<ge> y"
wenzelm@46509
   130
  by (blast dest!: greatestPD2 setleD)
chaieb@29838
   131
wenzelm@46509
   132
lemma isGlbD1: "isGlb R S x \<Longrightarrow> x <=* S"
wenzelm@46509
   133
  by (simp add: isGlb_def isLb_def greatestP_def)
chaieb@29838
   134
wenzelm@67613
   135
lemma isGlbD1a: "isGlb R S x \<Longrightarrow> x \<in> R"
wenzelm@46509
   136
  by (simp add: isGlb_def isLb_def greatestP_def)
chaieb@29838
   137
wenzelm@46509
   138
lemma isGlb_isLb: "isGlb R S x \<Longrightarrow> isLb R S x"
wenzelm@46509
   139
  unfolding isLb_def by (blast dest: isGlbD1 isGlbD1a)
chaieb@29838
   140
wenzelm@67613
   141
lemma isGlbD2: "isGlb R S x \<Longrightarrow> y \<in> S \<Longrightarrow> y \<ge> x"
wenzelm@46509
   142
  by (blast dest!: isGlbD1 setgeD)
chaieb@29838
   143
wenzelm@46509
   144
lemma isGlbD3: "isGlb R S x \<Longrightarrow> greatestP (isLb R S) x"
wenzelm@46509
   145
  by (simp add: isGlb_def)
chaieb@29838
   146
wenzelm@46509
   147
lemma isGlbI1: "greatestP (isLb R S) x \<Longrightarrow> isGlb R S x"
wenzelm@46509
   148
  by (simp add: isGlb_def)
chaieb@29838
   149
wenzelm@46509
   150
lemma isGlbI2: "isLb R S x \<Longrightarrow> Collect (isLb R S) *<= x \<Longrightarrow> isGlb R S x"
wenzelm@46509
   151
  by (simp add: isGlb_def greatestP_def)
chaieb@29838
   152
wenzelm@67613
   153
lemma isLbD: "isLb R S x \<Longrightarrow> y \<in> S \<Longrightarrow> y \<ge> x"
wenzelm@46509
   154
  by (simp add: isLb_def setge_def)
chaieb@29838
   155
wenzelm@46509
   156
lemma isLbD2: "isLb R S x \<Longrightarrow> x <=* S "
wenzelm@46509
   157
  by (simp add: isLb_def)
chaieb@29838
   158
wenzelm@67613
   159
lemma isLbD2a: "isLb R S x \<Longrightarrow> x \<in> R"
wenzelm@46509
   160
  by (simp add: isLb_def)
chaieb@29838
   161
wenzelm@67613
   162
lemma isLbI: "x <=* S \<Longrightarrow> x \<in> R \<Longrightarrow> isLb R S x"
wenzelm@46509
   163
  by (simp add: isLb_def)
chaieb@29838
   164
wenzelm@46509
   165
lemma isGlb_le_isLb: "isGlb R S x \<Longrightarrow> isLb R S y \<Longrightarrow> x \<ge> y"
wenzelm@46509
   166
  unfolding isGlb_def by (blast intro!: greatestPD3)
chaieb@29838
   167
wenzelm@46509
   168
lemma isGlb_ubs: "isGlb R S x \<Longrightarrow> lbs R S *<= x"
wenzelm@46509
   169
  unfolding lbs_def isGlb_def by (rule greatestPD2)
chaieb@29838
   170
hoelzl@51342
   171
lemma isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::'a::linorder)"
hoelzl@51342
   172
  apply (frule isGlb_isLb)
hoelzl@51342
   173
  apply (frule_tac x = y in isGlb_isLb)
hoelzl@51342
   174
  apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
hoelzl@51342
   175
  done
hoelzl@51342
   176
hoelzl@54263
   177
lemma bdd_above_setle: "bdd_above A \<longleftrightarrow> (\<exists>a. A *<= a)"
hoelzl@54263
   178
  by (auto simp: bdd_above_def setle_def)
hoelzl@54263
   179
hoelzl@54263
   180
lemma bdd_below_setge: "bdd_below A \<longleftrightarrow> (\<exists>a. a <=* A)"
hoelzl@54263
   181
  by (auto simp: bdd_below_def setge_def)
hoelzl@54263
   182
hoelzl@54263
   183
lemma isLub_cSup: 
hoelzl@54263
   184
  "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
hoelzl@54263
   185
  by  (auto simp add: isLub_def setle_def leastP_def isUb_def
hoelzl@54263
   186
            intro!: setgeI cSup_upper cSup_least)
hoelzl@54263
   187
hoelzl@54263
   188
lemma isGlb_cInf: 
hoelzl@54263
   189
  "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. b <=* S) \<Longrightarrow> isGlb UNIV S (Inf S)"
hoelzl@54263
   190
  by  (auto simp add: isGlb_def setge_def greatestP_def isLb_def
hoelzl@54263
   191
            intro!: setleI cInf_lower cInf_greatest)
hoelzl@54263
   192
hoelzl@54263
   193
lemma cSup_le: "(S::'a::conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
hoelzl@54263
   194
  by (metis cSup_least setle_def)
hoelzl@54263
   195
hoelzl@54263
   196
lemma cInf_ge: "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
hoelzl@54263
   197
  by (metis cInf_greatest setge_def)
hoelzl@54263
   198
hoelzl@54263
   199
lemma cSup_bounds:
hoelzl@54263
   200
  fixes S :: "'a :: conditionally_complete_lattice set"
hoelzl@54263
   201
  shows "S \<noteq> {} \<Longrightarrow> a <=* S \<Longrightarrow> S *<= b \<Longrightarrow> a \<le> Sup S \<and> Sup S \<le> b"
hoelzl@54263
   202
  using cSup_least[of S b] cSup_upper2[of _ S a]
hoelzl@54263
   203
  by (auto simp: bdd_above_setle setge_def setle_def)
hoelzl@54263
   204
hoelzl@54263
   205
lemma cSup_unique: "(S::'a :: {conditionally_complete_linorder, no_bot} set) *<= b \<Longrightarrow> (\<forall>b'<b. \<exists>x\<in>S. b' < x) \<Longrightarrow> Sup S = b"
hoelzl@54263
   206
  by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def)
hoelzl@54263
   207
hoelzl@54263
   208
lemma cInf_unique: "b <=* (S::'a :: {conditionally_complete_linorder, no_top} set) \<Longrightarrow> (\<forall>b'>b. \<exists>x\<in>S. b' > x) \<Longrightarrow> Inf S = b"
hoelzl@54263
   209
  by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def)
hoelzl@54263
   210
wenzelm@60500
   211
text\<open>Use completeness of reals (supremum property) to show that any bounded sequence has a least upper bound\<close>
hoelzl@54263
   212
hoelzl@54263
   213
lemma reals_complete: "\<exists>X. X \<in> S \<Longrightarrow> \<exists>Y. isUb (UNIV::real set) S Y \<Longrightarrow> \<exists>t. isLub (UNIV :: real set) S t"
hoelzl@54263
   214
  by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro!: cSup_upper)
hoelzl@54263
   215
hoelzl@54263
   216
lemma Bseq_isUb: "\<And>X :: nat \<Rightarrow> real. Bseq X \<Longrightarrow> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
hoelzl@54263
   217
  by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
hoelzl@54263
   218
hoelzl@54263
   219
lemma Bseq_isLub: "\<And>X :: nat \<Rightarrow> real. Bseq X \<Longrightarrow> \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
hoelzl@54263
   220
  by (blast intro: reals_complete Bseq_isUb)
hoelzl@54263
   221
hoelzl@54263
   222
lemma isLub_mono_imp_LIMSEQ:
hoelzl@54263
   223
  fixes X :: "nat \<Rightarrow> real"
hoelzl@54263
   224
  assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
hoelzl@54263
   225
  assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
wenzelm@61969
   226
  shows "X \<longlonglongrightarrow> u"
hoelzl@54263
   227
proof -
wenzelm@61969
   228
  have "X \<longlonglongrightarrow> (SUP i. X i)"
hoelzl@54263
   229
    using u[THEN isLubD1] X
hoelzl@54263
   230
    by (intro LIMSEQ_incseq_SUP) (auto simp: incseq_def image_def eq_commute bdd_above_setle)
hoelzl@54263
   231
  also have "(SUP i. X i) = u"
hoelzl@54263
   232
    using isLub_cSup[of "range X"] u[THEN isLubD1]
haftmann@62343
   233
    by (intro isLub_unique[OF _ u]) (auto simp add: image_def eq_commute)
hoelzl@54263
   234
  finally show ?thesis .
hoelzl@54263
   235
qed
hoelzl@54263
   236
hoelzl@54263
   237
lemmas real_isGlb_unique = isGlb_unique[where 'a=real]
hoelzl@54263
   238
hoelzl@54263
   239
lemma real_le_inf_subset: "t \<noteq> {} \<Longrightarrow> t \<subseteq> s \<Longrightarrow> \<exists>b. b <=* s \<Longrightarrow> Inf s \<le> Inf (t::real set)"
hoelzl@54263
   240
  by (rule cInf_superset_mono) (auto simp: bdd_below_setge)
hoelzl@54263
   241
hoelzl@54263
   242
lemma real_ge_sup_subset: "t \<noteq> {} \<Longrightarrow> t \<subseteq> s \<Longrightarrow> \<exists>b. s *<= b \<Longrightarrow> Sup s \<ge> Sup (t::real set)"
hoelzl@54263
   243
  by (rule cSup_subset_mono) (auto simp: bdd_above_setle)
hoelzl@54263
   244
chaieb@29838
   245
end