# Re: [isabelle] simp and type variables

`You could try sledgehammer, which doesn't care about the orientation
``of equations. Of course, it doesn't simplify: you get either a full
``proof or nothing.
`Larry
On 12 Feb 2008, at 16:25, Elsa L Gunter wrote:

Dear Isabelle Users,

`Is there a way in Isabelle to specialize the type variables in a
``theorem to type expressions using the type variables of a goal
``context? And in particular, can this be combined with simp? I have
``a frequently arising situation where I have a set of theorems of the
``form "e1('a) = e2('a, 'b)" and I wish to rewrite using these.
``That is, I have equations where there are more type variables on the
``right than on the left (think "True = \<all> x. x = x"). simp will
``not use the equations as rewrites. As a result I am forced to use
``fairly low level reasoning with ssubst (or at least I seem to be).
``However, often times, I want to use a specialization of my equation
``to "e1(('c,'d)tyc) = e2(('c,'d)tyc, 'c)". This equation would be
``accepted by simp. But the only way I know of creating this lemma is
``by using "lemma" and proving it separately. But I have many
``different such specializations, each of which will like be used only
``once. This seems to me to be just where you want to use [of ... ]
``or the like to inline the specialization into an ongoing proof.
``Since I can see no way of doing so, I thought I should ask if I am
``missing something.
`---Elsa

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