Theory "string"

Signature

Definitions

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_BIJ

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

isLower_def

|- ∀c. isLower c ⇔ 97 ≤ ORD c ∧ ORD c ≤ 122

isUpper_def

|- ∀c. isUpper c ⇔ 65 ≤ ORD c ∧ ORD c ≤ 90

isDigit_def

|- ∀c. isDigit c ⇔ 48 ≤ ORD c ∧ ORD c ≤ 57

isAlpha_def

|- ∀c. isAlpha c ⇔ isLower c ∨ isUpper c

isHexDigit_def

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

isAlphaNum_def

|- ∀c. isAlphaNum c ⇔ isAlpha c ∨ isDigit c

isPrint_def

|- ∀c. isPrint c ⇔ 32 ≤ ORD c ∧ ORD c < 127

isSpace_def

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

isGraph_def

|- ∀c. isGraph c ⇔ isPrint c ∧ ¬isSpace c

isPunct_def

|- ∀c. isPunct c ⇔ isGraph c ∧ ¬isAlphaNum c

isAscii_def

|- ∀c. isAscii c ⇔ ORD c ≤ 127

isCntrl_def

|- ∀c. isCntrl c ⇔ ORD c < 32 ∨ 127 ≤ ORD c

toLower_def

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

toUpper_def

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

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_size_def

|- ∀c. char_size c = 0

SUB_def

|- ∀s n. SUB (s,n) = EL n s

STR_def

|- ∀c. STR c = STRING 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

TRANSLATE_def

|- ∀f s. TRANSLATE f s = CONCAT (MAP f s)

TOKENS_tupled_primitive_def

|- TOKENS_tupled =
   WFREC
     (@R.
        WF R ∧
        (∀t h P l r.
           ((l,r) = SPLITP P (STRING h t)) ∧ NULL l ⇒
           R (P,TL r) (P,STRING h t)) ∧
        ∀t h P l r.
          ((l,r) = SPLITP P (STRING h t)) ∧ ¬NULL l ⇒ R (P,r) (P,STRING h t))
     (λTOKENS_tupled a.
        case a of
          (P,"") => I []
        | (P,STRING h t) =>
            I
              (let (l,r) = SPLITP P (STRING h t)
               in
                 if NULL l then TOKENS_tupled (P,TL r)
                 else l::TOKENS_tupled (P,r)))

TOKENS_curried_def

|- ∀x x1. TOKENS x x1 = TOKENS_tupled (x,x1)

FIELDS_tupled_primitive_def

|- FIELDS_tupled =
   WFREC
     (@R.
        WF R ∧
        (∀t h P l r.
           ((l,r) = SPLITP P (STRING h t)) ∧ NULL l ⇒
           R (P,TL r) (P,STRING h t)) ∧
        ∀t h P l r.
          ((l,r) = SPLITP P (STRING h t)) ∧ ¬NULL l ∧ ¬NULL r ⇒
          R (P,TL r) (P,STRING h t))
     (λFIELDS_tupled a.
        case a of
          (P,"") => I [""]
        | (P,STRING h t) =>
            I
              (let (l,r) = SPLITP P (STRING h t)
               in
                 if NULL l then ""::FIELDS_tupled (P,TL r)
                 else if NULL r then [l]
                 else l::FIELDS_tupled (P,TL r)))

FIELDS_curried_def

|- ∀x x1. FIELDS x x1 = FIELDS_tupled (x,x1)

IMPLODE_def

|- (IMPLODE "" = "") ∧ ∀c cs. IMPLODE (STRING c cs) = STRING c (IMPLODE cs)

EXPLODE_def

|- (EXPLODE "" = "") ∧ ∀c s. EXPLODE (STRING c s) = STRING c (EXPLODE s)

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

string_lt_tupled_primitive_def

|- string_lt_tupled =
   WFREC (@R. WF R ∧ ∀c2 c1 s2 s1. R (s1,s2) (STRING c1 s1,STRING c2 s2))
     (λstring_lt_tupled a.
        case a of
          (s,"") => I F
        | ("",STRING c s') => I T
        | (STRING c1 s1,STRING c s') =>
            I (c1 < c ∨ (c1 = c) ∧ string_lt_tupled (s1,s')))

string_lt_curried_def

|- ∀x x1. x < x1 ⇔ string_lt_tupled (x,x1)

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

Theorems

IMPLODE_STRING

|- ∀clist. IMPLODE clist = FOLDR STRING "" clist

EXPLODE_DEST_STRING

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

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

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

IMPLODE_EQ_EMPTYSTRING

|- ((IMPLODE l = "") ⇔ (l = "")) ∧ (("" = IMPLODE l) ⇔ (l = ""))

IMPLODE_EQNS

|- (IMPLODE "" = "") ∧ ∀c cs. IMPLODE (STRING c cs) = STRING c (IMPLODE cs)

EXPLODE_EQNS

|- (EXPLODE "" = "") ∧ ∀c s. EXPLODE (STRING c s) = STRING c (EXPLODE s)

DEST_STRING_LEMS

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

STRLEN_EXPLODE_THM

|- STRLEN s = STRLEN (EXPLODE s)

ORD_11

|- ∀a a'. (ORD a = ORD a') ⇔ (a = a')

CHR_11

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

ORD_ONTO

|- ∀r. r < 256 ⇔ ∃a. r = ORD a

CHR_ONTO

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

CHR_ORD

|- ∀a. CHR (ORD a) = a

ORD_CHR

|- ∀r. r < 256 ⇔ (ORD (CHR r) = r)

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 > 255 (CHR n)

ORD_BOUND

|- ∀c. ORD c < 256

char_nchotomy

|- ∀c. ∃n. c = CHR n

ranged_char_nchotomy

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

CHAR_EQ_THM

|- ∀c1 c2. (c1 = c2) ⇔ (ORD c1 = ORD c2)

CHAR_INDUCT_THM

|- ∀P. (∀n. n < 256 ⇒ P (CHR n)) ⇒ ∀c. P c

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

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

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

IMPLODE_EXPLODE_I

|- (EXPLODE s = s) ∧ (IMPLODE s = s)

IMPLODE_EXPLODE

|- IMPLODE (EXPLODE s) = s

EXPLODE_IMPLODE

|- EXPLODE (IMPLODE cs) = cs

EXPLODE_ONTO

|- ∀cs. ∃s. cs = EXPLODE s

IMPLODE_ONTO

|- ∀s. ∃cs. s = IMPLODE cs

EXPLODE_11

|- (EXPLODE s1 = EXPLODE s2) ⇔ (s1 = s2)

IMPLODE_11

|- (IMPLODE cs1 = IMPLODE cs2) ⇔ (cs1 = cs2)

STRING_ACYCLIC

|- ∀s c. STRING c s ≠ s ∧ s ≠ STRING c s

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

STRLEN_EQ_0

|- ∀l. (STRLEN l = 0) ⇔ (l = "")

STRLEN_THM

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

STRLEN_DEF

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

STRCAT_def

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

STRCAT

|- STRCAT s1 s2 = STRCAT s1 s2

STRCAT_EQNS

|- (STRCAT "" s = s) ∧ (STRCAT s "" = s) ∧
   (STRCAT (STRING c s1) s2 = STRING c (STRCAT s1 s2))

STRCAT_ASSOC

|- ∀l1 l2 l3. STRCAT l1 (STRCAT l2 l3) = STRCAT (STRCAT l1 l2) l3

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_ACYCLIC

|- ∀s s1. ((s = STRCAT s s1) ⇔ (s1 = "")) ∧ ((s = STRCAT s1 s) ⇔ (s1 = ""))

STRCAT_EXPLODE

|- ∀s1 s2. STRCAT s1 s2 = FOLDR STRING s2 (EXPLODE s1)

STRCAT_EQ_EMPTY

|- ∀l1 l2. (STRCAT l1 l2 = "") ⇔ (l1 = "") ∧ (l2 = "")

STRLEN_CAT

|- ∀l1 l2. STRLEN (STRCAT l1 l2) = STRLEN l1 + STRLEN l2

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

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_STRCAT

|- ∀s1 s2. s1 ≼ s2 ⇔ ∃s3. s2 = STRCAT s1 s3

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_nonrefl

|- ∀s. ¬(s < s)

string_lt_antisym

|- ∀s t. ¬(s < t ∧ t < s)

string_lt_cases

|- ∀s t. (s = t) ∨ s < t ∨ t < s

string_lt_trans

|- ∀s1 s2 s3. s1 < s2 ∧ s2 < s3 ⇒ s1 < s3