Towards ray optics formalization of optical imaging systems

The verification of optical systems is an important issue due to their safety and financial critical nature (e.g., laser surgeries and space telescopes). Theorem proving offers an attractive solution to overcome the accuracy and soundness problems of traditional approaches like paper-and-pencil based proofs and computer simulation. However, existing formalizations of optics theories do not provide the facility to analyze optical imaging systems which describe the behavior of light ray within the system. In this paper, we present the ray optics formalization of cardinal points which are the most fundamental requirement to model imaging properties of optical systems. We also present the verification of cardinal points for a general system consisting of any number of optical components. For illustration purposes, we present the formal analysis of a thick lens.