bY
On Jun 29, 2012 9:47 AM, "Bill Richter" <[email protected]>
wrote:
>
> Here's a question Ramana got me thinking about. Going through the
> tutorial, I see functions (p 83) which interpret just fine:
>
> # let fib2 = define
> `(fib2 0 = 1) /\
> (fib2 1 = 1) /\
> (fib2 (n + 2) = fib2(n) + fib2(n + 1))`;;
> val fib2 : thm =
> |- fib2 0 = 1 /\ fib2 1 = 1 /\ fib2 (n + 2) = fib2 n + fib2 (n + 1)
>
> But how can I use fib2 to calculate Fibonacci numbers? I suppose if I
> was trying to prove something about Fibonacci numbers, HOL Light with
> this definition would be great. But this doesn't get me anything:
>
> # `fib2 6`;;
> val it : term = `fib2 6`
>
> and here I got an error:
>
> # REAL_ARITH `fib2 6`;;
> Exception: Failure "mk_neg".
>
> Maybe what I'm really asking is how to use HOL Light as a CAS, I see
> that at least one person, Cezary Kaliszyk, has done this:
> http://cl-informatik.uibk.ac.at/users/cek/holcas.php
> I bet a coauthor of Barendregt would do a good job here, but I'd guess
> there a way in HOL Light to crank out some numbers from functions.
In HOL4 this functionality is called computeLib, primarily the EVAL
function. I don't know if it exists in HOL Light. You can get some way
towards it in either system by just using rewriting rules (e.g., pretend
you're trying to prove an equality and call rewriting tactics).
>
> --
> 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
------------------------------------------------------------------------------
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
