miz3/Samples/wishes.ml

   1 let EXAMPLE = prove
   2  (`!n. nsum(0..n) (\i. i) = (n*(n + 1)) DIV 2`,
   3   INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN ARITH_TAC);;
   4
   5 let EXAMPLE_IN_MIZAR_LIGHT = thm `;
   6   !n. nsum (0..n) (\i. i) = (n * (n + 1)) DIV 2 [1]
   7   proof
   8     nsum (0..0) (\i. i) = 0 [2] by NSUM_CLAUSES_NUMSEG;
   9       ... = (0 * (0 + 1)) DIV 2 [3] by ARITH_TAC;
  10     !n. nsum (0..n) (\i. i) = (n * (n + 1)) DIV 2
  11         ==> nsum (0..SUC n) (\i. i) = (SUC n * (SUC n + 1)) DIV 2 [4]
  12     proof
  13       let n be num;
  14       assume nsum (0..n) (\i. i) = (n * (n + 1)) DIV 2 [5];
  15     qed by #;
  16   qed by INDUCT_TAC from 3,4`;;