Update from HH
[hl193./.git] / 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);;