Update from HH
[hl193./.git] / Tutorial / Wellfounded_induction.ml
1 let NSQRT_2 = prove
2  (`!p q. p * p = 2 * q * q ==> q = 0`,
3   MATCH_MP_TAC num_WF THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
4   REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o AP_TERM `EVEN`) THEN
5   REWRITE_TAC[EVEN_MULT; ARITH] THEN REWRITE_TAC[EVEN_EXISTS] THEN
6   DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN
7   FIRST_X_ASSUM(MP_TAC o SPECL [`q:num`; `m:num`]) THEN
8   ASM_REWRITE_TAC[ARITH_RULE
9    `q < 2 * m ==> q * q = 2 * m * m ==> m = 0 <=>
10     (2 * m) * 2 * m = 2 * q * q ==> 2 * m <= q`] THEN
11   ASM_MESON_TAC[LE_MULT2; MULT_EQ_0; ARITH_RULE `2 * x <= x <=> x = 0`]);;