100/lagrange.ml

   1 (* ========================================================================= *)
   2 (* Very trivial group theory, just to reach Lagrange theorem.                *)
   3 (* ========================================================================= *)
   4
   5 loadt "Library/prime.ml";;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* Definition of what a group is.                                            *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 let group = new_definition
  12   `group(g,( ** ),i,(e:A)) <=>
  13     (e IN g) /\ (!x. x IN g ==> i(x) IN g) /\
  14     (!x y. x IN g /\ y IN g ==> (x ** y) IN g) /\
  15     (!x y z. x IN g /\ y IN g /\ z IN g ==> (x ** (y ** z) = (x ** y) ** z)) /\
  16     (!x. x IN g ==> (x ** e = x) /\ (e ** x = x)) /\
  17     (!x. x IN g ==> (x ** i(x) = e) /\ (i(x) ** x = e))`;;
  18
  19 (* ------------------------------------------------------------------------- *)
  20 (* Notion of a subgroup.                                                     *)
  21 (* ------------------------------------------------------------------------- *)
  22
  23 let subgroup = new_definition
  24   `subgroup h (g,( ** ),i,(e:A)) <=> h SUBSET g /\ group(h,( ** ),i,e)`;;
  25
  26 (* ------------------------------------------------------------------------- *)
  27 (* Lagrange theorem, introducing the coset representatives.                  *)
  28 (* ------------------------------------------------------------------------- *)
  29
  30 let GROUP_LAGRANGE_COSETS = prove
  31  (`!g h ( ** ) i e.
  32         group (g,( ** ),i,e:A) /\ subgroup h (g,( ** ),i,e) /\ FINITE g
  33         ==> ?q. (CARD(g) = CARD(q) * CARD(h)) /\
  34                 (!b. b IN g ==> ?a x. a IN q /\ x IN h /\ (b = a ** x))`,
  35   REPEAT GEN_TAC THEN REWRITE_TAC[group; subgroup; SUBSET] THEN STRIP_TAC THEN
  36   ABBREV_TAC
  37    `coset = \a:A. {b:A | b IN g /\ (?x:A. x IN h /\ (b = a ** x))}` THEN
  38   SUBGOAL_THEN `!a:A. a IN g ==> a IN (coset a)` ASSUME_TAC THENL
  39    [GEN_TAC THEN DISCH_TAC THEN EXPAND_TAC "coset" THEN
  40     ASM_SIMP_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[];
  41     ALL_TAC] THEN
  42   SUBGOAL_THEN `FINITE(h:A->bool)` ASSUME_TAC THENL
  43    [ASM_MESON_TAC[FINITE_SUBSET; SUBSET]; ALL_TAC] THEN
  44   SUBGOAL_THEN `!a. FINITE((coset:A->A->bool) a)` ASSUME_TAC THENL
  45    [GEN_TAC THEN EXPAND_TAC "coset" THEN
  46     MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `g:A->bool` THEN
  47     ASM_SIMP_TAC[IN_ELIM_THM; SUBSET];
  48     ALL_TAC] THEN
  49   SUBGOAL_THEN
  50    `!a:A x:A y. a IN g /\ x IN g /\ y IN g /\ ((a ** x) :A = a ** y)
  51                 ==> (x = y)`
  52   ASSUME_TAC THENL
  53    [REPEAT STRIP_TAC THEN
  54     SUBGOAL_THEN `(e:A ** x:A):A = e ** y` (fun th -> ASM_MESON_TAC[th]) THEN
  55     SUBGOAL_THEN
  56      `((i(a):A ** a:A) ** x) = (i(a) ** a) ** y`
  57      (fun th -> ASM_MESON_TAC[th]) THEN
  58     ASM_MESON_TAC[];
  59     ALL_TAC] THEN
  60   SUBGOAL_THEN `!a:A. a IN g ==> (CARD(coset a :A->bool) = CARD(h:A->bool))`
  61   ASSUME_TAC THENL
  62    [REPEAT STRIP_TAC THEN
  63     SUBGOAL_THEN
  64      `(coset:A->A->bool) (a:A) = IMAGE (\x. a ** x) (h:A->bool)`
  65     SUBST1_TAC THENL
  66      [EXPAND_TAC "coset" THEN
  67       REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_IMAGE; IN_ELIM_THM] THEN
  68       ASM_MESON_TAC[];
  69       ALL_TAC] THEN
  70     MATCH_MP_TAC CARD_IMAGE_INJ THEN ASM_REWRITE_TAC[] THEN
  71     ASM_MESON_TAC[];
  72     ALL_TAC] THEN
  73   SUBGOAL_THEN `!x:A y. x IN g /\ y IN g ==> (i(x ** y) = i(y) ** i(x))`
  74   ASSUME_TAC THENL
  75    [REPEAT STRIP_TAC THEN
  76     FIRST_ASSUM MATCH_MP_TAC THEN
  77     EXISTS_TAC `(x:A ** y:A) :A` THEN ASM_SIMP_TAC[] THEN
  78     MATCH_MP_TAC EQ_TRANS THEN
  79     EXISTS_TAC `(x:A ** (y ** i(y))) ** i(x)` THEN
  80     ASM_MESON_TAC[];
  81     ALL_TAC] THEN
  82   SUBGOAL_THEN `!x:A. x IN g ==> (i(i(x)) = x)` ASSUME_TAC THENL
  83    [REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
  84     EXISTS_TAC `(i:A->A)(x)` THEN ASM_MESON_TAC[];
  85     ALL_TAC] THEN
  86   SUBGOAL_THEN
  87    `!a b. a IN g /\ b IN g
  88           ==> ((coset:A->A->bool) a = coset b) \/
  89               ((coset a) INTER (coset b) = {})`
  90   ASSUME_TAC THENL
  91    [REPEAT STRIP_TAC THEN
  92     ASM_CASES_TAC `((i:A->A)(b) ** a:A) IN (h:A->bool)` THENL
  93      [DISJ1_TAC THEN EXPAND_TAC "coset" THEN
  94       REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
  95       GEN_TAC THEN AP_TERM_TAC THEN
  96       SUBGOAL_THEN
  97        `!x:A. x IN h ==> (b ** (i(b) ** a:A) ** x = a ** x) /\
  98                          (a ** i(i(b) ** a) ** x = b ** x)`
  99        (fun th -> EQ_TAC THEN REPEAT STRIP_TAC THEN
 100           ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[th]) THEN
 101       ASM_SIMP_TAC[];
 102       ALL_TAC] THEN
 103     DISJ2_TAC THEN REWRITE_TAC[EXTENSION; NOT_IN_EMPTY; IN_INTER] THEN
 104     X_GEN_TAC `x:A` THEN EXPAND_TAC "coset" THEN REWRITE_TAC[IN_ELIM_THM] THEN
 105     REWRITE_TAC[TAUT `(a /\ b) /\ (a /\ c) <=> a /\ b /\ c`] THEN
 106     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 107     DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_THEN `y:A` STRIP_ASSUME_TAC)
 108                                (X_CHOOSE_THEN `z:A` STRIP_ASSUME_TAC)) THEN
 109     SUBGOAL_THEN `(i(b:A) ** a ** y):A = i(b) ** b ** z` ASSUME_TAC THENL
 110      [ASM_MESON_TAC[]; ALL_TAC] THEN
 111     SUBGOAL_THEN `(i(b:A) ** a:A ** y):A = e ** z` ASSUME_TAC THENL
 112      [ASM_MESON_TAC[]; ALL_TAC] THEN
 113     SUBGOAL_THEN `(i(b:A) ** a:A ** y):A = z` ASSUME_TAC THENL
 114      [ASM_MESON_TAC[]; ALL_TAC] THEN
 115     SUBGOAL_THEN `((i(b:A) ** a:A) ** y):A = z` ASSUME_TAC THENL
 116      [ASM_MESON_TAC[]; ALL_TAC] THEN
 117     SUBGOAL_THEN `((i(b:A) ** a:A) ** y) ** i(y) = z ** i(y)` ASSUME_TAC THENL
 118      [ASM_MESON_TAC[]; ALL_TAC] THEN
 119     SUBGOAL_THEN `(i(b:A) ** a:A) ** (y ** i(y)) = z ** i(y)` ASSUME_TAC THENL
 120      [ASM_MESON_TAC[]; ALL_TAC] THEN
 121     SUBGOAL_THEN `(i(b:A) ** a:A) ** e = z ** i(y)` ASSUME_TAC THENL
 122      [ASM_MESON_TAC[]; ALL_TAC] THEN
 123     SUBGOAL_THEN `(i(b:A) ** a:A):A = z ** i(y)` ASSUME_TAC THENL
 124      [ASM_MESON_TAC[]; ALL_TAC] THEN
 125     ASM_MESON_TAC[];
 126     ALL_TAC] THEN
 127   EXISTS_TAC `{c:A | ?a:A. a IN g /\ (c = (@)(coset a))}` THEN
 128   MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> b /\ a`) THEN CONJ_TAC THENL
 129    [X_GEN_TAC `b:A` THEN DISCH_TAC THEN
 130     EXISTS_TAC `(@)((coset:A->A->bool) b)` THEN
 131     REWRITE_TAC[RIGHT_EXISTS_AND_THM] THEN CONJ_TAC THENL
 132      [REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `b:A` THEN
 133       ASM_REWRITE_TAC[];
 134       ALL_TAC] THEN
 135     SUBGOAL_THEN `(@)((coset:A->A->bool) b) IN (coset b)` MP_TAC THENL
 136      [REWRITE_TAC[IN] THEN MATCH_MP_TAC SELECT_AX THEN
 137       ASM_MESON_TAC[IN];
 138       ALL_TAC] THEN
 139     FIRST_ASSUM(fun th -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o RATOR_CONV)
 140                          [SYM th]) THEN
 141     REWRITE_TAC[] THEN
 142     ABBREV_TAC `C = (@)((coset:A->A->bool) b)` THEN
 143     REWRITE_TAC[IN_ELIM_THM] THEN
 144     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
 145      (X_CHOOSE_THEN `c:A` STRIP_ASSUME_TAC)) THEN
 146     EXISTS_TAC `(i:A->A)(c)` THEN ASM_SIMP_TAC[] THEN
 147     ASM_MESON_TAC[];
 148     ALL_TAC] THEN
 149   ABBREV_TAC `q = {c:A | ?a:A. a IN g /\ (c = (@)(coset a))}` THEN
 150   DISCH_TAC THEN
 151   SUBGOAL_THEN
 152    `!a:A b. a IN g /\ b IN g /\ a IN coset(b) ==> b IN coset(a)`
 153   ASSUME_TAC THENL
 154    [REPEAT GEN_TAC THEN EXPAND_TAC "coset" THEN
 155     REWRITE_TAC[IN_ELIM_THM] THEN REWRITE_TAC[GSYM CONJ_ASSOC] THEN
 156     REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 157     DISCH_THEN(X_CHOOSE_THEN `c:A` STRIP_ASSUME_TAC) THEN
 158     ASM_REWRITE_TAC[] THEN EXISTS_TAC `(i:A->A) c` THEN
 159     ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[];
 160     ALL_TAC] THEN
 161   SUBGOAL_THEN
 162    `!a:A b c. a IN coset(b) /\ b IN coset(c) /\ c IN g ==> a IN coset(c)`
 163   ASSUME_TAC THENL
 164    [REPEAT GEN_TAC THEN EXPAND_TAC "coset" THEN
 165     REWRITE_TAC[IN_ELIM_THM] THEN
 166     STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[];
 167     ALL_TAC] THEN
 168   SUBGOAL_THEN `!a:A b:A. a IN coset(b) ==> a IN g` ASSUME_TAC THENL
 169    [EXPAND_TAC "coset" THEN REWRITE_TAC[IN_ELIM_THM] THEN MESON_TAC[];
 170     ALL_TAC] THEN
 171   SUBGOAL_THEN
 172    `!a:A b. a IN coset(b) /\ b IN g ==> (coset a = coset b)`
 173   ASSUME_TAC THENL
 174    [REWRITE_TAC[EXTENSION] THEN
 175     MAP_EVERY UNDISCH_TAC
 176      [`!a:A b:A. a IN coset(b) ==> a IN g`;
 177       `!a:A b c. a IN coset(b) /\ b IN coset(c) /\ c IN g ==> a IN coset(c)`;
 178       `!a:A b. a IN g /\ b IN g /\ a IN coset(b) ==> b IN coset(a)`] THEN
 179     MESON_TAC[];
 180     ALL_TAC] THEN
 181   SUBGOAL_THEN `!a:A. a IN g ==> (@)(coset a):A IN (coset a)` ASSUME_TAC THENL
 182    [REPEAT STRIP_TAC THEN UNDISCH_TAC `!a:A. a IN g ==> a IN coset a` THEN
 183     DISCH_THEN(MP_TAC o SPEC `a:A`) THEN
 184     ASM_REWRITE_TAC[] THEN REWRITE_TAC[IN; SELECT_AX];
 185     ALL_TAC] THEN
 186   SUBGOAL_THEN `!a:A. a IN q ==> a IN g` ASSUME_TAC THENL
 187    [GEN_TAC THEN EXPAND_TAC "q" THEN REWRITE_TAC[IN_ELIM_THM] THEN
 188     STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[];
 189     ALL_TAC] THEN
 190   SUBGOAL_THEN
 191    `!a:A x:A a' x'. a IN q /\ a' IN q /\ x IN h /\ x' IN h /\
 192                     ((a' ** x') :A = a ** x) ==> (a' = a) /\ (x' = x)`
 193   ASSUME_TAC THENL
 194    [REPEAT GEN_TAC THEN EXPAND_TAC "q" THEN REWRITE_TAC[IN_ELIM_THM] THEN
 195     MATCH_MP_TAC(TAUT `(c ==> a /\ b ==> d) ==> a /\ b /\ c ==> d`) THEN
 196     STRIP_TAC THEN
 197     DISCH_THEN(CONJUNCTS_THEN2
 198      (X_CHOOSE_THEN `a1:A` STRIP_ASSUME_TAC)
 199      (X_CHOOSE_THEN `a2:A` STRIP_ASSUME_TAC)) THEN
 200     SUBGOAL_THEN `a:A IN g /\ a' IN g` STRIP_ASSUME_TAC THENL
 201      [ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]; ALL_TAC] THEN
 202     MATCH_MP_TAC(TAUT `(a ==> b) /\ a ==> a /\ b`) THEN
 203     CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 204     SUBGOAL_THEN
 205      `((coset:A->A->bool) a1 = coset a) /\ (coset a2 = coset a')`
 206     MP_TAC THENL
 207      [CONJ_TAC THEN CONV_TAC SYM_CONV THEN FIRST_ASSUM MATCH_MP_TAC THEN
 208       ASM_SIMP_TAC[];
 209       ALL_TAC] THEN
 210     DISCH_THEN(CONJUNCTS_THEN SUBST_ALL_TAC) THEN
 211     ONCE_ASM_REWRITE_TAC[] THEN AP_TERM_TAC THEN
 212     FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
 213     EXPAND_TAC "coset" THEN REWRITE_TAC[IN_ELIM_THM] THEN
 214     ASM_REWRITE_TAC[] THEN EXISTS_TAC `(x:A ** (i:A->A)(x')):A` THEN
 215     ASM_SIMP_TAC[] THEN UNDISCH_TAC `(a':A ** x':A):A = a ** x` THEN
 216     DISCH_THEN(MP_TAC o C AP_THM `(i:A->A) x'` o AP_TERM `(**):A->A->A`) THEN
 217     DISCH_THEN(SUBST1_TAC o SYM) THEN ASM_MESON_TAC[];
 218     ALL_TAC] THEN
 219   SUBGOAL_THEN `g = IMAGE (\(a:A,x:A). (a ** x):A) {(a,x) | a IN q /\ x IN h}`
 220   SUBST1_TAC THENL
 221    [REWRITE_TAC[EXTENSION; IN_IMAGE; IN_ELIM_THM] THEN
 222     REWRITE_TAC[EXISTS_PAIR_THM] THEN
 223     CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
 224     REWRITE_TAC[PAIR_EQ] THEN
 225     REWRITE_TAC[CONJ_ASSOC; ONCE_REWRITE_RULE[CONJ_SYM] UNWIND_THM1] THEN
 226     ASM_MESON_TAC[];
 227     ALL_TAC] THEN
 228   MATCH_MP_TAC EQ_TRANS THEN
 229   EXISTS_TAC `CARD {(a:A,x:A) | a IN q /\ x IN h}` THEN CONJ_TAC THENL
 230    [MATCH_MP_TAC CARD_IMAGE_INJ THEN CONJ_TAC THENL
 231      [REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_THM] THEN
 232       CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
 233       REWRITE_TAC[PAIR_EQ] THEN REPEAT GEN_TAC THEN
 234       REPEAT(DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC)) THEN
 235       ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[];
 236       ALL_TAC] THEN
 237     MATCH_MP_TAC FINITE_PRODUCT THEN CONJ_TAC THEN
 238     MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `g:A->bool` THEN
 239     ASM_REWRITE_TAC[SUBSET];
 240     ALL_TAC] THEN
 241   MATCH_MP_TAC CARD_PRODUCT THEN CONJ_TAC THEN
 242   MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `g:A->bool` THEN
 243   ASM_REWRITE_TAC[SUBSET]);;
 244
 245 (* ------------------------------------------------------------------------- *)
 246 (* Traditional statement is only part of this.                               *)
 247 (* ------------------------------------------------------------------------- *)
 248
 249 let GROUP_LAGRANGE = prove
 250  (`!g h ( ** ) i e.
 251         group (g,( ** ),i,e:A) /\ subgroup h (g,( ** ),i,e) /\ FINITE g
 252         ==> (CARD h) divides (CARD g)`,
 253   REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP GROUP_LAGRANGE_COSETS) THEN
 254   MESON_TAC[DIVIDES_LMUL; DIVIDES_REFL]);;