miz3/Samples/lagrange.ml

   1 needs "Library/prime.ml";;
   2
   3 let group = new_definition
   4   `group(g,(**),i,(e:A)) <=>
   5     (e IN g) /\ (!x. x IN g ==> i(x) IN g) /\
   6     (!x y. x IN g /\ y IN g ==> x**y IN g) /\
   7     (!x y z. x IN g /\ y IN g /\ z IN g ==> x**(y**z) = (x**y)**z) /\
   8     (!x. x IN g ==> x**e = x /\ e**x = x) /\
   9     (!x. x IN g ==> x**i(x) = e /\ i(x)**x = e)`;;
  10
  11 let subgroup = new_definition
  12   `subgroup h (g,(**),i,(e:A)) <=> h SUBSET g /\ group(h,(**),i,e)`;;
  13
  14 let bijection = new_definition
  15   `bijection f s t <=> ?g. (!x:A. x IN s ==> f x IN t /\ g (f x) = x) /\
  16                            (!y:B. y IN t ==> g y IN s /\ f (g y) = y)`;;
  17
  18 parse_as_infix("PARTITIONS",(12,"right"));;
  19
  20 let PARTITIONS = new_definition
  21   `X PARTITIONS s <=> UNIONS X = (s:A->bool) /\
  22                       !t u. t IN X /\ u IN X /\ ~(t = u) ==> t INTER u = {}`;;
  23
  24 parse_as_infix("**",(20,"left"));;
  25 parse_as_infix("***",(20,"left"));;
  26
  27 horizon := -1;;
  28
  29 let LAGRANGE_SKETCH = ref None;;
  30
  31 LAGRANGE_SKETCH := Some `;
  32   let H G be A->bool; let (**) be A->A->A; let i be A->A; let e be A;
  33   assume FINITE H /\ group (H,(**),i,e:A) /\ subgroup G (H,(**),i,e);
  34   consider (***) such that !h G. h***G = {h**g | g IN G};
  35 //
  36   now let a be A; assume a IN H; let b be A; assume b IN H;
  37     assume i(a)**b IN G;
  38     b***G = a**i(a)**b***G; .= a***(i(a)**b***G); thus .= a***G;
  39   end;
  40   !a b. a IN H /\ b IN H /\ ~(a***G = b***G) ==> a***G INTER b***G = {}
  41   proof let a be A; assume a IN H; let b be A; assume b IN H;
  42     now assume ~(a***G INTER b***G = {});
  43       consider g1 g2 such that g1 IN G /\ g2 IN G /\ a**g1 = b**g2;
  44       g1**i(g2) = i(a)**b;
  45       i(a)**b IN G;
  46       thus a***G = b***G;
  47     end;
  48   qed;
  49   !a. a IN H ==> a IN a***G
  50   proof let a be A; assume a IN H;
  51     a**e = a;
  52   qed;
  53   {a***G | a IN H} PARTITIONS H;
  54   !a b. a IN H /\ b IN H ==> CARD (a***G) = CARD (b***G)
  55   proof let a be A; assume a IN H; let b be A; assume b IN H;
  56     consider f such that !g. g IN G ==> f(a**g) = b**g;
  57     bijection f (a***G) (b***G);
  58   qed;
  59   set INDEX = CARD {a***G | a IN H};
  60   set N = CARD H; set n = CARD G; set j = INDEX;
  61   N = j*n;
  62   thus CARD G divides CARD H;
  63 //
  64 `;;
  65
  66 LAGRANGE_SKETCH := Some `;
  67   let H G be A->bool; let (**) be A->A->A; let i be A->A; let e be A;
  68   assume FINITE H /\ group (H,(**),i,e:A) /\ subgroup G (H,(**),i,e);
  69   consider (***) such that !h G. h***G = {h**g | g IN G};
  70 ::                                                      #2
  71 :: 2: inference time-out
  72 //
  73   now let a be A; assume a IN H; let b be A; assume b IN H;
  74     assume i(a)**b IN G;
  75     b***G = a**i(a)**b***G; .= a***(i(a)**b***G); thus .= a***G;
  76 ::                        #2                    #2             #2
  77   end;
  78   !a b. a IN H /\ b IN H /\ ~(a***G = b***G) ==> a***G INTER b***G = {}
  79   proof let a be A; assume a IN H; let b be A; assume b IN H;
  80     now assume ~(a***G INTER b***G = {});
  81       consider g1 g2 such that g1 IN G /\ g2 IN G /\ a**g1 = b**g2;
  82 ::                                                                #2
  83       g1**i(g2) = i(a)**b;
  84 ::                       #2
  85       i(a)**b IN G;
  86 ::                #2
  87       thus a***G = b***G;
  88     end;
  89   qed;
  90   !a. a IN H ==> a IN a***G
  91   proof let a be A; assume a IN H;
  92     a**e = a;
  93 ::          #1
  94 :: 1: inference error
  95   qed;
  96 ::   #2
  97   {a***G | a IN H} PARTITIONS H;
  98 ::                             #2
  99   !a b. a IN H /\ b IN H ==> CARD (a***G) = CARD (b***G)
 100   proof let a be A; assume a IN H; let b be A; assume b IN H;
 101     consider f such that !g. g IN G ==> f(a**g) = b**g;
 102 ::                                                    #2
 103     bijection f (a***G) (b***G);
 104 ::                             #2
 105   qed;
 106 ::   #2
 107   set INDEX = CARD {a***G | a IN H};
 108   set N = CARD H; set n = CARD G; set j = INDEX;
 109   N = j*n;
 110 ::       #2
 111   thus CARD G divides CARD H;
 112 ::                          #2
 113 //
 114 `;;
 115
 116 horizon := 3;;
 117
 118 let UNIONS_FINITE = thm `;
 119   !s. FINITE (UNIONS s) <=>
 120       FINITE s /\ !t:A->bool. t IN s ==> FINITE t
 121 proof
 122   let s be (A->bool)->bool;
 123   now assume FINITE (UNIONS s) [1];
 124     now let t be A->bool; assume t IN s;
 125       now let x be A; assume x IN t;
 126         ?t. t IN s /\ x IN t;
 127         thus x IN UNIONS s by ALL_TAC,UNIONS,IN_ELIM_THM;
 128       end;
 129       thus t IN {t | t SUBSET UNIONS s} by SUBSET,IN_ELIM_THM;
 130     end;
 131     s SUBSET {t | t SUBSET UNIONS s} by REWRITE_TAC,SUBSET;
 132     FINITE {t | t SUBSET UNIONS s} by 1,FINITE_POWERSET;
 133     thus FINITE s by FINITE_SUBSET;
 134   end;
 135 qed by FINITE_UNIONS`;;
 136
 137 let CARD_UNIONS_EQUAL = thm `;
 138   !X s n. FINITE s /\ X PARTITIONS s /\ (!t:A->bool. t IN X ==> CARD t = n)
 139           ==> CARD s = (CARD X)*n
 140 proof
 141   let X be (A->bool)->bool;
 142   let s be A->bool;
 143   let n be num;
 144   assume FINITE s;
 145   assume X PARTITIONS s [1];
 146   assume !t. t IN X ==> CARD t = n [2];
 147   FINITE (UNIONS X) by PARTITIONS;
 148   !t. t IN X ==> FINITE t [3] by UNIONS_FINITE;
 149   FINITE X [4] by UNIONS_FINITE;
 150   !t. t IN X ==> CARD t = (\t. n) t [5] by 2;
 151   !t u. t IN X /\ u IN X /\ ~(t = u) ==> t INTER u = {} by 1,PARTITIONS;
 152   CARD s = CARD (UNIONS X) by 1,PARTITIONS;
 153     .= nsum X CARD by 2,3,4,CARD_UNIONS;
 154     .= nsum X (\t. n) by 5,NSUM_EQ;
 155 qed by 4,NSUM_CONST`;;
 156
 157 let BIJECTION_CARD_EQ = thm `;
 158   let f be A->B;
 159   let s be A->bool;
 160   let t be B->bool;
 161   assume FINITE s /\ bijection f s t [1];
 162   ?g. (!x. x IN s ==> f x IN t /\ g (f x) = x) /\
 163       (!y. y IN t ==> g y IN s /\ f (g y) = y)
 164     by REWRITE_TAC,-,GSYM bijection;
 165   thus CARD s = CARD t by -,1,BIJECTIONS_CARD_EQ`;;
 166
 167 horizon := 0;;
 168
 169 let LAGRANGE = thm `;
 170   let H G be A->bool;
 171   let (**) be A->A->A;
 172   let i be A->A;
 173   let e be A;
 174   assume FINITE H /\ group (H,(**),i,e) /\ subgroup G (H,(**),i,e) [1];
 175   (e IN H) /\ (!x. x IN H ==> i(x) IN H) /\
 176     (!x y. x IN H /\ y IN H ==> x**y IN H) /\
 177     (!x y z. x IN H /\ y IN H /\ z IN H ==> x**(y**z) = (x**y)**z) /\
 178     (!x. x IN H ==> x**e = x /\ e**x = x) /\
 179     (!x. x IN H ==> x**i(x) = e /\ i(x)**x = e) [2]
 180       by REWRITE_TAC,1,GSYM group;
 181   (G SUBSET H) /\ group (G,(**),i,e) [3] by 1,subgroup;
 182   !x. x IN G ==> x IN H [4] by -,SUBSET;
 183   FINITE G [5] by 3,1,FINITE_SUBSET;
 184   (e IN G) /\ (!x. x IN G ==> i(x) IN G) /\
 185     (!x y. x IN G /\ y IN G ==> x**y IN G) /\
 186     (!x y z. x IN G /\ y IN G /\ z IN G ==> x**(y**z) = (x**y)**z) /\
 187     (!x. x IN G ==> x**e = x /\ e**x = x) /\
 188     (!x. x IN G ==> x**i(x) = e /\ i(x)**x = e) [6]
 189       by REWRITE_TAC,3,GSYM group;
 190   set (***) = \h G. {h**g | g IN G} [7];
 191   !x h G. x IN h***G <=> ?g. g IN G /\ x = h**g [8] by ALL_TAC,-,IN_ELIM_THM;
 192   !h1 h2. h1 IN H /\ h2 IN H ==> (h1**h2)***G = h1***(h2***G) [9]
 193   proof
 194     let h1 h2 be A;
 195     assume h1 IN H /\ h2 IN H [10];
 196     now [11]
 197       let x be A;
 198       assume x IN (h1**h2)***G;
 199       consider g such that g IN G /\ x = (h1**h2)**g [12] by -,8;
 200       g IN H by -,4;
 201       x = h1**(h2**g) [13] by -,2,10,12;
 202       h2**g IN h2***G by 8,12;
 203       thus x IN h1***(h2***G) by -,13,8;
 204     end;
 205     now
 206       let x be A;
 207       assume x IN h1***(h2***G);
 208       consider y such that y IN h2***G /\ x = h1**y [14] by -,8;
 209       consider g such that g IN G /\ y = h2**g [15] by -,8;
 210       g IN H [16] by -,4;
 211       x = h1**(h2**g) by 14,15;
 212         .= (h1**h2)**g by -,2,10,14,16;
 213       thus x IN (h1**h2)***G by -,8,15;
 214     end;
 215   qed by -,11,EXTENSION;
 216   !g. g IN G ==> g***G = G [17]
 217   proof
 218     let g be A;
 219     assume g IN G [18];
 220     now [19]
 221       let x be A;
 222       assume x IN g***G;
 223       consider g' such that g' IN G /\ x = g**g' by -,8;
 224       thus x IN G by -,6,18;
 225     end;
 226     now
 227       let x be A;
 228       assume x IN G [20];
 229       x = g**i(g)**x by -,6,18;
 230         .= g**(i(g)**x) [21] by -,6,18,20;
 231       i(g)**x IN G by 6,18,20;
 232       thus x IN g***G by -,21,8;
 233     end;
 234   qed by -,19,EXTENSION;
 235 //
 236   now [22]
 237     let a be A; assume a IN H [23];
 238     let b be A; assume b IN H [24];
 239     i(a)**b IN H [25] by 2,23,24;
 240     assume i(a)**b IN G [26];
 241     b***G = e**b***G by 2,24;
 242       .= a**i(a)**b***G by -,2,23;
 243       .= a**(i(a)**b)***G by -,2,23,24;
 244       .= a***(i(a)**b***G) by -,9,23,25;
 245     thus .= a***G by -,17,26;
 246   end;
 247   !a b. a IN H /\ b IN H /\ ~(a***G = b***G) ==> a***G INTER b***G = {} [27]
 248   proof
 249     let a be A; assume a IN H [28];
 250     let b be A; assume b IN H [29];
 251     now assume ~(a***G INTER b***G = {});
 252       consider x such that x IN a***G INTER b***G by -,MEMBER_NOT_EMPTY;
 253       x IN a***G /\ x IN b***G [30] by -,IN_INTER;
 254       consider g1 such that g1 IN G /\ x = a**g1 [31] by 8,30;
 255       consider g2 such that g2 IN G /\ x = b**g2 [32] by 8,30;
 256       g1 IN H /\ g2 IN H [33] by 4,31,32;
 257       a**g1 = b**g2 [34] by 31,32;
 258       g1**i(g2) = e**g1**i(g2) by 2,33;
 259         .= (i(a)**a)**g1**i(g2) by -,2,28;
 260         .= i(a)**(a**g1)**i(g2) by -,2,28,33;
 261         .= i(a)**(b**g2)**i(g2) by -,34;
 262         .= i(a)**(b**g2**i(g2)) by -,2,28,29,33;
 263         .= i(a)**(b**(g2**i(g2))) by -,2,29,33;
 264         .= i(a)**(b**e) by -,2,33;
 265         .= i(a)**b by -,2,29;
 266       i(a)**b IN G by -,6,31,32;
 267       thus a***G = b***G by -,22,28,29;
 268     end;
 269   qed by -,28,29;
 270   !a. a IN H ==> a IN a***G [35]
 271   proof
 272     let a be A; assume a IN H;
 273     a**e = a by -,2;
 274   qed by -,6,8;
 275   now
 276     now [36]
 277       let x be A;
 278       assume x IN UNIONS {a***G | a IN H};
 279       consider s such that s IN {a***G | a IN H} /\ x IN s [37]
 280         by -,IN_UNIONS;
 281       consider a such that a IN H /\ s = a***G [38] by -;
 282       consider g such that g IN G /\ x = a**g by -,8,37;
 283       thus x IN H by -,2,4,38;
 284     end;
 285     now
 286       let x be A;
 287       assume x IN H;
 288       x IN x***G /\ x***G IN {a***G | a IN H} by -,35;
 289       thus x IN UNIONS {a***G | a IN H} by -,IN_UNIONS;
 290     end;
 291     thus UNIONS {a***G | a IN H} = H by -,36,EXTENSION;
 292     let t u be A->bool;
 293     assume t IN {a***G | a IN H} /\ u IN {a***G | a IN H} /\ ~(t = u) [39];
 294     consider a b such that a IN H /\ t = a***G /\ b IN H /\ t = b***G by -;
 295     thus t INTER u = {} by -,27,39;
 296   end;
 297   {a***G | a IN H} PARTITIONS H [40] by REWRITE_TAC,-,PARTITIONS;
 298   !a b. a IN H /\ b IN H ==> CARD (a***G) = CARD (b***G) [41]
 299   proof
 300     let a be A; assume a IN H [42];
 301     let b be A; assume b IN H [43];
 302     set f = \x. b**(i(a)**x);
 303     set f' = \x. a**(i(b)**x);
 304     !g. g IN G ==> f(a**g) = b**g /\ f'(b**g) = a**g [44]
 305     proof
 306       let g be A; assume g IN G;
 307       g IN H [45] by -,4;
 308       f(a**g) = b**(i(a)**(a**g));
 309         .= b**(i(a)**a**g) by -,2,42,45;
 310         .= b**(e**g) by -,2,42;
 311         .= b**g [46] by -,2,45;
 312       f'(b**g) = a**(i(b)**(b**g));
 313         .= a**(i(b)**b**g) by -,2,43,45;
 314         .= a**(e**g) by -,2,43;
 315         .= a**g by -,2,45;
 316     qed by -,46;
 317     now
 318       take f';
 319       thus !x. x IN a***G ==> f x IN b***G /\ f' (f x) = x
 320       proof
 321         let x be A; assume x IN a***G;
 322         consider g such that g IN G /\ x = a**g [47] by -,8;
 323         f x = b**g by -,44;
 324       qed by -,8,44,47;
 325       thus !y. y IN b***G ==> f' y IN a***G /\ f (f' y) = y
 326       proof
 327         let y be A; assume y IN b***G;
 328         consider g such that g IN G /\ y = b**g [48] by -,8;
 329         f' y = a**g by -,44;
 330       qed by -,8,44,48;
 331     end;
 332     bijection f (a***G) (b***G) [49] by ALL_TAC,-,bijection;
 333     FINITE {a**g | g IN G} by SIMP_TAC,5,SIMPLE_IMAGE,FINITE_IMAGE;
 334   qed by -,7,49,BIJECTION_CARD_EQ;
 335   set INDEX = CARD {a***G | a IN H};
 336   now
 337     let t be A->bool;
 338     assume t IN {a***G | a IN H};
 339     consider a such that a IN H /\ t = a***G [50] by -;
 340     CARD t = CARD (a***G) by -;
 341       .= CARD (e***G) by -,2,41,50;
 342     thus .= CARD G by -,6,17;
 343   end;
 344   set N = CARD H;
 345   set n = CARD G;
 346   set j = INDEX;
 347   N = (CARD {a***G | a IN H})*(CARD G) by -,1,40,CARD_UNIONS_EQUAL;
 348     .= j*n by -;
 349   thus CARD G divides CARD H by -,divides,MULT_SYM;
 350 //
 351 `;;
 352
 353 parse_as_infix("**",(20,"right"));;