Re: [isabelle] Running a function defined in Isabelle

On 22/01/15 23:53, Bob Fang wrote:
Hi all,

Just wondering if I have defined a function in Isabelle, is there anyway to
write some simple test cases on my own first instead of jumping directly
into proving properties of it?

If you really want to do that, look into the code generator, which can produce ML and Haskell (at least). It's an urge that I remember when starting Isabelle, but after a while you tend to realise that you didn't really need to do it.

Also, if I have proved a theorem, is it automatically added to the
rewriting rules or I have to add "[simp]:" in the theorem declaration?

No. Not all rules make safe (or even valid) rewriting rules. I strongly recommend that you don't do this, unless you're absolutely certain that you've got a safe and universally-useful simp rule.

David Cock

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.