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)

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