Re: [isabelle] New AFP entries, List-Infinite

Dear David,

my point was not to criticize your work. I merely wanted to point out that at present, any user has to buy into one of the three versions. Switching from one to the other might be difficult because of the small differences, in particular different names for constants and lemmas and types of constants. Like you, I have tried to stay close to HOL/List for Coinductive, too. In fact, many definitions of yours and mine are equivalent. So I wondered whether there is any interest in combining the formalisations into one - and how that would be done.


David Trachtenherz schrieb:
> An additional remark on infinite lists in my entry: I designed them very
> pragmatically; the definitions and lemmas are named similar to those for
> finite lists and also work similar, also w. r. t. lemmas added to the
> simpset. Some lemmas work even simpler because infinite lists naturally
> don't need assumptions of the form "i < length xs" or "length xs =
> length ys". So I do hope that everybody used to work with finite lists
> will also be comfortable with this formalization of infinite lists.
> David

Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.