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

On Fri, 10 Oct 2014, Wenda Li wrote:

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.

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

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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.