Theory "string_num"

Signature

Definitions

n2nsum_def

⊢ ∀n. n2nsum n = if ODD n then INL (n DIV 2) else INR (n DIV 2)

n2s_primitive_def

⊢ n2s =
  WFREC
    (@R. WF R ∧
         ∀n r0 r.
           n ≠ 0 ∧ (r0 = n MOD 256) ∧ (r = if r0 = 0 then 256 else r0) ⇒
           R ((n − r) DIV 256) n)
    (λn2s a.
         I
           (if a = 0 then ""
            else
              (let
                 r0 = a MOD 256;
                 r = if r0 = 0 then 256 else r0;
                 s0 = n2s ((a − r) DIV 256)
               in
                 STRING (CHR (r − 1)) s0)))

nsum2n_def

⊢ (∀n. nsum2n (INL n) = 2 * n + 1) ∧ ∀n. nsum2n (INR n) = 2 * n

s2n_def

⊢ (s2n "" = 0) ∧ ∀c s. s2n (STRING c s) = s2n s * 256 + ORD c + 1

s2ssum_def

⊢ ∀s. s2ssum s = SUM_MAP n2s n2s (n2nsum (s2n s))

ssum2s_def

⊢ ∀sm. ssum2s sm = n2s (nsum2n (SUM_MAP s2n s2n sm))

Theorems

n2nsum_nsum2n

⊢ n2nsum (nsum2n ns) = ns

n2s_11

⊢ (n2s x = n2s y) ⇔ (x = y)

n2s_def

⊢ ∀n. n2s n =
      if n = 0 then ""
      else
        (let
           r0 = n MOD 256;
           r = if r0 = 0 then 256 else r0;
           s0 = n2s ((n − r) DIV 256)
         in
           STRING (CHR (r − 1)) s0)

n2s_ind

⊢ ∀P. (∀n. (∀r0 r.
              n ≠ 0 ∧ (r0 = n MOD 256) ∧ (r = if r0 = 0 then 256 else r0) ⇒
              P ((n − r) DIV 256)) ⇒
           P n) ⇒
      ∀v. P v

n2s_onto

⊢ ∀s. ∃n. s = n2s n

n2s_s2n

⊢ n2s (s2n s) = s

nsum2n_n2nsum

⊢ nsum2n (n2nsum n) = n

s2n_11

⊢ (s2n x = s2n y) ⇔ (x = y)

s2n_n2s

⊢ ∀n. s2n (n2s n) = n

s2n_onto

⊢ ∀n. ∃s. n = s2n s

s2ssum_ssum2s

⊢ s2ssum (ssum2s sm) = sm

ssum2s_s2ssum

⊢ ssum2s (s2ssum s) = s