Tutorial/Tactics_and_tacticals.ml

   1 g `2 <= n /\ n <= 2 ==> f(2,2) + n < f(n,n) + 7`;;
   2 e DISCH_TAC;;
   3 b();;
   4 e(CONV_TAC(REWRITE_CONV[LE_ANTISYM]));;
   5 e(SIMP_TAC[]);;
   6 e(ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
   7 e DISCH_TAC;;
   8 e(ASM_REWRITE_TAC[]);;
   9 e(CONV_TAC ARITH_RULE);;
  10 let trivial = top_thm();;
  11
  12 g `2 <= n /\ n <= 2 ==> f(2,2) + n < f(n,n) + 7`;;
  13 e(CONV_TAC(REWRITE_CONV[LE_ANTISYM]));;
  14 e(SIMP_TAC[]);;
  15 e(ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
  16 e DISCH_TAC;;
  17 e(ASM_REWRITE_TAC[]);;
  18 e(CONV_TAC ARITH_RULE);;
  19 let trivial = top_thm();;
  20
  21 g `2 <= n /\ n <= 2 ==> f(2,2) + n < f(n,n) + 7`;;
  22 e(CONV_TAC(REWRITE_CONV[LE_ANTISYM]) THEN
  23   SIMP_TAC[] THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
  24   DISCH_TAC THEN ASM_REWRITE_TAC[] THEN CONV_TAC ARITH_RULE);;
  25 let trivial = top_thm();;
  26
  27 let trivial = prove
  28  (`2 <= n /\ n <= 2 ==> f(2,2) + n < f(n,n) + 7`,
  29   CONV_TAC(REWRITE_CONV[LE_ANTISYM]) THEN
  30   SIMP_TAC[] THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
  31   DISCH_TAC THEN ASM_REWRITE_TAC[] THEN CONV_TAC ARITH_RULE);;
  32
  33 let trivial = prove
  34  (`!x y:real. &0 < x * y ==> (&0 < x <=> &0 < y)`,
  35   REPEAT GEN_TAC THEN MP_TAC(SPECL [`--x`; `y:real`] REAL_LE_MUL) THEN
  36   MP_TAC(SPECL [`x:real`; `--y`] REAL_LE_MUL) THEN REAL_ARITH_TAC);;
  37
  38 let trivial = prove
  39  (`!x y:real. &0 < x * y ==> (&0 < x <=> &0 < y)`,
  40   MATCH_MP_TAC REAL_WLOG_LE THEN CONJ_TAC THEN REPEAT GEN_TAC THEN
  41   MP_TAC(SPECL [`--x`; `y:real`] REAL_LE_MUL) THEN REAL_ARITH_TAC);;
  42
  43 let SUM_OF_NUMBERS = prove
  44  (`!n. nsum(1..n) (\i. i) = (n * (n + 1)) DIV 2`,
  45   INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN ARITH_TAC);;
  46
  47 let SUM_OF_SQUARES = prove
  48  (`!n. nsum(1..n) (\i. i * i) = (n * (n + 1) * (2 * n + 1)) DIV 6`,
  49   INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN ARITH_TAC);;
  50
  51 let SUM_OF_CUBES = prove
  52  (`!n. nsum(1..n) (\i. i*i*i) = (n * n * (n + 1) * (n + 1)) DIV 4`,
  53   INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN ARITH_TAC);;