有理整数の性質 by num_WF.

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

let lem0 = prove
 (`prop2 0`,
  SIMP_TAC[def0;def1;def2] THEN ARITH_TAC);;
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 = REWRITE_RULE[UNDISCH(ARITH_RULE `5<=n ==>SUC (SUC (SUC (SUC (SUC (n-5)))))=n`)](SPEC`n-5`lem1);;

g `!n. prop1 n` ;;
e( MATCH_MP_TAC num_WF THEN GEN_TAC);;
e( DISJ_CASES_TAC (ARITH_RULE `(n=0 \/ n=SUC 0 \/ n=SUC (SUC 0) \/ n=SUC (SUC (SUC 0))  \/ n=SUC (SUC (SUC (SUC 0))) ) \/ 5<=n`)  );;
e( ASM_MESON_TAC[def2;lem0] );;
e( ASSUME_TAC (UNDISCH(ARITH_RULE `5<=n==>n-5<n`))  );;
e( DISCH_THEN (MP_TAC o (UNDISCH o (SPEC `n-5`))) THEN SIMP_TAC [def1;CONTRAPOS_THM;lem1;lem2;MOD_MULT_ADD;ADD_AC]  );;
let lem3 = top_thm () ;;
let theorem_20130310_2 = MESON[lem3;def0;def1]`!n. ~( (n EXP 2 + n + 1) MOD 5= 0)`;;

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