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
