Re: [isabelle] Code generation for predicates with variable number of premises



Dear Mark and Lukas,

I did use list_all2 in JinjaThreads a lot, and the setup is already there. It's just not in List.thy, but in ~~/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy.

Andreas

On 01/12/16 13:45, Lukas Bulwahn wrote:
Dear Mark,


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 [1]. 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.

[1] http://isabelle.in.tum.de/repos/isabelle/rev/c802042066e8

Lukas





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