## L. Morris's material for CSE 773, Spring 2003

My e-mail address is lockwood@ecs.syr.edu

Purpose of this directory

Notes on some basic tactics in HOL

Notes on some additional HOL tactics

Notes for Jan. 28 lecture

Notes for Feb. 10 lecture

More examples of the use of lists

Generalized counters (See also the
link below to LCM_chcScript.sml)

Notes for Mar. 27 lecture

Notes for April 10 lecture

Use of Hol_defn for making non-standard
recursive definitions

Some tactics, conversions, etc. written originally for my own convenience
in using HOL, but of possible interest and use to CSE 773 students:
description (PostScript, 14 pp., index on page 14);

ante_allTacs.sml ML source
(8 pp.);

ante_allTacs.sig ML
signature (2 pp.).

The ML files and their compiled forms are located in, and loadable from,
directory /home/ecefac/cse773.

A mathematical theory of LCM, Iter, period, and characteristic abstracted
from gen_count.txt (concerning Prof. Stabler's generalized notion of a
counter) which has in consequence become quite short. Also compiled in
/home/ecefac/cse773:
LCM_chcScript.sml

A theory of breaking natural numbers and lists into as nearly equal halves
as possible, largely avoiding struggles with DIV. Provides facilities
for induction and, in effect, recursive function definition by
decomposition into (nearly) equal halves:
halvesScript.sml

A theory specifying addition for natural numbers represented as bool lists,
least significant bit first, and defining (with the facilities provided
by halvesTheory) a carry-lookahead adder for any fixed word length, and
proving the implementation correct:
adder_halvesScript.sml