Re: [isabelle] Running a function defined in Isabelle

Some additions:

On 01/23/2015 10:20 AM, David Cock wrote:

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.

You can use the "value" command to check the result of a function on specific inputs manually. E.g.,

value "rev [x,y,z]"

will result in


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.
Most of the time theorems are not added to the simplifier by default. However, there are exceptions. E.g, if you define a constant by "primrec" or "fun", the corresponding equations will be added as rewrite rules. The same is true for certain facts about datatypes. Having said that. When you prove a theorem by hand, you have to add [simp] manually in order to add it as a rewrite rule. As David said, this can be dangerous.



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