Repository logo
 

An Isabelle/HOL Formalisation of Green’s Theorem

Accepted version
Peer-reviewed

Type

Book chapter

Change log

Authors

Abdulaziz, Mohammad 
Paulson, LC 

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.

Description

Title

An Isabelle/HOL Formalisation of Green’s Theorem

Keywords

Is Part Of

Interactive Theorem Proving

Book type

Publisher

Springer

ISBN

Sponsorship
European Research Council (742178)