Abstract
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 first mechanisation of Green’s theorem.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Notes
The gauge integral [15] is a generalisation of the well-known Riemann integral.
Formally, this observation follows immediately from theorem
.
This is not exactly true, since the instantiations
and
are obtained using a pair of orthonormal unit vectors
and
. If
and
are to be assigned to
and
, then the instantiations of
in
and
can be seen as the x-axis and y-axis Green statements.
Rutter [13] explains curve speeds and velocities.
bitbucket.org/MohammadAbdulaziz/isabellegeometry/
References
Abdulaziz, M., Paulson, L.C.: An Isabelle/HOL formalisation of Green’s theorem. In: Blanchette, J.C., Merz, S. (eds.) Interactive Theorem Proving—7th International Conference, ITP 2016. pp. 3–19. Springer (2016)
Apostol, T.M.: Calculus, vol. 2, 2nd edn. Wiley, New York (1969)
Federer, H.: Geometric Measure Theory. Springer, Berlin (2014)
Green, G.: An essay on the application of mathematical analysis to the theories of electricity and magnetism. (1828) arXiv:0807.0088
Harrison, J.: Formalizing basic complex analysis. From Insight to Proof: Festschrift in Honour of Andrzej Trybulec. Stud. Logic Gramm. Rhetor. 10(23), 151–165 (2007)
Harrison, J.: The HOL Light theory of Euclidean space. J. Autom. Reason. 50(2), 173–190 (2013)
Hölzl, J., Heller, A.: Three chapters of measure theory in Isabelle/HOL. In: Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) Interactive Theorem Proving—Second International Conference, pp. 135–151. Springer (2011)
Hölzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving—4th International Conference, pp. 279–294. Springer (2013)
Jurkat, W., Nonnenmacher, D.: The general form of Green’s theorem. Proc. Am. Math. Soc. 109(4), 1003–1009 (1990)
Michael, J.: An approximation to a rectifiable plane curve. J. Lond. Math. Soc. 1(1), 1–11 (1955)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: a proof assistant for higher-order logic. Springer, Berlin (2002)
Protter, M.H.: Basic Elements of Real Analysis. Springer, Berlin (2006)
Rutter, J.W.: Geometry of Curves. CRC press, Boca Raton (2000)
Spivak, M.: A Comprehensive Introduction to Differential Geometry. Publish or Perish Inc., University of Tokyo Press (1981)
Swartz, C.: Introduction to Gauge Integrals. World Scientific, Singapore (2001)
Wenzel, M.: Type classes and overloading in higher-order logic. In: Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs’97, Murray Hill, NJ, USA, August 19–22, 1997, Proceedings, pp. 307–322 (1997)
Zorich, V.A., Cooke, R.: Mathematical Analysis II. Springer, Berlin (2004)
Acknowledgements
We thank Johannes Hoelzl, Fabian Immler and Manuel Eberl for their help with different aspects of the Analysis Library and for the useful discussions we had with them. We also note that the first author is supported by the DFG Koselleck Grant NI 491/16-1 and that the second author is supported by the ERC Advanced Grant ALEXANDRIA (Project 742178).
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Abdulaziz, M., Paulson, L.C. An Isabelle/HOL Formalisation of Green’s Theorem. J Autom Reasoning 63, 763–786 (2019). https://doi.org/10.1007/s10817-018-9495-z
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-018-9495-z