Structure bword_arithTheory

signature bword_arithTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val ACARRY_DEF : thm
    val ICARRY_DEF : thm
  
  (*  Theorems  *)
    val ACARRY_ACARRY_WSEG : thm
    val ACARRY_EQ_ADD_DIV : thm
    val ACARRY_EQ_ICARRY : thm
    val ACARRY_MSB : thm
    val ACARRY_WSEG : thm
    val ADD_BNVAL_LESS_EQ1 : thm
    val ADD_BV_BNVAL_DIV_LESS_EQ1 : thm
    val ADD_BV_BNVAL_LESS_EQ : thm
    val ADD_BV_BNVAL_LESS_EQ1 : thm
    val ADD_NBWORD_EQ0_SPLIT : thm
    val ADD_WORD_SPLIT : thm
    val BNVAL_LESS_EQ : thm
    val ICARRY_WSEG : thm
    val WSEG_NBWORD_ADD : thm
  
  val bword_arith_grammars : type_grammar.grammar * term_grammar.grammar
  
  
(*
   [bword_num] Parent theory of "bword_arith"
   
   [ACARRY_DEF]  Definition
      
      |- (!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]  Definition
      
      |- (!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
   
   [ACARRY_ACARRY_WSEG]  Theorem
      
      |- !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]  Theorem
      
      |- !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]  Theorem
      
      |- !n (w1::PWORDLEN n) (w2::PWORDLEN n) cin k.
           k <= n ==> (ACARRY k w1 w2 cin = ICARRY k w1 w2 cin)
   
   [ACARRY_MSB]  Theorem
      
      |- !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]  Theorem
      
      |- !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_BNVAL_LESS_EQ1]  Theorem
      
      |- !n cin (w1::PWORDLEN n) (w2::PWORDLEN n).
           (BNVAL w1 + (BNVAL w2 + BV cin)) DIV 2 ** n <= SUC 0
   
   [ADD_BV_BNVAL_DIV_LESS_EQ1]  Theorem
      
      |- !n x1 x2 cin (w1::PWORDLEN n) (w2::PWORDLEN n).
           (BV x1 + BV x2 + (BNVAL w1 + (BNVAL w2 + BV cin)) DIV 2 ** n) DIV 2 <= 1
   
   [ADD_BV_BNVAL_LESS_EQ]  Theorem
      
      |- !n x1 x2 cin (w1::PWORDLEN n) (w2::PWORDLEN n).
           BV x1 + BV x2 + (BNVAL w1 + (BNVAL w2 + BV cin)) <= SUC (2 ** SUC n)
   
   [ADD_BV_BNVAL_LESS_EQ1]  Theorem
      
      |- !n x1 x2 cin (w1::PWORDLEN n) (w2::PWORDLEN n).
           (BV x1 + BV x2 + (BNVAL w1 + (BNVAL w2 + BV cin))) DIV 2 ** SUC n <= 1
   
   [ADD_NBWORD_EQ0_SPLIT]  Theorem
      
      |- !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]  Theorem
      
      |- !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))
   
   [BNVAL_LESS_EQ]  Theorem
      
      |- !n (w::PWORDLEN n). BNVAL w <= 2 ** n - 1
   
   [ICARRY_WSEG]  Theorem
      
      |- !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]  Theorem
      
      |- !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)))
   
   
*)
end