Re: [isabelle] Syntax issue: lost between HOL and Isar
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and