NameDateSize

..25-Jul-201913

acl2_packageScript.smlH A D25-Jul-201910.5 KiB

axioms.mlH A D25-Jul-20191.3 MiB

complex_rationalScript.smlH A D25-Jul-201912 KiB

hol_defaxiomsScript.smlH A D25-Jul-2019155.7 KiB

Holmake.logH A D25-Jul-201930.7 KiB

imported_acl2Script.smlH A D25-Jul-20193.4 KiB

m1_story.smlH A D25-Jul-2019123.3 KiB

M1Examples.smlH A D25-Jul-20192.4 KiB

M1Examples.txtH A D25-Jul-201941.3 KiB

M1Script.smlH A D25-Jul-20192.6 KiB

PKGS.smlH A D25-Jul-2019476.7 KiB

problem_set_1_answers.smlH A D25-Jul-201927.1 KiB

READMEH A D25-Jul-20192.5 KiB

sexp.smlH A D25-Jul-2019119 KiB

sexpScript.smlH A D25-Jul-201979.2 KiB

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