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

`
`