[isabelle] Make all selectors measure_functions?

[Dmitriy Traytel]

Hi Joachim,

that indeed would be a nice feature, not only for product types but for all non-recursive arguments of a (co)datatype constructor. Similarly for records.

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.

Cheers,
Dmitriy

Dear Isabelle list,
I was surprised to find that one function definition involving a type
(t1 × t2) would work, but the equivalent function definition involving
a custom data type isomorphic to (t1 × t2) (i.e. one constructor with
two fields) would not work. See
http://stackoverflow.com/questions/35225110/termination-checking-for-product-types
for the example.
The reason is, of course, that the selectors of the pair type are set
lemma measure_fst[measure_function]: "is_measure f ⟹ is_measure (λp. f (fst p))"
by (rule is_measure_trivial)
lemma measure_snd[measure_function]: "is_measure f ⟹ is_measure (λp. f (snd p))"
by (rule is_measure_trivial)
and doing something similar for my custom type solves the problem.
But it was still surprising, so I wonder if there is a reason not to
register a similar measure function for product data types by default.
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ₙ)"..
Greetings,
Joachim
--
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

[Richard Molitor via Cl-isabelle-users]

Hi Dmitriy,

Post by Dmitriy Traytel

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 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).

[Dmitriy Traytel]

Hi Richard,

Post by Richard Molitor via Cl-isabelle-users
Hi Dmitriy,

Post by Dmitriy Traytel

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 shot!

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

Post by Richard Molitor via Cl-isabelle-users
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).

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.

Dmitriy

[Makarius]

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).

I've already commented on an earlier version of this material, and you
seem to have improved it further. It generally looks good -- above the
average of various ML experiments that are already in AFP.

Some years ago, the AFP editors did not want to see actual ML tools there,
but de-facto we have that already.


Note that the "auto-magic" maintenance in AFP means that someone changing
certain Isabelle/ML things in Pure or HOL also goes through applications
in AFP and tries to adapt them. This sometimes requires to go over it with
the lawn-mower first, to put it into maintainable form. (Your sources look
quite maintainable already.)


I cannot say anything about the application, i.e. the problem that is
addressed here from a user perspective.


Makarius

[Richard Molitor via Cl-isabelle-users]

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).

I've already commented on an earlier version of this material, and you seem
to have improved it further. It generally looks good -- above the average of
various ML experiments that are already in AFP.

Your comments have been very helpful! The main thing I wanted to finish
before submitting it to the "lawnmower phase" was to finish the move to
use morphisms in all relevant places (which is only half-finished, if I
recall correctly).

Hopefully I will just sit down on a rainy weekend one day and do that,
once that is done you'll hear back from me :)

Some years ago, the AFP editors did not want to see actual ML tools there,
but de-facto we have that already.

That's what I've heard from the colleagues in Karlsruhe as well, so this
was not a concern.

I cannot say anything about the application, i.e. the problem that is
addressed here from a user perspective.

At least in Karlsruhe there seemed to be some use-cases for it, although
some additional hand-holding (i.e. automation) in my code would make it
considerably more user-friendly. That was labelled "future work" though,
maybe for when another bachelor/master student is looking for thesis
material -- or when I become very bored for a longer period of time.

Richard