Dear Anthony,
Thank you very much for your response. Is it a general case and we can do the
same for all the other theorems like the n2w_DIV or no?
Regards,
--- On Mon, 3/4/13, Anthony Fox <[email protected]> wrote:
Hi Hamed,
Yes, the side-condition
n < dimindex (:α)
is redundant. I’ve updated this theorem accordingly.
To get a theorem with no side-conditions we can introduce a MOD:
wordsTheory.n2w_DIV
|> Q.SPEC `a MOD dimword(:'a)`
|> SIMP_RULE (srw_ss()) [wordsTheory.n2w_mod]
|> GEN_ALL
val it =
|- ∀a n. n2w (a MOD dimword (:α) DIV 2 ** n) = n2w a ⋙ n:
thm
It would also have been possible to get to this theorem using word_lsr_n2w as
the starting point.
Regards,
Anthony
On 4 Mar 2013, at 19:48, hamed nemati <[email protected]> wrote:
> Hello all,
> For Theorems like the following one what is the corresponding theorem if
> the guard conditions do not hold, I mean what the n2w_DIV theorem would like
> if a or n or
> both of them are greater that dimword (:α).
> [n2w_DIV
> ] Theorem
>
> |- ∀a n.
> n < dimindex (:α) ∧ a < dimword (:α) ⇒
>
> (n2w (a DIV 2 ** n) = n2w a ⋙ n)
>
> do we have module to dimword(:'a) of these two numbers? if no what we can
> do in such a case? Thanks in advance.
>
> Regards,
> Hamed Nemati
> ------------------------------------------------------------------------------
> Everyone hates slow websites. So do we.
> Make your web apps faster with AppDynamics
> Download AppDynamics Lite for free today:
> http://p.sf.net/sfu/appdyn_d2d_feb_______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Everyone hates slow websites. So do we.
Make your web apps faster with AppDynamics
Download AppDynamics Lite for free today:
http://p.sf.net/sfu/appdyn_d2d_feb
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
