Added a new file "compute.ml" from Alexey Solovyev containing tools

for doing ML-style call-by-value reduction of terms by inference
inside the logic. This is a port of the HOL4 "computeLib" library
originally developed by Bruno Barras (see "Programming and Computing
in HOL", TPHOLs 2000).

Made a few documentation and test fixes to keep in step with recent
changes. Also added a few simple extra theorems about initial segments
of N and sums over them:

        ITERATE_CLAUSES_NUMSEG_LE
        ITERATE_CLAUSES_NUMSEG_LT
        NSUM_CLAUSES_NUMSEG_LE
        NSUM_CLAUSES_NUMSEG_LT
        NUMSEG_CLAUSES_LE
        NUMSEG_CLAUSES_LT
        SUM_CLAUSES_NUMSEG_LE
        SUM_CLAUSES_NUMSEG_LT

CHANGES

@@ -8,6 +8,64 @@
   * page: https://github.com/jrh13/hol-light/commits/master         *
   * *****************************************************************
 
+Sat  9th Feb 2019       compute.ml [new file]
+
+Added a new file from Alexey Solovyev containing tools for doing ML-style
+call-by-value reduction of terms by inference inside the logic. This is a port
+of the HOL4 "computeLib" library originally developed by Bruno Barras
+(see "Programming and Computing in HOL", TPHOLs 2000).
+
+Wed  6th Feb 2019       lib.ml, parser.ml, printer.ml, system.ml, tactics.ml, Help/print_num.doc [new file], Help/pp_print_num.doc [new file]
+
+Made several fixes from pull requests prepared by Alexey Solovyev. Made the
+parser error messages a bit more explicit (based on local code in Flyspeck by
+Tom Hales). Fixed some cases where printing functions were not properly
+parametrized by the formatter, with new functions "pp_print_num" and
+"pp_print_fpf" that are used to print nums and finite partial functions, plus
+proper use of the pre-existing parametrized form for types, terms, theorems,
+goals and goalstacks in the #install_printer directives.
+
+Wed  6th Feb 2019       sets.ml
+
+Added a couple of trivial but handy clausal theorems about initial number
+segments:
+
+  NUMSEG_CLAUSES_LT =
+    |- {i | i < 0} = {} /\ (!k. {i | i < SUC k} = k INSERT {i | i < k})
+
+  NUMSEG_CLAUSES_LE =
+    |- {i | i <= 0} = {0} /\ (!k. {i | i <= SUC k} = SUC k INSERT {i | i <= k})
+
+and some corresponding clauses for sums and other iterated operations:
+
+  ITERATE_CLAUSES_NUMSEG_LE =
+    |- !op. monoidal op
+            ==> iterate op {i | i <= 0} f = f 0 /\
+                (!k. iterate op {i | i <= SUC k} f =
+                     op (iterate op {i | i <= k} f) (f (SUC k)))
+
+  ITERATE_CLAUSES_NUMSEG_LT =
+    |- !op. monoidal op
+            ==> iterate op {i | i < 0} f = neutral op /\
+                (!k. iterate op {i | i < SUC k} f =
+                     op (iterate op {i | i < k} f) (f k))
+
+  NSUM_CLAUSES_NUMSEG_LE =
+    |- nsum {i | i <= 0} f = f 0 /\
+       (!k. nsum {i | i <= SUC k} f = nsum {i | i <= k} f + f (SUC k))
+
+  NSUM_CLAUSES_NUMSEG_LT =
+    |- nsum {i | i < 0} f = 0 /\
+       (!k. nsum {i | i < SUC k} f = nsum {i | i < k} f + f k)
+
+  SUM_CLAUSES_NUMSEG_LE =
+    |- sum {i | i <= 0} f = f 0 /\
+       (!k. sum {i | i <= SUC k} f = sum {i | i <= k} f + f (SUC k))
+
+  SUM_CLAUSES_NUMSEG_LT =
+    |- sum {i | i < 0} f = &0 /\
+       (!k. sum {i | i < SUC k} f = sum {i | i < k} f + f k)
+
 Sat  2nd Feb 2019       Multivariate/vectors.ml, Multivariate/msum.ml [new file]
 
 Added a lot of new material, mainly about matrices, from Andrea Gabrielli

Help/pp_print_fpf.doc

@@ -0,0 +1,23 @@
+\DOC pp_print_fpf
+
+\TYPE {pp_print_fpf : Format.formatter -> ('a, 'b) func -> unit}
+
+\SYNOPSIS
+Print a finite partial function to a formatter.
+
+\DESCRIBE
+This prints a finite partial function but only as a trivial string `{<func>}',
+to the given formatter. Installed automatically at the top level and probably
+not useful for most users.
+
+\FAILURE
+Never fails.
+
+\COMMENTS
+The usual case where the formatter is the standard output is {print_fpf}.
+
+\SEEALSO
+|->, |=>, apply, applyd, choose, combine, defined, dom, foldl, foldr,
+graph, is_undefined, mapf, print_fpf, ran, tryapplyd, undefine, undefined.
+
+\ENDDOC

Help/pp_print_num.doc

@@ -0,0 +1,23 @@
+\DOC pp_print_num
+
+\TYPE {pp_print_num : Format.formatter -> num -> unit}
+
+\SYNOPSIS
+Print an arbitrary-precision number to the given formatter.
+
+\DESCRIBE
+This function prints an arbitrary-precision (type {num}) number to the
+formatter given as first argument. It is automatically invoked on anything of
+type {num} at the toplevel anyway, but it may sometimes be useful to issue it
+under user control.
+
+\FAILURE
+Never fails.
+
+\COMMENTS
+The usual case where the formatter is the standard output is {print_num}.
+
+\SEEALSO
+print_num.
+
+\ENDDOC

Help/print_fpf.doc

@@ -7,14 +7,14 @@ Print a finite partial function.
 
 \DESCRIBE
 This prints a finite partial function but only as a trivial string `{<func>}'.
-Installed automatically at the top level and probably not useful for most 
+Installed automatically at the top level and probably not useful for most
 users.
 
 \FAILURE
 Never fails.
 
 \SEEALSO
-|->, |=>, apply, applyd, choose, combine, defined, dom, foldl, foldr, 
-graph, is_undefined, mapf, ran, tryapplyd, undefine, undefined.
+|->, |=>, apply, applyd, choose, combine, defined, dom, foldl, foldr,
+graph, is_undefined, mapf, pp_print_fpf, ran, tryapplyd, undefine, undefined.
 
 \ENDDOC

Help/print_num.doc

@@ -6,11 +6,14 @@
 Print an arbitrary-precision number to the terminal.
 
 \DESCRIBE
-This function prints an arbitrary-precision (type {num}) number to the 
-terminal. It is automatically invoked on anything of type {num} at the toplevel 
+This function prints an arbitrary-precision (type {num}) number to the
+terminal. It is automatically invoked on anything of type {num} at the toplevel
 anyway, but it may sometimes be useful to issue it under user control.
 
 \FAILURE
 Never fails.
 
+\SEEALSO
+pp_print_num.
+
 \ENDDOC

Multivariate/complex_database.ml

@@ -9866,6 +9866,8 @@ theorems :=
 "ITERATE_CLAUSES",ITERATE_CLAUSES;
 "ITERATE_CLAUSES_GEN",ITERATE_CLAUSES_GEN;
 "ITERATE_CLAUSES_NUMSEG",ITERATE_CLAUSES_NUMSEG;
+"ITERATE_CLAUSES_NUMSEG_LE",ITERATE_CLAUSES_NUMSEG_LE;
+"ITERATE_CLAUSES_NUMSEG_LT",ITERATE_CLAUSES_NUMSEG_LT;
 "ITERATE_CLOSED",ITERATE_CLOSED;
 "ITERATE_DELETE",ITERATE_DELETE;
 "ITERATE_DELTA",ITERATE_DELTA;
@@ -12345,6 +12347,8 @@ theorems :=
 "NSUM_CLAUSES",NSUM_CLAUSES;
 "NSUM_CLAUSES_LEFT",NSUM_CLAUSES_LEFT;
 "NSUM_CLAUSES_NUMSEG",NSUM_CLAUSES_NUMSEG;
+"NSUM_CLAUSES_NUMSEG_LE",NSUM_CLAUSES_NUMSEG_LE;
+"NSUM_CLAUSES_NUMSEG_LT",NSUM_CLAUSES_NUMSEG_LT;
 "NSUM_CLAUSES_RIGHT",NSUM_CLAUSES_RIGHT;
 "NSUM_CLOSED",NSUM_CLOSED;
 "NSUM_CONST",NSUM_CONST;
@@ -12432,6 +12436,8 @@ theorems :=
 "NUMSEG_ADD_SPLIT",NUMSEG_ADD_SPLIT;
 "NUMSEG_CARD_LE",NUMSEG_CARD_LE;
 "NUMSEG_CLAUSES",NUMSEG_CLAUSES;
+"NUMSEG_CLAUSES_LE",NUMSEG_CLAUSES_LE;
+"NUMSEG_CLAUSES_LT",NUMSEG_CLAUSES_LT;
 "NUMSEG_COMBINE_L",NUMSEG_COMBINE_L;
 "NUMSEG_COMBINE_R",NUMSEG_COMBINE_R;
 "NUMSEG_DIMINDEX_NONEMPTY",NUMSEG_DIMINDEX_NONEMPTY;
@@ -16891,6 +16897,8 @@ theorems :=
 "SUM_CLAUSES",SUM_CLAUSES;
 "SUM_CLAUSES_LEFT",SUM_CLAUSES_LEFT;
 "SUM_CLAUSES_NUMSEG",SUM_CLAUSES_NUMSEG;
+"SUM_CLAUSES_NUMSEG_LE",SUM_CLAUSES_NUMSEG_LE;
+"SUM_CLAUSES_NUMSEG_LT",SUM_CLAUSES_NUMSEG_LT;
 "SUM_CLAUSES_RIGHT",SUM_CLAUSES_RIGHT;
 "SUM_CLOSED",SUM_CLOSED;
 "SUM_COMBINE_L",SUM_COMBINE_L;

Multivariate/multivariate_database.ml

@@ -8249,6 +8249,8 @@ theorems :=
 "ITERATE_CLAUSES",ITERATE_CLAUSES;
 "ITERATE_CLAUSES_GEN",ITERATE_CLAUSES_GEN;
 "ITERATE_CLAUSES_NUMSEG",ITERATE_CLAUSES_NUMSEG;
+"ITERATE_CLAUSES_NUMSEG_LE",ITERATE_CLAUSES_NUMSEG_LE;
+"ITERATE_CLAUSES_NUMSEG_LT",ITERATE_CLAUSES_NUMSEG_LT;
 "ITERATE_CLOSED",ITERATE_CLOSED;
 "ITERATE_DELETE",ITERATE_DELETE;
 "ITERATE_DELTA",ITERATE_DELTA;
@@ -10512,6 +10514,8 @@ theorems :=
 "NSUM_CLAUSES",NSUM_CLAUSES;
 "NSUM_CLAUSES_LEFT",NSUM_CLAUSES_LEFT;
 "NSUM_CLAUSES_NUMSEG",NSUM_CLAUSES_NUMSEG;
+"NSUM_CLAUSES_NUMSEG_LE",NSUM_CLAUSES_NUMSEG_LE;
+"NSUM_CLAUSES_NUMSEG_LT",NSUM_CLAUSES_NUMSEG_LT;
 "NSUM_CLAUSES_RIGHT",NSUM_CLAUSES_RIGHT;
 "NSUM_CLOSED",NSUM_CLOSED;
 "NSUM_CONST",NSUM_CONST;
@@ -10598,6 +10602,8 @@ theorems :=
 "NUMSEG_ADD_SPLIT",NUMSEG_ADD_SPLIT;
 "NUMSEG_CARD_LE",NUMSEG_CARD_LE;
 "NUMSEG_CLAUSES",NUMSEG_CLAUSES;
+"NUMSEG_CLAUSES_LE",NUMSEG_CLAUSES_LE;
+"NUMSEG_CLAUSES_LT",NUMSEG_CLAUSES_LT;
 "NUMSEG_COMBINE_L",NUMSEG_COMBINE_L;
 "NUMSEG_COMBINE_R",NUMSEG_COMBINE_R;
 "NUMSEG_DIMINDEX_NONEMPTY",NUMSEG_DIMINDEX_NONEMPTY;
@@ -13714,6 +13720,8 @@ theorems :=
 "SUM_CLAUSES",SUM_CLAUSES;
 "SUM_CLAUSES_LEFT",SUM_CLAUSES_LEFT;
 "SUM_CLAUSES_NUMSEG",SUM_CLAUSES_NUMSEG;
+"SUM_CLAUSES_NUMSEG_LE",SUM_CLAUSES_NUMSEG_LE;
+"SUM_CLAUSES_NUMSEG_LT",SUM_CLAUSES_NUMSEG_LT;
 "SUM_CLAUSES_RIGHT",SUM_CLAUSES_RIGHT;
 "SUM_CLOSED",SUM_CLOSED;
 "SUM_COMBINE_L",SUM_COMBINE_L;