Re: [isabelle] making use of star



Am 22/06/2012 18:26, schrieb James Smith:
> More fundamentally, I do not want to create executable code, although I am
> giving the impression that I do. I am just adjusting to the use of a theorem
> prover after using a model checker. I should be proving things about the
> types that I think up, rather than instantiating them. Creating instances of
> `State' to confirm that `succ star' appears to be transitive is stupid when
> I already have a proof that `star' is transitive without needing to execute
> or indeed instantiate anything.

Of course, if you have a proof, there is no need to run test cases to check the
property. But with larger definitions, proofs become expensive enough that a bit
of rapid prototyping to weed out the most glaring bugs can be quite beneficial.

Tobias





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