Abstract
We present an Isabelle/HOL development that allows for the automatic generation of certain operations for user-defined datatypes. Since the operations are defined within the logic, they are applicable for code generation. Triggered by the demand to provide readable error messages as well as to access efficient data structures like sorted trees in generated code, we provide show functions that compute the string representation of a given value, comparators that yield linear orders, and hash functions. Moreover, large parts of the employed machinery should be reusable for other operations like read functions, etc.
In contrast to similar mechanisms, like Haskell’s “deriving,” we do not only generate definitions, but also prove some desired properties, e.g., that a comparator indeed orders values linearly. This is achieved by a collection of tactics that discharge the corresponding proof obligations automatically.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
A further technicality—allowing for things like phantom types—is the separation between “used” and “unused” type parameters. To simplify matters, we consider all variables to be “used” in the remainder, even though our implementation also supports “unused” ones.
- 2.
- 3.
References
Blanchette, J.C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 93–110. Springer, Heidelberg (2014). doi:10.1007/978-3-319-08970-6_7
Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.-G.: A fully verified executable LTL model checker. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 463–478. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_31
Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 103–117. Springer, Heidelberg (2010). doi:10.1007/978-3-642-12251-4_9
Hinze, R., Peyton Jones, S.: Derivable type classes. ENTCS 41(1), 5–35 (2001). doi:10.1016/S1571-0661(05)80542-0
Krauss, A.: Partial and nested recursive function definitions in higher-order logic. JAR 44(4), 303–336 (2010). doi:10.1007/s10817-009-9157-2
Lammich, P., Lochbihler, A.: The Isabelle collections framework. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 339–354. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14052-5_24
Lochbihler, A.: Light-weight containers for Isabelle: efficient, extensible, nestable. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 116–132. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39634-2_11
Magalhães, J.P., Dijkstra, A., Jeuring, J., Löh, A.: A generic deriving mechanism for Haskell. SIGPLAN Not. 45(11), 37–48 (2010). doi:10.1145/2088456.1863529
Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Peyton Jones, S.: The Haskell 98 language. JFP 13(1), 139–144 (2003). doi:10.1017/S0956796803001217
Slind, K., Hurd, J.: Applications of polytypism in theorem proving. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 103–119. Springer, Heidelberg (2003). doi:10.1007/10930755_7
Sternagel, C., Thiemann, R.: Haskell’s show-class in Isabelle/HOL. Archive of Formal Proofs, July 2014. http://afp.sf.net/entries/Show.shtml
Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 452–468. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03359-9_31
Thiemann, R.: Generating linear orders for datatypes. Archive of Formal Proofs, August 2012. http://afp.sf.net/entries/Datatype_Order_Generator.shtml
Traytel, D., Popescu, A., Blanchette, J.C.: Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving. In: Proceedings of the 27th LICS, pp. 596–605 (2012). doi:10.1109/LICS.2012.75
Acknowledgments
We thank S. Berghofer, J. Blanchette, L. Bulwahn, F. Haftmann, B. Huffman, A. Krauss, P. Lammich, A. Lochbihler, C. Urban, T. Nipkow, D. Traytel, and M. Wenzel for their valuable support w.r.t. motivating our development, information on the old and new datatype packages, and for answering several Isabelle/ML related questions. We thank the anonymous reviewers for their helpful comments. This work was supported by Austrian Science Fund (FWF) projects P27502 and Y757. The authors are listed in alphabetical order regardless of individual contribution or seniority.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Sternagel, C., Thiemann, R. (2015). Deriving Comparators and Show Functions in Isabelle/HOL. In: Urban, C., Zhang, X. (eds) Interactive Theorem Proving. ITP 2015. Lecture Notes in Computer Science(), vol 9236. Springer, Cham. https://doi.org/10.1007/978-3-319-22102-1_28
Download citation
DOI: https://doi.org/10.1007/978-3-319-22102-1_28
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-22101-4
Online ISBN: 978-3-319-22102-1
eBook Packages: Computer ScienceComputer Science (R0)