Theory "string_num"

Signature

Definitions

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

s2n_def

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

n2nsum_def

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

nsum2n_def

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

s2ssum_def

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

ssum2s_def

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

Theorems

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)

s2n_n2s

⊢ ∀n. s2n (n2s n) = n

n2s_s2n

⊢ n2s (s2n s) = s

n2s_11

⊢ n2s x = n2s y ⇔ x = y

s2n_11

⊢ s2n x = s2n y ⇔ x = y

n2s_onto

⊢ ∀s. ∃n. s = n2s n

s2n_onto

⊢ ∀n. ∃s. n = s2n s

n2nsum_nsum2n

⊢ n2nsum (nsum2n ns) = ns

nsum2n_n2nsum

⊢ nsum2n (n2nsum n) = n

s2ssum_ssum2s

⊢ s2ssum (ssum2s sm) = sm

ssum2s_s2ssum

⊢ ssum2s (s2ssum s) = s