Is the following behavior of Kananaskis-5 correct?
-----------------------------------------------------------------
HOL-4 [Kananaskis 5 (built Fri Nov 28 13:45:15 2008)]
For introductory HOL help, type: help "hol";
-----------------------------------------------------------------
[loading theories and proof tools ************** ]
[closing file "/usr/local/hol/kananaskis-5/tools/end-init-boss.sml"]
- show_types := true;
> val it = () : unit
- val (tmins,tyins) = ho_match_term [] empty_tmset ``\x:'a. y:'b`` ``\x:num.
x + x``;
> val tmins = [{redex = ``(y :num)``, residue = ``(x :num) + x``}] :
{redex : term, residue : term} list
val tyins =
[{redex = ``:'b``, residue = ``:num``},
{redex = ``:'a``, residue = ``:num``}] :
{redex : hol_type, residue : hol_type} list
- subst tmins (inst tyins ``\x:'a. y:'b``);
> val it = ``\(x' :num). (x :num) + x`` : term
- aconv it ``\x:num. x + x``;
> val it = false : bool
-
It seems unreasonable that these two terms should match, since then the
instantiation of the pattern term (as shown above using the results of the
higher order match) does not in fact produce the target term. Isn't that
the point of matching, to arrive at a substitution that makes the pattern
into the target?
Peter
--
"In Your majesty ride prosperously
because of truth, humility, and righteousness;
and Your right hand shall teach You awesome things." (Psalm 45:4)
------------------------------------------------------------------------------
SF.Net email is Sponsored by MIX09, March 18-20, 2009 in Las Vegas, Nevada.
The future of the web can't happen without you. Join us at MIX09 to help
pave the way to the Next Web now. Learn more and register at
http://ad.doubleclick.net/clk;208669438;13503038;i?http://2009.visitmix.com/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
