Email Gateway (Aug 18 2022 at 11:21): Email Gateway (Aug 18 2022 at 11:21):From: Elsa L Gunter <egunter@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? I have a frequently
arising situation where I have a set of theorems of the form "e1('a) =
e2('a, 'b)" and I wish to rewrite using these. That is, I have
equations where there are more type variables on the right than on the
left (think "True = \<all> x. x = x"). simp will not use the equations
as rewrites. As a result I am forced to use fairly low level reasoning
with ssubst (or at least I seem to be). However, often times, I want to
use a specialization of my equation to "e1(('c,'d)tyc) = e2(('c,'d)tyc,
'c)". This equation would be accepted by simp. But the only way I know
of creating this lemma is by using "lemma" and proving it separately.
But I have many different such specializations, each of which will like
be used only once. This seems to me to be just where you want to use
[of ... ] or the like to inline the specialization into an ongoing
proof. Since I can see no way of doing so, I thought I should ask if I
am missing something.
---Elsa
Email Gateway (Aug 18 2022 at 11:21):From: Lawrence Paulson <lp15@cam.ac.uk>
You could try sledgehammer, which doesn't care about the orientation
of equations. Of course, it doesn't simplify: you get either a full
proof or nothing.
Larry
Email Gateway (Aug 18 2022 at 11:21):From: Brian Huffman <brianh@cs.pdx.edu>
Quoting Elsa L Gunter <egunter@cs.uiuc.edu>:
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])
Email Gateway (Aug 18 2022 at 11:21):From: Tobias Nipkow <nipkow@in.tum.de>
Indeed, a relative of "of", "where", does the job: if your fact is
called th and the type variables are flexible (ie ?'a, not 'a), then
just write th[where 'b = "..."] to instantiate ?'b.
Tobias
Elsa L Gunter schrieb:
Email Gateway (Aug 18 2022 at 11:21):From: Elsa L Gunter <egunter@cs.uiuc.edu>
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:
Last updated: May 03 2024 at 04:19 UTC