needs "Library/prime.ml";;

parse_as_infix("**",(20,"right"));;

let group = new_definition
  `group(g,(**),i,(e:A)) <=>
    (e IN g) /\ (!x. x IN g ==> i(x) IN g) /\
    (!x y. x IN g /\ y IN g ==> x**y IN g) /\
    (!x y z. x IN g /\ y IN g /\ z IN g ==> x**(y**z) = (x**y)**z) /\
    (!x. x IN g ==> x**e = x /\ e**x = x) /\
    (!x. x IN g ==> x**i(x) = e /\ i(x)**x = e)`;;
let subgroup = new_definition
  `subgroup h (g,(**),i,(e:A)) <=> h SUBSET g /\ group(h,(**),i,e)`;;
(* ======== translation of John's proof ==================================== *)

horizon := 1;;

let GROUP_LAGRANGE_COSETS = thm `;
  !g h (**) i e.
       group(g,(**),i,e:A) /\ subgroup h (g,(**),i,e) /\ FINITE g
       ==> ?q. CARD g = CARD q * CARD h /\
               !b. b IN g ==> ?a x. a IN q /\ x IN h /\ b = a**x
proof exec REWRITE_TAC[group; subgroup; SUBSET];
  let g h be A->bool;
  let (**) be A->A->A;
  let i be A->A;
  let e be A;
  assume e IN g;
  assume !x. x IN g ==> i(x) IN g [1];
  assume !x y. x IN g /\ y IN g ==> x**y IN g [2];
  assume !x y z. x IN g /\ y IN g /\ z IN g
                 ==> x**(y**z) = (x**y)**z [3];
  assume !x. x IN g ==> x**e = x /\ e**x = x [4];
  assume !x. x IN g ==> x**i(x) = e /\ i(x)**x = e [5];
  assume !x. x IN h ==> x IN g [6];
  assume e IN h [7];
  assume !x. x IN h ==> i(x) IN h [8];
  assume !x y. x IN h /\ y IN h ==> x**y IN h [9];
  assume !x y z. x IN h /\ y IN h /\ z IN h
                 ==> x**(y**z) = (x**y)**z;
  assume !x. x IN h ==> x**e = x /\ e**x = x [10];
  assume !x. x IN h ==> x**i(x) = e /\ i(x)**x = e [11];
  assume FINITE g [12];
  set coset = \a. {b | b IN g /\ ?x. x IN h /\ b = a**x} [coset];
  !a. coset a = {b' | b' IN g /\ ?x. x IN h /\ b' = a**x} [13];
  !a. a IN g ==> a IN coset a [14]
  proof let a be A;
    assume a IN g [15];
    ?x. x IN h /\ a = a**x by 4,7;
  qed by SIMP_TAC,13,15,IN_ELIM_THM;
  FINITE h [16] by 6,12,FINITE_SUBSET,SUBSET;
  !a. FINITE (coset a)
  proof let a be A;
    ?t. FINITE t /\ coset a SUBSET t
    proof take g;
    qed by SIMP_TAC,12,13,IN_ELIM_THM,SUBSET;
  qed by MATCH_MP_TAC,FINITE_SUBSET;
  !a x y. a IN g /\ x IN g /\ y IN g /\ a**x = a**y ==> x = y [17]
  proof let a x y be A;
    assume a IN g /\ x IN g /\ y IN g /\ a**x = a**y [18];
    (i(a)**a)**x = (i(a)**a)**y by 1,3;
    e**x = e**y by 5,18;
  qed by 4,18;
  !a. a IN g ==> CARD (coset a) = CARD h
  proof let a be A;
    assume a IN g [19];
    coset a = IMAGE (\x. a**x) h [20]
    proof
      !x. x IN g /\ (?x'. x' IN h /\ x = a**x') <=>
          ?x'. x = a**x' /\ x' IN h by 2,6;
    qed by REWRITE_TAC,13,EXTENSION,IN_IMAGE,IN_ELIM_THM;
    (!x y. x IN h /\ y IN h /\ a**x = a**y ==> x = y) /\ FINITE h
      by 6,16,17,19;
    CARD (IMAGE (\x. a**x) h) = CARD h by MATCH_MP_TAC,CARD_IMAGE_INJ;
  qed by 20;
  !x y. x IN g /\ y IN g ==> i(x**y) = i(y)**i(x) [21]
  proof let x y be A;
    assume x IN g /\ y IN g [22];
    ?a. a IN g /\ i(x**y) IN g /\ i(y)**i(x) IN g /\
        a**i(x**y) = a**i(y)**i(x)
    proof take x**y;
      e = x**(y**i(y))**i(x) by 1,4,5,22;
        .= ((x**y)**i(y))**i(x) by 1,2,3,22;
    qed by SIMP_TAC,1,2,3,5,22;
  qed by 17;
  !x. x IN g ==> i(i(x)) = x [23]
  proof let x be A;
    assume x IN g;
    ?a. a IN g /\ i(i(x)) IN g /\ x IN g /\ a**i(i(x)) = a**x
    proof take i(x);
    qed by 1,5;
  qed by MATCH_MP_TAC,17;
  !a b. a IN g /\ b IN g
        ==> coset a = coset b \/ coset a INTER coset b = {}
  proof let a b be A;
    assume a IN g /\ b IN g [24];
    cases;
    suppose i(b)**a IN h [25];
      now let x be A;
        !x. x IN h ==> b**(i(b)**a)**x = a**x /\ a**i(i(b)**a)**x = b**x
          by SIMP_TAC,1,3,4,5,6,21,23,24;
        thus x IN g /\ (?x'. x' IN h /\ x = a**x') <=>
             x IN g /\ (?x'. x' IN h /\ x = b**x') by 8,9,25;
      end;
      coset a = coset b by REWRITE_TAC,13,EXTENSION,IN_ELIM_THM;
    qed;
    suppose ~(i(b)**a IN h) [26];
      now let x be A;
        assume x IN g /\ (?y. y IN h /\ x = a**y) /\ (?z. z IN h /\ x = b**z);
        consider y z such that y IN h /\ x = a**y /\ z IN h /\ x = b**z [27];
        (i(b)**a)**y = i(b)**a**y by 1,3,6,24,27;
          .= i(b)**b**z by 27;
          .= e**z by 1,3,5,6,24,27;
          .= z by 10,27;
        z**i(y) = ((i(b)**a)**y)**i(y);
          .= (i(b)**a)**y**i(y) by 1,2,3,5,6,24,27;
          .= (i(b)**a)**e by 11,27;
          .= i(b)**a by 1,2,4,24;
        thus F by 8,9,26,27;
      end;
      !x. ~((x IN g /\ ?y. y IN h /\ x = a**y) /\
            (x IN g /\ ?z. z IN h /\ x = b**z));
      coset a INTER coset b = {}
        by REWRITE_TAC,13,EXTENSION,NOT_IN_EMPTY,IN_INTER,IN_ELIM_THM;
    qed;
  end;
  set q = {c | ?a. a IN g /\ c = (@)(coset a)} [q] [28]; take q;
  !b. b IN g ==> ?a x. a IN q /\ x IN h /\ b = a**x [29]
  proof let b be A;
    assume b IN g [30];
    set C = (@)(coset b) [C] [31]; take C;
    (@)(coset b) IN {c | ?a. a IN g /\ c = (@)(coset a)} by 30;
    thus C IN q by q,C;
    C IN coset b by 14,30,C,IN,SELECT_AX;
    C IN {b' | b' IN g /\ ?x. x IN h /\ b' = b**x} by 13;
    consider c such that
      C IN g /\ c IN h /\ C = b**c [32];
    take i(c);
    (b**c)**i(c) = b**c**i(c) by 1,3,6,30;
      .= b by 1,4,5,6,30,32;
  qed by 8,32;
  !a b. a IN g /\ b IN g /\ a IN coset b ==> b IN coset a [33]
  proof let a b be A;
    a IN g /\ b IN g /\ a IN g /\ (?x. x IN h /\ a = b**x)
    ==> b IN g /\ (?x. x IN h /\ b = a**x)
    proof
      assume a IN g /\ b IN g /\ a IN g /\ ?x. x IN h /\ a = b**x [34];
      thus b IN g;
      consider c such that c IN h /\ a = b**c by 34;
      take i(c);
    qed by 3,4,6,8,11,34;
  qed by REWRITE_TAC,13,IN_ELIM_THM;
  !a b c. a IN coset b /\ b IN coset c /\ c IN g ==> a IN coset c [35]
  proof let a b c be A;
    now assume (a IN g /\ ?x. x IN h /\ a = b**x) /\
               (b IN g /\ ?x. x IN h /\ b = c**x) /\ c IN g [36];
      consider x x' such that x IN h /\ a = b**x /\ x' IN h /\ b = c**x';
      thus a IN g /\ ?x. x IN h /\ a = c**x by 3,6,9,36;
    end;
  qed by REWRITE_TAC,13,IN_ELIM_THM;
  !a b. a IN coset b ==> a IN g [37]
  proof let a b be A;
    a IN g /\ (?x. x IN h /\ a = b**x) ==> a IN g;
  qed by REWRITE_TAC,13,IN_ELIM_THM;
  !a b. a IN coset b /\ b IN g ==> coset a = coset b [38]
    by 33,35,37,EXTENSION;
  !a. a IN g ==> (@)(coset a) IN coset a [39] by 14,IN,SELECT_AX;
  !a. a IN q ==> a IN g [40]
  proof let a be A; assume a IN q;
    a IN {c | ?a. a IN g /\ c = (@)(coset a)} by q;
    consider a' such that a' IN g /\ a = (@)(coset a');
  qed by 37,39;
  !a x a' x'. a IN q /\ a' IN q /\ x IN h /\ x' IN h /\ a'**x' = a**x
              ==> a' = a /\ x' = x [41]
  proof let a x a' x' be A;
    assume a IN q /\ a' IN q /\ x IN h /\ x' IN h /\ a'**x' = a**x [42];
    a IN {c | ?a. a IN g /\ c = (@)(coset a)} /\
    a' IN {c | ?a. a IN g /\ c = (@)(coset a)} by q;
    consider a1 a2 such that
      a1 IN g /\ a = (@)(coset a1) /\ a2 IN g /\ a' = (@)(coset a2) [43];
    a IN g /\ a' IN g [44] by 37,39;
    coset a = coset a1 /\ coset a' = coset a2 by 38,39,43;
    a = (@)(coset a) /\ a' = (@)(coset a') [45] by 43;
    ?x. x IN h /\ a' = a**x
    proof take x**i(x');
      thus x**i(x') IN h by 8,9,42;
      a' = a'**x'**i(x') by 4,5,6,42,44;
        .= (a**x)**i(x') by 1,2,3,6,42,44;
    qed by 1,2,3,6,42,44;
    a' IN coset a by REWRITE_TAC,13,44,IN_ELIM_THM;
    coset a = coset a' by 38,44;
  qed by 6,17,42,44,45;
  g = IMAGE (\(a,x). a**x) {(a,x) | a IN q /\ x IN h}
  proof
    !x. x IN g <=> ?p1 p2. (x = p1**p2 /\ p1 IN q) /\ p2 IN h by 2,6,29,40;
  qed by REWRITE_TAC,EXTENSION,IN_IMAGE,IN_ELIM_THM,EXISTS_PAIR_THM,PAIR_EQ,
         CONJ_ASSOC,ONCE_REWRITE_RULE[CONJ_SYM] UNWIND_THM1;
  CARD g = CARD (IMAGE (\(a,x). a**x) {(a,x) | a IN q /\ x IN h}) [46];
    .= CARD {(a,x) | a IN q /\ x IN h}
  proof
    !x y. x IN {(a,x) | a IN q /\ x IN h} /\
          y IN {(a,x) | a IN q /\ x IN h} /\
          (\(a,x). a**x) x = (\(a,x). a**x) y
          ==> x = y [47]
    proof
      !p1 p2 p1' p2'. (?a x. (a IN q /\ x IN h) /\ p1 = a /\ p2 = x) /\
                      (?a x. (a IN q /\ x IN h) /\ p1' = a /\ p2' = x) /\
                      p1**p2 = p1'**p2'
                      ==> p1 = p1' /\ p2 = p2' by 41;
    qed by REWRITE_TAC,FORALL_PAIR_THM,IN_ELIM_THM,PAIR_EQ;
    FINITE q /\ FINITE h by 6,12,40,FINITE_SUBSET,SUBSET;
    FINITE {(a,x) | a IN q /\ x IN h} by FINITE_PRODUCT;
  qed by MATCH_MP_TAC CARD_IMAGE_INJ,47;
    .= CARD q * CARD h by 6,12,40,46,CARD_PRODUCT,FINITE_SUBSET,SUBSET;
qed by 29`;;

let GROUP_LAGRANGE = thm `;
  !g h (**) i e.
       group (g,( ** ),i,e:A) /\ subgroup h (g,(**),i,e) /\ FINITE g
       ==> CARD h divides CARD g
  by GROUP_LAGRANGE_COSETS,DIVIDES_LMUL,DIVIDES_REFL`;;

(* ======== and formal proof sketch derived from this translation ========== *)

horizon := -1;;

let GROUP_LAGRANGE_COSETS_SKETCH = ref None;;

GROUP_LAGRANGE_COSETS_SKETCH := Some `;
  !g h (**) i e.
       group(g,(**),i,e:A) /\ subgroup h (g,(**),i,e) /\ FINITE g
       ==> ?q. CARD g = CARD q * CARD h /\
               !b. b IN g ==> ?a x. a IN q /\ x IN h /\ b = a**x
proof exec REWRITE_TAC[group; subgroup; SUBSET];
  let g h be A->bool;
  let (**) be A->A->A;
  let i be A->A;
  let e be A;
  assume e IN g;
  assume !x. x IN g ==> i(x) IN g;
  assume !x y. x IN g /\ y IN g ==> x**y IN g;
  assume !x y z. x IN g /\ y IN g /\ z IN g
                 ==> x**(y**z) = (x**y)**z;
  assume !x. x IN g ==> x**e = x /\ e**x = x;
  assume !x. x IN g ==> x**i(x) = e /\ i(x)**x = e;
  assume !x. x IN h ==> x IN g;
  assume e IN h;
  assume !x. x IN h ==> i(x) IN h;
  assume !x y. x IN h /\ y IN h ==> x**y IN h;
  assume !x y z. x IN h /\ y IN h /\ z IN h
                 ==> x**(y**z) = (x**y)**z;
  assume !x. x IN h ==> x**e = x /\ e**x = x;
  assume !x. x IN h ==> x**i(x) = e /\ i(x)**x = e;
  assume FINITE g;
  set coset = \a. {b | b IN g /\ ?x. x IN h /\ b = a**x};
  !a. coset a = {b' | b' IN g /\ ?x. x IN h /\ b' = a**x};
  !a. a IN g ==> a IN coset a
  proof let a be A;
    assume a IN g;
    ?x. x IN h /\ a = a**x;
  qed;
  FINITE h;
::        #1
:: 1: inference error
  !a. FINITE (coset a)
  proof let a be A;
    ?t. FINITE t /\ coset a SUBSET t
    proof take g;
    qed;
::     #2
:: 2: inference time-out
  qed;
::   #2
  !a x y. a IN g /\ x IN g /\ y IN g /\ a**x = a**y ==> x = y
  proof let a x y be A;
    assume a IN g /\ x IN g /\ y IN g /\ a**x = a**y;
    (i(a)**a)**x = (i(a)**a)**y;
    e**x = e**y;
::             #2
  qed;
  !a. a IN g ==> CARD (coset a) = CARD h
  proof let a be A;
    assume a IN g;
    coset a = IMAGE (\x. a**x) h
    proof
      !x. x IN g /\ (?x'. x' IN h /\ x = a**x') <=>
          ?x'. x = a**x' /\ x' IN h;
    qed;
::     #2
    (!x y. x IN h /\ y IN h /\ a**x = a**y ==> x = y) /\ FINITE h;
    CARD (IMAGE (\x. a**x) h) = CARD h;
::                                    #2
  qed;
  !x y. x IN g /\ y IN g ==> i(x**y) = i(y)**i(x)
  proof let x y be A;
    assume x IN g /\ y IN g;
    ?a. a IN g /\ i(x**y) IN g /\ i(y)**i(x) IN g /\
        a**i(x**y) = a**i(y)**i(x)
    proof take x**y;
      e = x**(y**i(y))**i(x);
::                          #2
        .= ((x**y)**i(y))**i(x);
::                             #2
    qed;
  qed;
  !x. x IN g ==> i(i(x)) = x
  proof let x be A;
    assume x IN g;
    ?a. a IN g /\ i(i(x)) IN g /\ x IN g /\ a**i(i(x)) = a**x
    proof take i(x);
    qed;
  qed;
  !a b. a IN g /\ b IN g
        ==> coset a = coset b \/ coset a INTER coset b = {}
  proof let a b be A;
    assume a IN g /\ b IN g;
    cases;
    suppose i(b)**a IN h;
      now let x be A;
        !x. x IN h ==> b**(i(b)**a)**x = a**x /\ a**i(i(b)**a)**x = b**x;
::                                                                      #2
        thus x IN g /\ (?x'. x' IN h /\ x = a**x') <=>
             x IN g /\ (?x'. x' IN h /\ x = b**x');
::                                                #2
      end;
      coset a = coset b;
::                     #2
    qed;
    suppose ~(i(b)**a IN h);
      now let x be A;
        assume x IN g /\ (?y. y IN h /\ x = a**y) /\ (?z. z IN h /\ x = b**z);
        consider y z such that y IN h /\ x = a**y /\ z IN h /\ x = b**z;
        (i(b)**a)**y = i(b)**a**y;
          .= i(b)**b**z;
          .= e**z;
::               #2
          .= z;
        z**i(y) = ((i(b)**a)**y)**i(y);
          .= (i(b)**a)**y**i(y);
::                             #2
          .= (i(b)**a)**e;
          .= i(b)**a;
::                  #2
        thus F;
::            #2
      end;
      !x. ~((x IN g /\ ?y. y IN h /\ x = a**y) /\
            (x IN g /\ ?z. z IN h /\ x = b**z));
      coset a INTER coset b = {};
::                              #2
    qed;
  end;
  set q = {c | ?a. a IN g /\ c = (@)(coset a)};
  take q;
  !b. b IN g ==> ?a x. a IN q /\ x IN h /\ b = a**x
  proof let b be A;
    assume b IN g;
    set C = (@)(coset b);
    take C;
    (@)(coset b) IN {c | ?a. a IN g /\ c = (@)(coset a)};
    thus C IN q;
    C IN coset b;
::              #2
    C IN {b' | b' IN g /\ ?x. x IN h /\ b' = b**x};
    consider c such that
      C IN g /\ c IN h /\ C = b**c;
    take i(c);
    (b**c)**i(c) = b**c**i(c);
      .= b;
  qed;
  !a b. a IN g /\ b IN g /\ a IN coset b ==> b IN coset a
  proof let a b be A;
    a IN g /\ b IN g /\ a IN g /\ (?x. x IN h /\ a = b**x)
    ==> b IN g /\ (?x. x IN h /\ b = a**x)
    proof
      assume a IN g /\ b IN g /\ a IN g /\ ?x. x IN h /\ a = b**x;
      thus b IN g;
      consider c such that c IN h /\ a = b**c;
      take i(c);
    qed;
::     #2
  qed;
  !a b c. a IN coset b /\ b IN coset c /\ c IN g ==> a IN coset c
  proof let a b c be A;
    now assume (a IN g /\ ?x. x IN h /\ a = b**x) /\
               (b IN g /\ ?x. x IN h /\ b = c**x) /\ c IN g;
      consider x x' such that x IN h /\ a = b**x /\ x' IN h /\ b = c**x';
      thus a IN g /\ ?x. x IN h /\ a = c**x;
::                                         #2
    end;
  qed;
::   #2
  !a b. a IN coset b ==> a IN g
  proof let a b be A;
    a IN g /\ (?x. x IN h /\ a = b**x) ==> a IN g;
  qed;
  !a b. a IN coset b /\ b IN g ==> coset a = coset b;
::                                                  #2
  !a. a IN g ==> (@)(coset a) IN coset a;
::                                      #2
  !a. a IN q ==> a IN g
  proof let a be A;
    assume a IN q;
    a IN {c | ?a. a IN g /\ c = (@)(coset a)};
    consider a' such that a' IN g /\ a = (@)(coset a');
  qed;
  !a x a' x'. a IN q /\ a' IN q /\ x IN h /\ x' IN h /\ a'**x' = a**x
              ==> a' = a /\ x' = x
  proof let a x a' x' be A;
    assume a IN q /\ a' IN q /\ x IN h /\ x' IN h /\ a'**x' = a**x;
    a IN {c | ?a. a IN g /\ c = (@)(coset a)} /\
    a' IN {c | ?a. a IN g /\ c = (@)(coset a)};
    consider a1 a2 such that
      a1 IN g /\ a = (@)(coset a1) /\ a2 IN g /\ a' = (@)(coset a2);
::                                                                 #2
    a IN g /\ a' IN g;
    coset a = coset a1 /\ coset a' = coset a2;
::                                           #2
    a = (@)(coset a) /\ a' = (@)(coset a');
    ?x. x IN h /\ a' = a**x
    proof take x**i(x');
      thus x**i(x') IN h;
::                      #2
      a' = a'**x'**i(x');
::                      #2
        .= (a**x)**i(x');
::                      #2
    qed;
::     #2
    a' IN coset a;
::               #2
    coset a = coset a';
  qed;
::   #2
  g = IMAGE (\(a,x). a**x) {(a,x) | a IN q /\ x IN h}
  proof
    !x. x IN g <=> ?p1 p2. (x = p1**p2 /\ p1 IN q) /\ p2 IN h;
::                                                           #2
  qed;
::   #2
  CARD g = CARD (IMAGE (\(a,x). a**x) {(a,x) | a IN q /\ x IN h});
    .= CARD {(a,x) | a IN q /\ x IN h}
  proof
    !x y. x IN {(a,x) | a IN q /\ x IN h} /\
          y IN {(a,x) | a IN q /\ x IN h} /\
          (\(a,x). a**x) x = (\(a,x). a**x) y
          ==> x = y
    proof
      !p1 p2 p1' p2'. (?a x. (a IN q /\ x IN h) /\ p1 = a /\ p2 = x) /\
                      (?a x. (a IN q /\ x IN h) /\ p1' = a /\ p2' = x) /\
                      p1**p2 = p1'**p2'
                      ==> p1 = p1' /\ p2 = p2';
    qed;
::     #2
    FINITE q /\ FINITE h;
::                      #2
    FINITE {(a,x) | a IN q /\ x IN h};
::                                   #2
  qed;
::   #2
    .= CARD q * CARD h;
::                    #2
qed`;;