peteg's blog - cs - 2007 03 14 InsertionSort

Proving insertion sort correct.

Wed, Mar 14, 2007./cs | Link
Fun and games. All I want to do is convince Isabelle of the proposition that, for a given list of objects, there is a permutation that is sorted according to a given order. In case anyone thinks this is completely trivial, I ask that you try to show that a recursive insertion sort does it before reading this cheat sheet. Perhaps merge sort is easier. Anyway, it is annoying that there appear to be no results on sorting sequences in Isabelle's library.