100/ballot.ml

   1 (* ========================================================================= *)
   2 (* Ballot problem.                                                           *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/binomial.ml";;
   6
   7 prioritize_num();;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* Restricted function space.                                                *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 parse_as_infix("-->",(13,"right"));;
  14
  15 let funspace = new_definition
  16  `(s --> t) = {f:A->B | (!x. x IN s ==> f(x) IN t) /\
  17                         (!x. ~(x IN s) ==> f(x) = @y. T)}`;;
  18
  19 let FUNSPACE_EMPTY = prove
  20  (`({} --> t) = {(\x. @y. T)}`,
  21   REWRITE_TAC[EXTENSION; IN_SING; funspace; IN_ELIM_THM; NOT_IN_EMPTY] THEN
  22   REWRITE_TAC[FUN_EQ_THM]);;
  23
  24 let HAS_SIZE_FUNSPACE = prove
  25  (`!s:A->bool t:B->bool m n.
  26         s HAS_SIZE m /\ t HAS_SIZE n ==> (s --> t) HAS_SIZE (n EXP m)`,
  27   REWRITE_TAC[HAS_SIZE; GSYM CONJ_ASSOC] THEN
  28   ONCE_REWRITE_TAC[IMP_CONJ] THEN
  29   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
  30   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN CONJ_TAC THENL
  31    [SIMP_TAC[CARD_CLAUSES; FINITE_RULES; FUNSPACE_EMPTY; NOT_IN_EMPTY] THEN
  32     REPEAT GEN_TAC THEN DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
  33     ASM_REWRITE_TAC[EXP; ARITH];
  34     ALL_TAC] THEN
  35   REWRITE_TAC[GSYM HAS_SIZE] THEN REPEAT STRIP_TAC THEN
  36   SUBGOAL_THEN
  37    `(x INSERT s) --> t =
  38         IMAGE (\(y:B,g) u:A. if u = x then y else g(u))
  39               {y,g | y IN t /\ g IN s --> t}`
  40   SUBST1_TAC THENL
  41    [REWRITE_TAC[EXTENSION; IN_IMAGE; funspace; IN_ELIM_THM] THEN
  42     ONCE_REWRITE_TAC[TAUT `(a /\ b /\ c) /\ d <=> d /\ a /\ b /\ c`] THEN
  43     REWRITE_TAC[PAIR_EQ; EXISTS_PAIR_THM; GSYM CONJ_ASSOC] THEN
  44     REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
  45     CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
  46     X_GEN_TAC `f:A->B` THEN EQ_TAC THENL
  47      [STRIP_TAC THEN MAP_EVERY EXISTS_TAC
  48        [`(f:A->B) x`; `\u. if u = x then @y. T else (f:A->B) u`] THEN
  49       REWRITE_TAC[FUN_EQ_THM] THEN ASM_MESON_TAC[IN_INSERT];
  50       REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
  51       MAP_EVERY X_GEN_TAC [`y:B`; `g:A->B`] THEN
  52       STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
  53       ASM_MESON_TAC[IN_INSERT]];
  54     ALL_TAC] THEN
  55   MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN CONJ_TAC THENL
  56    [REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_THM] THEN
  57     CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
  58     ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ d <=> d /\ a /\ b`] THEN
  59     REWRITE_TAC[PAIR_EQ; EXISTS_PAIR_THM; GSYM CONJ_ASSOC] THEN
  60     REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
  61     REWRITE_TAC[FUN_EQ_THM; funspace; IN_ELIM_THM] THEN
  62     REPEAT GEN_TAC THEN STRIP_TAC THEN CONJ_TAC THENL
  63      [ASM_MESON_TAC[IN_INSERT]; ALL_TAC] THEN
  64     X_GEN_TAC `u:A` THEN ASM_CASES_TAC `u:A = x` THEN ASM_MESON_TAC[];
  65     ALL_TAC] THEN
  66   FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN ASM_SIMP_TAC[CARD_CLAUSES; EXP] THEN
  67   MATCH_MP_TAC HAS_SIZE_PRODUCT THEN ASM_MESON_TAC[]);;
  68
  69 let FINITE_FUNSPACE = prove
  70  (`!s t. FINITE s /\ FINITE t ==> FINITE(s --> t)`,
  71   MESON_TAC[HAS_SIZE_FUNSPACE; HAS_SIZE]);;
  72
  73 (* ------------------------------------------------------------------------- *)
  74 (* Definition of the problem.                                                *)
  75 (* ------------------------------------------------------------------------- *)
  76
  77 let vote_INDUCT,vote_RECURSION = define_type
  78  "vote = A | B";;
  79
  80 let all_countings = new_definition
  81  `all_countings a b =
  82         let n = a + b in
  83         CARD {f | f IN (1..n --> {A,B}) /\
  84                   CARD { i | i IN 1..n /\ f(i) = A} = a /\
  85                   CARD { i | i IN 1..n /\ f(i) = B} = b}`;;
  86
  87 let valid_countings = new_definition
  88  `valid_countings a b =
  89         let n = a + b in
  90         CARD {f | f IN (1..n --> {A,B}) /\
  91                   CARD { i | i IN 1..n /\ f(i) = A} = a /\
  92                   CARD { i | i IN 1..n /\ f(i) = B} = b /\
  93                   !m. 1 <= m /\ m <= n
  94                       ==> CARD { i | i IN 1..m /\ f(i) = A} >
  95                           CARD { i | i IN 1..m /\ f(i) = B}}`;;
  96
  97 (* ------------------------------------------------------------------------- *)
  98 (* Various lemmas.                                                           *)
  99 (* ------------------------------------------------------------------------- *)
 100
 101 let vote_CASES = cases "vote"
 102 and vote_DISTINCT = distinctness "vote";;
 103
 104 let FINITE_COUNTINGS = prove
 105  (`FINITE {f | f IN (1..n --> {A,B}) /\ P f}`,
 106   MATCH_MP_TAC FINITE_RESTRICT THEN
 107   MATCH_MP_TAC FINITE_FUNSPACE THEN
 108   REWRITE_TAC[FINITE_NUMSEG; FINITE_INSERT; FINITE_RULES]);;
 109
 110 let UNIV_VOTE = prove
 111  (`(:vote) = {A,B}`,
 112   REWRITE_TAC[EXTENSION; IN_UNIV; IN_INSERT; NOT_IN_EMPTY; vote_CASES]);;
 113
 114 let ADD1_NOT_IN_NUMSEG = prove
 115  (`!m n. ~((n + 1) IN m..n)`,
 116   REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);;
 117
 118 let NUMSEG_1_CLAUSES = prove
 119  (`!n. 1..(n+1) = (n + 1) INSERT (1..n)`,
 120   REWRITE_TAC[GSYM ADD1; NUMSEG_CLAUSES; ARITH_RULE `1 <= SUC n`]);;
 121
 122 let NUMSEG_RESTRICT_SUC = prove
 123  (`{i | i IN 1..(n+1) /\ P i} =
 124         if P(n + 1) then (n + 1) INSERT {i | i IN 1..n /\ P i}
 125         else {i | i IN 1..n /\ P i}`,
 126   REPEAT GEN_TAC THEN COND_CASES_TAC THEN
 127   ASM_REWRITE_TAC[EXTENSION; IN_ELIM_THM; NUMSEG_1_CLAUSES; IN_INSERT] THEN
 128   ASM_MESON_TAC[ADD1_NOT_IN_NUMSEG]);;
 129
 130 let CARD_NUMSEG_RESTRICT_SUC = prove
 131  (`CARD {i | i IN 1..(n+1) /\ P i} =
 132         if P(n + 1) then CARD {i | i IN 1..n /\ P i} + 1
 133         else CARD {i | i IN 1..n /\ P i}`,
 134   REPEAT GEN_TAC THEN REWRITE_TAC[NUMSEG_RESTRICT_SUC] THEN
 135   COND_CASES_TAC THEN
 136   ASM_SIMP_TAC[CARD_CLAUSES; FINITE_RESTRICT; FINITE_NUMSEG] THEN
 137   REWRITE_TAC[IN_ELIM_THM; ADD1_NOT_IN_NUMSEG; ADD1]);;
 138
 139 let FORALL_RANGE_SUC = prove
 140  (`(!i. 1 <= i /\ i <= n + 1 ==> P i) <=>
 141       P(n + 1) /\ (!i. 1 <= i /\ i <= n ==> P i)`,
 142   REWRITE_TAC[ARITH_RULE `i <= n + 1 <=> i <= n \/ i = n + 1`] THEN
 143   MESON_TAC[ARITH_RULE `1 <= n + 1`]);;
 144
 145 let IN_NUMSEG_RESTRICT_FALSE = prove
 146  (`m <= n
 147    ==> (i IN 1..m /\ (if i = n + 1 then p i else q i) <=> i IN 1..m /\ q i)`,
 148   REWRITE_TAC[IN_NUMSEG] THEN
 149   MESON_TAC[ARITH_RULE `i <= m /\ m <= n ==> ~(i = n + 1)`]);;
 150
 151 let CARD_NUMSEG_RESTRICT_EXTREMA = prove
 152  (`(CARD {i | i IN 1..n /\ P i} = n <=> !i. 1 <= i /\ i <= n ==> P i) /\
 153    (CARD {i | i IN 1..n /\ P i} = 0 <=> !i. 1 <= i /\ i <= n ==> ~(P i))`,
 154   SIMP_TAC[CARD_EQ_0; FINITE_RESTRICT; FINITE_NUMSEG] THEN
 155   MP_TAC(ISPECL [`{i | i IN 1..n /\ P i}`; `1..n`] SUBSET_CARD_EQ) THEN
 156   SIMP_TAC[FINITE_NUMSEG; SUBSET; IN_ELIM_THM; CARD_NUMSEG_1] THEN
 157   DISCH_THEN(K ALL_TAC) THEN
 158   REWRITE_TAC[EXTENSION; NOT_IN_EMPTY; IN_NUMSEG; IN_ELIM_THM] THEN
 159   MESON_TAC[]);;
 160
 161 let VOTE_NOT_EQ = prove
 162  (`(!x. ~(x = A) <=> x = B) /\
 163    (!x. ~(x = B) <=> x = A)`,
 164   MESON_TAC[vote_CASES; vote_DISTINCT]);;
 165
 166 let FUNSPACE_FIXED = prove
 167  (`{f | f IN (s --> t) /\ (!i. i IN s ==> f i = a)} =
 168    if s = {} \/ a IN t then {(\i. if i IN s then a else @x. T)} else {}`,
 169   REWRITE_TAC[EXTENSION; NOT_IN_EMPTY] THEN GEN_TAC THEN
 170   COND_CASES_TAC THEN
 171   ASM_REWRITE_TAC[IN_ELIM_THM; funspace; NOT_IN_EMPTY; IN_SING] THEN
 172   REWRITE_TAC[FUN_EQ_THM] THEN ASM_MESON_TAC[]);;
 173
 174 let COUNTING_LEMMA = prove
 175  (`CARD {f | f IN (1..(n+1) --> {A,B}) /\ P f} =
 176    CARD {f | f IN (1..n --> {A,B}) /\ P (\i. if i = n + 1 then A else f i)} +
 177    CARD {f | f IN (1..n --> {A,B}) /\ P (\i. if i = n + 1 then B else f i)}`,
 178   MATCH_MP_TAC EQ_TRANS THEN
 179   EXISTS_TAC `CARD {f | f IN (1..(n+1) --> {A,B}) /\ f(n+1) = A /\ P f} +
 180               CARD {f | f IN (1..(n+1) --> {A,B}) /\ f(n+1) = B /\ P f}` THEN
 181   CONJ_TAC THENL
 182    [CONV_TAC SYM_CONV THEN MATCH_MP_TAC CARD_UNION_EQ THEN
 183     REWRITE_TAC[FINITE_COUNTINGS; EXTENSION; IN_INTER; IN_UNION] THEN
 184     REWRITE_TAC[IN_ELIM_THM; NOT_IN_EMPTY] THEN
 185     MESON_TAC[vote_CASES; vote_DISTINCT];
 186     ALL_TAC] THEN
 187   BINOP_TAC THEN
 188   MATCH_MP_TAC BIJECTIONS_CARD_EQ THEN
 189   EXISTS_TAC `\f i. if i = n + 1 then @x:vote. T else f i` THENL
 190    [EXISTS_TAC `\f i. if i = n + 1 then A else f i`;
 191     EXISTS_TAC `\f i. if i = n + 1 then B else f i`] THEN
 192   REWRITE_TAC[FINITE_COUNTINGS] THEN
 193   REWRITE_TAC[IN_ELIM_THM; funspace; GSYM UNIV_VOTE; IN_UNIV] THEN
 194   REWRITE_TAC[NUMSEG_1_CLAUSES; IN_INSERT] THEN REPEAT STRIP_TAC THEN
 195   TRY(FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (MESON[]
 196    `P x ==> x = y ==> P y`))) THEN
 197   TRY(GEN_REWRITE_TAC I [FUN_EQ_THM]) THEN ASM_MESON_TAC[ADD1_NOT_IN_NUMSEG]);;
 198
 199 (* ------------------------------------------------------------------------- *)
 200 (* Recurrence relations.                                                     *)
 201 (* ------------------------------------------------------------------------- *)
 202
 203 let ALL_COUNTINGS_0 = prove
 204  (`!a. all_countings a 0 = 1 /\ all_countings 0 a = 1`,
 205   REWRITE_TAC[all_countings; CARD_NUMSEG_RESTRICT_EXTREMA; GSYM IN_NUMSEG;
 206               LET_DEF; LET_END_DEF; ADD_CLAUSES; VOTE_NOT_EQ] THEN
 207   REWRITE_TAC[FUNSPACE_FIXED; IN_INSERT] THEN
 208   SIMP_TAC[CARD_CLAUSES; FINITE_RULES; NOT_IN_EMPTY; ARITH_SUC]);;
 209
 210 let VALID_COUNTINGS_0 = prove
 211  (`valid_countings 0 0 = 1 /\
 212    !a. valid_countings (SUC a) 0 = 1 /\ valid_countings 0 (SUC a) = 0`,
 213   let lemma = prove
 214    (`{x} INTER s = if x IN s then {x} else {}`,
 215     COND_CASES_TAC THEN ASM SET_TAC[]) in
 216   REWRITE_TAC[valid_countings; CARD_NUMSEG_RESTRICT_EXTREMA; GSYM IN_NUMSEG;
 217               LET_DEF; LET_END_DEF; ADD_CLAUSES; VOTE_NOT_EQ;
 218               TAUT `a /\ a /\ b <=> a /\ b`] THEN
 219   REWRITE_TAC[CONJUNCT1 NUMSEG_CLAUSES; ARITH_EQ; NOT_IN_EMPTY] THEN
 220   CONJ_TAC THENL
 221    [REWRITE_TAC[funspace; IN_ELIM_THM; NOT_IN_EMPTY; GSYM FUN_EQ_THM] THEN
 222     REWRITE_TAC[SET_RULE `{x | x = a} = {a}`] THEN
 223     SIMP_TAC[CARD_CLAUSES; FINITE_RULES; NOT_IN_EMPTY; ARITH];
 224     ALL_TAC] THEN
 225   ONCE_REWRITE_TAC[SET_RULE `{x | P x /\ Q x /\ R x} =
 226                              {x | P x /\ Q x} INTER {x | R x}`] THEN
 227   REWRITE_TAC[FUNSPACE_FIXED; IN_INSERT; lemma] THEN
 228   REWRITE_TAC[IN_ELIM_THM] THEN
 229   GEN_TAC THEN CONJ_TAC THEN COND_CASES_TAC THEN
 230   ASM_SIMP_TAC[CARD_CLAUSES; FINITE_RULES; NOT_IN_EMPTY; ARITH] THEN
 231   POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM] THENL
 232    [X_GEN_TAC `k:num` THEN DISCH_TAC THEN
 233     MATCH_MP_TAC(ARITH_RULE `b = 0 /\ ~(a = 0) ==> a > b`) THEN
 234     ASM_SIMP_TAC[CARD_NUMSEG_RESTRICT_EXTREMA] THEN
 235     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [IN_NUMSEG]) THEN
 236     DISCH_THEN(ASSUME_TAC o MATCH_MP (ARITH_RULE
 237      `1 <= k /\ k <= a ==> 1 <= k /\ !i. i <= k ==> i <= a`)) THEN
 238     ASM_SIMP_TAC[IN_NUMSEG; vote_DISTINCT] THEN
 239     DISCH_THEN(MP_TAC o SPEC `1`) THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
 240     EXISTS_TAC `1` THEN REWRITE_TAC[NUMSEG_SING; IN_SING] THEN
 241     REWRITE_TAC[IN_NUMSEG; LE_REFL; ARITH_RULE `1 <= SUC n`] THEN
 242     MATCH_MP_TAC(ARITH_RULE `b = 0 /\ ~(a = 0) ==> ~(b > a)`) THEN
 243     ONCE_REWRITE_TAC[SET_RULE `{x | x = a /\ P x} = {x | x = a /\ P a}`] THEN
 244     REWRITE_TAC[IN_NUMSEG; LE_REFL; ARITH_RULE `1 <= SUC n`] THEN
 245     SIMP_TAC[vote_DISTINCT; SET_RULE `{x | F} = {} /\ {x | x = a} = {a}`;
 246              CARD_CLAUSES; FINITE_RULES; NOT_IN_EMPTY; ARITH]]);;
 247
 248 let ALL_COUNTINGS_SUC = prove
 249  (`!a b. all_countings (a + 1) (b + 1) =
 250                 all_countings a (b + 1) + all_countings (a + 1) b`,
 251   REPEAT GEN_TAC THEN REWRITE_TAC[all_countings] THEN
 252   SUBST1_TAC(ARITH_RULE `(a + 1) + (b + 1) = (a + b + 1) + 1`) THEN
 253   SUBST1_TAC(ARITH_RULE `(a + 1) + b = a + b + 1`) THEN
 254   ABBREV_TAC `n = a + b + 1` THEN
 255   CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
 256   GEN_REWRITE_TAC LAND_CONV [COUNTING_LEMMA] THEN
 257   REWRITE_TAC[] THEN BINOP_TAC THEN
 258   ONCE_REWRITE_TAC[COND_RAND] THEN ONCE_REWRITE_TAC[COND_RATOR] THEN
 259   REWRITE_TAC[vote_DISTINCT] THEN
 260   REWRITE_TAC[CARD_NUMSEG_RESTRICT_SUC] THEN
 261   SIMP_TAC[IN_NUMSEG_RESTRICT_FALSE; LE_REFL; EQ_ADD_RCANCEL]);;
 262
 263 let VALID_COUNTINGS_SUC = prove
 264  (`!a b. valid_countings (a + 1) (b + 1) =
 265                 if a <= b then 0
 266                 else valid_countings a (b + 1) + valid_countings (a + 1) b`,
 267   REPEAT STRIP_TAC THEN
 268   ASM_CASES_TAC `b:num < a` THEN ASM_REWRITE_TAC[GSYM NOT_LT] THEN
 269   REWRITE_TAC[valid_countings] THEN
 270   SUBST1_TAC(ARITH_RULE `(a + 1) + (b + 1) = (a + b + 1) + 1`) THEN
 271   SUBST1_TAC(ARITH_RULE `(a + 1) + b = a + b + 1`) THEN
 272   ABBREV_TAC `n = a + b + 1` THEN
 273   CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
 274   GEN_REWRITE_TAC LAND_CONV [COUNTING_LEMMA] THEN REWRITE_TAC[] THEN
 275   ONCE_REWRITE_TAC[COND_RAND] THEN ONCE_REWRITE_TAC[COND_RATOR] THEN
 276   REWRITE_TAC[vote_DISTINCT] THEN
 277   REWRITE_TAC[FORALL_RANGE_SUC] THEN
 278   REWRITE_TAC[CARD_NUMSEG_RESTRICT_SUC] THEN
 279   SIMP_TAC[IN_NUMSEG_RESTRICT_FALSE; LE_REFL; EQ_ADD_RCANCEL] THEN
 280   SIMP_TAC[MESON[] `x = a /\ y = b /\ P x y <=> x = a /\ y = b /\ P a b`] THEN
 281   ASM_REWRITE_TAC[GT; LT_ADD_RCANCEL] THEN
 282   REWRITE_TAC[SET_RULE `{x | F} = EMPTY`; CARD_CLAUSES; ADD_CLAUSES]);;
 283
 284 (* ------------------------------------------------------------------------- *)
 285 (* Main result.                                                              *)
 286 (* ------------------------------------------------------------------------- *)
 287
 288 let ALL_COUNTINGS = prove
 289  (`!a b. all_countings a b = binom(a + b,a)`,
 290   INDUCT_TAC THEN
 291   REWRITE_TAC[ADD_CLAUSES; BINOM_REFL; binom; ALL_COUNTINGS_0] THEN
 292   INDUCT_TAC THEN
 293   REWRITE_TAC[ADD_CLAUSES; BINOM_REFL; binom; ALL_COUNTINGS_0] THEN
 294   REWRITE_TAC[ARITH_RULE `1 = a + 1 <=> a = 0`; BINOM_EQ_0;
 295               ARITH_RULE `a < SUC a`] THEN
 296   REWRITE_TAC[ALL_COUNTINGS_SUC; ADD1] THEN
 297   ASM_REWRITE_TAC[binom; GSYM ADD1] THEN
 298   REWRITE_TAC[ADD_CLAUSES; ADD_AC]);;
 299
 300 let VALID_COUNTINGS = prove
 301  (`!a b. (a + b) * valid_countings a b = (a - b) * binom(a + b,a)`,
 302   INDUCT_TAC THENL
 303    [REWRITE_TAC[VALID_COUNTINGS_0; SUB_0; MULT_CLAUSES] THEN INDUCT_TAC THEN
 304     ASM_REWRITE_TAC[VALID_COUNTINGS_0; MULT_CLAUSES; ADD_CLAUSES];
 305     ALL_TAC] THEN
 306   INDUCT_TAC THENL
 307    [REWRITE_TAC[VALID_COUNTINGS_0; ADD_CLAUSES; BINOM_REFL; SUB_0];
 308     ALL_TAC] THEN
 309   REWRITE_TAC[ADD1; VALID_COUNTINGS_SUC] THEN REWRITE_TAC[GSYM ADD1] THEN
 310   COND_CASES_TAC THEN
 311   ASM_SIMP_TAC[MULT_CLAUSES; ARITH_RULE `a <= b ==> SUC a - SUC b = 0`] THEN
 312   MATCH_MP_TAC(NUM_RING
 313    `~(a + b + 1 = 0) /\
 314     (SUC a + SUC b) *
 315     ((SUC a + b) * (a + SUC b) * y + (a + SUC b) * (SUC a + b) * z) =
 316     (SUC a + b) * (a + SUC b) * w
 317     ==> (SUC a + SUC b) * (y + z) = w`) THEN
 318   ASM_REWRITE_TAC[ADD_EQ_0; ARITH] THEN
 319   MP_TAC(SPECL [`SUC b`; `a:num`] BINOM_FACT) THEN
 320   MP_TAC(SPECL [`b:num`; `SUC a`] BINOM_FACT) THEN
 321   MP_TAC(SPECL [`SUC b`; `SUC a`] BINOM_FACT) THEN
 322   REWRITE_TAC[ADD_CLAUSES; FACT] THEN
 323   SUBST1_TAC(ARITH_RULE `b + a:num = a + b`) THEN
 324   MAP_EVERY (fun t -> MP_TAC(SPEC t FACT_LT))
 325    [`a:num`; `b:num`; `a + b:num`] THEN
 326   ASM_SIMP_TAC[GSYM REAL_OF_NUM_EQ; GSYM REAL_OF_NUM_MUL; GSYM REAL_OF_NUM_ADD;
 327     GSYM REAL_OF_NUM_SUC; GSYM REAL_OF_NUM_SUB; REAL_OF_NUM_LE; LT_NZ;
 328     ARITH_RULE `~(a <= b) ==> b <= SUC a /\ SUC b <= a /\ SUC b <= SUC a`] THEN
 329   CONV_TAC REAL_RING);;
 330
 331 let BALLOT = prove
 332  (`!a b. &(valid_countings a b) =
 333             if a <= b then if b = 0 then &1 else &0
 334             else (&a - &b) / (&a + &b) *  &(all_countings a b)`,
 335   REPEAT INDUCT_TAC THEN REWRITE_TAC[ALL_COUNTINGS_0; VALID_COUNTINGS_0] THEN
 336   REWRITE_TAC[LE_REFL; REAL_MUL_LID; LE_0; NOT_SUC; CONJUNCT1 LE] THEN
 337   SIMP_TAC[REAL_ADD_RID; REAL_SUB_RZERO; REAL_DIV_REFL; REAL_OF_NUM_EQ;
 338            NOT_SUC; REAL_MUL_LID] THEN
 339   MP_TAC(SPECL [`SUC a`; `SUC b`] VALID_COUNTINGS) THEN
 340   REWRITE_TAC[GSYM ALL_COUNTINGS; LE_SUC] THEN
 341   COND_CASES_TAC THEN
 342   ASM_SIMP_TAC[ARITH_RULE `a <= b ==> (SUC a - SUC b) = 0`] THEN
 343   REWRITE_TAC[MULT_EQ_0; MULT_CLAUSES; ADD_EQ_0; NOT_SUC; REAL_OF_NUM_EQ] THEN
 344   ASM_SIMP_TAC[GSYM REAL_OF_NUM_EQ; GSYM REAL_OF_NUM_MUL; GSYM REAL_OF_NUM_ADD;
 345                GSYM REAL_OF_NUM_SUC; GSYM REAL_OF_NUM_SUB;
 346                ARITH_RULE `~(a <= b) ==> SUC b <= SUC a`] THEN
 347   CONV_TAC REAL_FIELD);;