Removed trailing whitespace in many files

100/arithmetic.ml

@@ -7,7 +7,7 @@ let ARITHMETIC_PROGRESSION_LEMMA = prove
   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

@@ -67,7 +67,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

100/ballot.ml

@@ -311,7 +311,7 @@ let VALID_COUNTINGS = prove
   ASM_SIMP_TAC[MULT_CLAUSES; ARITH_RULE `a <= b ==> SUC a - SUC b = 0`] THEN
   MATCH_MP_TAC(NUM_RING
    `~(a + b + 1 = 0) /\
-    (SUC a + SUC b) * 
+    (SUC a + SUC b) *
     ((SUC a + b) * (a + SUC b) * y + (a + SUC b) * (SUC a + b) * z) =
     (SUC a + b) * (a + SUC b) * w
     ==> (SUC a + SUC b) * (y + z) = w`) THEN

100/bertrand.ml

@@ -1838,7 +1838,7 @@ let PSI_SQRT = prove
   ASM_REWRITE_TAC[ARITH_RULE `1 + n = SUC n`] THEN
   REWRITE_TAC[mangoldt; primepow] THEN
   ONCE_REWRITE_TAC[MULT_SYM] THEN REWRITE_TAC[EXP_MULT] THEN
-  REWRITE_TAC[EXP_MONO_EQ; ARITH_EQ] THEN COND_CASES_TAC THEN 
+  REWRITE_TAC[EXP_MONO_EQ; ARITH_EQ] THEN COND_CASES_TAC THEN
   ASM_REWRITE_TAC[] THEN
   REWRITE_TAC[aprimedivisor] THEN
   REPEAT AP_TERM_TAC THEN ABS_TAC THEN

100/cantor.ml

@@ -73,7 +73,7 @@ let CANTOR_TAYLOR = prove
   ASM_MESON_TAC[]);;
 
 let SURJECTIVE_COMPOSE = prove
- (`(!y. ?x. f(x) = y) /\ (!z. ?y. g(y) = z) 
+ (`(!y. ?x. f(x) = y) /\ (!z. ?y. g(y) = z)
    ==> (!z. ?x. (g o f) x = z)`,
   MESON_TAC[o_THM]);;
 
@@ -93,5 +93,5 @@ let CANTOR_JOHNSTONE = prove
     (REWRITE_RULE[NOT_EXISTS_THM] CANTOR)) THEN
   REWRITE_TAC[] THEN MATCH_MP_TAC SURJECTIVE_COMPOSE THEN
   ASM_REWRITE_TAC[SURJECTIVE_IMAGE] THEN
-  MATCH_MP_TAC INJECTIVE_SURJECTIVE_PREIMAGE THEN 
+  MATCH_MP_TAC INJECTIVE_SURJECTIVE_PREIMAGE THEN
   ASM_REWRITE_TAC[]);;

100/cubic.ml

@@ -46,7 +46,7 @@ let CUBIC_BASIC = COMPLEX_FIELD
     s3 = --s1 * (Cx(&1) - i * t) / Cx(&2) /\
     i pow 2 + Cx(&1) = Cx(&0) /\
     t pow 2 = Cx(&3)
-    ==> if p = Cx(&0) then 
+    ==> if p = Cx(&0) then
           (y pow 3 + Cx(&3) * p * y - Cx(&2) * q = Cx(&0) <=>
            y = s1 \/ y = s2 \/ y = s3)
         else
@@ -67,20 +67,20 @@ let CUBIC = prove
        let s1 = if p = Cx(&0) then ccbrt(Cx(&2) * q) else ccbrt(q + s) in
        let s2 = --s1 * (Cx(&1) + ii * csqrt(Cx(&3))) / Cx(&2)
        and s3 = --s1 * (Cx(&1) - ii * csqrt(Cx(&3))) / Cx(&2) in
-       if p = Cx(&0) then 
+       if p = Cx(&0) then
          a * x pow 3 + b * x pow 2 + c * x + d = Cx(&0) <=>
             x = s1 - b / (Cx(&3) * a) \/
-            x = s2 - b / (Cx(&3) * a) \/               
+            x = s2 - b / (Cx(&3) * a) \/
             x = s3 - b / (Cx(&3) * a)
        else
-         ~(s1 = Cx(&0)) /\                          
+         ~(s1 = Cx(&0)) /\
          (a * x pow 3 + b * x pow 2 + c * x + d = Cx(&0) <=>
              x = s1 - p / s1 - b / (Cx(&3) * a) \/
              x = s2 - p / s2 - b / (Cx(&3) * a) \/
              x = s3 - p / s3 - b / (Cx(&3) * a))`,
   DISCH_TAC THEN REPEAT LET_TAC THEN
   ABBREV_TAC `y = x + b / (Cx(&3) * a)` THEN
-  SUBGOAL_THEN 
+  SUBGOAL_THEN
    `a * x pow 3 + b * x pow 2 + c * x + d = Cx(&0) <=>
     y pow 3 + Cx(&3) * p * y - Cx(&2) * q = Cx(&0)`
   SUBST1_TAC THENL
@@ -89,7 +89,7 @@ let CUBIC = prove
     ALL_TAC] THEN
   ONCE_REWRITE_TAC[COMPLEX_RING `x = a - b <=> x + b = (a:complex)`] THEN
   ASM_REWRITE_TAC[] THEN MATCH_MP_TAC CUBIC_BASIC THEN
-  MAP_EVERY EXISTS_TAC 
+  MAP_EVERY EXISTS_TAC
    [`ii`; `csqrt(Cx(&3))`; `csqrt (q pow 2 + p pow 3)`] THEN
   ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
    [ASM_MESON_TAC[CSQRT];

100/descartes.ml

@@ -500,18 +500,18 @@ let MULTIPLICITY_UNIQUE = prove
     MAP_EVERY EXISTS_TAC [`b:num->real`; `m:num`] THEN ASM_REWRITE_TAC[]]);;
 
 let MULTIPLICITY_WORKS = prove
- (`!r n a. 
+ (`!r n a.
     (?i. i IN 0..n /\ ~(a i = &0))
-    ==> ?b m. 
+    ==> ?b m.
         ~(sum(0..m) (\i. b i * r pow i) = &0) /\
-        !x. sum(0..n) (\i. a i * x pow i) =                    
+        !x. sum(0..n) (\i. a i * x pow i) =
             (x - r) pow multiplicity (\x. sum(0..n) (\i. a i * x pow i)) r *
             sum(0..m) (\i. b i * x pow i)`,
   REWRITE_TAC[multiplicity] THEN CONV_TAC(ONCE_DEPTH_CONV SELECT_CONV) THEN
-  GEN_TAC THEN MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN  
+  GEN_TAC THEN MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN
   DISCH_TAC THEN X_GEN_TAC `a:num->real` THEN
   ASM_CASES_TAC `(a:num->real) n = &0` THENL
-   [ASM_CASES_TAC `n = 0` THEN     
+   [ASM_CASES_TAC `n = 0` THEN
     ASM_REWRITE_TAC[NUMSEG_SING; IN_SING; UNWIND_THM2]
     THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
     DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `n - 1`) THEN
@@ -532,7 +532,7 @@ let MULTIPLICITY_WORKS = prove
       ASM_REWRITE_TAC[NUMSEG_SING; IN_SING; UNWIND_THM2; SUM_SING] THEN
       REWRITE_TAC[real_pow; REAL_MUL_RID] THEN ASM_MESON_TAC[];
       ALL_TAC] THEN
-    MP_TAC(GEN `x:real` (ISPECL [`a:num->real`; `x:real`; `r:real`; `n:num`] 
+    MP_TAC(GEN `x:real` (ISPECL [`a:num->real`; `x:real`; `r:real`; `n:num`]
         REAL_SUB_POLYFUN)) THEN ASM_SIMP_TAC[LE_1; REAL_SUB_RZERO] THEN
     ABBREV_TAC `b j = sum (j + 1..n) (\i. a i * r pow (i - j - 1))` THEN
     DISCH_THEN(K ALL_TAC) THEN
@@ -551,7 +551,7 @@ let MULTIPLICITY_WORKS = prove
     STRIP_TAC THEN ASM_REWRITE_TAC[real_pow; GSYM REAL_MUL_ASSOC];
     MAP_EVERY EXISTS_TAC [`0`; `a:num->real`; `n:num`] THEN
     ASM_REWRITE_TAC[real_pow; REAL_MUL_LID]]);;
-  
+
 let MULTIPLICITY_OTHER_ROOT = prove
  (`!a n r s.
     ~(r = s) /\ (?i. i IN 0..n /\ ~(a i = &0))
@@ -560,7 +560,7 @@ let MULTIPLICITY_OTHER_ROOT = prove
   REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN
   CONV_TAC SYM_CONV THEN MATCH_MP_TAC MULTIPLICITY_UNIQUE THEN
   REWRITE_TAC[] THEN
-  MP_TAC(ISPECL [`s:real`; `n:num`; `a:num->real`] 
+  MP_TAC(ISPECL [`s:real`; `n:num`; `a:num->real`]
         MULTIPLICITY_WORKS) THEN
   ASM_REWRITE_TAC[] THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
   MAP_EVERY X_GEN_TAC [`c:num->real`; `p:num`] THEN
@@ -584,7 +584,7 @@ let MULTIPLICITY_OTHER_ROOT = prove
   MAP_EVERY X_GEN_TAC [`a:num->real`; `n:num`] THEN
   DISCH_THEN(ASSUME_TAC o GSYM) THEN
   ASM_REWRITE_TAC[real_pow; GSYM REAL_MUL_ASSOC] THEN
-  EXISTS_TAC `\i. (if 0 < i then a(i - 1) else &0) - 
+  EXISTS_TAC `\i. (if 0 < i then a(i - 1) else &0) -
                   (if i <= n then r * a i else &0)` THEN
   EXISTS_TAC `n + 1` THEN
   REWRITE_TAC[REAL_SUB_RDISTRIB; SUM_SUB_NUMSEG] THEN X_GEN_TAC `x:real` THEN
@@ -744,10 +744,10 @@ let VARIATION_POSITIVE_ROOT_MULTIPLICITY_FACTOR = prove
 (* ------------------------------------------------------------------------- *)
 
 let DESCARTES_RULE_OF_SIGNS = prove
- (`!f a n. f = (\x. sum(0..n) (\i. a i * x pow i)) /\ 
+ (`!f a n. f = (\x. sum(0..n) (\i. a i * x pow i)) /\
            (?i. i IN 0..n /\ ~(a i = &0))
            ==> ?d. EVEN d /\
-                   variation(0..n) a = 
+                   variation(0..n) a =
                    nsum {r | &0 < r /\ f(r) = &0} (\r. multiplicity f r) + d`,
   REPEAT GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
   DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN
@@ -757,7 +757,7 @@ let DESCARTES_RULE_OF_SIGNS = prove
    [ASM_CASES_TAC `n = 0` THEN
     ASM_REWRITE_TAC[NUMSEG_SING; IN_SING; UNWIND_THM2]
     THENL [ASM_MESON_TAC[]; DISCH_TAC] THEN
-    FIRST_X_ASSUM(MP_TAC o SPEC `n - 1`) THEN ANTS_TAC THENL 
+    FIRST_X_ASSUM(MP_TAC o SPEC `n - 1`) THEN ANTS_TAC THENL
      [ASM_ARITH_TAC; DISCH_THEN(MP_TAC o SPEC `a:num->real`)] THEN
     ANTS_TAC THENL
      [ASM_MESON_TAC[IN_NUMSEG; ARITH_RULE `i <= n ==> i <= n - 1 \/ i = n`];
@@ -781,17 +781,17 @@ let DESCARTES_RULE_OF_SIGNS = prove
   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
   REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
   X_GEN_TAC `r:real` THEN STRIP_TAC THEN
-  MP_TAC(ISPECL [`r:real`; `n:num`; `a:num->real`] 
+  MP_TAC(ISPECL [`r:real`; `n:num`; `a:num->real`]
     VARIATION_POSITIVE_ROOT_MULTIPLICITY_FACTOR) THEN
   ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
   MAP_EVERY X_GEN_TAC [`b:num->real`; `m:num`] THEN
   DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
-  FIRST_X_ASSUM(MP_TAC o SPEC `m:num`) THEN 
+  FIRST_X_ASSUM(MP_TAC o SPEC `m:num`) THEN
   ANTS_TAC THENL [ASM_REWRITE_TAC[]; ALL_TAC] THEN
   DISCH_THEN(MP_TAC o SPEC `b:num->real`) THEN ANTS_TAC THENL
    [EXISTS_TAC `m:num` THEN ASM_REWRITE_TAC[IN_NUMSEG; LE_REFL; LE_0];
     ALL_TAC] THEN
-  DISCH_THEN(X_CHOOSE_THEN `d1:num` 
+  DISCH_THEN(X_CHOOSE_THEN `d1:num`
     (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN
   FIRST_X_ASSUM(X_CHOOSE_THEN `d2:num`
     (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN
@@ -800,7 +800,7 @@ let DESCARTES_RULE_OF_SIGNS = prove
   MATCH_MP_TAC(ARITH_RULE
    `x + y = z ==> (x + d1) + (y + d2):num = z + d1 + d2`) THEN
   SUBGOAL_THEN
-   `{r | &0 < r /\ sum(0..n) (\i. a i * r pow i) = &0} = 
+   `{r | &0 < r /\ sum(0..n) (\i. a i * r pow i) = &0} =
     r INSERT {r | &0 < r /\ sum(0..m) (\i. b i * r pow i) = &0}`
   SUBST1_TAC THENL
    [MATCH_MP_TAC(SET_RULE `x IN s /\ s DELETE x = t ==> s = x INSERT t`) THEN

100/friendship.ml

@@ -704,18 +704,18 @@ let FRIENDSHIP = prove
   SUBGOAL_THEN `~(p divides 1)` MP_TAC THENL
    [ASM_MESON_TAC[DIVIDES_ONE; PRIME_1]; ALL_TAC] THEN
   REWRITE_TAC[] THEN
-  MATCH_MP_TAC(NUMBER_RULE 
+  MATCH_MP_TAC(NUMBER_RULE
    `!x. p divides (x + 1) /\ p divides x ==> p divides 1`) THEN
   EXISTS_TAC `m - 1` THEN ASM_REWRITE_TAC[] THEN
   ASM_SIMP_TAC[ARITH_RULE `~(m = 0) ==> m - 1 + 1 = m`] THEN
   MATCH_MP_TAC PRIME_DIVEXP THEN EXISTS_TAC `p - 2` THEN
   ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(NUMBER_RULE
    `!q c K1 K2.
-        p divides q /\ p divides c /\                
+        p divides q /\ p divides c /\
         c = (q + 1) * K1 + K2 /\
         K1 + K2 = ((q + 1) * q + 1) * nep2
         ==> p divides nep2`) THEN
-  MAP_EVERY EXISTS_TAC 
+  MAP_EVERY EXISTS_TAC
    [`m - 1`; `CARD {x:num->person | cycle friend p x}`;
     `CARD {x:num->person | path friend (p-2) x /\ x (p-2) = x 0}`;
     `CARD {x:num->person | path friend (p-2) x /\ ~(x (p-2) = x 0)}`] THEN
@@ -743,7 +743,7 @@ let FRIENDSHIP = prove
     ASM_REWRITE_TAC[] THEN
     CONJ_TAC THENL [ASM_MESON_TAC[HAS_SIZE]; ALL_TAC] THEN
     CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
-    UNDISCH_TAC `3 <= p` THEN ARITH_TAC; 
+    UNDISCH_TAC `3 <= p` THEN ARITH_TAC;
     ALL_TAC] THEN
   MP_TAC(ISPECL [`N:num`; `m:num`; `friend:person->person->bool`; `p - 2`]
                HAS_SIZE_PATHS) THEN

100/heron.ml

@@ -24,7 +24,7 @@ let SQRT_ELIM_TAC =
 (* ------------------------------------------------------------------------- *)
 
 let HERON = prove
- (`!A B C:real^2. 
+ (`!A B C:real^2.
         let a = dist(C,B)
         and b = dist(A,C)
         and c = dist(B,A) in

100/minkowski.ml

@@ -72,18 +72,18 @@ let BLICHFELDT = prove
         ==> ?x y. x IN s /\ y IN s /\ ~(x = y) /\
                   !i. 1 <= i /\ i <= dimindex(:N) ==> integer(x$i - y$i)`,
   SUBGOAL_THEN
-   `!s:real^N->bool.                                                   
+   `!s:real^N->bool.
         bounded s /\ measurable s /\ &1 < measure s
         ==> ?x y. x IN s /\ y IN s /\ ~(x = y) /\
                   !i. 1 <= i /\ i <= dimindex(:N) ==> integer(x$i - y$i)`
   ASSUME_TAC THENL
    [ALL_TAC;
-    REPEAT STRIP_TAC THEN 
-    FIRST_ASSUM(MP_TAC o SPEC `measure(s:real^N->bool) - &1` o 
+    REPEAT STRIP_TAC THEN
+    FIRST_ASSUM(MP_TAC o SPEC `measure(s:real^N->bool) - &1` o
       MATCH_MP (REWRITE_RULE[IMP_CONJ] MEASURABLE_INNER_COMPACT)) THEN
     ASM_REWRITE_TAC[REAL_SUB_LT; LEFT_IMP_EXISTS_THM] THEN
     X_GEN_TAC `c:real^N->bool` THEN STRIP_TAC THEN
-    FIRST_X_ASSUM(MP_TAC o SPEC `c:real^N->bool`) THEN 
+    FIRST_X_ASSUM(MP_TAC o SPEC `c:real^N->bool`) THEN
     ASM_SIMP_TAC[COMPACT_IMP_BOUNDED] THEN
     ANTS_TAC THENL [ASM_REAL_ARITH_TAC; ASM SET_TAC[]]] THEN
   REPEAT STRIP_TAC THEN
@@ -181,22 +181,22 @@ let BLICHFELDT = prove
 (* The usual form of the theorem.                                            *)
 (* ------------------------------------------------------------------------- *)
 
-let MINKOWSKI = prove                                                       
- (`!s:real^N->bool.                                                            
-        convex s /\                                                            
-        (!x. x IN s ==> (--x) IN s) /\                                         
-        &2 pow dimindex(:N) < measure s                                        
-        ==> ?u. ~(u = vec 0) /\                                    
-                (!i. 1 <= i /\ i <= dimindex(:N) ==> integer(u$i)) /\       
-                u IN s`,                            
+let MINKOWSKI = prove
+ (`!s:real^N->bool.
+        convex s /\
+        (!x. x IN s ==> (--x) IN s) /\
+        &2 pow dimindex(:N) < measure s
+        ==> ?u. ~(u = vec 0) /\
+                (!i. 1 <= i /\ i <= dimindex(:N) ==> integer(u$i)) /\
+                u IN s`,
   SUBGOAL_THEN
-   `!s:real^N->bool.                                                            
-        convex s /\                                                            
-        bounded s /\                                                           
-        (!x. x IN s ==> (--x) IN s) /\                                         
-        &2 pow dimindex(:N) < measure s                                        
-        ==> ?u. ~(u = vec 0) /\                                    
-                (!i. 1 <= i /\ i <= dimindex(:N) ==> integer(u$i)) /\       
+   `!s:real^N->bool.
+        convex s /\
+        bounded s /\
+        (!x. x IN s ==> (--x) IN s) /\
+        &2 pow dimindex(:N) < measure s
+        ==> ?u. ~(u = vec 0) /\
+                (!i. 1 <= i /\ i <= dimindex(:N) ==> integer(u$i)) /\
                 u IN s`
   ASSUME_TAC THENL
    [ALL_TAC;
@@ -206,7 +206,7 @@ let MINKOWSKI = prove
     ASM_SIMP_TAC[LEBESGUE_MEASURABLE_CONVEX] THEN
     DISCH_THEN(X_CHOOSE_THEN `c:real^N->bool` STRIP_ASSUME_TAC) THEN
     FIRST_ASSUM(MP_TAC o MATCH_MP COMPACT_IMP_BOUNDED) THEN
-    DISCH_THEN(X_CHOOSE_THEN `r:real` STRIP_ASSUME_TAC o SPEC `vec 0:real^N` o 
+    DISCH_THEN(X_CHOOSE_THEN `r:real` STRIP_ASSUME_TAC o SPEC `vec 0:real^N` o
       MATCH_MP BOUNDED_SUBSET_BALL) THEN
     FIRST_X_ASSUM(MP_TAC o SPEC `s INTER ball(vec 0:real^N,r)`) THEN
     ANTS_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
@@ -219,25 +219,25 @@ let MINKOWSKI = prove
     MATCH_MP_TAC MEASURABLE_CONVEX THEN
      SIMP_TAC[BOUNDED_INTER; BOUNDED_BALL] THEN
     ASM_SIMP_TAC[CONVEX_INTER; CONVEX_BALL]] THEN
-  REPEAT STRIP_TAC THEN                                            
-  MP_TAC(ISPEC `IMAGE (\x:real^N. (&1 / &2) % x) s` BLICHFELDT) THEN       
-  ASM_SIMP_TAC[MEASURABLE_SCALING; MEASURE_SCALING; MEASURABLE_CONVEX;         
-               BOUNDED_SCALING] THEN                                       
-  REWRITE_TAC[real_div; REAL_MUL_LID; REAL_ABS_INV; REAL_ABS_NUM] THEN        
-  ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN                                      
-  REWRITE_TAC[GSYM real_div; REAL_POW_INV] THEN                           
-  ASM_SIMP_TAC[REAL_LT_RDIV_EQ; REAL_LT_POW2; REAL_MUL_LID] THEN      
-  REWRITE_TAC[RIGHT_EXISTS_AND_THM; EXISTS_IN_IMAGE] THEN                   
+  REPEAT STRIP_TAC THEN
+  MP_TAC(ISPEC `IMAGE (\x:real^N. (&1 / &2) % x) s` BLICHFELDT) THEN
+  ASM_SIMP_TAC[MEASURABLE_SCALING; MEASURE_SCALING; MEASURABLE_CONVEX;
+               BOUNDED_SCALING] THEN
+  REWRITE_TAC[real_div; REAL_MUL_LID; REAL_ABS_INV; REAL_ABS_NUM] THEN
+  ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
+  REWRITE_TAC[GSYM real_div; REAL_POW_INV] THEN
+  ASM_SIMP_TAC[REAL_LT_RDIV_EQ; REAL_LT_POW2; REAL_MUL_LID] THEN
+  REWRITE_TAC[RIGHT_EXISTS_AND_THM; EXISTS_IN_IMAGE] THEN
   REWRITE_TAC[VECTOR_ARITH `inv(&2) % x:real^N = inv(&2) % y <=> x = y`] THEN
-  REWRITE_TAC[LEFT_IMP_EXISTS_THM; RIGHT_AND_EXISTS_THM] THEN                  
-  SIMP_TAC[VECTOR_MUL_COMPONENT; GSYM REAL_SUB_LDISTRIB] THEN                  
-  MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`] THEN STRIP_TAC THEN             
-  EXISTS_TAC `inv(&2) % (u - v):real^N` THEN                                   
-  ASM_SIMP_TAC[VECTOR_ARITH `inv(&2) % (u - v):real^N = vec 0 <=> u = v`] THEN 
-  ASM_SIMP_TAC[VECTOR_MUL_COMPONENT; VECTOR_SUB_COMPONENT] THEN                
-  REWRITE_TAC[VECTOR_SUB; VECTOR_ADD_LDISTRIB] THEN                        
-  FIRST_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [convex]) THEN    
-  ASM_SIMP_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV);;        
+  REWRITE_TAC[LEFT_IMP_EXISTS_THM; RIGHT_AND_EXISTS_THM] THEN
+  SIMP_TAC[VECTOR_MUL_COMPONENT; GSYM REAL_SUB_LDISTRIB] THEN
+  MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`] THEN STRIP_TAC THEN
+  EXISTS_TAC `inv(&2) % (u - v):real^N` THEN
+  ASM_SIMP_TAC[VECTOR_ARITH `inv(&2) % (u - v):real^N = vec 0 <=> u = v`] THEN
+  ASM_SIMP_TAC[VECTOR_MUL_COMPONENT; VECTOR_SUB_COMPONENT] THEN
+  REWRITE_TAC[VECTOR_SUB; VECTOR_ADD_LDISTRIB] THEN
+  FIRST_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [convex]) THEN
+  ASM_SIMP_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV);;
 
 (* ------------------------------------------------------------------------- *)
 (* A slightly sharper variant for use when the set is also closed.           *)

100/ratcountable.ml

@@ -60,9 +60,9 @@ let DENUMERABLE_RATIONALS = prove
 (* ------------------------------------------------------------------------- *)
 
 let DENUMERABLE_RATIONALS_EXPAND = prove
- (`?rat:num->real. (!n. rational(rat n)) /\ 
+ (`?rat:num->real. (!n. rational(rat n)) /\
                    (!x. rational x ==> ?!n. x = rat n)`,
   MP_TAC DENUMERABLE_RATIONALS THEN REWRITE_TAC[denumerable] THEN
   ONCE_REWRITE_TAC[CARD_EQ_SYM] THEN REWRITE_TAC[eq_c] THEN
-  REWRITE_TAC[IN_UNIV; IN_ELIM_THM] THEN 
+  REWRITE_TAC[IN_UNIV; IN_ELIM_THM] THEN
   MATCH_MP_TAC MONO_EXISTS THEN MESON_TAC[]);;