Re: [isabelle] making use of star



Tobias, hi,

many thanks for your reply. I understand now that you don't need to execute
definitions in order to prove things about them. So, for example, the proof
that `star' is indeed transitive doesn't require `code_pred star', but
computing with it does. I find it fascinating that you can compute with
Isabelle in this way nonetheless.

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.

As an interesting aside, working with Isabelle in a room full of Coq users
seems to be working out fine. Those around me get an introduction to basic
Isabelle syntax amongst other things and I get valuable conversations about
theorem proving and types in general.

Kind regards,

James






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