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



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.