Indeed. As Ramana suggested, you should use DEEP_INTRO_TAC in situations like
this.
Michael
On 9 Jun 2016, at 21:05, Rob Arthan
<r...@lemma-one.com<mailto:r...@lemma-one.com>> wrote:
On 9 Jun 2016, at 00:15, Ramana Kumar
<ramana.ku...@cl.cam.ac.uk<mailto:ramana.ku...@cl.cam.ac.uk>> 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
hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>
https://lists.sourceforge.net/lists/listinfo/hol-info
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
------------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
