Email Gateway (Aug 22 2022 at 12:35): Email Gateway (Aug 22 2022 at 12:35):From: Dmitriy Traytel <traytel@inf.ethz.ch>
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
Email Gateway (Aug 22 2022 at 12:36):From: Richard Molitor via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi Dmitriy,
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).
Email Gateway (Aug 22 2022 at 12:36):From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Richard,
On 12 Feb 2016, at 06:58, Richard Molitor <gattschardo@googlemail.com> wrote:
Hi Dmitriy,
On Thu, 11 Feb 2016, Dmitriy Traytel wrote:
On 05 Feb 2016, at 14:59, Joachim Breitner <breitner@kit.edu> wrote:
Concrete proposal for your consideration: For product data typesdatatype 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 (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
Email Gateway (Aug 22 2022 at 12:38):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 22 2022 at 12:49):From: Joachim Breitner <breitner@kit.edu>
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
up as measure functions:
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
lemma measure_t[measure_function]:
"is_measure f ⟹ is_measure (λ t. case t of C t₁ ... tₙ ⇒ (t₁,...,tₙ)"..
Greetings,
Joachim
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC