An Isabelle/HOL formalisation of Green's Theorem


Title: An Isabelle/HOL formalisation of Green's Theorem
Authors: Mohammad Abdulaziz (mohammad /dot/ abdulaziz8 /at/ gmail /dot/ com) 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.
  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{},
            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.