Structure numposrepTheory

signature numposrepTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val BOOLIFY_def : thm
    val l2n2 : thm
    val l2n_def : thm
    val num_from_bin_list_def : thm
    val num_from_dec_list_def : thm
    val num_from_hex_list_def : thm
    val num_from_oct_list_def : thm
    val num_to_bin_list_def : thm
    val num_to_dec_list_def : thm
    val num_to_hex_list_def : thm
    val num_to_oct_list_def : thm
  
  (*  Theorems  *)
    val BIT_num_from_bin_list : thm
    val EL_n2l : thm
    val EL_num_to_bin_list : thm
    val LENGTH_l2n : thm
    val LENGTH_n2l : thm
    val LOG_l2n : thm
    val LOG_l2n_dropWhile : thm
    val l2n_2_thms : thm
    val l2n_DIGIT : thm
    val l2n_SNOC_0 : thm
    val l2n_dropWhile_0 : thm
    val l2n_eq_0 : thm
    val l2n_lt : thm
    val l2n_n2l : thm
    val l2n_pow2_compute : thm
    val n2l_BOUND : thm
    val n2l_def : thm
    val n2l_ind : thm
    val n2l_l2n : thm
    val n2l_pow2_compute : thm
    val num_bin_list : thm
    val num_dec_list : thm
    val num_hex_list : thm
    val num_oct_list : thm
  
  val numposrep_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [bit] Parent theory of "numposrep"
   
   [rich_list] Parent theory of "numposrep"
   
   [BOOLIFY_def]  Definition
      
      ⊢ (∀m a. BOOLIFY 0 m a = a) ∧
        ∀n m a. BOOLIFY (SUC n) m a = BOOLIFY n (DIV2 m) (ODD m::a)
   
   [l2n2]  Definition
      
      ⊢ numposrep$l2n2 = l2n 2
   
   [l2n_def]  Definition
      
      ⊢ (∀b. l2n b [] = 0) ∧ ∀b h t. l2n b (h::t) = h MOD b + b * l2n b t
   
   [num_from_bin_list_def]  Definition
      
      ⊢ num_from_bin_list = l2n 2
   
   [num_from_dec_list_def]  Definition
      
      ⊢ num_from_dec_list = l2n 10
   
   [num_from_hex_list_def]  Definition
      
      ⊢ num_from_hex_list = l2n 16
   
   [num_from_oct_list_def]  Definition
      
      ⊢ num_from_oct_list = l2n 8
   
   [num_to_bin_list_def]  Definition
      
      ⊢ num_to_bin_list = n2l 2
   
   [num_to_dec_list_def]  Definition
      
      ⊢ num_to_dec_list = n2l 10
   
   [num_to_hex_list_def]  Definition
      
      ⊢ num_to_hex_list = n2l 16
   
   [num_to_oct_list_def]  Definition
      
      ⊢ num_to_oct_list = n2l 8
   
   [BIT_num_from_bin_list]  Theorem
      
      ⊢ ∀x l.
            EVERY ($> 2) l ∧ x < LENGTH l ⇒
            (BIT x (num_from_bin_list l) ⇔ EL x l = 1)
   
   [EL_n2l]  Theorem
      
      ⊢ ∀b x n.
            1 < b ∧ x < LENGTH (n2l b n) ⇒
            EL x (n2l b n) = (n DIV b ** x) MOD b
   
   [EL_num_to_bin_list]  Theorem
      
      ⊢ ∀x n.
            x < LENGTH (num_to_bin_list n) ⇒
            EL x (num_to_bin_list n) = BITV n x
   
   [LENGTH_l2n]  Theorem
      
      ⊢ ∀b l.
            1 < b ∧ EVERY ($> b) l ∧ l2n b l ≠ 0 ⇒
            SUC (LOG b (l2n b l)) ≤ LENGTH l
   
   [LENGTH_n2l]  Theorem
      
      ⊢ ∀b n. 1 < b ⇒ LENGTH (n2l b n) = if n = 0 then 1 else SUC (LOG b n)
   
   [LOG_l2n]  Theorem
      
      ⊢ ∀b.
            1 < b ⇒
            ∀l.
                l ≠ [] ∧ 0 < LAST l ∧ EVERY ($> b) l ⇒
                LOG b (l2n b l) = PRE (LENGTH l)
   
   [LOG_l2n_dropWhile]  Theorem
      
      ⊢ ∀b l.
            1 < b ∧ EXISTS (λy. 0 ≠ y) l ∧ EVERY ($> b) l ⇒
            LOG b (l2n b l) = PRE (LENGTH (dropWhile ($= 0) (REVERSE l)))
   
   [l2n_2_thms]  Theorem
      
      ⊢ (∀t. l2n 2 (0::t) = NUMERAL (numposrep$l2n2 (0::t))) ∧
        (∀t. l2n 2 (1::t) = NUMERAL (numposrep$l2n2 (1::t))) ∧
        numposrep$l2n2 [] = ZERO ∧
        (∀t. numposrep$l2n2 (0::t) = numeral$iDUB (numposrep$l2n2 t)) ∧
        ∀t. numposrep$l2n2 (1::t) = BIT1 (numposrep$l2n2 t)
   
   [l2n_DIGIT]  Theorem
      
      ⊢ ∀b l x.
            1 < b ∧ EVERY ($> b) l ∧ x < LENGTH l ⇒
            (l2n b l DIV b ** x) MOD b = EL x l
   
   [l2n_SNOC_0]  Theorem
      
      ⊢ ∀b ls. 0 < b ⇒ l2n b (SNOC 0 ls) = l2n b ls
   
   [l2n_dropWhile_0]  Theorem
      
      ⊢ ∀b ls.
            0 < b ⇒
            l2n b (REVERSE (dropWhile ($= 0) (REVERSE ls))) = l2n b ls
   
   [l2n_eq_0]  Theorem
      
      ⊢ ∀b. 0 < b ⇒ ∀l. l2n b l = 0 ⇔ EVERY ($= 0 ∘ combin$C $MOD b) l
   
   [l2n_lt]  Theorem
      
      ⊢ ∀l b. 0 < b ⇒ l2n b l < b ** LENGTH l
   
   [l2n_n2l]  Theorem
      
      ⊢ ∀b n. 1 < b ⇒ l2n b (n2l b n) = n
   
   [l2n_pow2_compute]  Theorem
      
      ⊢ (∀p. l2n (2 ** p) [] = 0) ∧
        ∀p h t.
            l2n (2 ** p) (h::t) =
            MOD_2EXP p h + TIMES_2EXP p (l2n (2 ** p) t)
   
   [n2l_BOUND]  Theorem
      
      ⊢ ∀b n. 0 < b ⇒ EVERY ($> b) (n2l b n)
   
   [n2l_def]  Theorem
      
      ⊢ ∀n b.
            n2l b n =
            if n < b ∨ b < 2 then [n MOD b] else n MOD b::n2l b (n DIV b)
   
   [n2l_ind]  Theorem
      
      ⊢ ∀P.
            (∀b n. (¬(n < b ∨ b < 2) ⇒ P b (n DIV b)) ⇒ P b n) ⇒
            ∀v v1. P v v1
   
   [n2l_l2n]  Theorem
      
      ⊢ ∀b l.
            1 < b ∧ EVERY ($> b) l ⇒
            n2l b (l2n b l) =
            if l2n b l = 0 then [0] else TAKE (SUC (LOG b (l2n b l))) l
   
   [n2l_pow2_compute]  Theorem
      
      ⊢ ∀p n.
            0 < p ⇒
            n2l (2 ** p) n =
            (let
               (q,r) = DIVMOD_2EXP p n
             in
               if q = 0 then [r] else r::n2l (2 ** p) q)
   
   [num_bin_list]  Theorem
      
      ⊢ num_from_bin_list ∘ num_to_bin_list = I
   
   [num_dec_list]  Theorem
      
      ⊢ num_from_dec_list ∘ num_to_dec_list = I
   
   [num_hex_list]  Theorem
      
      ⊢ num_from_hex_list ∘ num_to_hex_list = I
   
   [num_oct_list]  Theorem
      
      ⊢ num_from_oct_list ∘ num_to_oct_list = I
   
   
*)
end

HOL 4, Kananaskis-13