An Isabelle/HOL Formalisation of Green’s Theorem
Interactive Theorem Proving
MetadataShow full item record
Abdulaziz, M., & Paulson, L. (2019). An Isabelle/HOL Formalisation of Green’s Theorem. Springer, Interactive Theorem Proving. [Book chapter]. https://doi.org/10.1007/978-3-319-43144-4_1
We mechanise a proof of Green’s theorem in Isabelle/HOL. We use a novel proof that avoids the ubiquitous line integral cancellation argument. This eliminates the need to formalise orientations and region boundaries explicitly with respect to the outwards-pointing normal vector. Instead we appeal to a homological argument about equivalences between paths. Contributions include mechanised theories of line integrals and partial derivatives, as well as the ﬁrst mechanisation of Green’s theorem.
European Research Council (742178)
External DOI: https://doi.org/10.1007/978-3-319-43144-4_1
This record's DOI: https://doi.org/10.17863/CAM.35379