[isabelle] Ways to use expression shorthands in proof?

Hi people out there,

Sorry for an other rather beginner's question, but here is: I favor explicit proof over automated one, except for some simplifications group. That works, but this often lead to repeated subexpressions in multiple “have”, and that bloats the proof text, which in turn, does not help readability. I wondered if there is a way to have shorthands for common expression appearing at multiple places. I tried with a “def E ≡ "my-expression"” and then an “have "blah E blah"”, but it does not work, seems E is not replaced with the corresponding expression as I expected, and proofs by simp which succeed with the literal subexpression, fails when I replace the literal subexpression with E. I also tried a naive “write "my-expression" ("E")”, but that's even worse, Isabelle complains the expression is an unknown constant.

You see that's not a question about proving, but a question about style in writing proofs.

I have another in the same vein, for which I don't wish to open a new thread. I don't know about LaTex, and wondered if there a way, to do the same with plain text comments. That is, I would write a comment somewhere, and either include it at another place or else add a reference to it from that other place.

I may also have a question about the different way to invoke the simplifier, but I leave that for later; that's enough for that thread.

  Have a nice day all

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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