The theorem n2w_w2n |- !w. n2w (w2n w) = w
cannot be applied in ``n2w (w2n w) = v`` when w and v do not have the same length, which is the case in your goal. For proving things about ``a @@ b``, I would recommend using the latest HOL snapshot. I'm assuming that you're using the latest official release? (The type ``:i2`` has since become ``:2``.) I'm not sure what your original goal is but it may be provable using tools located in wordsLib. For example: - wordsLib.WORD_DECIDE ``!cv:word2. (cv = 0w) ==> (cv @@ cv = 0w:word4)``; > val it = |- !cv. (cv = 0w) ==> (cv @@ cv = 0w) : thm - Q.prove( `!cv:word2. (cv = 0w) ==> (cv @@ cv = 0w:word4)`, SRW_TAC [wordsLib.WORD_EXTRACT_ss] []); > val it = |- !cv. (cv = 0w) ==> (cv @@ cv = 0w) : thm These tools work best when word lengths are ground i.e. when goal's don't contain an ``:'a word`` (``:bool['a]``). Anthony. On 29 Dec 2008, at 08:27, Nikhil Kikkeri wrote: > Hi, > > My current proof obligation looks something like this > > 1 subgoal: >> val it = > w2n (n2w (w2n (cv << dimindex (:i2) !! cv))) = 0 > ------------------------------------ > 0. (1 -- 1) add_in = 0w > 1. (0 -- 0) add_in = 0w > 2. Abbrev (cv = w2w 0w) > : goalstack > > > Now I would assume that doing something like > > e (PURE_REWRITE_TAC[n2w_w2n]); > > should reduce the goal to > > w2n (cv << dimindex (:i2) !! cv) = 0 > --------------------------------------------------- > 0. (1 -- 1) add_in = 0w > 1. (0 -- 0) add_in = 0w > 2. Abbrev (cv = w2w 0w) > : goalstack > > Now if I am seeing things correctly, the rewrite should happen > without a > hitch. However that has not been the case, and that is gating me from > discharging this goal, which looks trivial. > > Thank you in advance, > > Nikhil > > ------------------------------------------------------------------------------ > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
