Re: [isabelle] simps_of_case has problems with records



Hi Lars, Andreas,

Lars wrote:

> The problem is that "#splits o Ctr_Sugar.ctr_sugar_of ctxt" returns
> Drule.dummy_thm for records, which has not the expected format for a
> split rule.

This immediately points to a workaround for Andreas:

    free_constructors foo_ext for foo_ext
      by (erule foo.cases_scheme) (rule foo.ext_inject)

will update the âCtr_Sugarâ entry for your record type so that it works with âsimps_of_caseâ.

This of course raises the question of whether we can/should integrate records better with the emerging âfree constructorâ architecture. This is mostly an engineering or design issue. Records and datatypes have some obvious conceptual overlap: A plain (non-extended) record is like a nonrecursive single-constructor datatype. Also, for extended records, there is no single constant that acts as a constructor, so the âfree constructorâ architecture would have to be extended to cope with that. Hence, right now we do the minimum automatically and let users invoke âfree_constructorsâ if they want to go further. If this is too much of an annoyance, we could at least derive the split rule automatically from âfoo.cases_scheme".

Jasmin





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