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