Re: [isabelle-dev] Merge-Sort Implementation (and a question, on induction_schema)
Hi Christian, I am not completely sure what you mean. It is possible to leave key out of the conclusion in sequences_induct. lemma sequences_induct[case_names Nil singleton IH]: assumes P [] and !!x. P [x] and !!a b xs. [| key b key a == P (drop_desc key b xs); ~ key b key a == P (drop_asc key b xs) |] == P (a # b # xs) shows P xs using assms by (induction_schema)(pat_completeness, lexicographic_order) However, when you apply this rule using induct, key is not instantiated by unification. In order to use the case Nil syntax in Isar proofs, you must explicitly instantiate key in the induction method via the taking clause. Otherwise, key is left as an unbound variable in the goal state. For example: proof(induct xs taking: concrete_key rule: sequences_induct) Andreas -- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Adenauerring 20a, Geb. 50.41, Raum 031 76131 Karlsruhe Telefon: +49 721 608-47399 Fax: +49 721 608-48457 E-Mail: andreas.lochbih...@kit.edu http://pp.info.uni-karlsruhe.de KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Merge-Sort Implementation (and a question, on induction_schema)
Hi Andreas, taking was actually what I was searching for, thanks! I just found it strange to write (induct key xs rule: ...) when key staid the same all the time. cheers chris On 11/03/2011 12:40 PM, Andreas Lochbihler wrote: Hi Christian, I am not completely sure what you mean. It is possible to leave key out of the conclusion in sequences_induct. lemma sequences_induct[case_names Nil singleton IH]: assumes P [] and !!x. P [x] and !!a b xs. [| key b key a == P (drop_desc key b xs); ~ key b key a == P (drop_asc key b xs) |] == P (a # b # xs) shows P xs using assms by (induction_schema)(pat_completeness, lexicographic_order) However, when you apply this rule using induct, key is not instantiated by unification. In order to use the case Nil syntax in Isar proofs, you must explicitly instantiate key in the induction method via the taking clause. Otherwise, key is left as an unbound variable in the goal state. For example: proof(induct xs taking: concrete_key rule: sequences_induct) Andreas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Merge-Sort Implementation (and a question, on induction_schema)
Dear Christian, I ironed out the apply-style snippets and simplified some proofs. Also Christian's pointer to induction_schema significantly shortened the proof of an induction schema I use (sequences_induct). induction_schema is really useful! However, another induction schema (merge_induct) seems to be wrong for induction_schema. Maybe because of an additional assumption? Any ideas? Induction_schema is picky about the order of assumptions. Additional assumptions (typically those for consumes) must be fed into the induction_schema method *after* the inductive cases. Moreover, in your lemma sorted_merge_induct, P must not take key as argument because all inductive cases simply pass key on to P. Otherwise, induction_schema does not terminate. Note that it is not necessary to have the key parameter either because unification instantiates key when it consumes the first assumption. Here's how sorted_merge_induct works with induction_schema: lemma sorted_merge_induct[consumes 1, case_names Nil IH]: fixes key::'b \Rightarrow 'a assumes sorted (map key xs) and \Andxs. P xs [] and \Andxs y ys. sorted (map key xs) \Longrightarrow P (dropWhile (\lambdax. key x \le key y) xs) ys \Longrightarrow P xs (y#ys) shows P xs ys using assms(2-) assms(1) apply(induction_schema) Andreas -- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Adenauerring 20a, Geb. 50.41, Raum 031 76131 Karlsruhe Telefon: +49 721 608-47399 Fax: +49 721 608-48457 E-Mail: andreas.lochbih...@kit.edu http://pp.info.uni-karlsruhe.de KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Merge-Sort Implementation (and a question on induction_schema)
I was about to suggest the same as Andreas. For what it is
worth, here is my proof of this lemma.
lemma sorted_merge_induct[consumes 1, case_names Nil IH]:
fixes key::'b = 'a
assumes sorted (map key xs)
and !!xs. P xs []
and !!xs y ys. sorted (map key xs) == P (dropWhile (%x. key x = key y)
xs) ys == P xs (y#ys)
shows P xs ys
using assms(2-3) assms(1)
apply(induction_schema)
apply(case_tac ys)
apply(auto)[2]
apply(metis map_append sorted_append takeWhile_dropWhile_id)
apply(lexicographic_order)
done
Christian
Christian Sternagel writes:
Hi once more,
I ironed out the apply-style snippets and simplified some proofs. Also
Christian's pointer to induction_schema significantly shortened the
proof of an induction schema I use (sequences_induct).
induction_schema is really useful! However, another induction schema
(merge_induct) seems to be wrong for induction_schema. Maybe because
of an additional assumption? Any ideas?
cheers
chris
On 10/30/2011 08:50 PM, Christian Sternagel wrote:
Hi again,
stability (the third property required by @{thm
properties_for_sort_key}) did actually cause some difficulties ;)
Hence the attached theory has rough parts in some proofs. But since I
spent the most part of the weekend on the proof, I decided to post it
anyway. Finally I can sleep well again ;)
have fun,
chris
On 10/27/2011 03:30 PM, Florian Haftmann wrote:
Indeed, that would be the obvious next step. I have not tried yet but
would not expect too hard difficulties. If this is of general interest I
can try.
Well, if you want to superseed the existing quicksort, you have to
provide the same generality ;-)
Florian
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
--
(*
Copyright 2011 Christian Sternagel, René Thiemann
This file is part of IsaFoR/CeTA.
IsaFoR/CeTA is free software: you can redistribute it and/or modify it under
the
terms of the GNU Lesser General Public License as published by the Free
Software
Foundation, either version 3 of the License, or (at your option) any later
version.
IsaFoR/CeTA is distributed in the hope that it will be useful, but WITHOUT
ANY
WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
FOR A
PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
details.
You should have received a copy of the GNU Lesser General Public License
along
with IsaFoR/CeTA. If not, see http://www.gnu.org/licenses/.
*)
theory Efficient_Sort
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 :: ('b \Rightarrow 'a) \Rightarrow 'b list \Rightarrow
'b list list
and ascending :: ('b \Rightarrow 'a) \Rightarrow 'b \Rightarrow ('b
list \Rightarrow 'b list) \Rightarrow 'b list \Rightarrow 'b list list
and descending :: ('b \Rightarrow 'a) \Rightarrow 'b \Rightarrow 'b
list \Rightarrow 'b list \Rightarrow 'b list list
where
sequences key (a#b#xs) = (if key a key b
then descending key b [a] xs
else ascending key b (op # a) xs)
| sequences key xs = [xs]
| ascending key a f (b#bs) = (if \not key a key b
then ascending key b (f \circ op # a) bs
else f [a] # sequences key (b#bs))
| ascending key a f bs = f [a] # sequences key bs
| descending key a as (b#bs) = (if key a key b
then descending key b (a#as) bs
else (a#as) # sequences key (b#bs))
| descending key a as bs = (a#as) # sequences key bs
fun merge :: ('b \Rightarrow 'a) \Rightarrow 'b list \Rightarrow 'b
list \Rightarrow 'b list where
merge key (a#as) (b#bs) = (if key a key b
then b # merge key (a#as) bs
else a # merge key as (b#bs))
| merge key [] bs = bs
| merge key as [] = as
fun merge_pairs :: ('b \Rightarrow 'a) \Rightarrow 'b list list
\Rightarrow 'b list list where
merge_pairs key (a#b#xs) = merge key a b # merge_pairs key xs
| merge_pairs key xs = xs
lemma length_merge[simp]:
length (merge key xs ys) = length xs + length ys
by (induct xs ys rule: merge.induct) simp_all
lemma merge_pairs_length[simp]:
length (merge_pairs key xs) \le length xs
by (induct xs rule: merge_pairs.induct) simp_all
fun merge_all :: ('b \Rightarrow 'a) \Rightarrow 'b
Re: [isabelle-dev] Merge-Sort Implementation (and a question on induction_schema)
Thnx Andreas and Christian,
that worked fine! One minor thing: in the proof of sequences_induct, is
it possible to use induction_schema such that 'key' is not needed as
argument when applying the resulting induction rule using induct?
cheers
chris
On 11/02/2011 01:08 PM, Christian Urban wrote:
I was about to suggest the same as Andreas. For what it is
worth, here is my proof of this lemma.
lemma sorted_merge_induct[consumes 1, case_names Nil IH]:
fixes key::'b = 'a
assumes sorted (map key xs)
and !!xs. P xs []
and !!xs y ys. sorted (map key xs) == P (dropWhile (%x. key x= key y) xs) ys
== P xs (y#ys)
shows P xs ys
using assms(2-3) assms(1)
apply(induction_schema)
apply(case_tac ys)
apply(auto)[2]
apply(metis map_append sorted_append takeWhile_dropWhile_id)
apply(lexicographic_order)
done
Christian
Christian Sternagel writes:
Hi once more,
I ironed out the apply-style snippets and simplified some proofs. Also
Christian's pointer to induction_schema significantly shortened the
proof of an induction schema I use (sequences_induct).
induction_schema is really useful! However, another induction schema
(merge_induct) seems to be wrong for induction_schema. Maybe because
of an additional assumption? Any ideas?
cheers
chris
On 10/30/2011 08:50 PM, Christian Sternagel wrote:
Hi again,
stability (the third property required by @{thm
properties_for_sort_key}) did actually cause some difficulties ;)
Hence the attached theory has rough parts in some proofs. But since I
spent the most part of the weekend on the proof, I decided to post it
anyway. Finally I can sleep well again ;)
have fun,
chris
On 10/27/2011 03:30 PM, Florian Haftmann wrote:
Indeed, that would be the obvious next step. I have not tried yet but
would not expect too hard difficulties. If this is of general
interest I
can try.
Well, if you want to superseed the existing quicksort, you have to
provide the same generality ;-)
Florian
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
--
(*
Copyright 2011 Christian Sternagel, René Thiemann
This file is part of IsaFoR/CeTA.
IsaFoR/CeTA is free software: you can redistribute it and/or modify it
under the
terms of the GNU Lesser General Public License as published by the Free
Software
Foundation, either version 3 of the License, or (at your option) any later
version.
IsaFoR/CeTA is distributed in the hope that it will be useful, but WITHOUT
ANY
WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
FOR A
PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
details.
You should have received a copy of the GNU Lesser General Public License
along
with IsaFoR/CeTA. If not, seehttp://www.gnu.org/licenses/.
*)
theory Efficient_Sort
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 :: ('b \Rightarrow 'a) \Rightarrow 'b list \Rightarrow
'b list list
and ascending :: ('b \Rightarrow 'a) \Rightarrow 'b \Rightarrow ('b list
\Rightarrow 'b list) \Rightarrow 'b list \Rightarrow 'b list list
and descending :: ('b \Rightarrow 'a) \Rightarrow 'b \Rightarrow 'b list
\Rightarrow 'b list \Rightarrow 'b list list
where
sequences key (a#b#xs) = (if key a key b
then descending key b [a] xs
else ascending key b (op # a) xs)
| sequences key xs = [xs]
| ascending key a f (b#bs) = (if \not key a key b
then ascending key b (f \circ op # a) bs
else f [a] # sequences key (b#bs))
| ascending key a f bs = f [a] # sequences key bs
| descending key a as (b#bs) = (if key a key b
then descending key b (a#as) bs
else (a#as) # sequences key (b#bs))
| descending key a as bs = (a#as) # sequences key bs
fun merge :: ('b \Rightarrow 'a) \Rightarrow 'b list \Rightarrow 'b list
\Rightarrow 'b list where
merge key (a#as) (b#bs) = (if key a key b
then b # merge key (a#as) bs
else a # merge key as (b#bs))
| merge key [] bs = bs
| merge key as [] = as
Re: [isabelle-dev] Merge-Sort Implementation (and a question on induction_schema)
Hi once more,
I ironed out the apply-style snippets and simplified some proofs. Also
Christian's pointer to induction_schema significantly shortened the
proof of an induction schema I use (sequences_induct).
induction_schema is really useful! However, another induction schema
(merge_induct) seems to be wrong for induction_schema. Maybe because
of an additional assumption? Any ideas?
cheers
chris
On 10/30/2011 08:50 PM, Christian Sternagel wrote:
Hi again,
stability (the third property required by @{thm
properties_for_sort_key}) did actually cause some difficulties ;)
Hence the attached theory has rough parts in some proofs. But since I
spent the most part of the weekend on the proof, I decided to post it
anyway. Finally I can sleep well again ;)
have fun,
chris
On 10/27/2011 03:30 PM, Florian Haftmann wrote:
Indeed, that would be the obvious next step. I have not tried yet but
would not expect too hard difficulties. If this is of general interest I
can try.
Well, if you want to superseed the existing quicksort, you have to
provide the same generality ;-)
Florian
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
(*
Copyright 2011 Christian Sternagel, René Thiemann
This file is part of IsaFoR/CeTA.
IsaFoR/CeTA is free software: you can redistribute it and/or modify it under the
terms of the GNU Lesser General Public License as published by the Free Software
Foundation, either version 3 of the License, or (at your option) any later
version.
IsaFoR/CeTA is distributed in the hope that it will be useful, but WITHOUT ANY
WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A
PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public License along
with IsaFoR/CeTA. If not, see http://www.gnu.org/licenses/.
*)
theory Efficient_Sort
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 :: ('b \Rightarrow 'a) \Rightarrow 'b list \Rightarrow 'b
list list
and ascending :: ('b \Rightarrow 'a) \Rightarrow 'b \Rightarrow ('b
list \Rightarrow 'b list) \Rightarrow 'b list \Rightarrow 'b list list
and descending :: ('b \Rightarrow 'a) \Rightarrow 'b \Rightarrow 'b
list \Rightarrow 'b list \Rightarrow 'b list list
where
sequences key (a#b#xs) = (if key a key b
then descending key b [a] xs
else ascending key b (op # a) xs)
| sequences key xs = [xs]
| ascending key a f (b#bs) = (if \not key a key b
then ascending key b (f \circ op # a) bs
else f [a] # sequences key (b#bs))
| ascending key a f bs = f [a] # sequences key bs
| descending key a as (b#bs) = (if key a key b
then descending key b (a#as) bs
else (a#as) # sequences key (b#bs))
| descending key a as bs = (a#as) # sequences key bs
fun merge :: ('b \Rightarrow 'a) \Rightarrow 'b list \Rightarrow 'b list
\Rightarrow 'b list where
merge key (a#as) (b#bs) = (if key a key b
then b # merge key (a#as) bs
else a # merge key as (b#bs))
| merge key [] bs = bs
| merge key as [] = as
fun merge_pairs :: ('b \Rightarrow 'a) \Rightarrow 'b list list
\Rightarrow 'b list list where
merge_pairs key (a#b#xs) = merge key a b # merge_pairs key xs
| merge_pairs key xs = xs
lemma length_merge[simp]:
length (merge key xs ys) = length xs + length ys
by (induct xs ys rule: merge.induct) simp_all
lemma merge_pairs_length[simp]:
length (merge_pairs key xs) \le length xs
by (induct xs rule: merge_pairs.induct) simp_all
fun merge_all :: ('b \Rightarrow 'a) \Rightarrow 'b list list
\Rightarrow 'b list where
merge_all key [] = []
| merge_all key [x] = x
| merge_all key xs = merge_all key (merge_pairs key xs)
lemma set_merge[simp]:
set (merge key xs ys) = set xs \union set ys
by (induct xs ys rule: merge.induct) auto
lemma sorted_merge[simp]:
assumes sorted (map key xs) and sorted (map key ys)
shows sorted (map key (merge key xs ys))
using assms by (induct xs ys rule: merge.induct) (auto simp: sorted_Cons)
lemma multiset_of_merge[simp]:
multiset_of (merge key xs ys) = multiset_of xs + multiset_of ys
by (induct xs ys rule: merge.induct) (auto simp: ac_simps)
lemma sorted_merge_pairs[simp]:
assumes \forallx\inset xs. sorted (map key x)
shows \forallx\inset (merge_pairs key xs). sorted (map key x)
using assms by (induct xs rule: merge_pairs.induct) simp_all
lemma multiset_of_merge_pairs[simp]:
multiset_of (concat (merge_pairs key xs)) = multiset_of (concat
Re: [isabelle-dev] Merge-Sort Implementation
Hi again,
stability (the third property required by @{thm
properties_for_sort_key}) did actually cause some difficulties ;)
Hence the attached theory has rough parts in some proofs. But since I
spent the most part of the weekend on the proof, I decided to post it
anyway. Finally I can sleep well again ;)
have fun,
chris
On 10/27/2011 03:30 PM, Florian Haftmann wrote:
Indeed, that would be the obvious next step. I have not tried yet but
would not expect too hard difficulties. If this is of general interest I
can try.
Well, if you want to superseed the existing quicksort, you have to
provide the same generality ;-)
Florian
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
(*
Copyright 2011 Christian Sternagel, René Thiemann
This file is part of IsaFoR/CeTA.
IsaFoR/CeTA is free software: you can redistribute it and/or modify it under the
terms of the GNU Lesser General Public License as published by the Free Software
Foundation, either version 3 of the License, or (at your option) any later
version.
IsaFoR/CeTA is distributed in the hope that it will be useful, but WITHOUT ANY
WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A
PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public License along
with IsaFoR/CeTA. If not, see http://www.gnu.org/licenses/.
*)
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 :: ('b \Rightarrow 'a) \Rightarrow 'b list \Rightarrow 'b
list list
and ascending :: ('b \Rightarrow 'a) \Rightarrow 'b \Rightarrow ('b
list \Rightarrow 'b list) \Rightarrow 'b list \Rightarrow 'b list list
and descending :: ('b \Rightarrow 'a) \Rightarrow 'b \Rightarrow 'b
list \Rightarrow 'b list \Rightarrow 'b list list
where
sequences key (a#b#xs) = (if key a key b
then descending key b [a] xs
else ascending key b (op # a) xs)
| sequences key xs = [xs]
| ascending key a f (b#bs) = (if \not key a key b
then ascending key b (f \circ op # a) bs
else f [a] # sequences key (b#bs))
| ascending key a f bs = f [a] # sequences key bs
| descending key a as (b#bs) = (if key a key b
then descending key b (a#as) bs
else (a#as) # sequences key (b#bs))
| descending key a as bs = (a#as) # sequences key bs
fun merge :: ('b \Rightarrow 'a) \Rightarrow 'b list \Rightarrow 'b list
\Rightarrow 'b list where
merge key (a#as) (b#bs) = (if key a key b
then b # merge key (a#as) bs
else a # merge key as (b#bs))
| merge key [] bs = bs
| merge key as [] = as
fun merge_pairs :: ('b \Rightarrow 'a) \Rightarrow 'b list list
\Rightarrow 'b list list where
merge_pairs key (a#b#xs) = merge key a b # merge_pairs key xs
| merge_pairs key xs = xs
lemma length_merge[simp]:
length (merge key xs ys) = length xs + length ys
by (induct xs ys rule: merge.induct) simp_all
lemma merge_pairs_length[simp]:
length (merge_pairs key xs) \le length xs
by (induct xs rule: merge_pairs.induct) simp_all
fun merge_all :: ('b \Rightarrow 'a) \Rightarrow 'b list list
\Rightarrow 'b list where
merge_all key [] = []
| merge_all key [x] = x
| merge_all key xs = merge_all key (merge_pairs key xs)
lemma set_merge[simp]:
set (merge key xs ys) = set xs \union set ys
by (induct xs ys rule: merge.induct) auto
lemma sorted_merge[simp]:
assumes sorted (map key xs) and sorted (map key ys)
shows sorted (map key (merge key xs ys))
using assms by (induct xs ys rule: merge.induct) (auto simp: sorted_Cons)
lemma multiset_of_merge[simp]:
multiset_of (merge key xs ys) = multiset_of xs + multiset_of ys
by (induct xs ys rule: merge.induct) (auto simp: ac_simps)
lemma sorted_merge_pairs[simp]:
assumes \forallx\inset xs. sorted (map key x)
shows \forallx\inset (merge_pairs key xs). sorted (map key x)
using assms by (induct xs rule: merge_pairs.induct) simp_all
lemma multiset_of_merge_pairs[simp]:
multiset_of (concat (merge_pairs key xs)) = multiset_of (concat xs)
by (induct xs rule: merge_pairs.induct) (auto simp: ac_simps)
lemma sorted_merge_all:
assumes \forallx\inset xs. sorted (map key x)
shows sorted (map key (merge_all key xs))
using assms by (induct xs rule: merge_all.induct) simp_all
lemma multiset_of_merge_all[simp]:
multiset_of (merge_all key xs) = multiset_of (concat xs)
by (induct xs rule: merge_all.induct) (auto simp: ac_simps)
lemma
shows sorted_sequences: \forallx\inset (sequences key xs). sorted (map
key x)
and \lbrakk\forallx\inset (f []). key x \le key a; sorted (map key
(f [])); \forallxs ys. f (xs@ys) = f xs @ ys;
\forallx. f [x] = f []
[isabelle-dev] Merge-Sort Implementation
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
Re: [isabelle-dev] Merge-Sort Implementation
Hi Christian, 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 interesting to read that comment. The exiting quicksort implementation in HOL is indeed taken from Isabelle's ML library. Don't know what the ancient motivation for quicksort has been (maybe others can comment on this). A critical question: according to the comment, this should easily generalize to a stable sort_key implementation (as also the current quicksort does). Have you undertaken this? All the best, Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Merge-Sort Implementation
On Thu, 27 Oct 2011, Florian Haftmann wrote: The exiting quicksort implementation in HOL is indeed taken from Isabelle's ML library. Don't know what the ancient motivation for quicksort has been (maybe others can comment on this). In ancient times, the Isabelle/ML library had a really slow insertion sort. I replaced that by quicksort according to the discussion of sorting algorithms in Larry's ML for the working programmer (1st edition), when I was a young student. Later the implementation was slightly tuned in conjunction with a lot of profiling on the real applications in the system -- the most critical one being normalization of sorts, which often happens in the inference kernel. In recent years, mergesort definitely gained more popularity than quicksort in general public. Norbert Schirmer was the first to look at this again in ML, but he did not find a significant difference to the existing Isabelle/ML implementation. I've occasionally reconsidered the question myself, but there was never the critical mass to make a change to this important detail of the trusted code base. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Merge-Sort Implementation
If my memory is correct, quicksort was the clear winner in the performance tests that I undertook for my book. Larry On 27 Oct 2011, at 13:50, Florian Haftmann wrote: interesting to read that comment. The exiting quicksort implementation in HOL is indeed taken from Isabelle's ML library. Don't know what the ancient motivation for quicksort has been (maybe others can comment on this). ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Merge-Sort Implementation
On Thu, 27 Oct 2011, Lawrence Paulson wrote: If my memory is correct, quicksort was the clear winner in the performance tests that I undertook for my book. I can confirm it for some later measurements of the refined implementation -- data from 2005..2007, IIRC. There are some anecdotes about other tips from the book, such as the floating-point based random generator. This made its way into Moscow ML, from there into Metis, from there back into the Metis version of Isabelle. Here it caused huge performance issues, especially in parallel Poly/ML. Later David Matthews improved that significantly, and the random generator for Metis was replaced by an old word-based version according to Knuth. Nonetheless, we still have the real-based Library.random from ML for the working programmer, because without it quickcheck performs really bad. See also http://dilbert.com/dyn/str_strip/0//000/00/0/2000/300/2318/2318.strip.gif Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Merge-Sort Implementation
On 10/27/2011 04:38 PM, Florian Haftmann wrote: Nonetheless, we still have the real-based Library.random from ML for the working programmer, because without it quickcheck performs really bad. AFAIR this has only been the case for the ancient SML quickcheck, whereas my quickcheck implementation comes with a random generator in HOL based on a cousin in Haskell. If this is true, we could throw away Library.random. Maybe Lukas can comment on this. What Florian mentioned is correct. A closer code inspection tells me: Matrix/Compute_Oracle/am_sml.ML still uses it to get a unique identifier, probably this can be replaced by a more standard serial_string () Slegdehammer uses it to randomly announce information from Geoff Sutcliffe to our users. Mutabelle has another copy of a Random engine for some random-choice function. It is seems feasible to get rid of the Random engine if one can replace these occurrences by something else appropriate. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
