Email Gateway (Aug 19 2022 at 16:18): 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
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
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
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: Nov 21 2024 at 12:39 UTC