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