Stream: Beginner Questions

Topic: Name of the Language used in .thy files


view this post on Zulip Jia Hong Lee (Nov 13 2021 at 06:22):

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?

view this post on Zulip Wolfgang Jeltsch (Nov 13 2021 at 17:26):

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.

view this post on Zulip Jia Hong Lee (Nov 14 2021 at 01:35):

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

view this post on Zulip Jia Hong Lee (Nov 14 2021 at 01:40):

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?

view this post on Zulip Manuel Eberl (Nov 14 2021 at 10:59):

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

view this post on Zulip Jia Hong Lee (Nov 14 2021 at 12:29):

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.


Last updated: Jul 15 2022 at 23:21 UTC