An Isabelle/HOL formalisation of Green's Theorem

Title:	An Isabelle/HOL formalisation of Green's Theorem
Authors:	Mohammad Abdulaziz and Lawrence C. Paulson
Submission date:	2018-01-11
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.
BibTeX:	@article{Green-AFP, author = {Mohammad Abdulaziz and Lawrence C. Paulson}, title = {An Isabelle/HOL formalisation of Green's Theorem}, journal = {Archive of Formal Proofs}, month = jan, year = 2018, note = {\url{http://isa-afp.org/entries/Green.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.