Email Gateway (Aug 22 2022 at 09:17): Email Gateway (Aug 22 2022 at 09:17):From: Walther Neuper <wneuper@ist.tugraz.at>
Looking at
val ctxt = Proof_Context.init_global @{theory Main};
Syntax.read_term ctxt "add_assoc"
(* = Free ("add_assoc", "'a"): term *)
Syntax.read_term ctxt "add.assoc"
(* ERROR: Undefined constant: "add.assoc"*)
is my assumption right, that the latter is considered outer syntax only?
In other words: The latter is NOT considered to become a valid term
(i.e. inner syntax) within some context ?
If both questions are answered "yes", then this question comes up: How
comes that the designers of Isabelle are sure, that theorem names never
shall occur in functions defined within Isabelle's function package
(where function definitions are terms, i.e. belong to inner syntax) ?
And how does that design decision relate to the announcement of
"Eisbach, a new sub-language for Isabelle which allows users to write
automated reasoning techniques with high-level syntax, avoiding the
necessity of descending into ML"?
Walther
Email Gateway (Aug 22 2022 at 09:17):From: Manuel Eberl <eberlm@in.tum.de>
There /is/ a context in which the latter becomes a valid term.
add_assoc and add.assoc are both valid inner syntax names. Both of them
can denote constants; add_assoc can even be a free or bound variable.
Nothing prevents you from declaring a function called "add_assoc", or
calling variables in your lemmas "add_assoc".
add.assoc is a bit different due to the qualifying dot in the name; that
is why add_assoc, in your example, is considered a free variable and
add.assoc returns an error. "add.assoc" is not a valid name for a free
or bound variable. You can, however, easily define a locale "add" and a
function "assoc" in it, resulting in a constant called "add.assoc", and
then your example does not return an error:
locale add
begin
fun assoc where "assoc x = x"
end
ML_val {* Syntax.read_term @{context} "add.assoc" *}
val it = Const ("Scratch.add.assoc", "'a ⇒ 'a"): term
So I suppose the answer to your question is: theorem names /can/ occur
in inner syntax, but then they do not refer to theorems; they are just
names like any other, because the inner syntax does not know anything
about theorems or theorem names. The name "add_assoc" is a priori no
different from the name "x", and "add.assoc" no different from
"foo.bar", even though the former are fact names.
How that relates to Eisbach I cannot say, since I don't know the first
thing about Eisbach. I would, however, imagine that Eisbach also has the
strict separation between outer level (lemmas, definitions, etc.) and
inner level (object logic terms) and therefore your question does not
affect Eisbach at all.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 09:17):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
I can confirm that part. There’s nothing special about Eisbach in that respect.
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 22 2022 at 09:18):From: Makarius <makarius@sketis.net>
Isabelle is not Coq or PVS. There is not just one big lambda calculus to
assimilate everything, but we have arbitrarily nested languages and
syntaxes.
Name spaces are strictly separate for each "kind" of things. The syntax
is usually done in a way that the distinction of kinds is clear from how
the text is written. E.g. fact expressions refer to attributes and
theorems in a certain way, and cannot be mistaken as terms, for example.
The main exception to the syntactic distinction of kinds is the inner term
language: consts, frees, bounds can all look the same in the syntax, but
are later distinguished by their scope.
The main meta-problem on this thread might be actually an expectation of
something complicated, but the situation is quite plain and simple. And
after decades of reforms of the system implementation it should all work
out smoothly, including arbitrary nesting of languages.
If you want do implement something like that yourself, you can take the
"rail" language for syntax diagrams as an example (see
~~/src/Pure/Tools/rail.ML). It has the advantage that it is rather small,
and has no connection to logic or lambda calculus to get confused. There
is also a fair amount of IDE support just from the few canonical things
done in that module; e.g. see uses of @{rail} in ~~/src/Doc/.
Makarius
Email Gateway (Aug 22 2022 at 09:18):From: Walther Neuper <wneuper@ist.tugraz.at>
Thank you for the explanations
Name spaces are strictly separate for each "kind" of things. The
syntax is usually done in a way that the distinction of kinds is clear
from how the text is written. E.g. fact expressions refer to
attributes and theorems in a certain way, and cannot be mistaken as
terms, for example.
and
So I suppose the answer to your question is: theorem names /can/ occur
in inner syntax, but then they do not refer to theorems;
while with respect to the following
The main meta-problem on this thread might be actually an expectation
of something complicated, but the situation is quite plain and
simple. And after decades of reforms of the system implementation it
should all work out smoothly, including arbitrary nesting of languages.
some smoothness is lost in case one uses Isabelle not anticipated by
design, for instance Lucas-Interpretation [1]: Here programs [2] contain
theorem names, which are turned into theorems by functions available in
Isabelle; this now requires additional conversion [3].
So thanks a lot for all the replies -- they tell us about prospects on
Eisbach.
Walther
[1] http://eptcs.web.cse.unsw.edu.au/paper.cgi?THedu11.5
[2] We plan to employ Isabelle's function package for that purpose.
[3] https://intra.ist.tugraz.at/hg/isa/rev/419308245588
Last updated: Apr 19 2024 at 08:19 UTC