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




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)"
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.