[isabelle-dev] pull request (HOL-Library/Sublist(_Order))
florian.haftmann at informatik.tu-muenchen.de
Mon Jun 30 20:37:45 CEST 2014
Is there any serious objection against these patches? If not and nobody
else volunteers, I plan to get hands on by Thursday.
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".
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 263 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev