Re: [isabelle] simp and type variables
Dear Brian and Tobias,
Thank you for your very prompt reply. Your suggestion of using where
was a little surprising to me, since where is specifically not context
sensitive in the midst of goal proving, for (universally quantified)
term variables. (Also, I didn't see in the documentation that where
could be used with type variables.) I gather type variables (even
those generated by unification) are treated as "user supplied" free
variables and not universally quantified variables). I know HOL does
not have explicit type quantification, but I have thought of type
variables (especially those generated from unification) as if they were
universally quantified at the top most level, which would indicate that
they were out of scope for where. Anyway, your reply has enlightened me
and saved my lots of grief. Again I thank you both.
Brian Huffman wrote:
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