Email Gateway (Aug 18 2022 at 11:09): Email Gateway (Aug 18 2022 at 11:09):From: Peter Sewell <Peter.Sewell@cl.cam.ac.uk>
Dear Isabelle,
I'd like to write an expository document based on some Isabelle, and
so need to quote selected definitions, not necessarily in the order
they appear in the main .thy.
I expect this is a standard and solved problem, but the Tutorial
doesn't seem to address it. I can see how to quote (e.g.) type and
constant names, viz
text {* @{typ event_structure} @{const writes} *}
but not the bodies of selected "types" or "constdefs" definitions...?
many thanks,
Peter
p.s. While I'm here, could I appeal for _line numbers_ in the error
messages reported by the isabelle/proof-general combo? I recall that
a couple of years ago we humble users (primarily Keith Wansbrough) had
to add line numbers to the HOL error messages, dragging that kicking
and screaming into the 1960s. It'd be great if Isabelle could also catch up...:)
p.p.s. Also, the LaTeX generated from my .thy by "isatool make"
doesn't typeset !, ?, --> etc with the proper LaTeX symbols. Is there
any way to turn that on, without rewriting my sources with \<forall>
etc?
Email Gateway (Aug 18 2022 at 11:09):From: Tobias Nipkow <nipkow@in.tum.de>
You cannot quote type abbreviations but definitions work: @{thm f_def}
You may also want to look at "LaTeX sugar for proof documents"
http://isabelle.in.tum.de/dist/Isabelle/doc/sugar.pdf
There is no way to display "!" etc as \forall, you need to write it that
way in the first place - it's a subtle issue.
Tobias
Peter Sewell wrote:
Email Gateway (Aug 18 2022 at 11:09):From: Peter Sewell <Peter.Sewell@cl.cam.ac.uk>
You cannot quote type abbreviations but definitions work: @{thm f_def}
I hadn't thought of that, but it destroys the line breaks and
indentation, so it looks like the only real option is to cut-and-paste
from the generated LaTeX :( A crude but very useful thing we do in
Ott, which maybe could be done by Isabelle with minimal effort, is to
factor generated LaTeX into definitions of separate LaTeX commands
to generate each component of the output, with a predictable naming
convention - e.g.
\newcommand{\myisadatatypeXXXdirn}{dirn\ {\isacharequal}\ R\ {\isacharbar}\ W}
in one file, with
\isanewline
\isacommand{datatype}\isamarkupfalse%
\ \myisadatatypeXXXdirn\ \ \ \isanewline
\isanewline
in another, instead of
\isanewline
\isacommand{datatype}\isamarkupfalse%
\ dirn\ {\isacharequal}\ R\ {\isacharbar}\ W\ \ \ \isanewline
\isanewline
You may also want to look at "LaTeX sugar for proof documents"
http://isabelle.in.tum.de/dist/Isabelle/doc/sugar.pdf
y - seen that, which looks useful indeed.
There is no way to display "!" etc as \forall, you need to write it that
way in the first place - it's a subtle issue.
thanks,
Peter
Email Gateway (Aug 18 2022 at 11:09):From: Makarius <makarius@sketis.net>
On Fri, 14 Dec 2007, Peter Sewell wrote:
into
\newcommand{\myisadatatypeXXXdirn}{dirn\ {\isacharequal}\ R\ {\isacharbar}\ W}
This does not work in general, because the presentation system does not
know about the syntax of individual commands. Even if we pretend to know
the particular datatype syntax, what happens with mutual datatype
definitions, for example?
Then the user can LaTeX-include the first file and write just
\myisadatatypeXXXdirn
whereever they need to quote that defn.
This also does not work, because specifications of name bindings do not
identify the resulting internal object uniquely. E.g. there could be
several "dirn" types in different name spaces, local scopes etc.
The Isabelle document preparation might look crude at first sight, but it
is indeed very sophisticated: it manages to get 99% of typesetting quality
with only 1% of knowledge about the structure of the sources.
See also chapter 2 of the Isabelle system manual for the general
explanation on how things really work. The gory details can then be
glimpsed from the Isabelle style files and the generated LaTeX.
If you really want to move around portions of typeset text, you can try to
find a LaTeX package that allows to move marked regions. You can then let
Isabelle insert the required markup either via the 'text_raw' command or
using the new %tag facility, which is also explained in the manual.
Makarius
Email Gateway (Aug 18 2022 at 11:09):From: Thomas Bleher <ThomasBleher@gmx.de>
The attached crude perl script takes a number of theory files as input,
parses them (well, not really, but enough for my purposes) and creates
text_raw {* *} blocks in which it defines appropriate LaTeX commands.
So if you have a constdef foo it defines two LaTeX commands: \fooDef and
\fooDefInline (with different display options).
I put the output of the script into a new theory file with dependencies
on the original theories, processed it with Isabelle into a .tex file
and \included the resulting file into my main .tex file (after removing
the preamble and other unneeded stuff).
Worked very well for me.
Regards,
Thomas
generate_presentation_theorem
signature.asc
Last updated: May 03 2024 at 12:27 UTC