[isabelle] Non-idempotence of datatype constructors



This is one for our datatype experts:

I just noticed that theorems like

Cons x xs ≠ xs

are not automatically provided by the datatype package although they
should clearly hold for any datatype. To be more precise, I am talking
about theorems of the form

C x1 … xn ≠ x1
…
C x1 … xn ≠ xn

for any n-ary datatype constructor C (and of course also the flipped
variant).

I'm not sure how useful something like this is in practice and it's
fairly easy to prove these by hand when needed. I just ran into a
situation where I had an assumption of the form "C a b ≠ b" and was
surprised that the simplifier didn't take care of it automatically.

I realise that the datatype package already provides an absurd number of
theorems and one should be careful to blow it up even more, but seeing
as the number of theorems to be generated is linear in the number of
constructors and they're probably very easy to prove, one could consider
it. Or perhaps at least as an optional plugin or standalone tool.

Manuel






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