[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
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.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and