src/HOL/Real/HahnBanach/Bounds.thy
author wenzelm
Fri Oct 08 16:40:27 1999 +0200 (1999-10-08)
changeset 7808 fd019ac3485f
parent 7656 2f18c0ffc348
child 7917 5e5b9813cce7
permissions -rw-r--r--
update from Gertrud;
wenzelm@7566
     1
(*  Title:      HOL/Real/HahnBanach/Bounds.thy
wenzelm@7566
     2
    ID:         $Id$
wenzelm@7566
     3
    Author:     Gertrud Bauer, TU Munich
wenzelm@7566
     4
*)
wenzelm@7535
     5
wenzelm@7808
     6
header {* Bounds *};
wenzelm@7808
     7
wenzelm@7535
     8
theory Bounds = Main + Real:;
wenzelm@7535
     9
wenzelm@7535
    10
wenzelm@7808
    11
subsection {* The sets of lower and upper bounds *};
wenzelm@7535
    12
wenzelm@7535
    13
constdefs
wenzelm@7535
    14
  is_LowerBound :: "('a::order) set => 'a set => 'a => bool"
wenzelm@7535
    15
  "is_LowerBound A B == %x. x:A & (ALL y:B. x <= y)"
wenzelm@7535
    16
   
wenzelm@7535
    17
  LowerBounds :: "('a::order) set => 'a set => 'a set"
wenzelm@7535
    18
  "LowerBounds A B == Collect (is_LowerBound A B)"
wenzelm@7535
    19
wenzelm@7535
    20
  is_UpperBound :: "('a::order) set => 'a set => 'a => bool"
wenzelm@7535
    21
  "is_UpperBound A B == %x. x:A & (ALL y:B. y <= x)"
wenzelm@7535
    22
 
wenzelm@7535
    23
  UpperBounds :: "('a::order) set => 'a set => 'a set"
wenzelm@7535
    24
  "UpperBounds A B == Collect (is_UpperBound A B)";
wenzelm@7535
    25
wenzelm@7535
    26
syntax
wenzelm@7808
    27
  "_UPPERS" :: "[pttrn, 'a set, 'a => bool] => 'a set"     
wenzelm@7808
    28
    ("(3UPPER'_BOUNDS _:_./ _)" 10)
wenzelm@7808
    29
  "_UPPERS_U" :: "[pttrn, 'a => bool] => 'a set"           
wenzelm@7808
    30
    ("(3UPPER'_BOUNDS _./ _)" 10)
wenzelm@7808
    31
  "_LOWERS" :: "[pttrn, 'a set, 'a => bool] => 'a set"     
wenzelm@7808
    32
    ("(3LOWER'_BOUNDS _:_./ _)" 10)
wenzelm@7808
    33
  "_LOWERS_U" :: "[pttrn, 'a => bool] => 'a set"           
wenzelm@7808
    34
    ("(3LOWER'_BOUNDS _./ _)" 10);
wenzelm@7535
    35
wenzelm@7535
    36
translations
wenzelm@7535
    37
  "UPPER_BOUNDS x:A. P" == "UpperBounds A (Collect (%x. P))"
wenzelm@7535
    38
  "UPPER_BOUNDS x. P" == "UPPER_BOUNDS x:UNIV. P"
wenzelm@7535
    39
  "LOWER_BOUNDS x:A. P" == "LowerBounds A (Collect (%x. P))"
wenzelm@7535
    40
  "LOWER_BOUNDS x. P" == "LOWER_BOUNDS x:UNIV. P";
wenzelm@7535
    41
wenzelm@7535
    42
wenzelm@7808
    43
subsection {* Least and greatest elements *};
wenzelm@7535
    44
wenzelm@7535
    45
constdefs
wenzelm@7535
    46
  is_Least :: "('a::order) set => 'a => bool"
wenzelm@7535
    47
  "is_Least B == is_LowerBound B B"
wenzelm@7535
    48
wenzelm@7535
    49
  Least :: "('a::order) set => 'a"
wenzelm@7535
    50
  "Least B == Eps (is_Least B)"
wenzelm@7535
    51
wenzelm@7535
    52
  is_Greatest :: "('a::order) set => 'a => bool"
wenzelm@7535
    53
  "is_Greatest B == is_UpperBound B B"
wenzelm@7535
    54
wenzelm@7535
    55
  Greatest :: "('a::order) set => 'a" 
wenzelm@7535
    56
  "Greatest B == Eps (is_Greatest B)";
wenzelm@7535
    57
wenzelm@7535
    58
syntax
wenzelm@7808
    59
  "_LEAST"    :: "[pttrn, 'a => bool] => 'a"  
wenzelm@7808
    60
    ("(3LLEAST _./ _)" 10)
wenzelm@7808
    61
  "_GREATEST" :: "[pttrn, 'a => bool] => 'a"  
wenzelm@7808
    62
    ("(3GREATEST _./ _)" 10);
wenzelm@7535
    63
wenzelm@7535
    64
translations
wenzelm@7535
    65
  "LLEAST x. P" == "Least {x. P}"
wenzelm@7535
    66
  "GREATEST x. P" == "Greatest {x. P}";
wenzelm@7535
    67
wenzelm@7535
    68
wenzelm@7808
    69
subsection {* Infimum and Supremum *};
wenzelm@7535
    70
wenzelm@7535
    71
constdefs
wenzelm@7535
    72
  is_Sup :: "('a::order) set => 'a set => 'a => bool"
wenzelm@7535
    73
  "is_Sup A B x == isLub A B x"
wenzelm@7535
    74
   
wenzelm@7535
    75
  Sup :: "('a::order) set => 'a set => 'a"
wenzelm@7535
    76
  "Sup A B == Eps (is_Sup A B)"
wenzelm@7535
    77
wenzelm@7535
    78
  is_Inf :: "('a::order) set => 'a set => 'a => bool"  
wenzelm@7535
    79
  "is_Inf A B x == x:A & is_Greatest (LowerBounds A B) x"
wenzelm@7535
    80
wenzelm@7535
    81
  Inf :: "('a::order) set => 'a set => 'a"
wenzelm@7535
    82
  "Inf A B == Eps (is_Inf A B)";
wenzelm@7535
    83
wenzelm@7535
    84
syntax
wenzelm@7808
    85
  "_SUP" :: "[pttrn, 'a set, 'a => bool] => 'a set"     
wenzelm@7808
    86
    ("(3SUP _:_./ _)" 10)
wenzelm@7808
    87
  "_SUP_U" :: "[pttrn, 'a => bool] => 'a set"           
wenzelm@7808
    88
    ("(3SUP _./ _)" 10)
wenzelm@7808
    89
  "_INF" :: "[pttrn, 'a set, 'a => bool] => 'a set"     
wenzelm@7808
    90
    ("(3INF _:_./ _)" 10)
wenzelm@7808
    91
  "_INF_U" :: "[pttrn, 'a => bool] => 'a set"           
wenzelm@7808
    92
    ("(3INF _./ _)" 10);
wenzelm@7535
    93
wenzelm@7535
    94
translations
wenzelm@7535
    95
  "SUP x:A. P" == "Sup A (Collect (%x. P))"
wenzelm@7535
    96
  "SUP x. P" == "SUP x:UNIV. P"
wenzelm@7535
    97
  "INF x:A. P" == "Inf A (Collect (%x. P))"
wenzelm@7535
    98
  "INF x. P" == "INF x:UNIV. P";
wenzelm@7535
    99
wenzelm@7656
   100
lemma sup_le_ub: "isUb A B y ==> is_Sup A B s ==> s <= y";
wenzelm@7535
   101
  by (unfold is_Sup_def, rule isLub_le_isUb);
wenzelm@7535
   102
wenzelm@7535
   103
lemma sup_ub: "y:B ==> is_Sup A B s ==> y <= s";
wenzelm@7535
   104
  by (unfold is_Sup_def, rule isLubD2);
wenzelm@7535
   105
wenzelm@7535
   106
lemma sup_ub1: "ALL y:B. a <= y ==> is_Sup A B s ==> x:B ==> a <= s";
wenzelm@7535
   107
proof -; 
wenzelm@7535
   108
  assume "ALL y:B. a <= y" "is_Sup A B s" "x:B";
wenzelm@7535
   109
  have "a <= x"; by (rule bspec);
wenzelm@7535
   110
  also; have "x <= s"; by (rule sup_ub);
wenzelm@7535
   111
  finally; show "a <= s"; .;
wenzelm@7535
   112
qed;
wenzelm@7535
   113
  
wenzelm@7808
   114
end;