有理整数の性質 by INDUCT_TAC.

let def0 = new_definition `f0 n = n EXP 2 + n + 1` ;;
let def1 = new_definition `prop1 n <=> ~((f0 n) MOD 5 = 0)` ;;
let def2 = new_definition `prop2 n <=> prop1 n /\ prop1 (SUC n) /\ prop1 (SUC (SUC n)) /\ prop1 (SUC (SUC (SUC n))) /\ prop1 (SUC (SUC (SUC (SUC n))))` ;;

let lem1 = prove
 (`!n. f0 (SUC (SUC (SUC (SUC (SUC n))))) = f0 n + (2 * n + 6) * 5`,
  REWRITE_TAC [def0] THEN ARITH_TAC);;

let lem2 = prove
 (`!n:num. prop2 n`,
  INDUCT_TAC THENL
  [REWRITE_TAC [def0;def1;def2] THEN ARITH_TAC;
   POP_ASSUM MP_TAC THEN REWRITE_TAC [def2] THEN
   STRIP_TAC THEN UNDISCH_TAC `prop1 n` THEN
   ASM_SIMP_TAC [def1;lem1;CONTRAPOS_THM] THEN
   MESON_TAC [MOD_MULT_ADD; ADD_AC]]);;

let theorem_20130310 = MESON[lem2;def0;def1;def2]`!n. ~( (n EXP 2 + n + 1) MOD 5= 0)`;;

val theorem_20130310 : thm = |- !n. ~((n EXP 2 + n + 1) MOD 5 = 0)