Thanks a lot for your reply! WORD_ARITH_PROVE is exactly what I wanted, and seems to be working well. The reference on http://hol.sourceforge.net/ doesn't list this, hence attempting to use METIS_TAC.
I'm attempting to prove that certain ARM assembly instructions are equivalent, so it mostly boils down to small arithmetic operations. Tom On 23 June 2011 14:32, Anthony Fox <[email protected]> wrote: > 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 >> [email protected] >> 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
