Indeed I find the code peculiar, in that it delivers the higher-order matchers
followed by the first-order ones. But these are different things. And I imagine
there is often redundancy.
Larry
On 19 Nov 2010, at 15:50, Michael Chan wrote:
> 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.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.
>>>
>>
>>
>
>
> --
> 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
