Re: [isabelle] Syntax issue: lost between HOL and Isar

On 8/2/2012 10:42 AM, Lars Noschinski wrote:
On 02.08.2012 15:58, Gottfried Barrow wrote:
So some HOL syntax is defined with Isar commands, and some HOL syntax is
defined with ML, where some HOL syntax is added as outer syntax.

"HOL syntax" is not a very useful term here. In Isabelle/Isar, we distinguish between outer and inner syntax. The inner syntax is the syntax used to input terms (and types). Apart from trivial cases, inner syntax needs to be quoted.

Lars, I sent the last email before I got this one. But in prog-prove, Tobias says,

"When Isabelle prints a syntax error message, it refers to the HOL syntax as the inner syntax
   and the enclosing theory language as the outer syntax."

I'm trying to pin down "what is the Isar programming language". I want to speak of one programming language, "Isar", but if it's not that simple, then I want to be more sophisticated about it.

I understand that between "theory MyTheory" and "end" in "MyTheory.thy" there are things like Latex and ML. But I can consider any of that as part of an argument to an Isar command like "ML{ .... }" or "text{ ... }". I'm trying to figure out if there's anything between "theory" and "end" that someone would have to say, "Most of what's between 'theory' and 'end' is Isar, but there are exceptions."

The outer syntax is everything else. Most of it is already part of Pure (i.e. independent of any logic), mainly everything which makes up proof and document structure; but logics often add additional commands for logic-specific operations (e.g. "fun" and "inductive" for HOL).

But if you can't combine "HOL syntax" with "inner syntax" and "outer syntax", then it makes it hard to talk about what's specific to HOL. There's the HOL specific outer syntax "datatype". I want to call that "HOL syntax", or at least "HOL outer syntax".

Both syntaxes can be extended, but after bootstrapping, the outer syntax usually stays pretty static; where as the inner syntax is changed with any definition or syntax annotation you issue. I think, by default there is no tool on the Isar level which would modify the outer syntax (just as there is no construct on the term level, which would modify the inner syntax).

This brings up "Outer_syntax.command", which I mentioned in the email I sent out before this one.

I'm going to call "Outer_syntax.command" an Isar command, and it's used in Datatype.thy to define "datatype" as outer syntax. If I don't call it an Isar command, then what am I going to call it? If I call it an ML command or a Pure command, then I can't say that Isar is the programming language that's being used to define "datatype". If that's the case, then there's a lower level programming language that I'm using. If there is, I want to know what to call it.


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