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)"
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
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
You should be able to use an instantiated version as a simp rule, as in:
apply (simp only: foo [where 'a=nat])
This archive was generated by a fusion of
Pipermail (Mailman edition) and