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`]);;