[isabelle] Mixfix syntax with fewer arguments



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.