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



Dear Gottfried,

On 08/02/2012 10:40 AM, Gottfried Barrow wrote:
Is this right? There's Isar syntax, which is defined in Pure. There's
HOL syntax, which is defined using Isar keywords. And there is the HOL
logic which is a combination of Isar syntax and HOL syntax.

What I'm thinking about in particular is that the proof of a HOL theorem
is a HOL proof, but it may contain Isar commands.
I would really prefer to hand this question over to a wizard ;)

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).

cheers

chris





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