An Isabelle/HOL formalisation of Green's Theorem

Mohammad Abdulaziz 🌐 and Lawrence C. Paulson 🌐

January 11, 2018

Abstract

We formalise a statement of Green’s theorem—the first formalisation to our knowledge—in Isabelle/HOL. The theorem statement that we formalise is enough for most applications, especially in physics and engineering. Our formalisation is made possible by 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.

License

BSD License

Topics

Session Green