Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Query about instantiating theorems in Isabelle/ML


view this post on Zulip Email Gateway (Aug 19 2022 at 16:18):

From: Wenda Li <wl302@cam.ac.uk>
Dear Isabelle/ML experts,

Suppose I have a lemma:

lemma foo: "(x::int) = y+z ==> x - y = z" sorry

I want to instantiate y to 1. In Isabelle/Isar I can do this easily by
foo[of _ 1] or foo[where y=1]. How can I do such things in Isabelle/ML?

I believe the answer should have something to do with the
Drule.instantiate' method in drule.ML, but I don't know how to use this
method properly in my case.

If variables in foo don't have type restrictions, then the following
would work:

lemma foo1: "x = y+z ==> x - y = z" sorry
ML{*
Drule.instantiate' [SOME @{ctyp "int"}] [NONE,SOME @{cterm "(1::int)"}]
@{thm foo1};
*}

However, with foo,

ML{*
Drule.instantiate' [SOME @{ctyp "int"}] [NONE,SOME @{cterm "(1::int)"}]
@{thm foo};
*}

Isabelle/ML will complain:

exception TYPE raised (line 810 of "drule.ML"):
instantiate': more instantiations than variables in thm
int
1

Many thanks in advance,
Wenda

view this post on Zulip Email Gateway (Aug 19 2022 at 16:18):

From: Manuel Eberl <eberlm@in.tum.de>
Hallo,

the first parameter to instantiate is the type variables to be
instantiated. Lemma foo1 has the free type variable 'a :: plus. Lemma
foo does not have any free type variables. Therefore, there is nothing
you could instantiate with ‘int’.

Just give it the empty list instead of [SOME @{ctyp "int"}].

Cheers,
Manuel

view this post on Zulip Email Gateway (Aug 19 2022 at 16:18):

From: Makarius <makarius@sketis.net>
ML is not Java, so Drule.instantiate' is just a plain function, not a
"method". (The inventors of OO would complain fiercly about this abuse of
their specific terminology, but this is hardly relevant today.)

To find out how things in Isabelle/ML are used, there are various standard
approaches:

* look at the definitions in ML

* try to find relevant bits of documentation in the manuals

* look around how such functions are usually used in existing
applications

Since the situation of instantiation in Isabelle is a bit convoluted, with
many historic layers, here are some more direct hints as well:

* Thm.instantiate is the main operation at the bottom; it is briefly
described in the "implementation" manual. It is the most robust
operation for high-quality tools, but sometimes awkward to use, due to
extra fiddling with type-instantiations.

* Drule.cterm_instantiate is convenient due to its built-in
type-inference. Its name is maybe a bit misleading -- the point is
not to work with certified entities (which is awkward) but to have
type instantiation implicit according to usual Hindley-Milner
discipline.

Makarius


http://stop-ttip.org


view this post on Zulip Email Gateway (Aug 19 2022 at 16:18):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Hi,

my favorite to simulate the "of" of Isar within Isabelle/ML is

Ctr_Sugar_Util.cterm_instantiate_pos : cterm option list -> thm -> thm

where you just have to provide the terms, but not the types.

Cheers,
René


Last updated: Mar 29 2024 at 01:04 UTC