Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

[Peter Lammich]

Currently heating my CPU with test-building the patch ...
If everything goes fine, I will push it.

--
  Peter


On Do, 2015-11-19 at 10:46 +0100, Florian Haftmann wrote:
> Hi all,
> 
> >> These suggestions are worth a discussion. Should we go ahead? Would
> anybody like to apply this patch and test that everything still works?
> > 
> > I could do it, if nobody has objections.
> 
> I see no obstacles in going ahead.  What requires some thought is the
> material in ex/ directories is typically not assumed to be used in other
> sessions.  I have no idea wether these examples in Imperative-HOL where
> ever supposed to be used as libraries.
> 
> Cheers,
>   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

Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

[Florian Haftmann]

Hi all,

>> These suggestions are worth a discussion. Should we go ahead? Would
anybody like to apply this patch and test that everything still works?
> 
> I could do it, if nobody has objections.

I see no obstacles in going ahead.  What requires some thought is the
material in ex/ directories is typically not assumed to be used in other
sessions.  I have no idea wether these examples in Imperative-HOL where
ever supposed to be used as libraries.

Cheers,
Florian

-- 

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] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

[Lawrence Paulson]

As I recall, the Library directory get special treatment. But I forget what 
this special treatment consists of. It might make sense to move this particular 
entry to Library.

Larry

> On 19 Nov 2015, at 09:46, Florian Haftmann 
>  wrote:
> 
> Hi all,
> 
>>> These suggestions are worth a discussion. Should we go ahead? Would
> anybody like to apply this patch and test that everything still works?
>> 
>> I could do it, if nobody has objections.
> 
> I see no obstacles in going ahead.  What requires some thought is the
> material in ex/ directories is typically not assumed to be used in other
> sessions.  I have no idea wether these examples in Imperative-HOL where
> ever supposed to be used as libraries.
> 
> Cheers,
>   Florian
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

[Jasmin Blanchette]

> On 18.11.2015, at 16:26, Lawrence Paulson  wrote:
> 
> These suggestions are worth a discussion. Should we go ahead? Would anybody 
> like to apply this patch and test that everything still works?

I could do it, if nobody has objections.

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

[Peter Gammie]

Hi,

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.

thanks,
peter


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

[Peter Gammie]

… and this time with the patch …

> On 15 Nov 2015, at 22:15, Peter Gammie  wrote:
> 
> Hi,
> 
> 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.
> 
> thanks,
> peter



Imperative_HOL.patch
Description: Binary data

-- 
http://peteg.org/

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev