Hi Tony,
| How would I go about proving something simple like this?
|
| 1 + 2 + 3 + \dots + n = \frac{n(n+1)}{2}
You can find a discussion of this and related proofs in the HOL
Light tutorial, section 8.2:
http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf
For example:
let SUM_OF_NUMBERS = prove
(`!n. nsum(1..n) (\i. i) = (n * (n + 1)) DIV 2`,
INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN ARITH_TAC);;
John.
------------------------------------------------------------------------------
Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day
trial. Simplify your report design, integration and deployment - and focus on
what you do best, core application coding. Discover what's new with
Crystal Reports now. http://p.sf.net/sfu/bobj-july
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
