THEORY Approximation
  IMPORT THEORY PROJECTS
    /SimpleDEq THEORIES /SimpleDEq/ApproximationBase.dtf|org.eventb.theory.core.deployedTheoryRoot#ApproximationBase
  TYPE PARAMETERS E,F1,F2,F3,UF1,UF2,F
  OPERATORS
    FDeltaNeighborhood predicate (PE: POW(E),delta: RRealPlus,a: F,f2: E +-> F)
      well-definedness PE <: dom(f2)
      direct definition 
        ! x . x : PE => DeltaNeighborhood(delta,a,f2(x))
    DeltaApproximation predicate (PE: POW(E),delta: RRealPlus,f1: E +-> F,f2: E +-> F)
      well-definedness PE <: dom(f1),PE <: dom(f2)
      direct definition 
        ! x . x : PE => DeltaNeighborhood(delta,f1(x),f2(x))
    DeltaApproximationEq predicate (DR: POW(RReal),delta: RRealPlus,e1: DE(F),e2: DE(F))
      well-definedness Solvable(DR,e1),Solvable(DR,e2)
      direct definition 
        ! eta1,eta2 .
          eta1 : RReal +-> F & eta2 : RReal +-> F &
          DR <: dom(eta1) & DR <: dom(eta2) &
          solutionOf(DR,eta1,e1) & solutionOf(DR,eta2,e2)
            => DeltaApproximation(DR,delta,eta1,eta2)
    DeltaApproximationEqObs predicate (DR: POW(RReal),delta: RRealPlus,ee1: DE(F1),g1: F1 --> F,ee2: DE(F2),g2: F2 --> F)
      well-definedness Solvable(DR,ee1),Solvable(DR,ee2)
      direct definition 
        ! eta1,eta2 .
          eta1 : RReal +-> F1 & eta2 : RReal +-> F2 &
          DR <: dom(eta1) & DR <: dom(eta2) &
          solutionOf(DR,eta1,ee1) & solutionOf(DR,eta2,ee2)
            => DeltaApproximation(DR,delta,g1 circ eta1,g2 circ eta2)
    DeltaApproximationEqF predicate (DR: POW(RReal),delta: RRealPlus,e: DE(F),g: RReal +-> F)
      well-definedness Solvable(DR,e),DR <: dom(g)
      direct definition 
        ! eta .
          eta : RReal +-> F & DR <: dom(eta) & solutionOf(DR,eta,e)
            => DeltaApproximation(DR,delta,eta,g)
    ProjectiveHull expression (delta: RRealPlus,SF: POW(F))
      direct definition 
        { f2 | f2 : F & (# f1 . f1 : SF & DeltaNeighborhood(delta,f1,f2)) }
    DeltaNeighborhoodSet expression (delta: RRealPlus,x: E)
      direct definition 
        { y | y : E & DeltaNeighborhood(delta,x,y) }
  AXIOMATIC DEFINITIONS  simulation_functions:
    OPERATORS
      SimulationFunctions expression (DF1: POW(F1),DF2: POW(F2),DUF1: POW(UF1),DUF2: POW(UF2),f1: F1*UF1 +-> F1,f2: F2*UF2 +-> F2,g1: F1 --> F,g2: F2 --> F) : POW(POW((F1*F2)*RReal))
        well-definedness DF1*DUF1 <: dom(f1),DF2*DUF2 <: dom(f2)
    AXIOMS
      SimulationFunctions_char: 
        ! DF1,DF2,DUF1,DUF2,f1,f2,g1,g2,V .
          DF1 <: F1 & DF2 <: F2 & DUF1 <: UF1 & DUF2 <: UF2 &
          f1 : F1*UF1 +-> F1 & f2 : F2*UF2 +-> F2 &
          g1 : F1 --> F & g2 : F2 --> F &
          DF1*DUF1 <: dom(f1) & DF2*DUF2 <: dom(f2) &
          V : SimulationFunctions(DF1,DF2,DUF1,DUF2,f1,f2,g1,g2) & 
          V : F1*F2 +-> RReal
            => (
              DF1*DF2 <: dom(V)
                  & (! x1,x2 . x1 : DF1 & x2 : DF2 => V(x1|->x2) : RRealPlus)
            )
      SimulationFunction_control_ODE: 
        ! DR,eta01,eta02,t0,DF1,DF2,DUF1,DUF2,f1,f2,g1,g2,u1,u2,V .
          DR <: RReal & t0 : DR & eta01 : F1 & eta02 : F2 &
          DF1 <: F1 & DF2 <: F2 & DUF1 <: UF1 & DUF2 <: UF2 &
          f1 : F1*UF1 +-> F1 & DF1*DUF1 <: dom(f1) &
          f2 : F2*UF2 +-> F2 & DF2*DUF2 <: dom(f2) &
          g1 : F1 --> F & g2 : F2 --> F &
          u1 : RReal +-> UF1 & DR <: dom(u1) & ran(u1) <: UF1 &
          u2 : RReal +-> UF2 & DR <: dom(u2) & ran(u2) <: UF2 &
          V : SimulationFunctions(DF1,DF2,DUF1,DUF2,f1,f2,g1,g2) &
          SolvableWith(DR,caode(f1,eta01,t0),u1) & SolvableWith(DR,caode(f2,eta02,t0),u2) =>
            (# delta .
              delta : RRealPlus & 
              DeltaApproximationEqObs(DR,delta,
                withControl(DR,caode(f1,eta01,t0),u1), g1,
                withControl(DR,caode(f2,eta02,t0),u2), g2
              )
            )
      SimulationFunction_control_ODE_delta: 
        ! DR,eta01,eta02,t0,DF1,DF2,DUF1,DUF2,f1,f2,g1,g2,u1,u2,V,delta .
          DR <: RReal & t0 : DR & eta01 : F1 & eta02 : F2 &
          DF1 <: F1 & DF2 <: F2 & DUF1 <: UF1 & DUF2 <: UF2 &
          f1 : F1*UF1 +-> F1 & DF1*DUF1 <: dom(f1) &
          f2 : F2*UF2 +-> F2 & DF2*DUF2 <: dom(f2) &
          g1 : F1 --> F & g2 : F2 --> F &
          u1 : RReal +-> UF1 & DR <: dom(u1) & ran(u1) <: UF1 &
          u2 : RReal +-> UF2 & DR <: dom(u2) & ran(u2) <: UF2 &
          V : SimulationFunctions(DF1,DF2,DUF1,DUF2,f1,f2,g1,g2) &
          delta : RReal & Rzero |-> delta : lt & boundedBy(DF1*DF2,V,Rzero,delta) &
          SolvableWith(DR,caode(f1,eta01,t0),u1) & SolvableWith(DR,caode(f2,eta02,t0),u2) =>
            DeltaApproximationEqObs(DR,delta,
              withControl(DR,caode(f1,eta01,t0),u1), g1,
              withControl(DR,caode(f2,eta02,t0),u2), g2
            )  neighborhoods:
    AXIOMS
      deltaNSet_open: 
        ! delta,x . delta : RRealPlus & Rzero |-> delta : lt & x : E =>
          IsOpen(DeltaNeighborhoodSet(delta,x))
  THEOREMS
    deltaA_restriction: 
      ! PE,PE2,delta,f1,f2 .
        PE <: E & PE2 <: PE & delta : RRealPlus &
        f1 : E +-> F & f2 : E +-> F &
        PE <: dom(f1) & PE <: dom(f2) &
        DeltaApproximation(PE,delta,f1,f2)
          =>
            DeltaApproximation(PE2,delta,f1,f2)
    deltaAeq_restriction: 
      ! DR,DR2,delta,e1,e2 .
        DR <: RReal & DR2 <: DR & delta : RRealPlus &
        e1 : DE(F) & e2 : DE(F) &
        Solvable(DR,e1) & Solvable(DR2,e2) &
        DeltaApproximationEq(DR,delta,e1,e2)
          =>
            DeltaApproximationEq(DR2,delta,e1,e2)
    deltaAeqobs_restriction: 
      ! DR,DR2,delta,e1,e2,g1,g2 .
        DR <: RReal & DR2 <: DR & delta : RRealPlus &
        e1 : DE(F1) & e2 : DE(F2) &
        g1 : F1 --> F & g2 : F2 --> F &
        Solvable(DR,e1) & Solvable(DR2,e2) &
        DeltaApproximationEqObs(DR,delta,e1,g1,e2,g2)
          =>
            DeltaApproximationEqObs(DR2,delta,e1,g1,e2,g2)
    deltaA_comp: 
      ! DF1,PE,f,g,h,delta .
        DF1 <: F1 & PE <: E &
        g : F1 +-> E & f : E +-> F & h : E +-> F &
        DF1 <: dom(g) & PE <: dom(f) & PE <: dom(h) &
        DeltaApproximation(PE,delta,f,h) &
        (! x . x : DF1 => g(x) : PE) =>
          DeltaApproximation(DF1,delta,f circ g,h circ g)
    deltaA_commutative: 
      ! PE,delta,f1,f2 .
        PE <: E & delta : RRealPlus & f1 : E +-> F & f2 : E +-> F &
          PE <: dom(f1) & PE <: dom(f2) =>
        (DeltaApproximation(PE,delta,f1,f2) <=> DeltaApproximation(PE,delta,f2,f1))
    deltaAeq_commutative: 
      ! DR,delta,e1,e2 .
        DR <: RReal & delta : RRealPlus & e1 : DE(F) & e2 : DE(F) & Solvable(DR,e1) & Solvable(DR,e2) =>
          (DeltaApproximationEq(DR,delta,e1,e2) <=> DeltaApproximationEq(DR,delta,e2,e1))
    deltaAeqobs_commutative: 
      ! DR,delta,e1,e2,g1,g2 .
        DR <: RReal & delta : RRealPlus &
        e1 : DE(F1) & e2 : DE(F2) &
        Solvable(DR,e1) & Solvable(DR,e2) &
        g1 : F1 --> F & g2 : F2 --> F
          =>
            (DeltaApproximationEqObs(DR,delta,e1,g1,e2,g2)
            <=>
             DeltaApproximationEqObs(DR,delta,e2,g2,e1,g1))
    deltaApp_induction: 
      ! delta,eqA,eqC,etaA,etaC,etaAp,etaCp,t,tp,InvA,InvC .
        delta : RRealPlus &
        t : RRealPlus &
        eqA : DE(F) & eqC : DE(F) &
        etaA : RReal +-> F & Closed2Closed(Rzero,t) <: dom(etaA) &
        etaC : RReal +-> F & Closed2Closed(Rzero,t) <: dom(etaC) &
        DeltaApproximationEq(Closed2Closed(t,tp),delta,eqA,eqC) &
        DeltaApproximation(Closed2Closed(Rzero,t),delta,etaA,etaC) &
        CBAPsolutionOf(t,tp,etaA,etaAp,eqA,InvA) & CBAPsolutionOf(t,tp,etaC,etaCp,eqC,InvC)
          => DeltaApproximation(Closed2Closed(Rzero,tp),delta,etaAp,etaCp)
    deltaApp_obs_induction: 
      ! delta,eqA,eqC,gA,gC,etaA,etaC,etaAp,etaCp,t,tp,InvA,InvC .
        delta : RRealPlus &
        t : RRealPlus &
        eqA : DE(F1) & eqC : DE(F2) & gA : F1 --> F & gC : F2 --> F &
        etaA : RReal +-> F1 & Closed2Closed(Rzero,t) <: dom(etaA) &
        etaC : RReal +-> F2 & Closed2Closed(Rzero,t) <: dom(etaC) &
        DeltaApproximationEqObs(Closed2Closed(t,tp),delta,eqA,gA,eqC,gC) &
        DeltaApproximation(Closed2Closed(Rzero,t),delta,gA circ etaA,gC circ etaC) &
        CBAPsolutionOf(t,tp,etaA,etaAp,eqA,InvA) & CBAPsolutionOf(t,tp,etaC,etaCp,eqC,InvC)
          => DeltaApproximation(Closed2Closed(Rzero,tp),delta,gA circ etaAp,gC circ etaCp)
    ProjectiveHull_INV: 
      ! delta,xA,xC,IA,IC .
        delta : RRealPlus &
        IA <: F & xA : F &
        IC <: F & xC : F & xC : IC &
        ProjectiveHull(delta, IC) <: IA =>
          xA : IA
END