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

[Michael Chan]

On 19/11/10 14:10, Lawrence Paulson wrote:
> 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.

Thanks. The variable and type variables assignments for matcher 4. (from 
the FO matcher) are

[?f::?'b1 => ?'a1 := g, ?v::?'a1 := 0::nat, ?stuff::?'b1 := a]
[?'a1 := nat, ?'b1 := nat]

so that's what is expected and it's equivalent to matcher 2. (from the 
HO matcher):

[?f::nat => nat := g, ?v::nat := 0::nat, ?stuff::nat := a]
[?'a1 := nat, ?'b1 := nat]

Would you regard the FO matcher to be a redundant duplicate? If so, 
should it be dropped?

Michael

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


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