Discussion:
[isabelle] syntax issue in document preparation
(too old to reply)
Gergely Buday
2014-12-30 16:42:17 UTC
Permalink
Hi,

in Nominal/Ex/Lambda.thy a proof command refers to path.induct . Now I
cannot use

@{term path.induct}

in a proof document as it fails, but

@{term path_induct}

which works but I wonder as it does not exist as a valid term.

Do I not understand something important about terms and antiquotations?

- Gergely
C. Diekmann
2014-12-30 17:28:34 UTC
Permalink
Hi,

In my Isabelle2014, I did not find the file, so I tried to reproduce a
minimal example for you.

theory Scratch
imports Main
begin

fun test :: "nat ⇒ nat" where
"test 0 = 0" |
"test (Suc n) = test n"

text{*Undefined constant: @{term test.induct}.*} (*Isabelle2014
highlights the error in jEdit, without running latex*)
text{*You can use the term antiquotation to display terms: @{term
"test 0 = 0"} *}
text{*The term antiquotation checks for errors: @{term "test 0 = -1"}
*} (*Type unification failed: No type arity nat :: uminus*)
text{*You can use the text antiquotation to do things without checks:
@{text "test 0 = -1"}*}
thm test.induct
text{*If you want to reference facts (things you can also view with
the thm command in Isabelle), use the thm antiquotation: @{thm
test.induct}*}

end

Happy New Year
Cornelius
Post by Gergely Buday
Hi,
in Nominal/Ex/Lambda.thy a proof command refers to path.induct . Now I
cannot use
@{term path.induct}
in a proof document as it fails, but
@{term path_induct}
which works but I wonder as it does not exist as a valid term.
Do I not understand something important about terms and antiquotations?
- Gergely
Christian Sternagel
2014-12-30 18:47:25 UTC
Permalink
Dear Gergely,

maybe you wanted to type

@{thm path.induct}

which would work, since "path.induct" is the name of a theorem (from the
nominal2 repository, which I'm just guessing you are referring to).

The reason why @{term path_induct} works (even though, no constant of
this name exists), is that it fits the "ident" token category (see
isar-ref, ~ page 51) and is just interpreted as some variable, while
"path.induct" is of category "longident" (which is not allowed for
variables, I think) and thus interpreted as constant name.

This difference is also visible in Isabelle/jEdit, where in

@{term path_induct}

"path_induct" is blue (and identified as "free variable" by C-hover) and in

@{term path.induct}

"path.induct" is black (and identified as belonging to the term language
by C-hover).

cheers

chris
Post by Gergely Buday
Hi,
in Nominal/Ex/Lambda.thy a proof command refers to path.induct . Now I
cannot use
@{term path.induct}
in a proof document as it fails, but
@{term path_induct}
which works but I wonder as it does not exist as a valid term.
Do I not understand something important about terms and antiquotations?
- Gergely
Gergely Buday
2014-12-30 19:02:00 UTC
Permalink
Post by Christian Sternagel
maybe you wanted to type
@{thm path.induct}
which would work, since "path.induct" is the name of a theorem (from the
nominal2 repository, which I'm just guessing you are referring to).
Sorry I did not include a rationale for this. My aim is a list that
contains theorem names and the theorems itself. First I used plain
text but the underscores in theorem names break latex typesetting as
it thinks as if it were some subscript and missing the math mode $.
Replacing underscores with backslash-underscore is tedious by hand. So
I tried the following scheme:

\item @{term alpha_lst} @{thm alpha_lst}

Should I use another antiquotation keyword for such theorem names as
path.induct? It would be nice if Isabelle checked its validity.

- Gergely
Christian Sternagel
2014-12-30 19:24:31 UTC
Permalink
I think @{thm [source] some_theorem_name} might work (i.e., print the
name instead of the theorem statement; but it has been a while since I
used this and I haven't had time to check).

cheers

chris
Post by Gergely Buday
Post by Christian Sternagel
maybe you wanted to type
@{thm path.induct}
which would work, since "path.induct" is the name of a theorem (from the
nominal2 repository, which I'm just guessing you are referring to).
Sorry I did not include a rationale for this. My aim is a list that
contains theorem names and the theorems itself. First I used plain
text but the underscores in theorem names break latex typesetting as
it thinks as if it were some subscript and missing the math mode $.
Replacing underscores with backslash-underscore is tedious by hand. So
Should I use another antiquotation keyword for such theorem names as
path.induct? It would be nice if Isabelle checked its validity.
- Gergely
Gerwin Klein
2014-12-30 23:02:09 UTC
Permalink
Yes, @{thm [source] name} is the way to do it.

Cheers,
Gerwin
Post by Christian Sternagel
cheers
chris
Post by Gergely Buday
Post by Christian Sternagel
maybe you wanted to type
@{thm path.induct}
which would work, since "path.induct" is the name of a theorem (from the
nominal2 repository, which I'm just guessing you are referring to).
Sorry I did not include a rationale for this. My aim is a list that
contains theorem names and the theorems itself. First I used plain
text but the underscores in theorem names break latex typesetting as
it thinks as if it were some subscript and missing the math mode $.
Replacing underscores with backslash-underscore is tedious by hand. So
Should I use another antiquotation keyword for such theorem names as
path.induct? It would be nice if Isabelle checked its validity.
- Gergely
________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Makarius
2014-12-31 10:54:43 UTC
Permalink
My aim is a list that contains theorem names and the theorems itself.
First I used plain text but the underscores in theorem names break latex
typesetting as it thinks as if it were some subscript and missing the
math mode $. Replacing underscores with backslash-underscore is tedious
by hand.
Such manual LaTeX-ing is indeed pointless in the Isabelle document
preparation system. If you need unchecked text that looks like formal
text, the @{text} antiquotation can do that.


Makarius

----------------------------------------------------------------------------
http://stop-ttip.org 1,236,823 Participants
----------------------------------------------------------------------------
Loading...