The constant ``SIGMA`` in pred_setTheory can be used to express a sum.
It has type ``:('a -> num) -> ('a set) -> num``.
So, for example, to do the sum of f(z) for z in 1..n, you could use:
``SIGMA (\z. f (z+1)) (count n)``
On Sat, Jun 16, 2012 at 4:27 PM, Thomas Melham <
[email protected]> wrote:
> Dear Anggha,
>
> I'm afraid it's been a very long time since I was a HOL user, so I can't
> answer your question. But I hereby forward your query to the HOL mailing
> list, hoping some active user can help.
>
> Best regards,
> Tom
>
> From: Anggha Nugraha <[email protected]>
> Reply-To: Anggha Nugraha <[email protected]>
> Date: Tuesday, 12 June 2012 06:14
> To: Tom Melham <[email protected]>
> Subject: Asking about HOL TP (sum syntax)
>
> Good evening Professor Melham.
>
> Firstly, let me introduce my self. My name is Anggha and now I'm a
> master student in Faculty of Computer Science in University of Indonesia.
> Now, I'm making my master thesis about proving the partial correctness of
> matrix multiplication program. I plan to making the manual proof using
> Hoare logic and then making the automation in HOL Theorem Proving.
>
> I have read your paper entitled,"A MECHANIZED THEORY OF THE -CALCULUS IN
> HOL" and I know that you're an expert in HOL TP.
>
> I have a problem in writing in HOL. I wanna write: C[i,j] = sum z=1..n
> A[i,z]*B[z,j]
> I use # to indicate array, so C[i,j] is written as (C#i)#j. Am I right
> doc?
>
> About the summation, I don't have any idea how to write this in HOL. How
> I define the syntax of sum? What library that I have to use prof?
> May you help me prof? And if you don't mind, can you give me an example?
>
> Thank you very much Prof. Melham and I really sorry if I disturb you
> prof.
>
> --
> Best regards,
> Anggha Satya Nugraha
> Graduate Student in Faculty of Computer Science
> University of Indonesia (Universitas Indonesia)
>
>
>
>
> ------------------------------------------------------------------------------
> Live Security Virtual Conference
> Exclusive live event will cover all the ways today's security and
> threat landscape has changed and how IT managers can respond. Discussions
> will include endpoint security, mobile security and the latest in malware
> threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
