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
