Re: [isabelle] Make all selectors measure_functions?



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


> On 05 Feb 2016, at 14:59, Joachim Breitner <breitner at kit.edu> wrote:
> 
> 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
> 
> -- 
> Dipl.-Math. Dipl.-Inform. Joachim Breitner
> Wissenschaftlicher Mitarbeiter
> http://pp.ipd.kit.edu/~breitner
> 





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