Email Gateway (Aug 19 2022 at 16:43): Email Gateway (Aug 19 2022 at 16:43):From: Gergely Buday <gbuday@gmail.com>
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?
Email Gateway (Aug 19 2022 at 16:43):From: "C. Diekmann" <diekmann@in.tum.de>
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
Email Gateway (Aug 19 2022 at 16:43):From: Christian Sternagel <c.sternagel@gmail.com>
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
Email Gateway (Aug 19 2022 at 16:43):From: Gergely Buday <gbuday@gmail.com>
Christian Sternagel wrote:
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.
Email Gateway (Aug 19 2022 at 16:43):From: Christian Sternagel <c.sternagel@gmail.com>
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
Email Gateway (Aug 19 2022 at 16:43):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Yes, @{thm [source] name} is the way to do it.
Cheers,
Gerwin
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.
Email Gateway (Aug 19 2022 at 16:44):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 19 2024 at 12:27 UTC