Re: [isabelle] Make all selectors measure_functions?



Hi Dmitriy,

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

   lemma measure_t[measure_function]:
     "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 shot!

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

Best regards
Richard

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