Theory string_encoding

⊢ (∀delopt. char_decode delopt "" = NONE) ∧
  ∀delopt c s.
    char_decode delopt (STRING c s) =
    if c = #"\\" then
      case s of
        "" => NONE
      | STRING #"n" stl => SOME (#"\n",stl)
      | STRING #"t" stl => SOME (#"\t",stl)
      | STRING #"\\" stl => SOME (#"\\",stl)
      | STRING c2 stl =>
        if isDigit c2 then
          (let
             d23 = TAKE 2 stl
           in
             if STRLEN d23 = 2 ∧ EVERY isDigit d23 then
               (let
                  n = toNum (STRING c2 d23)
                in
                  if n < 256 then SOME (CHR n,DROP 2 stl) else NONE)
             else NONE)
        else
          case delopt of
            NONE => NONE
          | SOME d => if del_to_char d = c2 then SOME (c2,stl) else NONE
    else if isPrint c then
      case delopt of
        NONE => SOME (c,s)
      | SOME d => if del_to_char d = c then NONE else SOME (c,s)
    else NONE

⊢ ∀delopt c.
    char_encode delopt c =
    if ¬isPrint c then
      if c = #"\n" then "\\n"
      else if c = #"\t" then "\\t"
      else if ORD c < 10 then STRCAT "\\00" (toString (ORD c))
      else if ORD c < 100 then STRCAT "\\0" (toString (ORD c))
      else STRCAT "\\" (toString (ORD c))
    else if c = #"\\" then "\\\\"
    else
      case delopt of
        NONE => STRING c ""
      | SOME d =>
        if c = del_to_char d then STRCAT "\\" (STRING c "")
        else STRING c ""

⊢ del_to_char DQ = #"\"" ∧ del_to_char SQ = #"'" ∧ del_to_char PIPE = #"|"

⊢ (∀a. num2delimiter (delimiter2num a) = a) ∧
  ∀r. (λn. n < 3) r ⇔ delimiter2num (num2delimiter r) = r

⊢ ∀x v0 v1 v2.
    (case x of DQ => v0 | SQ => v1 | PIPE => v2) =
    (λm. if m < 1 then v0 else if m = 1 then v1 else v2) (delimiter2num x)

⊢ ∃rep. TYPE_DEFINITION (λn. n < 3) rep

⊢ ∀x. delimiter_size x = 0

⊢ delopt_to_str NONE = "" ∧
  ∀d. delopt_to_str (SOME d) = STRING (del_to_char d) ""

⊢ ∀delopt s. strencode delopt s = CONCAT (MAP (char_encode delopt) s)

⊢ char_decode delopt (STRCAT (char_encode delopt c) s) = SOME (c,s)

⊢ char_decode delopt s = SOME (c,s') ⇒ STRLEN s' < STRLEN s

⊢ EVERY isPrint (char_encode delopt c)

⊢ DATATYPE (delimiter DQ SQ PIPE)

⊢ ∀a a'. delimiter2num a = delimiter2num a' ⇔ a = a'

⊢ ∀r. r < 3 ⇔ ∃a. r = delimiter2num a

⊢ ∀r. r < 3 ⇔ delimiter2num (num2delimiter r) = r

⊢ delimiter2num DQ = 0 ∧ delimiter2num SQ = 1 ∧ delimiter2num PIPE = 2

⊢ ∀x0 x1 x2. ∃f. f DQ = x0 ∧ f SQ = x1 ∧ f PIPE = x2

⊢ ∀a a'. a = a' ⇔ delimiter2num a = delimiter2num a'

⊢ ∀M M' v0 v1 v2.
    M = M' ∧ (M' = DQ ⇒ v0 = v0') ∧ (M' = SQ ⇒ v1 = v1') ∧
    (M' = PIPE ⇒ v2 = v2') ⇒
    (case M of DQ => v0 | SQ => v1 | PIPE => v2) =
    case M' of DQ => v0' | SQ => v1' | PIPE => v2'

⊢ (∀v0 v1 v2. (case DQ of DQ => v0 | SQ => v1 | PIPE => v2) = v0) ∧
  (∀v0 v1 v2. (case SQ of DQ => v0 | SQ => v1 | PIPE => v2) = v1) ∧
  ∀v0 v1 v2. (case PIPE of DQ => v0 | SQ => v1 | PIPE => v2) = v2

⊢ (case x of DQ => v0 | SQ => v1 | PIPE => v2) = v ⇔
  x = DQ ∧ v0 = v ∨ x = SQ ∧ v1 = v ∨ x = PIPE ∧ v2 = v

⊢ DQ ≠ SQ ∧ DQ ≠ PIPE ∧ SQ ≠ PIPE

⊢ ∀P. P DQ ∧ P PIPE ∧ P SQ ⇒ ∀a. P a

⊢ ∀a. a = DQ ∨ a = SQ ∨ a = PIPE

⊢ ∀r r'. r < 3 ⇒ r' < 3 ⇒ (num2delimiter r = num2delimiter r' ⇔ r = r')

⊢ ∀a. ∃r. a = num2delimiter r ∧ r < 3

⊢ ∀a. num2delimiter (delimiter2num a) = a

⊢ num2delimiter 0 = DQ ∧ num2delimiter 1 = SQ ∧ num2delimiter 2 = PIPE

⊢ ∀s delopt.
    strdecode delopt s =
    case char_decode delopt s of
      NONE =>
        (case (s,delopt) of
           ("",v1) => SOME ("","")
         | (STRING c tl,NONE) => NONE
         | (STRING c tl,SOME d) =>
           if c = del_to_char d then SOME ("",STRING c tl) else NONE)
    | SOME (c,rest) => OPTION_MAP (STRING c ## I) (strdecode delopt rest)

⊢ ∀P. (∀delopt s.
         (∀v2 c rest.
            char_decode delopt s = SOME v2 ∧ v2 = (c,rest) ⇒ P delopt rest) ⇒
         P delopt s) ⇒
      ∀v v1. P v v1

⊢ strdecode delopt (strencode delopt s) = SOME (s,"")

⊢ strdecode delopt (STRCAT (strencode delopt s) (delopt_to_str delopt)) =
  SOME (s,delopt_to_str delopt)

⊢ EVERY isPrint (strencode delopt s)