Publikation
Structural Formal Development with Quotient Types in Isabelle/HOL
Maksym Bortin; Christoph Lüth
In: 10th International Conference on Artificial Intelligence and Symbolic Computation (AISC 2010). International Conference on Artificial Intelligence and Symbolic Computation (AISC-2010), 10th, located at Intelligent Computer Mathematics 2010 (CICM 2010), July 5-10, Paris, France, Pages 34-48, Lecture Notes in Computer Science (LNCS), Vol. 6167, Springer, 2010.
Zusammenfassung
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.