Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
To: info-hol@edu.uidaho.cs.ted
Cc: Wai.Wong@uk.ac.cam.cl
Subject: Re: Labeling assumptions in the asl
In-Reply-To: Your message of Sun, 10 May 92 16:58:40 -0700. <9205102358.AA29794@toadflax.cs.ucdavis.edu>
Date: Mon, 11 May 92 12:47:17 +0100
From: Wai.Wong@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.990:11.04.92.11.47.29"@cl.cam.ac.uk>

It has been sometime since the discussion of wordn library appeared
here. I have done some work on it, based on an earlier attempt by
Tom Melham. I think it is at a state it can be used in some real
works, at least, it is enough for my main work for now. I have to
stop working on it and go back to my own main work to make some
progress. This is also a good time for comments and suggestions,
therefore, I post a summary of what is in the wordn library at the
moment. I welcome any suggestions and comments, but I'm afraid I
cannot implement any immediately. Whether any suggestion will be
implemented depends on:
  1. how difficult it is to implement it?
  2. how long does it take to implement it?
  3. how many people require it?
  4. do I have the time to do it?
Here is summary:

The wordn library consists of several theories whose ancestry
is as below:

	wordn_base    wordn_bitops   wordn_num
	     |             |              |
	     |             |              |
	     ------------------------------
	                   |
	                 wordn

Each thoery may have a number of definitions and/or theorems stored in it,
and there may also be some derived rules and conversions associated with it.
A brief description of each theory is given below, and the result of a
test run is listed at the end as an example.

wordn_base:
	This thoery is for defining the types of n-bit words. For a
speific word length N, a type, namely :wordN, can be defined, together
with a constructor WORDN and a destructor BITSN. The underlying
representation type of :wordN is :(bool)list and the subset of
:(bool)list which represents :wordN satisfies (\l. length l = N).
As far as the users concern, the representation of :wordn is hidden
unless you really want to work with :(bool)list rather than :wordn.

	There are serval theorems stored in this theory, but they
should be of no interest to the users. There are also a number of ML
functions implementing derived rules and conversions, such as proving
induction theorem, and so on.

wordn_bitops:
	This theory is for defining bitwise operators and proving
theorems about them. There are ML functions performing these tasks. To
define a (binary) bitwise operator on a type :wordN, the user should
supply a function of type :bool->bool->bool, eg. $/\ and the name of
the new constant as a string, eg. `ANDN`. A constant
ANDN:wordN->wordN->wordN will be defined for you. To prove a theorem
stating the symmetry of the operator ANDN, the user should supply the
definiton and a theorem stating the symmetry of the underlying
operator, namely CONJ_SYM, then a theorem
 |- !w1 w2. w1 ANDN w2 = w2 ANDN w1
will be derived. There are also function for defining constant to
split a word into two parts and to join two words into a longer word.
For example, JOIN_n_m:(wordn # wordm) -> wordl and
 SPLIT_n_m:wordl -> (wordn # wordn).

The above two theories and associated functions treat a word just as a
bit vector. They do not concern with how these bits are interpreted.
In contrast, the theory wordn_num maps n-bit words to natural numbers.

wordn_num:
	This theory interprets n-bit words as natural numbers in a
big-endian format, ie. #011 = 3. Constants for mapping between :wordn
and :num can be defined. And there are conversions for the some
purposes.

wordn:
	This theory contains no definition nor theorems. It just acts
as a common descendant for all the theories.

Since the library has been organized as modules, theories implementing
other interpretations, eg. integers and little-endian, can be added
without difficuty.

Below is a test run which excercises all the ML functions in the
library:

#load_library`wordn`;;
Loading library `wordn` ...
Updating search path.
Updating help search path......
.Theory wordn loaded
.....................................................................() : void
Library `wordn` loaded.

#timer true;;
false : bool
Run time: 0.0s

#new_theory `test2`;;
() : void
Run time: 0.0s
Intermediate theorems generated: 1

#let word3 = define_wordn_type `word3` 3;;
word3 = 
|- (!w. WORD3(BITS3 w) = w) /\
   (!l. (LENGTH l = 3) = (BITS3(WORD3 l) = l))
Run time: 0.4s
Intermediate theorems generated: 9

#let word3_BITS_11 = prove_BITS_one_one word3;;
word3_BITS_11 = |- !w' w. (BITS3 w = BITS3 w') ==> (w = w')
Run time: 0.1s
Intermediate theorems generated: 11

#let word3_BITS_onto = prove_BITS_onto word3;;
word3_BITS_onto = |- !l. (LENGTH l = 3) ==> (?w. BITS3 w = l)
Run time: 0.0s
Intermediate theorems generated: 7

#let word3_WORD_11 = prove_WORD_one_one word3;;
word3_WORD_11 = 
|- !l l'.
    (LENGTH l = 3) /\ (LENGTH l' = 3) ==>
    (WORD3 l = WORD3 l') ==>
    (l = l')
Run time: 0.1s
Intermediate theorems generated: 17

#let word3_WORD_onto = prove_WORD_onto word3;;
word3_WORD_onto = |- !w. ?l. (LENGTH l = 3) /\ (WORD3 l = w)
Run time: 0.1s
Intermediate theorems generated: 11

#let word3_LENGTH_BITS = prove_LENGTH_BITS_thm word3;;
word3_LENGTH_BITS = |- !w. LENGTH(BITS3 w) = 3
Run time: 0.0s
Intermediate theorems generated: 8

#let word3_FNDEF = prove_function_defn_thm word3;;
word3_FNDEF = |- !f. ?! fn. !b0 b1 b2. fn(WORD3[b0;b1;b2]) = f b0 b1 b2
Run time: 1.2s
Intermediate theorems generated: 108

#let word3_INDUCT = prove_wordn_induction_thm word3_FNDEF;;
word3_INDUCT = |- !P. (!b0 b1 b2. P(WORD3[b0;b1;b2])) ==> (!w. P w)
Run time: 0.7s
Intermediate theorems generated: 59

#let word3_CASES = prove_wordn_cases_thm word3_INDUCT;;
word3_CASES = |- !w. ?b0 b1 b2. w = WORD3[b0;b1;b2]
Run time: 0.2s
Intermediate theorems generated: 19

#let MID_DEF = new_wordn_definition false word3_FNDEF `MID_DEF`
#    "MID (WORD3[b0;b1;b2]) = b1";;
MID_DEF = |- !b0 b1 b2. MID(WORD3[b0;b1;b2]) = b1
Run time: 1.7s
Intermediate theorems generated: 115

#let word3_3 = wordn_CONV "#011";;
word3_3 = |- #011 = WORD3[F;T;T]
Run time: 0.0s
Intermediate theorems generated: 1

#let word3_CCASES = prove_wordn_const_cases word3_CASES;;
word3_CCASES = 
|- !w.
    (((w = #000) \/ (w = #001)) \/ (w = #010) \/ (w = #011)) \/
    ((w = #100) \/ (w = #101)) \/
    (w = #110) \/
    (w = #111)
Run time: 0.9s
Garbage collection time: 4.1s
Intermediate theorems generated: 126

#let word3_EQ = wordn_EQ_CONV word3 "#010 = #011";;
word3_EQ = |- (#010 = #011) = F
Run time: 1.1s
Intermediate theorems generated: 112

#let word3_BITS_WORD = prove_BITS_WORD word3;;
word3_BITS_WORD = |- !b0 b1 b2. BITS3(WORD3[b0;b1;b2]) = [b0;b1;b2]
Run time: 0.4s
Intermediate theorems generated: 35

#let NOT3_DEF = define_bit_op word3_FNDEF `NOT3_DEF` `NOT3`  "$~";;
NOT3_DEF = |- !w. NOT3 w = WORD3(MAP $~(BITS3 w))
Run time: 0.6s
Intermediate theorems generated: 37

#let ithm = CONJUNCT1 NOT_CLAUSES;;
ithm = |- !t. ~~t = t
Run time: 0.0s
Intermediate theorems generated: 1

#let NOT3 = prove_not_thm word3 NOT3_DEF ithm word3_LENGTH_BITS;;
NOT3 = |- !w. NOT3(NOT3 w) = w
Run time: 0.2s
Intermediate theorems generated: 22

#let AND3_DEF = define_bin_bit_op true word3_FNDEF `AND3_DEF` `AND3`  "$/\";;
AND3_DEF = |- !w w'. w AND3 w' = WORD3(MAP2 $/\(BITS3 w)(BITS3 w'))
Run time: 0.7s
Intermediate theorems generated: 37

#let AND3_SYM = prove_sym_thm AND3_DEF CONJ_SYM word3_LENGTH_BITS;;
AND3_SYM = |- !w w'. w AND3 w' = w' AND3 w
Run time: 0.2s
Intermediate theorems generated: 20

#let AND3_ASSOC = prove_assoc_thm word3 AND3_DEF CONJ_ASSOC word3_LENGTH_BITS;;
AND3_ASSOC = |- !w w' w''. w AND3 (w' AND3 w'') = (w AND3 w') AND3 w''
Run time: 0.8s
Intermediate theorems generated: 74

#let word5 = define_wordn_type `word5` 5;;
word5 = 
|- (!w. WORD5(BITS5 w) = w) /\
   (!l. (LENGTH l = 5) = (BITS5(WORD5 l) = l))
Run time: 0.4s
Intermediate theorems generated: 9

#let word5_FNDEF = prove_function_defn_thm word5;;
word5_FNDEF = 
|- !f.
    ?! fn. !b0 b1 b2 b3 b4. fn(WORD5[b0;b1;b2;b3;b4]) = f b0 b1 b2 b3 b4
Run time: 1.9s
Intermediate theorems generated: 158

#let word5_INDUCT = prove_wordn_induction_thm word5_FNDEF;;
word5_INDUCT = 
|- !P. (!b0 b1 b2 b3 b4. P(WORD5[b0;b1;b2;b3;b4])) ==> (!w. P w)
Run time: 0.8s
Intermediate theorems generated: 71

#let word5_CASES = prove_wordn_cases_thm word5_INDUCT;;
word5_CASES = |- !w. ?b0 b1 b2 b3 b4. w = WORD5[b0;b1;b2;b3;b4]
Run time: 0.3s
Intermediate theorems generated: 23

#let word5_BITS_WORD = prove_BITS_WORD word5;;
word5_BITS_WORD = 
|- !b0 b1 b2 b3 b4. BITS5(WORD5[b0;b1;b2;b3;b4]) = [b0;b1;b2;b3;b4]
Run time: 0.4s
Intermediate theorems generated: 51

#let word8 = define_wordn_type `word8` 8;;
word8 = 
|- (!w. WORD8(BITS8 w) = w) /\
   (!l. (LENGTH l = 8) = (BITS8(WORD8 l) = l))
Run time: 0.5s
Intermediate theorems generated: 9

#let word8_FNDEF = prove_function_defn_thm word8;;
word8_FNDEF = 
|- !f.
    ?! fn.
     !b0 b1 b2 b3 b4 b5 b6 b7.
      fn(WORD8[b0;b1;b2;b3;b4;b5;b6;b7]) = f b0 b1 b2 b3 b4 b5 b6 b7
Run time: 3.3s
Intermediate theorems generated: 233

#let word8_INDUCT = prove_wordn_induction_thm word8_FNDEF;;
word8_INDUCT = 
|- !P.
    (!b0 b1 b2 b3 b4 b5 b6 b7. P(WORD8[b0;b1;b2;b3;b4;b5;b6;b7])) ==>
    (!w. P w)
Run time: 1.2s
Intermediate theorems generated: 89

#let word8_CASES = prove_wordn_cases_thm word8_INDUCT;;
word8_CASES = 
|- !w. ?b0 b1 b2 b3 b4 b5 b6 b7. w = WORD8[b0;b1;b2;b3;b4;b5;b6;b7]
Run time: 0.6s
Garbage collection time: 4.3s
Intermediate theorems generated: 29

#let word8_BITS_WORD = prove_BITS_WORD word8;;
word8_BITS_WORD = 
|- !b0 b1 b2 b3 b4 b5 b6 b7.
    BITS8(WORD8[b0;b1;b2;b3;b4;b5;b6;b7]) = [b0;b1;b2;b3;b4;b5;b6;b7]
Run time: 0.7s
Intermediate theorems generated: 75

#let JOIN_3_5_DEF,SPLIT_3_5_DEF =
#    define_word_partition (`JOIN_3_5`,`SPLIT_3_5`)
#    	[word3_BITS_WORD; word5_BITS_WORD; word8_BITS_WORD];;
JOIN_3_5_DEF = 
|- !b0 b1 b2 b3 b4 b5 b6 b7.
    JOIN_3_5(WORD3[b0;b1;b2],WORD5[b3;b4;b5;b6;b7]) =
    WORD8[b0;b1;b2;b3;b4;b5;b6;b7]
SPLIT_3_5_DEF = 
|- !b0 b1 b2 b3 b4 b5 b6 b7.
    SPLIT_3_5(WORD8[b0;b1;b2;b3;b4;b5;b6;b7]) =
    WORD3[b0;b1;b2],WORD5[b3;b4;b5;b6;b7]
Run time: 3.0s
Intermediate theorems generated: 187

#let PARTION_3_5 = prove_partition_thm (JOIN_3_5_DEF,SPLIT_3_5_DEF)
#    	[word3_CASES; word5_CASES; word8_CASES];;
PARTION_3_5 = 
|- (!wl. JOIN_3_5(SPLIT_3_5 wl) = wl) /\
   (!wm wn. SPLIT_3_5(JOIN_3_5(wm,wn)) = wm,wn)
Run time: 1.1s
Intermediate theorems generated: 140


#let [NVAL3_DEF;NWORD3_DEF] = define_word_val word3
#    (`NVAL3`,`NVAL3_DEF`) (`NWORD3`,`NWORD3_DEF`);;
NVAL3_DEF = |- !w. NVAL3 w = VAL(BITS3 w)
NWORD3_DEF = |- !n. NWORD3 n = WORD3(WORDN 3 n)
Run time: 0.5s
Intermediate theorems generated: 5

#let word3_NVAL_NWORD = prove_word_val word3 NVAL3_DEF NWORD3_DEF;;
word3_NVAL_NWORD = 
|- (!w. NWORD3(NVAL3 w) = w) /\ (!m. NVAL3(NWORD3 m) = m MOD (2 EXP 3))
Run time: 0.2s
Intermediate theorems generated: 40

#let word3_NWORD_MOD = prove_NWORD_MOD word3_NVAL_NWORD;;
word3_NWORD_MOD = |- !m. NWORD3 m = NWORD3(m MOD 8)
Run time: 1.0s
Intermediate theorems generated: 95

#let NVAL3_3 = NVAL_CONV word3 NVAL3_DEF "NVAL3 #011";;
NVAL3_3 = |- NVAL3 #011 = 3
Run time: 2.0s
Intermediate theorems generated: 170

#let NWORD3_3 = NWORD_CONV NWORD3_DEF word3_NWORD_MOD "NWORD3 3";;
NWORD3_3 = |- NWORD3 3 = #011
Run time: 2.1s
Intermediate theorems generated: 173

# close_theory();;
() : void
Run time: 0.3s
Intermediate theorems generated: 1

#

---------------------------------
Wai Wong                 
ww@cl.cam.ac.uk                 University of Cambridge
				Computer laboratory
                                Cambridge CB2 3QG
Tel:+44 223 334688		England
=========================================================================