[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
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â)"..


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

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

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