I think I just learned something about MP_TAC, that these are different:
MP_TAC t THEN MESON_TAC[]
MESON_TAC[t]
This is important to me because of the HOL Light tutorial's Mizar-like
definitions
let by labs tac = MAP_EVERY (fun l -> USE_THEN l MP_TAC) labs THEN tac;;
let using ths tac = MAP_EVERY MP_TAC ths THEN tac;;
where the tutorial recommends MESON_TAC[] as a possible "tac". In this case
I've used instead something I imagined was the same: with
let mby labs ths = MAP_EVERY (fun l -> USE_THEN l MP_TAC) labs THEN
(MESON_TAC ths);;
But this example below indicates they're not the same.
needs "Multivariate/vectors.ml";;
g `!u v w:real^2.
~(v = w) /\ independent {v,w} ==> ?s t. s % v + t % w = u`;;
e(REPEAT STRIP_TAC);;
e(SUBGOAL_THEN `rank (transp (vector [v; w]):real^2^2) = dimindex (:2)
==> ?x:real^2. transp (vector [v; w]) ** x = u` ASSUME_TAC);;
e(MESON_TAC[MATRIX_FULL_LINEAR_EQUATIONS]);;
(* That worked! But this times out: *)
g `!u v w:real^2.
~(v = w) /\ independent {v,w} ==> ?s t. s % v + t % w = u`;;
e(REPEAT STRIP_TAC);;
e(SUBGOAL_THEN `rank (transp (vector [v; w]):real^2^2) = dimindex (:2)
==> ?x:real^2. transp (vector [v; w]) ** x = u` ASSUME_TAC);;
e(MP_TAC MATRIX_FULL_LINEAR_EQUATIONS THEN MESON_TAC[]);;
(* --
Best,
Bill *)
------------------------------------------------------------------------------
Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS,
MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current
with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft
MVPs and experts. ON SALE this month only -- learn more at:
http://p.sf.net/sfu/learnnow-d2d
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
