Re: [isabelle] Make all selectors measure_functions?

Hi Richard,

> On 12 Feb 2016, at 06:58, Richard Molitor <gattschardo at> wrote:
> Hi Dmitriy,
> On Thu, 11 Feb 2016, Dmitriy Traytel wrote:
>>> On 05 Feb 2016, at 14:59, Joachim Breitner <breitner at> 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!

Great to hear. Iâll provide some pointers in a separate mail (sent a bit later today) off this list.

> 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 ( and I
> made it work with Isabelle2015 (and this week Isabelle2016-RC4).

Yes, Iâve came across your nice work at some point (I donât remember the occasion). It certainly belongs into the AFP.

Actually, putting the thing into the AFP will reduce your work in the long term. Basically, youâll almost never again will have to make it work with IsabelleXXX. This is particularly true for Isabelle/ML code which changes more rapidly than well-established concepts from HOL-Main.


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