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
