Top

Journal of Automated Reasoning

Published in:

09-11-2018

An Isabelle/HOL Formalisation of Green’s Theorem

Authors: Mohammad Abdulaziz, Lawrence C. Paulson

Published in: Journal of Automated Reasoning | Issue 3/2019

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

previous article Wombit: A Portfolio Bit-Vector Solver Using Word-Level Propagation

next article Formalization of Geometric Algebra in HOL Light

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

The gauge integral [15] is a generalisation of the well-known Riemann integral.

Formally, this observation follows immediately from theorem

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9495-z/MediaObjects/10817_2018_9495_Figbj_HTML.gif

This is not exactly true, since the instantiations

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9495-z/MediaObjects/10817_2018_9495_Figea_HTML.gif

and

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9495-z/MediaObjects/10817_2018_9495_Figeb_HTML.gif

are obtained using a pair of orthonormal unit vectors

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9495-z/MediaObjects/10817_2018_9495_Figec_HTML.gif

and

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9495-z/MediaObjects/10817_2018_9495_Figed_HTML.gif

. If

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9495-z/MediaObjects/10817_2018_9495_Figee_HTML.gif

and

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9495-z/MediaObjects/10817_2018_9495_Figef_HTML.gif

are to be assigned to

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9495-z/MediaObjects/10817_2018_9495_Figeg_HTML.gif

and

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9495-z/MediaObjects/10817_2018_9495_Figeh_HTML.gif

, then the instantiations of

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9495-z/MediaObjects/10817_2018_9495_Figei_HTML.gif

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9495-z/MediaObjects/10817_2018_9495_Figej_HTML.gif

and

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9495-z/MediaObjects/10817_2018_9495_Figek_HTML.gif

can be seen as the x-axis and y-axis Green statements.

Rutter [13] explains curve speeds and velocities.

bitbucket.org/MohammadAbdulaziz/isabellegeometry/

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)MATH

Federer, H.: Geometric Measure Theory. Springer, Berlin (2014)MATH

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)MathSciNetCrossRefMATH

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)MathSciNetMATH

10.

Michael, J.: An approximation to a rectifiable plane curve. J. Lond. Math. Soc. 1(1), 1–11 (1955)MathSciNetCrossRefMATH

11.

Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: a proof assistant for higher-order logic. Springer, Berlin (2002)

12.

Protter, M.H.: Basic Elements of Real Analysis. Springer, Berlin (2006)MATH

13.

Rutter, J.W.: Geometry of Curves. CRC press, Boca Raton (2000)CrossRefMATH

14.

Spivak, M.: A Comprehensive Introduction to Differential Geometry. Publish or Perish Inc., University of Tokyo Press (1981)MATH

15.

Swartz, C.: Introduction to Gauge Integrals. World Scientific, Singapore (2001)CrossRefMATH

16.

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)

17.

Zorich, V.A., Cooke, R.: Mathematical Analysis II. Springer, Berlin (2004)

Title: An Isabelle/HOL Formalisation of Green’s Theorem
Authors: Mohammad Abdulaziz
Lawrence C. Paulson
Publication date: 09-11-2018
Publisher: Springer Netherlands
Published in: Journal of Automated Reasoning / Issue 3/2019
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-018-9495-z

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 3/2019

Formally Verifying the Solution to the Boolean Pythagorean Triples Problem

A PSpace Algorithm for Acyclic Epistemic DL

Wombit: A Portfolio Bit-Vector Solver Using Word-Level Propagation

Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF

Formalization of Geometric Algebra in HOL Light

Semantics of Mizar as an Isabelle Object Logic

Premium Partner