Dear Lu,
On Thu, 2010-04-08 at 21:20 -0600, Lu Zhao wrote:
> 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
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 +
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.
Thank
