README
1Overview
2--------
3
4This directory is a preliminary slurping in of J Moore's M1 ACL2 JVM
5model into HOL, tweaked manually to try to get it to build in HOL4
6under Moscow ML and Poly/ML.
7
8Holmake should perform the complete proof, including rebuilding the
9HOL-ACL2 infrastructure. This will takes tens of minutes.
10
11There is a rather arbitrary division of HOL functions operating on
12s-expressions into those that are defined properly in HOL (using
13acl2Define) and those that are axiomatically defined based on trusting
14ACL2 (these are defined with acl2AxiomDefine). Ideally everything
15should be properly defined, but I was too lazy to figure out the
16termination proofs for ACL2::NONNEGATIVE-INTEGER-QUOTIENT and
17COMMON-LISP::EXPT (see file hol_defaxiomsScript.sml). See the file
18acl2/ISSUES for some more discussion.
19
20To get a flavour of the M1 example in HOL, run hol in this directory,
21load "M1Examples" and then look at M1Examples.Examples1 (some selected
22examples) and M1Examples.Examples2 (shows all the theorems in
23imported_acl2Theory).
24
25A log of doing this (in Moscow ML) is in the file M1Examples.txt.
26
27Notes:
28
29 1. The HOL functions corresponding to the AC2 M1 JVM model are in
30 imported_acl2Theory;
31
32 2. The ML function acl2_simp performs some simplifications on
33 imported ACL2.
34
35 3. The ACL2 name "!" (i.e. factorial) is translated to "exclaim" in HOL.
36
37
38Files in this directory
39-----------------------
40
41 READ-ME ............................... This file
42
43 Holmake.log ........................... Log of Holmake (Moscow ML)
44
45 sexp.sml .............................. Tools for processing s-expressions
46 complex_rationalScript.sml ............ Script to build theory of complex rationals
47 sexpScript.sml ........................ Script to build theory of s-expressions
48 acl2_packageScript.sml ................ Script to build gigantic ACL2 package specification
49 hol_defaxiomsScript.sml ............... HOL definitions of functions in defaxioms
50 imported_acl2Script.sml................ Script to build M1 in HOL
51 axioms.ml ............................. Exported from ACL2 (currently not used)
52
53 PKGS.sml .............................. Generated by ACL2 and then manually edited
54 m1-story.sml .......................... Exported from ACL2 and then manually edited
55 problem-set-1-answers.sml.............. Exported from ACL2 and then manually edited
56 M1Examples.sml ........................ Some examples (see above)
57 M1Examples.txt ........................ Log of loading M1Examples (Moscow ML)
58
59MJCG
60Wed Aug 25 16:04:43 BST 2010
61
62
63