[isabelle] Automatic derivation of specialised theorems


I currently have the following situation: I have a number of theorems in
some typeclass that contain terms such as “x div foo x” (where foo is a
function constant and x is a free variable)

For particular instantiations of this typeclass, “x div foo x” often has
a much easier form. Say, for instance, I have a theorem “(?x::nat) div
foo ?x = ?x” I would therefore like to do the following for any theorem
that contains “?x div foo ?x” as a subterm:

1. replace every occurrence of “x div foo x” in the theorem with “?x”
(i.e. just replace lhs of equation with rhs everywhere)
2. perform some simplification, possibly with a restricted simpset
3. register the new theorem under the name of the old one, plus the
suffix “_nat”

Are there any existing mechanisms for something like this? If not, how
should I proceed? For instance, how do I get a list of all theorems
containing such a pattern? (All of this will be done only in the theory
where the type class instance was first derived, so this is a very
“local” operation, the number of theorems affected is not very large)


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