Added a complete revision from Marco Maggesi of the "Ntrie" library

for manipulation of concrete numeral sets using a trie-like
representation. Among other improvements, the conversions have been
made cleaner (always failing predictably on non-minimal ntries) and
much more efficient (typically 5x-15x as fast), and a syntax
extension for ntries has been added.

Moved a few existing things (theorems DIVIDES_ANTISYM,
DIVIDES_LE_STRONG, DIVIDES_ONE and the definition of "prime") from
"Library/prime.ml" into the core, to avoid loading all that file for
a few more simple facts, and also added two new (and trivial)
theorems ONE_OR_PRIME and FORALL_INT_CASES.

CHANGES

@@ -8,6 +8,27 @@
   * page: https://github.com/jrh13/hol-light/commits/master         *
   * *****************************************************************
 
+Sun 24th Sep 2017       Ntrie/ntrie.ml
+
+Added a complete revision from Marco Maggesi of the "Ntrie" library for
+manipulation of concrete numeral sets using a trie-like representation. Among
+other improvements, the conversions have been made cleaner (always failing
+predictably on non-minimal ntries) and much more efficient (typically 5x-15x as
+fast), and a syntax extension for ntries has been added.
+
+Wed 20th Sep 2017       int.ml, Library/prime.ml
+
+Moved a few existing things (theorems DIVIDES_ANTISYM, DIVIDES_LE_STRONG,
+DIVIDES_ONE and the definition of "prime") from "Library/prime.ml" into the
+core, to avoid loading all that file for a few more simple facts, and also
+added two new (and trivial) theorems:
+
+  ONE_OR_PRIME =
+    |- !p. p = 1 \/ prime p <=> (!n. n divides p ==> n = 1 \/ n = p)
+
+  FORALL_INT_CASES =
+    |- !P:int->bool. (!x. P x) <=> (!n. P(&n)) /\ (!n. P(-- &n))
+
 Sat 16th Sep 2017       Library/frag.ml [new file], Library/grouptheory.ml
 
 Added another file "Library/frag.ml" with a type constructor for defining the

Library/prime.ml

@@ -195,13 +195,6 @@ let DIVIDES_1 = prove
  (`!x. 1 divides x`,
   NUMBER_TAC);;
 
-let DIVIDES_ONE = prove(
-  `!x. (x divides 1) <=> (x = 1)`,
-  GEN_TAC THEN REWRITE_TAC[divides] THEN
-  CONV_TAC(LAND_CONV(ONCE_DEPTH_CONV SYM_CONV)) THEN
-  REWRITE_TAC[MULT_EQ_1] THEN EQ_TAC THEN STRIP_TAC THEN
-  ASM_REWRITE_TAC[] THEN EXISTS_TAC `1` THEN REFL_TAC);;
-
 let DIVIDES_REFL = prove
  (`!x. x divides x`,
   NUMBER_TAC);;
@@ -210,17 +203,6 @@ let DIVIDES_TRANS = prove
  (`!a b c. a divides b /\ b divides c ==> a divides c`,
   NUMBER_TAC);;
 
-let DIVIDES_ANTISYM = prove
- (`!x y. x divides y /\ y divides x <=> (x = y)`,
-  REPEAT GEN_TAC THEN EQ_TAC THENL
-   [REWRITE_TAC[divides] THEN
-    DISCH_THEN(CONJUNCTS_THEN2 MP_TAC (CHOOSE_THEN SUBST1_TAC)) THEN
-    DISCH_THEN(CHOOSE_THEN MP_TAC) THEN
-    CONV_TAC(LAND_CONV SYM_CONV) THEN
-    REWRITE_TAC[GSYM MULT_ASSOC; MULT_FIX; MULT_EQ_1] THEN
-    STRIP_TAC THEN ASM_REWRITE_TAC[];
-    DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[DIVIDES_REFL]]);;
-
 let DIVIDES_ADD = prove
  (`!d a b. d divides a /\ d divides b ==> d divides (a + b)`,
   NUMBER_TAC);;
@@ -292,13 +274,6 @@ let DIVIDES_CASES = prove
   SIMP_TAC[divides; LEFT_IMP_EXISTS_THM] THEN
   REWRITE_TAC[MULT_EQ_0; EQ_MULT_LCANCEL; LE_MULT_LCANCEL] THEN ARITH_TAC);;
 
-let DIVIDES_LE_STRONG = prove
- (`!m n. m divides n ==> 1 <= m /\ m <= n \/ n = 0`,
-  REPEAT GEN_TAC THEN ASM_CASES_TAC `m = 0` THEN
-  ASM_REWRITE_TAC[DIVIDES_ZERO; ARITH] THEN
-  DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_LE) THEN
-  POP_ASSUM MP_TAC THEN ARITH_TAC);;
-
 let DIVIDES_DIV_NOT = prove(
   `!n x q r. (x = (q * n) + r) /\ 0 < r /\ r < n ==> ~(n divides x)`,
   REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
@@ -970,13 +945,6 @@ let CHINESE_REMAINDER = prove
   REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; MULT_CLAUSES] THEN
   REWRITE_TAC[MULT_AC] THEN REWRITE_TAC[ADD_AC]);;
 
-(* ------------------------------------------------------------------------- *)
-(* Primality                                                                 *)
-(* ------------------------------------------------------------------------- *)
-
-let prime = new_definition
-  `prime(p) <=> ~(p = 1) /\ !x. x divides p ==> (x = 1) \/ (x = p)`;;
-
 (* ------------------------------------------------------------------------- *)
 (* A few useful theorems about primes                                        *)
 (* ------------------------------------------------------------------------- *)

Multivariate/complex_database.ml

@@ -4738,7 +4738,10 @@ theorems :=
 "DIST_TRIANGLE_HALF_R",DIST_TRIANGLE_HALF_R;
 "DIST_TRIANGLE_LE",DIST_TRIANGLE_LE;
 "DIST_TRIANGLE_LT",DIST_TRIANGLE_LT;
+"DIVIDES_ANTISYM",DIVIDES_ANTISYM;
 "DIVIDES_LE",DIVIDES_LE;
+"DIVIDES_LE_STRONG",DIVIDES_LE_STRONG;
+"DIVIDES_ONE",DIVIDES_ONE;
 "DIVISION",DIVISION;
 "DIVISION_0",DIVISION_0;
 "DIVISION_1_SORT",DIVISION_1_SORT;
@@ -5645,6 +5648,7 @@ theorems :=
 "FORALL_FINITE_SUBSET_IMAGE_INJ",FORALL_FINITE_SUBSET_IMAGE_INJ;
 "FORALL_INTEGER",FORALL_INTEGER;
 "FORALL_INTERSECTION_OF",FORALL_INTERSECTION_OF;
+"FORALL_INT_CASES",FORALL_INT_CASES;
 "FORALL_IN_CLAUSES",FORALL_IN_CLAUSES;
 "FORALL_IN_CLOSURE",FORALL_IN_CLOSURE;
 "FORALL_IN_CLOSURE_EQ",FORALL_IN_CLOSURE_EQ;
@@ -10925,6 +10929,7 @@ theorems :=
 "OEP",OEP;
 "ONE",ONE;
 "ONE_ONE",ONE_ONE;
+"ONE_OR_PRIME",ONE_OR_PRIME;
 "ONORM",ONORM;
 "ONORM_ADJOINT",ONORM_ADJOINT;
 "ONORM_CMUL",ONORM_CMUL;
@@ -16383,6 +16388,7 @@ theorems :=
 "poset",poset;
 "positive_definite",positive_definite;
 "positive_semidefinite",positive_semidefinite;
+"prime",prime;
 "prod_metric",prod_metric;
 "prod_topology",prod_topology;
 "prod_tybij",prod_tybij;

Multivariate/multivariate_database.ml

@@ -3783,7 +3783,10 @@ theorems :=
 "DIST_TRIANGLE_HALF_R",DIST_TRIANGLE_HALF_R;
 "DIST_TRIANGLE_LE",DIST_TRIANGLE_LE;
 "DIST_TRIANGLE_LT",DIST_TRIANGLE_LT;
+"DIVIDES_ANTISYM",DIVIDES_ANTISYM;
 "DIVIDES_LE",DIVIDES_LE;
+"DIVIDES_LE_STRONG",DIVIDES_LE_STRONG;
+"DIVIDES_ONE",DIVIDES_ONE;
 "DIVISION",DIVISION;
 "DIVISION_0",DIVISION_0;
 "DIVISION_1_SORT",DIVISION_1_SORT;
@@ -4652,6 +4655,7 @@ theorems :=
 "FORALL_FINITE_SUBSET_IMAGE_INJ",FORALL_FINITE_SUBSET_IMAGE_INJ;
 "FORALL_INTEGER",FORALL_INTEGER;
 "FORALL_INTERSECTION_OF",FORALL_INTERSECTION_OF;
+"FORALL_INT_CASES",FORALL_INT_CASES;
 "FORALL_IN_CLAUSES",FORALL_IN_CLAUSES;
 "FORALL_IN_CLOSURE",FORALL_IN_CLOSURE;
 "FORALL_IN_CLOSURE_EQ",FORALL_IN_CLOSURE_EQ;
@@ -9094,6 +9098,7 @@ theorems :=
 "OEP",OEP;
 "ONE",ONE;
 "ONE_ONE",ONE_ONE;
+"ONE_OR_PRIME",ONE_OR_PRIME;
 "ONORM",ONORM;
 "ONORM_ADJOINT",ONORM_ADJOINT;
 "ONORM_CMUL",ONORM_CMUL;
@@ -12988,6 +12993,7 @@ theorems :=
 "poset",poset;
 "positive_definite",positive_definite;
 "positive_semidefinite",positive_semidefinite;
+"prime",prime;
 "prod_metric",prod_metric;
 "prod_topology",prod_topology;
 "prod_tybij",prod_tybij;