I am trying to apply HO_MATCH_MP_TAC, but it is not successfully matching
the consequent of the theorem to the current goal the way I thought it
would. The example below is not meant to be a provable theorem, just a
simple instance to show this issue.
By the way, HO_PART_MATCH fails for this case as well.
I can certainly force the matching to work by providing explicit
substitutions, such as shown below, but this is both ugly and not robust
for proof maintenance. The explicit substitutions show the original theorem
can match the goal, but the matching substitution is not found by higher
order matching in this case.
What am I not understanding here? Why does higher order matching fail?
Transcript:
---------------------------------------------------------------------
HOL-4 [Kananaskis 11 (stdknl, built Tue May 24 15:32:51 2016)]
For introductory HOL help, type: help "hol";
To exit type <Control>-D
---------------------------------------------------------------------
[extending loadPath with Holmakefile INCLUDES variable]
[In non-standard heap:
/usr/local/hol/cakeml/cakeml-master/candle/set-theory/heap]
> > > > load "bitTheory";
val it = (): unit
> g `BIT (LEAST n. BIT n x) x`;
val it =
Proof manager status: 1 proof.
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):
thm
> e(HO_MATCH_MP_TAC whileTheory.LEAST_ELIM);
OK..
Exception raised at Tactic.HO_MATCH_MP_TAC:
at HolKernel.ho_match_term:
at Term.dest_comb:
not a comb
Exception-
HOL_ERR
{message =
"at HolKernel.ho_match_term:\nat Term.dest_comb:\nnot a comb",
origin_function = "HO_MATCH_MP_TAC", origin_structure = "Tactic"}
raised
> (BETA_RULE o SPECL[``\a. BIT a x``,``\n. BIT n x``])
whileTheory.LEAST_ELIM;
val it =
|- (∃n. BIT n x) ∧ (∀n. (∀m. m < n ⇒ ¬BIT m x) ∧ BIT n x ⇒ BIT n x) ⇒
BIT (LEAST n. BIT n x) x:
thm
> e(HO_MATCH_MP_TAC ((BETA_RULE o SPECL[``\a. BIT a x``,``\n. BIT n x``])
whileTheory.LEAST_ELIM));
OK..
1 subgoal:
val it =
(∃n. BIT n x) ∧ ∀n. (∀m. m < n ⇒ ¬BIT m x) ∧ BIT n x ⇒ BIT n x
:
proof
>
Thanks for your help.
Peter
"In Your majesty ride prosperously
because of truth, humility, and righteousness;
and Your right hand shall teach You awesome things." (Psalm 45:4)
------------------------------------------------------------------------------
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
