products/Sources/formale Sprachen/Isabelle/HOL/ex/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: convergence_aux.pvs   Sprache: Unknown

%------------------------------------------------------------------------------
% Metric Convergence Properties
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            17/08/07  Initial Version
%------------------------------------------------------------------------------
convergence_aux: THEORY

BEGIN
            
  IMPORTING metric_space_def[real,(LAMBDA (x,y:real): abs(x-y))],
            metric_space[real,(LAMBDA (x,y:real): abs(x-y))],
            reals@bounded_reals[real],
            reals@real_fun_ops_aux[nat],
            reals@real_fun_preds[nat]

  u,v: VAR sequence[real]
  x,y: VAR real
  n,i: VAR nat
  r:   VAR posreal
  nnc: VAR nnreal
  ua:  VAR (real_fun_preds.bounded_above?)
  ub:  VAR (real_fun_preds.bounded_below?)

%  bounded_above?(u):bool = bounded_above?(image[nat,real](u,fullset[nat]))
%  bounded_below?(u):bool = bounded_below?(image[nat,real](u,fullset[nat]))
  bounded_seq?(u)  :bool = bounded?(image[nat,real](u,fullset[nat]))

  bounded_seq_def: LEMMA bounded_seq?(u) <=>
                         (bounded_above?(u) AND bounded_below?(u))

  upper_bound?(u):[real->bool] = upper_bound?(image[nat,real](u,fullset[nat]))
  lower_bound?(u):[real->bool] = lower_bound?(image[nat,real](u,fullset[nat]))

  lub(ua):real = lub(image[nat,real](ua,fullset[nat]))
  glb(ub):real = glb(image[nat,real](ub,fullset[nat]))

% following should be in real_topology, but is it even needed?
%  cauchy_convergent: LEMMA cauchy?(u) <=> metric_convergent?(u)

  converges_upto?(u,x):bool = convergence?(u,x) AND increasing?(u)

  convergent_upto?(u):bool = EXISTS x: converges_upto?(u,x)

  converges_upto_bounded_above: LEMMA converges_upto?(u,x) =>
                                      bounded_above?(u)

  converges_upto_le: LEMMA converges_upto?(u,x) => (FORALL n: u(n) <= x)

  converges_upto_def: LEMMA
      converges_upto?(u,x) <=>
      increasing?(u) AND
      (FORALL n: u(n) <= x) AND
      (FORALL r: EXISTS n: FORALL i: i >= n => x-u(i) < r)

  converges_upto_is_lub: LEMMA 
      converges_upto?(u,x) <=>
          (bounded_above?(u) AND increasing?(u) AND
           least_upper_bound?(x,image[nat,real](u,fullset[nat])))

  bounded_above_is_convergent:
    LEMMA bounded_above?(u) AND increasing?(u) => convergent_upto?(u)

  converges_upto_add:  LEMMA converges_upto?(u,x) AND converges_upto?(v,y)
                             => converges_upto?(u+v,x+y)

  converges_upto_scal: LEMMA converges_upto?(u,x) =>
                             converges_upto?(nnc*u,nnc*x)

  converges_downto?(u,x):bool = convergence?(u,x) AND decreasing?(u)

  convergent_downto?(u):bool = EXISTS x: converges_downto?(u,x)

  converges_downto_bounded_below: LEMMA converges_downto?(u,x) =>
                                        bounded_below?(u)

  converges_downto_ge: LEMMA converges_downto?(u,x) => FORALL n: x<=u(n)

  converges_downto_def: LEMMA
      converges_downto?(u,x) <=>
      decreasing?(u) AND
      (FORALL n: x <= u(n)) AND
      (FORALL r: EXISTS n: FORALL i: i >= n => u(i)-x < r)

  converges_downto_is_glb: LEMMA 
      converges_downto?(u,x) <=>
          (bounded_below?(u) AND decreasing?(u) AND
           greatest_lower_bound?(x,image[nat,real](u,fullset[nat])))

  bounded_below_is_convergent:
    LEMMA bounded_below?(u) AND decreasing?(u) => convergent_downto?(u)

  converges_downto_add: LEMMA converges_downto?(u,x) AND converges_downto?(v,y)
                              => converges_downto?(u+v,x+y)

  converges_downto_scal:LEMMA converges_downto?(u,x) =>
                              converges_downto?(nnc*u,nnc*x)

  monotonic_converges?(u,x):bool
    = convergence?(u,x) AND (increasing?(u) OR decreasing?(u))

  monotonic_convergent?(u):bool = EXISTS x: monotonic_converges?(u,x)

END convergence_aux

[ Dauer der Verarbeitung: 0.1 Sekunden  (vorverarbeitet)  ]