Is there any serious objection against these patches? If not and nobody else volunteers, I plan to get hands on by Thursday.
Florian
On 30.06.2014 15:59, Christian Sternagel wrote:
> Dear developers,
>
> would somebody be willing to pull in the attached patches into
> HOL/Library? The patches where generated with the help of mercurial's mq
> extension (i.e., the "series" file gives the order of application) and
> each patch can be imported into a repository by
>
> hg import --user "Christian Sternagel" <patch-file>
>
> In the AFP the attached changes do only influence my entry
> Well-Quasi-Orders and (to a tiny amount) Myhill-Nerode, for which I have
> corresponding patches in my local AFP repo.
>
> The intention behind the patches is as follows:
>
> * No built-in reflexivity for list embedding. Which is more standard in
> the literature. Then reflexivity of list embedding depends on the
> reflexivity of the given relation on elements.
>
> * To make this more obvious remove "eq" suffix from "list_hembeq". Plus,
> to obtain a slightly shorter (and as I think, more easy to parse) name,
> rename "list_hembeq" into "list_emb" (ideally this should be "List.emb"
> at some point).
>
> * Added monotonicity lemma for "list_emb" which is needed for inductive
> definitions based on it.
>
> * Weaker assumption for transitivity lemma of "list_emb".
>
> * Added lemma that for a list that is embedded in another one, i.e.,
> "list_emb P xs ys", all its elements are in the given base relation "P"
> with some element of the latter, i.e., "ALL x : set xs. EX y : set ys. P
> x y".
>
> cheers
>
> chris
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
--
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
