src/HOL/SupInf.thy
author paulson
Tue Oct 27 12:59:57 2009 +0000 (2009-10-27)
changeset 33269 3b7e2dbbd684
child 33271 7be66dee1a5a
permissions -rw-r--r--
New theory SupInf of the supremum and infimum operators for sets of reals.
     1 (*  Author: Amine Chaieb and L C Paulson, University of Cambridge *)
     2 
     3 header {*Sup and Inf Operators on Sets of Reals.*}
     4 
     5 theory SupInf
     6 imports RComplete
     7 begin
     8 
     9 lemma minus_max_eq_min:
    10   fixes x :: "'a::{lordered_ab_group_add, linorder}"
    11   shows "- (max x y) = min (-x) (-y)"
    12 by (metis le_imp_neg_le linorder_linear min_max.inf_absorb2 min_max.le_iff_inf min_max.le_iff_sup min_max.sup_absorb1)
    13 
    14 lemma minus_min_eq_max:
    15   fixes x :: "'a::{lordered_ab_group_add, linorder}"
    16   shows "- (min x y) = max (-x) (-y)"
    17 by (metis minus_max_eq_min minus_minus)
    18 
    19 lemma minus_Max_eq_Min [simp]:
    20   fixes S :: "'a::{lordered_ab_group_add, linorder} set"
    21   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Max S) = Min (uminus ` S)"
    22 proof (induct S rule: finite_ne_induct)
    23   case (singleton x)
    24   thus ?case by simp
    25 next
    26   case (insert x S)
    27   thus ?case by (simp add: minus_max_eq_min) 
    28 qed
    29 
    30 lemma minus_Min_eq_Max [simp]:
    31   fixes S :: "'a::{lordered_ab_group_add, linorder} set"
    32   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Min S) = Max (uminus ` S)"
    33 proof (induct S rule: finite_ne_induct)
    34   case (singleton x)
    35   thus ?case by simp
    36 next
    37   case (insert x S)
    38   thus ?case by (simp add: minus_min_eq_max) 
    39 qed
    40 
    41 instantiation real :: Sup 
    42 begin
    43 definition
    44   Sup_real_def [code del]: "Sup X == (LEAST z::real. \<forall>x\<in>X. x\<le>z)"
    45 
    46 instance ..
    47 end
    48 
    49 instantiation real :: Inf 
    50 begin
    51 definition
    52   Inf_real_def [code del]: "Inf (X::real set) == - (Sup (uminus ` X))"
    53 
    54 instance ..
    55 end
    56 
    57 subsection{*Supremum of a set of reals*}
    58 
    59 lemma Sup_upper [intro]: (*REAL_SUP_UBOUND in HOL4*)
    60   fixes x :: real
    61   assumes x: "x \<in> X"
    62       and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
    63   shows "x \<le> Sup X"
    64 proof (auto simp add: Sup_real_def) 
    65   from reals_complete2
    66   obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
    67     by (blast intro: x z)
    68   hence "x \<le> s"
    69     by (blast intro: x z)
    70   also with s have "... = (LEAST z. \<forall>x\<in>X. x \<le> z)"
    71     by (fast intro: Least_equality [symmetric])  
    72   finally show "x \<le> (LEAST z. \<forall>x\<in>X. x \<le> z)" .
    73 qed
    74 
    75 lemma Sup_least [intro]: (*REAL_IMP_SUP_LE in HOL4*)
    76   fixes z :: real
    77   assumes x: "X \<noteq> {}"
    78       and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
    79   shows "Sup X \<le> z"
    80 proof (auto simp add: Sup_real_def) 
    81   from reals_complete2 x
    82   obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
    83     by (blast intro: z)
    84   hence "(LEAST z. \<forall>x\<in>X. x \<le> z) = s"
    85     by (best intro: Least_equality)  
    86   also with s z have "... \<le> z"
    87     by blast
    88   finally show "(LEAST z. \<forall>x\<in>X. x \<le> z) \<le> z" .
    89 qed
    90 
    91 lemma Sup_singleton [simp]: "Sup {x::real} = x"
    92   by (force intro: Least_equality simp add: Sup_real_def)
    93  
    94 lemma Sup_eq_maximum: (*REAL_SUP_MAX in HOL4*)
    95   fixes z :: real
    96   assumes X: "z \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
    97   shows  "Sup X = z"
    98   by (force intro: Least_equality X z simp add: Sup_real_def)
    99  
   100 lemma Sup_upper2: (*REAL_IMP_LE_SUP in HOL4*)
   101   fixes x :: real
   102   shows "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X"
   103   by (metis Sup_upper real_le_trans)
   104 
   105 lemma Sup_real_iff : (*REAL_SUP_LE in HOL4*)
   106   fixes z :: real
   107   shows "X ~= {} ==> (!!x. x \<in> X ==> x \<le> z) ==> (\<exists>x\<in>X. y<x) <-> y < Sup X"
   108   by (metis Sup_least Sup_upper linorder_not_le le_less_trans)
   109 
   110 lemma Sup_eq:
   111   fixes a :: real
   112   shows "(!!x. x \<in> X \<Longrightarrow> x \<le> a) 
   113         \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y) \<Longrightarrow> Sup X = a"
   114   by (metis Sup_least Sup_upper add_le_cancel_left diff_add_cancel insert_absorb
   115         insert_not_empty real_le_anti_sym)
   116 
   117 lemma Sup_le:
   118   fixes S :: "real set"
   119   shows "S \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
   120 by (metis SupInf.Sup_least setle_def)
   121 
   122 lemma Sup_upper_EX: 
   123   fixes x :: real
   124   shows "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> x \<le> z \<Longrightarrow>  x \<le> Sup X"
   125   by blast
   126 
   127 lemma Sup_insert_nonempty: 
   128   fixes x :: real
   129   assumes x: "x \<in> X"
   130       and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
   131   shows "Sup (insert a X) = max a (Sup X)"
   132 proof (cases "Sup X \<le> a")
   133   case True
   134   thus ?thesis
   135     apply (simp add: max_def) 
   136     apply (rule Sup_eq_maximum)
   137     apply (metis insertCI)
   138     apply (metis Sup_upper insertE le_iff_sup real_le_linear real_le_trans sup_absorb1 z)     
   139     done
   140 next
   141   case False
   142   hence 1:"a < Sup X" by simp
   143   have "Sup X \<le> Sup (insert a X)"
   144     apply (rule Sup_least)
   145     apply (metis empty_psubset_nonempty psubset_eq x)
   146     apply (rule Sup_upper_EX) 
   147     apply blast
   148     apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
   149     done
   150   moreover 
   151   have "Sup (insert a X) \<le> Sup X"
   152     apply (rule Sup_least)
   153     apply blast
   154     apply (metis False Sup_upper insertE real_le_linear z) 
   155     done
   156   ultimately have "Sup (insert a X) = Sup X"
   157     by (blast intro:  antisym )
   158   thus ?thesis
   159     by (metis 1 min_max.le_iff_sup real_less_def)
   160 qed
   161 
   162 lemma Sup_insert_if: 
   163   fixes X :: "real set"
   164   assumes z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
   165   shows "Sup (insert a X) = (if X={} then a else max a (Sup X))"
   166 by auto (metis Sup_insert_nonempty z) 
   167 
   168 lemma Sup: 
   169   fixes S :: "real set"
   170   shows "S \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
   171 by  (auto simp add: isLub_def setle_def leastP_def isUb_def intro!: setgeI) 
   172 
   173 lemma Sup_finite_Max: 
   174   fixes S :: "real set"
   175   assumes fS: "finite S" and Se: "S \<noteq> {}"
   176   shows "Sup S = Max S"
   177 using fS Se
   178 proof-
   179   let ?m = "Max S"
   180   from Max_ge[OF fS] have Sm: "\<forall> x\<in> S. x \<le> ?m" by metis
   181   with Sup[OF Se] have lub: "isLub UNIV S (Sup S)" by (metis setle_def)
   182   from Max_in[OF fS Se] lub have mrS: "?m \<le> Sup S"
   183     by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
   184   moreover
   185   have "Sup S \<le> ?m" using Sm lub
   186     by (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
   187   ultimately  show ?thesis by arith
   188 qed
   189 
   190 lemma Sup_finite_in:
   191   fixes S :: "real set"
   192   assumes fS: "finite S" and Se: "S \<noteq> {}"
   193   shows "Sup S \<in> S"
   194   using Sup_finite_Max[OF fS Se] Max_in[OF fS Se] by metis
   195 
   196 lemma Sup_finite_ge_iff: 
   197   fixes S :: "real set"
   198   assumes fS: "finite S" and Se: "S \<noteq> {}"
   199   shows "a \<le> Sup S \<longleftrightarrow> (\<exists> x \<in> S. a \<le> x)"
   200 by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS linorder_not_le less_le_trans)
   201 
   202 lemma Sup_finite_le_iff: 
   203   fixes S :: "real set"
   204   assumes fS: "finite S" and Se: "S \<noteq> {}"
   205   shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
   206 by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS le_iff_sup real_le_trans) 
   207 
   208 lemma Sup_finite_gt_iff: 
   209   fixes S :: "real set"
   210   assumes fS: "finite S" and Se: "S \<noteq> {}"
   211   shows "a < Sup S \<longleftrightarrow> (\<exists> x \<in> S. a < x)"
   212 by (metis Se Sup_finite_le_iff fS linorder_not_less)
   213 
   214 lemma Sup_finite_lt_iff: 
   215   fixes S :: "real set"
   216   assumes fS: "finite S" and Se: "S \<noteq> {}"
   217   shows "a > Sup S \<longleftrightarrow> (\<forall> x \<in> S. a > x)"
   218 by (metis Se Sup_finite_ge_iff fS linorder_not_less)
   219 
   220 lemma Sup_unique:
   221   fixes S :: "real set"
   222   shows "S *<= b \<Longrightarrow> (\<forall>b' < b. \<exists>x \<in> S. b' < x) \<Longrightarrow> Sup S = b"
   223 unfolding setle_def
   224 apply (rule Sup_eq, auto) 
   225 apply (metis linorder_not_less) 
   226 done
   227 
   228 lemma Sup_abs_le:
   229   fixes S :: "real set"
   230   shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
   231 by (auto simp add: abs_le_interval_iff) (metis Sup_upper2) 
   232 
   233 lemma Sup_bounds:
   234   fixes S :: "real set"
   235   assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
   236   shows "a \<le> Sup S \<and> Sup S \<le> b"
   237 proof-
   238   from Sup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast
   239   hence b: "Sup S \<le> b" using u 
   240     by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) 
   241   from Se obtain y where y: "y \<in> S" by blast
   242   from lub l have "a \<le> Sup S"
   243     by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
   244        (metis le_iff_sup le_sup_iff y)
   245   with b show ?thesis by blast
   246 qed
   247 
   248 lemma Sup_asclose: 
   249   fixes S :: "real set"
   250   assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Sup S - l\<bar> \<le> e"
   251 proof-
   252   have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" by arith
   253   thus ?thesis using S b Sup_bounds[of S "l - e" "l+e"] unfolding th
   254     by  (auto simp add: setge_def setle_def)
   255 qed
   256 
   257 
   258 subsection{*Infimum of a set of reals*}
   259 
   260 lemma Inf_lower [intro]: 
   261   fixes z :: real
   262   assumes x: "x \<in> X"
   263       and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
   264   shows "Inf X \<le> x"
   265 proof -
   266   have "-x \<le> Sup (uminus ` X)"
   267     by (rule Sup_upper [where z = "-z"]) (auto simp add: image_iff x z)
   268   thus ?thesis 
   269     by (auto simp add: Inf_real_def)
   270 qed
   271 
   272 lemma Inf_greatest [intro]: 
   273   fixes z :: real
   274   assumes x: "X \<noteq> {}"
   275       and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
   276   shows "z \<le> Inf X"
   277 proof -
   278   have "Sup (uminus ` X) \<le> -z" using x z by (force intro: Sup_least)
   279   hence "z \<le> - Sup (uminus ` X)"
   280     by simp
   281   thus ?thesis 
   282     by (auto simp add: Inf_real_def)
   283 qed
   284 
   285 lemma Inf_singleton [simp]: "Inf {x::real} = x"
   286   by (simp add: Inf_real_def) 
   287  
   288 lemma Inf_eq_minimum: (*REAL_INF_MIN in HOL4*)
   289   fixes z :: real
   290   assumes x: "z \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
   291   shows  "Inf X = z"
   292 proof -
   293   have "Sup (uminus ` X) = -z" using x z
   294     by (force intro: Sup_eq_maximum x z)
   295   thus ?thesis
   296     by (simp add: Inf_real_def) 
   297 qed
   298  
   299 lemma Inf_lower2:
   300   fixes x :: real
   301   shows "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
   302   by (metis Inf_lower real_le_trans)
   303 
   304 lemma Inf_real_iff:
   305   fixes z :: real
   306   shows "X \<noteq> {} \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> (\<exists>x\<in>X. x<y) \<longleftrightarrow> Inf X < y"
   307   by (metis Inf_greatest Inf_lower less_le_not_le real_le_linear 
   308             order_less_le_trans)
   309 
   310 lemma Inf_eq:
   311   fixes a :: real
   312   shows "(!!x. x \<in> X \<Longrightarrow> a \<le> x) \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a) \<Longrightarrow> Inf X = a"
   313   by (metis Inf_greatest Inf_lower add_le_cancel_left diff_add_cancel
   314         insert_absorb insert_not_empty real_le_anti_sym)
   315 
   316 lemma Inf_ge: 
   317   fixes S :: "real set"
   318   shows "S \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
   319 by (metis SupInf.Inf_greatest setge_def)
   320 
   321 lemma Inf_lower_EX: 
   322   fixes x :: real
   323   shows "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> z \<le> x \<Longrightarrow> Inf X \<le> x"
   324   by blast
   325 
   326 lemma Inf_insert_nonempty: 
   327   fixes x :: real
   328   assumes x: "x \<in> X"
   329       and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
   330   shows "Inf (insert a X) = min a (Inf X)"
   331 proof (cases "a \<le> Inf X")
   332   case True
   333   thus ?thesis
   334     by (simp add: min_def)
   335        (blast intro: Inf_eq_minimum Inf_lower real_le_refl real_le_trans z) 
   336 next
   337   case False
   338   hence 1:"Inf X < a" by simp
   339   have "Inf (insert a X) \<le> Inf X"
   340     apply (rule Inf_greatest)
   341     apply (metis empty_psubset_nonempty psubset_eq x)
   342     apply (rule Inf_lower_EX) 
   343     apply (blast intro: elim:) 
   344     apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
   345     done
   346   moreover 
   347   have "Inf X \<le> Inf (insert a X)"
   348     apply (rule Inf_greatest)
   349     apply blast
   350     apply (metis False Inf_lower insertE real_le_linear z) 
   351     done
   352   ultimately have "Inf (insert a X) = Inf X"
   353     by (blast intro:  antisym )
   354   thus ?thesis
   355     by (metis False min_max.inf_absorb2 real_le_linear)
   356 qed
   357 
   358 lemma Inf_insert_if: 
   359   fixes X :: "real set"
   360   assumes z:  "!!x. x \<in> X \<Longrightarrow> z \<le> x"
   361   shows "Inf (insert a X) = (if X={} then a else min a (Inf X))"
   362 by auto (metis Inf_insert_nonempty z) 
   363 
   364 text{*We could prove the analogous result for the supremum, and also generalise it to the union operator.*}
   365 lemma Inf_binary:
   366   "Inf{a, b::real} = min a b"
   367   by (subst Inf_insert_nonempty, auto)
   368 
   369 lemma Inf_greater:
   370   fixes z :: real
   371   shows "X \<noteq> {} \<Longrightarrow>  Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
   372   by (metis Inf_real_iff mem_def not_leE)
   373 
   374 lemma Inf_close:
   375   fixes e :: real
   376   shows "X \<noteq> {} \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>x \<in> X. x < Inf X + e"
   377   by (metis add_strict_increasing comm_monoid_add.mult_commute Inf_greater linorder_not_le pos_add_strict)
   378 
   379 lemma Inf_finite_Min:
   380   fixes S :: "real set"
   381   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> Inf S = Min S"
   382 by (simp add: Inf_real_def Sup_finite_Max image_image) 
   383 
   384 lemma Inf_finite_in: 
   385   fixes S :: "real set"
   386   assumes fS: "finite S" and Se: "S \<noteq> {}"
   387   shows "Inf S \<in> S"
   388   using Inf_finite_Min[OF fS Se] Min_in[OF fS Se] by metis
   389 
   390 lemma Inf_finite_ge_iff: 
   391   fixes S :: "real set"
   392   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)"
   393 by (metis Inf_finite_Min Inf_finite_in Min_le real_le_trans)
   394 
   395 lemma Inf_finite_le_iff:
   396   fixes S :: "real set"
   397   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
   398 by (metis Inf_finite_Min Inf_finite_ge_iff Inf_finite_in Min_le
   399           real_le_anti_sym real_le_linear)
   400 
   401 lemma Inf_finite_gt_iff: 
   402   fixes S :: "real set"
   403   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a < Inf S \<longleftrightarrow> (\<forall> x \<in> S. a < x)"
   404 by (metis Inf_finite_le_iff linorder_not_less)
   405 
   406 lemma Inf_finite_lt_iff: 
   407   fixes S :: "real set"
   408   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a > Inf S \<longleftrightarrow> (\<exists> x \<in> S. a > x)"
   409 by (metis Inf_finite_ge_iff linorder_not_less)
   410 
   411 lemma Inf_unique:
   412   fixes S :: "real set"
   413   shows "b <=* S \<Longrightarrow> (\<forall>b' > b. \<exists>x \<in> S. b' > x) \<Longrightarrow> Inf S = b"
   414 unfolding setge_def
   415 apply (rule Inf_eq, auto) 
   416 apply (metis less_le_not_le linorder_not_less) 
   417 done
   418 
   419 lemma Inf_abs_ge:
   420   fixes S :: "real set"
   421   shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
   422 by (simp add: Inf_real_def) (rule Sup_abs_le, auto) 
   423 
   424 lemma Inf_asclose:
   425   fixes S :: "real set"
   426   assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Inf S - l\<bar> \<le> e"
   427 proof -
   428   have "\<bar>- Sup (uminus ` S) - l\<bar> =  \<bar>Sup (uminus ` S) - (-l)\<bar>"
   429     by auto
   430   also have "... \<le> e" 
   431     apply (rule Sup_asclose) 
   432     apply (auto simp add: S)
   433     apply (metis abs_minus_add_cancel b comm_monoid_add.mult_commute real_diff_def) 
   434     done
   435   finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
   436   thus ?thesis
   437     by (simp add: Inf_real_def)
   438 qed
   439 
   440 subsection{*Relate max and min to sup and inf.*}
   441 
   442 lemma real_max_Sup:
   443   fixes x :: real
   444   shows "max x y = Sup {x,y}"
   445 proof-
   446   have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
   447   from Sup_finite_le_iff[OF f, of "max x y"] have "Sup {x,y} \<le> max x y" by simp
   448   moreover
   449   have "max x y \<le> Sup {x,y}" using Sup_finite_ge_iff[OF f, of "max x y"]
   450     by (simp add: linorder_linear)
   451   ultimately show ?thesis by arith
   452 qed
   453 
   454 lemma real_min_Inf: 
   455   fixes x :: real
   456   shows "min x y = Inf {x,y}"
   457 proof-
   458   have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
   459   from Inf_finite_le_iff[OF f, of "min x y"] have "Inf {x,y} \<le> min x y"
   460     by (simp add: linorder_linear)
   461   moreover
   462   have "min x y \<le> Inf {x,y}" using Inf_finite_ge_iff[OF f, of "min x y"]
   463     by simp
   464   ultimately show ?thesis by arith
   465 qed
   466 
   467 end