Remove TABs from examples

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

Patching broken proofs. The proofs were broken due changes to
stringTheory and parsing of $-. Is there a reason for why the parser
does not maintain backwards compatibility for unary minus?

I was unable to fix some of the proofs, for example in:

basic_defaxiomsScript.sml

Various tweaks (some ugly) to get things working again.

Modifications to allow the translation to run under PolyML.

Complete rework of the function encoding for ACL2. Usage of the encoding is
contained in acl2encodeLib.sig.

Attempt to get my local version in sync with repository copy. If
it causes trouble for others, I can fix in the next few days.

encodeLib.sml,translateScript.sml : Modified to use 'natp' from hol_defaxioms

encodeLib: Major rewrite to allow encoding of functions with partial specifications.
translateScript: Extra theorems added for better resolution of natural numbers
testEncode: Updated to test partial specifications and some extra red-black tree examples added.

encodeLib: Now handles lambda abstractions and let syntax natively
Improved support for difficult recursion schemes (eg. DIV)
translateScript: Added translations for strings and characters
Definitions are now checked one by one to avoid the
'couldn't protect' error
sexp: Added support for 'let a = b and c = d in...' syntax

Tweaks: temporarily disabled ACL2 invocation (not working on my machine).
Updated README + comment typo fixes in sexp.sml.

translateScript: A few more definitions (quot,rem,...) and added all the typing judgements for the new definitions.

translateScript: New acl2 definitions and rewrites for list definitions
acl2_packageScript: A bit faster again...

translateScript: Definitions are now named as those in ACL2 and an
equivalence proof is generated on compilation
README: Updated to indicate the fact that compiling translateScript
requires the ACL2 executable

translateScript: Added a reduction for SUC (PRE a)
encodeLib: It's now possible to encoding HO functions such as FILTER, MAP etc... and re-use these in further definitions. Flattening these definitions into ACL2 is still unsupported however.

Proof of another couple of ACL2 axioms. Exported some theorems proved in
translateScript.sml that were useful in hol_defaxioms_proofsScript.sml.

translateScript: Modified NAT_CASE to use PRE a, which translates to (+ a (- 1)) rather than nfix (+ a (- 1)) which occasionally introduced termination problems.
encodeLib: Fixed a few type inferences bugs associated with the changes in translateScript.

encodeLib: Now encodes theorems, also some minor improvements to type checking and resolving constraints, such as non-zero denominators for divide.
translateLib: A few minor changes, added an andl judgement

encodeLib: Complete re-vamp, can now do PolyTypism, however has limited support for case functions eg. NULL

translateScript: Now uses |= for type judgements, and makes use of some new functions such as andl and implies.

translateLib: Some functions to support encoding which are used in both encodeLib and translateScript

Replace the temporary acl2_defs_theory by hol_defaxiomsTheory.

Initially hol_defaxiomsScript.sml started as a list of desired
definitions (and -- later in the file -- theorems) imported from
ACL2. The imported desired stuff is in the comments.

For example, after the boilerplate, hol_defaxiomsScript.sml starts
with:

(*
[oracles: DEFUN ACL2::IFF, DISK_THM] [axioms: ] []
|- iff p q = itel [(p,andl [q; t]); (q,nil)] t,
*)

This comment contains a printout of a theorem created by trusting ACL2
(see added tag, which indicates that DEFUN is trusted and showing the
ACL2 name). The long-term goal is to eliminate the need to trust ACL2 when
defining the core ACL2 theory. Thus we have the pure HOL definition:

val iff_def =
acl2Define "ACL2::IFF"
`iff p q = itel [(p,andl [q; t]); (q,nil)] t`;

So far we have only made HOL definitions of those functions
immediately needed (e.g. by James' translate tool).

Sometimes, for historical reasons, we define a function slightly
different from the definition in the comment (e.g. see ACL2::ZP) and
then prove that the definition made implements the one in the comment.

Eventually desired recursive definitions will be needed. So far
acl2Define doesn't support this well, so we have the interim
implementation of

(*
[oracles: DEFUN ACL2::TRUE-LISTP, DISK_THM] [axioms: ] []
|- true_listp x = ite (consp x) (true_listp (cdr x)) (eq x nil),
*)

implemented as:

val (true_listp_def,true_listp_ind) =
Defn.tprove
(Hol_defn
"true_listp"
`true_listp x = ite (consp x) (true_listp (cdr x)) (eq x nil)`,
WF_REL_TAC `measure sexp_size`
THEN RW_TAC arith_ss [sexp_size_cdr]);

but eventually we need the constant to be named "ACL2::TRUE-LISTP",
and "true_lisp" is just overloaded onto that.

Once all the definitions have been made, we hope to prove the ACL2
axioms, thereby establishing that we have a model of the ACL2
theory. This may be a lot of work though.

Tidying up. Note that acl2_defsTheory replaces basic_defaxiomsTheory.

Incremental changes (including ``cond`` --> ``ite``).

Getting things to work with the new improved naming scheme.
(e.g. COMMON-LISP::= is now called common_lisp_equal rather than acl2_equal,
and definitions proviously named *_acl2_defun are now stored as *_def).

File: encodeLib.sml

Provides functions to encode HOL into ACL2

File: encodeLib.sig

Signature for encodeLib.sml

File: translateScript.sml

Provides translation theorems between HOL and the sexp type.
New constants are also defined here, which must be slurped along with anything
being encoded.