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



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é

Am 10.10.2014 um 18:22 schrieb Manuel Eberl <eberlm at 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
> 
> 
> 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.