Hello,
I have a set of hypotheses involving the words library that I would
like to prove automatically. My first attempt at this was to ask HOL
to prove them against the entirety of wordsTheory, using:
> prove(hypothesis, METIS_TAC(map snd (DB.theorems "words")));
While this appeared to work at first, it seems that it is able to
'prove' obviously-incorrect hypotheses, for example:
> load "wordsTheory"; open wordsTheory;
> show_assums := true;
> prove(``F``, METIS_TAC(map snd (DB.theorems "words")));
[%%genvar%%8939 = @m. dimindex (:'XXfolXX_40996) = SUC m,
%%genvar%%8939 = @m. dimindex (:2) = SUC m,
%%genvar%%8939 = @m. dimindex (:unit) = SUC m] |- F:
thm
Is this more likely to indicate an inconsistency in wordsTheory, or me
doing something wrong? I've only started using HOL recently, so it's
probably the latter ;)
Thanks in advance,
Tom Nixon
------------------------------------------------------------------------------
Simplify data backup and recovery for your virtual environment with vRanger.
Installation's a snap, and flexible recovery options mean your data is safe,
secure and there when you need it. Data protection magic?
Nope - It's vRanger. Get your free trial download today.
http://p.sf.net/sfu/quest-sfdev2dev
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
