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
On 02/06/15 13:43, Jasmin Blanchette wrote:
Hi Lars, Andreas,
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
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".
This archive was generated by a fusion of
Pipermail (Mailman edition) and