miz3/Samples/talk.ml

   1 let ARITHMETIC_PROGRESSION_SIMPLE = prove
   2  (`!n. nsum(1..n) (\i. i) = (n*(n + 1)) DIV 2`,
   3   INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN
   4   ARITH_TAC);;
   5
   6 horizon := 1;;
   7
   8 thm `;
   9 !n. nsum(0..n) (\i. i) = (n*(n + 1)) DIV 2
  10 proof
  11   nsum(0..0) (\i. i) = 0 by NSUM_CLAUSES_NUMSEG;
  12     .= (0*(0 + 1)) DIV 2 [A1] by ARITH_TAC;
  13   now let n be num;
  14     assume nsum(0..n) (\i. i) = (n*(n + 1)) DIV 2;
  15     nsum(0..SUC n) (\i. i) = (n*(n + 1)) DIV 2 + SUC n
  16       by NSUM_CLAUSES_NUMSEG,ARITH_RULE (parse_term "0 <= SUC n");
  17     thus .= ((SUC n)*(SUC n + 1)) DIV 2 by ARITH_TAC;
  18   end;
  19 qed by INDUCT_TAC,A1`;;
  20
  21 thm `;
  22 now
  23   (if 1 = 0 then 0 else 0) = (0 * (0 + 1)) DIV 2 [A1] by ARITH_TAC;
  24   nsum (1..0) (\i. i) = (0 * (0 + 1)) DIV 2 [A2]
  25     by REWRITE_TAC,NSUM_CLAUSES_NUMSEG,A1;
  26   now [A3]
  27     let n be num;
  28     assume nsum (1..n) (\i. i) = (n * (n + 1)) DIV 2 [A4];
  29     (if 1 <= SUC n then (n * (n + 1)) DIV 2 + SUC n else (n * (n + 1)) DIV 2) =
  30       (SUC n * (SUC n + 1)) DIV 2 [A5] by ARITH_TAC;
  31     thus nsum (1..SUC n) (\i. i) = (SUC n * (SUC n + 1)) DIV 2 [A6]
  32       by REWRITE_TAC,NSUM_CLAUSES_NUMSEG,A4,A5;
  33   end;
  34   thus !n. nsum (1..n) (\i. i) = (n * (n + 1)) DIV 2 [A7] by INDUCT_TAC,A2,A3;
  35 end`;;
  36
  37 let EXAMPLE = ref None;;
  38
  39 EXAMPLE := Some `;
  40 !n. nsum(0..n) (\i. i) = (n*(n + 1)) DIV 2
  41 proof
  42   nsum(0..0) (\i. i) = (0*(0 + 1)) DIV 2;
  43   now let n be nat;
  44     assume nsum(0..n) (\i. i) = (n*(n + 1)) DIV 2;
  45     thus nsum(0..SUC n) (\i. i) = ((SUC n)*(SUC n + 1)) DIV 2 by #;
  46   end;
  47 qed`;;
  48
  49 thm `;
  50 !n. nsum (1..n) (\i. i) = (n * (n + 1)) DIV 2
  51 proof
  52   (if 1 = 0 then 0 else 0) = (0 * (0 + 1)) DIV 2 by ARITH_TAC;
  53   nsum (1..0) (\i. i) = (0 * (0 + 1)) DIV 2 [A1]
  54     by ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG];
  55   !n. nsum (1..n) (\i. i) = (n * (n + 1)) DIV 2
  56       ==> nsum (1..SUC n) (\i .i) = (SUC n * (SUC n + 1)) DIV 2
  57   proof
  58     let n be num;
  59     assume nsum (1..n) (\i. i) = (n * (n + 1)) DIV 2 [A2];
  60     (if 1 <= SUC n then (n * (n + 1)) DIV 2 + SUC n else (n * (n + 1)) DIV 2) =
  61       (SUC n * (SUC n + 1)) DIV 2 by ARITH_TAC;
  62   qed by ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG],A2;
  63 qed by INDUCT_TAC,A1`;;
  64
  65 let NSUM_CLAUSES_NUMSEG' = thm `;
  66 !s. nsum(0..0) s = s 0 /\ !n. nsum(0..n + 1) s = nsum(0..n) s + s (n + 1)
  67 proof
  68   !n. 0 <= SUC n by ARITH_TAC;
  69 qed by NSUM_CLAUSES_NUMSEG,ADD1`;;
  70
  71 let num_INDUCTION' = REWRITE_RULE[ADD1] num_INDUCTION;;
  72
  73 thm `;
  74 !s. (!i. s i = i) ==> !n. nsum(0..n) s = (n*(n + 1)) DIV 2
  75 proof
  76   let s be num->num;
  77   assume !i. s i = i [A1];
  78   set X = \n. (nsum(0..n) s = (n*(n + 1)) DIV 2);
  79   nsum(0..0) s = s 0 by NSUM_CLAUSES_NUMSEG';
  80     .= 0 by A1;
  81     .= (0*(0 + 1)) DIV 2 by ARITH_TAC;
  82   X 0 [A2];
  83   now [A3] let n be num;
  84     assume X n;
  85     nsum(0..n + 1) s = (n*(n + 1)) DIV 2 + s (n + 1) by NSUM_CLAUSES_NUMSEG';
  86       .= (n*(n + 1)) DIV 2 + (n + 1) by A1;
  87     thus X (n + 1) by ARITH_TAC;
  88   end;
  89   !n. X n by MATCH_MP_TAC,num_INDUCTION',A2,A3;
  90 qed`;;
  91