# Re: [isabelle] simp and type variables

Quoting Elsa L Gunter <egunter at cs.uiuc.edu>:

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?

`The "of" theorem attribute can only instantiate schematic term
``variables. But the "where" attribute can be used to instantiate either
``type variables or term variables. For example:
`
lemma foo: "True = (ALL x. x = x)"
by simp

`If you type "thm foo" with the "show types" option enabled, you'll see
``that there is a schematic type variable in this theorem:
`True = (ALL x::?'a. x = x)

`Now, if you type "thm foo [where 'a=nat]" you will get the
``instantiated version:
`True = (ALL x::nat. x = x)

`You can also instantiate a schematic type variable with a specific
``free type variable (which may be mentioned in your proof context). For
``example, "thm foo [where'a='b]" gives "True = (ALL x::'b. x = x)"
``(notice that 'b is fixed, not a schematic variable, since it lacks a
``question mark)
`
You should be able to use an instantiated version as a simp rule, as in:
apply (simp only: foo [where 'a=nat])
- Brian

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