If you look at the file Pure/envir.ML, you will find the definition of
environments (which has separate components for the two assignments) as well as
primitives that you should use to apply an environment to a term. If you only
look at assignments to variables (as opposed to type variables), you won't see
the effect of the type variable assignments.
Larry
On 19 Nov 2010, at 13:02, Michael Chan wrote:
> On 19/11/10 12:28, Lawrence Paulson wrote:
>> Looking at this again, I'm not certain there is a bug. You are displaying
>> the variable assignments, but are you first applying the type variable
>> assignments? Both must be used in order to instantiate the object term.
>
> Please bear with me -- I'm not sure about the type variable assignments part
> of your response. Doesn't the unifier unify both types and terms? If so, why
> are type variable assignments needed in order to instantiate the object term?
>
> I'm calling Unify.matchers on the pattern and the lemma, so I suspect I might
> not be applying the type variable assignments. How can they be obtained? And
> when you said applying the assignments, did you mean giving the unifier the
> assignments?
>
> Here's a snippet of my code:
>
> ML {*
>
> val trm1 = term_of @{cpat "(?f::?'a=>?'b) ?stuff = ?v"};
> val trm2 = Thm.prop_of @{thm lem};
>
> val mtch_seq = let
> val init = Envir.empty 0
> val ctxt = @{context}
> val (Const ("Trueprop",_) $ trm2) = Thm.prop_of (ProofContext.get_thm ctxt
> "lem")
> in
> Unify.matchers @{theory} [(trm1,trm2)]
> end;
>
> *}
>
> Thanks again
>
> Michael
>
>> Larry
>>
>> On 19 Nov 2010, at 11:11, Michael Chan wrote:
>>
>>> I can confirm that the first lemma's matcher 4. and the second lemma's only
>>> matcher are results of the FO matcher. So, I guess the above question
>>> becomes: how come the FO matcher doesn't instantiate the type variables? Of
>>> course, this is a different question to why the HO matcher doesn't return
>>> matchers to the second lemma.
>>
>>
>
>
> --
> Postal Address: School of Informatics, University of Edinburgh,
> Room 2.05, Informatics Forum, 10 Crichton Street,
> Edinburgh EH8 9AB, UK.
> Telephone Number: +44-131-651-3077,
> Fax Number: +44-131-650-6899,
> Email: m.c...@ed.ac.uk
> Web Page: http://homepages.inf.ed.ac.uk/mchan/
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
