[isabelle-dev] Merge-Sort Implementation

Christian Sternagel christian.sternagel at uibk.ac.at
Thu Oct 27 13:32:23 CEST 2011

Hi all,

please find attached the formalization of the merge-sort algorithm as 
used in GHC's standard library. See also:


Due to experiments and comments found there, I suggest that this 
implementation is used in future Isabelle releases for Haskell 
code-generation ;)

Some compliments are also in order:

1) I was positively surprised that the mutually recursive functions 
sequences, ascending, and descending where accepted without further ado 
by the function package.

2) Sledgehammer is great! It shrunk the proof of sorted_sequences from 7 
explicit cases (about 50 lines) -- with lots of tedious instantiations 
to make simp or force solve the goal -- to 4 lines. And the resulting 
metis proof is much faster than my original one.


-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: Sort_Impl.thy
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20111027/10c68bd2/attachment.ksh>

More information about the isabelle-dev mailing list