A lot of verification methodologies of Object-Oriented models based on statecharts have been proposed. This approach becomes unrealistic when it comes to prove properties involving multiple objects as it needs to construct a global state space, which often results in state explosion. We propose a verification method to prove such properties from the viewpoint of collaboration. Collaboration is an aspect of a system that cross-cuts its class structure and directly describes global interaction between objects. As a groundwork for verification, we defined an OO theory in the HOL theorem prover. In this paper, we explain the definition of the theory and implementation in HOL. We also show a verification example using the theory.