Formalizing Potential Flows Using the HOL Light Theorem Prover

Potential flow is a theoretical model that describes the movement of a fluid, e.g., water or air in situations where viscosity and turbulence are assumed to be negligible. This type of flow is often used as an idealized model to describe the behavior of fluids in specific contexts, such as in fluid dynamics and aerodynamics. In this paper, we present a higher-order logic formalization of potential flows that are governed by the Laplace equation. We focus on formally modeling fundamental flows such as the uniform, source/sink, doublet, and vortex flows in the HOL Light theorem prover. We then prove the validity of these exact potential flow solutions of the Laplace equation. Moreover, we present the formal verification of the linearity of the Laplace operator, which is essential to apply the superposition principle. To demonstrate the practical effectiveness of our formalization, we formally verify several applications such as the Rankine oval, flow past a circular cylinder and flow past a rotating circular cylinder, each of which involves combining these standard flows using the superposition principle to model more complex fluid dynamics.