Hi, just to make it clear, what is the name of the language that one write inside a `.thy`

file? It is very ML-like, but I'm sure it's not Standard ML.

Is it called the Isabelle/HOL language or HOL language or Isabelle/Pure language or Pure language or Isar language?

I would say it’s the Isabelle language and would use the name Isabelle/Isar for the extensions for structured specifications and proofs that were introduced perhaps about 15–20 years ago. However, I have the impression that nowadays Isabelle/Isar stands for the whole language, including the less structured parts (the reference manual for what I’d call Isabelle is called The Isabelle/Isar Reference Manual).

Isabelle/Pure is Isabelle’s meta-logic, Isabelle/HOL is one of several object logics built on it.

Thanks, that makes sense, I'll go with the name "Isabelle/Isar" since the project pushes it as the de facto way of writing proof in Isabelle

Isabelle/Pure is Isabelle’s meta-logic, Isabelle/HOL is one of several object logics built on it.

It sounds like one can write other logic type/system(?) in Isabelle/Isar? E.g. can you write Isabelle/FOL or Isabelle/ZF in Isabelle/Isar?

Also note that you can define new commands at any time. All the commands when you see in a typical Isabelle theory (`definition`

, `lemma`

, `typedef`

, `fun`

, but also the Isar ones like `have`

, `obtain`

) are not part of some fixed language, but in a sense ‘user-defined’.

Hi, that's quite a confusing and yet enlightening statement.

That said, after `Ctrl-<Left-click>`

around, I can see that most commands I use in a `.thy`

file are defined in Isabelle/Pure. Then Isabelle/Isar is built on-top of Isabelle/Pure. So, I'll just think that I'm writing Isabelle/Isar (together with commands exposed from the lower Isabelle/Pure level). As you mention, I can defined my own commands in Isabelle/Isar. I'll see this as its language feature.

So, I guess my question is solved in some sense.

Jia Hong Lee has marked this topic as resolved.

Jia Hong Lee said:

It sounds like one can write other logic type/system(?) in Isabelle/Isar? E.g. can you write Isabelle/FOL or Isabelle/ZF in Isabelle/Isar?

Yes, you can. The translation of Isar constructs into logical constructs uses only logical operators of Isabelle/Pure.

Jia Hong Lee said:

Thanks, that makes sense, I'll go with the name "Isabelle/Isar" since the project pushes it as the de facto way of writing proof in Isabelle

If you’re aiming at using the structured constructs whereever possible, which is what I would recommend, it’s perfectly fair to say you’re writing in Isabelle/Isar, I guess.

Thanks for your input! You make it even clearer for me to comprehend =D

Last updated: Feb 27 2024 at 08:17 UTC