Library/multiplicative.ml

   1 (* ========================================================================= *)
   2 (* Multiplicative functions into N or R (could add Z, C etc.)                *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/prime.ml";;
   6 needs "Library/pocklington.ml";;
   7
   8 (* ------------------------------------------------------------------------- *)
   9 (* Definition of multiplicativity of functions into N.                       *)
  10 (* ------------------------------------------------------------------------- *)
  11
  12 let multiplicative = new_definition
  13  `multiplicative f <=>
  14      f(1) = 1 /\ !m n. coprime(m,n) ==> f(m * n) = f(m) * f(n)`;;
  15
  16 let MULTIPLICATIVE_1 = prove
  17  (`!f. multiplicative f ==> f(1) = 1`,
  18   SIMP_TAC[multiplicative]);;
  19
  20 (* ------------------------------------------------------------------------- *)
  21 (* We can really ignore the value at zero.                                   *)
  22 (* ------------------------------------------------------------------------- *)
  23
  24 let MULTIPLICATIVE = prove
  25  (`multiplicative f <=>
  26         f(1) = 1 /\
  27         !m n. ~(m = 0) /\ ~(n = 0) /\ coprime(m,n) ==> f(m * n) = f(m) * f(n)`,
  28   REWRITE_TAC[multiplicative] THEN EQ_TAC THEN
  29   STRIP_TAC THEN ASM_SIMP_TAC[] THEN
  30   MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN
  31   ASM_CASES_TAC `n = 0` THEN ASM_SIMP_TAC[MULT_CLAUSES] THEN
  32   ONCE_REWRITE_TAC[COPRIME_SYM] THEN
  33   ASM_CASES_TAC `m = 0` THEN ASM_SIMP_TAC[MULT_CLAUSES] THEN
  34   ASM_MESON_TAC[COPRIME_SYM; COPRIME_0; DIVIDES_ONE; MULT_CLAUSES]);;
  35
  36 let MULTIPLICATIVE_IGNOREZERO = prove
  37  (`!f g. (!n. ~(n = 0) ==> g(n) = f(n)) /\ multiplicative f
  38          ==> multiplicative g`,
  39   REPEAT GEN_TAC THEN SIMP_TAC[MULTIPLICATIVE; ARITH_EQ] THEN
  40   REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
  41   REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
  42   DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
  43   ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[MULT_EQ_0]);;
  44
  45 (* ------------------------------------------------------------------------- *)
  46 (* A key "building block" theorem.                                           *)
  47 (* ------------------------------------------------------------------------- *)
  48
  49
  50 let MULTIPLICATIVE_CONVOLUTION = prove
  51  (`!f g. multiplicative f /\ multiplicative g
  52          ==> multiplicative (\n. nsum {d | d divides n}
  53                                       (\d. f(d) * g(n DIV d)))`,
  54   REPEAT GEN_TAC THEN
  55   GEN_REWRITE_TAC (LAND_CONV o BINOP_CONV) [multiplicative] THEN
  56   REWRITE_TAC[MULTIPLICATIVE; GSYM NSUM_LMUL] THEN STRIP_TAC THEN
  57   ASM_REWRITE_TAC[DIVIDES_ONE; DIV_1; SING_GSPEC; NSUM_SING; MULT_CLAUSES] THEN
  58   MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN STRIP_TAC THEN
  59   GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [MULT_SYM] THEN
  60   ASM_SIMP_TAC[GSYM NSUM_LMUL; NSUM_NSUM_PRODUCT; FINITE_DIVISORS] THEN
  61   CONV_TAC SYM_CONV THEN MATCH_MP_TAC NSUM_EQ_GENERAL THEN
  62   EXISTS_TAC `\(a:num,b). a * b` THEN REWRITE_TAC[EXISTS_UNIQUE_DEF] THEN
  63   REWRITE_TAC[FORALL_PAIR_THM; EXISTS_PAIR_THM; IN_ELIM_PAIR_THM] THEN
  64   CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN REWRITE_TAC[IN_ELIM_THM] THEN
  65   REWRITE_TAC[PAIR_EQ] THEN CONJ_TAC THENL
  66    [GEN_TAC THEN DISCH_THEN(ASSUME_TAC o MATCH_MP DIVISION_DECOMP) THEN
  67     CONJ_TAC THENL [ASM_MESON_TAC[MULT_SYM]; ALL_TAC] THEN
  68     MAP_EVERY X_GEN_TAC [`a1:num`; `b1:num`; `a2:num`; `b2:num`] THEN
  69     STRIP_TAC THEN FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN
  70     REWRITE_TAC[GSYM DIVIDES_ANTISYM] THEN REPEAT CONJ_TAC THEN
  71     MATCH_MP_TAC COPRIME_DIVPROD THENL
  72      (map EXISTS_TAC [`b2:num`; `b1:num`; `a2:num`; `a1:num`]) THEN
  73     ASM_MESON_TAC[COPRIME_DIVISORS; DIVIDES_REFL;
  74                   DIVIDES_RMUL; COPRIME_SYM; MULT_SYM];
  75     MAP_EVERY X_GEN_TAC [`d:num`; `e:num`] THEN STRIP_TAC THEN
  76     CONJ_TAC THENL [ASM_MESON_TAC[DIVIDES_MUL2; MULT_SYM]; ALL_TAC] THEN
  77     MP_TAC(REWRITE_RULE[divides] (ASSUME `(d:num) divides n`)) THEN
  78     DISCH_THEN(X_CHOOSE_THEN `d':num` SUBST_ALL_TAC) THEN
  79     MP_TAC(REWRITE_RULE[divides] (ASSUME `(e:num) divides m`)) THEN
  80     DISCH_THEN(X_CHOOSE_THEN `e':num` SUBST_ALL_TAC) THEN
  81     RULE_ASSUM_TAC(REWRITE_RULE[MULT_EQ_0; DE_MORGAN_THM]) THEN
  82     ONCE_REWRITE_TAC[AC MULT_AC
  83      `(e * e') * d * d':num = (d * e) * (d' * e')`] THEN
  84     ASM_SIMP_TAC[DIV_MULT; MULT_EQ_0] THEN
  85     FIRST_ASSUM(ASSUME_TAC o MATCH_MP (NUMBER_RULE
  86      `coprime(a * b,c * d) ==> coprime(c,a) /\ coprime(d,b)`)) THEN
  87     ASM_SIMP_TAC[] THEN ARITH_TAC]);;
  88
  89 let MULTIPLICATIVE_CONST = prove
  90  (`!c. multiplicative(\n. c) <=> c = 1`,
  91   GEN_TAC THEN REWRITE_TAC[multiplicative] THEN
  92   ASM_CASES_TAC `c = 1` THEN ASM_REWRITE_TAC[MULT_CLAUSES]);;
  93
  94 let MULTIPLICATIVE_DELTA = prove
  95  (`multiplicative(\n. if n = 1 then 1 else 0)`,
  96   REWRITE_TAC[MULTIPLICATIVE; MULT_EQ_1] THEN ARITH_TAC);;
  97
  98 let MULTIPLICATIVE_DIVISORSUM = prove
  99  (`!f. multiplicative f ==> multiplicative (\n. nsum {d | d divides n} f)`,
 100   REPEAT STRIP_TAC THEN
 101   MP_TAC(ISPECL [`f:num->num`; `\n:num. 1`] MULTIPLICATIVE_CONVOLUTION) THEN
 102   ASM_REWRITE_TAC[MULT_CLAUSES; MULTIPLICATIVE_CONST; ETA_AX]);;
 103
 104 (* ------------------------------------------------------------------------- *)
 105 (* Some particular multiplicative functions.                                 *)
 106 (* ------------------------------------------------------------------------- *)
 107
 108 let MULTIPLICATIVE_ID = prove
 109  (`multiplicative(\n. n)`,
 110   REWRITE_TAC[multiplicative]);;
 111
 112 let MULTIPLICATIVE_POWERSUM = prove
 113  (`!k. multiplicative(\n. nsum {d | d divides n} (\d. d EXP k))`,
 114   GEN_TAC THEN MATCH_MP_TAC MULTIPLICATIVE_DIVISORSUM THEN
 115   REWRITE_TAC[MULTIPLICATIVE; EXP_ONE; MULT_EXP]);;
 116
 117 let sigma = new_definition
 118  `sigma(n) = if n = 0 then 0 else nsum {d | d divides n} (\i. i)`;;
 119
 120 let tau = new_definition
 121  `tau(n) = if n = 0 then 0 else CARD {d | d divides n}`;;
 122
 123 let MULTIPLICATIVE_SIGMA = prove
 124  (`multiplicative(sigma)`,
 125   MP_TAC(SPEC `1` MULTIPLICATIVE_POWERSUM) THEN
 126   MATCH_MP_TAC(REWRITE_RULE[GSYM IMP_IMP] MULTIPLICATIVE_IGNOREZERO) THEN
 127   SIMP_TAC[sigma; EXP_1]);;
 128
 129 let MULTIPLICATIVE_TAU = prove
 130  (`multiplicative(tau)`,
 131   MP_TAC(SPEC `0` MULTIPLICATIVE_POWERSUM) THEN
 132   MATCH_MP_TAC(REWRITE_RULE[GSYM IMP_IMP] MULTIPLICATIVE_IGNOREZERO) THEN
 133   SIMP_TAC[tau; EXP; NSUM_CONST; MULT_CLAUSES; FINITE_DIVISORS]);;
 134
 135 let MULTIPLICATIVE_PHI = prove
 136  (`multiplicative(phi)`,
 137   REWRITE_TAC[multiplicative; PHI_MULTIPLICATIVE; PHI_1]);;
 138
 139 let MULTIPLICATIVE_GCD = prove
 140  (`!n. multiplicative(\m. gcd(n,m))`,
 141   REWRITE_TAC[multiplicative; ONCE_REWRITE_RULE[GCD_SYM] GCD_1] THEN
 142   ONCE_REWRITE_TAC[GSYM DIVIDES_ANTISYM] THEN NUMBER_TAC);;
 143
 144 (* ------------------------------------------------------------------------- *)
 145 (* Uniqueness of multiplicative functions if equal on prime powers.          *)
 146 (* ------------------------------------------------------------------------- *)
 147
 148 let MULTIPLICATIVE_UNIQUE = prove
 149  (`!f g. multiplicative f /\ multiplicative g /\
 150          (!p k. prime p ==> f(p EXP k) = g(p EXP k))
 151          ==> !n. ~(n = 0) ==> f n = g n`,
 152   REPEAT GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC num_WF THEN
 153   X_GEN_TAC `n:num` THEN REPEAT STRIP_TAC THEN
 154   FIRST_X_ASSUM(DISJ_CASES_THEN2 ASSUME_TAC MP_TAC o MATCH_MP (ARITH_RULE
 155    `~(n = 0) ==> n = 1 \/ 1 < n`))
 156   THENL [ASM_MESON_TAC[multiplicative]; ALL_TAC] THEN
 157   SPEC_TAC(`n:num`,`n:num`) THEN MATCH_MP_TAC INDUCT_COPRIME_STRONG THEN
 158   ASM_MESON_TAC[multiplicative]);;
 159
 160 (* ------------------------------------------------------------------------- *)
 161 (* Derive the divisor-sum identity for phi from this.                        *)
 162 (* ------------------------------------------------------------------------- *)
 163
 164 let PHI_DIVISORSUM = prove
 165  (`!n. ~(n = 0) ==> nsum {d | d divides n} (\d. phi(d)) = n`,
 166   MATCH_MP_TAC MULTIPLICATIVE_UNIQUE THEN REWRITE_TAC[MULTIPLICATIVE_ID] THEN
 167   SIMP_TAC[MULTIPLICATIVE_DIVISORSUM; ETA_AX; MULTIPLICATIVE_PHI] THEN
 168   SIMP_TAC[DIVIDES_PRIMEPOW; SET_RULE
 169     `{d | ?i. i <= k /\ d = p EXP i} = IMAGE (\i. p EXP i) {i | i <= k}`] THEN
 170   SIMP_TAC[NSUM_IMAGE; EQ_PRIMEPOW; o_DEF; PHI_PRIMEPOW] THEN
 171   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
 172   INDUCT_TAC THEN REWRITE_TAC[LE; NOT_SUC] THEN
 173   REWRITE_TAC[CONJUNCT1 EXP; SET_RULE `{x | x = 0} = {0}`; NSUM_SING] THEN
 174   REWRITE_TAC[SET_RULE `{i | i = a \/ i <= b} = a INSERT {i | i <= b}`] THEN
 175   ASM_SIMP_TAC[NSUM_CLAUSES; FINITE_NUMSEG_LE; NOT_SUC] THEN
 176   REWRITE_TAC[IN_ELIM_THM; SUC_SUB1; ARITH_RULE `~(SUC k <= k)`] THEN
 177   MATCH_MP_TAC(ARITH_RULE `a:num <= b ==> b - a + a = b`) THEN
 178   ASM_SIMP_TAC[LE_EXP; PRIME_IMP_NZ] THEN ARITH_TAC);;
 179
 180 (* ------------------------------------------------------------------------- *)
 181 (* Now the real analog.                                                      *)
 182 (* ------------------------------------------------------------------------- *)
 183
 184 let real_multiplicative = new_definition
 185  `real_multiplicative (f:num->real) <=>
 186      f(1) = &1 /\ !m n. coprime(m,n) ==> f(m * n) = f(m) * f(n)`;;
 187
 188 let REAL_MULTIPLICATIVE = prove
 189  (`real_multiplicative f <=>
 190         f(1) = &1 /\
 191         !m n. ~(m = 0) /\ ~(n = 0) /\ coprime(m,n) ==> f(m * n) = f(m) * f(n)`,
 192   REWRITE_TAC[real_multiplicative] THEN EQ_TAC THEN
 193   STRIP_TAC THEN ASM_SIMP_TAC[] THEN
 194   MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN
 195   ASM_CASES_TAC `n = 0` THEN
 196   ASM_SIMP_TAC[COPRIME_0; MULT_CLAUSES; REAL_MUL_LID] THEN
 197   ONCE_REWRITE_TAC[COPRIME_SYM] THEN
 198   ASM_CASES_TAC `m = 0` THEN
 199   ASM_SIMP_TAC[COPRIME_0; MULT_CLAUSES; REAL_MUL_RID] THEN
 200   ASM_MESON_TAC[COPRIME_SYM; COPRIME_0; DIVIDES_ONE; MULT_CLAUSES]);;
 201
 202 let REAL_MULTIPLICATIVE_CONST = prove
 203  (`!c. real_multiplicative(\n. c) <=> c = &1`,
 204   GEN_TAC THEN REWRITE_TAC[real_multiplicative] THEN
 205   ASM_CASES_TAC `c:real = &1` THEN ASM_REWRITE_TAC[REAL_MUL_LID]);;
 206
 207 let REAL_MULTIPLICATIVE_DELTA = prove
 208  (`real_multiplicative(\n. if n = 1 then &1 else &0)`,
 209   REWRITE_TAC[REAL_MULTIPLICATIVE; MULT_EQ_1] THEN REAL_ARITH_TAC);;
 210
 211 let REAL_MULTIPLICATIVE_IGNOREZERO = prove
 212  (`!f g. (!n. ~(n = 0) ==> g(n) = f(n)) /\ real_multiplicative f
 213          ==> real_multiplicative g`,
 214   REPEAT GEN_TAC THEN SIMP_TAC[REAL_MULTIPLICATIVE; ARITH_EQ] THEN
 215   REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 216   REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
 217   DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
 218   ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[MULT_EQ_0]);;
 219
 220 let REAL_MULTIPLICATIVE_CONVOLUTION = prove
 221  (`!f g. real_multiplicative f /\ real_multiplicative g
 222          ==> real_multiplicative (\n. sum {d | d divides n}
 223                                           (\d. f(d) * g(n DIV d)))`,
 224   REPEAT GEN_TAC THEN
 225   GEN_REWRITE_TAC (LAND_CONV o BINOP_CONV) [real_multiplicative] THEN
 226   REWRITE_TAC[REAL_MULTIPLICATIVE; GSYM SUM_LMUL] THEN STRIP_TAC THEN
 227   ASM_REWRITE_TAC[DIVIDES_ONE; DIV_1; SING_GSPEC; SUM_SING; REAL_MUL_LID] THEN
 228   MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN STRIP_TAC THEN
 229   GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [REAL_MUL_SYM] THEN
 230   ASM_SIMP_TAC[GSYM SUM_LMUL; SUM_SUM_PRODUCT; FINITE_DIVISORS] THEN
 231   CONV_TAC SYM_CONV THEN MATCH_MP_TAC SUM_EQ_GENERAL THEN
 232   EXISTS_TAC `\(a:num,b). a * b` THEN REWRITE_TAC[EXISTS_UNIQUE_DEF] THEN
 233   REWRITE_TAC[FORALL_PAIR_THM; EXISTS_PAIR_THM; IN_ELIM_PAIR_THM] THEN
 234   REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN CONJ_TAC THENL
 235    [GEN_TAC THEN DISCH_THEN(ASSUME_TAC o MATCH_MP DIVISION_DECOMP) THEN
 236     CONJ_TAC THENL [ASM_MESON_TAC[MULT_SYM]; ALL_TAC] THEN
 237     MAP_EVERY X_GEN_TAC [`a1:num`; `b1:num`; `a2:num`; `b2:num`] THEN
 238     STRIP_TAC THEN FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN
 239     REWRITE_TAC[GSYM DIVIDES_ANTISYM] THEN REPEAT CONJ_TAC THEN
 240     MATCH_MP_TAC COPRIME_DIVPROD THENL
 241      (map EXISTS_TAC [`b2:num`; `b1:num`; `a2:num`; `a1:num`]) THEN
 242     ASM_MESON_TAC[COPRIME_DIVISORS; DIVIDES_REFL;
 243                   DIVIDES_RMUL; COPRIME_SYM; MULT_SYM];
 244     MAP_EVERY X_GEN_TAC [`d:num`; `e:num`] THEN STRIP_TAC THEN
 245     CONJ_TAC THENL [ASM_MESON_TAC[DIVIDES_MUL2; MULT_SYM]; ALL_TAC] THEN
 246     MP_TAC(REWRITE_RULE[divides] (ASSUME `(d:num) divides n`)) THEN
 247     DISCH_THEN(X_CHOOSE_THEN `d':num` SUBST_ALL_TAC) THEN
 248     MP_TAC(REWRITE_RULE[divides] (ASSUME `(e:num) divides m`)) THEN
 249     DISCH_THEN(X_CHOOSE_THEN `e':num` SUBST_ALL_TAC) THEN
 250     RULE_ASSUM_TAC(REWRITE_RULE[MULT_EQ_0; DE_MORGAN_THM]) THEN
 251     ONCE_REWRITE_TAC[AC MULT_AC
 252      `(e * e') * d * d':num = (d * e) * (d' * e')`] THEN
 253     ASM_SIMP_TAC[DIV_MULT; MULT_EQ_0] THEN
 254     FIRST_ASSUM(ASSUME_TAC o MATCH_MP (NUMBER_RULE
 255      `coprime(a * b,c * d) ==> coprime(c,a) /\ coprime(d,b)`)) THEN
 256     ASM_SIMP_TAC[] THEN REAL_ARITH_TAC]);;
 257
 258 let REAL_MULTIPLICATIVE_DIVISORSUM = prove
 259  (`!f. real_multiplicative f
 260        ==> real_multiplicative (\n. sum {d | d divides n} f)`,
 261   REPEAT STRIP_TAC THEN
 262   MP_TAC(ISPECL [`f:num->real`; `(\n. &1):num->real`]
 263      REAL_MULTIPLICATIVE_CONVOLUTION) THEN
 264   ASM_REWRITE_TAC[REAL_MUL_RID; REAL_MULTIPLICATIVE_CONST; ETA_AX]);;
 265
 266 (* ------------------------------------------------------------------------- *)
 267 (* The Mobius function (into the reals).                                     *)
 268 (* ------------------------------------------------------------------------- *)
 269
 270 prioritize_real();;
 271
 272 let mobius = new_definition
 273  `mobius(n) = if ?p. prime p /\ (p EXP 2) divides n then &0
 274               else --(&1) pow CARD {p | prime p /\ p divides n}`;;
 275
 276 let MOBIUS_0 = prove
 277  (`mobius 0 = &0`,
 278   REWRITE_TAC[mobius] THEN MP_TAC(SPEC `2 EXP 2` DIVIDES_0) THEN
 279   MESON_TAC[PRIME_2]);;
 280
 281 let MOBIUS_1 = prove
 282  (`mobius 1 = &1`,
 283   REWRITE_TAC[mobius; DIVIDES_ONE; EXP_EQ_1; ARITH] THEN
 284   COND_CASES_TAC THENL [ASM_MESON_TAC[PRIME_1]; ALL_TAC] THEN
 285   SUBGOAL_THEN `{p | prime p /\ p = 1} = {}`
 286    (fun th -> SIMP_TAC[th; CARD_CLAUSES; real_pow]) THEN SET_TAC[PRIME_1]);;
 287
 288 let REAL_ABS_MOBIUS = prove
 289  (`!n. abs(mobius n) <= &1`,
 290   GEN_TAC THEN REWRITE_TAC[mobius] THEN COND_CASES_TAC THEN
 291   REWRITE_TAC[REAL_ABS_POW; REAL_ABS_NEG; REAL_POW_ONE; REAL_ABS_NUM] THEN
 292   CONV_TAC REAL_RAT_REDUCE_CONV);;
 293
 294 let MOBIUS_MULT = prove
 295  (`!a b. coprime(a,b) ==> mobius(a * b) = mobius a * mobius b`,
 296   REPEAT STRIP_TAC THEN REWRITE_TAC[mobius] THEN
 297   ASM_CASES_TAC `?p. prime p /\ (p EXP 2) divides a` THENL
 298    [ASM_CASES_TAC `?p. prime p /\ p EXP 2 divides (a * b)` THEN
 299     ASM_REWRITE_TAC[REAL_MUL_LZERO] THEN ASM_MESON_TAC[DIVIDES_RMUL];
 300     ALL_TAC] THEN
 301   ASM_CASES_TAC `?p. prime p /\ (p EXP 2) divides b` THENL
 302    [ASM_CASES_TAC `?p. prime p /\ p EXP 2 divides (a * b)` THEN
 303     ASM_REWRITE_TAC[REAL_MUL_RZERO] THEN ASM_MESON_TAC[DIVIDES_LMUL];
 304     ALL_TAC] THEN
 305   ASM_CASES_TAC `?p. prime p /\ p EXP 2 divides (a * b)` THENL
 306    [ASM_MESON_TAC[PRIME_DIVPROD_POW]; ALL_TAC] THEN
 307   ASM_REWRITE_TAC[GSYM REAL_POW_ADD] THEN AP_TERM_TAC THEN
 308   CONV_TAC SYM_CONV THEN MATCH_MP_TAC CARD_UNION_EQ THEN
 309   ASM_CASES_TAC `a = 0` THENL [ASM_MESON_TAC[PRIME_2; DIVIDES_0]; ALL_TAC] THEN
 310   ASM_CASES_TAC `b = 0` THENL [ASM_MESON_TAC[PRIME_2; DIVIDES_0]; ALL_TAC] THEN
 311   CONJ_TAC THENL
 312    [MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{p | p divides a * b}` THEN
 313     ASM_SIMP_TAC[FINITE_DIVISORS; MULT_EQ_0] THEN SET_TAC[];
 314     SIMP_TAC[EXTENSION; IN_INTER; NOT_IN_EMPTY; IN_UNION; AND_FORALL_THM] THEN
 315     X_GEN_TAC `p:num` THEN REWRITE_TAC[IN_ELIM_THM] THEN
 316     UNDISCH_TAC `~(?p. prime p /\ p EXP 2 divides a * b)` THEN
 317     REWRITE_TAC[NOT_EXISTS_THM] THEN DISCH_THEN(MP_TAC o SPEC `p:num`) THEN
 318     ASM_CASES_TAC `prime p` THEN ASM_SIMP_TAC[PRIME_DIVPROD_EQ] THEN
 319     REWRITE_TAC[CONTRAPOS_THM; EXP_2] THEN CONV_TAC NUMBER_RULE]);;
 320
 321 let REAL_MULTIPLICATIVE_MOBIUS = prove
 322  (`real_multiplicative mobius`,
 323   SIMP_TAC[real_multiplicative; MOBIUS_1; MOBIUS_MULT]);;
 324
 325 let MOBIUS_PRIME = prove
 326  (`!p. prime p ==> mobius(p) = -- &1`,
 327   REPEAT STRIP_TAC THEN REWRITE_TAC[mobius] THEN COND_CASES_TAC THENL
 328    [FIRST_X_ASSUM(X_CHOOSE_THEN `q:num`
 329      (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 330     DISCH_THEN(fun th -> MP_TAC th THEN ASSUME_TAC
 331      (MATCH_MP(NUMBER_RULE `q EXP 2 divides p ==> q divides p`) th)) THEN
 332     SUBGOAL_THEN `q:num = p` SUBST_ALL_TAC THENL
 333      [ASM_MESON_TAC[DIVIDES_PRIME_PRIME]; ALL_TAC] THEN
 334     DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_LE) THEN
 335     REWRITE_TAC[ARITH_RULE `p EXP 2 <= p <=> p * p <= 1 * p`] THEN
 336     REWRITE_TAC[LE_MULT_RCANCEL] THEN
 337     FIRST_ASSUM(MP_TAC o MATCH_MP PRIME_GE_2) THEN ARITH_TAC;
 338     SUBGOAL_THEN `{q | prime q /\ q divides p} = {p}` SUBST1_TAC THENL
 339      [ASM SET_TAC[DIVIDES_PRIME_PRIME]; ALL_TAC] THEN
 340     SIMP_TAC[CARD_CLAUSES; FINITE_RULES; NOT_IN_EMPTY; ARITH; REAL_POW_1]]);;
 341
 342 let MOBIUS_PRIMEPOW = prove
 343  (`!p k. prime p ==> mobius(p EXP k) = if k = 0 then &1
 344                                        else if k = 1 then -- &1
 345                                        else &0`,
 346   REPEAT STRIP_TAC THEN
 347   ASM_CASES_TAC `k = 0` THEN ASM_REWRITE_TAC[EXP; MOBIUS_1] THEN
 348   ASM_CASES_TAC `k = 1` THEN ASM_SIMP_TAC[EXP_1; MOBIUS_PRIME] THEN
 349   REWRITE_TAC[mobius] THEN
 350   SUBGOAL_THEN `?q. prime q /\ q EXP 2 divides p EXP k`
 351    (fun th -> REWRITE_TAC[th]) THEN
 352   EXISTS_TAC `p:num` THEN ASM_SIMP_TAC[DIVIDES_PRIME_EXP_LE] THEN
 353   ASM_ARITH_TAC);;
 354
 355 let DIVISORSUM_MOBIUS = prove
 356  (`!n. 1 <= n
 357        ==> sum {d | d divides n} (\d. mobius d) = if n = 1 then &1 else &0`,
 358   REWRITE_TAC[ARITH_RULE `1 <= n <=> n = 1 \/ 1 < n`] THEN
 359   REWRITE_TAC[TAUT `(a \/ b ==> c) <=> (a ==> c) /\ (b ==> c)`] THEN
 360   SIMP_TAC[DIVIDES_ONE; SET_RULE `{x | x = a} = {a}`; SUM_SING; MOBIUS_1] THEN
 361   SIMP_TAC[ARITH_RULE `1 < n ==> ~(n = 1)`] THEN
 362   MATCH_MP_TAC INDUCT_COPRIME_STRONG THEN CONJ_TAC THENL
 363    [MP_TAC(MATCH_MP REAL_MULTIPLICATIVE_DIVISORSUM
 364                     REAL_MULTIPLICATIVE_MOBIUS) THEN
 365     SIMP_TAC[real_multiplicative; ETA_AX; REAL_MUL_LZERO];
 366     ALL_TAC] THEN
 367   MAP_EVERY X_GEN_TAC [`p:num`; `k:num`] THEN STRIP_TAC THEN
 368   MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `sum {1,p} (\d. mobius d)` THEN
 369   CONJ_TAC THENL
 370    [ALL_TAC;
 371     ASM_SIMP_TAC[SUM_CLAUSES; FINITE_RULES; NOT_IN_EMPTY; IN_SING;
 372                  MOBIUS_PRIME; MOBIUS_1; REAL_ADD_RID; REAL_ADD_RINV] THEN
 373     ASM_MESON_TAC[PRIME_1]] THEN
 374   MATCH_MP_TAC SUM_SUPERSET THEN ASM_SIMP_TAC[DIVIDES_PRIMEPOW] THEN
 375   REWRITE_TAC[SUBSET; IN_ELIM_THM; IN_INSERT; NOT_IN_EMPTY; DE_MORGAN_THM] THEN
 376   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
 377    [ASM_MESON_TAC[EXP; LE_0];
 378     ASM_MESON_TAC[EXP_1; LE_1];
 379     ASM_SIMP_TAC[MOBIUS_PRIMEPOW] THEN ASM_MESON_TAC[EXP; EXP_1]]);;
 380
 381 let MOBIUS_INVERSION = prove
 382  (`!f g. (!n. 1 <= n ==> g(n) = sum {d | d divides n} f)
 383          ==> !n. 1 <= n
 384                  ==> f(n) = sum {d | d divides n} (\d. mobius(d) * g(n DIV d))`,
 385   REPEAT STRIP_TAC THEN
 386   SUBGOAL_THEN `!d. d divides n ==> ~(n DIV d = 0)` ASSUME_TAC THENL
 387    [GEN_TAC THEN ASM_CASES_TAC `d = 0` THEN
 388     ASM_SIMP_TAC[DIVIDES_ZERO; LE_1] THEN
 389     DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_LE) THEN
 390     ASM_SIMP_TAC[LE_1; NOT_LT; DIV_EQ_0];
 391     ALL_TAC] THEN
 392   ASM_SIMP_TAC[LE_1] THEN
 393   MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
 394    `sum {d | d divides n} (\d. f(d) * (if n DIV d = 1 then &1 else &0))` THEN
 395   CONJ_TAC THENL
 396    [MATCH_MP_TAC EQ_TRANS THEN
 397     EXISTS_TAC `sum {n} (\d. f(d) * (if n DIV d = 1 then &1 else &0))` THEN
 398     CONJ_TAC THENL
 399      [ASM_SIMP_TAC[SUM_SING; DIV_REFL; LE_1; REAL_MUL_RID]; ALL_TAC] THEN
 400     CONV_TAC SYM_CONV THEN MATCH_MP_TAC SUM_SUPERSET THEN
 401     SIMP_TAC[SUBSET; IN_SING; IN_ELIM_THM; DIVIDES_REFL] THEN
 402     X_GEN_TAC `d:num` THEN REWRITE_TAC[DIVIDES_DIV_MULT] THEN
 403     DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
 404     COND_CASES_TAC THEN ASM_REWRITE_TAC[MULT_CLAUSES; REAL_MUL_RZERO];
 405     ASM_SIMP_TAC[GSYM DIVISORSUM_MOBIUS; LE_1] THEN
 406     REWRITE_TAC[GSYM SUM_LMUL] THEN
 407     ASM_SIMP_TAC[SUM_SUM_PRODUCT; FINITE_DIVISORS; LE_1; IN_ELIM_THM] THEN
 408     MATCH_MP_TAC SUM_EQ_GENERAL_INVERSES THEN
 409     REPEAT(EXISTS_TAC `\(m:num,n:num). (n,m)`) THEN
 410     REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_PAIR_THM] THEN
 411     CONJ_TAC THEN REPEAT GEN_TAC THEN
 412     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 413     REWRITE_TAC[REAL_MUL_SYM] THEN
 414     ASM_MESON_TAC[DIVIDES_DIVIDES_DIV; MULT_SYM;
 415                   NUMBER_RULE `(a * b) divides c ==> b divides c`]]);;