An Isabelle/HOL formalisation of Green’s theorem
Lecture Notes in Computer Science
MetadataShow full item record
Abdulaziz, M., & Paulson, L. (2016). An Isabelle/HOL formalisation of Green’s theorem. Lecture Notes in Computer Science, 9807 3-19. https://doi.org/10.1007/978-3-319-43144-4_1
We formalise a statement of Green’s theorem in Isabelle/ HOL, which is its first formalisation to our knowledge. The theorem statement that we formalise is enough for most applications, especially in physics and engineering. An interesting aspect of our formalisation is that we neither formalise orientations nor region boundaries explicitly, with respect to the outwards-pointing normal vector. Instead we refer to equivalences between paths.
External DOI: https://doi.org/10.1007/978-3-319-43144-4_1
This record's URL: https://www.repository.cam.ac.uk/handle/1810/262376