THEORY PlannarControlTheory
  IMPORT THEORY PROJECTS
    /SimpleDEq THEORIES /SimpleDEq/Approximation.dtf|org.eventb.theory.core.deployedTheoryRoot#Approximation
  OPERATORS
    SecondOrder2DimensionSystemFunction expression (correction_coeff: RReal,controlArea4: POW((RReal*RReal)*(RReal*RReal)))
      direct definition 
        (% ((x1|->x2)|->(x3|->x4))|->((vx|->vy)|->(wx|->wy)) .
          ((x1|->x2)|->(x3|->x4)) : (RReal*RReal)*(RReal*RReal) & ((vx|->vy)|->(wx|->wy)) : (RReal*RReal)*(RReal*RReal) & ((vx|->vy)|->(wx|->wy)) : controlArea4
        |  (minus(divide(vx|->Rtwo)|->minus(times(correction_coeff|->minus(x3|->wx))|->x1))
          |-> minus(divide(vy|->Rtwo)|->minus(times(correction_coeff|->minus(x4|->wy))|->x2)))
          |->(x1
          |-> x2)
        )
    FirstOrder2DimensionSystemFunction expression (controlArea2: POW(RReal*RReal))
      direct definition 
        (% (x1|->x2)|->(vx|->vy) .
          (x1|->x2) : RReal*RReal & (vx|->vy) : RReal*RReal & (vx|->vy) : controlArea2
        | ( vx
          |-> vy
          )
        )
    SecondOrder2DimensionSystem expression (correction_coeff: RReal,controlArea4: POW((RReal*RReal)*(RReal*RReal)),t0: RRealPlus,x0: (RReal*RReal)*(RReal*RReal))
      direct definition 
        caode(
          SecondOrder2DimensionSystemFunction(correction_coeff,controlArea4),
          x0,
          t0
        )
    FirstOrder2DimensionSystem expression (controlArea2: POW(RReal*RReal),t0: RRealPlus,y0: RReal*RReal)
      direct definition 
        caode(
          FirstOrder2DimensionSystemFunction(controlArea2),
          y0,
          t0
        )
    PointwiseSlopedControl expression (DR: POW(RReal),vx: RReal,vy: RReal,t0: RReal)
      well-definedness t0 : DR
      direct definition 
        (% t . t : DR & t0 |-> t : leq |
          (vx |-> vy)
          |->
          (times(vx |-> minus(t |-> t0)) |-> times(vy |-> minus(t |-> t0)))
        )
    PointwiseControl expression (DR: POW(RReal),vx: RReal,vy: RReal,t0: RReal)
      well-definedness t0 : DR
      direct definition 
        (% t . t : DR & t0 |-> t : leq | (vx |-> vy))
    FirstOrderSystemObserver expression ()
      direct definition 
        (% x . x : RReal*RReal | x )
    SecondOrderSystemObserver expression ()
      direct definition 
        (% (x1|->x2)|->(x3|->x4) . (x1|->x2|->x3|->x4) : RReal*RReal*RReal*RReal | x3|->x4)
  AXIOMATIC DEFINITIONS  pc_control:
    AXIOMS
      second_order_control: 
        ! DR,UF,vx,vy,cc,t0,x0 .
          cc : RReal &
          DR <: RReal & UF <: RReal*RReal &
          (vx|->vy) : UF &
          t0 : RReal & t0 : DR &
          x0 : (RReal*RReal)*(RReal*RReal) =>
            SolvableWith(
              DR,
              SecondOrder2DimensionSystem(cc,UF*(RReal*RReal),t0,x0),
              PointwiseSlopedControl(DR,vx,vy,t0)
            )
      first_order_control: 
        ! DR,UF,vx,vy,t0,x0 .
          DR <: RReal & UF <: RReal*RReal &
          (vx|->vy) : UF &
          t0 : RReal & t0 : DR &
          x0 : RReal*RReal =>
            SolvableWith(
              DR,
              FirstOrder2DimensionSystem(UF,t0,x0),
              PointwiseControl(DR,vx,vy,t0)
            )  pc_sim:
    OPERATORS
      NeighborhoodSimulationCondition predicate (mu: RRealPlus,nu: RRealPlus,cc: RReal) : 
        well-definedness Rzero |-> cc : lt
    AXIOMS
      nsc_def: 
        ! mu,nu,cc . mu : RRealPlus & nu : RRealPlus & cc : RReal & Rzero |-> cc : lt => (
          NeighborhoodSimulationCondition(mu,nu,cc) <=>
          (times(nu |-> plus(divide(Rone |-> Rtwo) |-> plus(times(Rtwo |-> cc) |-> sqrt(plus(Rone |-> times(plus(Rtwo |-> Rtwo) |-> cc)))))) |-> mu : leq)
        )
      first_second_order_simulation_function: 
        ! UF1,UF2,cc,mu,nu .
          cc : RReal &
          UF1 <: RReal*RReal & UF2 <: RReal*RReal &
          mu : RRealPlus & nu : RRealPlus &
          UF1 <: DeltaNeighborhoodSet(mu,Rzero|->Rzero) & UF2 <: DeltaNeighborhoodSet(nu,Rzero|->Rzero) &
          NeighborhoodSimulationCondition(mu,nu,cc)
           => (
            # V . V : SimulationFunctions(
              (RReal*RReal)*(RReal*RReal),  RReal*RReal,
              UF1*(RReal*RReal),        UF2,
              SecondOrder2DimensionSystemFunction(cc,UF1*(RReal*RReal)),  SecondOrderSystemObserver,
              FirstOrder2DimensionSystemFunction(UF2),          FirstOrderSystemObserver
            )
          )
      first_second_order_simulation_delta: 
        ! UF1,UF2,cc,mu,nu,V .
          cc : RReal &
          UF1 <: RReal*RReal & UF2 <: RReal*RReal &
          mu : RRealPlus & nu : RRealPlus &
          NeighborhoodSimulationCondition(mu,nu,cc) &
          V : SimulationFunctions(
            (RReal*RReal)*(RReal*RReal),  RReal*RReal,
            UF1*(RReal*RReal),        UF2,
            SecondOrder2DimensionSystemFunction(cc,UF1*(RReal*RReal)),  SecondOrderSystemObserver,
            FirstOrder2DimensionSystemFunction(UF2),          FirstOrderSystemObserver
          ) =>
            boundedBy(((RReal*RReal)*(RReal*RReal))*(RReal*RReal),V,Rzero,times(Rtwo|->nu))  distance:
    OPERATORS
      plannar_distance expression (r1: RReal*RReal,r2: RReal*RReal) : RReal
    AXIOMS
      dist_sym: 
        ! x,y . x : RReal*RReal & y : RReal*RReal =>
          plannar_distance(x,y) = plannar_distance(y,x)
      dist_sep: 
        ! x,y . x : RReal*RReal & y : RReal*RReal =>
          (plannar_distance(x,y) = Rzero <=> x = y)
      dist_tri: 
        ! x,y,z . x : RReal*RReal & y : RReal*RReal & z : RReal*RReal =>
          plannar_distance(x,z) |-> plus(plannar_distance(x,y)|->plannar_distance(y,z)) : leq
      open_ball_is_open: 
        ! x,delta . x : RReal*RReal & delta : RRealPlus & Rzero |-> delta : lt =>
          IsOpen({ y | plannar_distance(x,y) |-> delta : gt })
      dist_choice: 
        ! P,d . P : RReal*RReal & d : RReal & Rzero |-> d : lt => (
            # Q . Q : RReal*RReal & d |-> plannar_distance(P,Q) : lt
          )
      neighborhood_plannar_distance: 
        ! a,b,delta .
          a : RReal*RReal & b : RReal*RReal & delta : RRealPlus & Rzero |-> delta : lt &
          DeltaNeighborhood(delta,a,b)
            => plannar_distance(a,b) |-> delta : lt
  THEOREMS
    first_order_system_solvable: 
      ! DR,UF,t0,y0,vx,vy .
        DR <: RReal &
        UF <: RReal*RReal &
        t0 : DR & y0 : RReal*RReal &
        vx|->vy : UF =>
          SolvableWith(DR,FirstOrder2DimensionSystem(UF,t0,y0),PointwiseControl(DR,vx,vy,t0))
    second_order_system_solvable: 
      ! DR,UF,t0,x0,vx,vy,cc .
        DR <: RReal &
        UF <: RReal*RReal &
        t0 : DR & x0 : (RReal*RReal)*(RReal*RReal) &
        vx|->vy : UF &
        cc : RReal =>
          SolvableWith(DR,SecondOrder2DimensionSystem(cc,UF*(RReal*RReal),t0,x0),PointwiseSlopedControl(DR,vx,vy,t0))
END