The HOL wordn Library

T. F. Melham W. Wong

University of Cambridge, Computer Laboratory

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

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

Contents

1 The wordn Library 1 2 ML Functions in the wordn Library 3 3 Pre-proved Theorems 23

3.1 The theory wordn base . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 3.2 The theory wordn bitops . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 3.3 The theory wordn num . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

Index 26 iv Contents

Chapter 1

The wordn Library

2 Chapter 1. The wordn Library

Chapter 2

ML Functions in the wordn Library

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

 define_wordn_bit_ops

define_wordn_bit_ops : thm -> int -> (thm) list

Synopsis

Defines a set of bitwise logical operators for the given word length.

Description

define_wordn_bit_ops wordn n, where wordn is the theorem returned by define_wordn_type

and n is the word length, defines four commonly used bitwise logical operators: NOTn, ANDn, ORn, and XORn. The definitions are stored in the current theory under the names: NOTn_DEF, ANDn_DEF, ORn_DEF and XORn_DEF and are returned in a list as the value of this function.

Failure

Fails if either it is not in draft mode, or the input theorem is not in the expected form or the type :wordn has not been defined.

Example

define_wordn_bit_ops word3 3 returns the following list of definitons:

   [ |- !b0 b1 b2. NOT3(WORD3[b0;b1;b2]) = WORD3(B_NOT[b0;b1;b2]);
     |- !b0 b1 b2 w.
        (WORD3[b0;b1;b2]) AND3 w = WORD3(B_AND[b0;b1;b2](BITS3 w));
     |- !b0 b1 b2 w.
        (WORD3[b0;b1;b2]) OR3 w = WORD3(B_OR[b0;b1;b2](BITS3 w));
     |- !b0 b1 b2 w.
        (WORD3[b0;b1;b2]) XOR3 w = WORD3(B_XOR[b0;b1;b2](BITS3 w)) ]

and they are stored in the current theory under the names NOT3_DEF, AND3_DEF, OR3_DEF and XOR3_DEF, repectively.

See also

prove_bit_opthms, wordn_bit_ops.
 define_wordn_type
define_wordn_type : string -> int -> thm

Synopsis Description Failure Example Uses Comments See also

 define_word_val
define_word_val : int -> thm list

Synopsis

Defines two constants for converting between the type :wordn and :num.

Description

define_word_val takes a single argument, a positive integer n. It defines two logical constants for converting between the types :wordn and :num. The constants are named NVALn and NWORDn, and they have the types :wordn -> num and :num -> wordn, respectively. Natural numbers are represented by an n-bit word in a big-endian format, for example, #001 denotes 1 as a 3-bit word, and the following expressions are true:

   NVAL3 #001 = 1

define word val 5

   NWORD3 1 = #001

These constants are defined in terms of VAL and WORDN, which are the generic conversion functions between the represention type of the n-bit words, namely :(bool)list, and the type :num. The definitions of these generic conversion functions are as follows:

   |- (VAL[] = 0) /\
      (!b bs. VAL(CONS b bs) = ((BV b) * (2 EXP (LENGTH bs))) + (VAL bs))
   |- !n m. (LENGTH(WORDN n m) = n) /\ (VAL(WORDN n m) = m MOD (2 EXP n))

For a particular word length n, the conversion from :wordn to :num is defined to be

   !w. NVALn w = VAL(BITSn w)

and the conversion from :num to :wordn is defined to be

   !m. NWORDn m = WORDn(WORDN n m)

The functions NVALn converting words to natural numbers are one-one and onto, but the functions NWORDn are not one-one due to the finite length of a word. From the definition of WORDN, the theorem

   |- !m. NWORDn m = NWORDn (m MOD (2 EXP n))

can be deduced. The conversions can be better characterized by the theorem

   |- (!w. NWORDn(NVALn w) = w) /\
      (!m. m < (2 EXP m) ==> (NVALn(NWORDn m) = m))

which can be obtained by calling the function prove_word_val.

Failure

Fails if the type :wordn of the specified word length n has not been defined.

Example

The following HOL session illustrates the use of this function:

   # let [NVAL3_DEF; NWORD3_DEF] = define_word_val 3;;
   NVAL3_DEF = |- !w. NVAL3 w = VAL(BITS3 w)
   NWORD3_DEF = |- !n. NWORD3 n = WORD3(WORDN 3 n)

See also

define_wordn_type, prove_word_val.

 define_word_partition
define_word_partition : int -> int -> thm

Synopsis

Defines operators for splitting and joining words.

Description

define_word_partition m n defines the following two constants: JOIN_m_n which has type

:(wordm # wordn) -> wordl and SPLIT_m_n which has type :wordl -> (wordm # wordn)

where l = m + n. They are specified by the following theorem:

   |- (!wm wn. SPLIT_m_n(JOIN_m_n(wm,wn)) = wm,wn) /\
      (!w. JOIN_m_n(SPLIT_m_n w) = w)

which is stored in the current theory as a definition under the name PARTITION_m_n and is returned as the value of this function.

Failure

Fails if either it is not in draft mode or any of the word types involved has not been defined.

Example

define_word_partition 3 5 returns the following definition:

   |- (!wm wn. SPLIT_3_5(JOIN_3_5 (wm,wn)) = wm,wn) /\
      (!w. JOIN_3_5(SPLIT_3_5 w) = w)

where wm is of type :word3, wn is of type :word5 and w is :word8.

 new_wordn_definition
new_wordn_definition : (bool -> thm -> string -> conv)

Synopsis

Defines a function over the types of n-bit words.

Description

The function new_wordn_definition provides a facility for defining functions on the types of n-bit words. It takes four arguments. The first is a boolean flag which indicates if the function being defined will be an infix or not. The second is a theorem stating the existence of functions on the type of n-bit words; this must be a theorem returned by prove_function_defn_thm. The third argument is a name under which the resulting definition will be saved in the current theory segment. And the fourth argument is a term giving the desired function definition. The value returned by new_wordn_definiton is a theorem stating the definition requested by the user. This theorem is derived by formal proof from an instance of the theorem given as the second argument.

Failure

Failure occurs if HOL cannot prove there is a function satisfying the specification supplied as the last argument, or if any other condition for making constant specification (ie, the failure conditions of new_specification) is violated.

Example

Suppose that the type of 3-bit word has been defined by calling define_wordn_type 3, and the theorem returned by this type definition is bound to the name word3. Then, a call to the function prove_function_defn_thm with the theorem word3 will result in the following theorem:

   word3_FNDEF |- !f. ?! fn. !b0 b1 b2. fn(WORD3[b0;b1;b2]) = f b0 b1 b2

which is in the form expected by the function new_wordn_definition. The following definition will define a new constant on the type :word3:

   #let BIT1 = new_wordn_definition false word3_FNDEF `BIT1`
   #    "BIT1(WORD3[b0;b1;b2]) = b1";;
   BIT1 =
   |- !b0 b1 b2. BIT1(WORD3[b0;b1;b2]) = b1

See also

define_wordn_type, new_specification, new_recursive_definition,
prove_function_defn_thm, use_wordn.

 prove_BITS_one_one

prove_BITS_one_one : thm -> thm

8 Chapter 2. ML Functions in the wordn Library

Synopsis Description Failure Example Uses Comments See also

 prove_BITS_onto
prove_BITS_onto : thm -> thm

Synopsis Description Failure Example Uses Comments See also

 prove_BITS_WORD
prove_BITS_WORD : thm -> thm

Synopsis

Proves a theorem for reducing BITSn(WORDn [...]) to [...].

Description

prove_BITS_WORDS takes a theorem returned by define_wordn_type and deduces a theorem which is an instance of the second conjunct of the type definition theorem. This theorem is usually used in rewriting to simplify terms containing the expression BITSn(WORDn [...].

Failure

Fails if the input theorem is not in the expected form.

Example

prove_BITS_WORD word3 where word3 is the theorem
   |- (!w. WORD3(BITS3 w) = w) /\
      (!l. (LENGTH l = 3) = (BITS3(WORD3 l) = l))

returns the following theorem:

   |- !b0 b1 b2. BITS3(WORD3[b0; b1; b2]) = [b0; b1; b2]

 prove_bit_op_thms

prove_bit_op_thms : (int -> thm list)

Synopsis

Proves some basic theorems about the bitwise logical operators.

Description

prove_bit_op_thms takes a single integer as its argument and returns a list of theorems about the basic properties of the bitwise logical operators. These theorems are the selfinversion of the NOTn operator, the symmetry and associativity of the ANDn, ORn and XORn operators. They are also stored in the current theory under the names NOTn, ANDn_SYM,

ORn_SYM, XORn_SYM, ANDn_ASSOC, ORn_ASSOC and XORn_ASSOC.

Failure

Fails if either it is not in draft mode, or any of the operators has not been defined.

Example

prove_bit_op_thms 3 returns the following list of theorems and stores them in the current

theory under the names NOT3, AND3_SYM, OR3_SYM, XOR3_SYM, AND3_ASSOC, OR3_ASSOC and

XOR3_ASSOC, respectively.

   [ |- !w. NOT3(NOT3 w) = w;

10 Chapter 2. ML Functions in the wordn Library

|- !w1 w2. w1 AND3 w2 = w2 AND3 w1;
|- !w1 w2. w1 OR3 w2 = w2 OR3 w1;
|- !w1 w2. w1 XOR3 w2 = w2 XOR3 w1;
|- !w1 w2 w3. w1 AND3 (w2 AND3 w3) = (w1 AND3 w2) AND3 w3;
|- !w1 w2 w3. w1 OR3 (w2 OR3 w3) = (w1 OR3 w2) OR3 w3;
|- !w1 w2 w3. w1 XOR3 (w2 XOR3 w3) = (w1 XOR3 w2) XOR3 w3]

See also

define_wordn_bit_ops, wordn_bit_ops.
prove_function_defn_thm
prove_function_defn_thm : thm -> thm

Synopsis Description Failure Example Uses Comments See also

prove_LENGTH_BITS_thm
prove_LENGTH_BITS_thm : thm -> thm

prove NWORD MOD 11

Synopsis Description Failure Example Uses Comments See also

 prove_NWORD_MOD
prove_NWORD_MOD : int -> thm

Synopsis

Proves a theorem stating the periodicity of the function NWORDn.

Description

prove_NWORD_MOD n proves a theorem about the num-to-word conversion NWORDn which takes the following form:

   |- !m. NWORDn m = NWORDn (m MOD e)

where e is a constant number whose value equals to 2 EXP n.

Failure

Fails if the type :wordn or the conversion function NWORDn has not been defined.

Example

The following HOL session illustrates the use of this function:

   # let word3_NWORD_MOD = prove_NWORD_MOD 3;;
   word3_NWORD_MOD = |- !m. NWORD3 m = NWORD3(m MOD 8)

See also

define_wordn_type, define_word_val, prove_word_val.

 prove_wordn_cases_thm
prove_wordn_cases_thm : thm -> thm

Synopsis Description Failure Example Uses Comments See also

 prove_wordn_const_cases
prove_wordn_const_cases : thm -> thm

Synopsis

Exhaustive cases theorem for wordn constants.

Description

prove_wordn_const_cases derives an exhaustive cases theorem for constants of type :wordn. Use only for small n. The input is a theorem of the form returned by prove_word_cases_thm:

    |- !w. ?b0...bn-1. w = WORDn [b0;...;bn-1]

The corresponding output has the form:

   |- !w. ((w = #0...0) \/ ...)  \/ (... \/ w = #1...1)

Failure Example

prove_wordn_const_cases word3_CASES returns the following theorem:
   |- !w.

prove wordn induction thm 13

(((w = #000) \/ (w = #001)) \/ (w = #010) \/ (w = #011)) \/
((w = #100) \/ (w = #101)) \/
(w = #110) \/
(w = #111)

See also

prove_wordn_cases_thm
prove_wordn_induction_thm
prove_wordn_induction_thm : thm -> thm

Synopsis Description Failure Example Uses Comments See also

prove_WORD_one_one
prove_WORD_one_one : thm -> thm

14 Chapter 2. ML Functions in the wordn Library

Synopsis Description Failure Example Uses Comments See also

 prove_WORD_onto
prove_WORD_onto : thm -> thm

Synopsis Description Failure Example Uses Comments See also

 prove_word_val
prove_word_val : int -> thm

Synopsis

Proves the theorem characterizing the conversion functions between the types :wordn and

:num.

Description

prove_word_val takes a natural number as its single argument. It proves a theorem which characterizes the conversion functions NVALn and NWORDn. The theorem is returned as the function value, and it takes the following form:

   |- (!w. NWORDn(NVALn w) = w) /\
      (!m. m < (2 EXP n) ==> (NVALn(NWORDn m) = m))

Failure

Fails if the type :wordn or the conversion functions :NVALn and :NWORDn have not been defined.

Example

The following HOL session illustrates the use of this function:

   # let WORD_VAL_3 = save_thm(`WORD_VAL_3`, prove_word_val 3);;
   WORD_VAL_3 =
   |- (!w. NWORD3(NVAL3 w) = w) /\
      (!n. n < (2 EXP 3) ==> (NVAL3(NWORD3 n) = n))

See also

define_wordn_type, define_word_val.

 use_wordn

use_wordn : int -> (thm)list

Synopsis

Defines the type of n-bit words and proves some basic theorems.

Description

The function use_wordn is one of the top level user functions of the wordn library. It provides a facility to define the type of n-bit words and to prove some basic theorems on this type. When the user needs to use n-bit words in an application, he/she can simply make a call to use_wordn with a single argument n. This will define the type :wordn, and a list of basic theorems about the type are returned. use_wordn combines the function define_wordn_type and the following functions for proving theorems

about the type of n-bit words: prove_function_defn_thm, prove_wordn_induction_thm,

16 Chapter 2. ML Functions in the wordn Library

prove_wordn_cases_thm, prove_BITS_one_one, prove_BITS_onto, prove_WORD_one_one, prove_WORD_onto,
prove_LENGTH_BITS_thm.

Failure

Failure occurs if any of the functions invoked fails.

Example

The HOL session below illustrates the use of the function use_wordn:

# let [word3; word3_BITS_11; word3_BITS_onto;
# word3_WORD_11; word3_WORD_onto; word3_LENGTH_BITS;
# word3_FNDEF; word3_INDUCT; word3_CASES] =
# use_wordn 3;;
word3 =
|- (!w. WORD3(BITS3 w) = w) /\
   (!l. (LENGTH l = 3) = (BITS3(WORD3 l) = l))
word3_BITS_11 = |- !w' w. (BITS3 w = BITS3 w') ==> (w = w')
word3_BITS_onto = |- !l. (LENGTH l = 3) ==> (?w. BITS3 w = l)
word3_WORD_11 =
|- !l l'.
    (LENGTH l = 3) /\ (LENGTH l' = 3) ==>
    (WORD3 l = WORD3 l') ==>
    (l = l')
word3_WORD_onto = |- !w. ?l. (LENGTH l = 3) /\ (WORD3 l = w)
word3_LENGTH_BITS = |- !w. LENGTH(BITS3 w) = 3
word3_FNDEF = |- !f. ?! fn. !b0 b1 b2. fn(WORD3[b0;b1;b2]) = f b0 b1 b2
word3_INDUCT = |- !P. (!b0 b1 b2. P(WORD3[b0;b1;b2])) ==> (!w. P w)
word3_CASES = |- !w. ?b0 b1 b2. w = WORD3[b0;b1;b2]

See also

define_wordn_type, prove_function_defn_thm, prove_wordn_induction_thm,
prove_wordn_cases_thm, prove_BITS_one_one, prove_BITS_onto, prove_WORD_one_one,
prove_WORD_onto, prove_LENGTH_BITS_thm.

wordn_bit_ops

wordn_bit_ops : thm -> int -> (thm)list

Synopsis

Defines bitwise operators and proves some basic theorems about them. wordn CASES TAC 17

Description

wordn_bit_ops wordn n, where wordn is the theorem returned by define_wordn_type and

n is the word length, defines a set of commonly used bitwise logical operators and proves some basic theorems about these operators. It combines the functions of define_wordn_bit_ops,

and prove_bit_op_thms.

Failure

Fails if either it is not in draft mode, or the input theorem is not in the expected form or the type :wordn has not been defined.

Example

wordn_bit_ops word3 3 returns the following list of definitions and theorems:

[ |- !b0 b1 b2. NOT3(WORD3[b0;b1;b2]) = WORD3(B_NOT[b0;b1;b2]);
|- !b0 b1 b2 w.
   (WORD3[b0;b1;b2]) AND3 w = WORD3(B_AND[b0;b1;b2](BITS3 w));
|- !b0 b1 b2 w.
   (WORD3[b0;b1;b2]) OR3 w = WORD3(B_OR[b0;b1;b2](BITS3 w));
|- !b0 b1 b2 w.
   (WORD3[b0;b1;b2]) XOR3 w = WORD3(B_XOR[b0;b1;b2](BITS3 w));
|- !w. NOT3(NOT3 w) = w;
|- !w1 w2. w1 AND3 w2 = w2 AND3 w1;
|- !w1 w2. w1 OR3 w2 = w2 OR3 w1;
|- !w1 w2. w1 XOR3 w2 = w2 XOR3 w1;
|- !w1 w2 w3. w1 AND3 (w2 AND3 w3) = (w1 AND3 w2) AND3 w3;
|- !w1 w2 w3. w1 OR3 (w2 OR3 w3) = (w1 OR3 w2) OR3 w3;
|- !w1 w2 w3. w1 XOR3 (w2 XOR3 w3) = (w1 XOR3 w2) XOR3 w3 ]

See also

define_wordn_bit_ops, prove_bit_op_thms.

wordn_CASES_TAC

wordn_CASES_TAC : term -> thm_tactic

Synopsis

Instantiates variables of type :wordn with a list of bits.

Description

The tactic wordn_CASES_TAC instantiates occurrences of a variable of type :wordn in the goal with a list of bits. It takes, as its arguments, a term which indicates which variable is to be instantiated and a theorem which should in the form returned by prove_wordn_cases. The specification of wordn_CASES_TAC is:

              A ?- t[w]
   =============================== wordn_CASES_TAC "w" wordn_CASES
      A ?- t[WORDn[b0';...;bn-1']/w]

where wordn_CASES is the following theorem:

   |- !w. ?b0...bn-1. w = WORDn[b0;...bn-1]

This function specializes the universally quantified variable in the theorem wordn_CASES with the given term which should match the variable required to be instantiated in the goal. It then eliminaates the existentially quantified vairables b0,...,bn-1 by choosing some variants which are not free in the assumptions; normally these are just b0,...,bn-1. It then substitutes the right-hand side of the equation for the occurrences of the variable w in the goal.

Failure

Fails if the substitution cannot be performed due to no matching variable of the correct type is found or other reasons as given in the failure conditions of CHOOSE_TAC and

SUBST1_TAC.

Example

Suppose that one wants to solve the following goal:

   "!w. LENGTH(BITS3 w) = 3"
  The tactic GEN_TAC THEN wordn_CASES_TAC "w" word3_CASES may be used to transform

it to

   "LENGTH(BITS3(WORD3[b0;b1;b2])) = 3"

See also

wordn_X_CASES_TAC, prove_wordn_cases_thm, CHOOSE_TAC, SUBST1_TAC.

 wordn_CONV

wordn_CONV : conv

Synopsis

Definition scheme for wordn constants.

Description

wordn_CONV "#b1...bn" returns
   |- #b1...bn = WORDn [b1;...;bn]

Failure

Example

wordn_CONV "#110" returns the following theorem:

   |- #110 = WORD3 [T; T; F]

See also

define_wordn_type, wordn_NVAL_CONV, wordn_NWORD_CONV.

 wordn_EQ_CONV

wordn_EQ_CONV : thm -> conv

Synopsis

Derives a theorem stating the equality of two words.

Description

wordn_EQ_CONV wordn "w1 = w2" returns a theorem
   |- (w1 = w2) = T

if and only if w1 is equal to w2, otherwise, it returns

   |-  (w1 = w2) = F

wordn is the type definition theorem returned by define_wordn_type.

Failure

Example

wordn_EQ_CONV word3 "#010 = #110";; return the following theorem:
   |- (#010 = #110) = F

See also

define_wordn_type, wordn_CONV.

 wordn_NVAL_CONV
wordn_NVAL_CONV : conv

Synopsis

Derives a theorem stating the value of a word.

Description

wordn_NVAL_CONV takes a term in the form "NVALn #..." and derives a theorem stating the value of the given word when interpreted as natural number in a big-endian format. The length of the string following the hash # should be n, and it should consist of only the digits 0 and 1.

Failure

Fails if the type :wordn or the constant NVALn has not been defined, or the string is not in the form specified above.

Example

The HOL session below illustrates the use of this conversion:

   # let word3_val_6 = wordn_NVAL_CONV "NVAL3 #110";;
   word3_val_6 = |- NVAL3 #110 = 6

See also

define_wordn_type, define_word_val, wordn_NWORD_CONV.

 wordn_NWORD_CONV
wordn_NWORD_CONV : conv

Synopsis

Derives a theorem stating the representation of a natural number in an n-bit word.

Description

wordn_NWORD_CONV takes a term in the form "NWORDn m" and derives a theorem stating the n-bit word representing the natural number m as below:

|- NWORDn m = #...

If m is greater than the maximium that an n-bit word can represent, m MOD (2 EXP n) will be used to work out the n-bit word instead. By virtue of the theorem returned by prove_NWORD_MOD, the above theorem is still valid.

Failure

Fails if the type :wordn or the function NWORDn has not been defined.

Example

The HOL session below illustrates the use of this conversion:

   # wordn_NWORD_CONV "NWORD3 6";;
   |- NWORD3 6 = #110
   # wordn_NWORD_CONV "NWORD3 16";;
   |- NWORD3 16 = #000

See also

define_wordn_type, define_word_val, prove_NWORD_MOD, wordn_NVAL_CONV.

 wordn_X_CASES_TAC

wordn_X_CASES_TAC : term -> thm -> (term list) -> tactic

Synopsis

Instantiates variables of type :wordn with a list of bits.

Description

The tactic wordn_X_CASES_TAC instantiates occurrences of a variable of type :wordn in the goal with a list of bits. It takes, as its arguments, a term which indicates which variable is to be instantiated, a theorem which should in the form returned by prove_wordn_cases and a list of terms which is used as the bits in the instantiation. The specification of

wordn_X_CASES_TAC is:
              A ?- t[w]
   =============================== wordn_X_CASES_TAC "w" wordn_CASES
      A ?- t[WORDn[c0;...;cn-1]/w]       ["c0";..."cn-1"]

where wordn_CASES has the following theorem:

   |- !w. ?b0...bn. w = WORDn[b0;...bn]

This function specializes the universally quantified variable in the theorem wordn_CASES with the given term which should match the variable required to be instantiated in the goal. It then eliminates the existentially quantified vairables b0,...,bn-1 using the terms given in the last argument as specific witness. It then substitutes the right-hand side of the equation for the occurrences of the variable w in the goal.

Failure

Fails if the substitution cannot be performed due to no matching variable of the correct type is found, or the supplied terms involve variables which are free in the assumption or other reasons as given in the failure conditions of X_CHOOSE_TAC and SUBST1_TAC.

Example

Suppose that one wants to solve the following goal:

   "!w. LENGTH(BITS3 w) = 3"
The tactic GEN_TAC THEN wordn_X_CASES_TAC "w" word3_CASES ["c1";"c2";"c3"] may be

used to transform it to

   "LENGTH(BITS3(WORD3[c1;c2;c3])) = 3"

See also

wordn_CASES_TAC, prove_wordn_cases_thm, X_CHOOSE_TAC, SUBST1_TAC.

Chapter 3

Pre-proved Theorems

The sections that follow list all theorems in the wordn library, including definitions. The theorems are grouped into sections according to the theory segment in which they are stored. The reader may therefore have to consult more than one section when searching for any particular theorem.

When the wordn library is loaded, all the theorems listed in this chapter (including definitions) are set up to autoload when their names are mentioned in ML.

3.1 The theory wordn base

EXISTS_wordn_REP (wordn base)
|- !n. ?l. (\l. LENGTH l = n)l
wordn_ABS_REP (wordn base)
|- !n.
(?rep. TYPE_DEFINITION(\l'. LENGTH l' = n)rep) ==>
(?REP ABS.
  (!w. ABS(REP w) = w) /\ (!l. (LENGTH l = n) = (REP(ABS l) = l)))
wordn_FN_DEF_THM (wordn base)
|- !n ABS REP.
(!a. ABS(REP a) = a) /\ (!r. (LENGTH r = n) = (REP(ABS r) = r)) ==>
(!f. ?! fn. !r. (LENGTH r = n) ==> (fn(ABS r) = f r))

3.2 The theory wordn bitops

B_AND_ASSOC (wordn bitops)
|- !l1 l2 l3.
(LENGTH l1 = LENGTH l2) /\ (LENGTH l2 = LENGTH l3) ==>
(B_AND l1(B_AND l2 l3) = B_AND(B_AND l1 l2)l3)
B_AND_DEF (wordn bitops)
|- (!l. B_AND[]l = []) /\
(!x1 l1 l2. B_AND(CONS x1 l1)l2 = CONS(x1 /\ HD l2)(B_AND l1(TL l2)))

24 Chapter 3. Pre-proved Theorems

B_AND_SYM (wordn bitops)
  |- !l1 l2. (LENGTH l1 = LENGTH l2) ==> (B_AND l1 l2 = B_AND l2 l1)
B_NOT (wordn bitops)
  |- !l. B_NOT(B_NOT l) = l
B_NOT_DEF (wordn bitops)
  |- (B_NOT[] = []) /\ (!x l. B_NOT(CONS x l) = CONS~x(B_NOT l))
B_OR_ASSOC (wordn bitops)
  |- !l1 l2 l3.
      (LENGTH l1 = LENGTH l2) /\ (LENGTH l2 = LENGTH l3) ==>
      (B_OR l1(B_OR l2 l3) = B_OR(B_OR l1 l2)l3)
B_OR_DEF (wordn bitops)
  |- (!l. B_OR[]l = []) /\
     (!x1 l1 l2. B_OR(CONS x1 l1)l2 = CONS(x1 \/ HD l2)(B_OR l1(TL l2)))
B_OR_SYM (wordn bitops)
  |- !l1 l2. (LENGTH l1 = LENGTH l2) ==> (B_OR l1 l2 = B_OR l2 l1)
B_XOR_ASSOC (wordn bitops)
  |- !l1 l2 l3.
      (LENGTH l1 = LENGTH l2) /\ (LENGTH l2 = LENGTH l3) ==>
      (B_XOR l1(B_XOR l2 l3) = B_XOR(B_XOR l1 l2)l3)
B_XOR_DEF (wordn bitops)
  |- (!l. B_XOR[]l = []) /\
     (!x1 l1 l2. B_XOR(CONS x1 l1)l2 = CONS~(x1 = HD l2)(B_XOR l1(TL l2)))
B_XOR_SYM (wordn bitops)
  |- !l1 l2. (LENGTH l1 = LENGTH l2) ==> (B_XOR l1 l2 = B_XOR l2 l1)
XOR_ASSOC (wordn bitops)
  |- !x y z. ~(x = ~(y = z)) = ~(~(x = y) = z)

3.3 The theory wordn num

BV (wordn num)
  |- !b. BV b = (b => SUC 0 | 0)
VAL (wordn num)
  |- (VAL[] = 0) /\
     (!b bs. VAL(CONS b bs) = ((BV b) * (2 EXP (LENGTH bs))) + (VAL bs))

3.3. The theory wordn num 25

VAL_LESS (wordn num)
  |- !l. (VAL l) < (2 EXP (LENGTH l))
VAL_LESS_EQ (wordn num)
  |- !l. (VAL l) <= ((2 EXP (LENGTH l)) - 1)
VAL_ONE_ONE (wordn num)
  |- !l1 l2. (LENGTH l1 = LENGTH l2) ==> (VAL l1 = VAL l2) ==> (l1 = l2)
VAL_ONTO (wordn num)
  |- !l. ?n. VAL l = n
VAL_ONTO_LEMMA (wordn num)
  |- !m n. n < (2 EXP m) ==> (?l. (LENGTH l = m) /\ (n = VAL l))
WORDN (wordn num)
  |- !n m. (LENGTH(WORDN n m) = n) /\ (VAL(WORDN n m) = m MOD (2 EXP n))
WORDN_0 (wordn num)
  |- (!m. WORDN 0 m = []) /\ (!n. WORDN(SUC n)0 = CONS F(WORDN n 0))
WORDN_MOD (wordn num)
  |- !m n. WORDN n m = WORDN n(m MOD (2 EXP n))
WORDN_VAL (wordn num)
  |- !l. WORDN(LENGTH l)(VAL l) = l

Index

B_AND_ASSOC, 23
B_AND_DEF, 23
B_AND_SYM, 24
B_NOT, 24
B_NOT_DEF, 24
B_OR_ASSOC, 24
B_OR_DEF, 24
B_OR_SYM, 24
B_XOR_ASSOC, 24
B_XOR_DEF, 24
B_XOR_SYM, 24

BV, 24

define_word_partition, 6
define_word_val, 4
define_wordn_bit_ops, 3
define_wordn_type, 4
EXISTS_wordn_REP, 23
new_wordn_definition, 6
prove_bit_op_thms, 9
prove_BITS_one_one, 7
prove_BITS_onto, 8
prove_BITS_WORD, 8
prove_function_defn_thm, 10
prove_LENGTH_BITS_thm, 10
prove_NWORD_MOD, 11
prove_WORD_one_one, 13
prove_WORD_onto, 14
prove_word_val, 14
prove_wordn_cases_thm, 12
prove_wordn_const_cases, 12

                                       prove_wordn_induction_thm, 13
                                       use_wordn, 15
                                       VAL, 24
                                       VAL_LESS, 25
                                       VAL_LESS_EQ, 25
                                       VAL_ONE_ONE, 25
                                       VAL_ONTO, 25
                                       VAL_ONTO_LEMMA, 25
                                       WORDN, 25
                                       WORDN_0, 25
                                       wordn_ABS_REP, 23
                                       wordn_bit_ops, 16
                                       wordn_CASES_TAC, 17
                                       wordn_CONV, 18
                                       wordn_EQ_CONV, 19
                                       wordn_FN_DEF_THM, 23
                                       WORDN_MOD, 25
                                       wordn_NVAL_CONV, 20
                                       wordn_NWORD_CONV, 20
                                       WORDN_VAL, 25
                                       wordn_X_CASES_TAC, 21
                                       XOR_ASSOC, 24