Re: [isabelle] Datatype definition can be slow

Somebody once voiced the possibility of making it possible to switch off
the simplification lemmas (e.g. for constructor distinctness, of which
there are quadratically many) and replace them by a simproc that proves
them ad-hoc whenever one of them is needed.
This would make applying the theorems slightly more expensive, but
eliminate the need to prove all of them beforehand.

Not sure if this becomes enough of a problem to be worth it or if the
existing construction is fast enough for any reasonably-sized datatype.

Maybe the following approach would be nice:

Instead of generating pairwise inequalities, a function constructor_num is generated with the simp-rules "constructor_num A00 = 1" "constructor_num A01 = 2" "constructor_num A03 = 3" etc. (Where "constructor_num" is an overloaded function like size.)

Then we additionally add the simp-rule "constructor_num x != constructor_num y ==> x != y". (For each datatype one instances because the generic one would loop. Or alternatively, have a no-assumptions type class for which that rule holds is added to the simplifier.)

Now I believe that this would be enough to decide inequalities the same way as simp can do now. (Haven't tested this.)

To avoid unnecessary simplifications, maybe add a cong-rule that forbids simplifications in the argument of constructor_num.

(Sorry if this is obvious and anyway what you had in mind for the inner workings of the simproc.)

Best wishes,

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