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
