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



On 8/1/2012 9:18 PM, Christian Sternagel wrote:
But let me give it a try. What I think (but that does not necessarily mean that it's true) is the following:

- Pure is a kind of minimal logic independent from Isar.
- Isar syntax is not part of Pure, but the "Isar-language" is well-integrated on top of Pure. - HOL syntax is defined via commands (not sure whether those are really part of Isar or rather independent; my guess would be that they are just convenience tools built on top of the Isabelle/ML layer... but then, what is not?)
- HOL as a logic is independent from Isar.
- Proofs are irrelevant, thus they can't be part of the logic, i.e., they are not part of HOL. - In the end, a proof is just a step-wise manipulation of the abstract data type 'thm' through a well-defined interface (sometimes called the trusted Kernel).

Chris, thanks for the explanation. There's lots of interesting information there, but I reduced everything down to this statement, "I just want to know what word to use for Isabelle's programming language". I was in doubt for a while, and then it occurred to me, "Oh yea, it is called the Isar reference manual".

In Chapter 5, page 76, it says, "Isabelle/Isar theories are defined via theory files..." It then says that "theory" and "end" are Isar commands.

As far as I'm concerned, everything between "theory" and "end" is the Isar programming language. There is the ML in the "ML{ ... }", but other than that, it's all Isar to me now.

Regards,
GB







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