Second update of HOL Light.

PiperOrigin-RevId: 295094515
Change-Id: I5bc27bbba611324f9f1c090e5fa1cb79e03a0704

100/arithmetic.ml

@@ -2,12 +2,23 @@
 (* Sum of an arithmetic series.                                              *)
 (* ========================================================================= *)
 
+set_jrh_lexer;;
+
+open Parser;;
+open Tactics;;
+open Simp;;
+open Nums;;
+open Arith;;
+open Ints;;
+open Iterate;;
+
+
 let ARITHMETIC_PROGRESSION_LEMMA = prove
  (`!n. nsum(0..n) (\i. a + d * i) = ((n + 1) * (2 * a + n * d)) DIV 2`,
   INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN ARITH_TAC);;
 
 let ARITHMETIC_PROGRESSION = prove
- (`!n. 1 <= n 
+ (`!n. 1 <= n
        ==> nsum(0..n-1) (\i. a + d * i) = (n * (2 * a + (n - 1) * d)) DIV 2`,
   INDUCT_TAC THEN REWRITE_TAC[ARITHMETIC_PROGRESSION_LEMMA; SUC_SUB1] THEN
   ARITH_TAC);;

100/arithmetic_geometric_mean.ml

@@ -1,8 +1,32 @@
 (* ========================================================================= *)
 (* Arithmetic-geometric mean inequality.                                     *)
 (* ========================================================================= *)
+set_jrh_lexer;;
+Pb_printer.set_file_tags ["Top100"; "arithmetic_geometric_mean.ml"];;
+
+open Parser;;
+open Equal;;
+open Bool;;
+open Tactics;;
+open Simp;;
+open Theorems;;
+open Class;;
+open Nums;;
+open Arith;;
+open Calc_num;;
+open Realax;;
+open Calc_int;;
+open Realarith;;
+open Reals;;
+open Calc_rat;;
+open Ints;;
+open Iterate;;
+open Wo;;
+
+open Products;;
+
+open Transc;;
 
-needs "Library/products.ml";;
 prioritize_real();;
 
 (* ------------------------------------------------------------------------- *)
@@ -67,7 +91,7 @@ let AGM = prove
   ASM_CASES_TAC `n = 0` THENL
    [ASM_REWRITE_TAC[PRODUCT_CLAUSES_NUMSEG; ARITH; SUM_SING_NUMSEG] THEN
     REAL_ARITH_TAC;
-    REWRITE_TAC[ADD1] THEN STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN     
+    REWRITE_TAC[ADD1] THEN STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
     EXISTS_TAC `x(n + 1) * (sum(1..n) x / &n) pow n` THEN
     ASM_SIMP_TAC[LEMMA_3; GSYM REAL_OF_NUM_ADD; LE_1;
                  ARITH_RULE `i <= n ==> i <= n + 1`] THEN
@@ -78,8 +102,6 @@ let AGM = prove
 (* Finally, reformulate in the usual way using roots.                        *)
 (* ------------------------------------------------------------------------- *)
 
-needs "Library/transc.ml";;
-
 let AGM_ROOT = prove
  (`!n a. 1 <= n /\ (!i. 1 <= i /\ i <= n ==> &0 <= a(i))
          ==> root n (product(1..n) a) <= sum(1..n) a / &n`,
@@ -93,3 +115,4 @@ let AGM_ROOT = prove
     ASM_REWRITE_TAC[IN_NUMSEG; FINITE_NUMSEG];
     MATCH_MP_TAC REAL_EQ_IMP_LE THEN MATCH_MP_TAC POW_ROOT_POS THEN
     ASM_SIMP_TAC[REAL_LE_DIV; REAL_POS; SUM_POS_LE_NUMSEG]]);;
+Pb_printer.clear_file_tags();;

100/ballot.ml

@@ -2,28 +2,102 @@
 (* Ballot problem.                                                           *)
 (* ========================================================================= *)
 
-needs "Library/binomial.ml";;
+set_jrh_lexer;;
+open Lib;;
+open Fusion;;
+open Basics;;
+open Printer;;
+open Parser;;
+open Equal;;
+open Bool;;
+open Drule;;
+open Log;;
+open Import_proofs;;
+open Tactics;;
+open Itab;;
+open Replay;;
+open Simp;;
+open Embryo_extra;;
+open Theorems;;
+open Ind_defs;;
+open Class;;
+open Trivia;;
+open Canon;;
+open Meson;;
+open Metis;;
+open Quot;;
+open Impconv;;
+open Pair;;
+open Nums;;
+open Recursion;;
+open Arith;;
+open Wf;;
+open Calc_num;;
+open Normalizer;;
+open Grobner;;
+open Ind_types;;
+open Lists;;
+open Realax;;
+open Calc_int;;
+open Realarith;;
+open Reals;;
+open Calc_rat;;
+open Ints;;
+open Sets;;
+open Iterate;;
+open Cart;;
+open Define;;
+open Help;;
+open Wo;;
+open Binary;;
+open Card;;
+open Permutations;;
+open Products;;
+open Floor;;
+open Misc;;
+open Iter;;
+
+open Vectors;;
+open Determinants;;
+open Topology;;
+open Convex;;
+open Paths;;
+open Polytope;;
+open Degree;;
+open Derivatives;;
+open Clifford;;
+open Integration;;
+open Measure;;
+
+open Binomial;;
+open Complexes;;
+open Canal;;
+open Transcendentals;;
+open Realanalysis;;
+open Moretop;;
+open Cauchy;;
+
 
 prioritize_num();;
 
 (* ------------------------------------------------------------------------- *)
 (* Restricted function space.                                                *)
 (* ------------------------------------------------------------------------- *)
 
-parse_as_infix("-->",(13,"right"));;
+parse_as_infix("-->_ballot",(13,"right"));;
 
 let funspace = new_definition
- `(s --> t) = {f:A->B | (!x. x IN s ==> f(x) IN t) /\
+ `(s -->_ballot t) = {f:A->B | (!x. x IN s ==> f(x) IN t) /\
                         (!x. ~(x IN s) ==> f(x) = @y. T)}`;;
 
 let FUNSPACE_EMPTY = prove
- (`({} --> t) = {(\x. @y. T)}`,
+ (`({} -->_ballot t) = {(\x. @y. T)}`,
   REWRITE_TAC[EXTENSION; IN_SING; funspace; IN_ELIM_THM; NOT_IN_EMPTY] THEN
   REWRITE_TAC[FUN_EQ_THM]);;
 
 let HAS_SIZE_FUNSPACE = prove
  (`!s:A->bool t:B->bool m n.
-        s HAS_SIZE m /\ t HAS_SIZE n ==> (s --> t) HAS_SIZE (n EXP m)`,
+        s HAS_SIZE m /\ t HAS_SIZE n ==> (s -->_ballot t) HAS_SIZE (n EXP m)`,
   REWRITE_TAC[HAS_SIZE; GSYM CONJ_ASSOC] THEN
   ONCE_REWRITE_TAC[IMP_CONJ] THEN
   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
@@ -34,9 +108,9 @@ let HAS_SIZE_FUNSPACE = prove
     ALL_TAC] THEN
   REWRITE_TAC[GSYM HAS_SIZE] THEN REPEAT STRIP_TAC THEN
   SUBGOAL_THEN
-   `(x INSERT s) --> t =
+   `(x INSERT s) -->_ballot t =
         IMAGE (\(y:B,g) u:A. if u = x then y else g(u))
-              {y,g | y IN t /\ g IN s --> t}`
+              {y,g | y IN t /\ g IN s -->_ballot t}`
   SUBST1_TAC THENL
    [REWRITE_TAC[EXTENSION; IN_IMAGE; funspace; IN_ELIM_THM] THEN
     ONCE_REWRITE_TAC[TAUT `(a /\ b /\ c) /\ d <=> d /\ a /\ b /\ c`] THEN
@@ -67,7 +141,7 @@ let HAS_SIZE_FUNSPACE = prove
   MATCH_MP_TAC HAS_SIZE_PRODUCT THEN ASM_MESON_TAC[]);;
 
 let FINITE_FUNSPACE = prove
- (`!s t. FINITE s /\ FINITE t ==> FINITE(s --> t)`,
+ (`!s t. FINITE s /\ FINITE t ==> FINITE(s -->_ballot t)`,
   MESON_TAC[HAS_SIZE_FUNSPACE; HAS_SIZE]);;
 
 (* ------------------------------------------------------------------------- *)
@@ -80,14 +154,14 @@ let vote_INDUCT,vote_RECURSION = define_type
 let all_countings = new_definition
  `all_countings a b =
         let n = a + b in
-        CARD {f | f IN (1..n --> {A,B}) /\
+        CARD {f | f IN (1..n -->_ballot {A,B}) /\
                   CARD { i | i IN 1..n /\ f(i) = A} = a /\
                   CARD { i | i IN 1..n /\ f(i) = B} = b}`;;
 
 let valid_countings = new_definition
  `valid_countings a b =
         let n = a + b in
-        CARD {f | f IN (1..n --> {A,B}) /\
+        CARD {f | f IN (1..n -->_ballot {A,B}) /\
                   CARD { i | i IN 1..n /\ f(i) = A} = a /\
                   CARD { i | i IN 1..n /\ f(i) = B} = b /\
                   !m. 1 <= m /\ m <= n
@@ -102,7 +176,7 @@ let vote_CASES = cases "vote"
 and vote_DISTINCT = distinctness "vote";;
 
 let FINITE_COUNTINGS = prove
- (`FINITE {f | f IN (1..n --> {A,B}) /\ P f}`,
+ (`FINITE {f | f IN (1..n -->_ballot {A,B}) /\ P f}`,
   MATCH_MP_TAC FINITE_RESTRICT THEN
   MATCH_MP_TAC FINITE_FUNSPACE THEN
   REWRITE_TAC[FINITE_NUMSEG; FINITE_INSERT; FINITE_RULES]);;
@@ -164,20 +238,20 @@ let VOTE_NOT_EQ = prove
   MESON_TAC[vote_CASES; vote_DISTINCT]);;
 
 let FUNSPACE_FIXED = prove
- (`{f | f IN (s --> t) /\ (!i. i IN s ==> f i = a)} =
+ (`{f | f IN (s -->_ballot t) /\ (!i. i IN s ==> f i = a)} =
    if s = {} \/ a IN t then {(\i. if i IN s then a else @x. T)} else {}`,
   REWRITE_TAC[EXTENSION; NOT_IN_EMPTY] THEN GEN_TAC THEN
   COND_CASES_TAC THEN
   ASM_REWRITE_TAC[IN_ELIM_THM; funspace; NOT_IN_EMPTY; IN_SING] THEN
   REWRITE_TAC[FUN_EQ_THM] THEN ASM_MESON_TAC[]);;
 
 let COUNTING_LEMMA = prove
- (`CARD {f | f IN (1..(n+1) --> {A,B}) /\ P f} =
-   CARD {f | f IN (1..n --> {A,B}) /\ P (\i. if i = n + 1 then A else f i)} +
-   CARD {f | f IN (1..n --> {A,B}) /\ P (\i. if i = n + 1 then B else f i)}`,
+ (`CARD {f | f IN (1..(n+1) -->_ballot {A,B}) /\ P f} =
+   CARD {f | f IN (1..n -->_ballot {A,B}) /\ P (\i. if i = n + 1 then A else f i)} +
+   CARD {f | f IN (1..n -->_ballot {A,B}) /\ P (\i. if i = n + 1 then B else f i)}`,
   MATCH_MP_TAC EQ_TRANS THEN
-  EXISTS_TAC `CARD {f | f IN (1..(n+1) --> {A,B}) /\ f(n+1) = A /\ P f} +
-              CARD {f | f IN (1..(n+1) --> {A,B}) /\ f(n+1) = B /\ P f}` THEN
+  EXISTS_TAC `CARD {f | f IN (1..(n+1) -->_ballot {A,B}) /\ f(n+1) = A /\ P f} +
+              CARD {f | f IN (1..(n+1) -->_ballot {A,B}) /\ f(n+1) = B /\ P f}` THEN
   CONJ_TAC THENL
    [CONV_TAC "100/ballot.ml:SYM_CONV" SYM_CONV THEN MATCH_MP_TAC CARD_UNION_EQ THEN
     REWRITE_TAC[FINITE_COUNTINGS; EXTENSION; IN_INTER; IN_UNION] THEN

100/bernoulli.ml

@@ -2,9 +2,38 @@
 (* Bernoulli numbers and polynomials; sum of kth powers.                     *)
 (* ========================================================================= *)
 
-needs "Library/binomial.ml";;
-needs "Library/analysis.ml";;
-needs "Library/transc.ml";;
+set_jrh_lexer;;
+Pb_printer.set_file_tags ["Top100"; "bernoulli.ml"];;
+
+open System;;
+open Lib;;
+open Fusion;;
+open Basics;;
+open Parser;;
+open Equal;;
+open Bool;;
+open Drule;;
+open Tactics;;
+open Simp;;
+open Theorems;;
+open Class;;
+open Meson;;
+open Pair;;
+open Nums;;
+open Arith;;
+open Calc_num;;
+open Realax;;
+open Calc_int;;
+open Realarith;;
+open Reals;;
+open Calc_rat;;
+open Ints;;
+open Iterate;;
+open Define;;
+
+open Binomial;;
+open Analysis;;
+open Transc;;
 
 prioritize_real();;
 
@@ -272,3 +301,4 @@ time SOP_CONV `sum(0..n) (\k. &k pow 18)`;;
 time SOP_CONV `sum(0..n) (\k. &k pow 19)`;;
 time SOP_CONV `sum(0..n) (\k. &k pow 20)`;;
 time SOP_CONV `sum(0..n) (\k. &k pow 21)`;;
+Pb_printer.clear_file_tags();;

100/bertrand.ml

@@ -2,12 +2,63 @@
 (* Proof of Bertrand conjecture and weak form of prime number theorem.       *)
 (* ========================================================================= *)
 
-needs "Library/prime.ml";;
-needs "Library/pocklington.ml";;
-needs "Library/analysis.ml";;
-needs "Library/transc.ml";;
-needs "Library/calc_real.ml";;
-needs "Library/floor.ml";;
+set_jrh_lexer;;
+open System;;
+open Lib;;
+open Fusion;;
+open Basics;;
+open Nets;;
+open Printer;;
+open Parser;;
+open Equal;;
+open Bool;;
+open Drule;;
+open Log;;
+open Import_proofs;;
+open Tactics;;
+open Itab;;
+open Replay;;
+open Simp;;
+open Embryo_extra;;
+open Theorems;;
+open Ind_defs;;
+open Class;;
+open Trivia;;
+open Canon;;
+open Meson;;
+open Metis;;
+open Quot;;
+open Impconv;;
+open Pair;;
+open Nums;;
+open Recursion;;
+open Arith;;
+open Wf;;
+open Calc_num;;
+open Normalizer;;
+open Grobner;;
+open Ind_types;;
+open Lists;;
+open Realax;;
+open Calc_int;;
+open Realarith;;
+open Reals;;
+open Calc_rat;;
+open Ints;;
+open Sets;;
+open Iterate;;
+open Cart;;
+open Define;;
+open Help;;
+open Wo;;
+
+
+open Floor;;
+open Analysis;;
+open Transc;;
+open Prime;;
+open Pocklington;;
+open Calc_real;;
 
 prioritize_real();;