Hi, This appears to be a bug in METIS_TAC. It should fail but it instead returns a legitimate theorem - just one with inconsistent hypotheses. This appears to relate to the fact that METIS_TAC is at heart a first-order prover, which doesn't fit in with the types/theorems in wordsTheory. Joe Hurd may like to take a look at this...
Using METIS_TAC in this way is fairly non-standard -- it's mostly applied to small goals using a few hand-picked theorems. What sort of goals are you trying to prove? You may like to consider using one of the standard procedures in wordsLib or blastLib. If you're trying to prove arithmetic properties then you could try wordsLib.WORD_ARITH_PROVE, e.g. > load "wordsLib"; > wordsLib.WORD_ARITH_PROVE ``(a * (b + c) + b = a * b) = (a * c = -b)`` val it = |- (a * (b + c) + b = a * b) ⇔ (a * c = -b): thm (or as a tactic: CONV_TAC wordsLib.WORD_ARITH_CONV.) Note that WORD_ARITH_PROVE has only just been added to the SourceForge repository. wordsLib.WORD_DECIDE is similar but can't prove the goal above. If you are working with *known* word sizes then blastLib.BBLAST_PROVE (BBLAST_TAC) is a good option, e.g. > blastLib.BBLAST_PROVE ``(31 >< 2) (w2w (x:word30) << 2 + y:word32) = x + (31 >< 2) y``; val it = |- (31 >< 2) (w2w x ≪ 2 + y) = x + (31 >< 2) y: thm However, this isn't so suited to proving things about multiplication (by a non-literal) and division. If these routines don't work then you may have to rely on user guidance or writing custom routines, e.g. using the simplifier and the various tools in wordsLib. The help pages may be helpful there: help "wordsLib"; help "WORD_ARITH_CONV"; Anthony On 23 Jun 2011, at 12:33, Tom N wrote: > 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 > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info ------------------------------------------------------------------------------ All the data continuously generated in your IT infrastructure contains a definitive record of customers, application performance, security threats, fraudulent activity and more. Splunk takes this data and makes sense of it. Business sense. IT sense. Common sense.. http://p.sf.net/sfu/splunk-d2d-c1 _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
