Structure cv_primTheory
signature cv_primTheory =
sig
type thm = Thm.thm
(* Definitions *)
val cv_abs_def : thm
val cv_int_add_def : thm
val cv_int_div_def : thm
val cv_int_lt_def : thm
val cv_int_mul_def : thm
val cv_int_neg_def : thm
val cv_max_def : thm
val cv_min_def : thm
val cv_rat_add_def : thm
val cv_rat_lt_def : thm
val cv_rat_mul_def : thm
val cv_rat_neg_def : thm
val cv_rat_norm_def : thm
val cv_rat_reciprocal_def : thm
val cv_word_and_def : thm
val cv_word_lt_def : thm
val cv_word_or_def : thm
val cv_word_sub_def : thm
val cv_word_xor_def : thm
val total_int_div_def : thm
(* Theorems *)
val BITWISE : thm
val BITWISE_ADD : thm
val cv_Num : thm
val cv_chr_thm : thm
val cv_gcd_def : thm
val cv_gcd_ind : thm
val cv_gcd_thm : thm
val cv_inline_imp : thm
val cv_inline_v2n : thm
val cv_inline_v2w : thm
val cv_inline_w2i : thm
val cv_inline_w2v : thm
val cv_inline_word_log2 : thm
val cv_inline_word_ror : thm
val cv_inline_word_sw2sw : thm
val cv_int_add : thm
val cv_int_div : thm
val cv_int_ge : thm
val cv_int_gt : thm
val cv_int_le : thm
val cv_int_lt : thm
val cv_int_mul : thm
val cv_int_of_num : thm
val cv_int_sub : thm
val cv_log2_def : thm
val cv_log2_ind : thm
val cv_max_thm : thm
val cv_min_thm : thm
val cv_neg_int : thm
val cv_ord_thm : thm
val cv_rat_add : thm
val cv_rat_div : thm
val cv_rat_ge : thm
val cv_rat_gt : thm
val cv_rat_le : thm
val cv_rat_lt : thm
val cv_rat_mul : thm
val cv_rat_neg : thm
val cv_rat_norm_div_gcd : thm
val cv_rat_of_int : thm
val cv_rat_reciprocal : thm
val cv_rat_sub : thm
val cv_rep_F : thm
val cv_rep_LOG2 : thm
val cv_rep_T : thm
val cv_rep_add : thm
val cv_rep_and : thm
val cv_rep_arb : thm
val cv_rep_dimindex : thm
val cv_rep_div : thm
val cv_rep_eq : thm
val cv_rep_even : thm
val cv_rep_exp : thm
val cv_rep_if : thm
val cv_rep_le : thm
val cv_rep_let : thm
val cv_rep_lt : thm
val cv_rep_mod : thm
val cv_rep_mul : thm
val cv_rep_not : thm
val cv_rep_num_case : thm
val cv_rep_odd : thm
val cv_rep_or : thm
val cv_rep_sub : thm
val cv_rep_sub1 : thm
val cv_rep_suc : thm
val cv_rep_word_add : thm
val cv_rep_word_and : thm
val cv_rep_word_div : thm
val cv_rep_word_lsl : thm
val cv_rep_word_lsr : thm
val cv_rep_word_mod : thm
val cv_rep_word_msb : thm
val cv_rep_word_mul : thm
val cv_rep_word_n2w : thm
val cv_rep_word_neg : thm
val cv_rep_word_not : thm
val cv_rep_word_or : thm
val cv_rep_word_sub : thm
val cv_rep_word_uint_max : thm
val cv_rep_word_w2n : thm
val cv_rep_word_w2w : thm
val cv_rep_word_xor : thm
val cv_word_and_loop_def : thm
val cv_word_and_loop_ind : thm
val cv_word_and_loop_thm : thm
val cv_word_bit_thm : thm
val cv_word_bits_thm : thm
val cv_word_concat_thm : thm
val cv_word_extract : thm
val cv_word_ge_thm : thm
val cv_word_gt_thm : thm
val cv_word_hi_thm : thm
val cv_word_hs_thm : thm
val cv_word_join_thm : thm
val cv_word_le_thm : thm
val cv_word_lo_thm : thm
val cv_word_ls_thm : thm
val cv_word_lt_thm : thm
val cv_word_or_loop_def : thm
val cv_word_or_loop_ind : thm
val cv_word_or_loop_thm : thm
val cv_word_slice_thm : thm
val cv_word_xor_loop_def : thm
val cv_word_xor_loop_ind : thm
val cv_word_xor_loop_thm : thm
val total_int_div : thm
val v2n_custom_def : thm
val v2n_custom_ind : thm
val v2n_custom_thm : thm
val word_asr_add : thm
val cv_prim_grammars : type_grammar.grammar * term_grammar.grammar
(*
[bitstring] Parent theory of "cv_prim"
[cv_rep] Parent theory of "cv_prim"
[integer_word] Parent theory of "cv_prim"
[cv_abs_def] Definition
⊢ ∀i. cv_abs i = cv_if (cv_ispair i) (cv_fst i) i
[cv_int_add_def] Definition
⊢ ∀i j.
cv_int_add i j =
cv_if (cv_ispair i)
(cv_if (cv_ispair j)
(Pair (cv_add (cv_fst i) (cv_fst j)) (Num 0))
(cv_if (cv_int_lt j (cv_fst i))
(Pair (cv_sub (cv_fst i) j) (Num 0))
(cv_sub j (cv_fst i))))
(cv_if (cv_ispair j)
(cv_if (cv_int_lt i (cv_fst j))
(Pair (cv_sub (cv_fst j) i) (Num 0))
(cv_sub i (cv_fst j))) (cv_add i j))
[cv_int_div_def] Definition
⊢ ∀i j.
cv_int_div i j =
cv_if (cv_eq j (Num 0)) (Num 0)
(cv_if (cv_ispair j)
(cv_if (cv_ispair i) (cv_div (cv_fst i) (cv_fst j))
(cv_int_add (Pair (cv_div i (cv_fst j)) (Num 0))
(cv_if (cv_mod i (cv_fst j)) (Pair (Num 1) (Num 0))
(Num 0))))
(cv_if (cv_ispair i)
(cv_int_add (Pair (cv_div (cv_fst i) j) (Num 0))
(cv_if (cv_mod (cv_fst i) j) (Pair (Num 1) (Num 0))
(Num 0))) (cv_div i j)))
[cv_int_lt_def] Definition
⊢ ∀i j.
cv_int_lt i j =
cv_if (cv_ispair i)
(cv_if (cv_ispair j) (cv_lt (cv_abs j) (cv_abs i)) (Num 1))
(cv_if (cv_ispair j) (Num 0) (cv_lt i j))
[cv_int_mul_def] Definition
⊢ ∀i j.
cv_int_mul i j =
cv_if (cv_eq i (Num 0)) (Num 0)
(cv_if (cv_eq j (Num 0)) (Num 0)
(cv_if (cv_ispair i)
(cv_if (cv_ispair j) (cv_mul (cv_fst i) (cv_fst j))
(Pair (cv_mul (cv_fst i) j) (Num 0)))
(cv_if (cv_ispair j) (Pair (cv_mul i (cv_fst j)) (Num 0))
(cv_mul i j))))
[cv_int_neg_def] Definition
⊢ ∀x. cv_int_neg x =
cv_if (cv_eq x (Num 0)) x
(cv_if (cv_ispair x) (cv_fst x) (Pair x (Num 0)))
[cv_max_def] Definition
⊢ ∀x y. cv_max x y = cv_if (cv_lt x y) y x
[cv_min_def] Definition
⊢ ∀x y. cv_min x y = cv_if (cv_lt x y) x y
[cv_rat_add_def] Definition
⊢ ∀r1 r2.
cv_rat_add r1 r2 =
cv_rat_norm
(Pair
(cv_int_add (cv_int_mul (cv_fst r1) (cv_snd r2))
(cv_int_mul (cv_fst r2) (cv_snd r1)))
(cv_mul (cv_snd r1) (cv_snd r2)))
[cv_rat_lt_def] Definition
⊢ ∀r1 r2.
cv_rat_lt r1 r2 =
cv_int_lt (cv_int_mul (cv_fst r1) (cv_snd r2))
(cv_int_mul (cv_fst r2) (cv_snd r1))
[cv_rat_mul_def] Definition
⊢ ∀r1 r2.
cv_rat_mul r1 r2 =
cv_rat_norm
(Pair (cv_int_mul (cv_fst r1) (cv_fst r2))
(cv_mul (cv_snd r1) (cv_snd r2)))
[cv_rat_neg_def] Definition
⊢ ∀r. cv_rat_neg r = Pair (cv_int_neg (cv_fst r)) (cv_snd r)
[cv_rat_norm_def] Definition
⊢ ∀r. cv_rat_norm r =
(let
d = cv_gcd (cv_abs (cv_fst r)) (cv_snd r)
in
cv_if (cv_lt d (Num 2)) r
(Pair (cv_int_div (cv_fst r) d) (cv_div (cv_snd r) d)))
[cv_rat_reciprocal_def] Definition
⊢ ∀r. cv_rat_reciprocal r =
cv_if (cv_int_lt (cv_fst r) (Num 0))
(Pair (Pair (cv_snd r) (Num 0)) (cv_fst (cv_fst r)))
(Pair (cv_snd r) (cv_fst r))
[cv_word_and_def] Definition
⊢ ∀x y.
cv_word_and x y =
cv_if (cv_lt x y) (cv_word_and_loop x y) (cv_word_and_loop y x)
[cv_word_lt_def] Definition
⊢ ∀w1 w2 msb1 msb2.
cv_word_lt w1 w2 msb1 msb2 =
cv_if (cv_eq msb1 msb2) (cv_lt w1 w2)
(cv_if msb1 (Num 1) (cv_sub (Num 1) msb2))
[cv_word_or_def] Definition
⊢ ∀x y.
cv_word_or x y =
cv_if (cv_lt x y) (cv_word_or_loop x y) (cv_word_or_loop y x)
[cv_word_sub_def] Definition
⊢ ∀x y d.
cv_word_sub x y d =
cv_if (cv_lt x y) (cv_sub (cv_add x d) y) (cv_sub x y)
[cv_word_xor_def] Definition
⊢ ∀x y.
cv_word_xor x y =
cv_if (cv_lt x y) (cv_word_xor_loop x y) (cv_word_xor_loop y x)
[total_int_div_def] Definition
⊢ ∀i j. total_int_div i j = if j = 0 then 0 else i / j
[BITWISE] Theorem
⊢ BITWISE 0 b m n = 0 ∧
BITWISE (SUC k) b m n =
(if b (ODD m) (ODD n) then 1 else 0) +
2 * BITWISE k b (m DIV 2) (n DIV 2)
[BITWISE_ADD] Theorem
⊢ ∀l k m n b.
BITWISE (l + k) b m n =
BITWISE l b m n +
BITWISE k b (m DIV 2 ** l) (n DIV 2 ** l) * 2 ** l
[cv_Num] Theorem
⊢ Num (Num i) = cv_abs (from_int i)
[cv_chr_thm] Theorem
⊢ n < 256 ⇒ from_char (CHR n) = Num n
[cv_gcd_def] Theorem
⊢ ∀b a. cv_gcd a b = cv_if a (cv_gcd (cv_mod b a) a) b
[cv_gcd_ind] Theorem
⊢ ∀P. (∀a b. (c2b a ⇒ P (cv_mod b a) a) ⇒ P a b) ⇒ ∀v v1. P v v1
[cv_gcd_thm] Theorem
⊢ Num (gcd a b) = cv_gcd (Num a) (Num b)
[cv_inline_imp] Theorem
⊢ b2c (a ⇒ b) = cv_if (b2c a) (b2c b) (Num 1)
[cv_inline_v2n] Theorem
⊢ v2n = v2n_custom 0
[cv_inline_v2w] Theorem
⊢ ∀v. v2w v = n2w (v2n_custom 0 v)
[cv_inline_w2i] Theorem
⊢ w2i w = (let v = w in if word_msb v then -&w2n (-v) else &w2n v)
[cv_inline_w2v] Theorem
⊢ w2v w =
(let d = dimindex (:α) in GENLIST (λi. word_bit (d − 1 − i) w) d)
[cv_inline_word_log2] Theorem
⊢ ∀w. word_log2 w = n2w (LOG2 (w2n w))
[cv_inline_word_ror] Theorem
⊢ ∀r a.
a ⇄ r =
(let
a = a;
d = dimindex (:α);
r = r MOD d
in
a ≪ (d − r) ‖ a ⋙ r)
[cv_inline_word_sw2sw] Theorem
⊢ sw2sw w =
(let
v = w
in
(if word_msb v then -1w ≪ dimindex (:α) else 0w) + w2w v)
[cv_int_add] Theorem
⊢ from_int (i + j) = cv_int_add (from_int i) (from_int j)
[cv_int_div] Theorem
⊢ from_int (total_int_div i j) = cv_int_div (from_int i) (from_int j)
[cv_int_ge] Theorem
⊢ b2c (i ≥ j) =
cv_if (cv_int_lt (from_int i) (from_int j)) (Num 0) (Num 1)
[cv_int_gt] Theorem
⊢ b2c (i > j) = cv_int_lt (from_int j) (from_int i)
[cv_int_le] Theorem
⊢ b2c (i ≤ j) =
cv_if (cv_int_lt (from_int j) (from_int i)) (Num 0) (Num 1)
[cv_int_lt] Theorem
⊢ b2c (i < j) = cv_int_lt (from_int i) (from_int j)
[cv_int_mul] Theorem
⊢ from_int (i * j) = cv_int_mul (from_int i) (from_int j)
[cv_int_of_num] Theorem
⊢ from_int (&n) = Num n
[cv_int_sub] Theorem
⊢ from_int (i − j) =
cv_int_add (from_int i) (cv_int_neg (from_int j))
[cv_log2_def] Theorem
⊢ ∀n acc.
cv_log2 acc n =
cv_if (cv_lt (Num 1) n)
(cv_log2 (cv_add acc (Num 1)) (cv_div n (Num 2))) acc
[cv_log2_ind] Theorem
⊢ ∀P. (∀acc n.
(c2b (cv_lt (Num 1) n) ⇒
P (cv_add acc (Num 1)) (cv_div n (Num 2))) ⇒
P acc n) ⇒
∀v v1. P v v1
[cv_max_thm] Theorem
⊢ Num (MAX m n) = cv_max (Num m) (Num n)
[cv_min_thm] Theorem
⊢ Num (MIN m n) = cv_min (Num m) (Num n)
[cv_neg_int] Theorem
⊢ from_int (-x) = cv_int_neg (from_int x)
[cv_ord_thm] Theorem
⊢ Num (ORD c) = from_char c
[cv_rat_add] Theorem
⊢ from_rat (r1 + r2) = cv_rat_add (from_rat r1) (from_rat r2)
[cv_rat_div] Theorem
⊢ r2 ≠ 0 ⇒
from_rat (r1 / r2) =
cv_rat_mul (from_rat r1) (cv_rat_reciprocal (from_rat r2))
[cv_rat_ge] Theorem
⊢ b2c (r1 ≥ r2) =
cv_if (cv_rat_lt (from_rat r1) (from_rat r2)) (Num 0) (Num 1)
[cv_rat_gt] Theorem
⊢ b2c (r1 > r2) = cv_rat_lt (from_rat r2) (from_rat r1)
[cv_rat_le] Theorem
⊢ b2c (r1 ≤ r2) =
cv_if (cv_rat_lt (from_rat r2) (from_rat r1)) (Num 0) (Num 1)
[cv_rat_lt] Theorem
⊢ b2c (r1 < r2) = cv_rat_lt (from_rat r1) (from_rat r2)
[cv_rat_mul] Theorem
⊢ from_rat (r1 * r2) = cv_rat_mul (from_rat r1) (from_rat r2)
[cv_rat_neg] Theorem
⊢ from_rat (-r) = cv_rat_neg (from_rat r)
[cv_rat_norm_div_gcd] Theorem
⊢ (λ(x,y). Pair (from_int x) (Num y)) (div_gcd a b) =
cv_rat_norm (Pair (from_int a) (Num b))
[cv_rat_of_int] Theorem
⊢ from_rat (rat_of_int i) = Pair (from_int i) (Num 1)
[cv_rat_reciprocal] Theorem
⊢ r ≠ 0 ⇒ from_rat (rat_minv r) = cv_rat_reciprocal (from_rat r)
[cv_rat_sub] Theorem
⊢ from_rat (r1 − r2) =
cv_rat_add (from_rat r1) (cv_rat_neg (from_rat r2))
[cv_rep_F] Theorem
⊢ b2c F = Num 0
[cv_rep_LOG2] Theorem
⊢ n ≠ 0 ⇒ Num (LOG2 n) = cv_log2 (Num 0) (Num n)
[cv_rep_T] Theorem
⊢ b2c T = Num 1
[cv_rep_add] Theorem
⊢ Num (n + m) = cv_add (Num n) (Num m)
[cv_rep_and] Theorem
⊢ b2c (b1 ∧ b2) = cv_if (b2c b1) (b2c b2) (Num 0)
[cv_rep_arb] Theorem
⊢ F ⇒ f ARB = Num 0
[cv_rep_dimindex] Theorem
⊢ Num (dimindex (:α)) = Num (dimindex (:α))
[cv_rep_div] Theorem
⊢ Num (n DIV m) = cv_div (Num n) (Num m)
[cv_rep_eq] Theorem
⊢ cv_rep p1 c1 f x ∧ cv_rep p2 c2 f y ∧ from_to f t ⇒
cv_rep (p1 ∧ p2) (cv_eq c1 c2) b2c (x = y)
[cv_rep_even] Theorem
⊢ b2c (EVEN n) = cv_sub (Num 1) (cv_mod (Num n) (Num 2))
[cv_rep_exp] Theorem
⊢ Num (n ** m) = cv_exp (Num n) (Num m)
[cv_rep_if] Theorem
⊢ cv_rep p1 c1 b2c b ∧ cv_rep p2 c2 f t ∧ cv_rep p3 c3 f e ⇒
cv_rep (p1 ∧ (b ⇒ p2) ∧ (¬b ⇒ p3)) (cv_if c1 c2 c3) f
(if b then t else e)
[cv_rep_le] Theorem
⊢ b2c (n ≤ m) = cv_sub (Num 1) (cv_lt (Num m) (Num n))
[cv_rep_let] Theorem
⊢ cv_rep p1 c1 a x ∧ (∀v. cv_rep (p2 v) (c2 (a v)) b (y v)) ⇒
cv_rep (p1 ∧ ∀v. v = x ⇒ p2 v) (LET c2 c1) b (LET y x)
[cv_rep_lt] Theorem
⊢ b2c (n < m) = cv_lt (Num n) (Num m)
[cv_rep_mod] Theorem
⊢ Num (n MOD m) = cv_mod (Num n) (Num m)
[cv_rep_mul] Theorem
⊢ Num (n * m) = cv_mul (Num n) (Num m)
[cv_rep_not] Theorem
⊢ b2c (¬b1) = cv_sub (Num 1) (b2c b1)
[cv_rep_num_case] Theorem
⊢ cv_rep p1 c1 Num x ∧ cv_rep p2 c2 a y ∧
(∀v. cv_rep (p3 v) (c3 (Num v)) a (z v)) ⇒
cv_rep (p1 ∧ (x = 0 ⇒ p2) ∧ ∀n. x = SUC n ⇒ p3 n)
(cv_if (cv_lt (Num 0) c1) (let y = cv_sub c1 (Num 1) in c3 y) c2)
a (num_CASE x y z)
[cv_rep_odd] Theorem
⊢ b2c (ODD n) = cv_mod (Num n) (Num 2)
[cv_rep_or] Theorem
⊢ b2c (b1 ∨ b2) = cv_if (b2c b1) (Num 1) (b2c b2)
[cv_rep_sub] Theorem
⊢ Num (n − m) = cv_sub (Num n) (Num m)
[cv_rep_sub1] Theorem
⊢ Num (PRE n) = cv_sub (Num n) (Num 1)
[cv_rep_suc] Theorem
⊢ Num (SUC n) = cv_add (Num n) (Num 1)
[cv_rep_word_add] Theorem
⊢ from_word (w1 + w2) =
cv_mod (cv_add (from_word w1) (from_word w2)) (Num (dimword (:α)))
[cv_rep_word_and] Theorem
⊢ from_word (w1 && w2) = cv_word_and (from_word w1) (from_word w2)
[cv_rep_word_div] Theorem
⊢ from_word (w1 // w2) = cv_div (from_word w1) (from_word w2)
[cv_rep_word_lsl] Theorem
⊢ from_word (w ≪ n) =
cv_mod (cv_mul (from_word w) (cv_exp (Num 2) (Num n)))
(Num (2 ** dimindex (:α)))
[cv_rep_word_lsr] Theorem
⊢ from_word (w ⋙ n) = cv_div (from_word w) (cv_exp (Num 2) (Num n))
[cv_rep_word_mod] Theorem
⊢ from_word (word_mod w1 w2) = cv_mod (from_word w1) (from_word w2)
[cv_rep_word_msb] Theorem
⊢ b2c (word_msb w) =
cv_div (from_word w) (Num (2 ** (dimindex (:α) − 1)))
[cv_rep_word_mul] Theorem
⊢ from_word (w1 * w2) =
cv_mod (cv_mul (from_word w1) (from_word w2)) (Num (dimword (:α)))
[cv_rep_word_n2w] Theorem
⊢ from_word (n2w n) = cv_mod (Num n) (Num (2 ** dimindex (:α)))
[cv_rep_word_neg] Theorem
⊢ from_word (-w1) =
cv_word_sub (Num 0) (from_word w1) (Num (dimword (:α)))
[cv_rep_word_not] Theorem
⊢ from_word (¬w) =
cv_word_xor (from_word w) (Num (2 ** dimindex (:α) − 1))
[cv_rep_word_or] Theorem
⊢ from_word (w1 ‖ w2) = cv_word_or (from_word w1) (from_word w2)
[cv_rep_word_sub] Theorem
⊢ from_word (w1 − w2) =
cv_word_sub (from_word w1) (from_word w2) (Num (dimword (:α)))
[cv_rep_word_uint_max] Theorem
⊢ from_word UINT_MAXw = Num (2 ** dimindex (:α) − 1)
[cv_rep_word_w2n] Theorem
⊢ Num (w2n w) = from_word w
[cv_rep_word_w2w] Theorem
⊢ from_word (w2w w) =
if dimindex (:α) ≤ dimindex (:β) then from_word w
else cv_mod (from_word w) (Num (2 ** dimindex (:β)))
[cv_rep_word_xor] Theorem
⊢ from_word (w1 ⊕ w2) = cv_word_xor (from_word w1) (from_word w2)
[cv_word_and_loop_def] Theorem
⊢ ∀y x.
cv_word_and_loop x y =
cv_if (cv_lt (Num 0) x)
(cv_add
(cv_mul (Num 2)
(cv_word_and_loop (cv_div x (Num 2)) (cv_div y (Num 2))))
(cv_div (cv_add (cv_mod x (Num 2)) (cv_mod y (Num 2)))
(Num 2))) (Num 0)
[cv_word_and_loop_ind] Theorem
⊢ ∀P. (∀x y.
(c2b (cv_lt (Num 0) x) ⇒
P (cv_div x (Num 2)) (cv_div y (Num 2))) ⇒
P x y) ⇒
∀v v1. P v v1
[cv_word_and_loop_thm] Theorem
⊢ ∀m n.
m ≤ n ∧ n < dimword (:α) ⇒
cv_word_and_loop (Num m) (Num n) = Num (w2n (n2w m && n2w n))
[cv_word_bit_thm] Theorem
⊢ b2c (word_bit b w) =
cv_mod (cv_div (from_word w) (cv_exp (Num 2) (Num b))) (Num 2)
[cv_word_bits_thm] Theorem
⊢ from_word ((h -- l) w) =
cv_div
(cv_mod (from_word w)
(cv_exp (Num 2)
(cv_min (cv_add (Num h) (Num 1)) (Num (dimindex (:α))))))
(cv_exp (Num 2) (Num l))
[cv_word_concat_thm] Theorem
⊢ FINITE 𝕌(:α) ∧ FINITE 𝕌(:β) ⇒
from_word (w1 @@ w2) =
if dimindex (:α) + dimindex (:β) ≤ dimindex (:γ) then
cv_add
(cv_mul (from_word w1) (cv_exp (Num 2) (Num (dimindex (:β)))))
(from_word w2)
else
cv_mod
(cv_add
(cv_mul (from_word w1)
(cv_exp (Num 2) (Num (dimindex (:β))))) (from_word w2))
(Num (2 ** dimindex (:γ)))
[cv_word_extract] Theorem
⊢ from_word ((h >< l) w) =
if dimindex (:α) ≤ dimindex (:β) then
cv_div
(cv_mod (from_word w)
(cv_exp (Num 2)
(cv_min (cv_add (Num h) (Num 1)) (Num (dimindex (:α))))))
(cv_exp (Num 2) (Num l))
else
cv_mod
(cv_div
(cv_mod (from_word w)
(cv_exp (Num 2)
(cv_min (cv_add (Num h) (Num 1)) (Num (dimindex (:α))))))
(cv_exp (Num 2) (Num l))) (Num (2 ** dimindex (:β)))
[cv_word_ge_thm] Theorem
⊢ b2c (w1 ≥ w2) =
cv_sub (Num 1)
(cv_word_lt (from_word w1) (from_word w2)
(cv_div (from_word w1) (Num (2 ** (dimindex (:α) − 1))))
(cv_div (from_word w2) (Num (2 ** (dimindex (:α) − 1)))))
[cv_word_gt_thm] Theorem
⊢ b2c (w2 > w1) =
cv_word_lt (from_word w1) (from_word w2)
(cv_div (from_word w1) (Num (2 ** (dimindex (:α) − 1))))
(cv_div (from_word w2) (Num (2 ** (dimindex (:α) − 1))))
[cv_word_hi_thm] Theorem
⊢ b2c (w2 >₊ w1) = cv_lt (from_word w1) (from_word w2)
[cv_word_hs_thm] Theorem
⊢ b2c (w1 ≥₊ w2) =
cv_sub (Num 1) (cv_lt (from_word w1) (from_word w2))
[cv_word_join_thm] Theorem
⊢ FINITE 𝕌(:α) ∧ FINITE 𝕌(:β) ⇒
from_word (word_join w1 w2) =
cv_add
(cv_mul (from_word w1) (cv_exp (Num 2) (Num (dimindex (:β)))))
(from_word w2)
[cv_word_le_thm] Theorem
⊢ b2c (w2 ≤ w1) =
cv_sub (Num 1)
(cv_word_lt (from_word w1) (from_word w2)
(cv_div (from_word w1) (Num (2 ** (dimindex (:α) − 1))))
(cv_div (from_word w2) (Num (2 ** (dimindex (:α) − 1)))))
[cv_word_lo_thm] Theorem
⊢ b2c (w1 <₊ w2) = cv_lt (from_word w1) (from_word w2)
[cv_word_ls_thm] Theorem
⊢ b2c (w1 ≤₊ w2) =
cv_sub (Num 1) (cv_lt (from_word w2) (from_word w1))
[cv_word_lt_thm] Theorem
⊢ b2c (w1 < w2) =
cv_word_lt (from_word w1) (from_word w2)
(cv_div (from_word w1) (Num (2 ** (dimindex (:α) − 1))))
(cv_div (from_word w2) (Num (2 ** (dimindex (:α) − 1))))
[cv_word_or_loop_def] Theorem
⊢ ∀y x.
cv_word_or_loop x y =
cv_if (cv_lt (Num 0) x)
(cv_add
(cv_mul (Num 2)
(cv_word_or_loop (cv_div x (Num 2)) (cv_div y (Num 2))))
(cv_max (cv_mod x (Num 2)) (cv_mod y (Num 2)))) y
[cv_word_or_loop_ind] Theorem
⊢ ∀P. (∀x y.
(c2b (cv_lt (Num 0) x) ⇒
P (cv_div x (Num 2)) (cv_div y (Num 2))) ⇒
P x y) ⇒
∀v v1. P v v1
[cv_word_or_loop_thm] Theorem
⊢ ∀m n.
m ≤ n ∧ n < dimword (:α) ⇒
cv_word_or_loop (Num m) (Num n) = Num (w2n (n2w m ‖ n2w n))
[cv_word_slice_thm] Theorem
⊢ from_word ((h '' l) w) =
cv_mod
(cv_mul
(cv_div
(cv_mod (from_word w)
(cv_exp (Num 2)
(cv_min (cv_add (Num h) (Num 1))
(Num (dimindex (:α)))))) (cv_exp (Num 2) (Num l)))
(cv_exp (Num 2) (Num l))) (Num (dimword (:α)))
[cv_word_xor_loop_def] Theorem
⊢ ∀y x.
cv_word_xor_loop x y =
cv_if (cv_lt (Num 0) x)
(cv_add
(cv_mul (Num 2)
(cv_word_xor_loop (cv_div x (Num 2)) (cv_div y (Num 2))))
(cv_mod (cv_add (cv_mod x (Num 2)) (cv_mod y (Num 2)))
(Num 2))) y
[cv_word_xor_loop_ind] Theorem
⊢ ∀P. (∀x y.
(c2b (cv_lt (Num 0) x) ⇒
P (cv_div x (Num 2)) (cv_div y (Num 2))) ⇒
P x y) ⇒
∀v v1. P v v1
[cv_word_xor_loop_thm] Theorem
⊢ ∀m n.
m ≤ n ∧ n < dimword (:α) ⇒
cv_word_xor_loop (Num m) (Num n) = Num (w2n (n2w m ⊕ n2w n))
[total_int_div] Theorem
⊢ total_int_div i j =
if j = 0 then 0
else if j < 0 then
if i < 0 then &(Num i DIV Num j)
else -&(Num i DIV Num j) + if Num i MOD Num j = 0 then 0 else -1
else if i < 0 then
-&(Num i DIV Num j) + if Num i MOD Num j = 0 then 0 else -1
else &(Num i DIV Num j)
[v2n_custom_def] Theorem
⊢ (∀acc. v2n_custom acc [] = acc) ∧
(∀rest acc.
v2n_custom acc (T::rest) = v2n_custom (2 * acc + 1) rest) ∧
∀rest acc. v2n_custom acc (F::rest) = v2n_custom (2 * acc) rest
[v2n_custom_ind] Theorem
⊢ ∀P. (∀acc. P acc []) ∧
(∀acc rest. P (2 * acc + 1) rest ⇒ P acc (T::rest)) ∧
(∀acc rest. P (2 * acc) rest ⇒ P acc (F::rest)) ⇒
∀v v1. P v v1
[v2n_custom_thm] Theorem
⊢ v2n_custom 0 = v2n
[word_asr_add] Theorem
⊢ w ≫ n =
(let
x = w
in
if word_msb x then
(dimindex (:α) − 1 '' dimindex (:α) − n) UINT_MAXw + x ⋙ n
else x ⋙ n)
*)
end
HOL 4, Trindemossen-1