# [isabelle] Automatic derivation of specialised theorems

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] Automatic derivation of specialised theorems
*From*: Manuel Eberl <eberlm at in.tum.de>
*Date*: Tue, 18 Feb 2014 15:41:15 +0100
*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

Hallo,
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)
Cheers,
Manuel

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