[isabelle-dev] Merge-Sort Implementation
christian.sternagel at uibk.ac.at
Thu Oct 27 13:32:23 CEST 2011
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
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...
More information about the isabelle-dev