Theory: word_base

Parents

• res_quan
• rich_list

Types

• word(Arity = 1)

Constants

• WORDLEN  :'a word -> num
• word_case  :('a list -> 'b) -> 'a word -> 'b
• ii_internalword_base0  :'a list -> 'a word
• WCAT  :'a word # 'a word -> 'a word
• WSPLIT  :num -> 'a word -> 'a word # 'a word
• WORD  :'a list -> 'a word
• WSEG  :num -> num -> 'a word -> 'a word
• BIT  :num -> 'a word -> 'a
• ii_internal_dest_word  :'a word -> 'a list recspace
• LSB  :'a word -> 'a
• MSB  :'a word -> 'a
• PWORDLEN  :num -> 'a word -> bool
• word_size  :('a -> num) -> 'a word -> num
• ii_internal_mk_word  :'a list recspace -> 'a word

Definitions

BIT_DEF

|- !k l. BIT k (WORD l) = ELL k l

ii_internalword_base0_def

|- ii_internalword_base0 =
   (\a. ii_internal_mk_word ((\a. CONSTR 0 a (\n. BOTTOM)) a))

LSB_DEF

|- !l. LSB (WORD l) = LAST l

MSB_DEF

|- !l. MSB (WORD l) = HD l

PWORDLEN_DEF

|- !n l. PWORDLEN n (WORD l) = (n = LENGTH l)

WCAT_DEF

|- !l1 l2. WCAT (WORD l1,WORD l2) = WORD (APPEND l1 l2)

WORD

|- WORD = ii_internalword_base0

word_case_def

|- !f a. word_case f (WORD a) = f a

word_repfns

|- (!a. ii_internal_mk_word (ii_internal_dest_word a) = a) /\
   !r.
     (\a0.
        !'word'.
          (!a0. (?a. a0 = (\a. CONSTR 0 a (\n. BOTTOM)) a) ==> 'word' a0) ==>
          'word' a0) r =
     (ii_internal_dest_word (ii_internal_mk_word r) = r)

word_size_def

|- !f a. word_size f (WORD a) = 1 + list_size f a

word_TY_DEF

|- ?rep.
     TYPE_DEFINITION
       (\a0.
          !'word'.
            (!a0.
               (?a. a0 = (\a. CONSTR 0 a (\n. BOTTOM)) a) ==> 'word' a0) ==>
            'word' a0) rep

WORDLEN_DEF

|- !l. WORDLEN (WORD l) = LENGTH l

WSEG_DEF

|- !m k l. WSEG m k (WORD l) = WORD (LASTN m (BUTLASTN k l))

WSPLIT_DEF

|- !m l. WSPLIT m (WORD l) = (WORD (BUTLASTN m l),WORD (LASTN m l))

Theorems

BIT0

|- !b. BIT 0 (WORD [b]) = b

BIT_EQ_IMP_WORD_EQ

|- !n (w1::PWORDLEN n) (w2::PWORDLEN n).
     (!k. k < n ==> (BIT k w1 = BIT k w2)) ==> (w1 = w2)

BIT_WCAT1

|- !n (w::PWORDLEN n) b. BIT n (WCAT (WORD [b],w)) = b

BIT_WCAT_FST

|- !n1 n2 (w1::PWORDLEN n1) (w2::PWORDLEN n2) k.
     n2 <= k /\ k < n1 + n2 ==> (BIT k (WCAT (w1,w2)) = BIT (k - n2) w1)

BIT_WCAT_SND

|- !n1 n2 (w1::PWORDLEN n1) (w2::PWORDLEN n2) k.
     k < n2 ==> (BIT k (WCAT (w1,w2)) = BIT k w2)

BIT_WSEG

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

LSB

|- !n (w::PWORDLEN n). 0 < n ==> (LSB w = BIT 0 w)

MSB

|- !n (w::PWORDLEN n). 0 < n ==> (MSB w = BIT (PRE n) w)

PWORDLEN

|- !n w. PWORDLEN n w = (WORDLEN w = n)

PWORDLEN0

|- !w. PWORDLEN 0 w ==> (w = WORD [])

PWORDLEN1

|- !x. PWORDLEN 1 (WORD [x])

WCAT0

|- !w. (WCAT (WORD [],w) = w) /\ (WCAT (w,WORD []) = w)

WCAT_11

|- !m n (wm1::PWORDLEN m) (wm2::PWORDLEN m) (wn1::PWORDLEN n)
      (wn2::PWORDLEN n).
     (WCAT (wm1,wn1) = WCAT (wm2,wn2)) = (wm1 = wm2) /\ (wn1 = wn2)

WCAT_ASSOC

|- !w1 w2 w3. WCAT (w1,WCAT (w2,w3)) = WCAT (WCAT (w1,w2),w3)

WCAT_PWORDLEN

|- !n1 (w1::PWORDLEN n1) n2 (w2::PWORDLEN n2).
     PWORDLEN (n1 + n2) (WCAT (w1,w2))

WCAT_WSEG_WSEG

|- !n (w::PWORDLEN n) m1 m2 k.
     m1 + (m2 + k) <= n ==>
     (WCAT (WSEG m2 (m1 + k) w,WSEG m1 k w) = WSEG (m1 + m2) k w)

WORD_11

|- !l l'. (WORD l = WORD l') = (l = l')

word_Ax

|- !f. ?fn. !a. fn (WORD a) = f a

word_Axiom

|- !f. ?fn. !a. fn (WORD a) = f a

word_case_cong

|- !f' f M' M.
     (M = M') /\ (!a. (M' = WORD a) ==> (f a = f' a)) ==>
     (word_case f M = word_case f' M')

word_cases

|- !w. ?l. w = WORD l

WORD_CONS_WCAT

|- !x l. WORD (x::l) = WCAT (WORD [x],WORD l)

word_induct

|- !P. (!l. P (WORD l)) ==> !w. P w

word_induction

|- !P. (!l. P (WORD l)) ==> !w. P w

word_nchotomy

|- !w. ?l. w = WORD l

WORD_PARTITION

|- (!n (w::PWORDLEN n) m. m <= n ==> (WCAT (WSPLIT m w) = w)) /\
   !n m (w1::PWORDLEN n) (w2::PWORDLEN m). WSPLIT m (WCAT (w1,w2)) = (w1,w2)

WORD_SNOC_WCAT

|- !l x. WORD (SNOC x l) = WCAT (WORD l,WORD [x])

WORD_SPLIT

|- !n1 n2 (w::PWORDLEN (n1 + n2)). w = WCAT (WSEG n1 n2 w,WSEG n2 0 w)

WORDLEN_SUC_WCAT

|- !n w.
     PWORDLEN (SUC n) w ==> ?(b::PWORDLEN 1) (w'::PWORDLEN n). w = WCAT (b,w')

WORDLEN_SUC_WCAT_BIT_WSEG

|- !n (w::PWORDLEN (SUC n)). w = WCAT (WORD [BIT n w],WSEG n 0 w)

WORDLEN_SUC_WCAT_BIT_WSEG_RIGHT

|- !n (w::PWORDLEN (SUC n)). w = WCAT (WSEG n 1 w,WORD [BIT 0 w])

WORDLEN_SUC_WCAT_WSEG_WSEG

|- !w::PWORDLEN (SUC n). w = WCAT (WSEG 1 n w,WSEG n 0 w)

WORDLEN_SUC_WCAT_WSEG_WSEG_RIGHT

|- !w::PWORDLEN (SUC n). w = WCAT (WSEG n 1 w,WSEG 1 0 w)

WSEG0

|- !k w. WSEG 0 k w = WORD []

WSEG_BIT

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

WSEG_PWORDLEN

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

WSEG_WCAT1

|- !n1 n2 (w1::PWORDLEN n1) (w2::PWORDLEN n2). WSEG n1 n2 (WCAT (w1,w2)) = w1

WSEG_WCAT2

|- !n1 n2 (w1::PWORDLEN n1) (w2::PWORDLEN n2). WSEG n2 0 (WCAT (w1,w2)) = w2

WSEG_WCAT_WSEG

|- !n1 n2 (w1::PWORDLEN n1) (w2::PWORDLEN n2) m k.
     m + k <= n1 + n2 /\ k < n2 /\ n2 <= m + k ==>
     (WSEG m k (WCAT (w1,w2)) =
      WCAT (WSEG (m + k - n2) 0 w1,WSEG (n2 - k) k w2))

WSEG_WCAT_WSEG1

|- !n1 n2 (w1::PWORDLEN n1) (w2::PWORDLEN n2) m k.
     m <= n1 /\ n2 <= k ==> (WSEG m k (WCAT (w1,w2)) = WSEG m (k - n2) w1)

WSEG_WCAT_WSEG2

|- !n1 n2 (w1::PWORDLEN n1) (w2::PWORDLEN n2) m k.
     m + k <= n2 ==> (WSEG m k (WCAT (w1,w2)) = WSEG m k w2)

WSEG_WORD_LENGTH

|- !n (w::PWORDLEN n). WSEG n 0 w = w

WSEG_WORDLEN

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

WSEG_WSEG

|- !n (w::PWORDLEN n) m1 k1 m2 k2.
     m1 + k1 <= n /\ m2 + k2 <= m1 ==>
     (WSEG m2 k2 (WSEG m1 k1 w) = WSEG m2 (k1 + k2) w)

WSPLIT_PWORDLEN

|- !n (w::PWORDLEN n) m.
     m <= n ==>
     PWORDLEN (n - m) (FST (WSPLIT m w)) /\ PWORDLEN m (SND (WSPLIT m w))

WSPLIT_WSEG

|- !n (w::PWORDLEN n) k.
     k <= n ==> (WSPLIT k w = (WSEG (n - k) k w,WSEG k 0 w))

WSPLIT_WSEG1

|- !n (w::PWORDLEN n) k. k <= n ==> (FST (WSPLIT k w) = WSEG (n - k) k w)

WSPLIT_WSEG2

|- !n (w::PWORDLEN n) k. k <= n ==> (SND (WSPLIT k w) = WSEG k 0 w)