Re: [isabelle] Syntax issue: lost between HOL and Isar
On 8/1/2012 9:18 PM, Christian Sternagel wrote:
- 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?)
My questions about syntax end up being the easy (easier, but not
completely answered) questions. Your reply below as to what HOL is as a
logic becomes the "not so easily understood" reply.
Here's what I found: Isar outer syntax is defined in
(* Title: Pure/Isar/isar_syn.ML
Author: Markus Wenzel, TU Muenchen
Isar/Pure outer syntax.
So Isar/Pure outer syntax is used to define inner syntax (I guess), such
as HOL's inner syntax, because in that file there are the usual Isar
commands that are documented in isar-ref.pdf:
line 154: Outer_Syntax.command ("judgement
line 158: Outer_Syntax.command ("consts
line 207: Outer_Syntax.command ("axioms
line 219: Outer_Syntax.command ("defs
line 228: Outer_Syntax.command ("definition
line 249: Outer_Syntax.local_theory ("notation
Well, life is not so simple. "datatype" is not specific to Isar. It's
defined in ~/src/HOL/Datatype.thy, and is somehow defined with
I type "datatype" without typing anything else, and I get the error
"Outer syntax error".
That's enough of that stuff for now.
- 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
Yea, so I guess we could do it all in ML, where ML is the language of
Your second two statements are the "something to think about".
This archive was generated by a fusion of
Pipermail (Mailman edition) and