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