src/HOL/Real/HahnBanach/Bounds.thy

tuned presentation;

(*  Title:      HOL/Real/HahnBanach/Bounds.thy
    ID:         $Id$
    Author:     Gertrud Bauer, TU Munich
*)

header {* Bounds *};

theory Bounds = Main + Real:; (*<*)

subsection {* The sets of lower and upper bounds *};

constdefs
  is_LowerBound :: "('a::order) set => 'a set => 'a => bool"
  "is_LowerBound A B == \<lambda>x. x:A & (ALL y:B. x <= y)"
   
  LowerBounds :: "('a::order) set => 'a set => 'a set"
  "LowerBounds A B == Collect (is_LowerBound A B)"

  is_UpperBound :: "('a::order) set => 'a set => 'a => bool"
  "is_UpperBound A B == \<lambda>x. x:A & (ALL y:B. y <= x)"
 
  UpperBounds :: "('a::order) set => 'a set => 'a set"
  "UpperBounds A B == Collect (is_UpperBound A B)";

syntax
  "_UPPERS" :: "[pttrn, 'a set, 'a => bool] => 'a set"     
    ("(3UPPER'_BOUNDS _:_./ _)" 10)
  "_UPPERS_U" :: "[pttrn, 'a => bool] => 'a set"           
    ("(3UPPER'_BOUNDS _./ _)" 10)
  "_LOWERS" :: "[pttrn, 'a set, 'a => bool] => 'a set"     
    ("(3LOWER'_BOUNDS _:_./ _)" 10)
  "_LOWERS_U" :: "[pttrn, 'a => bool] => 'a set"           
    ("(3LOWER'_BOUNDS _./ _)" 10);

translations
  "UPPER_BOUNDS x:A. P" == "UpperBounds A (Collect (\<lambda>x. P))"
  "UPPER_BOUNDS x. P" == "UPPER_BOUNDS x:UNIV. P"
  "LOWER_BOUNDS x:A. P" == "LowerBounds A (Collect (\<lambda>x. P))"
  "LOWER_BOUNDS x. P" == "LOWER_BOUNDS x:UNIV. P";


subsection {* Least and greatest elements *};

constdefs
  is_Least :: "('a::order) set => 'a => bool"
  "is_Least B == is_LowerBound B B"

  Least :: "('a::order) set => 'a"
  "Least B == Eps (is_Least B)"

  is_Greatest :: "('a::order) set => 'a => bool"
  "is_Greatest B == is_UpperBound B B"

  Greatest :: "('a::order) set => 'a" 
  "Greatest B == Eps (is_Greatest B)";

syntax
  "_LEAST"    :: "[pttrn, 'a => bool] => 'a"  
    ("(3LLEAST _./ _)" 10)
  "_GREATEST" :: "[pttrn, 'a => bool] => 'a"  
    ("(3GREATEST _./ _)" 10);

translations
  "LLEAST x. P" == "Least {x. P}"
  "GREATEST x. P" == "Greatest {x. P}";


subsection {* Infimum and Supremum *};

(*>*)
text {*
 A supremum\footnote{The definition of the supremum is based on one in
 \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Lubs.html}}  of
 an ordered set $B$ w.~r.~t.~$A$ is defined as a least upper bound of
 $B$, which lies in $A$.
*};
   
text{* If a supremum exists, then $\idt{Sup}\ap A\ap B$
is equal to the supremum. *};

constdefs
  is_Sup :: "('a::order) set => 'a set => 'a => bool"
  "is_Sup A B x == isLub A B x"

  Sup :: "('a::order) set => 'a set => 'a"
  "Sup A B == Eps (is_Sup A B)"; (*<*)

constdefs
  is_Inf :: "('a::order) set => 'a set => 'a => bool"
  "is_Inf A B x == x:A & is_Greatest (LowerBounds A B) x"

  Inf :: "('a::order) set => 'a set => 'a"
  "Inf A B == Eps (is_Inf A B)";

syntax
  "_SUP" :: "[pttrn, 'a set, 'a => bool] => 'a set"
    ("(3SUP _:_./ _)" 10)
  "_SUP_U" :: "[pttrn, 'a => bool] => 'a set"
    ("(3SUP _./ _)" 10)
  "_INF" :: "[pttrn, 'a set, 'a => bool] => 'a set"
    ("(3INF _:_./ _)" 10)
  "_INF_U" :: "[pttrn, 'a => bool] => 'a set"
    ("(3INF _./ _)" 10);

translations
  "SUP x:A. P" == "Sup A (Collect (\<lambda>x. P))"
  "SUP x. P" == "SUP x:UNIV. P"
  "INF x:A. P" == "Inf A (Collect (\<lambda>x. P))"
  "INF x. P" == "INF x:UNIV. P";

(*>*)
text{* The supremum of $B$ is less than any upper bound
of $B$.*};

lemma sup_le_ub: "isUb A B y ==> is_Sup A B s ==> s <= y";
  by (unfold is_Sup_def, rule isLub_le_isUb);

text {* The supremum $B$ is an upper bound for $B$. *};

lemma sup_ub: "y:B ==> is_Sup A B s ==> y <= s";
  by (unfold is_Sup_def, rule isLubD2);

text{* The supremum of a non-empty set $B$ is greater
than a lower bound of $B$. *};

lemma sup_ub1: 
  "[| ALL y:B. a <= y; is_Sup A B s; x:B |] ==> a <= s";
proof -; 
  assume "ALL y:B. a <= y" "is_Sup A B s" "x:B";
  have "a <= x"; by (rule bspec);
  also; have "x <= s"; by (rule sup_ub);
  finally; show "a <= s"; .;
qed;
  
end;