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
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
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
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
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
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)
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
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
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
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
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.
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
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
13 matches
Mail list logo
