[isabelle-dev] [isabelle] Higher-order matching against schematic variables

[Michael Chan]

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.Chan at 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.