Re: [isabelle] Automatic derivation of specialised theorems

> 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”

1 + 2 sounds like the "unfolded" and "simplified" attributes.

For 3, I do not know any "clean" solution ;)

-- Peter

> 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.