Re: [isabelle] Mixfix syntax with fewer arguments

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:

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?