Structural Formal Development with Quotient Types in Isabelle/HOL
Maksym Bortin; Christoph Lüth
In: 10th International Conference on Artificial Intelligence and Symbolic Computation. 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, Vol. 6167, Springer, 2010.
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.