Structure bitTheory

signature bitTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val BITS_def : thm
    val BITV_def : thm
    val BITWISE_def : thm
    val BIT_MODIFY_def : thm
    val BIT_REVERSE_def : thm
    val BIT_def : thm
    val DIVMOD_2EXP_def : thm
    val LOG2_def : thm
    val LSB_def : thm
    val SBIT_def : thm
    val SIGN_EXTEND_def : thm
    val SLICE_def : thm
    val TIMES_2EXP_def : thm
  
  (*  Theorems  *)
    val BITSLT_THM : thm
    val BITS_COMP_THM : thm
    val BITS_COMP_THM2 : thm
    val BITS_DIV_THM : thm
    val BITS_LT_HIGH : thm
    val BITS_SLICE_THM : thm
    val BITS_SLICE_THM2 : thm
    val BITS_SUC : thm
    val BITS_SUC_THM : thm
    val BITS_SUM : thm
    val BITS_SUM2 : thm
    val BITS_THM : thm
    val BITS_THM2 : thm
    val BITS_ZERO : thm
    val BITS_ZERO2 : thm
    val BITS_ZERO3 : thm
    val BITS_ZERO4 : thm
    val BITS_ZEROL : thm
    val BITV_THM : thm
    val BITWISE_BITS : thm
    val BITWISE_COR : thm
    val BITWISE_EVAL : thm
    val BITWISE_LT_2EXP : thm
    val BITWISE_NOT_COR : thm
    val BITWISE_ONE_COMP_LEM : thm
    val BITWISE_THM : thm
    val BIT_B : thm
    val BIT_BITS_THM : thm
    val BIT_B_NEQ : thm
    val BIT_COMP_THM3 : thm
    val BIT_MODIFY_THM : thm
    val BIT_OF_BITS_THM : thm
    val BIT_OF_BITS_THM2 : thm
    val BIT_REVERSE_THM : thm
    val BIT_SHIFT_THM : thm
    val BIT_SHIFT_THM2 : thm
    val BIT_SHIFT_THM3 : thm
    val BIT_SLICE : thm
    val BIT_SLICE_LEM : thm
    val BIT_SLICE_THM : thm
    val BIT_SLICE_THM2 : thm
    val BIT_SLICE_THM3 : thm
    val BIT_SLICE_THM4 : thm
    val BIT_ZERO : thm
    val DIVMOD_2EXP : thm
    val DIV_MULT_1 : thm
    val DIV_MULT_THM : thm
    val DIV_MULT_THM2 : thm
    val EXP_SUB_LESS_EQ : thm
    val LESS_EQ_EXP_MULT : thm
    val LOG2_UNIQUE : thm
    val LSB_ODD : thm
    val MOD_2EXP_LT : thm
    val MOD_2EXP_MONO : thm
    val MOD_ADD_1 : thm
    val MOD_PLUS_1 : thm
    val MOD_PLUS_RIGHT : thm
    val NOT_BIT : thm
    val NOT_BITS : thm
    val NOT_BITS2 : thm
    val NOT_MOD2_LEM : thm
    val NOT_MOD2_LEM2 : thm
    val NOT_ZERO_ADD1 : thm
    val ODD_MOD2_LEM : thm
    val SBIT_DIV : thm
    val SBIT_MULT : thm
    val SLICELT_THM : thm
    val SLICE_COMP_RWT : thm
    val SLICE_COMP_THM : thm
    val SLICE_COMP_THM2 : thm
    val SLICE_THM : thm
    val SLICE_ZERO : thm
    val SLICE_ZERO_THM : thm
    val SUC_SUB : thm
    val TWOEXP_DIVISION : thm
    val TWOEXP_MONO : thm
    val TWOEXP_MONO2 : thm
    val TWOEXP_NOT_ZERO : thm
    val ZERO_LT_TWOEXP : thm
  
  val bit_grammars : type_grammar.grammar * term_grammar.grammar
  
  
(*
   [list] Parent theory of "bit"
   
   [logroot] Parent theory of "bit"
   
   [BITS_def]  Definition
      
      |- !h l n. BITS h l n = MOD_2EXP (SUC h - l) (DIV_2EXP l n)
   
   [BITV_def]  Definition
      
      |- !n b. BITV n b = BITS b b n
   
   [BITWISE_def]  Definition
      
      |- (!op x y. BITWISE 0 op x y = 0) /\
         !n op x y.
           BITWISE (SUC n) op x y =
           BITWISE n op x y + SBIT (op (BIT n x) (BIT n y)) n
   
   [BIT_MODIFY_def]  Definition
      
      |- (!f x. BIT_MODIFY 0 f x = 0) /\
         !n f x. BIT_MODIFY (SUC n) f x = BIT_MODIFY n f x + SBIT (f n (BIT n x)) n
   
   [BIT_REVERSE_def]  Definition
      
      |- (!x. BIT_REVERSE 0 x = 0) /\
         !n x. BIT_REVERSE (SUC n) x = BIT_REVERSE n x * 2 + SBIT (BIT n x) 0
   
   [BIT_def]  Definition
      
      |- !b n. BIT b n = (BITS b b n = 1)
   
   [DIVMOD_2EXP_def]  Definition
      
      |- !x n. DIVMOD_2EXP x n = (n DIV 2 ** x,n MOD 2 ** x)
   
   [LOG2_def]  Definition
      
      |- LOG2 = LOG 2
   
   [LSB_def]  Definition
      
      |- LSB = BIT 0
   
   [SBIT_def]  Definition
      
      |- !b n. SBIT b n = (if b then 2 ** n else 0)
   
   [SIGN_EXTEND_def]  Definition
      
      |- !l h n.
           SIGN_EXTEND l h n =
           (let m = n MOD 2 ** l in
              (if BIT (l - 1) n then 2 ** h - 2 ** l + m else m))
   
   [SLICE_def]  Definition
      
      |- !h l n. SLICE h l n = MOD_2EXP (SUC h) n - MOD_2EXP l n
   
   [TIMES_2EXP_def]  Definition
      
      |- !x n. TIMES_2EXP x n = n * 2 ** x
   
   [BITSLT_THM]  Theorem
      
      |- !h l n. BITS h l n < 2 ** (SUC h - l)
   
   [BITS_COMP_THM]  Theorem
      
      |- !h1 l1 h2 l2 n.
           h2 + l1 <= h1 ==> (BITS h2 l2 (BITS h1 l1 n) = BITS (h2 + l1) (l2 + l1) n)
   
   [BITS_COMP_THM2]  Theorem
      
      |- !h1 l1 h2 l2 n.
           BITS h2 l2 (BITS h1 l1 n) = BITS (MIN h1 (h2 + l1)) (l2 + l1) n
   
   [BITS_DIV_THM]  Theorem
      
      |- !h l x n. BITS h l x DIV 2 ** n = BITS h (l + n) x
   
   [BITS_LT_HIGH]  Theorem
      
      |- !h l n. n < 2 ** SUC h ==> (BITS h l n = n DIV 2 ** l)
   
   [BITS_SLICE_THM]  Theorem
      
      |- !h l n. BITS h l (SLICE h l n) = BITS h l n
   
   [BITS_SLICE_THM2]  Theorem
      
      |- !h l n. h <= h2 ==> (BITS h2 l (SLICE h l n) = BITS h l n)
   
   [BITS_SUC]  Theorem
      
      |- !h l n.
           l <= SUC h ==>
           (SBIT (BIT (SUC h) n) (SUC h - l) + BITS h l n = BITS (SUC h) l n)
   
   [BITS_SUC_THM]  Theorem
      
      |- !h l n.
           BITS (SUC h) l n =
           (if SUC h < l then 0 else SBIT (BIT (SUC h) n) (SUC h - l) + BITS h l n)
   
   [BITS_SUM]  Theorem
      
      |- !h l a b. b < 2 ** l ==> (BITS h l (a * 2 ** l + b) = BITS h l (a * 2 ** l))
   
   [BITS_SUM2]  Theorem
      
      |- !h l a b. BITS h l (a * 2 ** SUC h + b) = BITS h l b
   
   [BITS_THM]  Theorem
      
      |- !h l n. BITS h l n = (n DIV 2 ** l) MOD 2 ** (SUC h - l)
   
   [BITS_THM2]  Theorem
      
      |- !h l n. BITS h l n = n MOD 2 ** SUC h DIV 2 ** l
   
   [BITS_ZERO]  Theorem
      
      |- !h l n. h < l ==> (BITS h l n = 0)
   
   [BITS_ZERO2]  Theorem
      
      |- !h l. BITS h l 0 = 0
   
   [BITS_ZERO3]  Theorem
      
      |- !h n. BITS h 0 n = n MOD 2 ** SUC h
   
   [BITS_ZERO4]  Theorem
      
      |- !h l n. l <= h ==> (BITS h l (a * 2 ** l) = BITS (h - l) 0 a)
   
   [BITS_ZEROL]  Theorem
      
      |- !h a. a < 2 ** SUC h ==> (BITS h 0 a = a)
   
   [BITV_THM]  Theorem
      
      |- !b n. BITV n b = SBIT (BIT b n) 0
   
   [BITWISE_BITS]  Theorem
      
      |- !wl op a b.
           BITWISE (SUC wl) op (BITS wl 0 a) (BITS wl 0 b) = BITWISE (SUC wl) op a b
   
   [BITWISE_COR]  Theorem
      
      |- !x n op a b.
           x < n ==>
           op (BIT x a) (BIT x b) ==>
           ((BITWISE n op a b DIV 2 ** x) MOD 2 = 1)
   
   [BITWISE_EVAL]  Theorem
      
      |- !n op a b.
           BITWISE (SUC n) op a b =
           2 * BITWISE n op (a DIV 2) (b DIV 2) + SBIT (op (LSB a) (LSB b)) 0
   
   [BITWISE_LT_2EXP]  Theorem
      
      |- !n op a b. BITWISE n op a b < 2 ** n
   
   [BITWISE_NOT_COR]  Theorem
      
      |- !x n op a b.
           x < n ==>
           ~op (BIT x a) (BIT x b) ==>
           ((BITWISE n op a b DIV 2 ** x) MOD 2 = 0)
   
   [BITWISE_ONE_COMP_LEM]  Theorem
      
      |- !n a b. BITWISE (SUC n) (\x y. ~x) a b = 2 ** SUC n - 1 - BITS n 0 a
   
   [BITWISE_THM]  Theorem
      
      |- !x n op a b. x < n ==> (BIT x (BITWISE n op a b) = op (BIT x a) (BIT x b))
   
   [BIT_B]  Theorem
      
      |- !b. BIT b (2 ** b)
   
   [BIT_BITS_THM]  Theorem
      
      |- !h l a b.
           (!x. l <= x /\ x <= h ==> (BIT x a = BIT x b)) = (BITS h l a = BITS h l b)
   
   [BIT_B_NEQ]  Theorem
      
      |- !a b. ~(a = b) ==> ~BIT a (2 ** b)
   
   [BIT_COMP_THM3]  Theorem
      
      |- !h m l n.
           SUC m <= h /\ l <= m ==>
           (BITS h (SUC m) n * 2 ** (SUC m - l) + BITS m l n = BITS h l n)
   
   [BIT_MODIFY_THM]  Theorem
      
      |- !x n f a. x < n ==> (BIT x (BIT_MODIFY n f a) = f x (BIT x a))
   
   [BIT_OF_BITS_THM]  Theorem
      
      |- !n h l a. l + n <= h ==> (BIT n (BITS h l a) = BIT (l + n) a)
   
   [BIT_OF_BITS_THM2]  Theorem
      
      |- !h l x n. h < l + x ==> ~BIT x (BITS h l n)
   
   [BIT_REVERSE_THM]  Theorem
      
      |- !x n a. x < n ==> (BIT x (BIT_REVERSE n a) = BIT (n - 1 - x) a)
   
   [BIT_SHIFT_THM]  Theorem
      
      |- !n a s. BIT (n + s) (a * 2 ** s) = BIT n a
   
   [BIT_SHIFT_THM2]  Theorem
      
      |- !n a s. s <= n ==> (BIT n (a * 2 ** s) = BIT (n - s) a)
   
   [BIT_SHIFT_THM3]  Theorem
      
      |- !n a s. n < s ==> ~BIT n (a * 2 ** s)
   
   [BIT_SLICE]  Theorem
      
      |- !n a b. (BIT n a = BIT n b) = (SLICE n n a = SLICE n n b)
   
   [BIT_SLICE_LEM]  Theorem
      
      |- !y x n. SBIT (BIT x n) (x + y) = SLICE x x n * 2 ** y
   
   [BIT_SLICE_THM]  Theorem
      
      |- !x n. SBIT (BIT x n) x = SLICE x x n
   
   [BIT_SLICE_THM2]  Theorem
      
      |- !b n. BIT b n = (SLICE b b n = 2 ** b)
   
   [BIT_SLICE_THM3]  Theorem
      
      |- !b n. ~BIT b n = (SLICE b b n = 0)
   
   [BIT_SLICE_THM4]  Theorem
      
      |- !b h l n. BIT b (SLICE h l n) = l <= b /\ b <= h /\ BIT b n
   
   [BIT_ZERO]  Theorem
      
      |- !b. ~BIT b 0
   
   [DIVMOD_2EXP]  Theorem
      
      |- !x n. DIVMOD_2EXP x n = (DIV_2EXP x n,MOD_2EXP x n)
   
   [DIV_MULT_1]  Theorem
      
      |- !r n. r < n ==> ((n + r) DIV n = 1)
   
   [DIV_MULT_THM]  Theorem
      
      |- !x n. n DIV 2 ** x * 2 ** x = n - n MOD 2 ** x
   
   [DIV_MULT_THM2]  Theorem
      
      |- !n. 2 * (n DIV 2) = n - n MOD 2
   
   [EXP_SUB_LESS_EQ]  Theorem
      
      |- !a b. 2 ** (a - b) <= 2 ** a
   
   [LESS_EQ_EXP_MULT]  Theorem
      
      |- !a b. a <= b ==> ?p. 2 ** b = p * 2 ** a
   
   [LOG2_UNIQUE]  Theorem
      
      |- !n p. 2 ** p <= n /\ n < 2 ** SUC p ==> (LOG2 n = p)
   
   [LSB_ODD]  Theorem
      
      |- LSB = ODD
   
   [MOD_2EXP_LT]  Theorem
      
      |- !n k. k MOD 2 ** n < 2 ** n
   
   [MOD_2EXP_MONO]  Theorem
      
      |- !n h l. l <= h ==> n MOD 2 ** l <= n MOD 2 ** SUC h
   
   [MOD_ADD_1]  Theorem
      
      |- !n. 0 < n ==> !x. ~((x + 1) MOD n = 0) ==> ((x + 1) MOD n = x MOD n + 1)
   
   [MOD_PLUS_1]  Theorem
      
      |- !n. 0 < n ==> !x. ((x + 1) MOD n = 0) = (x MOD n + 1 = n)
   
   [MOD_PLUS_RIGHT]  Theorem
      
      |- !n. 0 < n ==> !j k. (j + k MOD n) MOD n = (j + k) MOD n
   
   [NOT_BIT]  Theorem
      
      |- !n a. ~BIT n a = (BITS n n a = 0)
   
   [NOT_BITS]  Theorem
      
      |- !n a. ~(BITS n n a = 0) = (BITS n n a = 1)
   
   [NOT_BITS2]  Theorem
      
      |- !n a. ~(BITS n n a = 1) = (BITS n n a = 0)
   
   [NOT_MOD2_LEM]  Theorem
      
      |- !n. ~(n MOD 2 = 0) = (n MOD 2 = 1)
   
   [NOT_MOD2_LEM2]  Theorem
      
      |- !n a. ~(n MOD 2 = 1) = (n MOD 2 = 0)
   
   [NOT_ZERO_ADD1]  Theorem
      
      |- !m. ~(m = 0) ==> ?p. m = SUC p
   
   [ODD_MOD2_LEM]  Theorem
      
      |- !n. ODD n = (n MOD 2 = 1)
   
   [SBIT_DIV]  Theorem
      
      |- !b m n. n < m ==> (SBIT b (m - n) = SBIT b m DIV 2 ** n)
   
   [SBIT_MULT]  Theorem
      
      |- !b m n. SBIT b n * 2 ** m = SBIT b (n + m)
   
   [SLICELT_THM]  Theorem
      
      |- !h l n. SLICE h l n < 2 ** SUC h
   
   [SLICE_COMP_RWT]  Theorem
      
      |- !h m' m l n.
           l <= m /\ (m' = m + 1) /\ m < h ==>
           (SLICE h m' n + SLICE m l n = SLICE h l n)
   
   [SLICE_COMP_THM]  Theorem
      
      |- !h m l n.
           SUC m <= h /\ l <= m ==> (SLICE h (SUC m) n + SLICE m l n = SLICE h l n)
   
   [SLICE_COMP_THM2]  Theorem
      
      |- !h l x y n. h <= x /\ y <= l ==> (SLICE h l (SLICE x y n) = SLICE h l n)
   
   [SLICE_THM]  Theorem
      
      |- !n h l. SLICE h l n = BITS h l n * 2 ** l
   
   [SLICE_ZERO]  Theorem
      
      |- !h l n. h < l ==> (SLICE h l n = 0)
   
   [SLICE_ZERO_THM]  Theorem
      
      |- !n h. SLICE h 0 n = BITS h 0 n
   
   [SUC_SUB]  Theorem
      
      |- SUC a - a = 1
   
   [TWOEXP_DIVISION]  Theorem
      
      |- !n k. k = k DIV 2 ** n * 2 ** n + k MOD 2 ** n
   
   [TWOEXP_MONO]  Theorem
      
      |- !a b. a < b ==> 2 ** a < 2 ** b
   
   [TWOEXP_MONO2]  Theorem
      
      |- !a b. a <= b ==> 2 ** a <= 2 ** b
   
   [TWOEXP_NOT_ZERO]  Theorem
      
      |- !n. ~(2 ** n = 0)
   
   [ZERO_LT_TWOEXP]  Theorem
      
      |- !n. 0 < 2 ** n
   
   
*)
end