1 (* ======== Examples/mizar.ml ============================================== *)
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))
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]
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;
27 (!x. x IN Y ==> a <= x) /\
28 (!a'. (!x. x IN Y ==> a' <= x) ==> a' <= a) [lub] by least_upper_bound;
30 !b. b IN Y ==> f a <= b
33 assume b IN Y [b_in_Y];
34 f b <= b [L0] by -,Y_thm;
36 f a <= f b by -,monotonicity;
37 thus f a <= b by -,L0,transitivity;
39 f(a) <= a [Part1] by -,lub;
40 f(f(a)) <= f(a) by -,monotonicity;
43 qed by -,Part1,antisymmetry`;;
45 unhide_constant "<=";;
47 (* ======== Mizarlight/duality.ml ========================================== *)
49 parse_as_infix("ON",(11,"right"));;
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)`;;
65 !(ON):Point->Line->bool. projective(ON) ==> !p. ?l. p ON l
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;
73 consider q q' such that ~(q = q':Point);
74 ~(p = q) \/ ~(p = q');
75 consider l such that p ON l by 1;
80 !(ON):Point->Line->bool. projective(ON)
82 p1 ON l /\ p2 ON l /\ p1 ON l1 /\ p2 ON l2 /\ q ON l2 /\
83 ~(q ON l) /\ ~(p1 = p2) ==> ~(l1 = l2)
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
96 assume ~(q ON l) [11];
97 assume ~(p1 = p2) [12];
100 l = l2 by 1,5,6,9,12;
104 let PROJECTIVE_DUALITY = thm `;
105 !(ON):Point->Line->bool. projective(ON) ==> projective (\l p. p ON l)
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;
116 !l1 l2. ~(l1 = l2) ==> ?!p. p ON l1 /\ p ON l2 [5]
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)
124 assume p' ON l1 /\ p' ON l2 [8];
131 !p1 p2. ?l. p1 ON l /\ p2 ON l [9]
141 ?l1 l2 l3. ~(l1 = l2) /\ ~(l2 = l3) /\ ~(l1 = l3) /\
142 ~(?p. p ON l1 /\ p ON l2 /\ p ON l3) [10]
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;
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];
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];
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;
167 !p0. ?l0 L1 L2. ~(l0 = L1) /\ ~(L1 = L2) /\ ~(l0 = L2) /\
168 p0 ON l0 /\ p0 ON L1 /\ p0 ON L2
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]
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);
187 l1 = l0 by 1,16,17,19;
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;
198 qed by REWRITE_TAC,5,9,10,projective`;;
200 unhide_constant "ON";;
202 (* ======== Mizarlight/duality_holby.ml ==================================== *)
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";;
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";;
214 let Point_DISTINCT = distinctness "fano_Point";;
216 let Line_DISTINCT = distinctness "fano_Line";;
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];;
222 let fano_point i = mk_const("Point_"^string_of_int i,[])
223 and fano_line i = mk_const("Line_"^string_of_int i,[]);;
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));;
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)));;
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`))
238 REWRITE_TAC[ON; Line_DISTINCT; Point_DISTINCT]);;
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
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
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;
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
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
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;
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]);;
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`;;
282 !l l'. ?p. p ON l /\ p ON l' by FANO_TAC`;;
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`;;
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`;;
294 let AXIOM_1' = thm `;
295 !p p' l l'. ~(p = p') /\ p ON l /\ p' ON l /\ p ON l' /\ p' ON l'
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]
308 let LEMMA_1' = thm `;
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;
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;
323 !l l'. ~(l = l') ==> ?p. p ON l /\ p ON l' /\
324 !p'. p' ON l /\ p' ON l' ==> (p' = p)
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';
335 !p p'. ?l. p ON l /\ p' ON l
337 let p p' be fano_Point;
338 ?l. p ON l [1] by LEMMA_1';
340 ?l. p ON l /\ p' ON l /\
341 !l'. p ON l' /\ p' ON l' ==> (l' = l) by AXIOM_1;
345 ?l1 l2 l3. ~(l1 = l2) /\ ~(l2 = l3) /\ ~(l1 = l3) /\
346 ~(?p. p ON l1 /\ p ON l2 /\ p ON l3)
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;
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;
366 !O. ?OP OQ OR. ~(OP = OQ) /\ ~(OQ = OR) /\ ~(OP = OR) /\
367 O ON OP /\ O ON OQ /\ O ON OR
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';
396 (* ======== Tutorial/Changing_proof_style.ml =============================== *)
400 let NSQRT_2_4 = thm `;
401 !p q. p * p = 2 * q * q ==> q = 0
403 !p. (!m. m < p ==> (!q. m * m = 2 * q * q ==> q = 0))
404 ==> (!q. p * p = 2 * q * q ==> q = 0)
407 assume !m. m < p ==> !q. m * m = 2 * q * q ==> q = 0 [A];
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;
416 q * q = 2 * m * m ==> m = 0 by A;
419 p * p <= q * q by LE_MULT2;
420 q * q = 0 by ARITH_TAC,B;
423 qed by MATCH_MP_TAC,num_WF`;;