[isabelle-dev] pull request (HOL-Library/Sublist(_Order))

[Florian Haftmann]

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-dev at 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140630/479681fb/attachment.sig>