miz3/Samples/other_mizs.ml

   1 (* ======== Examples/mizar.ml ============================================== *)
   2
   3 hide_constant "<=";;
   4
   5 horizon := 0;;
   6
   7 let KNASTER_TARSKI = thm `;
   8   let (<=) be A->A->bool;
   9   thus !f. (!x y. x <= y /\ y <= x ==> (x = y)) /\
  10       (!x y z. x <= y /\ y <= z ==> x <= z) /\
  11       (!x y. x <= y ==> f x <= f y) /\
  12       (!X. ?s. (!x. x IN X ==> s <= x) /\
  13                  (!s'. (!x. x IN X ==> s' <= x) ==> s' <= s))
  14       ==> ?x. f x = x
  15   proof
  16     let f be A->A;
  17     exec DISCH_THEN (LABEL_TAC "L");
  18     !x y. x <= y /\ y <= x ==> (x = y) [antisymmetry] by L;
  19     !x y z. x <= y /\ y <= z ==> x <= z [transitivity] by L;
  20     !x y. x <= y ==> f x <= f y [monotonicity] by L;
  21     !X. ?s:A. (!x. x IN X ==> s <= x) /\
  22               (!s'. (!x. x IN X ==> s' <= x) ==> s' <= s) [least_upper_bound]
  23       by L;
  24     set Y = {b | f b <= b} [Y_def];
  25     !b. b IN Y <=> f b <= b [Y_thm] by ALL_TAC,Y_def,IN_ELIM_THM,BETA_THM;
  26     consider a such that
  27       (!x. x IN Y ==> a <= x) /\
  28       (!a'. (!x. x IN Y ==> a' <= x) ==> a' <= a) [lub] by least_upper_bound;
  29     take a;
  30     !b. b IN Y ==> f a <= b
  31     proof
  32       let b be A;
  33       assume b IN Y [b_in_Y];
  34       f b <= b [L0] by -,Y_thm;
  35       a <= b by b_in_Y,lub;
  36       f a <= f b by -,monotonicity;
  37       thus f a <= b by -,L0,transitivity;
  38     end;
  39     f(a) <= a [Part1] by -,lub;
  40     f(f(a)) <= f(a) by -,monotonicity;
  41     f(a) IN Y by -,Y_thm;
  42     a <= f(a) by -,lub;
  43   qed by -,Part1,antisymmetry`;;
  44
  45 unhide_constant "<=";;
  46
  47 (* ======== Mizarlight/duality.ml ========================================== *)
  48
  49 parse_as_infix("ON",(11,"right"));;
  50
  51 hide_constant "ON";;
  52
  53 let projective = new_definition
  54  `projective((ON):Point->Line->bool) <=>
  55         (!p p'. ~(p = p') ==> ?!l. p ON l /\ p' ON l) /\
  56         (!l l'. ?p. p ON l /\ p ON l') /\
  57         (?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
  58                     ~(?l. p ON l /\ p' ON l /\ p'' ON l)) /\
  59         (!l. ?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
  60                         p ON l /\ p' ON l /\ p'' ON l)`;;
  61
  62 horizon := 1;;
  63
  64 let LEMMA_1 = thm `;
  65   !(ON):Point->Line->bool. projective(ON) ==> !p. ?l. p ON l
  66 proof
  67   let (ON) be Point->Line->bool;
  68   assume projective(ON) [0];
  69   !p p'. ~(p = p') ==> ?!l. p ON l /\ p' ON l [1] by 0,projective;
  70   ?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
  71              ~(?l. p ON l /\ p' ON l /\ p'' ON l) [3] by 0,projective;
  72   let p be Point;
  73   consider q q' such that ~(q = q':Point);
  74   ~(p = q) \/ ~(p = q');
  75   consider l such that p ON l by 1;
  76   take l;
  77 qed`;;
  78
  79 let LEMMA_2 = thm `;
  80   !(ON):Point->Line->bool. projective(ON)
  81    ==> !p1 p2 q l l1 l2.
  82      p1 ON l /\ p2 ON l /\ p1 ON l1 /\ p2 ON l2 /\ q ON l2 /\
  83      ~(q ON l) /\ ~(p1 = p2) ==> ~(l1 = l2)
  84 proof
  85   let (ON) be Point->Line->bool;
  86   assume projective(ON) [0];
  87   !p p'. ~(p = p') ==> ?!l. p ON l /\ p' ON l [1] by 0,projective;
  88 // here qed already works
  89   let p1 p2 q be Point;
  90   let l l1 l2 be Line;
  91   assume p1 ON l [5];
  92   assume p2 ON l [6];
  93   assume p1 ON l1 [7];
  94   assume p2 ON l2 [9];
  95   assume q ON l2 [10];
  96   assume ~(q ON l) [11];
  97   assume ~(p1 = p2) [12];
  98   assume l1 = l2 [13];
  99   p1 ON l2 by 7;
 100   l = l2 by 1,5,6,9,12;
 101   thus F by 10,11;
 102 end`;;
 103
 104 let PROJECTIVE_DUALITY = thm `;
 105   !(ON):Point->Line->bool. projective(ON) ==> projective (\l p. p ON l)
 106 proof
 107   let (ON) be Point->Line->bool;
 108   assume projective(ON) [0];
 109   !p p'. ~(p = p') ==> ?!l. p ON l /\ p' ON l [1] by 0,projective;
 110   !l l'. ?p. p ON l /\ p ON l' [2] by 0,projective;
 111   ?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
 112              ~(?l. p ON l /\ p' ON l /\ p'' ON l) [3] by 0,projective;
 113   !l. ?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
 114                  p ON l /\ p' ON l /\ p'' ON l [4] by 0,projective;
 115 // dual of axiom 1
 116   !l1 l2. ~(l1 = l2) ==> ?!p. p ON l1 /\ p ON l2 [5]
 117   proof
 118     let l1 l2 be Line;
 119     assume ~(l1 = l2) [6];
 120     consider p such that p ON l1 /\ p ON l2 [7] by 2;
 121     !p'. p' ON l1 /\ p' ON l2 ==> (p' = p)
 122     proof
 123       let p' be Point;
 124       assume p' ON l1 /\ p' ON l2 [8];
 125       assume ~(p' = p);
 126       l1 = l2 by 1,7,8;
 127       thus F by 6;
 128     end;
 129   qed by 7;
 130 // dual of axiom 2
 131   !p1 p2. ?l. p1 ON l /\ p2 ON l [9]
 132   proof
 133     let p1 p2 be Point;
 134     cases;
 135     suppose p1 = p2;
 136     qed by 0,LEMMA_1;
 137     suppose ~(p1 = p2);
 138     qed by 1;
 139   end;
 140 // dual of axiom 3
 141   ?l1 l2 l3. ~(l1 = l2) /\ ~(l2 = l3) /\ ~(l1 = l3) /\
 142              ~(?p. p ON l1 /\ p ON l2 /\ p ON l3) [10]
 143   proof
 144     consider p1 p2 p3 such that
 145       ~(p1 = p2) /\ ~(p2 = p3) /\ ~(p1 = p3) /\
 146       ~(?l. p1 ON l /\ p2 ON l /\ p3 ON l) [11] by 3;
 147     ~(p1 = p3) by 11;
 148     ?!l1. p1 ON l1 /\ p3 ON l1 by 1;  // ADDED STEP
 149     consider l1 such that p1 ON l1 /\ p3 ON l1 /\
 150       !l'. p1 ON l' /\ p3 ON l' ==> (l1 = l') [12];
 151     ~(p2 = p3) by 11;
 152     ?!l2. p2 ON l2 /\ p3 ON l2 by 1;  // ADDED STEP
 153     consider l2 such that p2 ON l2 /\ p3 ON l2 /\
 154       !l'. p2 ON l' /\ p3 ON l' ==> (l2 = l') [13];
 155     ~(p1 = p2) by 11;
 156     ?!l3. p1 ON l3 /\ p2 ON l3 by 1;  // ADDED STEP
 157     consider l3 such that p1 ON l3 /\ p2 ON l3 /\
 158       !l'. p1 ON l' /\ p2 ON l' ==> (l3 = l') [14];
 159     take l1; take l2; take l3;
 160     thus ~(l1 = l2) /\ ~(l2 = l3) /\ ~(l1 = l3) [15] by 11,12,13,14;
 161     assume ?q. q ON l1 /\ q ON l2 /\ q ON l3;
 162     consider q such that q ON l1 /\ q ON l2 /\ q ON l3;
 163     (p1 = q) /\ (p2 = q) /\ (p3 = q) by 5,12,13,14,15;
 164     thus F by 11;
 165   end;
 166 // dual of axiom 4
 167   !p0. ?l0 L1 L2. ~(l0 = L1) /\ ~(L1 = L2) /\ ~(l0 = L2) /\
 168                   p0 ON l0 /\ p0 ON L1 /\ p0 ON L2
 169   proof
 170     let p0 be Point;
 171     consider l0 such that p0 ON l0 [16] by 0,LEMMA_1;
 172     consider p such that ~(p = p0) /\ p ON l0 [17] by 4;
 173     consider q such that ~(q ON l0) [18] by 3;
 174     consider l1 such that p ON l1 /\ q ON l1 [19] by 1,16;
 175     consider r such that r ON l1 /\ ~(r = p) /\ ~(r = q) [20]
 176     proof
 177       consider r1 r2 r3 such that
 178         ~(r1 = r2) /\ ~(r2 = r3) /\ ~(r1 = r3) /\
 179        r1 ON l1 /\ r2 ON l1 /\ r3 ON l1 [21] by 4;
 180       ~(r1 = p) /\ ~(r1 = q) \/
 181       ~(r2 = p) /\ ~(r2 = q) \/
 182       ~(r3 = p) /\ ~(r3 = q);
 183     qed by 21;
 184     ~(p0 ON l1) [22]
 185     proof
 186       assume p0 ON l1;
 187       l1 = l0 by 1,16,17,19;
 188     qed by 18,19;
 189     ~(p0 = r) by 20;
 190     consider L1 such that r ON L1 /\ p0 ON L1 [23] by 1;
 191     consider L2 such that q ON L2 /\ p0 ON L2 [24] by 1,16,18;
 192     take l0; take L1; take L2;
 193     thus ~(l0 = L1) by 0,17,19,20,22,23,LEMMA_2;
 194     thus ~(L1 = L2) by 0,19,20,22,23,24,LEMMA_2;
 195     thus ~(l0 = L2) by 18,24;
 196     thus p0 ON l0 /\ p0 ON L2 /\ p0 ON L1 by 16,24,23;
 197   end;
 198 qed by REWRITE_TAC,5,9,10,projective`;;
 199
 200 unhide_constant "ON";;
 201
 202 (* ======== Mizarlight/duality_holby.ml ==================================== *)
 203
 204 horizon := 1;;
 205
 206 let Line_INDUCT,Line_RECURSION = define_type
 207  "fano_Line = Line_1 | Line_2 | Line_3 | Line_4 |
 208               Line_5 | Line_6 | Line_7";;
 209
 210 let Point_INDUCT,Point_RECURSION = define_type
 211  "fano_Point = Point_1 | Point_2 | Point_3 | Point_4 |
 212                Point_5 | Point_6 | Point_7";;
 213
 214 let Point_DISTINCT = distinctness "fano_Point";;
 215
 216 let Line_DISTINCT = distinctness "fano_Line";;
 217
 218 let fano_incidence =
 219   [1,1; 1,2; 1,3; 2,1; 2,4; 2,5; 3,1; 3,6; 3,7; 4,2; 4,4;
 220    4,6; 5,2; 5,5; 5,7; 6,3; 6,4; 6,7; 7,3; 7,5; 7,6];;
 221
 222 let fano_point i = mk_const("Point_"^string_of_int i,[])
 223 and fano_line i = mk_const("Line_"^string_of_int i,[]);;
 224
 225 let fano_clause (i,j) =
 226   let p = `p:fano_Point` and l = `l:fano_Line` in
 227   mk_conj(mk_eq(p,fano_point i),mk_eq(l,fano_line j));;
 228
 229 let ON = new_definition
 230  (mk_eq(`((ON):fano_Point->fano_Line->bool) p l`,
 231         list_mk_disj(map fano_clause fano_incidence)));;
 232
 233 let ON_CLAUSES = prove
 234  (list_mk_conj(allpairs
 235     (fun i j -> mk_eq(list_mk_comb(`(ON)`,[fano_point i; fano_line j]),
 236                       if mem (i,j) fano_incidence then `T` else `F`))
 237     (1--7) (1--7)),
 238   REWRITE_TAC[ON; Line_DISTINCT; Point_DISTINCT]);;
 239
 240 let FORALL_POINT = thm `;
 241   !P. (!p. P p) <=> P Point_1 /\ P Point_2 /\ P Point_3 /\ P Point_4 /\
 242                     P Point_5 /\ P Point_6 /\ P Point_7
 243     by Point_INDUCT`;;
 244
 245 let EXISTS_POINT = thm `;
 246   !P. (?p. P p) <=> P Point_1 \/ P Point_2 \/ P Point_3 \/ P Point_4 \/
 247                     P Point_5 \/ P Point_6 \/ P Point_7
 248 proof
 249   let P be fano_Point->bool;
 250   ~(?p. P p) <=> ~(P Point_1 \/ P Point_2 \/ P Point_3 \/ P Point_4 \/
 251                    P Point_5 \/ P Point_6 \/ P Point_7)
 252     by REWRITE_TAC,DE_MORGAN_THM,NOT_EXISTS_THM,FORALL_POINT;
 253 qed`;;
 254
 255 let FORALL_LINE = thm `;
 256   !P. (!p. P p) <=> P Line_1 /\ P Line_2 /\ P Line_3 /\ P Line_4 /\
 257                     P Line_5 /\ P Line_6 /\ P Line_7
 258     by Line_INDUCT`;;
 259
 260 let EXISTS_LINE = thm `;
 261   !P. (?p. P p) <=> P Line_1 \/ P Line_2 \/ P Line_3 \/ P Line_4 \/
 262                     P Line_5 \/ P Line_6 \/ P Line_7
 263 proof
 264   let P be fano_Line->bool;
 265   ~(?p. P p) <=> ~(P Line_1 \/ P Line_2 \/ P Line_3 \/ P Line_4 \/
 266                    P Line_5 \/ P Line_6 \/ P Line_7)
 267     by REWRITE_TAC,DE_MORGAN_THM,NOT_EXISTS_THM,FORALL_LINE;
 268 qed;`;;
 269
 270 let FANO_TAC =
 271   GEN_REWRITE_TAC DEPTH_CONV
 272    [FORALL_POINT; EXISTS_LINE; EXISTS_POINT; FORALL_LINE] THEN
 273   GEN_REWRITE_TAC DEPTH_CONV
 274    (basic_rewrites() @ [ON_CLAUSES; Point_DISTINCT; Line_DISTINCT]);;
 275
 276 let AXIOM_1 = thm `;
 277   !p p'. ~(p = p') ==> ?l. p ON l /\ p' ON l /\
 278                            !l'. p ON l' /\ p' ON l' ==> (l' = l)
 279     by TIMED_TAC 3 FANO_TAC`;;
 280
 281 let AXIOM_2 = thm `;
 282   !l l'. ?p. p ON l /\ p ON l' by FANO_TAC`;;
 283
 284 let AXIOM_3 = thm `;
 285   ?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
 286              ~(?l. p ON l /\ p' ON l /\ p'' ON l)
 287     by TIMED_TAC 2 FANO_TAC`;;
 288
 289 let AXIOM_4 = thm `;
 290   !l. ?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
 291                  p ON l /\ p' ON l /\ p'' ON l
 292     by TIMED_TAC 3 FANO_TAC`;;
 293
 294 let AXIOM_1' = thm `;
 295   !p p' l l'. ~(p = p') /\ p ON l /\ p' ON l /\ p ON l' /\ p' ON l'
 296               ==> (l' = l)
 297 proof
 298   let p p' be fano_Point;
 299   let l l' be fano_Line;
 300   assume ~(p = p') /\ p ON l /\ p' ON l /\ p ON l' /\ p' ON l' [1];
 301   consider l1 such that p ON l1 /\ p' ON l1 /\
 302                         !l'. p ON l' /\ p' ON l' ==> (l' = l1) [2]
 303     by 1,AXIOM_1;
 304   l = l1 by 1,2;
 305     .= l' by 1,2;
 306 qed`;;
 307
 308 let LEMMA_1' = thm `;
 309   !O. ?l. O ON l
 310 proof
 311   consider p p' p'' such that
 312     ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
 313     ~(?l. p ON l /\ p' ON l /\ p'' ON l) [1] by AXIOM_3;
 314   let O be fano_Point;
 315   ~(p = O) \/ ~(p' = O) by 1;
 316   consider P such that ~(P = O) [2];
 317   consider l such that O ON l /\ P ON l /\
 318     !l'. O ON l' /\ P ON l' ==> (l' = l) [3] by 2,AXIOM_1;
 319   thus ?l. O ON l by 3;
 320 end`;;
 321
 322 let DUAL_1 = thm `;
 323   !l l'. ~(l = l') ==> ?p. p ON l /\ p ON l' /\
 324          !p'. p' ON l /\ p' ON l' ==> (p' = p)
 325 proof
 326   assume ~thesis;
 327   consider l l' such that ~(l = l') /\ !p. p ON l /\ p ON l'
 328                           ==> ?p'. p' ON l /\ p' ON l' /\ ~(p' = p) [1];
 329   consider p such that p ON l /\ p ON l' [2] by AXIOM_2;
 330   consider p' such that p' ON l /\ p' ON l' /\ ~(p' = p) [3] by 1,2;
 331   thus F by 1,2,AXIOM_1';
 332 end`;;
 333
 334 let DUAL_2 = thm `;
 335   !p p'. ?l. p ON l /\ p' ON l
 336 proof
 337   let p p' be fano_Point;
 338   ?l. p ON l [1] by LEMMA_1';
 339   (p = p') \/
 340     ?l. p ON l /\ p' ON l /\
 341         !l'. p ON l' /\ p' ON l' ==> (l' = l) by AXIOM_1;
 342 qed by 1`;;
 343
 344 let DUAL_3 = thm `;
 345   ?l1 l2 l3. ~(l1 = l2) /\ ~(l2 = l3) /\ ~(l1 = l3) /\
 346              ~(?p. p ON l1 /\ p ON l2 /\ p ON l3)
 347 proof
 348   consider p1 p2 p3 such that
 349     ~(p1 = p2) /\ ~(p2 = p3) /\ ~(p1 = p3) /\
 350     ~(?l. p1 ON l /\ p2 ON l /\ p3 ON l) [1] by AXIOM_3;
 351   consider l1 such that p1 ON l1 /\ p3 ON l1 [2] by DUAL_2;
 352   consider l2 such that p2 ON l2 /\ p3 ON l2 [3] by DUAL_2;
 353   consider l3 such that p1 ON l3 /\ p2 ON l3 [4] by DUAL_2;
 354   take l1; take l2; take l3;
 355   thus ~(l1 = l2) /\ ~(l2 = l3) /\ ~(l1 = l3) [5] by 1,2,3,4;
 356   assume ~thesis;
 357   consider q such that q ON l1 /\ q ON l2 /\ q ON l3 [6];
 358   consider q' such that q' ON l1 /\ q' ON l3 /\
 359     !p'. p' ON l1 /\ p' ON l3 ==> (p' = q') [7] by 5,DUAL_1;
 360   q = q' by 6,7;
 361     .= p1 by 2,4,7;
 362   thus F by 1,3,6;
 363 end`;;
 364
 365 let DUAL_4 = thm `;
 366   !O. ?OP OQ OR. ~(OP = OQ) /\ ~(OQ = OR) /\ ~(OP = OR) /\
 367                  O ON OP /\ O ON OQ /\ O ON OR
 368 proof
 369   let O be fano_Point;
 370   consider OP such that O ON OP [1] by LEMMA_1';
 371   consider p p' p'' such that
 372     ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
 373     p ON OP /\ p' ON OP /\ p'' ON OP [2] by AXIOM_4;
 374   ~(p = O) \/ ~(p' = O) by 2;
 375   consider P such that ~(P = O) /\ P ON OP [3] by 2;
 376   consider q q' q'' such that
 377     ~(q = q') /\ ~(q' = q'') /\ ~(q = q'') /\
 378     ~(?l. q ON l /\ q' ON l /\ q'' ON l) [4] by AXIOM_3;
 379   ~(q ON OP) \/ ~(q' ON OP) \/ ~(q'' ON OP) by 4;
 380   consider Q such that ~(Q ON OP) [5];
 381   consider l such that P ON l /\ Q ON l [6] by DUAL_2;
 382   consider r r' r'' such that
 383   ~(r = r') /\ ~(r' = r'') /\ ~(r = r'') /\
 384   r ON l /\ r' ON l /\ r'' ON l [7] by AXIOM_4;
 385   ((r = P) \/ (r = Q) \/ ~(r = P) /\ ~(r = Q)) /\
 386   ((r' = P) \/ (r' = Q) \/ ~(r' = P) /\ ~(r' = Q));
 387   consider R such that R ON l /\ ~(R = P) /\ ~(R = Q) [8] by 7;
 388   consider OQ such that O ON OQ /\ Q ON OQ [9] by DUAL_2;
 389   consider OR such that O ON OR /\ R ON OR [10] by DUAL_2;
 390   take OP; take OQ; take OR;
 391   ~(O ON l) by 1,3,5,6,AXIOM_1';
 392   thus ~(OP = OQ) /\ ~(OQ = OR) /\ ~(OP = OR) /\
 393        O ON OP /\ O ON OQ /\ O ON OR by 1,3,5,6,8,9,10,AXIOM_1';
 394 end`;;
 395
 396 (* ======== Tutorial/Changing_proof_style.ml =============================== *)
 397
 398 horizon := 1;;
 399
 400 let NSQRT_2_4 = thm `;
 401   !p q. p * p = 2 * q * q ==> q = 0
 402 proof
 403   !p. (!m. m < p ==> (!q. m * m = 2 * q * q ==> q = 0))
 404       ==> (!q. p * p = 2 * q * q ==> q = 0)
 405   proof
 406     let p be num;
 407     assume !m. m < p ==> !q. m * m = 2 * q * q ==> q = 0 [A];
 408     let q be num;
 409     assume p * p = 2 * q * q [B];
 410     EVEN(p * p) <=> EVEN(2 * q * q);
 411     EVEN(p) by TIMED_TAC 2 o MESON_TAC,ARITH,EVEN_MULT;
 412 //  "EVEN 2 by CONV_TAC o HOL_BY,ARITH;" takes over a minute...
 413     consider m such that p = 2 * m [C] by EVEN_EXISTS;
 414     cases by ARITH_TAC;
 415     suppose q < p;
 416       q * q = 2 * m * m ==> m = 0 by A;
 417     qed by NUM_RING,B,C;
 418     suppose p <= q;
 419       p * p <= q * q by LE_MULT2;
 420       q * q = 0 by ARITH_TAC,B;
 421     qed by NUM_RING;
 422   end;
 423 qed by MATCH_MP_TAC,num_WF`;;
 424