Re: [isabelle] automatic case splitting during simp



On 08/12/2009, at 10:13 AM, Lucas Dixon wrote:
> It would be nice to have some tools that let one derive case statements
> from function definitions and visa-versa. Having the function definition
> style of equations provides nice simp rules which don't expand the case
> statements.

Thomas actually has made up a nice Isar attribute for that: it gives you (from a case statement) the standard simp rules you'd write in a function definition.

I'll see if we can dig this up and release it.

The other way would be to have the function package automatically prove the split rule instead.

Cheers,
Gerwin




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