Structure bword_numTheory

signature bword_numTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val BNVAL_DEF : thm
    val BV_DEF : thm
    val NBWORD_DEF : thm
    val VB_DEF : thm
  
  (*  Theorems  *)
    val ADD_BNVAL_LEFT : thm
    val ADD_BNVAL_RIGHT : thm
    val ADD_BNVAL_SPLIT : thm
    val BIT_NBWORD0 : thm
    val BNVAL0 : thm
    val BNVAL_11 : thm
    val BNVAL_MAX : thm
    val BNVAL_NBWORD : thm
    val BNVAL_NVAL : thm
    val BNVAL_ONTO : thm
    val BNVAL_WCAT : thm
    val BNVAL_WCAT1 : thm
    val BNVAL_WCAT2 : thm
    val BV_LESS_2 : thm
    val BV_VB : thm
    val DOUBL_EQ_SHL : thm
    val EQ_NBWORD0_SPLIT : thm
    val MSB_NBWORD : thm
    val NBWORD0 : thm
    val NBWORD_BNVAL : thm
    val NBWORD_MOD : thm
    val NBWORD_SPLIT : thm
    val NBWORD_SUC : thm
    val NBWORD_SUC_FST : thm
    val NBWORD_SUC_WSEG : thm
    val PWORDLEN_NBWORD : thm
    val VB_BV : thm
    val WCAT_NBWORD_0 : thm
    val WORDLEN_NBWORD : thm
    val WSEG_NBWORD : thm
    val WSEG_NBWORD_SUC : thm
    val WSPLIT_NBWORD_0 : thm
    val ZERO_WORD_VAL : thm
  
  val bword_num_grammars : type_grammar.grammar * term_grammar.grammar
  
  
(*
   [word_bitop] Parent theory of "bword_num"
   
   [word_num] Parent theory of "bword_num"
   
   [BNVAL_DEF]  Definition
      
      |- !l. BNVAL (WORD l) = LVAL BV 2 l
   
   [BV_DEF]  Definition
      
      |- !b. BV b = (if b then SUC 0 else 0)
   
   [NBWORD_DEF]  Definition
      
      |- !n m. NBWORD n m = WORD (NLIST n VB 2 m)
   
   [VB_DEF]  Definition
      
      |- !n. VB n = ~(n MOD 2 = 0)
   
   [ADD_BNVAL_LEFT]  Theorem
      
      |- !n (w1::PWORDLEN (SUC n)) (w2::PWORDLEN (SUC n)).
           BNVAL w1 + BNVAL w2 =
           (BV (BIT n w1) + BV (BIT n w2)) * 2 ** n +
           (BNVAL (WSEG n 0 w1) + BNVAL (WSEG n 0 w2))
   
   [ADD_BNVAL_RIGHT]  Theorem
      
      |- !n (w1::PWORDLEN (SUC n)) (w2::PWORDLEN (SUC n)).
           BNVAL w1 + BNVAL w2 =
           (BNVAL (WSEG n 1 w1) + BNVAL (WSEG n 1 w2)) * 2 +
           (BV (BIT 0 w1) + BV (BIT 0 w2))
   
   [ADD_BNVAL_SPLIT]  Theorem
      
      |- !n1 n2 (w1::PWORDLEN (n1 + n2)) (w2::PWORDLEN (n1 + n2)).
           BNVAL w1 + BNVAL w2 =
           (BNVAL (WSEG n1 n2 w1) + BNVAL (WSEG n1 n2 w2)) * 2 ** n2 +
           (BNVAL (WSEG n2 0 w1) + BNVAL (WSEG n2 0 w2))
   
   [BIT_NBWORD0]  Theorem
      
      |- !k n. k < n ==> (BIT k (NBWORD n 0) = F)
   
   [BNVAL0]  Theorem
      
      |- BNVAL (WORD []) = 0
   
   [BNVAL_11]  Theorem
      
      |- !w1 w2. (WORDLEN w1 = WORDLEN w2) ==> (BNVAL w1 = BNVAL w2) ==> (w1 = w2)
   
   [BNVAL_MAX]  Theorem
      
      |- !n (w::PWORDLEN n). BNVAL w < 2 ** n
   
   [BNVAL_NBWORD]  Theorem
      
      |- !n m. m < 2 ** n ==> (BNVAL (NBWORD n m) = m)
   
   [BNVAL_NVAL]  Theorem
      
      |- !w. BNVAL w = NVAL BV 2 w
   
   [BNVAL_ONTO]  Theorem
      
      |- !w. ?n. BNVAL w = n
   
   [BNVAL_WCAT]  Theorem
      
      |- !n m (w1::PWORDLEN n) (w2::PWORDLEN m).
           BNVAL (WCAT (w1,w2)) = BNVAL w1 * 2 ** m + BNVAL w2
   
   [BNVAL_WCAT1]  Theorem
      
      |- !n (w::PWORDLEN n) x. BNVAL (WCAT (w,WORD [x])) = BNVAL w * 2 + BV x
   
   [BNVAL_WCAT2]  Theorem
      
      |- !n (w::PWORDLEN n) x. BNVAL (WCAT (WORD [x],w)) = BV x * 2 ** n + BNVAL w
   
   [BV_LESS_2]  Theorem
      
      |- !x. BV x < 2
   
   [BV_VB]  Theorem
      
      |- !x. x < 2 ==> (BV (VB x) = x)
   
   [DOUBL_EQ_SHL]  Theorem
      
      |- !n.
           0 < n ==>
           !(w::PWORDLEN n) b. NBWORD n (BNVAL w + BNVAL w + BV b) = SND (SHL F w b)
   
   [EQ_NBWORD0_SPLIT]  Theorem
      
      |- !n (w::PWORDLEN n) m.
           m <= n ==>
           ((w = NBWORD n 0) =
            (WSEG (n - m) m w = NBWORD (n - m) 0) /\ (WSEG m 0 w = NBWORD m 0))
   
   [MSB_NBWORD]  Theorem
      
      |- !n m. BIT n (NBWORD (SUC n) m) = VB ((m DIV 2 ** n) MOD 2)
   
   [NBWORD0]  Theorem
      
      |- !m. NBWORD 0 m = WORD []
   
   [NBWORD_BNVAL]  Theorem
      
      |- !n (w::PWORDLEN n). NBWORD n (BNVAL w) = w
   
   [NBWORD_MOD]  Theorem
      
      |- !n m. NBWORD n (m MOD 2 ** n) = NBWORD n m
   
   [NBWORD_SPLIT]  Theorem
      
      |- !n1 n2 m. NBWORD (n1 + n2) m = WCAT (NBWORD n1 (m DIV 2 ** n2),NBWORD n2 m)
   
   [NBWORD_SUC]  Theorem
      
      |- !n m. NBWORD (SUC n) m = WCAT (NBWORD n (m DIV 2),WORD [VB (m MOD 2)])
   
   [NBWORD_SUC_FST]  Theorem
      
      |- !n m. NBWORD (SUC n) m = WCAT (WORD [VB ((m DIV 2 ** n) MOD 2)],NBWORD n m)
   
   [NBWORD_SUC_WSEG]  Theorem
      
      |- !n (w::PWORDLEN (SUC n)). NBWORD n (BNVAL w) = WSEG n 0 w
   
   [PWORDLEN_NBWORD]  Theorem
      
      |- !n m. NBWORD n m IN PWORDLEN n
   
   [VB_BV]  Theorem
      
      |- !x. VB (BV x) = x
   
   [WCAT_NBWORD_0]  Theorem
      
      |- !n1 n2. WCAT (NBWORD n1 0,NBWORD n2 0) = NBWORD (n1 + n2) 0
   
   [WORDLEN_NBWORD]  Theorem
      
      |- !n m. WORDLEN (NBWORD n m) = n
   
   [WSEG_NBWORD]  Theorem
      
      |- !m k n. m + k <= n ==> !l. WSEG m k (NBWORD n l) = NBWORD m (l DIV 2 ** k)
   
   [WSEG_NBWORD_SUC]  Theorem
      
      |- !n m. WSEG n 0 (NBWORD (SUC n) m) = NBWORD n m
   
   [WSPLIT_NBWORD_0]  Theorem
      
      |- !n m. m <= n ==> (WSPLIT m (NBWORD n 0) = (NBWORD (n - m) 0,NBWORD m 0))
   
   [ZERO_WORD_VAL]  Theorem
      
      |- !w::PWORDLEN n. (w = NBWORD n 0) = (BNVAL w = 0)
   
   
*)
end