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



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

--
"Never in the field of software development was so much owed by so
many to so few lines of code" -- Martin Fowler about JUnit






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