(* ======== Examples/mizar.ml ============================================== *)

hide_constant "<=";;

horizon := 0;;

let KNASTER_TARSKI = thm `;
  let (<=) be A->A->bool;
  thus !f. (!x y. x <= y /\ y <= x ==> (x = y)) /\
      (!x y z. x <= y /\ y <= z ==> x <= z) /\
      (!x y. x <= y ==> f x <= f y) /\
      (!X. ?s. (!x. x IN X ==> s <= x) /\
                 (!s'. (!x. x IN X ==> s' <= x) ==> s' <= s))
      ==> ?x. f x = x
  proof
    let f be A->A;
    exec DISCH_THEN (LABEL_TAC "L");
    !x y. x <= y /\ y <= x ==> (x = y) [antisymmetry] by L;
    !x y z. x <= y /\ y <= z ==> x <= z [transitivity] by L;
    !x y. x <= y ==> f x <= f y [monotonicity] by L;
    !X. ?s:A. (!x. x IN X ==> s <= x) /\
              (!s'. (!x. x IN X ==> s' <= x) ==> s' <= s) [least_upper_bound]
      by L;
    set Y = {b | f b <= b} [Y_def];
    !b. b IN Y <=> f b <= b [Y_thm] by ALL_TAC,Y_def,IN_ELIM_THM,BETA_THM;
    consider a such that
      (!x. x IN Y ==> a <= x) /\
      (!a'. (!x. x IN Y ==> a' <= x) ==> a' <= a) [lub] by least_upper_bound;
    take a;
    !b. b IN Y ==> f a <= b
    proof
      let b be A;
      assume b IN Y [b_in_Y];
      f b <= b [L0] by -,Y_thm;
      a <= b by b_in_Y,lub;
      f a <= f b by -,monotonicity;
      thus f a <= b by -,L0,transitivity;
    end;
    f(a) <= a [Part1] by -,lub;
    f(f(a)) <= f(a) by -,monotonicity;
    f(a) IN Y by -,Y_thm;
    a <= f(a) by -,lub;
  qed by -,Part1,antisymmetry`;;

unhide_constant "<=";;

(* ======== Mizarlight/duality.ml ========================================== *)

parse_as_infix("ON",(11,"right"));;

hide_constant "ON";;

let projective = new_definition
 `projective((ON):Point->Line->bool) <=>
        (!p p'. ~(p = p') ==> ?!l. p ON l /\ p' ON l) /\
        (!l l'. ?p. p ON l /\ p ON l') /\
        (?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
                    ~(?l. p ON l /\ p' ON l /\ p'' ON l)) /\
        (!l. ?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
                        p ON l /\ p' ON l /\ p'' ON l)`;;
horizon := 1;; let LEMMA_1 = thm `; !(ON):Point->Line->bool. projective(ON) ==> !p. ?l. p ON l proof let (ON) be Point->Line->bool; assume projective(ON) [0]; !p p'. ~(p = p') ==> ?!l. p ON l /\ p' ON l [1] by 0,projective; ?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\ ~(?l. p ON l /\ p' ON l /\ p'' ON l) [3] by 0,projective; let p be Point; consider q q' such that ~(q = q':Point); ~(p = q) \/ ~(p = q'); consider l such that p ON l by 1; take l; qed`;; let LEMMA_2 = thm `; !(ON):Point->Line->bool. projective(ON) ==> !p1 p2 q l l1 l2. p1 ON l /\ p2 ON l /\ p1 ON l1 /\ p2 ON l2 /\ q ON l2 /\ ~(q ON l) /\ ~(p1 = p2) ==> ~(l1 = l2) proof let (ON) be Point->Line->bool; assume projective(ON) [0]; !p p'. ~(p = p') ==> ?!l. p ON l /\ p' ON l [1] by 0,projective; // here qed already works let p1 p2 q be Point; let l l1 l2 be Line; assume p1 ON l [5]; assume p2 ON l [6]; assume p1 ON l1 [7]; assume p2 ON l2 [9]; assume q ON l2 [10]; assume ~(q ON l) [11]; assume ~(p1 = p2) [12]; assume l1 = l2 [13]; p1 ON l2 by 7; l = l2 by 1,5,6,9,12; thus F by 10,11; end`;; let PROJECTIVE_DUALITY = thm `; !(ON):Point->Line->bool. projective(ON) ==> projective (\l p. p ON l) proof let (ON) be Point->Line->bool; assume projective(ON) [0]; !p p'. ~(p = p') ==> ?!l. p ON l /\ p' ON l [1] by 0,projective; !l l'. ?p. p ON l /\ p ON l' [2] by 0,projective; ?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\ ~(?l. p ON l /\ p' ON l /\ p'' ON l) [3] by 0,projective; !l. ?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\ p ON l /\ p' ON l /\ p'' ON l [4] by 0,projective; // dual of axiom 1 !l1 l2. ~(l1 = l2) ==> ?!p. p ON l1 /\ p ON l2 [5] proof let l1 l2 be Line; assume ~(l1 = l2) [6]; consider p such that p ON l1 /\ p ON l2 [7] by 2; !p'. p' ON l1 /\ p' ON l2 ==> (p' = p) proof let p' be Point; assume p' ON l1 /\ p' ON l2 [8]; assume ~(p' = p); l1 = l2 by 1,7,8; thus F by 6; end; qed by 7; // dual of axiom 2 !p1 p2. ?l. p1 ON l /\ p2 ON l [9] proof let p1 p2 be Point; cases; suppose p1 = p2; qed by 0,LEMMA_1; suppose ~(p1 = p2); qed by 1; end; // dual of axiom 3 ?l1 l2 l3. ~(l1 = l2) /\ ~(l2 = l3) /\ ~(l1 = l3) /\ ~(?p. p ON l1 /\ p ON l2 /\ p ON l3) [10] proof consider p1 p2 p3 such that ~(p1 = p2) /\ ~(p2 = p3) /\ ~(p1 = p3) /\ ~(?l. p1 ON l /\ p2 ON l /\ p3 ON l) [11] by 3; ~(p1 = p3) by 11; ?!l1. p1 ON l1 /\ p3 ON l1 by 1; // ADDED STEP consider l1 such that p1 ON l1 /\ p3 ON l1 /\ !l'. p1 ON l' /\ p3 ON l' ==> (l1 = l') [12]; ~(p2 = p3) by 11; ?!l2. p2 ON l2 /\ p3 ON l2 by 1; // ADDED STEP consider l2 such that p2 ON l2 /\ p3 ON l2 /\ !l'. p2 ON l' /\ p3 ON l' ==> (l2 = l') [13]; ~(p1 = p2) by 11; ?!l3. p1 ON l3 /\ p2 ON l3 by 1; // ADDED STEP consider l3 such that p1 ON l3 /\ p2 ON l3 /\ !l'. p1 ON l' /\ p2 ON l' ==> (l3 = l') [14]; take l1; take l2; take l3; thus ~(l1 = l2) /\ ~(l2 = l3) /\ ~(l1 = l3) [15] by 11,12,13,14; assume ?q. q ON l1 /\ q ON l2 /\ q ON l3; consider q such that q ON l1 /\ q ON l2 /\ q ON l3; (p1 = q) /\ (p2 = q) /\ (p3 = q) by 5,12,13,14,15; thus F by 11; end; // dual of axiom 4 !p0. ?l0 L1 L2. ~(l0 = L1) /\ ~(L1 = L2) /\ ~(l0 = L2) /\ p0 ON l0 /\ p0 ON L1 /\ p0 ON L2 proof let p0 be Point; consider l0 such that p0 ON l0 [16] by 0,LEMMA_1; consider p such that ~(p = p0) /\ p ON l0 [17] by 4; consider q such that ~(q ON l0) [18] by 3; consider l1 such that p ON l1 /\ q ON l1 [19] by 1,16; consider r such that r ON l1 /\ ~(r = p) /\ ~(r = q) [20] proof consider r1 r2 r3 such that ~(r1 = r2) /\ ~(r2 = r3) /\ ~(r1 = r3) /\ r1 ON l1 /\ r2 ON l1 /\ r3 ON l1 [21] by 4; ~(r1 = p) /\ ~(r1 = q) \/ ~(r2 = p) /\ ~(r2 = q) \/ ~(r3 = p) /\ ~(r3 = q); qed by 21; ~(p0 ON l1) [22] proof assume p0 ON l1; l1 = l0 by 1,16,17,19; qed by 18,19; ~(p0 = r) by 20; consider L1 such that r ON L1 /\ p0 ON L1 [23] by 1; consider L2 such that q ON L2 /\ p0 ON L2 [24] by 1,16,18; take l0; take L1; take L2; thus ~(l0 = L1) by 0,17,19,20,22,23,LEMMA_2; thus ~(L1 = L2) by 0,19,20,22,23,24,LEMMA_2; thus ~(l0 = L2) by 18,24; thus p0 ON l0 /\ p0 ON L2 /\ p0 ON L1 by 16,24,23; end; qed by REWRITE_TAC,5,9,10,projective`;; unhide_constant "ON";; (* ======== Mizarlight/duality_holby.ml ==================================== *) horizon := 1;;
let Line_INDUCT,Line_RECURSION = define_type
 "fano_Line = Line_1 | Line_2 | Line_3 | Line_4 |
              Line_5 | Line_6 | Line_7";
;
let Point_INDUCT,Point_RECURSION = define_type
 "fano_Point = Point_1 | Point_2 | Point_3 | Point_4 |
               Point_5 | Point_6 | Point_7";
; let Point_DISTINCT = distinctness "fano_Point";; let Line_DISTINCT = distinctness "fano_Line";; let fano_incidence = [1,1; 1,2; 1,3; 2,1; 2,4; 2,5; 3,1; 3,6; 3,7; 4,2; 4,4; 4,6; 5,2; 5,5; 5,7; 6,3; 6,4; 6,7; 7,3; 7,5; 7,6];; let fano_point i = mk_const("Point_"^string_of_int i,[]) and fano_line i = mk_const("Line_"^string_of_int i,[]);; let fano_clause (i,j) = let p = `p:fano_Point` and l = `l:fano_Line` in mk_conj(mk_eq(p,fano_point i),mk_eq(l,fano_line j));;
let ON = new_definition
 (mk_eq(`((ON):fano_Point->fano_Line->bool) p l`,
        list_mk_disj(map fano_clause fano_incidence)));;
let ON_CLAUSES = prove
 (list_mk_conj(allpairs
    (fun i j -> mk_eq(list_mk_comb(`(ON)`,[fano_point i; fano_line j]),
                      if mem (i,j) fano_incidence then `T` else `F`))
    (1--7) (1--7)),
  REWRITE_TAC[ON; Line_DISTINCT; Point_DISTINCT]);;
let FORALL_POINT = thm `; !P. (!p. P p) <=> P Point_1 /\ P Point_2 /\ P Point_3 /\ P Point_4 /\ P Point_5 /\ P Point_6 /\ P Point_7 by Point_INDUCT`;; let EXISTS_POINT = thm `; !P. (?p. P p) <=> P Point_1 \/ P Point_2 \/ P Point_3 \/ P Point_4 \/ P Point_5 \/ P Point_6 \/ P Point_7 proof let P be fano_Point->bool; ~(?p. P p) <=> ~(P Point_1 \/ P Point_2 \/ P Point_3 \/ P Point_4 \/ P Point_5 \/ P Point_6 \/ P Point_7) by REWRITE_TAC,DE_MORGAN_THM,NOT_EXISTS_THM,FORALL_POINT; qed`;; let FORALL_LINE = thm `; !P. (!p. P p) <=> P Line_1 /\ P Line_2 /\ P Line_3 /\ P Line_4 /\ P Line_5 /\ P Line_6 /\ P Line_7 by Line_INDUCT`;; let EXISTS_LINE = thm `; !P. (?p. P p) <=> P Line_1 \/ P Line_2 \/ P Line_3 \/ P Line_4 \/ P Line_5 \/ P Line_6 \/ P Line_7 proof let P be fano_Line->bool; ~(?p. P p) <=> ~(P Line_1 \/ P Line_2 \/ P Line_3 \/ P Line_4 \/ P Line_5 \/ P Line_6 \/ P Line_7) by REWRITE_TAC,DE_MORGAN_THM,NOT_EXISTS_THM,FORALL_LINE; qed;`;; let FANO_TAC = GEN_REWRITE_TAC DEPTH_CONV [FORALL_POINT; EXISTS_LINE; EXISTS_POINT; FORALL_LINE] THEN GEN_REWRITE_TAC DEPTH_CONV (basic_rewrites() @ [ON_CLAUSES; Point_DISTINCT; Line_DISTINCT]);; let AXIOM_1 = thm `; !p p'. ~(p = p') ==> ?l. p ON l /\ p' ON l /\ !l'. p ON l' /\ p' ON l' ==> (l' = l) by TIMED_TAC 3 FANO_TAC`;; let AXIOM_2 = thm `; !l l'. ?p. p ON l /\ p ON l' by FANO_TAC`;; let AXIOM_3 = thm `; ?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\ ~(?l. p ON l /\ p' ON l /\ p'' ON l) by TIMED_TAC 2 FANO_TAC`;; let AXIOM_4 = thm `; !l. ?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\ p ON l /\ p' ON l /\ p'' ON l by TIMED_TAC 3 FANO_TAC`;; let AXIOM_1' = thm `; !p p' l l'. ~(p = p') /\ p ON l /\ p' ON l /\ p ON l' /\ p' ON l' ==> (l' = l) proof let p p' be fano_Point; let l l' be fano_Line; assume ~(p = p') /\ p ON l /\ p' ON l /\ p ON l' /\ p' ON l' [1]; consider l1 such that p ON l1 /\ p' ON l1 /\ !l'. p ON l' /\ p' ON l' ==> (l' = l1) [2] by 1,AXIOM_1; l = l1 by 1,2; .= l' by 1,2; qed`;; let LEMMA_1' = thm `; !O. ?l. O ON l proof consider p p' p'' such that ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\ ~(?l. p ON l /\ p' ON l /\ p'' ON l) [1] by AXIOM_3; let O be fano_Point; ~(p = O) \/ ~(p' = O) by 1; consider P such that ~(P = O) [2]; consider l such that O ON l /\ P ON l /\ !l'. O ON l' /\ P ON l' ==> (l' = l) [3] by 2,AXIOM_1; thus ?l. O ON l by 3; end`;; let DUAL_1 = thm `; !l l'. ~(l = l') ==> ?p. p ON l /\ p ON l' /\ !p'. p' ON l /\ p' ON l' ==> (p' = p) proof assume ~thesis; consider l l' such that ~(l = l') /\ !p. p ON l /\ p ON l' ==> ?p'. p' ON l /\ p' ON l' /\ ~(p' = p) [1]; consider p such that p ON l /\ p ON l' [2] by AXIOM_2; consider p' such that p' ON l /\ p' ON l' /\ ~(p' = p) [3] by 1,2; thus F by 1,2,AXIOM_1'; end`;; let DUAL_2 = thm `; !p p'. ?l. p ON l /\ p' ON l proof let p p' be fano_Point; ?l. p ON l [1] by LEMMA_1'; (p = p') \/ ?l. p ON l /\ p' ON l /\ !l'. p ON l' /\ p' ON l' ==> (l' = l) by AXIOM_1; qed by 1`;; let DUAL_3 = thm `; ?l1 l2 l3. ~(l1 = l2) /\ ~(l2 = l3) /\ ~(l1 = l3) /\ ~(?p. p ON l1 /\ p ON l2 /\ p ON l3) proof consider p1 p2 p3 such that ~(p1 = p2) /\ ~(p2 = p3) /\ ~(p1 = p3) /\ ~(?l. p1 ON l /\ p2 ON l /\ p3 ON l) [1] by AXIOM_3; consider l1 such that p1 ON l1 /\ p3 ON l1 [2] by DUAL_2; consider l2 such that p2 ON l2 /\ p3 ON l2 [3] by DUAL_2; consider l3 such that p1 ON l3 /\ p2 ON l3 [4] by DUAL_2; take l1; take l2; take l3; thus ~(l1 = l2) /\ ~(l2 = l3) /\ ~(l1 = l3) [5] by 1,2,3,4; assume ~thesis; consider q such that q ON l1 /\ q ON l2 /\ q ON l3 [6]; consider q' such that q' ON l1 /\ q' ON l3 /\ !p'. p' ON l1 /\ p' ON l3 ==> (p' = q') [7] by 5,DUAL_1; q = q' by 6,7; .= p1 by 2,4,7; thus F by 1,3,6; end`;; let DUAL_4 = thm `; !O. ?OP OQ OR. ~(OP = OQ) /\ ~(OQ = OR) /\ ~(OP = OR) /\ O ON OP /\ O ON OQ /\ O ON OR proof let O be fano_Point; consider OP such that O ON OP [1] by LEMMA_1'; consider p p' p'' such that ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\ p ON OP /\ p' ON OP /\ p'' ON OP [2] by AXIOM_4; ~(p = O) \/ ~(p' = O) by 2; consider P such that ~(P = O) /\ P ON OP [3] by 2; consider q q' q'' such that ~(q = q') /\ ~(q' = q'') /\ ~(q = q'') /\ ~(?l. q ON l /\ q' ON l /\ q'' ON l) [4] by AXIOM_3; ~(q ON OP) \/ ~(q' ON OP) \/ ~(q'' ON OP) by 4; consider Q such that ~(Q ON OP) [5]; consider l such that P ON l /\ Q ON l [6] by DUAL_2; consider r r' r'' such that ~(r = r') /\ ~(r' = r'') /\ ~(r = r'') /\ r ON l /\ r' ON l /\ r'' ON l [7] by AXIOM_4; ((r = P) \/ (r = Q) \/ ~(r = P) /\ ~(r = Q)) /\ ((r' = P) \/ (r' = Q) \/ ~(r' = P) /\ ~(r' = Q)); consider R such that R ON l /\ ~(R = P) /\ ~(R = Q) [8] by 7; consider OQ such that O ON OQ /\ Q ON OQ [9] by DUAL_2; consider OR such that O ON OR /\ R ON OR [10] by DUAL_2; take OP; take OQ; take OR; ~(O ON l) by 1,3,5,6,AXIOM_1'; thus ~(OP = OQ) /\ ~(OQ = OR) /\ ~(OP = OR) /\ O ON OP /\ O ON OQ /\ O ON OR by 1,3,5,6,8,9,10,AXIOM_1'; end`;; (* ======== Tutorial/Changing_proof_style.ml =============================== *) horizon := 1;; let NSQRT_2_4 = thm `; !p q. p * p = 2 * q * q ==> q = 0 proof !p. (!m. m < p ==> (!q. m * m = 2 * q * q ==> q = 0)) ==> (!q. p * p = 2 * q * q ==> q = 0) proof let p be num; assume !m. m < p ==> !q. m * m = 2 * q * q ==> q = 0 [A]; let q be num; assume p * p = 2 * q * q [B]; EVEN(p * p) <=> EVEN(2 * q * q); EVEN(p) by TIMED_TAC 2 o MESON_TAC,ARITH,EVEN_MULT; // "EVEN 2 by CONV_TAC o HOL_BY,ARITH;" takes over a minute... consider m such that p = 2 * m [C] by EVEN_EXISTS; cases by ARITH_TAC; suppose q < p; q * q = 2 * m * m ==> m = 0 by A; qed by NUM_RING,B,C; suppose p <= q; p * p <= q * q by LE_MULT2; q * q = 0 by ARITH_TAC,B; qed by NUM_RING; end; qed by MATCH_MP_TAC,num_WF`;;