100/friendship.ml

   1 (* ========================================================================= *)
   2 (* The friendship theorem.                                                   *)
   3 (*                                                                           *)
   4 (* Proof from "Combinatorics Tutorial 2: Friendship Theorem", copyright      *)
   5 (* MathOlymp.com, 2001. Apparently due to J. Q. Longyear and T. D. Parsons.  *)
   6 (* ========================================================================= *)
   7
   8 needs "Library/prime.ml";;
   9 needs "Library/pocklington.ml";;
  10
  11 (* ------------------------------------------------------------------------- *)
  12 (* Useful inductive breakdown principle ending at gcd.                       *)
  13 (* ------------------------------------------------------------------------- *)
  14
  15 let GCD_INDUCT = prove
  16  (`!P. (!m n. P m /\ P (m + n) ==> P n)
  17        ==> !m n. P m /\ P n ==> P (gcd(m,n))`,
  18   GEN_TAC THEN STRIP_TAC THEN REPEAT GEN_TAC THEN
  19   WF_INDUCT_TAC `m + n:num` THEN REPEAT(POP_ASSUM MP_TAC) THEN
  20   MAP_EVERY (fun t -> SPEC_TAC(t,t)) [`n:num`; `m:num`] THEN
  21   MATCH_MP_TAC WLOG_LE THEN CONJ_TAC THENL
  22    [REWRITE_TAC[CONJ_ACI; GCD_SYM; ADD_SYM]; REPEAT STRIP_TAC] THEN
  23   ASM_CASES_TAC `m = 0` THENL [ASM_MESON_TAC[GCD_0]; ALL_TAC] THEN
  24   UNDISCH_TAC `!m n:num. P m /\ P (m + n) ==> P n` THEN
  25   DISCH_THEN(MP_TAC o SPECL [`m:num`; `n - m:num`]) THEN
  26   ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_SIMP_TAC[SUB_ADD; LT_IMP_LE] THEN
  27   DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPECL [`m:num`; `n - m:num`]) THEN
  28   REWRITE_TAC[IMP_IMP] THEN ANTS_TAC THENL
  29    [ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC;
  30     ALL_TAC] THEN
  31   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LE_EXISTS]) THEN
  32   DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST_ALL_TAC) THEN
  33   REWRITE_TAC[ADD_SUB2; GCD_ADD]);;
  34
  35 (* ------------------------------------------------------------------------- *)
  36 (* General theorems about loops in a sequence.                               *)
  37 (* ------------------------------------------------------------------------- *)
  38
  39 let LOOP_GCD = prove
  40  (`!x m n. (!i. x(i + m) = x(i)) /\ (!i. x(i + n) = x(i))
  41            ==> !i. x(i + gcd(m,n)) = x(i)`,
  42   GEN_TAC THEN MATCH_MP_TAC GCD_INDUCT THEN MESON_TAC[ADD_AC]);;
  43
  44 let LOOP_COPRIME = prove
  45  (`!x m n. (!i. x(i + m) = x(i)) /\ (!i. x(i + n) = x(i)) /\ coprime(m,n)
  46            ==> !i. x i = x 0`,
  47   REPEAT GEN_TAC THEN STRIP_TAC THEN INDUCT_TAC THEN REWRITE_TAC[ADD1] THEN
  48   ASM_MESON_TAC[LOOP_GCD; COPRIME_GCD]);;
  49
  50 (* ------------------------------------------------------------------------- *)
  51 (* General theorem about partition into equally-sized eqv classes.           *)
  52 (* ------------------------------------------------------------------------- *)
  53
  54 let EQUIVALENCE_UNIFORM_PARTITION = prove
  55  (`!R s k. FINITE s /\
  56            (!x. x IN s ==> R x x) /\
  57            (!x y. R x y ==> R y x) /\
  58            (!x y z. R x y /\ R y z ==> R x z) /\
  59            (!x:A. x IN s ==> CARD {y | y IN s /\ R x y} = k)
  60            ==> k divides (CARD s)`,
  61   REPEAT GEN_TAC THEN
  62   WF_INDUCT_TAC `CARD(s:A->bool)` THEN
  63   ASM_CASES_TAC `s:A->bool = {}` THENL
  64    [ASM_MESON_TAC[CARD_CLAUSES; DIVIDES_0]; REPEAT STRIP_TAC] THEN
  65   FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
  66   DISCH_THEN(X_CHOOSE_TAC `a:A`) THEN
  67   FIRST_X_ASSUM(MP_TAC o SPEC `{y:A | y IN s /\ ~(R (a:A) y)}`) THEN
  68   REWRITE_TAC[IMP_IMP] THEN ANTS_TAC THENL
  69    [ASM_SIMP_TAC[IN_ELIM_THM; FINITE_RESTRICT] THEN ASM_REWRITE_TAC[] THEN
  70     CONJ_TAC THENL
  71      [MATCH_MP_TAC CARD_PSUBSET THEN
  72       ASM_SIMP_TAC[PSUBSET; SUBSET; EXTENSION; IN_ELIM_THM] THEN
  73       ASM_MESON_TAC[];
  74       GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN
  75       DISCH_THEN(CONJUNCTS_THEN2 (ANTE_RES_THEN MP_TAC) ASSUME_TAC) THEN
  76       DISCH_TAC THEN MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN
  77       AP_TERM_TAC THEN ASM SET_TAC[]];
  78     ALL_TAC] THEN
  79   DISCH_TAC THEN
  80   SUBGOAL_THEN `CARD(s) = CARD {y | y IN s /\ (R:A->A->bool) a y} +
  81                           CARD {y | y IN s /\ ~(R a y)}`
  82    (fun th -> ASM_SIMP_TAC[th; DIVIDES_ADD; DIVIDES_REFL]) THEN
  83   CONV_TAC SYM_CONV THEN MATCH_MP_TAC CARD_UNION_EQ THEN ASM SET_TAC[]);;
  84
  85 (* ------------------------------------------------------------------------- *)
  86 (* With explicit restricted quantification.                                  *)
  87 (* ------------------------------------------------------------------------- *)
  88
  89 let EQUIVALENCE_UNIFORM_PARTITION_RESTRICT = prove
  90  (`!R s k. FINITE s /\
  91            (!x. x IN s ==> R x x) /\
  92            (!x y. x IN s /\ y IN s /\ R x y ==> R y x) /\
  93            (!x y z. x IN s /\ y IN s /\ z IN s /\ R x y /\ R y z ==> R x z) /\
  94            (!x:A. x IN s ==> CARD {y | y IN s /\ R x y} = k)
  95            ==> k divides (CARD s)`,
  96   REPEAT STRIP_TAC THEN MATCH_MP_TAC EQUIVALENCE_UNIFORM_PARTITION THEN
  97   EXISTS_TAC `\x y:A. x IN s /\ y IN s /\ R x y` THEN
  98   SIMP_TAC[] THEN ASM_REWRITE_TAC[CONJ_ASSOC] THEN ASM_MESON_TAC[]);;
  99
 100 (* ------------------------------------------------------------------------- *)
 101 (* General theorem about pairing up elements of a set.                       *)
 102 (* ------------------------------------------------------------------------- *)
 103
 104 let ELEMENTS_PAIR_UP = prove
 105  (`!s r. FINITE s /\
 106          (!x. x IN s ==> ~(r x x)) /\
 107          (!x y. x IN s /\ y IN s /\ r x y ==> r y x) /\
 108          (!x:A. x IN s ==> ?!y. y IN s /\ r x y)
 109          ==> EVEN(CARD s)`,
 110   REPEAT GEN_TAC THEN WF_INDUCT_TAC `CARD(s:A->bool)` THEN
 111   STRIP_TAC THEN ASM_CASES_TAC `s:A->bool = {}` THEN
 112   ASM_REWRITE_TAC[CARD_CLAUSES; ARITH] THEN
 113   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
 114   DISCH_THEN(X_CHOOSE_TAC `a:A`) THEN
 115   MP_TAC(ASSUME `!x:A. x IN s ==> (?!y:A. y IN s /\ r x y)`) THEN
 116   DISCH_THEN(MP_TAC o SPEC `a:A`) THEN REWRITE_TAC[ASSUME `a:A IN s`] THEN
 117   DISCH_THEN(MP_TAC o EXISTENCE) THEN
 118   DISCH_THEN(X_CHOOSE_THEN `b:A` STRIP_ASSUME_TAC) THEN
 119   FIRST_X_ASSUM(MP_TAC o SPEC `s DELETE (a:A) DELETE b`) THEN
 120   REWRITE_TAC[IMP_IMP] THEN ANTS_TAC THENL
 121    [ALL_TAC;
 122     DISCH_TAC THEN
 123     SUBGOAL_THEN `s = (a:A) INSERT b INSERT (s DELETE a DELETE b)`
 124     SUBST1_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
 125     ASM_SIMP_TAC[CARD_CLAUSES; FINITE_DELETE; FINITE_INSERT] THEN
 126     REWRITE_TAC[IN_INSERT; IN_DELETE] THEN ASM_MESON_TAC[EVEN]] THEN
 127   ASM_SIMP_TAC[FINITE_DELETE; IN_DELETE] THEN CONJ_TAC THENL
 128    [MATCH_MP_TAC CARD_PSUBSET THEN ASM SET_TAC[]; ALL_TAC] THEN
 129   X_GEN_TAC `x:A` THEN STRIP_TAC THEN
 130   MP_TAC(ASSUME `!x:A. x IN s ==> (?!y. y IN s /\ r x y)`) THEN
 131   DISCH_THEN(MP_TAC o SPEC `x:A`) THEN REWRITE_TAC[ASSUME `x:A IN s`] THEN
 132   MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN
 133   X_GEN_TAC `y:A` THEN EQ_TAC THEN SIMP_TAC[] THEN ASM_MESON_TAC[]);;
 134
 135 (* ------------------------------------------------------------------------- *)
 136 (* Cycles and paths.                                                         *)
 137 (* ------------------------------------------------------------------------- *)
 138
 139 let cycle = new_definition
 140  `cycle r k x <=> (!i. r (x i) (x(i + 1))) /\ (!i. x(i + k) = x(i))`;;
 141
 142 let path = new_definition
 143  `path r k x <=> (!i. i < k ==> r (x i) (x(i + 1))) /\
 144                  (!i. k < i ==> x(i) = @x. T)`;;
 145
 146 (* ------------------------------------------------------------------------- *)
 147 (* Lemmas about these concepts.                                              *)
 148 (* ------------------------------------------------------------------------- *)
 149
 150 let CYCLE_OFFSET = prove
 151  (`!r k x:num->A. cycle r k x ==> !i m. x(m * k + i) = x(i)`,
 152   REPEAT GEN_TAC THEN REWRITE_TAC[cycle] THEN STRIP_TAC THEN GEN_TAC THEN
 153   INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN
 154   ASM_MESON_TAC[ADD_AC]);;
 155
 156 let CYCLE_MOD = prove
 157  (`!r k x:num->A. cycle r k x /\ ~(k = 0) ==> !i. x(i MOD k) = x(i)`,
 158   MESON_TAC[CYCLE_OFFSET; DIVISION]);;
 159
 160 let PATHS_MONO = prove
 161  (`(!x y. r x y ==> s x y) ==> {x | path r k x} SUBSET {x | path s k x}`,
 162   REWRITE_TAC[path; IN_ELIM_THM; SUBSET] THEN MESON_TAC[]);;
 163
 164 let HAS_SIZE_PATHS = prove
 165  (`!N m r k. (:A) HAS_SIZE N /\ (!x. {y | r x y} HAS_SIZE m)
 166              ==> {x:num->A | path r k x} HAS_SIZE (N * m EXP k)`,
 167   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
 168   INDUCT_TAC THEN REWRITE_TAC[EXP; MULT_CLAUSES] THENL
 169    [SUBGOAL_THEN `{x:num->A | path r 0 x} =
 170                   IMAGE (\a i. if i = 0 then a else @x. T) (:A)`
 171     SUBST1_TAC THENL
 172      [REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_IMAGE; IN_UNIV; path; LT] THEN
 173       REWRITE_TAC[FUN_EQ_THM; LT_NZ] THEN MESON_TAC[];
 174       ALL_TAC] THEN
 175     MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN ASM_REWRITE_TAC[IN_UNIV] THEN
 176     REWRITE_TAC[FUN_EQ_THM] THEN MESON_TAC[];
 177     ALL_TAC] THEN
 178   SUBGOAL_THEN
 179    `{x:num->A | path r (SUC k) x} =
 180     IMAGE (\(x,a) i. if i = SUC k then a else x i)
 181           {x,a | x IN {x | path r k x} /\ a IN {u | r (x k) u}}`
 182   SUBST1_TAC THENL
 183    [REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_IMAGE; EXISTS_PAIR_THM] THEN
 184     X_GEN_TAC `x:num->A` THEN REWRITE_TAC[PAIR_EQ] THEN
 185     ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c /\ d <=> c /\ d /\ a /\ b`] THEN
 186     REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
 187     REWRITE_TAC[FUN_EQ_THM; path; LT] THEN EQ_TAC THENL
 188      [STRIP_TAC THEN EXISTS_TAC `\i. if i = SUC k then @x. T else x(i):A` THEN
 189       EXISTS_TAC `x(SUC k):A` THEN SIMP_TAC[] THEN
 190       CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
 191       SIMP_TAC[ARITH_RULE `~(k = SUC k) /\ (i < k ==> ~(i = SUC k))`] THEN
 192       ASM_SIMP_TAC[ADD1; ARITH_RULE `i < k ==> ~(i + 1 = SUC k)`] THEN
 193       ASM_MESON_TAC[ARITH_RULE `k < i /\ ~(i = k + 1) ==> SUC k < i`];
 194       ALL_TAC] THEN
 195     REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 196     MAP_EVERY X_GEN_TAC [`z:num->A`; `a:A`] THEN STRIP_TAC THEN
 197     ASM_REWRITE_TAC[] THEN
 198     SIMP_TAC[ARITH_RULE `i = k \/ i < k ==> ~(i = SUC k)`] THEN
 199     REWRITE_TAC[ARITH_RULE `i + 1 = SUC k <=> i = k`] THEN
 200     ASM_MESON_TAC[ARITH_RULE `SUC k < i ==> ~(i = SUC k) /\ k < i`];
 201     ALL_TAC] THEN
 202   ONCE_REWRITE_TAC[ARITH_RULE `N * m * m EXP k = (N * m EXP k) * m`] THEN
 203   MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN CONJ_TAC THENL
 204    [REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_PAIR_THM; IN_ELIM_THM] THEN
 205     REWRITE_TAC[FUN_EQ_THM; path; PAIR_EQ] THEN REPEAT GEN_TAC THEN
 206     STRIP_TAC THEN CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
 207     X_GEN_TAC `i:num` THEN ASM_CASES_TAC `i = SUC k` THEN
 208     ASM_MESON_TAC[ARITH_RULE `k < SUC k`];
 209     ALL_TAC] THEN
 210   ASM_SIMP_TAC[HAS_SIZE_PRODUCT_DEPENDENT]);;
 211
 212 let FINITE_PATHS = prove
 213  (`!r k. FINITE(:A) ==> FINITE {x:num->A | path r k x}`,
 214   REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
 215   EXISTS_TAC `{x:num->A | path (\a b. T) k x}` THEN SIMP_TAC[PATHS_MONO] THEN
 216   MP_TAC(ISPECL [`CARD(:A)`; `CARD(:A)`; `\a:A b:A. T`; `k:num`]
 217                 HAS_SIZE_PATHS) THEN
 218   ANTS_TAC THEN ASM_SIMP_TAC[HAS_SIZE; SET_RULE `{y | T} = (:A)`]);;
 219
 220 let HAS_SIZE_CYCLES = prove
 221  (`!r k. FINITE(:A) /\ ~(k = 0)
 222          ==> {x:num->A | cycle r k x} HAS_SIZE
 223              CARD{x:num->A | path r k x /\ x(k) = x(0)}`,
 224   REPEAT STRIP_TAC THEN
 225   SUBGOAL_THEN
 226    `{x:num->A | cycle r k x} =
 227     IMAGE (\x i. x(i MOD k)) {x | path r k x /\ x(k) = x(0)}`
 228   SUBST1_TAC THENL
 229    [REWRITE_TAC[EXTENSION; IN_IMAGE; IN_ELIM_THM] THEN
 230     X_GEN_TAC `x:num->A` THEN EQ_TAC THENL
 231      [DISCH_TAC THEN
 232       EXISTS_TAC `\i. if i <= k then x(i):A else @x. T` THEN
 233       REPEAT CONJ_TAC THENL
 234        [ASM_SIMP_TAC[FUN_EQ_THM; LT_IMP_LE; DIVISION] THEN
 235         ASM_MESON_TAC[CYCLE_MOD];
 236         SIMP_TAC[path; LT_IMP_LE] THEN REWRITE_TAC[GSYM NOT_LT] THEN
 237         SIMP_TAC[ARITH_RULE `i < k ==> ~(k < i + 1)`] THEN
 238         ASM_MESON_TAC[cycle];
 239         REWRITE_TAC[LE_0; LE_REFL] THEN ASM_MESON_TAC[cycle; ADD_CLAUSES]];
 240       REWRITE_TAC[LEFT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
 241       X_GEN_TAC `y:num->A` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 242       REWRITE_TAC[cycle] THEN CONJ_TAC THEN X_GEN_TAC `i:num` THENL
 243        [ALL_TAC;
 244         AP_TERM_TAC THEN MATCH_MP_TAC MOD_EQ THEN EXISTS_TAC `1` THEN
 245         REWRITE_TAC[MULT_CLAUSES]] THEN
 246       SUBGOAL_THEN `y((i + 1) MOD k):A = y(i MOD k + 1)` SUBST1_TAC THENL
 247        [ALL_TAC; ASM_MESON_TAC[path; DIVISION]] THEN
 248       SUBGOAL_THEN `(i + 1) MOD k = (i MOD k + 1) MOD k` SUBST1_TAC THENL
 249        [MATCH_MP_TAC MOD_EQ THEN EXISTS_TAC `i DIV k` THEN
 250         REWRITE_TAC[ARITH_RULE `i + 1 = (m + 1) + ik <=> i = ik + m`] THEN
 251         ASM_MESON_TAC[DIVISION];
 252         ALL_TAC] THEN
 253       FIRST_ASSUM(MP_TAC o CONJUNCT2 o SPEC `i:num` o MATCH_MP DIVISION) THEN
 254       SPEC_TAC(`i MOD k`,`j:num`) THEN GEN_TAC THEN
 255       ONCE_REWRITE_TAC[ARITH_RULE `j < k <=> j + 1 < k \/ j + 1 = k`] THEN
 256       STRIP_TAC THEN ASM_SIMP_TAC[MOD_LT] THEN AP_TERM_TAC THEN
 257       MATCH_MP_TAC MOD_UNIQ THEN EXISTS_TAC `1` THEN
 258       UNDISCH_TAC `~(k = 0)` THEN ARITH_TAC];
 259     ALL_TAC] THEN
 260   MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN CONJ_TAC THENL
 261    [ALL_TAC;
 262     REWRITE_TAC[HAS_SIZE] THEN MATCH_MP_TAC FINITE_SUBSET THEN
 263     EXISTS_TAC `{x:num->A | path r k x}` THEN
 264     ASM_SIMP_TAC[FINITE_PATHS] THEN SET_TAC[]] THEN
 265   MAP_EVERY X_GEN_TAC [`x:num->A`; `y:num->A`] THEN SIMP_TAC[IN_ELIM_THM] THEN
 266   REWRITE_TAC[path; FUN_EQ_THM] THEN STRIP_TAC THEN X_GEN_TAC `i:num` THEN
 267   REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
 268    (SPECL [`i:num`; `k:num`] LT_CASES)
 269   THENL [ASM_MESON_TAC[MOD_LT]; ASM_MESON_TAC[]; ASM_REWRITE_TAC[]] THEN
 270   ASM_MESON_TAC[MOD_0]);;
 271
 272 let FINITE_CYCLES = prove
 273  (`!r k. FINITE(:A) /\ ~(k = 0) ==> FINITE {x:num->A | cycle r k x}`,
 274   MESON_TAC[HAS_SIZE_CYCLES; HAS_SIZE]);;
 275
 276 let CARD_PATHCYCLES_STEP = prove
 277  (`!N m r k.
 278      (:A) HAS_SIZE N /\ ~(k = 0) /\ ~(m = 0) /\
 279      (!x:A. {y | r x y} HAS_SIZE m) /\
 280      (!x y. r x y ==> r y x) /\
 281      (!x y. ~(x = y) ==> ?!z. r x z /\ r z y)
 282      ==> {x | path r (k + 2) x /\ x(k + 2) = x(0)} HAS_SIZE
 283          (m * CARD {x | path r k x /\ x(k) = x(0)} +
 284           CARD {x | path r (k) x /\ ~(x(k) = x(0))})`,
 285   REPEAT STRIP_TAC THEN
 286   REWRITE_TAC[SET_RULE
 287    `{x | path r (k + 2) x /\ x(k + 2) = x(0)} =
 288     {x | path r (k + 2) x /\ x k = x 0 /\ x(k + 2) = x(0)} UNION
 289     {x | path r (k + 2) x /\ ~(x k = x 0) /\ x(k + 2) = x(0)}`] THEN
 290   MATCH_MP_TAC HAS_SIZE_UNION THEN GEN_REWRITE_TAC I [CONJ_ASSOC] THEN
 291   CONJ_TAC THENL [ALL_TAC; SET_TAC[]] THEN CONJ_TAC THENL
 292    [SUBGOAL_THEN
 293      `{x:num->A | path r (k + 2) x /\ x k = x 0 /\ x (k + 2) = x 0} =
 294       IMAGE (\(x,a) i. if i = k + 1 then a
 295                      else if i = k + 2 then x(0)
 296                      else x(i))
 297             {x,a | x IN {x | path r k x /\ x(k) = x(0)} /\
 298                    a IN {u | r (x k) u}}`
 299     SUBST1_TAC THENL
 300      [ALL_TAC;
 301       MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN CONJ_TAC THENL
 302        [REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_PAIR_THM] THEN
 303         REWRITE_TAC[IN_ELIM_THM; FUN_EQ_THM; PAIR_EQ] THEN
 304         MAP_EVERY X_GEN_TAC [`y:num->A`; `a:A`; `z:num->A`; `b:A`] THEN
 305         DISCH_THEN(fun th -> CONJ_TAC THEN MP_TAC th THENL
 306          [ALL_TAC; MESON_TAC[]]) THEN
 307         REPEAT(DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC)) THEN
 308         DISCH_THEN(fun th -> X_GEN_TAC `i:num` THEN MP_TAC th) THEN
 309         DISCH_THEN(fun th -> MP_TAC th THEN MP_TAC(SPEC `0` th)) THEN
 310         REWRITE_TAC[ARITH_RULE `~(0 = k + 1) /\ ~(0 = k + 2)`] THEN
 311         DISCH_TAC THEN ASM_CASES_TAC `k:num < i` THENL
 312          [ASM_MESON_TAC[path]; ALL_TAC] THEN
 313         DISCH_THEN(MP_TAC o SPEC `i:num`) THEN
 314         ASM_MESON_TAC[ARITH_RULE `k < k + 1 /\ k < k + 2`];
 315         ALL_TAC] THEN
 316       ONCE_REWRITE_TAC[MULT_SYM] THEN
 317       MATCH_MP_TAC HAS_SIZE_PRODUCT_DEPENDENT THEN
 318       ASM_REWRITE_TAC[] THEN REWRITE_TAC[HAS_SIZE] THEN
 319       MATCH_MP_TAC FINITE_SUBSET THEN
 320       EXISTS_TAC `{x:num->A | path r k x}` THEN CONJ_TAC THENL
 321        [ALL_TAC; SET_TAC[]] THEN
 322       ASM_MESON_TAC[HAS_SIZE; FINITE_PATHS]] THEN
 323     REWRITE_TAC[EXTENSION; IN_IMAGE] THEN
 324     REWRITE_TAC[EXISTS_PAIR_THM; IN_ELIM_PAIR_THM] THEN
 325     REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN
 326     X_GEN_TAC `x:num->A` THEN EQ_TAC THENL
 327      [STRIP_TAC THEN
 328       EXISTS_TAC `\i. if i <= k then x(i):A else @x. T` THEN
 329       EXISTS_TAC `(x:num->A) (k + 1)` THEN
 330       REWRITE_TAC[IN_ELIM_THM; LE_REFL; LE_0] THEN
 331       ASM_REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
 332        [ALL_TAC; ASM_MESON_TAC[path; ARITH_RULE `k < k + 2`]] THEN
 333       CONJ_TAC THENL
 334        [ALL_TAC;
 335         UNDISCH_TAC `path r (k + 2) (x:num->A)` THEN
 336         SIMP_TAC[path; LT_IMP_LE; ARITH_RULE `i < k ==> i + 1 <= k`] THEN
 337         SIMP_TAC[GSYM NOT_LT] THEN
 338         MESON_TAC[ARITH_RULE `i < k ==> i < k + 2`]] THEN
 339       X_GEN_TAC `i:num` THEN
 340       ASM_CASES_TAC `i = k + 1` THEN ASM_REWRITE_TAC[] THEN
 341       ASM_CASES_TAC `i = k + 2` THEN ASM_REWRITE_TAC[] THEN
 342       FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [path]) THEN
 343       COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 344       DISCH_THEN(MP_TAC o SPEC `i:num` o CONJUNCT2) THEN
 345       ASM_REWRITE_TAC[ARITH_RULE
 346        `k + 2 < i <=> ~(i <= k) /\ ~(i = k + 1) /\ ~(i = k + 2)`];
 347       ALL_TAC] THEN
 348     REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 349     MAP_EVERY X_GEN_TAC [`z:num->A`; `b:A`] THEN
 350     DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
 351     DISCH_THEN(fun th -> MP_TAC th THEN MP_TAC(SPEC `0` th)) THEN
 352     REWRITE_TAC[COND_ID; ARITH_RULE `~(0 = k + 1)`] THEN DISCH_TAC THEN
 353     REWRITE_TAC[CONJ_ASSOC] THEN DISCH_THEN(LABEL_TAC "*") THEN CONJ_TAC THENL
 354      [ALL_TAC; REMOVE_THEN "*" (MP_TAC o SPEC `k + 2`) THEN
 355       ASM_REWRITE_TAC[ARITH_RULE `~(k + 2 = k + 1)`]] THEN
 356     CONJ_TAC THENL
 357      [ALL_TAC; REMOVE_THEN "*" (MP_TAC o SPEC `k:num`) THEN
 358       ASM_REWRITE_TAC[ARITH_RULE `~(k = k + 2) /\ ~(k = k + 1)`]] THEN
 359     UNDISCH_TAC `path r k (z:num->A)` THEN ASM_REWRITE_TAC[path] THEN
 360     SIMP_TAC[ARITH_RULE
 361      `k + 2 < i ==> k < i /\ ~(i = k + 1) /\ ~(i = k + 2)`] THEN
 362     STRIP_TAC THEN X_GEN_TAC `i:num` THEN DISCH_TAC THEN
 363     ASM_SIMP_TAC[ARITH_RULE `i < k + 2 ==> ~(i = k + 2)`] THEN
 364     REWRITE_TAC[ARITH_RULE `i + 1 = k + 2 <=> i = k + 1`] THEN
 365     ASM_CASES_TAC `i = k + 1` THEN ASM_REWRITE_TAC[] THENL
 366      [ASM_MESON_TAC[ARITH_RULE `~(x + 1 = x)`]; ALL_TAC] THEN
 367     REWRITE_TAC[EQ_ADD_RCANCEL] THEN COND_CASES_TAC THEN ASM_SIMP_TAC[] THENL
 368      [ASM_MESON_TAC[]; ALL_TAC] THEN
 369     ASM_MESON_TAC[ARITH_RULE `i < k + 2 /\ ~(i = k) /\ ~(i = k + 1)
 370                               ==> i < k`];
 371     ALL_TAC] THEN
 372   SUBGOAL_THEN
 373    `{x:num->A | path r (k + 2) x /\ ~(x k = x 0) /\ x (k + 2) = x 0} =
 374     IMAGE (\x i. if i = k + 1 then @z. r (x k) z /\ r z (x 0)
 375                else if i = k + 2 then x(0)
 376                else x(i))
 377         {x | path r k x /\ ~(x(k) = x(0))}`
 378   SUBST1_TAC THENL
 379    [ALL_TAC;
 380     MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN CONJ_TAC THENL
 381      [ALL_TAC;
 382       REWRITE_TAC[HAS_SIZE] THEN
 383       MATCH_MP_TAC FINITE_SUBSET THEN
 384       EXISTS_TAC `{x:num->A | path r k x}` THEN CONJ_TAC THENL
 385        [ALL_TAC; SET_TAC[]] THEN
 386       ASM_MESON_TAC[HAS_SIZE; FINITE_PATHS]] THEN
 387     MAP_EVERY X_GEN_TAC [`x:num->A`; `y:num->A`] THEN
 388     REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
 389     REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `i:num` THEN
 390     ASM_CASES_TAC `k:num < i` THENL
 391      [ASM_MESON_TAC[path]; ALL_TAC] THEN
 392     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [FUN_EQ_THM]) THEN
 393     DISCH_THEN(MP_TAC o SPEC `i:num`) THEN
 394     ASM_MESON_TAC[ARITH_RULE `k < k + 1 /\ k < k + 2`]] THEN
 395   REWRITE_TAC[EXTENSION; IN_IMAGE; IN_ELIM_THM] THEN
 396   X_GEN_TAC `x:num->A` THEN REWRITE_TAC[IN_ELIM_THM] THEN EQ_TAC THENL
 397    [STRIP_TAC THEN
 398     EXISTS_TAC `\i. if i <= k then x(i):A else @x. T` THEN
 399     ASM_REWRITE_TAC[LE_REFL; LE_0] THEN CONJ_TAC THENL
 400      [ALL_TAC;
 401       UNDISCH_TAC `path r (k + 2) (x:num->A)` THEN
 402       SIMP_TAC[path; LT_IMP_LE; ARITH_RULE `i < k ==> i + 1 <= k`] THEN
 403       SIMP_TAC[GSYM NOT_LT] THEN
 404       MESON_TAC[ARITH_RULE `i < k ==> i < k + 2`]] THEN
 405     REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `i:num` THEN
 406     ASM_CASES_TAC `i = k + 1` THEN ASM_REWRITE_TAC[] THENL
 407      [CONV_TAC SYM_CONV THEN MATCH_MP_TAC SELECT_UNIQUE THEN
 408       UNDISCH_TAC `path r (k + 2) (x:num->A)` THEN REWRITE_TAC[path] THEN
 409       DISCH_THEN(MP_TAC o CONJUNCT1) THEN
 410       DISCH_THEN(fun th -> MP_TAC(SPEC `k:num` th) THEN
 411                            MP_TAC(SPEC `k + 1` th)) THEN
 412       REWRITE_TAC[ARITH_RULE `k < k + 2 /\ k + 1 < k + 2`] THEN
 413       REWRITE_TAC[GSYM ADD_ASSOC; ARITH] THEN ASM_MESON_TAC[];
 414       ALL_TAC] THEN
 415     ASM_CASES_TAC `i = k + 2` THEN ASM_REWRITE_TAC[] THEN
 416     COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 417     UNDISCH_TAC `path r (k + 2) (x:num->A)` THEN REWRITE_TAC[path] THEN
 418     DISCH_THEN(MP_TAC o CONJUNCT2) THEN
 419     ASM_MESON_TAC[ARITH_RULE `~(i <= k) /\ ~(i = k + 1) /\ ~(i = k + 2)
 420                               ==> k + 2 < i`];
 421     ALL_TAC] THEN
 422   DISCH_THEN(X_CHOOSE_THEN `y:num->A` STRIP_ASSUME_TAC) THEN
 423   ASM_REWRITE_TAC[ARITH_RULE
 424    `~(k + 2 = k + 1) /\ ~(0 = k + 1) /\ ~(0 = k + 2) /\ ~(k = k + 1) /\
 425     ~(k = k + 2)`] THEN
 426   REWRITE_TAC[path] THEN CONJ_TAC THEN X_GEN_TAC `i:num` THEN DISCH_TAC THENL
 427    [REWRITE_TAC[ARITH_RULE `i + 1 = k + 2 <=> i = k + 1`] THEN
 428     ASM_CASES_TAC `i = k + 1` THEN ASM_REWRITE_TAC[] THENL
 429      [REWRITE_TAC[ARITH_RULE `(k + 1) + 1 = k + 1 <=> F`] THEN ASM_MESON_TAC[];
 430       ALL_TAC] THEN
 431     ASM_SIMP_TAC[ARITH_RULE `i < k + 2 ==> ~(i = k + 2)`] THEN
 432     REWRITE_TAC[EQ_ADD_RCANCEL] THEN COND_CASES_TAC THEN ASM_SIMP_TAC[] THENL
 433      [ASM_MESON_TAC[]; ALL_TAC] THEN
 434     UNDISCH_TAC `path r k (y:num->A)` THEN REWRITE_TAC[path] THEN
 435     DISCH_THEN(MATCH_MP_TAC o CONJUNCT1) THEN
 436     MAP_EVERY UNDISCH_TAC [`~(i:num = k)`; `~(i = k + 1)`; `i < k + 2`] THEN
 437     ARITH_TAC;
 438     ALL_TAC] THEN
 439   ASM_SIMP_TAC[ARITH_RULE `k + 2 < i ==> ~(i = k + 1) /\ ~(i = k + 2)`] THEN
 440   ASM_MESON_TAC[path; ARITH_RULE `k + 2 < i ==> k < i`]);;
 441
 442 (* ------------------------------------------------------------------------- *)
 443 (* The first lemma about the number of cycles.                               *)
 444 (* ------------------------------------------------------------------------- *)
 445
 446 let shiftable = new_definition
 447  `shiftable x y <=> ?k. !i. x(i) = y(i + k)`;;
 448
 449 let SHIFTABLE_REFL = prove
 450  (`!x. shiftable x x`,
 451   REWRITE_TAC[shiftable] THEN MESON_TAC[ADD_CLAUSES]);;
 452
 453 let SHIFTABLE_TRANS = prove
 454  (`!x y z. shiftable x y /\ shiftable y z ==> shiftable x z`,
 455   REWRITE_TAC[shiftable] THEN MESON_TAC[ADD_ASSOC]);;
 456
 457 let SHIFTABLE_LOCAL = prove
 458  (`!x y p r. cycle r p x /\ cycle r p y /\ ~(p = 0)
 459              ==> (shiftable x y <=> ?k. k < p /\ !i. x(i) = y(i + k))`,
 460   REPEAT STRIP_TAC THEN REWRITE_TAC[shiftable] THEN
 461   EQ_TAC THENL [ALL_TAC; MESON_TAC[]] THEN
 462   DISCH_THEN(X_CHOOSE_TAC `k:num`) THEN EXISTS_TAC `k MOD p` THEN
 463   FIRST_ASSUM(MP_TAC o SPEC `k:num` o MATCH_MP DIVISION) THEN
 464   DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN ASM_REWRITE_TAC[] THEN
 465   DISCH_THEN(fun th -> GEN_REWRITE_TAC
 466    (BINDER_CONV o LAND_CONV o ONCE_DEPTH_CONV) [th]) THEN
 467   ASM_MESON_TAC[CYCLE_OFFSET; ADD_AC]);;
 468
 469 let SHIFTABLE_SYM = prove
 470  (`!x y p r. cycle r p x /\ cycle r p y /\ ~(p = 0) /\ shiftable x y
 471              ==> shiftable y x`,
 472   REPEAT GEN_TAC THEN
 473   ONCE_REWRITE_TAC[TAUT `a /\ b /\ c /\ d <=> (a /\ b /\ c) /\ d`] THEN
 474   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 475   FIRST_ASSUM(SUBST1_TAC o MATCH_MP SHIFTABLE_LOCAL) THEN
 476   DISCH_THEN(X_CHOOSE_THEN `k:num` STRIP_ASSUME_TAC) THEN
 477   REWRITE_TAC[shiftable] THEN EXISTS_TAC `p - k:num` THEN
 478   ASM_SIMP_TAC[ARITH_RULE `k < p ==> (i + (p - k)) + k = i + p:num`] THEN
 479   ASM_MESON_TAC[cycle]);;
 480
 481 let CYCLES_PRIME_LEMMA = prove
 482  (`!r p x. FINITE(:A) /\ prime p /\ (!x. ~(r x x))
 483            ==> p divides CARD {x:num->A | cycle r p x}`,
 484   REPEAT GEN_TAC THEN ASM_CASES_TAC `p = 0` THEN ASM_REWRITE_TAC[PRIME_0] THEN
 485   STRIP_TAC THEN MATCH_MP_TAC EQUIVALENCE_UNIFORM_PARTITION_RESTRICT THEN
 486   EXISTS_TAC `shiftable:(num->A)->(num->A)->bool` THEN
 487   ASM_SIMP_TAC[IN_ELIM_THM; FINITE_CYCLES] THEN
 488   CONJ_TAC THENL [MESON_TAC[SHIFTABLE_REFL]; ALL_TAC] THEN
 489   CONJ_TAC THENL [ASM_MESON_TAC[SHIFTABLE_SYM]; ALL_TAC] THEN
 490   CONJ_TAC THENL [MESON_TAC[SHIFTABLE_TRANS]; ALL_TAC] THEN
 491   X_GEN_TAC `x:num->A` THEN DISCH_TAC THEN
 492   SUBGOAL_THEN `{y:num->A | cycle r p y /\ shiftable x y} HAS_SIZE p`
 493    (fun th -> MESON_TAC[HAS_SIZE; th]) THEN
 494   SUBGOAL_THEN `{y:num->A | cycle r p y /\ shiftable x y} =
 495                 IMAGE (\k i. x(i + k)) {k | k < p}`
 496   SUBST1_TAC THENL
 497    [REWRITE_TAC[EXTENSION; IN_IMAGE; IN_ELIM_THM] THEN
 498     X_GEN_TAC `y:num->A` THEN REWRITE_TAC[FUN_EQ_THM] THEN EQ_TAC THENL
 499      [ASM_MESON_TAC[SHIFTABLE_LOCAL; SHIFTABLE_SYM]; ALL_TAC] THEN
 500     REPEAT STRIP_TAC THENL
 501      [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [cycle]) THEN
 502       ASM_REWRITE_TAC[cycle] THEN MESON_TAC[ADD_AC];
 503       ALL_TAC] THEN
 504     MATCH_MP_TAC SHIFTABLE_SYM THEN
 505     MAP_EVERY EXISTS_TAC [`p:num`; `r:A->A->bool`] THEN
 506     ASM_REWRITE_TAC[] THEN
 507     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [cycle]) THEN
 508     ASM_REWRITE_TAC[cycle; shiftable] THEN MESON_TAC[ADD_AC];
 509     ALL_TAC] THEN
 510   MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN REWRITE_TAC[HAS_SIZE_NUMSEG_LT] THEN
 511   REWRITE_TAC[IN_ELIM_THM] THEN MATCH_MP_TAC WLOG_LE THEN
 512   REWRITE_TAC[FUN_EQ_THM] THEN CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
 513   MAP_EVERY X_GEN_TAC [`k:num`; `l:num`] THEN REPEAT STRIP_TAC THEN
 514   MATCH_MP_TAC(TAUT `(~p ==> F) ==> p`) THEN DISCH_TAC THEN
 515   SUBGOAL_THEN `!i. x(i):A = x(0)` MP_TAC THENL
 516    [ALL_TAC; ASM_MESON_TAC[cycle]] THEN
 517   MATCH_MP_TAC LOOP_COPRIME THEN EXISTS_TAC `p:num` THEN
 518   REWRITE_TAC[RIGHT_EXISTS_AND_THM] THEN
 519   CONJ_TAC THENL [ASM_MESON_TAC[cycle]; ALL_TAC] THEN
 520   EXISTS_TAC `l + (p - k):num` THEN CONJ_TAC THENL
 521    [X_GEN_TAC `i:num` THEN
 522     ONCE_REWRITE_TAC[ARITH_RULE `i + l + pk = (i + pk) + l:num`] THEN
 523     ASSUM_LIST(REWRITE_TAC o map GSYM) THEN
 524     SIMP_TAC[ARITH_RULE `k < p ==> (i + p - k) + k = i + p:num`;
 525              ASSUME `k < p:num`] THEN
 526     ASM_MESON_TAC[cycle];
 527     ALL_TAC] THEN
 528   SUBGOAL_THEN `l + p - k = p + l - k:num` SUBST1_TAC THENL
 529    [MAP_EVERY UNDISCH_TAC [`k < p:num`; `k <= l:num`] THEN ARITH_TAC;
 530     ALL_TAC] THEN
 531   REWRITE_TAC[NUMBER_RULE `coprime(p,p + d) <=> coprime(d,p)`] THEN
 532   MATCH_MP_TAC PRIME_COPRIME_LT THEN
 533   ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC);;
 534
 535 (* ------------------------------------------------------------------------- *)
 536 (* The theorem itself.                                                       *)
 537 (* ------------------------------------------------------------------------- *)
 538
 539 let FRIENDSHIP = prove
 540  (`!friend:person->person->bool.
 541       FINITE(:person) /\
 542       (!x. ~(friend x x)) /\
 543       (!x y. friend x y ==> friend y x) /\
 544       (!x y. ~(x = y) ==> ?!z. friend x z /\ friend y z)
 545       ==> ?u. !v. ~(v = u) ==> friend u v`,
 546   REPEAT STRIP_TAC THEN UNDISCH_TAC
 547    `!x y:person. ~(x = y) ==> ?!z:person. friend x z /\ friend y z` THEN
 548   REWRITE_TAC[EXISTS_UNIQUE_THM] THEN
 549   REWRITE_TAC[TAUT `a ==> b /\ c <=> (a ==> b) /\ (a ==> c)`] THEN
 550   REWRITE_TAC[FORALL_AND_THM; RIGHT_IMP_FORALL_THM] THEN
 551   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [RIGHT_IMP_EXISTS_THM] THEN
 552   REWRITE_TAC[SKOLEM_THM; IMP_IMP; GSYM CONJ_ASSOC] THEN
 553   DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
 554   DISCH_THEN(X_CHOOSE_TAC `mutualfriend:person->person->person`) THEN
 555   SUBGOAL_THEN `!s:person->bool. FINITE s` ASSUME_TAC THENL
 556    [ASM_MESON_TAC[SUBSET_UNIV; FINITE_SUBSET]; ALL_TAC] THEN
 557   ABBREV_TAC `degree = \p:person. CARD {q:person | friend p q}` THEN
 558   SUBGOAL_THEN `!x y:person. ~(friend x y) ==> degree(x):num <= degree(y)`
 559   ASSUME_TAC THENL
 560    [REPEAT STRIP_TAC THEN ASM_CASES_TAC `x:person = y` THENL
 561      [ASM_MESON_TAC[LE_REFL]; ALL_TAC] THEN
 562     EXPAND_TAC "degree" THEN MATCH_MP_TAC LE_TRANS THEN
 563     EXISTS_TAC `CARD(IMAGE (\u. (mutualfriend:person->person->person) u y)
 564                            {q | friend (x:person) q})` THEN
 565     CONJ_TAC THENL
 566      [ALL_TAC; MATCH_MP_TAC CARD_SUBSET THEN ASM SET_TAC[]] THEN
 567     MATCH_MP_TAC EQ_IMP_LE THEN CONV_TAC SYM_CONV THEN
 568     MATCH_MP_TAC CARD_IMAGE_INJ THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN
 569     MAP_EVERY X_GEN_TAC [`u1:person`; `u2:person`] THEN STRIP_TAC THEN
 570     FIRST_X_ASSUM(MP_TAC o SPECL
 571      [`x:person`; `(mutualfriend:person->person->person) u1 y`;
 572       `u1:person`; `u2:person`]) THEN ASM_MESON_TAC[];
 573     ALL_TAC] THEN
 574   SUBGOAL_THEN `!x y:person. ~(friend x y) ==> degree x:num = degree y`
 575   ASSUME_TAC THENL [ASM_MESON_TAC[LE_ANTISYM]; ALL_TAC] THEN
 576   GEN_REWRITE_TAC I [TAUT `p <=> ~ ~ p`] THEN
 577   GEN_REWRITE_TAC RAND_CONV [NOT_EXISTS_THM] THEN
 578   DISCH_THEN(ASSUME_TAC o REWRITE_RULE[NOT_FORALL_THM; NOT_IMP]) THEN
 579   SUBGOAL_THEN `?m:num. !x:person. degree(x) = m` STRIP_ASSUME_TAC THENL
 580    [FIRST_ASSUM(X_CHOOSE_THEN `b:person` STRIP_ASSUME_TAC o
 581       SPEC `a:person`) THEN
 582     ABBREV_TAC `c = (mutualfriend:person->person->person) a b` THEN
 583     ABBREV_TAC `k = (degree:person->num) a` THEN EXISTS_TAC `k:num` THEN
 584     SUBGOAL_THEN `(degree:person->num)(b) = k /\ ~(friend a b) /\
 585                   friend a c /\ friend b c`
 586     STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 587     SUBGOAL_THEN `!x:person. ~(x = c) ==> degree x = (k:num)` ASSUME_TAC THEN
 588     ASM_MESON_TAC[];
 589     ALL_TAC] THEN
 590   SUBGOAL_THEN `!p:person. {q:person | friend p q} HAS_SIZE m`
 591   ASSUME_TAC THENL [ASM_MESON_TAC[HAS_SIZE]; ALL_TAC] THEN
 592   SUBGOAL_THEN `~(m = 0)` ASSUME_TAC THENL
 593    [DISCH_TAC THEN
 594     UNDISCH_TAC `!p:person. {q:person | friend p q} HAS_SIZE m` THEN
 595     ASM_REWRITE_TAC[HAS_SIZE_0; EXTENSION; IN_ELIM_THM; NOT_IN_EMPTY] THEN
 596     ASM_MESON_TAC[];
 597     ALL_TAC] THEN
 598   SUBGOAL_THEN `EVEN(m)` ASSUME_TAC THENL
 599    [UNDISCH_TAC `!x:person. degree x = (m:num)` THEN
 600     DISCH_THEN(SUBST1_TAC o SYM o SPEC `a:person`) THEN
 601     EXPAND_TAC "degree" THEN MATCH_MP_TAC ELEMENTS_PAIR_UP THEN
 602     EXISTS_TAC `\x y:person. friend a x /\ friend a y /\ friend x y` THEN
 603     REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[HAS_SIZE];
 604     ALL_TAC] THEN
 605   ABBREV_TAC `N = CARD(:person)` THEN
 606   SUBGOAL_THEN `N = m * (m - 1) + 1` ASSUME_TAC THENL
 607    [ABBREV_TAC `t = {q:person | friend (a:person) q}` THEN
 608     SUBGOAL_THEN `FINITE(t:person->bool) /\ CARD t = m` STRIP_ASSUME_TAC THENL
 609      [ASM_MESON_TAC[HAS_SIZE]; ALL_TAC] THEN
 610     ABBREV_TAC
 611      `u = \b:person. {c:person | friend b c /\ ~(c IN (a INSERT t))}` THEN
 612     EXPAND_TAC "N" THEN
 613     SUBGOAL_THEN `(:person) = (a INSERT t) UNION UNIONS {u(b) | b IN t}`
 614     SUBST1_TAC THENL
 615      [REWRITE_TAC[EXTENSION; IN_INSERT; IN_UNIV; IN_UNION; IN_UNIONS] THEN
 616       MAP_EVERY EXPAND_TAC ["t"; "u"] THEN REWRITE_TAC[IN_ELIM_THM] THEN
 617       X_GEN_TAC `x:person` THEN
 618       MATCH_MP_TAC(TAUT `(~a /\ ~b ==> c) ==> (a \/ b) \/ c`) THEN
 619       STRIP_TAC THEN REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
 620       ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c <=> b /\ a /\ c`] THEN
 621       ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN REWRITE_TAC[UNWIND_THM2] THEN
 622       REWRITE_TAC[IN_ELIM_THM; IN_INSERT; DE_MORGAN_THM] THEN
 623       EXISTS_TAC `mutualfriend (a:person) (x:person) :person` THEN
 624       EXPAND_TAC "t" THEN REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[];
 625       ALL_TAC] THEN
 626     SUBGOAL_THEN `m * (m - 1) + 1 = (m + 1) + m * (m - 2)` SUBST1_TAC THENL
 627      [SIMP_TAC[ARITH_RULE `a + 1 = (m + 1) + m * c <=> a = m * (1 + c)`] THEN
 628       AP_TERM_TAC THEN UNDISCH_TAC `EVEN m` THEN
 629       ASM_CASES_TAC `m = 1` THEN ASM_REWRITE_TAC[ARITH] THEN DISCH_TAC THEN
 630       MAP_EVERY UNDISCH_TAC [`~(m = 0)`; `~(m = 1)`] THEN ARITH_TAC;
 631       ALL_TAC] THEN
 632     SUBGOAL_THEN `m + 1 = CARD((a:person) INSERT t)` SUBST1_TAC THENL
 633      [ASM_SIMP_TAC[CARD_CLAUSES; ADD1] THEN EXPAND_TAC "t" THEN
 634       REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[];
 635       ALL_TAC] THEN
 636     SUBGOAL_THEN
 637      `UNIONS {u b :person->bool | (b:person) IN t} HAS_SIZE m * (m - 2)`
 638     MP_TAC THENL
 639      [MATCH_MP_TAC HAS_SIZE_UNIONS THEN CONJ_TAC THENL
 640        [ASM_MESON_TAC[HAS_SIZE]; ALL_TAC] THEN
 641       CONJ_TAC THENL
 642        [ALL_TAC;
 643         EXPAND_TAC "u" THEN REWRITE_TAC[DISJOINT; EXTENSION; IN_INTER] THEN
 644         REWRITE_TAC[NOT_IN_EMPTY; IN_ELIM_THM; IN_INSERT] THEN
 645         EXPAND_TAC "t" THEN REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[]] THEN
 646       REPEAT STRIP_TAC THEN
 647       MP_TAC(ASSUME `(b:person) IN t`) THEN EXPAND_TAC "t" THEN
 648       REWRITE_TAC[IN_ELIM_THM] THEN DISCH_TAC THEN
 649       SUBGOAL_THEN
 650        `u (b:person) =
 651         {q:person | friend q b} DELETE a DELETE (mutualfriend a b)`
 652       SUBST1_TAC THENL
 653        [MAP_EVERY EXPAND_TAC ["u"; "t"] THEN
 654         REWRITE_TAC[EXTENSION; IN_INSERT; IN_DELETE; IN_ELIM_THM] THEN
 655         X_GEN_TAC `x:person` THEN
 656         FIRST_X_ASSUM(MP_TAC o SPECL [`a:person`; `b:person`;
 657          `(mutualfriend:person->person->person) a b`; `x:person`]) THEN
 658         ASM_MESON_TAC[];
 659         ALL_TAC] THEN
 660       ASM_SIMP_TAC[CARD_DELETE; HAS_SIZE] THEN
 661       REWRITE_TAC[IN_ELIM_THM; IN_DELETE] THEN
 662       COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
 663       SUBGOAL_THEN `{q:person | friend q (b:person)} = {q | friend b q}`
 664       SUBST1_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
 665       ASM_REWRITE_TAC[ARITH_RULE `m - 1 - 1 = m - 2`] THEN
 666       ASM_MESON_TAC[HAS_SIZE];
 667       ALL_TAC] THEN
 668     REWRITE_TAC[HAS_SIZE] THEN DISCH_THEN(SUBST1_TAC o SYM o CONJUNCT2) THEN
 669     MATCH_MP_TAC CARD_UNION THEN ASM_REWRITE_TAC[] THEN
 670     REWRITE_TAC[EXTENSION; IN_INSERT; IN_INTER; NOT_IN_EMPTY; IN_UNIONS] THEN
 671     REWRITE_TAC[IN_ELIM_THM; LEFT_AND_EXISTS_THM] THEN
 672     ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c <=> b /\ a /\ c`] THEN
 673     ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN REWRITE_TAC[UNWIND_THM2] THEN
 674     MAP_EVERY EXPAND_TAC ["u"; "t"] THEN
 675     REWRITE_TAC[IN_ELIM_THM; IN_INSERT] THEN ASM_MESON_TAC[];
 676     ALL_TAC] THEN
 677   SUBGOAL_THEN `~(m = 2)` ASSUME_TAC THENL
 678    [DISCH_THEN SUBST_ALL_TAC THEN
 679     RULE_ASSUM_TAC(CONV_RULE NUM_REDUCE_CONV) THEN
 680     SUBGOAL_THEN `(:person) HAS_SIZE 3` MP_TAC THENL
 681      [ASM_REWRITE_TAC[HAS_SIZE]; ALL_TAC] THEN
 682     CONV_TAC(LAND_CONV HAS_SIZE_CONV) THEN REWRITE_TAC[NOT_EXISTS_THM] THEN
 683     MAP_EVERY X_GEN_TAC [`a:person`; `b:person`; `c:person`] THEN
 684     REWRITE_TAC[EXTENSION; IN_UNIV; IN_INSERT; NOT_IN_EMPTY] THEN
 685     STRIP_TAC THEN
 686     UNDISCH_TAC `!u:person. ?v:person. ~(v = u) /\ ~friend u v` THEN
 687     REWRITE_TAC[NOT_FORALL_THM; NOT_EXISTS_THM] THEN
 688     EXISTS_TAC `a:person` THEN
 689     UNDISCH_TAC `!p:person. {q:person | friend p q} HAS_SIZE 2` THEN
 690     DISCH_THEN(MP_TAC o SPEC `a:person`) THEN ASM_REWRITE_TAC[] THEN
 691     CONV_TAC(LAND_CONV HAS_SIZE_CONV) THEN
 692     REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_INSERT; NOT_IN_EMPTY] THEN
 693     REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 694     MAP_EVERY X_GEN_TAC [`x:person`; `y:person`] THEN
 695     STRIP_TAC THEN X_GEN_TAC `z:person` THEN
 696     UNDISCH_TAC `!x:person. x = a \/ x = b \/ x = c` THEN
 697     DISCH_THEN(fun th -> MAP_EVERY (fun x -> MP_TAC(SPEC x th))
 698      [`x:person`; `y:person`; `z:person`]) THEN
 699     ASM_MESON_TAC[];
 700     ALL_TAC] THEN
 701   MP_TAC(SPEC `m - 1` PRIME_FACTOR) THEN ANTS_TAC THENL
 702    [UNDISCH_TAC `~(m = 2)` THEN ARITH_TAC; ALL_TAC] THEN
 703   DISCH_THEN(X_CHOOSE_THEN `p:num` STRIP_ASSUME_TAC) THEN
 704   SUBGOAL_THEN `~(p divides 1)` MP_TAC THENL
 705    [ASM_MESON_TAC[DIVIDES_ONE; PRIME_1]; ALL_TAC] THEN
 706   REWRITE_TAC[] THEN
 707   MATCH_MP_TAC(NUMBER_RULE
 708    `!x. p divides (x + 1) /\ p divides x ==> p divides 1`) THEN
 709   EXISTS_TAC `m - 1` THEN ASM_REWRITE_TAC[] THEN
 710   ASM_SIMP_TAC[ARITH_RULE `~(m = 0) ==> m - 1 + 1 = m`] THEN
 711   MATCH_MP_TAC PRIME_DIVEXP THEN EXISTS_TAC `p - 2` THEN
 712   ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(NUMBER_RULE
 713    `!q c K1 K2.
 714         p divides q /\ p divides c /\
 715         c = (q + 1) * K1 + K2 /\
 716         K1 + K2 = ((q + 1) * q + 1) * nep2
 717         ==> p divides nep2`) THEN
 718   MAP_EVERY EXISTS_TAC
 719    [`m - 1`; `CARD {x:num->person | cycle friend p x}`;
 720     `CARD {x:num->person | path friend (p-2) x /\ x (p-2) = x 0}`;
 721     `CARD {x:num->person | path friend (p-2) x /\ ~(x (p-2) = x 0)}`] THEN
 722   ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
 723    [MATCH_MP_TAC CYCLES_PRIME_LEMMA THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
 724   SUBGOAL_THEN `3 <= p` ASSUME_TAC THENL
 725    [MATCH_MP_TAC(ARITH_RULE `2 <= p /\ ~(p = 2) ==> 3 <= p`) THEN
 726     ASM_SIMP_TAC[PRIME_GE_2] THEN DISCH_THEN SUBST_ALL_TAC THEN
 727     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM DIVIDES_2]) THEN
 728     MP_TAC(DIVIDES_CONV `2 divides 1`) THEN REWRITE_TAC[CONTRAPOS_THM] THEN
 729     MATCH_MP_TAC(NUMBER_RULE
 730      `!q. t divides q /\ m = q + 1 ==> t divides m ==> t divides w`) THEN
 731     EXISTS_TAC `m - 1` THEN ASM_REWRITE_TAC[] THEN
 732     UNDISCH_TAC `~(m = 0)` THEN ARITH_TAC;
 733     ALL_TAC] THEN
 734   ASM_SIMP_TAC[ARITH_RULE `~(m = 0) ==> m - 1 + 1 = m`] THEN CONJ_TAC THENL
 735    [MP_TAC(ISPECL[`friend:person->person->bool`; `p:num`] HAS_SIZE_CYCLES) THEN
 736     ANTS_TAC THENL [ASM_MESON_TAC[PRIME_0]; ALL_TAC] THEN
 737     SIMP_TAC[HAS_SIZE] THEN DISCH_THEN(K ALL_TAC) THEN
 738     MATCH_MP_TAC HAS_SIZE_CARD THEN
 739     SUBGOAL_THEN `p = (p - 2) + 2` (fun th ->
 740       GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th])
 741     THENL [ASM_MESON_TAC[PRIME_GE_2; SUB_ADD]; ALL_TAC] THEN
 742     MATCH_MP_TAC CARD_PATHCYCLES_STEP THEN EXISTS_TAC `N:num` THEN
 743     ASM_REWRITE_TAC[] THEN
 744     CONJ_TAC THENL [ASM_MESON_TAC[HAS_SIZE]; ALL_TAC] THEN
 745     CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
 746     UNDISCH_TAC `3 <= p` THEN ARITH_TAC;
 747     ALL_TAC] THEN
 748   MP_TAC(ISPECL [`N:num`; `m:num`; `friend:person->person->bool`; `p - 2`]
 749                HAS_SIZE_PATHS) THEN
 750   ANTS_TAC THENL [ASM_MESON_TAC[HAS_SIZE]; ALL_TAC] THEN
 751   ASM_REWRITE_TAC[HAS_SIZE] THEN
 752   DISCH_THEN(SUBST1_TAC o SYM o CONJUNCT2) THEN
 753   MATCH_MP_TAC CARD_UNION_EQ THEN ASM_SIMP_TAC[FINITE_PATHS] THEN SET_TAC[]);;