On Jun 25, 2012 7:10 AM, "Bill Richter" <[email protected]>
wrote:
>
> Ramana, thanks for answering Colin's questions, as some expert should.
> Yes, Colin is using HOL Light, but you can probably answer his
> questions anyway.
>
> what is y_j? Also, how are you formalising vectors?
>
> y is any element of R^N, maybe written real^N. y_j is its j-th entry.
>
> What you wrote about sup & maximum probably has HOL Light analogues,
> but I studied the HOL Light *.ml files and didn't find an exact answer
> to Colin's first question, which was how to define this max function
>
> (1) \bar{y} = max_{j in N} y_j for any y in R^n
>
> The obvious way to do this is by recursion, by `let rec'. I still
> haven't mastered the syntax, where to put the $s etc, but you can
> probably write this recursive function right away, so I'll post!
you can define maximum either using Hilbert choice (the @ operator) as I
showed in my first reply, or, if it's over the indices 0 to n as in this
example you can use recursion as Bill suggests. Either way you'll also have
to prove some useful properties about your definition. The definition by
recursion might look like this:
(bar 0 m y = m) /\
(bar (SUC n) m y = bar n (real_max m (y n)) y)
where again I'm assuming y is a function taking an (in this case natural
number) index and returning a real. modify as appropriate.
>
> --
> Best,
> Bill
------------------------------------------------------------------------------
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
