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-...@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
