The HOL string Library

T. F. Melham

University of Cambridge, Computer Laboratory

New Museums Site, Pembroke Street Cambridge, CB2 3QG, England.

June 1991 \begin{matrix}c \\ ◯ \end{matrix} T. F. Melham 1991

Contents

1 The string Library 1

1.1 Ascii character codes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.1.1 Function definitions on type ascii . . . . . . . . . . . . . . . . . . 2 1.1.2 Theorems about the type ascii . . . . . . . . . . . . . . . . . . . . 2 1.1.3 Decision procedure for ascii code equality . . . . . . . . . . . . . . . 3

1.2 Character strings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2.1 Function definitions on type string . . . . . . . . . . . . . . . . . . 4 1.2.2 Theorems about the type string . . . . . . . . . . . . . . . . . . . 4 1.2.3 String constants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.2.4 Decision procedure for string equality . . . . . . . . . . . . . . . . . 6

1.3 Using the library . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.3.1 Example session . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.3.2 The load string function . . . . . . . . . . . . . . . . . . . . . . . 8

2 ML Functions in the string Library 9

3 Pre-proved Theorems 13 3.1 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 3.2 Theorems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

References 17

Index 18 iv Contents

Chapter 1

The string Library

This document describes the facilities provided by the string library and explains its logical basis. This library makes ascii character strings available in the HOL logic via two formally-defined logical types, ascii and string. The definitions of these types and some simple theorems about them reside in the two theory files ascii.th and string.th in the library string. The library also contains some very basic derived rules of inference for reasoning about character strings in logic.

1.1 Ascii character codes

The most basic theory in the library is the theory ascii, in which a type ascii of 8-bit ascii character codes is defined. In the notation for describing concrete types used by the function define_type, the type ascii is specified by the following equation.

    ascii  =  ASCII bool bool bool bool bool bool bool bool

The simple enumerated type ascii described by this equation provides a representation in logic for the set of all 8-bit ascii character codes. Each character is represented by a value obtained by applying the function ASCII to the eight boolean values of its standard ascii character code. The letter ‘a’, for example, has the 8-bit code ‘01100001’ and is represented formally in logic by the term

    "ASCII F T T F F F F T"

Of course, any other ascii character code can likewise be represented in logic by a value of type ascii constructed using the function constant ASCII.

The type ascii and the constant ASCII are defined formally in the library using the function define_type from the HOL recursive types package (see [1, 2]). This gives the following theorem, called ascii_Axiom, as an abstract characterization of the type ascii:

    |- !f. ?!fn:ascii->*.
         !b0 b1 b2 b3 b4 b5 b6 b7.
           fn(ASCII b0 b1 b2 b3 b4 b5 b6 b7) = f b0 b1 b2 b3 b4 b5 b6 b7

This simply says that functions on values of type ascii may be uniquely specified by defining them in terms of the eight boolean values from which these values are constructed.

1.1.1 Function definitions on type ascii

The theorem ascii_Axiom, having been proved using the recursive types package, is in the right form for use with the derived rule of definition new_recursive_definition. For example, once the string library is loaded into HOL, one can use this rule of definition to define a function that selects the high-order bit of an ascii character code:

1

 #let BIT1 =
      new_recursive_definition false ascii_Axiom `BIT1`
      "BIT1(ASCII b1 b2 b3 b4 b5 b6 b7 b8) = b1";;
 BIT1 =
 |- !b1 b2 b3 b4 b5 b6 b7 b8. BIT1(ASCII b1 b2 b3 b4 b5 b6 b7 b8) = b1

In fact, any function whatsoever on the ascii is definable using the theorem ascii_Axiom

and the rule new_recursive_definition.

1.1.2 Theorems about the type ascii

In addition to ascii_Axiom, several standard theorems about the defined type ascii proved using the recursive types package are available as built-in theorems of the string library. They are all set up to autoload, if possible, when the library is loaded into HOL.

The theorem ASCII_11 states that the function ASCII is injective:

    |- !b0 b1 b2 b3 b4 b5 b6 b7 b0' b1' b2' b3' b4' b5' b6' b7'.
       (ASCII b0 b1 b2 b3 b4 b5 b6 b7 = ASCII b0' b1' b2' b3' b4' b5' b6' b7')
         =
       (b0 = b0') /\ (b1 = b1') /\ (b2 = b2') /\ (b3 = b3') /\
       (b4 = b4') /\ (b5 = b5') /\ (b6 = b6') /\ (b7 = b7')

This theorem allows one to prove equality or inequality of ascii character codes; it also forms the basis for the decision-procedure ascii_EQ_CONV explained in section 1.1.3. A degenerate ‘structural induction’ theorem for the type ascii, called ascii_Induct, is also available in the library:

    |- !P. (!b0 b1 b2 b3 b4 b5 b6 b7. P(ASCII b0 b1 b2 b3 b4 b5 b6 b7))
             ==>
           (!a. P a)

This is in the standard form used by the recursive types package and can therefore be used with INDUCT_THEN if desired. Finally, there is the trivial case analysis theorem ascii_CASES:

    |- !a. ?b0 b1 b2 b3 b4 b5 b6 b7. a = ASCII b0 b1 b2 b3 b4 b5 b6 b7

This states that every value of type ascii can be constructed using the function ASCII and can be used, for example, with STRUCT_CASES_TAC to replace variables ranging over ascii by values explicitly constructed with ASCII.

1.1.3 Decision procedure for ascii code equality

The string library provides a highly optimized conversion for proving equality or inequality of constant terms that represent ascii character codes, in the form of applications of the constructor ASCII to the boolean constants T and F. This conversion, called ascii_EQ_COND, expects its term argument to be an equation of the form:

"ASCII a_{1} a_{2} a_{3} a_{4} a_{5} a_{6} a_{7} a_{8} = ASCII b_{1} b_{2} b_{3} b_{4} b_{5} b_{6} b_{7} b_{8}"

where each of a_{1}, …, a_{8}, b_{1}, …, b_{8} is either the constant T or the constant F. Given such an equation, ascii_EQ_COND proves that it is equal to true (T) if the left and right-hand sides represent the same ascii code or false (F) otherwise. The following session illustrates the use of the conversion:

1

 #ascii_EQ_CONV "ASCII T T F T T F T T = ASCII T T F T T F T T";;
 |- (ASCII T T F T T F T T = ASCII T T F T T F T T) = T
 #ascii_EQ_CONV "ASCII T T F T T F T T = ASCII T T F T T F T F";;
 |- (ASCII T T F T T F T T = ASCII T T F T T F T F) = F

The conversion is highly optimised and using it can be considerably faster than proving equality or inequality by, for example, rewriting with the theorem ASCII_11.

1.2 Character strings

The theory string in the library defines a logical type of ascii character strings. These are (possibly empty) sequences of character codes, and the theory ascii is a parent of the theory string. The type of ascii character strings, called string, is defined formally in the library using define_type, with the recursive specifying equation shown below.

    string  =  ``  |  STRING ascii string

Every value of type string consists of a finite sequence of ascii character codes. These sequences are constructed using the function STRING from the empty string represented by the constant ``. For example, the character string ‘ab’ is represented in logic by:

    "STRING (ASCII F T T F F F F T) (STRING (ASCII F T T F F F T F) ``)"

Any finite string of ascii characters can be represented in logic in a similar way.

The type string is defined in the library using the recursive types package. An abstract characterization of the type string, in the standard form used by the recursive types package, is provided by the theorem string_Axiom:

    |- !e f. ?! fn. (fn `` = e) /\ (!a s. fn(STRING a s) = f(fn s)a s)

This theorem, which is proved automatically by define_type, states the validity of primitive recursive definitions on the type string.

1.2.1 Function definitions on type string

The theorem string_Axiom is in the standard form accepted by new_recursive_definition and can therefore be used to define functions over type string by primitive recursion. For example, one can define the length of a string as follows.

1

 #let LEN =
      new_recursive_definition false string_Axiom `LEN`
      "(LEN `` = 0) /\ (LEN (STRING a s) = (LEN s) + 1)";;
 LEN = |- (LEN `` = 0) /\ (!a s. LEN(STRING a s) = (LEN s) + 1)

Other forms of primitive recursive definition may also be made using string_Axiom and new_recursive_definition; see the HOL system documentation for details.

1.2.2 Theorems about the type string

For the recursive type string, the library provides as built-in all the standard theorems provable using the recursive types package. These theorems, which are set up to autoload when the library is loaded, include theorems stating the distinctness of empty and nonempty strings:

    NOT_STRING_EMPTY   |- !a s. ~(`` = STRING a s)
    NOT_EMPTY_STRING   |- !a s. ~(STRING a s = ``)

The library also contains a theorem stating that the constructor STRING is injective:

    STRING_11   |- !a s a' s'. (STRING a s = STRING a' s') = (a=a') /\ (s=s')

This theorem, which can be used to reason about the equality of character strings, forms the basis of the equality conversion described in section 1.2.4 below. Also built-in are theorems for doing proofs by structural induction on type string and for empty vs nonempty case analysis on character strings:

    string_Induct |- !P. P `` /\ (!s. P s ==> (!a.P(STRING a s))) ==> (!s. P s)
    string_CASES  |- !s. (s = ``) \/ (?s' a. s = STRING a s')

The theorem string_Induct is in the correct form for use with the built-in induction

tactic INDUCT_THEN, and the theorem string_CASES may be used with STRUCT_CASES_TAC.

See the HOL manual for details of these two functions.

1.2.3 String constants

To provide a concise notation for strings in the HOL logic, the system parser and prettyprinter supports a notation for string constants is introduced. A string constant is a logical constant of type string written between single quotes as follows: "`c_{1} … c_{n}`". Such a term should be regarded as an object language abbreviation for the value of type string that represents the ascii character string ‘c_{1} … c_{n}’. For example, the string constant "`ab`" is (conceptually) defined formally by:

    |- `ab` = STRING(ASCII F T T F F F F T)(STRING(ASCII F T T F F F T F)``)

and abbreviates the term of type string that represents the string ‘ab’.

The HOL parser and pretty-printer supports the character string notation only when the string library has been loaded. This is illustrated by the following session, which begins before the library has been loaded.

1

 #"`abc`";;
 type ":string" not defined -- load library string?
 skipping: <string> " ;; parse failed

Here, character string constants like "`abc`" do not parse, since the logical type string is not present in the current theory. But the string notation becomes available when the library is loaded:

2

 #load_library `string`;;

⋮

 Library `string` loaded.
 () : void
 #"`abc`";;
 "`abc`" : term

Note that terms in the HOL logic like "`abc`" are in fact constants of type string:

3

 #is_const "`abc`";;
 true : bool
 #type_of "`abc`";;
 ":string" : type

Like numerals in HOL, strings written in this notation form an infinite family of defined constants. As such, their definitions are not directly available as theorems stored in a theory. Instead, a defining equation for any given string constant can be generated as required using the string library conversion string_CONV. This expects its term argument to be a non-empty ascii character string constant, for example "`a`", "`b`", or "`abc`". Given such a term, the conversion returns a theorem that defines this constant in terms of a shorter string. This is best illustrated by an example:

4

 #string_CONV "`abc`";;
 |- `abc` = STRING(ASCII F T T F F F F T)`bc`
 #string_CONV "`bc`";;
 |- `bc` = STRING(ASCII F T T F F F T F)`c`
 #string_CONV "`c`";;
 |- `c` = STRING(ASCII F T T F F F T T)``

Here, we have used string_CONV to iteratively unfold the formal definition of the string constant "`abc`". Note that string_CONV fails on the empty string "``".

1.2.4 Decision procedure for string equality

The string library includes an optimized conversion for proving equality or inequality of string constants This conversion is called string_EQ_COND. Its term argument is expected to be an equation between character strings of the following form:

    "`. . .` = `. . .`"

Given such an equation, string_EQ_CONV proves that it is equal to true if the string constants on the left and right-hand sides are identical or equal to false otherwise. The following session illustrates string_EQ_CONV in use:

5

 #string_EQ_CONV "`abc` = `abc`";;
 |- (`abc` = `abc`) = T
 #string_EQ_CONV "`abc` = `abd`";;
 |- (`abc` = `abd`) = F
 #string_EQ_CONV "`` = `abc`";;
 |- (`` = `abc`) = F
 #string_EQ_CONV "`abc` = `abcdef`";;
 |- (`abc` = `abcdef`) = F

Use of this conversion, which is highly optimised for speed, is to be preferred to other slower methods for proving equality or inequality of string constants, for example rewriting with the theorems STRING_11 and ASCII_11. The depth conversion ONCE_DEPTH_CONV may be used with string_EQ_CONV to reduce to true or false all the equations between string constants that occur in a term.

1.3 Using the library

The string library is loaded into a user’s HOL session using the function load_library (see the HOL manual for a general description of library loading). The first action in the load sequence initiated by load_library is to update the internal HOL search paths. A pathname to the string library is added to the search path, so that theorems may be autoloaded from the library theories ascii and string; and the HOL help search path is updated with a pathname to online help files for the ML functions in the library.

After updating search paths, the load sequence for string depends on the current state of the HOL session. If the system is in draft mode, the library theory string is added as a new parent to the current theory. If the system is not in draft mode, but the current theory is an ancestor of the string theory in the library (e.g. the user is in a fresh HOL session) then the string theory is made into the current theory. In both cases, the ML functions in the library are loaded into HOL and the theorems in the library theories are set up to be autoloaded on demand. The string library is at this point fully loaded into the user’s HOL session.

1.3.1 Example session

The following session shows how the string library may be loaded using load_library. Suppose, beginning in a fresh HOL session, the user wishes to create a theory foo whose parents include the theories in the string library. This may be done as follows:

1

 #new_theory `foo`;;
 () : void
 #load_library `string`;;

⋮

 Library `string` loaded.
 () : void

Loading the library while drafting the theory foo makes the library theory string into a parent of foo. The same effect could have been achieved (in a fresh session) by first loading the library and then creating foo:

1

 #load_library `string`;;

⋮

 Library `string` loaded.
 () : void
 #new_theory `foo`;;
 () : void

Here, the theory string is first made the current theory of the new session. It then automatically becomes a parent of foo when this theory is created by new_theory.

Now, suppose that foo has been created as shown above, and the user does some work in this theory, quits HOL and in a later session wishes to load the theory foo. This must be done by first loading the string library and then loading the theory foo.

1

 #load_library `string`;;

⋮

 Library `string` loaded.
 () : void
 #load_theory `foo`;;
 Theory foo loaded
 () : void

This sequence of actions ensures that the system can find the parent theory string when it comes to load foo, since loading the library updates the search path.

1.3.2 The load string function

The string library may in many cases simply be loaded into the system as illustrated by the examples given above. There are, however, certain situations in which the string library cannot be fully loaded at the time when the load_library is used. This occurs when the system is not in draft mode and the current theory is not an ancestor of the theory string. In this case, loading the library can and will update the search paths, as usual. But the string theory in the library can neither be made into a parent of the current theory nor can it be made the current theory. This means that autoloading from the library cannot at this stage be activated. Nor can the ML code in the library be loaded into HOL, since it requires access to some of the theorems in the library.

In the situation described above—when the system is not in draft mode and the current theory is not an ancestor of the theory string—the library load sequence defines an ML function called load_string in the current HOL session. If at a future point in the session the string theory (now accessible via the search path) becomes an ancestor of the current theory, this function can then be used to complete loading of the library. Evaluating

    load_string();;

in such a context loads the ML functions of the string library into HOL and activates autoloading from its theory files. The function load_string fails if the theory string is not a parent of the current theory.

Note that the function load_string becomes available when loading the string library only if the string theory at that point can neither be made into a new parent (i.e. the system is not in draft mode) nor be made the current theory.

ML Functions in the string Library

This chapter provides documentation on all the ML functions that are made available in HOL when the string library is loaded. This documentation is also available online via the help facility.

 ascii_EQ_CONV

ascii_EQ_CONV : conv

Synopsis

Decision-procedure for equality of ascii character constants.

Description

The conversion ascii_EQ_CONV implements a decision procedure for the equality of ascii character constants built up from boolean constants T and F using the constructor ASCII. The conversion expects its term argument to be an equation of the form:

   "ASCII a1 a2 a3 a4 a5 a6 a7 a8 = ASCII b1 b2 b3 b4 b5 b6 b7 b8"

where each of a1, ..., a8, b1, ..., b8 is either the constant T or the constant F. Given such a term, the conversion returns:

   |- (ASCII a1 a2 a3 a4 a5 a6 a7 a8 = ASCII b1 b2 b3 b4 b5 b6 b7 b8) = T

if ai is identical to bi for i from 1 to 8. Otherwise, the conversion returns:

   |- (ASCII a1 a2 a3 a4 a5 a6 a7 a8 = ASCII b1 b2 b3 b4 b5 b6 b7 b8) = F

Failure

Fails if applied to a term that is not of the form shown above.

See also

string_EQ_CONV.

 load_string

load_string : (void -> void)

Synopsis

Loads ML functions in the string library and sets up autoloading of theorems in the library.

Description

If the user is not in draft mode, or the current theory is not an ancestor of the library theory string, then the contents of the string library cannot immediately be made available when the library is loaded, since the theory string can neither be made a parent of the current theory nor loaded using load_theory. In this case, the library load sequence defines the function load_string. Calling this function when the library theory string is an ancestor of the current theory completes the library load sequence for the string library, making available the ML functions in the library and activating autoloading of theorems.

Failure

Fails if the theory string is not an ancestor of the current theory.

 string_CONV

string_CONV : conv

Synopsis

Axiom-scheme for character string constants.

Description

The conversion string_CONV expects its term argument to be a non-empty ascii character string constant (for example: "`a`", "`b`", "`abc`"). Given such a term, for example the term "`abc`", the conversion returns a theorem that defines this constant in terms of a shorter string:

   |- `abc` = STRING(ASCII F T T F F F F T)`bc`

where (ASCII F T T F F F F T) is the ascii character code for the first character in the supplied string (in this case `a`).

Failure

Fails if applied to a term that is not of the form shown above or if applied to the empty string "``".

See also

string_EQ_CONV.

 string_EQ_CONV

string_EQ_CONV : conv

Synopsis

Decision-procedure for equality of string constants.

Description

The conversion string_EQ_CONV expects its term argument to be an equation between character string constants (for example: "`a`", "`b`", "`abc`", etc). Given such a term, the conversion string_EQ_CONV returns:

   |- (lhs = rhs) = T

if lhs and rhs are identical character strings. Otherwise, the conversion returns:

   |- (lhs = rhs) = F

Failure

Fails if applied to a term that is not of the form specified above.

Example

#string_EQ_CONV "`aax` = `aay`";;
|- (`aax` = `aay`) = F

See also

ascii_EQ_CONV.

12 Chapter 2. ML Functions in the string Library

Pre-proved Theorems

The sections that follow list all the definitions and theorems in the string library. When the library is loaded, all the non-definitional theorems in the library are set up to autoload when their names are mentioned in ML. The definitions, however, do not autoload, since they are of very limited utility to the user. For convenience, definitions and theorems are listed separately. The name of the theory in which each theorem is stored is given in parentheses after the name of the theorem.

3.1 Definitions

ASCII_DEF (ascii)
|- !b0 b1 b2 b3 b4 b5 b6 b7.
ASCII b0 b1 b2 b3 b4 b5 b6 b7 =
ABS_ascii(Node(b0,b1,b2,b3,b4,b5,b6,b7)[])
ascii_ISO_DEF (ascii)
|- (!a. ABS_ascii(REP_ascii a) = a) /\
(!r.
 TRP
 (\v tl.
   (?b0 b1 b2 b3 b4 b5 b6 b7. v = b0,b1,b2,b3,b4,b5,b6,b7) /\
   (LENGTH tl = 0))
 r =
 (REP_ascii(ABS_ascii r) = r))
ascii_TY_DEF (ascii)
|- ?rep.
TYPE_DEFINITION
(TRP
 (\v tl.
   (?b0 b1 b2 b3 b4 b5 b6 b7. v = b0,b1,b2,b3,b4,b5,b6,b7) /\
   (LENGTH tl = 0)))
rep
STRING_DEF (string)
|- !a s. STRING a s = ABS_string(Node(INR a)[REP_string s])

14 Chapter 3. Pre-proved Theorems

string_ISO_DEF (string)
|- (!a. ABS_string(REP_string a) = a) /\
(!r.
 TRP
 (\v tl.
   (v = INL one) /\ (LENGTH tl = 0) \/
   (?a. v = INR a) /\ (LENGTH tl = SUC 0))
 r =
 (REP_string(ABS_string r) = r))
string_TY_DEF (string)
|- ?rep.
TYPE_DEFINITION
(TRP
 (\v tl.
   (v = INL one) /\ (LENGTH tl = 0) \/
   (?a. v = INR a) /\ (LENGTH tl = SUC 0)))
rep
``_DEF (string)
|- `` = ABS_string(Node(INL one)[]))

3.2 Theorems

ASCII_11 (ascii)
|- !b0 b1 b2 b3 b4 b5 b6 b7 b0' b1' b2' b3' b4' b5' b6' b7'.
(ASCII b0 b1 b2 b3 b4 b5 b6 b7 =
 ASCII b0' b1' b2' b3' b4' b5' b6' b7') =
(b0 = b0') /\
(b1 = b1') /\
(b2 = b2') /\
(b3 = b3') /\
(b4 = b4') /\
(b5 = b5') /\
(b6 = b6') /\
(b7 = b7')
ascii_Axiom (ascii)
|- !f.
?! fn.
 !b0 b1 b2 b3 b4 b5 b6 b7.
  fn(ASCII b0 b1 b2 b3 b4 b5 b6 b7) = f b0 b1 b2 b3 b4 b5 b6 b7
ascii_CASES (ascii)
|- !a. ?b0 b1 b2 b3 b4 b5 b6 b7. a = ASCII b0 b1 b2 b3 b4 b5 b6 b7

3.2. Theorems 15

ascii_Induct (ascii)
  |- !P.
      (!b0 b1 b2 b3 b4 b5 b6 b7. P(ASCII b0 b1 b2 b3 b4 b5 b6 b7)) ==>
      (!a. P a)
NOT_EMPTY_STRING (string)
  |- !a s. ~(STRING a s = ``)
NOT_STRING_EMPTY (string)
  |- !a s. ~(`` = STRING a s)
STRING_11 (string)
  |- !a s a' s'. (STRING a s = STRING a' s') = (a = a') /\ (s = s')
string_Axiom (string)
  |- !e f. ?! fn. (fn `` = e) /\ (!a s. fn(STRING a s) = f(fn s)a s)
string_CASES (string)
  |- !s. (s = ``) \/ (?s' a. s = STRING a s')
string_Induct (string)
  |- !P. P `` /\ (!s. P s ==> (!a. P(STRING a s))) ==> (!s. P s)

16 Chapter 3. Pre-proved Theorems

References

[1] University of Cambridge, DSTO and SRI International, The HOL System: DESCRIP-TION, (1991).

[2] T.F. Melham, ‘Automating Recursive Type Definitions in Higher Order Logic’, in: Current Trends in Hardware Verification and Automated Theorem Proving, edited by G. Birtwistle and P.A. Subrahmanyam (Springer-Verlag, 1989), pp. 341–386.

Index

"`…`" (string constants), 5–6

``_DEF, 14

ASCII_11, 2, 3, 6, 14

ascii_Axiom, 1–2, 14
ascii_CASES, 2, 14
ASCII_DEF, 13
ascii_EQ_CONV, 3, 9
ascii_Induct, 2, 15
ascii_ISO_DEF, 13
ascii_TY_DEF, 13

case analysis on type ascii, 2 on type string, 4

function definitions on type ascii, 2 on type string, 4

load_string, 8, 10
NOT_EMPTY_STRING, 4, 15
NOT_STRING_EMPTY, 4, 15

string constants, 5–6

STRING_11, 4, 6, 15
string_Axiom, 3–4, 15
string_CASES, 4, 15
string_CONV, 5–6, 10
STRING_DEF, 13
string_EQ_CONV, 6, 11
string_Induct, 4, 15
string_ISO_DEF, 14
string_TY_DEF, 14

structural induction, 4

theorems about the type ascii, 2 about the type string, 4