products/Sources/formale Sprachen/Delphi/Bille 0.71/Auslieferung/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: deriv_real_vect2.pvs   Sprache: Unknown

deriv_real_vect2 [ T : TYPE FROM real ] : THEORY
BEGIN
  ASSUMING
    IMPORTING analysis@deriv_domain_def

     deriv_domain     : ASSUMPTION deriv_domain?[T]

     not_one_element  : ASSUMPTION not_one_element?[T]


  ENDASSUMING


  IMPORTING analysis@deriv_domain, analysis@derivatives[T],
            vectors@det_2D

  s,v : VAR Vect2
  a,r : VAR T

  derivable_rv?(V:[T->Vect2]): bool =
    derivable?(LAMBDA(a):V(a)`x) AND
    derivable?(LAMBDA(a):V(a)`y)

  differentiable_rv?(V:[T->Vect2]): MACRO bool = derivable_rv?(V)

  V : VAR (derivable_rv?)

  deriv_rv(V)(r) : Vect2 =
    (deriv(LAMBDA(a):V(a)`x,r),deriv(LAMBDA(a):V(a)`y,r))

% ------- Properties of deriv

  deriv(V): [T -> Vect2] = (LAMBDA (r:T): deriv_rv(V)(r))

  AUTO_REWRITE- deriv_rv
  AUTO_REWRITE- deriv
  AUTO_REWRITE- derivable_rv?

  IMPORTING vect_fun_ops_rv

  f, f1, f2 : VAR (derivable_rv?)
  b,c : VAR real

  h: VAR deriv_fun[T]   %   h:[T -> real] AND derivable?(h)

  sum_derivable_rv   : LEMMA derivable_rv?(LAMBDA (x: T): f1(x) + f2(x))

  diff_derivable_rv  : LEMMA derivable_rv?(LAMBDA (x: T): f1(x) - f2(x))

  neg_derivable_rv   : LEMMA derivable_rv?(LAMBDA (x: T): -f(x))

  prod_derivable_rv  : LEMMA derivable_rv?(LAMBDA (x: T): h(x)*f(x))

  dot_derivable_rv   : LEMMA derivable?(LAMBDA (x: T): f1(x)*f2(x))

  sqv_derivable_rv   : LEMMA derivable?(LAMBDA (x: T): sqv(f(x)))


  const_derivable_rv : LEMMA derivable_rv?(LAMBDA (x: T): s) 

  scal_derivable_rv  : LEMMA derivable_rv?(LAMBDA (x: T): c * f(x))

  prod_id_derivable_rv: LEMMA derivable_rv?(LAMBDA (x: T): x * v)


  deriv_sum_vfun    : LEMMA deriv(LAMBDA (x: T): f1(x) + f2(x)) = deriv(f1) + deriv(f2)

  deriv_diff_vfun   : LEMMA deriv(LAMBDA (x: T): f1(x) - f2(x)) = deriv(f1) - deriv(f2)
 
  deriv_neg_vfun    : LEMMA deriv(LAMBDA (x:T): -f(x)) = -deriv(f)

  deriv_prod_vfun   : LEMMA deriv(LAMBDA (x: T): h(x) * f(x)) = deriv(h)*f + h*deriv(f)

  deriv_dot_vfun    : LEMMA deriv(LAMBDA (x: T): f1(x) * f2(x)) = deriv(f1)*f2 + f1*deriv(f2)

  deriv_sqv_vfun    : LEMMA 
     deriv(LAMBDA (x: T): sqv(f(x))) = (LAMBDA (x:T): 2*f(x)*deriv(f)(x)) 


  deriv_const_vfun  : LEMMA deriv(LAMBDA (x: T): s) = (LAMBDA (x:T): zero)

  deriv_scal_vfun   : LEMMA deriv(LAMBDA (x: T): c * f(x)) = c * deriv(f)

  deriv_prod_id_vfun: LEMMA deriv(LAMBDA (x: T): x * v) = (LAMBDA (x: T): v)


  d_sum_vfun   : LEMMA derivable_rv?(LAMBDA (x: T): f1(x) + f2(x)) AND
                       deriv(LAMBDA (x: T): f1(x) + f2(x)) = deriv(f1) + deriv(f2)

  d_diff_vfun  : LEMMA derivable_rv?(LAMBDA (x: T): f1(x) - f2(x)) AND 
                       deriv(LAMBDA (x: T): f1(x) - f2(x)) = deriv(f1) - deriv(f2)

  d_neg_vfun   : LEMMA derivable_rv?(LAMBDA (x: T): -f(x)) AND
                       deriv(LAMBDA (x:T): -f(x)) = -deriv(f)

  d_prod_vfun  : LEMMA derivable_rv?(LAMBDA (x: T): h(x)*f(x)) AND
                       deriv(LAMBDA (x: T): h(x) * f(x)) = deriv(h)*f + h*deriv(f)

  d_dot_vfun   : LEMMA derivable?(LAMBDA (x: T): f1(x)*f2(x)) AND
                       deriv(LAMBDA (x: T): f1(x) * f2(x)) = deriv(f1)*f2 + f1*deriv(f2)

  d_const_vfun : LEMMA derivable_rv?(LAMBDA (x: T): s) AND
                       deriv(LAMBDA (x: T): s) = (LAMBDA (x:T): zero)

  d_scal_vfun  : LEMMA derivable_rv?(LAMBDA (x: T): c * f(x)) AND
                       deriv(LAMBDA (x: T): c * f(x)) = c * deriv(f)



END deriv_real_vect2

[ Dauer der Verarbeitung: 0.1 Sekunden  (vorverarbeitet)  ]