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



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


On 10/10/14 18:12, Wenda Li wrote:
> 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
>





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