Theory: word_bitop

Parents

• word_base

Types

Constants

• EXISTSABIT  :('a -> bool) -> 'a word -> bool
• FORALLBITS  :('a -> bool) -> 'a word -> bool
• PBITBOP  :('a word -> 'b word -> 'c word) -> bool
• WMAP  :('a -> 'b) -> 'a word -> 'b word
• PBITOP  :('a word -> 'b word) -> bool
• SHL  :bool -> 'a word -> 'a -> 'a # 'a word
• SHR  :bool -> 'a -> 'a word -> 'a word # 'a

Definitions

EXISTSABIT_DEF

|- !P l. EXISTSABIT P (WORD l) = SOME_EL P l

FORALLBITS_DEF

|- !P l. FORALLBITS P (WORD l) = ALL_EL P l

PBITBOP_DEF

|- !op.
     PBITBOP op =
     !n (w1::PWORDLEN n) (w2::PWORDLEN n).
       PWORDLEN n (op w1 w2) /\
       !m k.
         m + k <= n ==> (op (WSEG m k w1) (WSEG m k w2) = WSEG m k (op w1 w2))

PBITOP_DEF

|- !op.
     PBITOP op =
     !n (w::PWORDLEN n).
       PWORDLEN n (op w) /\
       !m k. m + k <= n ==> (op (WSEG m k w) = WSEG m k (op w))

SHL_DEF

|- !f w b.
     SHL f w b =
     (BIT (PRE (WORDLEN w)) w,
      WCAT (WSEG (PRE (WORDLEN w)) 0 w,(if f then WSEG 1 0 w else WORD [b])))

SHR_DEF

|- !f b w.
     SHR f b w =
     (WCAT
        ((if f then WSEG 1 (PRE (WORDLEN w)) w else WORD [b]),
         WSEG (PRE (WORDLEN w)) 1 w),BIT 0 w)

WMAP_DEF

|- !f l. WMAP f (WORD l) = WORD (MAP f l)

Theorems

EXISTSABIT

|- !n (w::PWORDLEN n) P. EXISTSABIT P w = ?k. k < n /\ P (BIT k w)

EXISTSABIT_WCAT

|- !w1 w2 P. EXISTSABIT P (WCAT (w1,w2)) = EXISTSABIT P w1 \/ EXISTSABIT P w2

EXISTSABIT_WSEG

|- !n (w::PWORDLEN n) m k.
     m + k <= n ==> !P. EXISTSABIT P (WSEG m k w) ==> EXISTSABIT P w

FORALLBITS

|- !n (w::PWORDLEN n) P. FORALLBITS P w = !k. k < n ==> P (BIT k w)

FORALLBITS_WCAT

|- !w1 w2 P. FORALLBITS P (WCAT (w1,w2)) = FORALLBITS P w1 /\ FORALLBITS P w2

FORALLBITS_WSEG

|- !n (w::PWORDLEN n) P.
     FORALLBITS P w ==> !m k. m + k <= n ==> FORALLBITS P (WSEG m k w)

NOT_EXISTSABIT

|- !P w. ~EXISTSABIT P w = FORALLBITS ($~ o P) w

NOT_FORALLBITS

|- !P w. ~FORALLBITS P w = EXISTSABIT ($~ o P) w

PBITBOP_EXISTS

|- !f. ?fn. !l1 l2. fn (WORD l1) (WORD l2) = WORD (MAP2 f l1 l2)

PBITBOP_PWORDLEN

|- !(op::PBITBOP) n (w1::PWORDLEN n) (w2::PWORDLEN n). PWORDLEN n (op w1 w2)

PBITBOP_WSEG

|- !(op::PBITBOP) n (w1::PWORDLEN n) (w2::PWORDLEN n) m k.
     m + k <= n ==> (op (WSEG m k w1) (WSEG m k w2) = WSEG m k (op w1 w2))

PBITOP_BIT

|- !(op::PBITOP) n (w::PWORDLEN n) k.
     k < n ==> (op (WORD [BIT k w]) = WORD [BIT k (op w)])

PBITOP_PWORDLEN

|- !(op::PBITOP) n (w::PWORDLEN n). PWORDLEN n (op w)

PBITOP_WSEG

|- !(op::PBITOP) n (w::PWORDLEN n) m k.
     m + k <= n ==> (op (WSEG m k w) = WSEG m k (op w))

SHL_WSEG

|- !n (w::PWORDLEN n) m k.
     m + k <= n ==>
     0 < m ==>
     !f b.
       SHL f (WSEG m k w) b =
       (BIT (k + (m - 1)) w,
        (if f then
           WCAT (WSEG (m - 1) k w,WSEG 1 k w)
         else
           WCAT (WSEG (m - 1) k w,WORD [b])))

SHL_WSEG_1F

|- !n (w::PWORDLEN n) m k.
     m + k <= n ==>
     0 < m ==>
     !b.
       SHL F (WSEG m k w) b =
       (BIT (k + (m - 1)) w,WCAT (WSEG (m - 1) k w,WORD [b]))

SHL_WSEG_NF

|- !n (w::PWORDLEN n) m k.
     m + k <= n ==>
     0 < m ==>
     0 < k ==>
     (SHL F (WSEG m k w) (BIT (k - 1) w) =
      (BIT (k + (m - 1)) w,WSEG m (k - 1) w))

SHR_WSEG

|- !n (w::PWORDLEN n) m k.
     m + k <= n ==>
     0 < m ==>
     !f b.
       SHR f b (WSEG m k w) =
       ((if f then
           WCAT (WSEG 1 (k + (m - 1)) w,WSEG (m - 1) (k + 1) w)
         else
           WCAT (WORD [b],WSEG (m - 1) (k + 1) w)),BIT k w)

SHR_WSEG_1F

|- !n (w::PWORDLEN n) m k.
     m + k <= n ==>
     0 < m ==>
     !b.
       SHR F b (WSEG m k w) = (WCAT (WORD [b],WSEG (m - 1) (k + 1) w),BIT k w)

SHR_WSEG_NF

|- !n (w::PWORDLEN n) m k.
     m + k < n ==>
     0 < m ==>
     (SHR F (BIT (m + k) w) (WSEG m k w) = (WSEG m (k + 1) w,BIT k w))

WMAP_0

|- !f. WMAP f (WORD []) = WORD []

WMAP_BIT

|- !n (w::PWORDLEN n) k. k < n ==> !f. BIT k (WMAP f w) = f (BIT k w)

WMAP_o

|- !w f g. WMAP g (WMAP f w) = WMAP (g o f) w

WMAP_PBITOP

|- !f. PBITOP (WMAP f)

WMAP_PWORDLEN

|- !(w::PWORDLEN n) f. PWORDLEN n (WMAP f w)

WMAP_WCAT

|- !w1 w2 f. WMAP f (WCAT (w1,w2)) = WCAT (WMAP f w1,WMAP f w2)

WMAP_WSEG

|- !n (w::PWORDLEN n) m k.
     m + k <= n ==> !f. WMAP f (WSEG m k w) = WSEG m k (WMAP f w)

WSEG_SHL

|- !n (w::PWORDLEN (SUC n)) m k.
     0 < k /\ m + k <= SUC n ==>
     !b. WSEG m k (SND (SHL f w b)) = WSEG m (k - 1) w

WSEG_SHL_0

|- !n (w::PWORDLEN (SUC n)) m b.
     0 < m /\ m <= SUC n ==>
     (WSEG m 0 (SND (SHL f w b)) =
      WCAT (WSEG (m - 1) 0 w,(if f then WSEG 1 0 w else WORD [b])))