[isabelle] Make all selectors measure_functions?



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

Attachment: signature.asc
Description: This is a digitally signed message part



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