Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Theoryname.splits: Is this a feature?

Email Gateway (Aug 17 2022 at 13:45):

From: Nicole Rauch <rauch@informatik.uni-kl.de>
Hello all,

recently I painfully discovered that the splitting lemmas that are
generated for a datatype are not only bound to Datatype.splits and
Theoryname.Datatype.splits, but also to Theoryname.splits. It seems
as if the latter is bound to the splitting lemmas of the last
datatype found in the theory called Theoryname. Unfortunately, this
seems to be stronger than the binding to Datatype.splits.
Thus, in case Datatype equals Theoryname, and if the lemma
Datatype.splits is used somewhere in a subsequent theory, and if at a
later stage a new datatype New_Datatype is inserted into Theoryname,
the proofs in the subsequent theory will break due to the fact that
Datatype.splits then in fact refers to Theoryname.splits which is
bound to New_Datatype.splits.

A short example might look like this:

X.thy:

datatype X = ... something ...

Y.thy:

theory Y = X :

lemma xyz "..."
...
apply (simp split: X.splits)
...

If later on X.thy is changed to

datatype X = ... something ...
datatype Z = ... something else ...

the proofs of Y.thy will break because X.splits refers to X.Z.splits,
not to X.X.splits as intended.

Well...

Is this a feature? If so, what would it be good for?

Thanks for any insights!

Nicole

Last updated: May 03 2024 at 12:27 UTC