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_l2n_2 : thm
val BIT_num_from_bin_list : thm
val BOOLIFY_compute : 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_11 : thm
val l2n_2_thms : thm
val l2n_APPEND : 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 n2lA_10 : thm
val n2lA_def : thm
val n2lA_ind : thm
val n2lA_n2l : thm
val n2l_BOUND : thm
val n2l_def : thm
val n2l_ind : thm
val n2l_l2n : thm
val n2l_n2lA : 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 ∘ REVERSE
[num_from_dec_list_def] Definition
⊢ num_from_dec_list = l2n 10 ∘ REVERSE
[num_from_hex_list_def] Definition
⊢ num_from_hex_list = l2n 16 ∘ REVERSE
[num_from_oct_list_def] Definition
⊢ num_from_oct_list = l2n 8 ∘ REVERSE
[num_to_bin_list_def] Definition
⊢ num_to_bin_list = REVERSE ∘ n2l 2
[num_to_dec_list_def] Definition
⊢ num_to_dec_list = REVERSE ∘ n2l 10
[num_to_hex_list_def] Definition
⊢ num_to_hex_list = REVERSE ∘ n2l 16
[num_to_oct_list_def] Definition
⊢ num_to_oct_list = REVERSE ∘ n2l 8
[BIT_l2n_2] Theorem
⊢ ∀x l.
EVERY ($> 2) l ⇒ (BIT x (l2n 2 l) ⇔ x < LENGTH l ∧ EL x l = 1)
[BIT_num_from_bin_list] Theorem
⊢ ∀x l.
EVERY ($> 2) l ∧ x < LENGTH l ⇒
(BIT x (num_from_bin_list l) ⇔ EL x (REVERSE l) = 1)
[BOOLIFY_compute] Theorem
⊢ (∀m a. BOOLIFY 0 m a = a) ∧
(∀n m a.
BOOLIFY (NUMERAL (BIT1 n)) m a =
BOOLIFY (NUMERAL (BIT1 n) − 1) (DIV2 m) (ODD m::a)) ∧
∀n m a.
BOOLIFY (NUMERAL (BIT2 n)) m a =
BOOLIFY (NUMERAL (BIT1 n)) (DIV2 m) (ODD m::a)
[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 (REVERSE (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_11] Theorem
⊢ ∀b l1 l2.
1 < b ∧ EVERY ($> b) l1 ∧ EVERY ($> b) l2 ⇒
(l2n b (l1 ⧺ [1]) = l2n b (l2 ⧺ [1]) ⇔ l1 = l2)
[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_APPEND] Theorem
⊢ ∀b l1 l2. l2n b (l1 ⧺ l2) = l2n b l1 + b ** LENGTH l1 * l2n b l2
[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 ∘ flip $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)
[n2lA_10] Theorem
⊢ n2lA A f 10 n =
if n < 10 then f n::A else n2lA (f (n MOD 10)::A) f 10 (n DIV 10)
[n2lA_def] Theorem
⊢ ∀n f b A.
n2lA A f b n =
if n < b ∨ b < 2 then f (n MOD b)::A
else n2lA (f (n MOD b)::A) f b (n DIV b)
[n2lA_ind] Theorem
⊢ ∀P. (∀A f b n.
(¬(n < b ∨ b < 2) ⇒ P (f (n MOD b)::A) f b (n DIV b)) ⇒
P A f b n) ⇒
∀v v1 v2 v3. P v v1 v2 v3
[n2lA_n2l] Theorem
⊢ ∀A n. n2lA A f b n = MAP f (REVERSE (n2l b n)) ⧺ A
[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_n2lA] Theorem
⊢ n2l b n = REVERSE (n2lA [] I b n)
[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, Trindemossen-1