Theory string

⊢ DEST_STRING "" = NONE ∧ ∀c rst. DEST_STRING (STRING c rst) = SOME (c,rst)

⊢ EXPLODE "" = "" ∧ ∀c s. EXPLODE (STRING c s) = STRING c (EXPLODE s)

⊢ EXTRACT =
  WFREC (@R. WF R)
    (λEXTRACT a.
         case a of
           (s,i,NONE) => I (SUBSTRING (s,i,STRLEN s − i))
         | (s,i,SOME n) => I (SUBSTRING (s,i,n)))

⊢ IMPLODE "" = "" ∧ ∀c cs. IMPLODE (STRING c cs) = STRING c (IMPLODE cs)

⊢ ∀c. STR c = STRING c ""

⊢ ∀s i n. SUBSTRING (s,i,n) = SEG n i s

⊢ ∀s n. SUB (s,n) = s❲n❳

⊢ TOCHAR =
  WFREC (@R. WF R)
    (λTOCHAR a.
         case a of
           "" => ARB
         | STRING c "" => I c
         | STRING c (STRING v2 v3) => ARB)

⊢ ∀f s. TRANSLATE f s = CONCAT (MAP f s)

⊢ (∀a. CHR (ORD a) = a) ∧ ∀r. (λn. n < 256) r ⇔ ORD (CHR r) = r

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

⊢ ∀c1 c2. char_compare c1 c2 = num_compare (ORD c1) (ORD c2)

⊢ ∀a b. char_ge a b ⇔ ORD a ≥ ORD b

⊢ ∀a b. char_gt a b ⇔ ORD a > ORD b

⊢ ∀a b. char_le a b ⇔ ORD a ≤ ORD b

⊢ ∀a b. char_lt a b ⇔ ORD a < ORD b

⊢ ∀c. char_size c = 0

⊢ ∀c. isAlphaNum c ⇔ isAlpha c ∨ isDigit c

⊢ ∀c. isAlpha c ⇔ isLower c ∨ isUpper c

⊢ ∀c. isAscii c ⇔ ORD c ≤ 127

⊢ ∀c. isCntrl c ⇔ ORD c < 32 ∨ 127 ≤ ORD c

⊢ ∀c. isDigit c ⇔ 48 ≤ ORD c ∧ ORD c ≤ 57

⊢ ∀c. isGraph c ⇔ isPrint c ∧ ¬isSpace c

⊢ ∀c. isHexDigit c ⇔
      48 ≤ ORD c ∧ ORD c ≤ 57 ∨ 97 ≤ ORD c ∧ ORD c ≤ 102 ∨
      65 ≤ ORD c ∧ ORD c ≤ 70

⊢ ∀c. isLower c ⇔ 97 ≤ ORD c ∧ ORD c ≤ 122

⊢ ∀c. isPrint c ⇔ 32 ≤ ORD c ∧ ORD c < 127

⊢ ∀c. isPunct c ⇔ isGraph c ∧ ¬isAlphaNum c

⊢ ∀c. isSpace c ⇔ ORD c = 32 ∨ 9 ≤ ORD c ∧ ORD c ≤ 13

⊢ ∀c. isUpper c ⇔ 65 ≤ ORD c ∧ ORD c ≤ 90

⊢ string_compare = list_compare char_compare

⊢ ∀s. _ inject_string0022 s = s

⊢ ∀s1 s2. string_ge s1 s2 ⇔ string_le s2 s1

⊢ ∀s1 s2. string_gt s1 s2 ⇔ string_lt s2 s1

⊢ ∀s1 s2. string_le s1 s2 ⇔ s1 = s2 ∨ string_lt s1 s2

⊢ ∀c. toLower c = if isUpper c then CHR (ORD c + 32) else c

⊢ ∀c. toUpper c = if isLower c then CHR (ORD c − 32) else c

⊢ ∀c1 c2. c1 = c2 ⇔ ORD c1 = ORD c2

⊢ ∀P. (∀n. n < 256 ⇒ P (CHR n)) ⇒ ∀c. P c

⊢ ∀r r'. r < 256 ⇒ r' < 256 ⇒ (CHR r = CHR r' ⇔ r = r')

⊢ ∀a. ∃r. a = CHR r ∧ r < 256

⊢ ∀a. CHR (ORD a) = a

⊢ ∀s. (DEST_STRING s = NONE ⇔ s = "") ∧
      (DEST_STRING s = SOME (c,t) ⇔ s = STRING c t)

⊢ EXPLODE s1 = EXPLODE s2 ⇔ s1 = s2

⊢ ∀s. EXPLODE s =
      case DEST_STRING s of NONE => "" | SOME (c,t) => STRING c (EXPLODE t)

⊢ EXPLODE "" = "" ∧ ∀c s. EXPLODE (STRING c s) = STRING c (EXPLODE s)

⊢ (EXPLODE s = "" ⇔ s = "") ∧ ("" = EXPLODE s ⇔ s = "")

⊢ ∀s h t.
    (STRING h t = EXPLODE s ⇔ s = STRING h (IMPLODE t)) ∧
    (EXPLODE s = STRING h t ⇔ s = STRING h (IMPLODE t))

⊢ EXPLODE (IMPLODE cs) = cs

⊢ ∀cs. ∃s. cs = EXPLODE s

⊢ EXTRACT (s,i,NONE) = SUBSTRING (s,i,STRLEN s − i) ∧
  EXTRACT (s,i,SOME n) = SUBSTRING (s,i,n)

⊢ ∀P. (∀s i. P (s,i,NONE)) ∧ (∀s i n. P (s,i,SOME n)) ⇒
      ∀v v1 v2. P (v,v1,v2)

⊢ (∀P. FIELDS P "" = [""]) ∧
  ∀t h P.
    FIELDS P (STRING h t) =
    (let
       (l,r) = SPLITP P (STRING h t)
     in
       if NULL l then ""::FIELDS P (TL r)
       else if NULL r then [l]
       else l::FIELDS P (TL r))

⊢ ∀P'.
    (∀P. P' P "") ∧
    (∀P h t.
       (∀l r. (l,r) = SPLITP P (STRING h t) ∧ NULL l ⇒ P' P (TL r)) ∧
       (∀l r.
          (l,r) = SPLITP P (STRING h t) ∧ ¬NULL l ∧ ¬NULL r ⇒ P' P (TL r)) ⇒
       P' P (STRING h t)) ⇒
    ∀v v1. P' v v1

⊢ FINITE 𝕌(:char)

⊢ IMPLODE cs1 = IMPLODE cs2 ⇔ cs1 = cs2

⊢ IMPLODE "" = "" ∧ ∀c cs. IMPLODE (STRING c cs) = STRING c (IMPLODE cs)

⊢ (IMPLODE l = "" ⇔ l = "") ∧ ("" = IMPLODE l ⇔ l = "")

⊢ ∀c s l.
    (STRING c s = IMPLODE l ⇔ l = STRING c (EXPLODE s)) ∧
    (IMPLODE l = STRING c s ⇔ l = STRING c (EXPLODE s))

⊢ IMPLODE (EXPLODE s) = s

⊢ EXPLODE s = s ∧ IMPLODE s = s

⊢ ∀s. ∃cs. s = IMPLODE cs

⊢ ∀clist. IMPLODE clist = FOLDR STRING "" clist

⊢ INFINITE 𝕌(:string)

⊢ ∀a a'. ORD a = ORD a' ⇔ a = a'

⊢ ∀c. ORD c < 256

⊢ ∀r. r < 256 ⇔ ORD (CHR r) = r

⊢ ∀n. ORD (CHR n) = if n < 256 then n else FAIL ORD $var$(> 255) (CHR n)

⊢ ∀r. r < 256 ⇒ ORD (CHR r) = r

⊢ ∀r. r < 256 ⇔ ∃a. r = ORD a

⊢ RC char_lt = char_le

⊢ STRCAT s1 s2 = STRCAT s1 s2

⊢ (∀l1 l2 l3. STRCAT l1 l2 = STRCAT l1 l3 ⇔ l2 = l3) ∧
  ∀l1 l2 l3. STRCAT l2 l1 = STRCAT l3 l1 ⇔ l2 = l3

⊢ ∀s s1. (s = STRCAT s s1 ⇔ s1 = "") ∧ (s = STRCAT s1 s ⇔ s1 = "")

⊢ ∀l1 l2 l3. STRCAT l1 (STRCAT l2 l3) = STRCAT (STRCAT l1 l2) l3

⊢ STRCAT "" s = s ∧ STRCAT s "" = s ∧
  STRCAT (STRING c s1) s2 = STRING c (STRCAT s1 s2)

⊢ ∀l1 l2. STRCAT l1 l2 = "" ⇔ l1 = "" ∧ l2 = ""

⊢ ∀s1 s2. STRCAT s1 s2 = FOLDR STRING s2 (EXPLODE s1)

⊢ (∀l. STRCAT "" l = l) ∧
  ∀l1 l2 h. STRCAT (STRING h l1) l2 = STRING h (STRCAT l1 l2)

⊢ ∀s c. STRING c s ≠ s ∧ s ≠ STRING c s

⊢ ∀l1 l2. STRLEN (STRCAT l1 l2) = STRLEN l1 + STRLEN l2

⊢ STRLEN "" = 0 ∧ ∀h t. STRLEN (STRING h t) = SUC (STRLEN t)

⊢ ∀l. STRLEN l = 0 ⇔ l = ""

⊢ STRLEN s = STRLEN (EXPLODE s)

⊢ STRLEN "" = 0 ∧ ∀h t. STRLEN (STRING h t) = SUC (STRLEN t)

⊢ TOCHAR (STRING c "") = c

⊢ ∀P. (∀c. P (STRING c "")) ∧ P "" ∧
      (∀v6 v4 v5. P (STRING v6 (STRING v4 v5))) ⇒
      ∀v. P v

⊢ ∀P l1 x l2.
    P x ⇒ TOKENS P (STRCAT l1 (STRING x l2)) = TOKENS P l1 ⧺ TOKENS P l2

⊢ ¬NULL ls ∧ P (LAST ls) ⇒ TOKENS P (FRONT ls) = TOKENS P ls

⊢ ∀ls. TOKENS f ls = [] ⇔ EVERY f ls

⊢ (∀P. TOKENS P "" = []) ∧
  ∀t h P.
    TOKENS P (STRING h t) =
    (let
       (l,r) = SPLITP P (STRING h t)
     in
       if NULL l then TOKENS P (TL r) else l::TOKENS P r)

⊢ ∀P'.
    (∀P. P' P "") ∧
    (∀P h t.
       (∀l r. (l,r) = SPLITP P (STRING h t) ∧ NULL l ⇒ P' P (TL r)) ∧
       (∀l r. (l,r) = SPLITP P (STRING h t) ∧ ¬NULL l ⇒ P' P r) ⇒
       P' P (STRING h t)) ⇒
    ∀v v1. P' v v1

⊢ 𝕌(:char) = IMAGE CHR (count 256)

⊢ WF char_lt

⊢ ∀c. ∃n. c = CHR n

⊢ ∀x. isAlphaNum x ⇒ isPrint x

⊢ ∀x. isHexDigit x ⇒ isAlphaNum x

⊢ ∀x. isHexDigit x ⇒ isPrint x

⊢ ∀s1 s2.
    s1 ≼ s2 ⇔
    case (DEST_STRING s1,DEST_STRING s2) of
      (NONE,v1) => T
    | (SOME v2,NONE) => F
    | (SOME (c1,t1),SOME (c2,t2)) => c1 = c2 ∧ t1 ≼ t2

⊢ ∀P. (∀s1 s2.
         (∀c t1 t2.
            DEST_STRING s1 = SOME (c,t1) ∧ DEST_STRING s2 = SOME (c,t2) ⇒
            P t1 t2) ⇒
         P s1 s2) ⇒
      ∀v v1. P v v1

⊢ ∀s1 s2. s1 ≼ s2 ⇔ ∃s3. s2 = STRCAT s1 s3

⊢ ¬WF string_lt

⊢ ∀c. ∃n. c = CHR n ∧ n < 256

⊢ string_lt = LLEX char_lt

⊢ ∀s t. ¬(string_lt s t ∧ string_lt t s)

⊢ ∀s t. s = t ∨ string_lt s t ∨ string_lt t s

⊢ (∀s. string_lt s "" ⇔ F) ∧ (∀s c. string_lt "" (STRING c s) ⇔ T) ∧
  ∀s2 s1 c2 c1.
    string_lt (STRING c1 s1) (STRING c2 s2) ⇔
    char_lt c1 c2 ∨ c1 = c2 ∧ string_lt s1 s2

⊢ ∀P. (∀s. P s "") ∧ (∀c s. P "" (STRING c s)) ∧
      (∀c1 s1 c2 s2. P s1 s2 ⇒ P (STRING c1 s1) (STRING c2 s2)) ⇒
      ∀v v1. P v v1

⊢ ∀s. ¬string_lt s s

⊢ ∀s1 s2 s3. string_lt s1 s2 ∧ string_lt s2 s3 ⇒ string_lt s1 s3