### 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.

### License

BSD License

### Topics

- Mathematics/Analysis

### Session Green

- General_Utils
- Derivs
- Integrals
- Paths
- Green
- SymmetricR2Shapes
- CircExample
- DiamExample

## Cite

×

Green-AFP

    @article{Green-AFP,
      author  = {Mohammad Abdulaziz and Lawrence C. Paulson},
      title   = {An Isabelle/HOL formalisation of Green's Theorem},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Green.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Jan 12, 2018 : Isabelle2017