You check that your definition is correct by proving appropriate
theorems about it. For example, HOL4 provides an EVAL function so
that you can do things like
> EVAL ``FACT 20``;
val it = |- FACT 20 = 2432902008176640000: thm
and this is the sort of thing you'd like to see. In HOL Light, you
could certainly use rewriting to prove this sort of result.
Thanks, Michael! HOL Light does not have your EVAL, but maybe it has something
similar. EVAL is indeed the sort of thing that Colin Rowat and I were looking
for. I did read a bit about rewriting, and I see that it's in the EVAL
ballpark, but it sounds like you have to be pretty good at HOL Light to use it.
Any tip?
Freek, I was disappointed to not learn how to write readable code in Isar, as
Isabelle has great fonts and lots of respectable looking documentation. And
on top of that Makarius wrote me 100 lines of code. But I couldn't figure out
how to write readable proofs there. So I'm sticking with Mizar and your
excellent miz3. Can you jump into the discussion Michael and I were having
about whether miz3 is intentionally weakened? Michael seems to think yes, I
think no, but I wonder what effect the MESON depth limit of 50 has, or the fact
that MESON is just FOL and not HOL.
--
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
