Re: [isabelle] Running a function defined in Isabelle
On 01/23/2015 10:20 AM, David Cock wrote:
On 22/01/15 23:53, Bob Fang wrote:
Just wondering if I have defined a function in Isabelle, is there
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
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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and