Theory: bword_arith

Parents

• bword_num

Types

Constants

• ACARRY  :num -> bool word -> bool word -> bool -> bool
• ICARRY  :num -> bool word -> bool word -> bool -> bool

Definitions

ACARRY_DEF

|- (!w1 w2 cin. ACARRY 0 w1 w2 cin = cin) /\
   !n w1 w2 cin.
     ACARRY (SUC n) w1 w2 cin =
     VB ((BV (BIT n w1) + BV (BIT n w2) + BV (ACARRY n w1 w2 cin)) DIV 2)

ICARRY_DEF

|- (!w1 w2 cin. ICARRY 0 w1 w2 cin = cin) /\
   !n w1 w2 cin.
     ICARRY (SUC n) w1 w2 cin =
     BIT n w1 /\ BIT n w2 \/ (BIT n w1 \/ BIT n w2) /\ ICARRY n w1 w2 cin

Theorems

ACARRY_ACARRY_WSEG

|- !n (w1::PWORDLEN n) (w2::PWORDLEN n) cin m k1 k2.
     k1 < m /\ k2 < n /\ m + k2 <= n ==>
     (ACARRY k1 (WSEG m k2 w1) (WSEG m k2 w2) (ACARRY k2 w1 w2 cin) =
      ACARRY (k1 + k2) w1 w2 cin)

ACARRY_EQ_ADD_DIV

|- !n (w1::PWORDLEN n) (w2::PWORDLEN n) k.
     k < n ==>
     (BV (ACARRY k w1 w2 cin) =
      (BNVAL (WSEG k 0 w1) + BNVAL (WSEG k 0 w2) + BV cin) DIV 2 ** k)

ACARRY_EQ_ICARRY

|- !n (w1::PWORDLEN n) (w2::PWORDLEN n) cin k.
     k <= n ==> (ACARRY k w1 w2 cin = ICARRY k w1 w2 cin)

ACARRY_MSB

|- !n (w1::PWORDLEN n) (w2::PWORDLEN n) cin.
     ACARRY n w1 w2 cin =
     BIT n (NBWORD (SUC n) (BNVAL w1 + BNVAL w2 + BV cin))

ACARRY_WSEG

|- !n (w1::PWORDLEN n) (w2::PWORDLEN n) cin k m.
     k < m /\ m <= n ==>
     (ACARRY k (WSEG m 0 w1) (WSEG m 0 w2) cin = ACARRY k w1 w2 cin)

ADD_NBWORD_EQ0_SPLIT

|- !n1 n2 (w1::PWORDLEN (n1 + n2)) (w2::PWORDLEN (n1 + n2)) cin.
     (NBWORD (n1 + n2) (BNVAL w1 + BNVAL w2 + BV cin) = NBWORD (n1 + n2) 0) =
     (NBWORD n1
        (BNVAL (WSEG n1 n2 w1) + BNVAL (WSEG n1 n2 w2) +
         BV (ACARRY n2 w1 w2 cin)) =
      NBWORD n1 0) /\
     (NBWORD n2 (BNVAL (WSEG n2 0 w1) + BNVAL (WSEG n2 0 w2) + BV cin) =
      NBWORD n2 0)

ADD_WORD_SPLIT

|- !n1 n2 (w1::PWORDLEN (n1 + n2)) (w2::PWORDLEN (n1 + n2)) cin.
     NBWORD (n1 + n2) (BNVAL w1 + BNVAL w2 + BV cin) =
     WCAT
       (NBWORD n1
          (BNVAL (WSEG n1 n2 w1) + BNVAL (WSEG n1 n2 w2) +
           BV (ACARRY n2 w1 w2 cin)),
        NBWORD n2 (BNVAL (WSEG n2 0 w1) + BNVAL (WSEG n2 0 w2) + BV cin))

ICARRY_WSEG

|- !n (w1::PWORDLEN n) (w2::PWORDLEN n) cin k m.
     k < m /\ m <= n ==>
     (ICARRY k (WSEG m 0 w1) (WSEG m 0 w2) cin = ICARRY k w1 w2 cin)

WSEG_NBWORD_ADD

|- !n (w1::PWORDLEN n) (w2::PWORDLEN n) m k cin.
     m + k <= n ==>
     (WSEG m k (NBWORD n (BNVAL w1 + BNVAL w2 + BV cin)) =
      NBWORD m
        (BNVAL (WSEG m k w1) + BNVAL (WSEG m k w2) + BV (ACARRY k w1 w2 cin)))