Exploring the structure of an algebra text with locales. (English) Zbl 1468.68277

Summary: Locales, the module system of the theorem prover Isabelle, were designed so that developments in abstract algebra could be represented faithfully and concisely. Whether these goals were met is assessed through a case study. Parts of an algebra textbook, N. Jacobson’s [Basic algebra I. 2nd ed. New York: W. H. Freeman and Company (1985; Zbl 0557.16001)], that are challenging structurally were formalised. Key parts of the formalisation are presented in greater detail. An analysis of the work from both qualitative and quantitative perspectives substantiates that the design goals were met. In particular, the size ratio of formal to “pen and paper” text does not increase when going further into the book. The analysis also yields guidance on locales including patterns of use, which are identified and described.


68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
68V20 Formalization of mathematics in connection with theorem provers


Zbl 0557.16001
Full Text: DOI


[1] Aransay, J.; Ballarin, C.; Rubio, J., A mechanized proof of the basic perturbation lemma, J. Autom. Reason., 40, 4, 271-292 (2008) · Zbl 1140.68059
[2] Bailey, A.: The Machine-Checked Literate Formalisation of Algebra in Type Theory. Ph.D. Thesis, University of Manchester (1998)
[3] Ballarin, C.; Berardi, S.; Coppo, M.; Damiani, F., Locales and locale expressions in Isabelle/Isar, Types for Proofs and Programs, TYPES 2003, Torino, Italy, LNCS 3085, 34-50 (2004), Berlin: Springer, Berlin · Zbl 1100.68615
[4] Ballarin, C.: Tutorial to locales and locale interpretation. In: Lambán, L., Romero, A., Rubio, J. (eds.) Contribuciones Científicas en honor de Mirian Andrés Gómez. Servicio de Publicaciones de la Universidad de La Rioja, Logroño, Spain, Also part of the Isabelle user documentation (2010) · Zbl 1215.68208
[5] Ballarin, C.: Reading an algebra textbook. In: Lange C. et al. (eds.) CEUR Workshop Proceedings 1010. Intelligent Computer Mathematics, Bath (2013)
[6] Ballarin, C., Locales: a module system for mathematical theories, J. Autom. Reason., 52, 2, 123-153 (2014) · Zbl 1315.68218
[7] Ballarin, C.: A case study in basic algebra. Archive of Formal Proofs https://isa-afp.org/entries/Jacobson_Basic_Algebra.html (2019)
[8] Ballarin, C. et al.: The Isabelle/HOL algebra library. Part of the Isabelle distribution, https://isabelle.in.tum.de/library/HOL/HOL-Algebra/
[9] Chan, H-L; Norrish, M.; Urban, C.; Zhang, X., Mechanisation of AKS algorithm: Part 1-the main theorem, Interactive Theorem Proving, ITP 2015, Nanjing, China, LNCS 9236, 117-136 (2015), Berlin: Springer, Berlin · Zbl 1465.68302
[10] Farmer, WM; Heering, J.; Mainke, K.; Möller, B.; Nipkow, T., Theory interpretation in simple type theory, Higher-Order Algebra, Logic, and Term Rewriting, HOA ’93, Amsterdam, The Netherlands, LNCS 816, 96-123 (1994), Berlin: Springer, Berlin
[11] Goguen, JA; Burstall, RM, Institutions: abstract model theory for specification and programming, J. ACM, 39, 1, 95-146 (1992) · Zbl 0799.68134
[12] Gunter, E.L.: Doing Algebra in Simple Type Theory. Technical Report MS-CIS-89-38, University of Pennsylvania (1989)
[13] Haftmann, F.; Wenzel, M.; Altenkirch, T.; McBride, C., Constructive type classes in Isabelle, Types for proofs and programs, TYPES 2006, Nottingham, UK, LNCS 4502, 160-174 (2007), Berlin: Springer, Berlin · Zbl 1178.68529
[14] Haftmann, F., Wenzel, M., (2009) Local theory specifications in Isabelle, Isar. In: Berardi S., Damiani F., de’Liguoro U. (eds) Types for Proofs and Programs, TYPES, Torino, Italy, LNCS 5497, pp. 153-168. Springer, Berlin (2008) · Zbl 1246.68197
[15] Harper, R.; Pierce, BC; Pierce, BC, Design considerations for ML-style module systems, Advanced Topics in Types and Programming Languages (2005), Cambridge: MIT Press, Cambridge
[16] Jacobson, N., Basic Algebra (1985), Dallas: Freeman, Dallas
[17] Kammüller, F.: Modular Reasoning in Isabelle. Ph.D. Thesis, University of Cambridge, Computer Laboratory, Also Technical Report No. 470 (1999) · Zbl 0942.68116
[18] Kammüller, F.; Wenzel, M.; Paulson, LC; Bertot, Y.; Dowek, G.; Hirschowitz, A.; Paulin, C.; Théry, L., Locales: a sectioning concept for Isabelle, Theorem Proving in Higher Order Logics: TPHOLs’99, Nice, France, LNCS 1690, 149-165 (1999), Berlin: Springer, Berlin
[19] Mahboubi, A.; Tassi, E.; Blazy, S.; Paulin-Mohring, C.; Pichardie, D., Canonical structures for the working Coq user, Interactive Theorem Proving, ITP 2013, Rennes, France, LNCS 7998, 19-34 (2013), Berlin: Springer, Berlin · Zbl 1317.68221
[20] Naraschewski, W., Wenzel, M.: Object-oriented verification based on record subtyping in higher-order logic. In: Theorem Proving in Higher Order Logics, LNCS 1479. Springer, pp 349-366 (1998) · Zbl 0927.03026
[21] Paulson, LC, Defining functions on equivalence classes, ACM Transactions on Computational Logic, 7, 4, 658-675 (2006) · Zbl 1367.68254
[22] Soubiran, E.: Modular Development of Theories and Name-Space Management for the Coq Proof Assistant. Ph.D. Thesis, École Polytechnique (2012)
[23] van Benthem Jutting, L.S.: Checking Landau’s “Grundlagen” in the Automath System. Ph.D Thesis, Technische Hogeschool Eindhoven (1977) · Zbl 0352.68105
[24] von Raumer, J.: Secondary Sylow Theorems. Archive of Formal Proofs, https://isa-afp.org/entries/Secondary_Sylow.html, (2014)
[25] Wenzel, M., Isabelle/Isar-a generic framework for human-readable proof documents, Stud. Log. Gramm. Rhetor., 10, 23, 277-298 (2007)
[26] Wiedijk, F.: The de Bruijn factor. https://www.cs.ru.nl/ freek/factor/factor.pdf (2000)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.