Re: [isabelle] add_assoc, add.assoc and reflection



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


On 20/04/15 08:40, Walther Neuper wrote:
> 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
>





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