Re: [isabelle] simps_of_case has problems with records



Hi Jasmin and Lars,

Thanks for your input. After Lars' explanations, I found another workaround, namely explicitly listing the relevant split rules using (splits: ...).

Of course, I'd appreciate a better integration of record with the other packages. This would, e.g., allow to pattern-match on records in function definitions, as in

  record foo = foo :: nat
  record bar = foo + bar :: int

  free_constructors foo_ext for foo_ext by (fact foo.cases_scheme foo.ext_inject)+
  free_constructors bar_ext for bar_ext by (meson bar.ext_surjective)(fact bar.ext_inject)

  fun f :: "'a bar_scheme â int" where "f (|foo = x, bar = y, â = z|) = int x + y"

Though, I do not see why the free constructor architecture would have to be extended. An extended extensible record like 'a bar_scheme just abbreviates "'a bar_ext foo_ext" and the functions foo_ext and bar_ext can serve as constructors for foo_ext and bar_ext, respectively. That is, we just have nested types with free constructors. What am I missing?

Unfortunately, the record package is still completely unlocalised. That's probably the bigger hurdle.

Cheers,
Andreas

On 02/06/15 13:43, Jasmin Blanchette wrote:
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.