[isabelle-dev] Merge-Sort Implementation

[Christian Sternagel]

Hi all,

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

http://hackage.haskell.org/packages/archive/base/latest/doc/html/src/Data-List.html#sort

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.

cheers

chris
-------------- 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>