Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] new AFP entry: Green's Theorem


view this post on Zulip Email Gateway (Aug 22 2022 at 16:34):

From: Gerwin.Klein@data61.csiro.au
[https://www.isa-afp.org/entries/Green.html]

An Isabelle/HOL formalisation of Green's Theorem
by Mohammad Abdulaziz and Lawrence C. Paulson

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.

Enjoy!
Gerwin


Last updated: Mar 29 2024 at 04:18 UTC