Quelle  linear_functions.pvs

linear_functions[T: TYPE FROM real]: THEORY
BEGIN

   ASSUMING            %% ----- restrict T to single interval ------

    connected_domain : ASSUMPTION
 FORALL (x, y : T), (z : real) :
     x <= z AND z <= y IMPLIES T_pred(z)

    not_one_element : ASSUMPTION
  FORALL (x : T) : EXISTS (y : T) : x /= y

   ENDASSUMING

   IMPORTING reals@real_fun_props

   a,b,c,x,y: VAR T
   m,k: VAR real

   f,g: VAR [T -> real]
 
   linear?(f): bool = (EXISTS m,k: f = (LAMBDA x: m*x + k))

   linear_on?(f,a,b): bool = 
           (EXISTS m,k: (FORALL x: a <= x AND x <= b IMPLIES f(x) = m*x + k))


   linear_add: LEMMA linear?(f) AND linear?(g) IMPLIES
                       linear?(f+g)

END linear_functions