Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
(* ------------------------------------------------------------------------- *) (* Definition of rationality (& = natural injection N->R). *) (* ------------------------------------------------------------------------- *) let rational = new_definition `rational(r) = ?p q. ~(q = 0) /\ abs(r) = &p / &q`;; (* ------------------------------------------------------------------------- *) (* The main lemma, purely in terms of natural numbers. *) (* ------------------------------------------------------------------------- *) let NSQRT_2 = prove (`!p q. p * p = 2 * q * q ==> q = 0`, MATCH_MP_TAC num_WF THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o AP_TERM `EVEN`) THEN REWRITE_TAC[EVEN_MULT; ARITH] THEN REWRITE_TAC[EVEN_EXISTS] THEN DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN FIRST_X_ASSUM(MP_TAC o SPECL [`q:num`; `m:num`]) THEN POP_ASSUM MP_TAC THEN CONV_TAC SOS_RULE);; (* ------------------------------------------------------------------------- *) (* Hence the irrationality of sqrt(2). *) (* ------------------------------------------------------------------------- *) let SQRT_2_IRRATIONAL = prove (`~rational(sqrt(&2))`, SIMP_TAC[rational; real_abs; SQRT_POS_LE; REAL_POS; NOT_EXISTS_THM] THEN REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN DISCH_THEN(MP_TAC o AP_TERM `\x. x pow 2`) THEN ASM_SIMP_TAC[SQRT_POW_2; REAL_POS; REAL_POW_DIV; REAL_POW_2; REAL_LT_SQUARE; REAL_OF_NUM_EQ; REAL_EQ_RDIV_EQ] THEN ASM_MESON_TAC[NSQRT_2; REAL_OF_NUM_EQ; REAL_OF_NUM_MUL]);;