Re: [isabelle] Ways to use expression shorthands in proof?



Le Sat, 04 Aug 2012 16:24:18 +0200, Gottfried Barrow <gottfried.barrow at gmx.com> a écrit:
For an interesting discussion of an explicit proof example using introduction and elimination rules, scroll down to Wenzel's PhD thesis on the page below, and have a look at pages 77 to 92 where he takes a simple example and starts with a very abbreviated form and keeps expanding it into more explicit forms.

http://www4.in.tum.de/~wenzelm/papers/
<http://www4.in.tum.de/%7Ewenzelm/papers/>

Currently on the page 77 you mentioned, looking at “is” and “concl is”. Looks even shorter and straighter than using “let”. That's what I like with my discovery of Isabelle: as I go, I understand it's intentionally designed to author concise and readable proof, and to balance both (conciseness and verbosity) as you see fits.

--
“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.