Email Gateway (Aug 18 2022 at 11:53): Email Gateway (Aug 18 2022 at 11:53):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
Hi all,
I am preparing a paper based on some of my Isabelle theories with the
isatool facility to generate LaTeX. A problem that I am frequently
facing is that I want to hide the constant name completely from the
paper and just fancy notation. However, I often do not want to supply
all parameters to some function and still get the notation.
For example, suppose there are two definitions, one of which is with
mixfix syntax, and some text...
definition foo :: "'a => 'b => 'c => bool"
("_ |- _ : _ *" [50, 0, 20] 70)
where "a |- b : c * == True"
definition bar :: "'a => ('a => 'b => 'c => bool) => bool"
where "bar a f == !b c. f a b c"
text {*
@{term "foo a b"} is a predicate on @{typ 'c} saying that ...
@{term "bar a foo"} denotes that @{term "foo a"} holds everywhere.
*}
What I would like the text to be typeset (with appropriate LaTeX symbols
instead of the ASCII art) is:
"a |- b : _ * is a predicate on 'c saying that ...
bar a (_ |- _ : _ *) denotes that a |- _ : _ * holds everywhere."
I.e. I would like to have the mixfix syntax printed even though foo is
not given all parameters. Those parameters which are missing should be
replaced by some placeholder (like _, but . or \cdot would equally do.
The simple way would clearly be to write @{text "a |- b : _ *"}, but in
thm-antiquotations, this trick does not work, e.g.
lemma foo: "foo a b = (%x. True)"
by(auto intro: ext simp add: foo_def)
text {* @{thm foo} *}
should produce "?a |- ?b : _ * = (%x. True)".
How can I have "foo" (automatically) translated to "_ |- _ : _ *", "foo
a" to "a |- _ : _ *", "foo a b" to "a |- b : _ *" and so on?
Thanks in advance,
Andreas
Email Gateway (Aug 18 2022 at 11:53):From: Tobias Nipkow <nipkow@in.tum.de>
I don't think there is any way to achieve automatically what you want.
Certainly not for thm antiquotations. For terms you need to write what
you suggested: @{text "foo a _"} (or @{term "foo a DUMMY"}, where DUMMY
is defined in LaTeXsugar for such purposes.)
You can print the thm "foo a b = (%x. True)" as "foo a b _ = True" as
follows: @{thm foo[THEN ext, OF _ _ DUMMY]} - hope I got that right.
Tobias
Andreas Lochbihler wrote:
Last updated: May 03 2024 at 08:18 UTC