Theory "string_num"

Signature

Definitions

ssum2s_def

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

s2ssum_def

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

s2n_def

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

nsum2n_def

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

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

n2nsum_def

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

Theorems

ssum2s_s2ssum

⊢ ssum2s (s2ssum s) = s

s2ssum_ssum2s

⊢ s2ssum (ssum2s sm) = sm

s2n_onto

⊢ ∀n. ∃s. n = s2n s

s2n_n2s

⊢ ∀n. s2n (n2s n) = n

s2n_11

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

nsum2n_n2nsum

⊢ nsum2n (n2nsum n) = n

n2s_s2n

⊢ n2s (s2n s) = s

n2s_onto

⊢ ∀s. ∃n. s = n2s n

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_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_11

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

n2nsum_nsum2n

⊢ n2nsum (nsum2n ns) = ns