{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,9]],"date-time":"2026-10-09T00:35:03Z","timestamp":1791506103757,"version":"4.3.4"},"reference-count":33,"publisher":"Wiley","license":[{"start":{"date-parts":[[2010,2,1]],"date-time":"2010-02-01T00:00:00Z","timestamp":1264982400000},"content-version":"unspecified","delay-in-days":3684,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["LMS J. Comput. Math."],"published-print":{"date-parts":[[2000]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper first describes the construction and use of the hyperreals in the theorem-prover Isabelle within the framework of higher-order logic (HOL). The theory, which includes infinitesimals and infinite numbers, is based on the hyperreal number system developed by Abraham Robinson in his nonstandard analysis (NSA). The construction of the hyperreal number system has been carried out strictly through the use of definitions to ensure that the foundations of NSA in Isabelle are sound. Mechanizing the construction has required that various number systems including the rationals and the reals be built up first. Moreover, to construct the hyperreals from the reals has required developing a theory of filters and ultrafilters and proving Zorn's lemma, an equivalent form of the axiom of choice.<\/jats:p><jats:p>This paper also describes the use of the new types of numbers and new relations on them to formalize familiar concepts from analysis. The current work provides both standard and nonstandard definitions for the various notions, and proves their equivalence in each case. To achieve this aim, systematic methods, through which sets and functions are extended to the hyperreals, are developed in the framework. The merits of the nonstandard approach with respect to the practice of analysis and mechanical theorem-proving are highlighted throughout the exposition.<\/jats:p>","DOI":"10.1112\/s1461157000000267","type":"journal-article","created":{"date-parts":[[2010,10,21]],"date-time":"2010-10-21T15:23:10Z","timestamp":1287674590000},"page":"140-190","source":"Crossref","is-referenced-by-count":10,"title":["Mechanizing Nonstandard Real Analysis"],"prefix":"10.1112","volume":"3","author":[{"given":"Jacques D.","family":"Fleuriot","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"311","published-online":{"date-parts":[[2010,2,1]]},"reference":[{"key":"S1461157000000267_ref032","volume-title":"Introduction to the theory of infinitesimals","author":"Stroyan","year":"1976"},{"key":"S1461157000000267_ref013","first-page":"145","volume-title":"Proceedings of the IFIP TC10\/WG10.2 International Workshop on Higher Order Logic Theorem Proving and its Applications","author":"Harrison","year":"1992"},{"key":"S1461157000000267_ref002","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1145\/322017.322018","article-title":"\u2018Automatic proofs of theorems in analysis using nonstandard analysis\u2019","volume":"24","author":"Ballantyne","year":"1977","journal-title":"J. ACM"},{"key":"S1461157000000267_ref008","volume-title":"On numbers and games","author":"Conway","year":"1976"},{"key":"S1461157000000267_ref024","first-page":"161","volume-title":"Proc. 25th ACM Symp. Principles of Programming Languages","author":"Nipkow","year":"1998"},{"key":"S1461157000000267_ref017","volume-title":"P. A. LOEB, An introduction to nonstandard real analysis","volume":"118","author":"Hurd","year":"1985"},{"key":"S1461157000000267_ref022","doi-asserted-by":"publisher","DOI":"10.1016\/0315-0860(87)90045-0"},{"key":"S1461157000000267_ref033","volume-title":"Constructive Mathematics","volume":"873","author":"Vesley","year":"1983"},{"key":"S1461157000000267_ref003","unstructured":"3. Bedrax T. , \u2018Infmal: prototype of an interactive theorem prover based on infinitesimal analysis\u2019, Master's thesis, Pontifica Universidad Catolica de Chile, 1993. Liciendoen Mathematica con Mencion en Computation Thesis."},{"key":"S1461157000000267_ref018","unstructured":"18. \u2018Isabelle-online\u2019, http:\/\/www.cl.cam.ac.uk\/Research\/HVG\/Isabelle\/library\/HOL\/HOL-Real\/index.html"},{"key":"S1461157000000267_ref025","article-title":"Lecture Notes in Comput. Sci.","author":"Paulson","year":"1994","journal-title":"Isabelle: a generic theorem prover"},{"key":"S1461157000000267_ref020","unstructured":"20. Keisler H. J. , Foundations of infinitesimal calculus (Prindle, Weber & Schmidt, 1976)."},{"key":"S1461157000000267_ref005","volume-title":"A second course in mathematical analysis","author":"Burkill","year":"1970"},{"key":"S1461157000000267_ref010","first-page":"3\u201816","volume-title":"Automated deduction \u2014CADE-15","author":"Fleuriot","year":"1998"},{"key":"S1461157000000267_ref014","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-1591-5"},{"key":"S1461157000000267_ref007","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"S1461157000000267_ref016","article-title":"Standard and nonstandard analysis","author":"Hoskins","year":"1990","journal-title":"Math. Appl."},{"key":"S1461157000000267_ref001","unstructured":"1. Abrial J. R. and Laffitte G. , \u2018Towards the mechanization of the proofs of some classical theorems of set theory\u2018, Preprint, February 1993."},{"key":"S1461157000000267_ref027","unstructured":"27. Paulson L. C. , \u2018Isabelle's object-logics\u2019, Tech. Rep. 286, Computer Laboratory, University of Cambridge (February 1998)."},{"key":"S1461157000000267_ref011","article-title":"Series in Mathematics","author":"Gleason","year":"1966","journal-title":"Fundamentals of abstract analysis"},{"key":"S1461157000000267_ref015","volume-title":"Infinitesimal calculus","author":"Henle","year":"1979"},{"key":"S1461157000000267_ref021","unstructured":"21. Landau E. , Foundations of analysis (Chelsea, 1951)."},{"key":"S1461157000000267_ref019","unstructured":"19. Jutting L. S. , \u2018Checking Landau's \u201cGrundlagen\u201d in the Automath system\u2019, Ph.D. thesis, Eindhoven University of Technology, 1977."},{"key":"S1461157000000267_ref029","unstructured":"29. Robinson A. , Non-standard analysis (North-Holland, 1980)."},{"key":"S1461157000000267_ref004","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054195000172"},{"key":"S1461157000000267_ref009","unstructured":"9. Davis P. J. and Hersh R. , The mathematical experience (Harmondsworth, Penguin, 1983)."},{"key":"S1461157000000267_ref030","volume-title":"Handbook of analysis and its foundations","author":"Schechter","year":"1997"},{"key":"S1461157000000267_ref031","doi-asserted-by":"publisher","DOI":"10.1007\/BF03024016"},{"key":"S1461157000000267_ref023","first-page":"1","volume-title":"Nonstandard analysis and its applications","author":"Lindstr\u00f8m","year":"1988"},{"key":"S1461157000000267_ref028","first-page":"291","article-title":"\u2018Mechanizing set theory: cardinal arithmetic and the axiom of choice\u2019","volume":"17","author":"Paulson","year":"1996","journal-title":"Journal of Automat. Reason."},{"key":"S1461157000000267_ref006","doi-asserted-by":"publisher","DOI":"10.2307\/2275512"},{"key":"S1461157000000267_ref026","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1998-61-205"},{"key":"S1461157000000267_ref012","volume-title":"Introduction to HOL: a theorem proving environment for higher order logic","author":"Gordon","year":"1993"}],"container-title":["LMS Journal of Computation and Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1461157000000267","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T23:49:21Z","timestamp":1559951361000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1461157000000267\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"references-count":33,"alternative-id":["S1461157000000267"],"URL":"https:\/\/doi.org\/10.1112\/s1461157000000267","relation":{},"ISSN":["1461-1570"],"issn-type":[{"value":"1461-1570","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000]]}}}