Re: [isabelle] Make all selectors measure_functions?
On Thu, 11 Feb 2016, Dmitriy Traytel wrote:
On 05 Feb 2016, at 14:59, Joachim Breitner <breitner at kit.edu> wrote:
Concrete proposal for your consideration: For product data types
datatype t = C tâ ... tâ
automatically generate the equivalent of
"is_measure f â is_measure (Î t. case t of C tâ ... tâ â (tâ,...,tâ)"..
I guess one non-invasive to implement this would be via a plugin to
the free_constructors abstraction (c.f.
Ctr_Sugar.ctr_sugar_interpretation). Jasmin and me are putting this on
some low-priority feature request list. But if you really want the
functionality (i.e. want to do it by yourself), we would be happy to
give more guidance.
I talked to Joachim yesterday, he said he was not interested at the
moment, but if you want to provide some pointers I would like to give it
A bit of background maybe: I did spend some time implementing an
extension to inductive predicates for Isabelle for my masters thesis
(Joachim was my supervisor). -- What I am trying to say is that I am
somewhat proficient in digging around in Isabelle-style ML-code and
making some sense of what I read, so if you provide me with some
guidance your time wont be wasted :)
 I originally intended to get it into the AFP, but then never pushed
it when I got busy with applying for jobs and other things. The code is
on github though (https://github.com/gattschardo/open-inductive) and I
made it work with Isabelle2015 (and this week Isabelle2016-RC4).
This archive was generated by a fusion of
Pipermail (Mailman edition) and