motion-planning verification of a robot motion planning algorithm with Isabelle in a 2D static world using trapezoidal map to construct a road map