[isabelle-dev] Fwd: minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist
lp15 at cam.ac.uk
Wed Nov 18 16:26:58 CET 2015
These suggestions are worth a discussion. Should we go ahead? Would anybody like to apply this patch and test that everything still works?
> Begin forwarded message:
> From: Peter Gammie <peteg42 at gmail.com>
> Date: 15 November 2015 at 15:15:48 GMT
> To: isabelle-dev at mailbroy.informatik.tu-muenchen.de
> Subject: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist
> Can someone please apply the attached patch to Isabelle for me?
> It does three things:
> - generalises Imperative_Quicksort to work on linearly-ordered, heap-representable types, and not just nat
> - renames Sublist to List_Sublist to avoid clashing with HOL/Library/Sublist
> - mildly weakens the assumptions of lemma subarray_append in theory Subarray
> The first may require existing theories to add type annotations. If this is a concern then perhaps the right thing to do is introduce new names for the polymorphic operations and preserve the existing ones, but I think that is overkill.
> The second may also break existing theories but I do not know how to otherwise get around having two theories with the same name.
More information about the isabelle-dev