General purpose theorem provers provide sophisticated proof methods, but lack some of the advanced structuring mechanisms found in specification languages. This paper builds on previous work extending the theorem prover Isabelle with such mechanisms. A way to build the quotient type over a given base type and an equivalence relation on it, and a generalised notion of folding over quotiented types is given as a formalised high-level step called a design tactic. The core of this paper are four axiomatic theories capturing the design tactic. The applicability is demonstrated by derivations of implementations for finite multisets and finite sets from lists in Isabelle. © 2010 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Bortin, M., & Lüth, C. (2010). Structured formal development with quotient types in Isabelle/HOL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6167 LNAI, pp. 34–48). https://doi.org/10.1007/978-3-642-14128-7_5
Mendeley helps you to discover research relevant for your work.