Theory "string"

Signature

Definitions

TRANSLATE_def

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

toUpper_def

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

toLower_def

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

TOCHAR_primitive_def

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

SUBSTRING_def

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

SUB_def

⊢ ∀s n. SUB (s,n) = EL n s

string_le_def

⊢ ∀s1 s2. s1 ≤ s2 ⇔ (s1 = s2) ∨ s1 < s2

string_gt_def

⊢ ∀s1 s2. s1 > s2 ⇔ s2 < s1

string_ge_def

⊢ ∀s1 s2. s1 ≥ s2 ⇔ s2 ≤ s1

string_elim__magic

⊢ ∀s. _ inject_string0022 s = s

STR_def

⊢ ∀c. STR c = STRING c ""

isUpper_def

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

isSpace_def

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

isPunct_def

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

isPrint_def

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

isLower_def

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

isHexDigit_def

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

isGraph_def

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

isDigit_def

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

isCntrl_def

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

isAscii_def

⊢ ∀c. isAscii c ⇔ ORD c ≤ 127

isAlphaNum_def

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

isAlpha_def

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

IMPLODE_def

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

EXTRACT_primitive_def

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

EXPLODE_def

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

DEST_STRING_def

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

char_TY_DEF

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

char_size_def

⊢ ∀c. char_size c = 0

char_lt_def

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

char_le_def

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

char_gt_def

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

char_ge_def

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

char_BIJ

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

Theorems

TOKENS_NIL

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

TOKENS_ind

⊢ ∀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

TOKENS_FRONT

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

TOKENS_def

⊢ (∀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)

TOKENS_APPEND

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

TOCHAR_ind

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

TOCHAR_def

⊢ TOCHAR (STRING c "") = c

STRLEN_THM

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

STRLEN_EXPLODE_THM

⊢ STRLEN s = STRLEN (EXPLODE s)

STRLEN_EQ_0

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

STRLEN_DEF

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

STRLEN_CAT

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

string_lt_trans

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

string_lt_nonrefl

⊢ ∀s. ¬(s < s)

string_lt_ind

⊢ ∀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

string_lt_def

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

string_lt_cases

⊢ ∀s t. (s = t) ∨ s < t ∨ t < s

string_lt_antisym

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

STRING_ACYCLIC

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

STRCAT_EXPLODE

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

STRCAT_EQNS

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

STRCAT_EQ_EMPTY

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

STRCAT_def

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

STRCAT_ASSOC

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

STRCAT_ACYCLIC

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

STRCAT_11

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

STRCAT

⊢ STRCAT s1 s2 = STRCAT s1 s2

ranged_char_nchotomy

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

ORD_ONTO

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

ORD_CHR_RWT

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

ORD_CHR_COMPUTE

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

ORD_CHR

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

ORD_BOUND

⊢ ∀c. ORD c < 256

ORD_11

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

isPREFIX_STRCAT

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

isPREFIX_IND

⊢ ∀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

isPREFIX_DEF

⊢ ∀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

isHexDigit_isPrint

⊢ ∀x. isHexDigit x ⇒ isPrint x

isHexDigit_isAlphaNum

⊢ ∀x. isHexDigit x ⇒ isAlphaNum x

isAlphaNum_isPrint

⊢ ∀x. isAlphaNum x ⇒ isPrint x

IMPLODE_STRING

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

IMPLODE_ONTO

⊢ ∀s. ∃cs. s = IMPLODE cs

IMPLODE_EXPLODE_I

⊢ (EXPLODE s = s) ∧ (IMPLODE s = s)

IMPLODE_EXPLODE

⊢ IMPLODE (EXPLODE s) = s

IMPLODE_EQNS

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

IMPLODE_EQ_THM

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

IMPLODE_EQ_EMPTYSTRING

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

IMPLODE_11

⊢ (IMPLODE cs1 = IMPLODE cs2) ⇔ (cs1 = cs2)

FIELDS_ind

⊢ ∀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

FIELDS_def

⊢ (∀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))

EXTRACT_ind

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

EXTRACT_def

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

EXPLODE_ONTO

⊢ ∀cs. ∃s. cs = EXPLODE s

EXPLODE_IMPLODE

⊢ EXPLODE (IMPLODE cs) = cs

EXPLODE_EQNS

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

EXPLODE_EQ_THM

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

EXPLODE_EQ_NIL

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

EXPLODE_DEST_STRING

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

EXPLODE_11

⊢ (EXPLODE s1 = EXPLODE s2) ⇔ (s1 = s2)

DEST_STRING_LEMS

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

CHR_ORD

⊢ ∀a. CHR (ORD a) = a

CHR_ONTO

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

CHR_11

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

char_nchotomy

⊢ ∀c. ∃n. c = CHR n

CHAR_INDUCT_THM

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

CHAR_EQ_THM

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