Theory cv_prim

⊢ ∀i. cv_abs i = cv_if (cv_ispair i) (cv_fst i) i

⊢ ∀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))

⊢ ∀i j.
    cv_int_div i j =
    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))

⊢ ∀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))

⊢ ∀i j.
    cv_int_mod i j =
    cv_int_add i (cv_int_neg (cv_int_mul (cv_int_div i j) j))

⊢ ∀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))))

⊢ ∀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)))

⊢ ∀x y. cv_max x y = cv_if (cv_lt x y) y x

⊢ ∀x y. cv_min x y = cv_if (cv_lt x y) x y

⊢ ∀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)))

⊢ ∀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))

⊢ ∀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)))

⊢ ∀r. cv_rat_neg r = Pair (cv_int_neg (cv_fst r)) (cv_snd r)

⊢ ∀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_total_int_div (cv_fst r) d) (cv_div (cv_snd r) d)))

⊢ ∀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))

⊢ ∀i j.
    cv_total_int_div i j = cv_if (cv_eq j (Num 0)) (Num 0) (cv_int_div i j)

⊢ ∀i j. cv_total_int_mod i j = cv_if (cv_eq j (Num 0)) i (cv_int_mod i j)

⊢ ∀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)

⊢ ∀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))

⊢ ∀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)

⊢ ∀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)

⊢ ∀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)

⊢ ∀i j. total_int_div i j = if j = 0 then 0 else i / j

⊢ ∀i j. total_int_mod i j = if j = 0 then i else i % j

⊢ 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)

⊢ ∀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

⊢ Num (Num i) = cv_abs (from_int i)

⊢ n < 256 ⇒ from_char (CHR n) = Num n

⊢ ∀b a. cv_gcd a b = cv_if a (cv_gcd (cv_mod b a) a) b

⊢ ∀P. (∀a b. (c2b a ⇒ P (cv_mod b a) a) ⇒ P a b) ⇒ ∀v v1. P v v1

⊢ Num (gcd a b) = cv_gcd (Num a) (Num b)

⊢ b2c (a ⇒ b) = cv_if (b2c a) (b2c b) (Num 1)

⊢ v2n = v2n_custom 0

⊢ ∀v. v2w v = n2w (v2n_custom 0 v)

⊢ w2i w = (let v = w in if word_msb v then -&w2n (-v) else &w2n v)

⊢ w2v w = (let d = dimindex (:α) in GENLIST (λi. word_bit (d − 1 − i) w) d)

⊢ ∀w. word_log2 w = n2w (LOG2 (w2n w))

⊢ ∀r a.
    a ⇄ r =
    (let a = a; d = dimindex (:α); r = r MOD d in a ≪ (d − r) ‖ a ⋙ r)

⊢ sw2sw w =
  (let v = w in (if word_msb v then -1w ≪ dimindex (:α) else 0w) + w2w v)

⊢ from_int (i + j) = cv_int_add (from_int i) (from_int j)

⊢ j ≠ 0 ⇒ from_int (i / j) = cv_int_div (from_int i) (from_int j)

⊢ b2c (i ≥ j) = cv_if (cv_int_lt (from_int i) (from_int j)) (Num 0) (Num 1)

⊢ b2c (i > j) = cv_int_lt (from_int j) (from_int i)

⊢ b2c (i ≤ j) = cv_if (cv_int_lt (from_int j) (from_int i)) (Num 0) (Num 1)

⊢ b2c (i < j) = cv_int_lt (from_int i) (from_int j)

⊢ j ≠ 0 ⇒ from_int (i % j) = cv_int_mod (from_int i) (from_int j)

⊢ from_int (i * j) = cv_int_mul (from_int i) (from_int j)

⊢ from_int (&n) = Num n

⊢ from_int (i − j) = cv_int_add (from_int i) (cv_int_neg (from_int j))

⊢ ∀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

⊢ ∀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

⊢ Num (MAX m n) = cv_max (Num m) (Num n)

⊢ Num (MIN m n) = cv_min (Num m) (Num n)

⊢ from_int (-x) = cv_int_neg (from_int x)

⊢ Num (ORD c) = from_char c

⊢ from_rat (r1 + r2) = cv_rat_add (from_rat r1) (from_rat r2)

⊢ r2 ≠ 0 ⇒
  from_rat (r1 / r2) =
  cv_rat_mul (from_rat r1) (cv_rat_reciprocal (from_rat r2))

⊢ b2c (r1 ≥ r2) =
  cv_if (cv_rat_lt (from_rat r1) (from_rat r2)) (Num 0) (Num 1)

⊢ b2c (r1 > r2) = cv_rat_lt (from_rat r2) (from_rat r1)

⊢ b2c (r1 ≤ r2) =
  cv_if (cv_rat_lt (from_rat r2) (from_rat r1)) (Num 0) (Num 1)

⊢ b2c (r1 < r2) = cv_rat_lt (from_rat r1) (from_rat r2)

⊢ from_rat (r1 * r2) = cv_rat_mul (from_rat r1) (from_rat r2)

⊢ from_rat (-r) = cv_rat_neg (from_rat r)

⊢ (λ(x,y). Pair (from_int x) (Num y)) (div_gcd a b) =
  cv_rat_norm (Pair (from_int a) (Num b))

⊢ from_rat (rat_of_int i) = Pair (from_int i) (Num 1)

⊢ r ≠ 0 ⇒ from_rat (rat_minv r) = cv_rat_reciprocal (from_rat r)

⊢ from_rat (r1 − r2) = cv_rat_add (from_rat r1) (cv_rat_neg (from_rat r2))

⊢ b2c F = Num 0

⊢ n ≠ 0 ⇒ Num (LOG2 n) = cv_log2 (Num 0) (Num n)

⊢ b2c T = Num 1

⊢ Num (n + m) = cv_add (Num n) (Num m)

⊢ b2c (b1 ∧ b2) = cv_if (b2c b1) (b2c b2) (Num 0)

⊢ F ⇒ f ARB = Num 0

⊢ b2c (char_ge n m) = cv_sub (Num 1) (cv_lt (from_char n) (from_char m))

⊢ b2c (char_gt n m) = cv_lt (from_char m) (from_char n)

⊢ b2c (char_le n m) = cv_sub (Num 1) (cv_lt (from_char m) (from_char n))

⊢ b2c (char_lt n m) = cv_lt (from_char n) (from_char m)

⊢ Num (dimindex (:α)) = Num (dimindex (:α))

⊢ Num (n DIV m) = cv_div (Num n) (Num m)

⊢ 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)

⊢ b2c (EVEN n) = cv_sub (Num 1) (cv_mod (Num n) (Num 2))

⊢ Num (n ** m) = cv_exp (Num n) (Num m)

⊢ b2c (n ≥ m) = cv_sub (Num 1) (cv_lt (Num n) (Num m))

⊢ b2c (n > m) = cv_lt (Num m) (Num n)

⊢ 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)

⊢ b2c (n ≤ m) = cv_sub (Num 1) (cv_lt (Num m) (Num n))

⊢ 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)

⊢ b2c (n < m) = cv_lt (Num n) (Num m)

⊢ Num (n MOD m) = cv_mod (Num n) (Num m)

⊢ Num (n * m) = cv_mul (Num n) (Num m)

⊢ b2c (¬b1) = cv_sub (Num 1) (b2c b1)

⊢ 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)

⊢ b2c (ODD n) = cv_mod (Num n) (Num 2)

⊢ b2c (b1 ∨ b2) = cv_if (b2c b1) (Num 1) (b2c b2)

⊢ Num (n − m) = cv_sub (Num n) (Num m)

⊢ Num (PRE n) = cv_sub (Num n) (Num 1)

⊢ Num (SUC n) = cv_add (Num n) (Num 1)

⊢ from_word (w1 + w2) =
  cv_mod (cv_add (from_word w1) (from_word w2)) (Num (dimword (:α)))

⊢ from_word (w1 && w2) = cv_word_and (from_word w1) (from_word w2)

⊢ from_word (w1 // w2) = cv_div (from_word w1) (from_word w2)

⊢ from_word (w ≪ n) =
  cv_mod (cv_mul (from_word w) (cv_exp (Num 2) (Num n)))
    (Num (2 ** dimindex (:α)))

⊢ from_word (w ⋙ n) =
  (let
     k = Num n
   in
     cv_if (cv_lt k (Num (dimindex (:α))))
       (cv_div (from_word w) (cv_exp (Num 2) k)) (Num 0))

⊢ from_word (word_mod w1 w2) = cv_mod (from_word w1) (from_word w2)

⊢ b2c (word_msb w) = cv_div (from_word w) (Num (2 ** (dimindex (:α) − 1)))

⊢ from_word (w1 * w2) =
  cv_mod (cv_mul (from_word w1) (from_word w2)) (Num (dimword (:α)))

⊢ from_word (n2w n) = cv_mod (Num n) (Num (2 ** dimindex (:α)))

⊢ from_word (-w1) = cv_word_sub (Num 0) (from_word w1) (Num (dimword (:α)))

⊢ from_word (¬w) = cv_word_xor (from_word w) (Num (2 ** dimindex (:α) − 1))

⊢ from_word (w1 ‖ w2) = cv_word_or (from_word w1) (from_word w2)

⊢ from_word (w1 − w2) =
  cv_word_sub (from_word w1) (from_word w2) (Num (dimword (:α)))

⊢ from_word UINT_MAXw = Num (2 ** dimindex (:α) − 1)

⊢ Num (w2n w) = from_word w

⊢ from_word (w2w w) =
  if dimindex (:α) ≤ dimindex (:β) then from_word w
  else cv_mod (from_word w) (Num (2 ** dimindex (:β)))

⊢ from_word (w1 ⊕ w2) = cv_word_xor (from_word w1) (from_word w2)

⊢ from_int (total_int_div i j) = cv_total_int_div (from_int i) (from_int j)

⊢ from_int (total_int_mod i j) = cv_total_int_mod (from_int i) (from_int j)

⊢ ∀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)

⊢ ∀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

⊢ ∀m n.
    m ≤ n ∧ n < dimword (:α) ⇒
    cv_word_and_loop (Num m) (Num n) = Num (w2n (n2w m && n2w n))

⊢ b2c (word_bit b w) =
  cv_mod (cv_div (from_word w) (cv_exp (Num 2) (Num b))) (Num 2)

⊢ 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))

⊢ 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 (:γ)))

⊢ 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 (:β)))

⊢ 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)))))

⊢ 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))))

⊢ b2c (w2 >₊ w1) = cv_lt (from_word w1) (from_word w2)

⊢ b2c (w1 ≥₊ w2) = cv_sub (Num 1) (cv_lt (from_word w1) (from_word w2))

⊢ FINITE 𝕌(:α) ∧ FINITE 𝕌(:β) ⇒
  from_word (word_join w1 w2) =
  cv_add (cv_mul (from_word w1) (cv_exp (Num 2) (Num (dimindex (:β)))))
    (from_word w2)

⊢ 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)))))

⊢ b2c (w1 <₊ w2) = cv_lt (from_word w1) (from_word w2)

⊢ b2c (w1 ≤₊ w2) = cv_sub (Num 1) (cv_lt (from_word w2) (from_word w1))

⊢ 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))))

⊢ ∀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

⊢ ∀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

⊢ ∀m n.
    m ≤ n ∧ n < dimword (:α) ⇒
    cv_word_or_loop (Num m) (Num n) = Num (w2n (n2w m ‖ n2w n))

⊢ 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 (:α)))

⊢ ∀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

⊢ ∀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

⊢ ∀m n.
    m ≤ n ∧ n < dimword (:α) ⇒
    cv_word_xor_loop (Num m) (Num n) = Num (w2n (n2w m ⊕ n2w n))

⊢ (∀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

⊢ ∀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 0 = v2n

⊢ w ≫ n =
  (let
     x = w
   in
     if word_msb x then
       (dimindex (:α) − 1 '' dimindex (:α) − n) UINT_MAXw + x ⋙ n
     else x ⋙ n)