THEORY
  IMPORT THEORY PROJECTS
    /SimpleDEq THEORIES /SimpleDEq/Approximation.dtf|org.eventb.theory.core.deployedTheoryRoot#Approximation
  OPERATORS
    PendulumRawFun expression (omega0: RReal)
      direct definition 
        (% t_|->(x1_|->x2_)|->u_ .
          t_ : RRealPlus & x1_ : RReal & x2_ : RReal & u_ : RReal
          | x2_ |-> (plus(times(u_ |-> cos(x1_)) |-> times(times(omega0|->omega0)|->sin(x1_))))
        )
    PendulumRaw expression (omega0: RReal,x0: RReal*RReal,t0: RRealPlus)
      direct definition 
        code(PendulumRawFun(omega0),x0,t0)
    PendulumLinFun expression (omega0: RReal)
      direct definition 
        (% t_|->(x1_|->x2_)|->u_ .
          t_ : RRealPlus & x1_ : RReal & x2_ : RReal & u_ : RReal
          | x2_ |-> (plus(u_ |-> times(times(omega0|->omega0)|->x1_)))
        )
    PendulumLin expression (omega0: RReal,x0: RReal*RReal,t0: RRealPlus)
      direct definition 
        code(PendulumLinFun(omega0),x0,t0)
  AXIOMATIC DEFINITIONS  pendulum_solvability:
    OPERATORS
      theta_max expression (omega0: RReal) : RReal
    AXIOMS
      theta_max_bounds: 
        ! omega0 . omega0 : RReal => Rzero |-> theta_max(omega0) : leq & theta_max(omega0) |-> divide(pi|->Rtwo) : leq
      pendulum_raw_controllability: 
        ! omega0,theta0,thetap0,t0 .
          omega0 : RReal &
          theta0 : RReal & abs(theta0) |-> theta_max(omega0) : lt &
          thetap0 : RReal &
          t0 : RRealPlus
            => (
          # t1 . t1 : RRealPlus & t0 |-> t1 : lt &
            Controllable(Closed2Closed(t0,t1),PendulumRaw(omega0,(theta0|->thetap0),t0))
        )
      pendulum_lin_controllability: 
        ! omega0,theta0,thetap0,t0 .
          omega0 : RReal &
          theta0 : RReal & abs(theta0) |-> theta_max(omega0) : lt &
          thetap0 : RReal &
          t0 : RRealPlus
            => (
          # t1 . t1 : RRealPlus & t0 |-> t1 : lt &
            Controllable(Closed2Closed(t0,t1),PendulumLin(omega0,(theta0|->thetap0),t0))
        )  pendulum_approx:
    OPERATORS
      PendulumApproxWD predicate (delta: RReal,omega0: RReal,theta_bound: RReal,ctrl_bound: RReal,ctrl_bound_lin: RReal,ctrl_delta: RReal,t0: RRealPlus,t1: RRealPlus) : 
        well-definedness Rzero|->delta : lt,Rzero|->theta_bound : lt,theta_bound |-> theta_max(omega0) : lt,Rzero|->ctrl_bound : lt,Rzero|->ctrl_bound_lin : lt,Rzero|->ctrl_delta : lt,t0 |-> t1 : lt
    AXIOMS
      PAWD_Approximation: 
        ! delta,omega0,theta_bound,ctrl_bound,ctrl_bound_lin,ctrl_delta,t0,t1,x0_raw,x0_lin,u_raw,u_lin .
          delta : RReal & Rzero |-> delta : lt &
          omega0 : RReal &
          theta_bound : RReal & Rzero |-> theta_bound : lt & theta_bound |-> theta_max(omega0) : lt &
          ctrl_bound : RReal & Rzero |-> ctrl_bound : lt &
          ctrl_bound_lin : RReal & Rzero |-> ctrl_bound_lin : lt &
          ctrl_delta : RReal & Rzero |-> ctrl_delta : lt &
          t0 : RRealPlus & t1 : RRealPlus & t0 |-> t1 : lt &
          PendulumApproxWD(delta,omega0,theta_bound,ctrl_bound,ctrl_bound_lin,ctrl_delta,t0,t1) &
          u_raw : RReal +-> RReal & Closed2Closed(t0,t1) <: dom(u_raw) & (! t_ . t_ : Closed2Closed(t0,t1) => abs(u_raw(t_)) |-> ctrl_bound : lt) &
          u_lin : RReal +-> RReal & Closed2Closed(t0,t1) <: dom(u_lin) & (! t_ . t_ : Closed2Closed(t0,t1) => abs(u_lin(t_)) |-> ctrl_bound_lin : lt) &
          DeltaApproximation(Closed2Closed(t0,t1),ctrl_delta,u_raw,u_lin) &
          x0_raw : RReal*RReal & x0_lin : RReal*RReal & DeltaNeighborhood(delta,x0_raw,x0_lin)
            =>
              DeltaApproximationEq(Closed2Closed(t0,t1),delta,
                withControl(Closed2Closed(t0,t1),PendulumRaw(omega0,x0_raw,t0),u_raw),
                withControl(Closed2Closed(t0,t1),PendulumLin(omega0,x0_lin,t0),u_lin)
              )  pendulum_control:
    OPERATORS
      PendulumRawControl expression (omega0: RReal,theta0: RReal,thetap0: RReal,t0: RRealPlus) : POW(RReal*RReal)
        well-definedness abs(theta0) |-> theta_max(omega0) : lt
      PendulumLinControl expression (omega0: RReal,theta0: RReal,thetap0: RReal,t0: RRealPlus) : POW(RReal*RReal)
        well-definedness abs(theta0) |-> theta_max(omega0) : lt
      PC_raw_bound expression () : RReal
      PC_lin_bound expression () : RReal
      PendulumControlDelta expression (omega0: RReal,delta: RReal) : RReal
        well-definedness Rzero |-> delta : lt
    AXIOMS
      pendulum_raw_control_type: 
        ! omega0,theta0,thetap0,t0 .
          omega0 : RReal &
          theta0 : RReal & abs(theta0) |-> theta_max(omega0) : lt &
          thetap0 : RReal &
          t0 : RRealPlus
            => (
              PendulumRawControl(omega0,theta0,thetap0,t0) : RReal +-> RReal &
              Closed2Infinity(t0) <: dom(PendulumRawControl(omega0,theta0,thetap0,t0))
        )
      pendulum_lin_control_type: 
        ! omega0,theta0,thetap0,t0 .
          omega0 : RReal &
          theta0 : RReal & abs(theta0) |-> theta_max(omega0) : lt &
          thetap0 : RReal &
          t0 : RRealPlus
            => (
              PendulumLinControl(omega0,theta0,thetap0,t0) : RReal +-> RReal &
              Closed2Infinity(t0) <: dom(PendulumLinControl(omega0,theta0,thetap0,t0))
        )
      pendulum_raw_control_bound_def: 
        Rzero |-> PC_raw_bound : lt
      pendulum_raw_control_bound: 
        ! omega0,theta0,thetap0,t0 .
          omega0 : RReal &
          theta0 : RReal & abs(theta0) |-> theta_max(omega0) : lt &
          thetap0 : RReal &
          t0 : RRealPlus
            => (
              ! t_ . t_ : RRealPlus & t0 |-> t_ : leq =>
                abs(PendulumRawControl(omega0,theta0,thetap0,t0)(t_)) |-> PC_raw_bound : lt
        )
      pendulum_raw_control_acceptable: 
        ! omega0,theta0,thetap0,t0 .
          omega0 : RReal &
          theta0 : RReal & abs(theta0) |-> theta_max(omega0) : lt &
          thetap0 : RReal &
          t0 : RRealPlus
            => (
            # t1 . t1 : RRealPlus & t0 |-> t1 : lt &
              SolvableWith(
                Closed2Closed(t0,t1),
                PendulumRaw(omega0,(theta0|->thetap0),t0),
                PendulumRawControl(omega0,theta0,thetap0,t0)
              )
        )
      pendulum_raw_control_solution_bounded: 
        ! omega0,theta0,thetap0,t0,t1 .
          omega0 : RReal &
          theta0 : RReal & abs(theta0) |-> theta_max(omega0) : lt &
          thetap0 : RReal &
          t0 : RRealPlus & t1 : RRealPlus & t0 |-> t1 : lt &
          SolvableWith(Closed2Closed(t0,t1),PendulumRaw(omega0,(theta0|->thetap0),t0),PendulumRawControl(omega0,theta0,thetap0,t0))
          => (
            ! theta_,thetap_ .
              theta_ : RReal +-> RReal & Closed2Closed(t0,t1) <: dom(theta_) &
              thetap_ : RReal +-> RReal & Closed2Closed(t0,t1) <: dom(thetap_) &
              solutionOf(
                Closed2Closed(t0,t1),
                bind(theta_,thetap_),
                withControl(
                  Closed2Closed(t0,t1),
                  PendulumRaw(omega0,(theta0|->thetap0),t0),
                  PendulumRawControl(omega0,theta0,thetap0,t0)
                )
              )
              => (
                ! t_ . t_ : Closed2Closed(t0,t1) => abs(theta_(t_)) |-> theta0 : lt
            )
        )
      pendulum_lin_control_bound_def: 
        Rzero |-> PC_lin_bound : lt
      pendulum_lin_control_bound: 
        ! omega0,theta0,thetap0,t0 .
          omega0 : RReal &
          theta0 : RReal & abs(theta0) |-> theta_max(omega0) : lt &
          thetap0 : RReal &
          t0 : RRealPlus
            => (
              ! t_ . t_ : RRealPlus & t0 |-> t_ : leq =>
                abs(PendulumLinControl(omega0,theta0,thetap0,t0)(t_)) |-> PC_lin_bound : lt
        )
      pendulum_lin_control_acceptable: 
        ! omega0,theta0,thetap0,t0 .
          omega0 : RReal &
          theta0 : RReal & abs(theta0) |-> theta_max(omega0) : lt &
          thetap0 : RReal &
          t0 : RRealPlus
            => (
            # t1 . t1 : RRealPlus & t0 |-> t1 : lt &
              SolvableWith(
                Closed2Closed(t0,t1),
                PendulumLin(omega0,(theta0|->thetap0),t0),
                PendulumLinControl(omega0,theta0,thetap0,t0)
              )
        )
      pendulum_lin_control_solution_bounded: 
        ! omega0,theta0,thetap0,t0,t1 .
          omega0 : RReal &
          theta0 : RReal & abs(theta0) |-> theta_max(omega0) : lt &
          thetap0 : RReal &
          t0 : RRealPlus & t1 : RRealPlus & t0 |-> t1 : lt &
          SolvableWith(Closed2Closed(t0,t1),PendulumLin(omega0,(theta0|->thetap0),t0),PendulumLinControl(omega0,theta0,thetap0,t0))
          => (
            ! theta_,thetap_ .
              theta_ : RReal +-> RReal & Closed2Closed(t0,t1) <: dom(theta_) &
              thetap_ : RReal +-> RReal & Closed2Closed(t0,t1) <: dom(thetap_) &
              solutionOf(
                Closed2Closed(t0,t1),
                bind(theta_,thetap_),
                withControl(
                  Closed2Closed(t0,t1),
                  PendulumLin(omega0,(theta0|->thetap0),t0),
                  PendulumLinControl(omega0,theta0,thetap0,t0)
                )
              )
              => (
                ! t_ . t_ : Closed2Closed(t0,t1) => abs(theta_(t_)) |-> theta0 : lt
            )
        )
      pendulum_control_delta_def: 
        ! omega0,delta .
          omega0 : RReal &
          delta : RReal & Rzero |-> delta : lt
            =>
              Rzero |-> PendulumControlDelta(omega0,delta) : lt
      pendulum_control_approx: 
        ! delta,omega0,theta0_raw,thetap0_raw,theta0_lin,thetap0_lin,t0 .
          delta : RReal & Rzero |-> delta : lt &
          omega0 : RReal &
          theta0_raw : RReal & abs(theta0_raw) |-> theta_max(omega0) : lt &
          thetap0_raw : RReal &
          theta0_lin : RReal & abs(theta0_lin) |-> theta_max(omega0) : lt &
          thetap0_lin : RReal &
          t0 : RRealPlus &
          DeltaNeighborhood(delta,(theta0_raw|->thetap0_raw),(theta0_lin|->thetap0_lin))
            =>
              DeltaApproximation(
                Closed2Infinity(t0),
                PendulumControlDelta(omega0,delta),
                PendulumRawControl(omega0,theta0_raw,thetap0_raw,t0),
                PendulumLinControl(omega0,theta0_lin,thetap0_lin,t0)
              )
END