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 ~/src/Pure/isar_syn.ML.

(*  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
etc.

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 ~/src/HOL/Tools/Datatype/datatype.ML.

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

Yea, so I guess we could do it all in ML, where ML is the language of the foundation.

Your second two statements are the "something to think about".

Regards,
GB






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