Re: [isabelle] Code generation for predicates with variable number of premises
- To: Mark Wassell <mpwassell at gmail.com>, Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>
- Subject: Re: [isabelle] Code generation for predicates with variable number of premises
- From: Lukas Bulwahn <lukas.bulwahn at gmail.com>
- Date: Thu, 1 Dec 2016 13:45:11 +0100
- In-reply-to: <CAKXUXMzz+aXOKRKXvVjST1TEfObKzPQZ0QNAuYdAfrwM=B5_4A@mail.gmail.com>
- References: <CAK0o7caJGdiF2t8OtCrfvfnXyhjnpqxj_cTz8MVqDbTTRnC2PA@mail.gmail.com> <firstname.lastname@example.org> <CAK0o7cZXe8P5CVXtNuVSFA+Mqp+xhckRyZLwBHDbkWX6AqYxrw@mail.gmail.com> <CAKXUXMzz+aXOKRKXvVjST1TEfObKzPQZ0QNAuYdAfrwM=B5_4A@mail.gmail.com>
> If you are wondering why this predicate compiler setup for list_all2
> in is not provided by the default HOL-Main setup (what also crossed my
> mind going though the example), this is due to historic circumstances:
> I developed the predicate compiler in 2009-2012; the new datatype
> package, which defines list_all2, was developed since 2012. Until now,
> no one has considered to set up the predicate compiler for the
> constants defined by the new datatype package.
Tobias pointed out to me that list_all2 actually existed long before
the new datatype package, which just happens to define the constant
now automatically as it is the natural relator for lists.
As I found out by a more precise look at the history, Tobias defined
the list_all2 constant already in January 2000, i.e., in changeset
8115:c802042066e8 . So the reason that there is no setup for
list_all2 is probably due to the fact that I did not come across an
example for the predicate compiler that uses list_all2 in 2009-2012;
even though Andreas Lochbihler and I used the predicate compiler
heavily for making the Jinja with threads semantics executable.
I have put it on my todo list to add the setup for list_all2 for the
predicate compiler in HOL-Main; it will happen eventually.
This archive was generated by a fusion of
Pipermail (Mailman edition) and