THEORY ApproximationBase
  IMPORT THEORY PROJECTS
    /SimpleDEq THEORIES /SimpleDEq/DiffEq.dtf|org.eventb.theory.core.deployedTheoryRoot#DiffEq
  TYPE PARAMETERS E,F1,F2,F3,F
  OPERATORS
    absdiff commutative expression (a: RReal,b: RReal)
      direct definition 
        abs(minus(a |-> b))
  AXIOMATIC DEFINITIONS  approx_rel:
    OPERATORS
      DeltaNeighborhood predicate (delta: RRealPlus,a: F,b: F) : 
    AXIOMS
      deltaN_commutative: 
        ! delta,a,b . delta : RRealPlus & a : F & b : F =>
          (DeltaNeighborhood(delta,a,b) <=> DeltaNeighborhood(delta,b,a))
      deltaN_refl: 
        ! delta,a . delta : RRealPlus & a : F => DeltaNeighborhood(delta,a,a)
      deltaN_widen: 
        ! a,b,delta1 . delta1 : RRealPlus & a : F & b : F & DeltaNeighborhood(delta1,a,b) =>
          (! delta2 . delta2 : RRealPlus & delta1 |-> delta2 : leq => DeltaNeighborhood(delta2,a,b))
      deltaN_pseudo_trans: 
        ! a,b,c,delta1,delta2 .
          delta1 : RRealPlus & delta2 : RRealPlus &
          a : F & b : F & c : F &
          DeltaNeighborhood(delta1,a,b) & DeltaNeighborhood(delta2,b,c) =>
            DeltaNeighborhood(plus(delta1|->delta2),a,c)
      deltaN_R: 
        ! a,b,delta . a : RReal & b : RReal & delta : RRealPlus =>
          (DeltaNeighborhood(delta,a,b) <=> (absdiff(a,b) |-> delta : leq))
      deltaN_R_add: 
        ! a,b,k,delta . a : RReal & b : RReal & k : RReal & delta : RRealPlus => 
          (DeltaNeighborhood(delta,a,b) <=> DeltaNeighborhood(delta,plus(a|->k),plus(b|->k)))
      deltaN_R_add2: 
        ! a,b,c,d,delta1,delta2 .
          a : RReal & b : RReal & c : RReal & d : RReal &
          delta1 : RRealPlus & delta2 : RRealPlus &
          DeltaNeighborhood(delta1,a,b) & DeltaNeighborhood(delta2,c,d) =>
            DeltaNeighborhood(plus(delta1|->delta2),plus(a|->c),plus(b|->d))
END