Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: real_fun_on_compact_sets.prf Sprache: PVS

Original von: PVS^©

linear_transformations_2D: THEORY

%----------------------------------------------------------------------------
%------------linear transformations over vect2-------------------------------
%------------Original Date: Dec 15, 2009-------------------------------------
%----------------------------------------------------------------------------
%------------Authors: Anthony Narkawicz, NASA--------------------------------
%----------------------------------------------------------------------------
%----------------------------------------------------------------------------
%----------------------------------------------------------------------------

BEGIN

IMPORTING vectors_2D, det_2D, basis_2D

   u,v,w     : VAR Vector
   a,b,c     : VAR real
   nza       : VAR nzreal
   L,J      : VAR [Vector -> Vector] % Linear Transformations
   F,G      : VAR [Vector -> real] % Linear Functionals

% LINEAR TRANSFORMATIONS

  linear_transform?(L): bool =
    FORALL (u,v: Vector): FORALL (a,b: real): L(a*u+b*v) = a*L(u) + b*L(v)

% Basic Properties

  linear_transform_zero: LEMMA
    linear_transform?(L) IMPLIES L(zero) = zero

  linear_transform_scal: LEMMA
    linear_transform?(L) IMPLIES
    FORALL (u: Vector, a: real): L(a*u) = a*L(u)

  linear_transform_add: LEMMA
    linear_transform?(L) IMPLIES
    FORALL (u,v: Vector): L(u+v) = L(u) + L(v)

  linear_transform_sub: LEMMA
    linear_transform?(L) IMPLIES
    FORALL (u,v: Vector): L(u-v) = L(u) - L(v)

% Equivalent Characterizations

  linear_transform_rew: LEMMA linear_transform?(L) IFF
    (FORALL (u,v: Vector): L(u+v) = L(u) + L(v)) AND
    (FORALL (u: Vector, a: real): L(a*u) = a*L(u))

  linear_transform_alt_left: LEMMA linear_transform?(L) IFF
    FORALL (u,v: Vector): FORALL (a: real): L(a*u + v) = a*L(u) + L(v)

  linear_transform_alt_right: LEMMA linear_transform?(L) IFF
    FORALL (u,v: Vector): FORALL (a: real): L(u+a*v) = L(u) + a*L(v)

% Other Theorems

  linear_transform_perp_unique: LEMMA u /= zero AND v /= zero AND
    linear_transform?(L) AND
    linear_transform?(J) AND
    orthogonal?(u,v) AND
    L(u) = J(u) AND
    L(v) = J(v)
    IMPLIES
    L = J

% Auto rewrites for linear transformations Vect2 -> Vect2
   AUTO_REWRITE+ linear_transform_zero           % L(zero) = zero

% LINEAR FUNCTIONALS

  linear_functional?(F): bool =
    FORALL (u,v: Vector): FORALL (a,b: real): F(a*u+b*v) = a*F(u) + b*F(v)

% Basic Properties

  linear_functional_zero: LEMMA
    linear_functional?(F) IMPLIES F(zero) = 0

  linear_functional_scal: LEMMA
    linear_functional?(F) IMPLIES
    FORALL (u: Vector, a: real): F(a*u) = a*F(u)

  linear_functional_add: LEMMA
    linear_functional?(F) IMPLIES
    FORALL (u,v: Vector): F(u+v) = F(u) + F(v)

  linear_functional_sub: LEMMA
    linear_functional?(F) IMPLIES
    FORALL (u,v: Vector): F(u-v) = F(u) - F(v)

  kernel_functional_nonempty: LEMMA
    linear_functional?(F) IMPLIES
    EXISTS (v: Vector): v /= zero AND F(v) = 0

  linear_functional_is_dot: LEMMA
    linear_functional?(F) IMPLIES
    EXISTS (w: Vector): F = (LAMBDA (v: Vector): w*v)

% Equivalent Characterizations

  linear_functional_rew: LEMMA linear_functional?(F) IFF
    (FORALL (u,v: Vector): F(u+v) = F(u) + F(v)) AND
    (FORALL (u: Vector, a: real): F(a*u) = a*F(u))

  linear_functional_alt_left: LEMMA linear_functional?(F) IFF
    FORALL (u,v: Vector): FORALL (a: real): F(a*u + v) = a*F(u) + F(v)

  linear_functional_alt_right: LEMMA linear_functional?(F) IFF
    FORALL (u,v: Vector): FORALL (a: real): F(u+a*v) = F(u) + a*F(v)

% Other Theorems

  linear_functional_perp_unique: LEMMA u /= zero AND v /= zero AND
    linear_functional?(F) AND
    linear_functional?(G) AND
    orthogonal?(u,v) AND
    F(u) = G(u) AND
    F(v) = G(v)
    IMPLIES
    F = G

  linear_functional_is_perp_dot: LEMMA
    linear_functional?(F) AND
    u/=zero AND
    F(u) = 0
    IMPLIES
    (EXISTS (rzk: real): F = (LAMBDA (v: Vector): rzk*det(v,u)))

  linear_functional_perp_signs_unique: LEMMA v /= zero AND
    linear_functional?(F) AND
    linear_functional?(G) AND
    F(u)*G(u) > 0 AND
    F(v) = 0 AND
    G(v) = 0
    IMPLIES
    FORALL (w: Vector): F(w)*G(w) >= 0

% Auto rewrites for linear functionalations Vect2 -> Vect2
   AUTO_REWRITE+ linear_functional_zero           % F(zero) = zero

END linear_transformations_2D

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.