Formalization of metric spaces in HOL Light Copyright (c) 20142015 Marco Maggesi The files in this folder contain a formalization of metric spaces for the HOL Light theorem prover. This code is now part of the HOL Light distribution (since svn revision 230 of 20150517) with the exception of the file metricarith.hl. The most important results proved in this formalization are the Contraction Mapping Principle (also known as Banach FixedPoint Theorem), the completeness of the space of continuous bounded functions and the Baire Category theorem. An implementation of a simple decision procedure for metric spaces, as described in the paper R. M. Solovay, R. D. Arthan, J. Harrison "Some new results on decidability for elementary algebra and geometry" http://arxiv.org/abs/0904.3482 is also included. As an application, we prove the PicardLindelĂ¶f theorem (or CauchyLipschitz theorem) about the existence of the solutions of ordinary differential equations. Part of this code is based on a previous work of Claudia Carapelle. For practical reasons, everything has been rewritten from scratch in order to change certain implementation choices and for better adherence to the HOL Light coding style.
Source
Metric /
Filename  Size  Date modified  Message 

1.3 KB

…  
1.3 KB

…  
21.9 KB

…  
2.2 KB

…  
22.3 KB

…  
1.0 KB

…  
78.6 KB

…  
11.6 KB

…  
2.9 KB

…  
2.0 KB

…  
7.7 KB

… 