(*  等差数列和の定理  *)



val SIGMA = Define
    `(SIGMA 0 = 0) /\
    (SIGMA n = n + SIGMA (n - 1))`;;


val ARW_TAC = RW_TAC arith_ss;;


val MULT_ASSOC = arithmeticTheory.MULT_ASSOC;;
val MULT_SYM = arithmeticTheory.MULT_SYM;;
val MULT_DIV = arithmeticTheory.MULT_DIV;;

val lemma1 = prove
    (``!a b. 2 * a * b DIV 2 = a * b``,
     REWRITE_TAC [EQ_SYM_RULE MULT_ASSOC] THEN
     REWRITE_TAC [SPECL [``2``,``a*b``] MULT_SYM] THEN
     RW_TAC arith_ss [MULT_DIV]);;

val lemma2 = prove
    (``!m. SUC (SUC (2 * m)) = (SUC m) * 2``,
     RW_TAC arith_ss []);;

val EVEN_ODD_EXISTS = arithmeticTheory.EVEN_ODD_EXISTS;;
val MULT_SUC = arithmeticTheory.MULT_SUC;;
val ODD_EVEN = arithmeticTheory.ODD_EVEN;;
val RIGHT_ADD_DISTRIB = arithmeticTheory.RIGHT_ADD_DISTRIB;;

val SIGMA_THM = prove
    (``!n. SIGMA n = n * (SUC n) DIV 2``,
     Induct_on `n` THENL
     [REWRITE_TAC [SIGMA] THEN RW_TAC arith_ss [],
      REWRITE_TAC [SIGMA] THEN RW_TAC arith_ss [] THEN
      Cases_on `EVEN n` THENL
      [IMP_RES_TAC EVEN_ODD_EXISTS THEN
       RW_TAC arith_ss [] THEN
       REWRITE_TAC [lemma1,lemma2] THEN
       REWRITE_TAC [MULT_ASSOC] THEN
       RW_TAC arith_ss [MULT_DIV] THEN
       REWRITE_TAC [SPECL [``m:num``,``SUC (2 * m)``] MULT_SYM] THEN
       REWRITE_TAC [EQ_SYM_RULE MULT_SUC],
       IMP_RES_TAC (EQ_SYM_RULE ODD_EVEN) THEN
       IMP_RES_TAC EVEN_ODD_EXISTS THEN
       RW_TAC arith_ss [] THEN
       REWRITE_TAC [lemma2] THEN
       REWRITE_TAC [MULT_ASSOC] THEN
       RW_TAC arith_ss [MULT_DIV] THEN
       REWRITE_TAC 
       [SPECL [``SUC m * 2``,``SUC (SUC m * 2)``] MULT_SYM] THEN
       REWRITE_TAC [MULT_ASSOC] THEN
       RW_TAC arith_ss [MULT_DIV] THEN
       REWRITE_TAC [SPECL [``SUC m``,``2``] MULT_SYM] THEN
       REWRITE_TAC [EQ_SYM_RULE RIGHT_ADD_DISTRIB] THEN
       RW_TAC arith_ss []]]);;