Email Gateway (Aug 18 2022 at 12:08): Email Gateway (Aug 18 2022 at 12:08):From: Erich Kummerfeld <ekummerfeld@gmail.com>
Hi,
I'm having a problem of types, I believe, and their interaction with
placeholder functions. I've been able to reduce it to this example:
consts
P :: "'a => bool"
theorem "P x ==> P (?x21 x)"
If I apply assumption here I get an empty result sequence error. It works
just fine if P is defined as a function from a bool to a bool or a nat to a
bool, as I'd expect it to. I'm not sure why it doesn't work for type 'a
also. Is there another way I can solve proofs of this form if I'm defining
P the way that I am?
Thanks in advance,
Erich Kummerfeld
Email Gateway (Aug 18 2022 at 12:08):From: Tobias Nipkow <nipkow@in.tum.de>
Your P is polymorphic. Hence two occurrences of P need not have the same
type. Hence Isabelle gave your two P's the most general type, ie one is
of type 'a => bool and the other of type 'b => bool.
Many problems are typing problems. General advice: always switch on
Isabelle -> Settings -> Show types
when you have a problem.
You can fix it with explicit annotations, eg
theorem "P(x::'a) ==> P(?x21 x :: 'a)"
Tobias
PS I don't recommend theorems with unknowns in them, but that's a matter
of taste.
Erich Kummerfeld wrote:
Email Gateway (Aug 18 2022 at 12:09):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Tobias Nipkow wrote:
Part of the problem is also that the types are also fixed. You can also
specify unknown types, thus
"P (x :: 'a) ==> P (?x21 x :: ?'x)" ;
Then also it will work. (Not that there is normally any good reason to
do this)
Jeremy
Last updated: May 03 2024 at 04:19 UTC