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 n.
        I
          (if n = 0 then ""
           else
             (let r0 = n MOD 256 in
              let r = if r0 = 0 then 256 else r0 in
              let s0 = n2s ((n − 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

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 in
        let r = if r0 = 0 then 256 else r0 in
        let 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