Hi Lu,
Both of your goals can be solved with:
SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED_CLAUSES]
See HOL/examples/machine-code/hoare-triple/addressScript.sml.
ALIGNED is another useful theorem about alignment, e.g.
> REWRITE_CONV [ALIGNED] ``ALIGNED (a + 12w)``;
val it =
|- ALIGNED (a + 12w) <=> ALIGNED a
: thm
> REWRITE_CONV [ALIGNED] ``ALIGNED (a + 11w)``;
val it =
|- ALIGNED (a + 11w) <=> ALIGNED (a + 3w)
: thm
> REWRITE_CONV [ALIGNED] ``ALIGNED (a - 11w)``;
val it =
|- ALIGNED (a - 11w) <=> ALIGNED (a - 3w)
: thm
Magnus
On 9 April 2010 04:20, Lu Zhao <luz...@cs.utah.edu> wrote:
> Hi,
>
> How can I proceed to prove this seemingly very simple expression? I'm
> not familiar with word proofs.
>
> ``(0x3w && (x :bool[32]) + 0x4w = 0x0w) <=> (0x3w && x = 0x0w)``
>
> or more general,
>
> ``(0x3w && (x :bool[32]) + y * 0x4w = 0x0w) <=> (0x3w && x = 0x0w)``
>
> Any suggestion is appreciated.
>
> Thanks.
> Lu
>
>
> ------------------------------------------------------------------------------
> Download Intel® Parallel Studio Eval
> Try the new software tools for yourself. Speed compiling, find bugs
> proactively, and fine-tune applications for parallel performance.
> See why Intel Parallel Studio got high marks during beta.
> http://p.sf.net/sfu/intel-sw-dev
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
Download Intel® Parallel Studio Eval
Try the new software tools for yourself. Speed compiling, find bugs
proactively, and fine-tune applications for parallel performance.
See why Intel Parallel Studio got high marks during beta.
http://p.sf.net/sfu/intel-sw-dev
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
