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. -- 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
