Theory "string"

Parents list

Signature

Type	Arity
string	0
char	0
Constant	Type
string_case	:'a -> (char -> string -> 'a) -> string -> 'a
isPREFIX_tupled	:string # string -> bool
isPREFIX	:string -> string -> bool
STRLEN	:string -> num
STRING	:char -> string -> string
STRCAT	:string -> string -> string
ORD	:char -> num
IMPLODE	:char list -> string
EXPLODE	:string -> char list
EMPTYSTRING	:string
DEST_STRING	:string -> (char # string) option
CHR	:num -> char

Definitions

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)

string_TY_DEF

|- ?rep. TYPE_DEFINITION (\x. T) rep

string_bij

|- (!a. IMPLODE (EXPLODE a) = a) /\ !r. (\x. T) r = (EXPLODE (IMPLODE r) = r)

EMPTYSTRING_DEF

|- "" = IMPLODE []

STRING_DEF

|- !c str. STRING c str = IMPLODE (c::EXPLODE str)

STRING_CASE_DEF

|- (!b f. string_case b f "" = b) /\
   !b f c s. string_case b f (STRING c s) = f c s

STRLEN_DEF

|- (STRLEN "" = 0) /\ !c s. STRLEN (STRING c s) = 1 + STRLEN s

DEST_STRING

|- (DEST_STRING "" = NONE) /\
   !c rst. DEST_STRING (STRING c rst) = SOME (c,rst)

STRCAT

|- !s1 s2. STRCAT s1 s2 = IMPLODE (EXPLODE s1 ++ EXPLODE s2)

isPREFIX_tupled_primitive_def

|- isPREFIX_tupled =
   WFREC
     (@R.
        WF R /\
        !s2 s1 v v1 v2 c1 t1 v7 c2 t2.
          ((DEST_STRING s1,DEST_STRING s2) = (v,v1)) /\ (v = SOME v2) /\
          (v2 = (c1,t1)) /\ (v1 = SOME v7) /\ (v7 = (c2,t2)) ==>
          R (t1,t2) (s1,s2))
     (\isPREFIX_tupled a.
        case a of
           (s1,s2) ->
             I
               case (DEST_STRING s1,DEST_STRING s2) of
                  (NONE,v1) -> T
               || (SOME (c1,t1),NONE) -> F
               || (SOME (c1,t1),SOME (c2,t2)) ->
                    (c1 = c2) /\ isPREFIX_tupled (t1,t2))

isPREFIX_curried_def

|- !x x1. isPREFIX x x1 = isPREFIX_tupled (x,x1)

Theorems

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

|- !r. ORD (CHR r) = (if r < 256 then r else ORD (CHR r))

ORD_BOUND

|- !c. ORD c < 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

IMPLODE_EXPLODE

|- !a. IMPLODE (EXPLODE a) = a

EXPLODE_IMPLODE

|- !r. EXPLODE (IMPLODE r) = r

EXPLODE_ONTO

|- !r. ?a. r = EXPLODE a

IMPLODE_ONTO

|- !a. ?r. a = IMPLODE r

EXPLODE_11

|- !a a'. (EXPLODE a = EXPLODE a') = (a = a')

IMPLODE_11

|- !r r'. (IMPLODE r = IMPLODE r') = (r = r')

STRING_11

|- !c1 c2 s1 s2. (STRING c1 s1 = STRING c2 s2) = (c1 = c2) /\ (s1 = s2)

STRING_DISTINCT

|- (!c s. ~("" = STRING c s)) /\ !c s. ~(STRING c s = "")

string_Axiom

|- !b g. ?f. (f "" = b) /\ !c t. f (STRING c t) = g c t (f t)

STRING_INDUCT_THM

|- !P. P "" /\ (!s. P s ==> !c. P (STRING c s)) ==> !s. P s

STRING_ACYCLIC

|- !s c. ~(STRING c s = s) /\ ~(s = STRING c s)

STRING_CASES

|- !s. (s = "") \/ ?c str. s = STRING c str

STRING_CASE_CONG

|- !M M' b f.
     (M = M') /\ ((M' = "") ==> (b = b')) /\
     (!c s. (M' = STRING c s) ==> (f c s = f' c s)) ==>
     (string_case b f M = string_case b' f' M')

DEST_STRING_LEMS

|- !s.
     ((DEST_STRING s = NONE) = (s = "")) /\
     ((DEST_STRING s = SOME (c,t)) = (s = STRING c t))

EXPLODE_EQNS

|- (EXPLODE "" = []) /\ !c s. EXPLODE (STRING c s) = c::EXPLODE s

IMPLODE_EQNS

|- (IMPLODE [] = "") /\ !c s. IMPLODE (c::t) = STRING c (IMPLODE t)

IMPLODE_EQ_EMPTYSTRING

|- ((IMPLODE l = "") = (l = [])) /\ (("" = IMPLODE l) = (l = []))

EXPLODE_EQ_NIL

|- ((EXPLODE s = []) = (s = "")) /\ (([] = EXPLODE s) = (s = ""))

EXPLODE_EQ_THM

|- !s h t.
     ((h::t = EXPLODE s) = (s = STRING h (IMPLODE t))) /\
     ((EXPLODE s = h::t) = (s = STRING h (IMPLODE t)))

IMPLODE_EQ_THM

|- !c s l.
     ((STRING c s = IMPLODE l) = (l = c::EXPLODE s)) /\
     ((IMPLODE l = STRING c s) = (l = c::EXPLODE s))

EXPLODE_DEST_STRING

|- !s.
     EXPLODE s =
     case DEST_STRING s of NONE -> [] || SOME (c,t) -> c::EXPLODE t

IMPLODE_STRING

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

STRLEN_THM

|- !s. STRLEN s = LENGTH (EXPLODE s)

STRLEN_EQ_0

|- !x. (STRLEN x = 0) = (x = "")

STRCAT_EQNS

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

STRCAT_ASSOC

|- !s1 s2 s3. STRCAT s1 (STRCAT s2 s3) = STRCAT (STRCAT s1 s2) s3

STRCAT_11

|- !s1 s2 s3.
     ((STRCAT s1 s2 = STRCAT s1 s3) = (s2 = s3)) /\
     ((STRCAT s1 s3 = STRCAT s2 s3) = (s1 = s2))

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

|- !x y. (STRCAT x y = "") = (x = "") /\ (y = "")

STRLEN_CAT

|- !x y. STRLEN (STRCAT x y) = STRLEN x + STRLEN y

isPREFIX_DEF

|- isPREFIX s1 s2 =
   case (DEST_STRING s1,DEST_STRING s2) of
      (NONE,v1) -> T
   || (SOME (c1,t1),NONE) -> F
   || (SOME (c1,t1),SOME (c2,t2)) -> (c1 = c2) /\ isPREFIX t1 t2

isPREFIX_IND

|- !P.
     (!s1 s2.
        (!c1 c2 t1 t2.
           (DEST_STRING s1 = SOME (c1,t1)) /\
           (DEST_STRING s2 = SOME (c2,t2)) ==>
           P t1 t2) ==>
        P s1 s2) ==>
     !v v1. P v v1

isPREFIX_STRCAT

|- !s1 s2. isPREFIX s1 s2 = ?s3. s2 = STRCAT s1 s3

DATATYPE_STRING

|- DATATYPE (string "" STRING)