%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Properties of real numbers   %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

real_facts : THEORY

  BEGIN

  S: VAR (nonempty?[real])

  bounded?_lem  : LEMMA bounded?(S) IFF
                          EXISTS (B: real): FORALL (x: (S)):  abs(x) <= B


  %----------------------------------------
  %  More properties of archimedean field 
  %----------------------------------------

  archimedean2 : THEOREM
 FORALL (x : posreal) : EXISTS (a : posnat) : 1/a < x

  archimedean3 : THEOREM
 FORALL (x : nonneg_real) :
    (FORALL (a : posnat) : x <= 1/a) implies x = 0


  %-------------------------------------------------
  %  Every real is between two successive integers
  %-------------------------------------------------

  nat_interval : LEMMA
 FORALL (x : nonneg_real) : EXISTS (a : nat) : a <= x and x < a + 1

  int_interval : LEMMA
 FORALL (x : real) : EXISTS (a : integer) : a <= x and x < a +1 


  %---------------------------------------
  %  Short cuts for lub and glb of sets
  %---------------------------------------

  U: VAR (bounded_above?)
  V: VAR (bounded_below?)
  a,b,x, y: VAR real
  epsilon: VAR posreal


  lub_is_bound: LEMMA FORALL (x: (U)):  x <= lub(U)

  lub_is_lub: LEMMA lub(U) <= y IFF FORALL (x: (U)): x <= y

  lub_closed_intv: LEMMA a < b IMPLIES lub({x | a <= x AND x <= b}) = b


  adherence_sup: LEMMA 
 FORALL epsilon: EXISTS (x: (U)): lub(U) - epsilon < x


  glb_is_bound: LEMMA FORALL (x: (V)): glb(V) <= x

  glb_is_glb: LEMMA y <= glb(V) IFF FORALL (x: (V)): y <= x

  glb_closed_intv: LEMMA a < b IMPLIES glb({x | a <= x AND x <= b}) = a

  adherence_inf: LEMMA
 FORALL epsilon: EXISTS (x: (V)): x < glb(V) + epsilon



  END real_facts