Email Gateway (Aug 19 2022 at 16:59): Email Gateway (Aug 19 2022 at 16:59):From: Bob Fang <bf283@cam.ac.uk>
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?
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?
Thanks.
Best,
Bob
=====================================================
Bob Fang
MPhill Advanced Computer Science Student at Computer Lab, University of
Cambridge.
Contact Address: Churchill College, Cambridge. CB3 0DS
Email Gateway (Aug 19 2022 at 16:59):From: David Cock <david.cock@inf.ethz.ch>
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
Email Gateway (Aug 19 2022 at 16:59):From: Christian Sternagel <c.sternagel@gmail.com>
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
"[z,y,x]"
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.
cheers
chris
Email Gateway (Aug 19 2022 at 16:59):From: Tobias Nipkow <nipkow@in.tum.de>
On 22/01/2015 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?
See the value command:
value "<expression>"
If any of the functions involved are not executable, you may get a strange result.
Tobias
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?Thanks.
Best,
Bob
=====================================================
Bob Fang
MPhill Advanced Computer Science Student at Computer Lab, University of
Cambridge.
Contact Address: Churchill College, Cambridge. CB3 0DS
Last updated: Apr 25 2024 at 20:15 UTC