Automatic Functional Correctness Proofs for Functional Search Trees

Tobias Nipkow

In a new approach, functional correctness specifications of insert/update and delete operations on search trees are expressed on the level of lists by means of an inorder traversal function that projects trees to lists. With the help of a small lemma library, functional correctness and preservation of the search tree property are proved automatically (in Isabelle/HOL) for a range of data structures: unbalanced binary trees, AVL trees, red-black trees, 2-3 trees, 2-3-4 trees, 1-2 brother trees, AA trees and splay trees.



author={Tobias Nipkow},
title={Automatic Functional Correctness Proofs for Functional Search Trees},
booktitle={Interactive Theorem Proving (ITP 2016)},
editor={J. Blanchette and S. Merz},

Isabelle theories