# Re: [isabelle] simp and type variables

`Indeed, a relative of "of", "where", does the job: if your fact is
``called th and the type variables are flexible (ie ?'a, not 'a), then
``just write th[where 'b = "..."] to instantiate ?'b.
`
Tobias
Elsa L Gunter schrieb:

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