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

[Christian Sternagel]

Thanks! I'll take care of the AFP now. -cheers chris

On 07/03/2014 02:41 PM, Florian Haftmann wrote:
> Hi Christian,
>
> see now
>
> 	http://isabelle.in.tum.de/repos/isabelle/rev/b69a1272cb04
>
> Cheers,
> 	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
>>
>