1 needs "Library/transc.ml";;
2 needs "Examples/sos.ml";;
8 let rational = new_definition
9 `rational(r) = ?p q. ~(q = 0) /\ abs(r) = &p/ &q`;;
11 (* ======== Mizar-style version ============================================ *)
13 let NSQRT_2_1 = thm `;
14 !p q. p*p = 2*q*q ==> q = 0
16 exec MATCH_MP_TAC num_WF;
18 assume !p'. p' < p ==> !q. p'*p' = 2*q*q ==> q = 0 [1];
20 assume p*p = 2*q*q [2];
21 EVEN (p*p) by EVEN_DOUBLE;
24 p = 2*p' [3] by EVEN_EXISTS;
25 q*q = 2*p'*p' [4] by 2,NUM_RING;
26 EVEN (q*q) by EVEN_DOUBLE;
29 q = 2*q' [5] by EVEN_EXISTS;
30 p'*p' = 2*q'*q' [6] by 4,NUM_RING;
32 ~(p = 0) by 2,NUM_RING;
34 p' < p by 3,ARITH_TAC;
36 qed by 5,7,MULT_EQ_0`;;
38 let SQRT_2_IRRATIONAL_1 = thm `;
41 assume rational(sqrt(&2));
42 set x = abs(sqrt(&2));
43 consider p q such that
44 ~(q = 0) /\ x = &p/ &q [7] by rational;
45 ~(&q = &0) by REAL_INJ;
46 x* &q = &p [8] by 7,REAL_DIV_RMUL;
47 &0 <= &2 by REAL_ARITH_TAC;
48 sqrt(&2) pow 2 = &2 by SQRT_POW2;
49 x pow 2 = &2 by REAL_ARITH_TAC;
50 &p* &p = &2* &q* &q by 8,REAL_RING;
51 p*p = 2*q*q by 8,REAL_INJ,REAL_OF_NUM_MUL;
54 (* ======== "automatically" converted from John's version ================== *)
56 let NSQRT_2_2 = thm `;
60 assume !m q. m < p ==> m * m = 2 * q * q ==> q = 0 [1];
61 assume p * p = 2 * q * q [2];
64 assume !m' q. m' < 2 * m ==> m' * m' = 2 * q * q ==> q = 0 [3];
65 assume (2 * m) * 2 * m = 2 * q * q [4];
66 (2 * m) * 2 * m = 2 * q * q
67 ==> (q < 2 * m ==> q * q = 2 * m * m ==> m = 0)
69 by TIMED_TAC 2 (CONV_TAC SOS_RULE);
70 (q < 2 * m ==> q * q = 2 * m * m ==> m = 0) ==> q = 0
71 by POP_ASSUM MP_TAC,4 from -;
72 thus q = 0 by FIRST_X_ASSUM
73 (MP_TAC o SPECL [parse_term "q:num"; parse_term "m:num"]),3,4;
75 (?m. p = 2 * m) ==> q = 0
76 by DISCH_THEN(X_CHOOSE_THEN (parse_term "m:num") SUBST_ALL_TAC),1,2;
77 EVEN p ==> q = 0 by REWRITE_TAC[EVEN_EXISTS],1,2;
78 (EVEN (p * p) <=> EVEN (2 * q * q)) ==> q = 0
79 by REWRITE_TAC[EVEN_MULT; ARITH],1,2;
80 thus q = 0 by FIRST_ASSUM(MP_TAC o AP_TERM (parse_term "EVEN")),1,2;
83 (!m q. m < p ==> m * m = 2 * q * q ==> q = 0)
85 ==> q = 0 by REPEAT STRIP_TAC;
86 !p. (!m. m < p ==> (!q. m * m = 2 * q * q ==> q = 0))
87 ==> (!q. p * p = 2 * q * q ==> q = 0)
88 by REWRITE_TAC[RIGHT_IMP_FORALL_THM];
89 thus !p q. p * p = 2 * q * q ==> q = 0 by MATCH_MP_TAC num_WF;
92 let SQRT_2_IRRATIONAL_2 = thm `;
98 ~(&2 * &q * &q = &p * &p)
99 by ASM_MESON_TAC[NSQRT_2_2; REAL_OF_NUM_EQ; REAL_OF_NUM_MUL];
100 ~((\x. x pow 2) (sqrt (&2)) = (\x. x pow 2) (&p / &q))
101 by ASM_SIMP_TAC[SQRT_POW_2; REAL_POS; REAL_POW_DIV; REAL_POW_2;
102 REAL_LT_SQUARE; REAL_OF_NUM_EQ; REAL_EQ_RDIV_EQ],1;
103 thus ~(sqrt (&2) = &p / &q)
104 by DISCH_THEN(MP_TAC o AP_TERM (parse_term "\\x. x pow 2")),1;
106 thus ~(~(q = 0) /\ sqrt (&2) = &p / &q)
107 by DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC);
109 !p q. ~(~(q = 0) /\ sqrt (&2) = &p / &q) by REPEAT GEN_TAC;
110 thus ~rational (sqrt (&2))
111 by SIMP_TAC[rational; real_abs; SQRT_POS_LE; REAL_POS; NOT_EXISTS_THM];
114 (* ======== humanized version of John's version ============================ *)
116 let NSQRT_2_3 = thm `;
117 !p q. p*p = 2*q*q ==> q = 0
119 set P = \p. !q. p*p = 2*q*q ==> q = 0;
122 assume !m. m < p ==> P m [1];
124 assume p*p = 2*q*q [2];
125 EVEN(2*q*q) by REWRITE_TAC,EVEN_MULT,ARITH;
126 EVEN p by 2,EVEN_MULT;
127 consider m such that p = 2*m [3] by EVEN_EXISTS;
128 (2*m)*2*m = 2*q*q /\ (q < 2*m /\ q*q = 2*m*m ==> m = 0) ==> q = 0
129 from TIMED_TAC 2 (CONV_TAC SOS_RULE);
132 qed by MATCH_MP_TAC num_WF`;;
134 let SQRT_2_IRRATIONAL_3 = thm `;
137 assume rational(sqrt(&2));
138 consider p q such that ~(q = 0) /\ sqrt(&2) = &p/ &q [1]
139 by rational,real_abs,SQRT_POS_LE,REAL_POS;
140 (&p* &p)/(&q* &q) = &2 [2] by SQRT_POW_2,REAL_POS,REAL_POW_DIV,REAL_POW_2;
141 &0 < &q* &q by 1,REAL_LT_SQUARE,REAL_OF_NUM_EQ;
142 &2*(&q* &q) = (&p* &p) by 2,REAL_EQ_RDIV_EQ;
143 qed by 1,NSQRT_2_3,REAL_OF_NUM_EQ,REAL_OF_NUM_MUL`;;