@inproceedings{36ea4f90a49848d69002af8efedf069d,
title = "Exploring the Foundations of Discrete Analytical Geometry in Isabelle/HOL",
abstract = "This paper gives an overview of the formalization of the Harthong-Reeb integer number system (HRω) in the proof-assistant Isabelle. The work builds on an existing mechanization of nonstandard analysis and describes how the basic notions underlying HRω can be recovered and shown to have their expected properties, without the need to introduce any axioms. We also look at the formalization of the well-known Euler method over the new integers and formally prove that the algorithmic approximation produced can be made to be infinitely-close to its continuous counterpart. This enables the discretization of continuous functions and of geometric concepts such as the straight line and ellipse and acts as the starting point for the field of discrete analytical geometry.",
author = "Jacques Fleuriot",
year = "2011",
doi = "10.1007/978-3-642-25070-5_2",
language = "English",
isbn = "978-3-642-25069-9",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "34--50",
editor = "Pascal Schreck and Julien Narboux and J{\"u}rgen Richter-Gebert",
booktitle = "Automated Deduction in Geometry",
address = "United Kingdom",
}