> On 9 Jun 2016, at 00:15, Ramana Kumar <[email protected]> wrote:
>
> Hi Peter,
>
> I'm not sure I can explain why HO_MATCH_MP_TAC is not powerful enough for
> this kind of match
[snip]
> 1. Incomplete goalstack:
> Initial goal:
>
> BIT (LEAST n. BIT n x) x
>
>
> :
> proofs
> > whileTheory.LEAST_ELIM;
> val it =
> |- ∀Q P. (∃n. P n) ∧ (∀n. (∀m. m < n ⇒ ¬P m) ∧ P n ⇒ Q n) ⇒ Q ($LEAST P):
I don’t know the HOL4 code well enough to confirm this, but I believe that
like HOL Light and ProofPower, its implementation of higher-order matching
is based on Miller and Nipkow’s algorithm for matching linear patterns.
A linear pattern is one where each term appearing in the argument list
of a function variable is (eta-equivalent to) a variable. Here Q has an
argument that is an application, so this pattern isn’t linear and the algorithm
is not guaranteed to work.
If you are interested in the details of the algorithm, see this very nice paper:
@inproceedings{Nipkow93,
author = {Tobias Nipkow},
title = {Functional Unification of Higher-Order Patterns},
booktitle = {Proceedings, Eighth Annual {IEEE} Symposium on Logic in
Computer Science,
19-23 June 1993, Montreal, Canada},
pages = {64--74},
year = {1993},
crossref = {lics93},
}
Regards,
Rob.------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are
consuming the most bandwidth. Provides multi-vendor support for NetFlow,
J-Flow, sFlow and other flows. Make informed decisions using capacity
planning reports. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
