Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Theorems and types

Email Gateway (Aug 22 2022 at 11:50):

From: Mohammad Abdul Aziz <mohammad.abdulaziz8@gmail.com>
Dear all,
I have two questions regarding types of variables in Isabelle theorems:
1) I understand that a way to print a theorem T in the library is by
printing thm M in the editor. Is there a way to ask for printing the types
of the bound variable?
2) I understand that to instantiate a quantified variable x in a theorem T
with a term t, one uses T[of "t"]. Is there an equivalent way to
instantiate polymorphic type variables in a theorem?

Best,
Mohammad

Email Gateway (Aug 22 2022 at 11:50):

From: Lars Noschinski <noschinl@in.tum.de>
On 09.11.2015 17:59, Mohammad Abdul Aziz wrote:

Dear all,
I have two questions regarding types of variables in Isabelle theorems:
1) I understand that a way to print a theorem T in the library is by
printing thm M in the editor. Is there a way to ask for printing the types
of the bound variable?

Use print_statement.

2) I understand that to instantiate a quantified variable x in a theorem T
with a term t, one uses T[of "t"]. Is there an equivalent way to
instantiate polymorphic type variables in a theorem?

You can use [where 'a=T] or [of x for x :: 'a]. However, this should be
very seldom necessary.

-- Lars

Email Gateway (Aug 22 2022 at 11:54):

From: Makarius <makarius@sketis.net>
If you just want to know the types, and not print them explicitly, you can
use the C-hover idom of the prover IDE to get a popup with the type
information.

This works slightly asymmetrically for input and output of terms, theorems
etc.

Here is another possibility to get lots of type information printed
(usually way too much):

declare [[show_types]]
thm allI
print_statement allI

Makarius

Last updated: Apr 16 2024 at 12:28 UTC