Hi, John, Could I use the related theorem of HOL Light in HOL? Actually, I need use List or Vector in HOL now. However, I don't know how to use a list or vector in HOL, although I know a rich source of theorems on Vector can be find in HOL Light. Since I have to use some other important theorems in HOL, Could you give me some information?
Best Wishes, Liya Liu Quoting John Harrison <[email protected]>: > > 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 > ------------------------------------------------------------------------------ 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
