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
theory Sort_Impl
imports "~~/src/HOL/Library/Multiset"
begin
section {* GHC version of merge sort *}
context linorder
begin
text {*
Split a list into chunks of ascending and descending parts, where
descending parts are reversed. Hence, the result is a list of
sorted lists.
*}
fun sequences :: "'a list => 'a list list"
and ascending :: "'a => ('a list => 'a list) => 'a list => 'a list list"
and descending :: "'a => 'a list => 'a list => 'a list list"
where
"sequences (a#b#xs) = (if a > b
then descending b [a] xs
else ascending b (op # a) xs)"
| "sequences xs = [xs]"
| "ascending a f (b#bs) = (if ~ a > b
then ascending b (f o op # a) bs
else f [a] # sequences (b#bs))"
| "ascending a f bs = f [a] # sequences bs"
| "descending a as (b#bs) = (if a > b
then descending b (a#as) bs
else (a#as) # sequences (b#bs))"
| "descending a as bs = (a#as) # sequences bs"
fun merge :: "'a list => 'a list => 'a list" where
"merge (a#as) (b#bs) = (if a > b
then b # merge (a#as) bs
else a # merge as (b#bs))"
| "merge [] bs = bs"
| "merge as [] = as"
fun merge_pairs :: "'a list list => 'a list list" where
"merge_pairs (a#b#xs) = merge a b # merge_pairs xs"
| "merge_pairs xs = xs"
lemma merge_length[simp]: "length (merge xs ys) = length xs + length ys"
by (induct xs ys rule: merge.induct) simp_all
lemma merge_pairs_length[simp]: "length (merge_pairs xs) <= length xs"
by (induct xs rule: merge_pairs.induct) simp_all
fun merge_all :: "'a list list => 'a list" where
"merge_all [] = []"
| "merge_all [x] = x"
| "merge_all xs = merge_all (merge_pairs xs)"
definition msort :: "'a list => 'a list" where
"msort = merge_all o sequences"
lemma set_merge[simp]: "set (merge xs ys) = set xs Un set ys"
by (induct xs ys rule: merge.induct) auto
lemma sorted_merge[simp]: "sorted xs ==> sorted ys ==> sorted (merge xs ys)"
by (induct xs ys rule: merge.induct) (auto simp: sorted_Cons)
lemma multiset_of_merge[simp]: "multiset_of (merge xs ys) = multiset_of xs +
multiset_of ys"
by (induct xs ys rule: merge.induct) (auto simp: ac_simps)
lemma sorted_merge_pairs[simp]:
"ALL x:set xs. sorted x ==> ALL x:set (merge_pairs xs). sorted x"
by (induct xs rule: merge_pairs.induct) simp_all
lemma multiset_of_merge_pairs[simp]:
"multiset_of (concat (merge_pairs xs)) = multiset_of (concat xs)"
by (induct xs rule: merge_pairs.induct) (auto simp: ac_simps)
lemma sorted_merge_all: "ALL x:set xs. sorted x ==> sorted (merge_all xs)"
by (induct xs rule: merge_all.induct) simp_all
lemma multiset_of_merge_all[simp]:
"multiset_of (merge_all xs) = multiset_of (concat xs)"
by (induct xs rule: merge_all.induct) (auto simp: ac_simps)
lemma
shows sorted_sequences: "ALL x:set (sequences xs). sorted x"
and "[| ALL x:set (f []). x <= a; sorted (f []); ALL xs ys. f (xs@ys) = f xs
@ ys;
ALL x. f [x] = f [] @ [x] |] ==> ALL x:set (ascending a f xs). sorted x"
and "[| ALL x:set bs. c <= x; sorted bs |] ==> ALL x:set (descending c bs
xs). sorted x"
by (induct xs and a f xs and c bs xs rule:
sequences_ascending_descending.induct)
(simp_all add: sorted_append sorted_Cons,
metis append_Cons append_Nil le_less_linear order_trans,
metis less_le less_trans)
lemma
shows multiset_of_sequences[simp]: "multiset_of (concat (sequences xs)) =
multiset_of xs"
and "(!!x xs. multiset_of (f (x#xs)) = {#x#} + multiset_of (f []) +
multiset_of xs)
==> multiset_of (concat (ascending a f xs)) = {#a#} + multiset_of (f []) +
multiset_of xs"
and "multiset_of (concat (descending c bs xs)) = {#c#} + multiset_of bs +
multiset_of xs"
by (induct xs and a f xs and c bs xs rule:
sequences_ascending_descending.induct)
(simp_all add: ac_simps)
lemma multiset_of_msort[simp]: "multiset_of (msort xs) = multiset_of xs"
by (simp add: msort_def o_def)
lemma sorted_msort[simp]: "sorted (msort xs)"
by (simp add: msort_def o_def sorted_merge_all[OF sorted_sequences])
lemma sort_msort: "sort = msort"
by (intro ext properties_for_sort) simp_all
end
end
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
